%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW840_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:03 PM UTC 2026 % Result : Timeout 300.12s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW840_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n001.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 14:38:24 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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.16/0.73 % (395366)Will run a generic schedule for satisfiability detection. % 3.16/0.73 % (395376)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1897249911:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.16/0.73 % (395372)% WARNING: option uhcvi not known. % 3.16/0.73 % (395371)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=101309074_2999 on theBenchmark for (2999ds/0Mi) % 3.16/0.73 % (395372)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=86982012:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.16/0.73 % (395373)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2967925185:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.16/0.73 % (395374)dis+10_1_sil=32000:sp=arity:random_seed=1147813196:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.16/0.73 % (395375)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3512879232:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.16/0.73 % (395377)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=273810336:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.16/0.73 % (395371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.16/0.73 % (395371)Terminated due to inappropriate strategy. % 3.16/0.73 % (395371)------------------------------ % 3.16/0.73 % (395371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.16/0.73 % (395371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.16/0.73 % (395371)CaDiCaL version: 2.1.3 % 3.16/0.73 % (395371)Termination reason: Inappropriate % 3.16/0.73 % (395371)Time elapsed: 0.028 s % 3.16/0.73 % (395371)Peak memory usage: 12 MB % 3.16/0.73 % (395371)Instructions burned: 61 (million) % 3.16/0.73 % (395371)------------------------------ % 3.16/0.73 % (395371)------------------------------ % 3.16/0.73 % (395376)Instruction limit reached! % 3.16/0.73 % (395376)------------------------------ % 3.16/0.73 % (395376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.16/0.73 % (395376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.16/0.73 % (395376)CaDiCaL version: 2.1.3 % 3.16/0.73 % (395376)Termination reason: Instruction limit % 3.16/0.73 % (395376)Termination phase: Saturation % 3.16/0.73 % (395376)Time elapsed: 0.040 s % 3.16/0.73 % (395376)Peak memory usage: 14 MB % 3.16/0.73 % (395376)Instructions burned: 134 (million) % 3.16/0.73 % (395386)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4058175623:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.16/0.73 % (395385)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3564720666:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.16/0.73 % (395374)Instruction limit reached! % 3.16/0.73 % (395374)------------------------------ % 3.16/0.73 % (395374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.16/0.73 % (395374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.16/0.73 % (395374)CaDiCaL version: 2.1.3 % 3.16/0.73 % (395374)Termination reason: Instruction limit % 3.16/0.73 % (395374)Termination phase: Saturation % 3.16/0.73 % (395374)Time elapsed: 0.055 s % 3.16/0.73 % (395374)Peak memory usage: 13 MB % 3.16/0.73 % (395374)Instructions burned: 104 (million) % 3.16/0.73 % (395375)Instruction limit reached! % 3.16/0.73 % (395375)------------------------------ % 3.16/0.73 % (395375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.16/0.73 % (395375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.16/0.73 % (395375)CaDiCaL version: 2.1.3 % 3.16/0.73 % (395375)Termination reason: Instruction limit % 3.16/0.73 % (395375)Termination phase: Saturation % 3.16/0.73 % (395375)Time elapsed: 0.060 s % 3.16/0.73 % (395375)Peak memory usage: 14 MB % 3.16/0.73 % (395375)Instructions burned: 117 (million) % 3.16/0.73 % (395389)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=3088237657:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.16/0.73 % (395385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.16/0.73 % (395385)Terminated due to inappropriate strategy. % 3.16/0.73 % (395385)------------------------------ % 3.16/0.73 % (395385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.16/0.73 % (395385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395385)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395385)Termination reason: Inappropriate % 7.20/1.30 % (395385)Time elapsed: 0.029 s % 7.20/1.30 % (395385)Peak memory usage: 12 MB % 7.20/1.30 % (395385)Instructions burned: 60 (million) % 7.20/1.30 % (395390)ott-21_1_sil=16000:fs=off:random_seed=3094398967:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.20/1.30 % (395385)------------------------------ % 7.20/1.30 % (395385)------------------------------ % 7.20/1.30 % (395386)Instruction limit reached! % 7.20/1.30 % (395386)------------------------------ % 7.20/1.30 % (395386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.20/1.30 % (395386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395386)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395386)Termination reason: Instruction limit % 7.20/1.30 % (395386)Termination phase: Saturation % 7.20/1.30 % (395386)Time elapsed: 0.039 s % 7.20/1.30 % (395386)Peak memory usage: 14 MB % 7.20/1.30 % (395386)Instructions burned: 133 (million) % 7.20/1.30 % (395394)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=265240206:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.20/1.30 % (395377)Instruction limit reached! % 7.20/1.30 % (395377)------------------------------ % 7.20/1.30 % (395377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.20/1.30 % (395377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395377)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395377)Termination reason: Instruction limit % 7.20/1.30 % (395377)Termination phase: Saturation % 7.20/1.30 % (395377)Time elapsed: 0.095 s % 7.20/1.30 % (395377)Peak memory usage: 14 MB % 7.20/1.30 % (395377)Instructions burned: 160 (million) % 7.20/1.30 % (395393)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2527400070:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.20/1.30 % (395394)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.20/1.30 % (395394)Terminated due to inappropriate strategy. % 7.20/1.30 % (395394)------------------------------ % 7.20/1.30 % (395394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.20/1.30 % (395394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395394)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395394)Termination reason: Inappropriate % 7.20/1.30 % (395394)Time elapsed: 0.014 s % 7.20/1.30 % (395394)Peak memory usage: 12 MB % 7.20/1.30 % (395394)Instructions burned: 60 (million) % 7.20/1.30 % (395394)------------------------------ % 7.20/1.30 % (395394)------------------------------ % 7.20/1.30 % (395396)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=519140430:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.20/1.30 % (395398)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3665042141:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.20/1.30 % (395398)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.20/1.30 % (395398)Terminated due to inappropriate strategy. % 7.20/1.30 % (395398)------------------------------ % 7.20/1.30 % (395398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.20/1.30 % (395398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395398)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395398)Termination reason: Inappropriate % 7.20/1.30 % (395398)Time elapsed: 0.015 s % 7.20/1.30 % (395398)Peak memory usage: 12 MB % 7.20/1.30 % (395398)Instructions burned: 61 (million) % 7.20/1.30 % (395398)------------------------------ % 7.20/1.30 % (395398)------------------------------ % 7.20/1.30 % (395401)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=2092505715: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) % 7.20/1.30 % (395390)Instruction limit reached! % 7.20/1.30 % (395390)------------------------------ % 7.20/1.30 % (395390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.20/1.30 % (395390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.30 % (395390)CaDiCaL version: 2.1.3 % 7.20/1.30 % (395390)Termination reason: Instruction limit % 7.20/1.30 % (395390)Termination phase: Saturation % 7.20/1.30 % (395390)Time elapsed: 0.084 s % 7.20/1.30 % (395390)Peak memory usage: 14 MB % 7.20/1.30 % (395390)Instructions burned: 181 (million) % 21.57/3.33 % (395403)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3749428709:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.57/3.33 % (395401)Instruction limit reached! % 21.57/3.33 % (395401)------------------------------ % 21.57/3.33 % (395401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395401)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395401)Termination reason: Instruction limit % 21.57/3.33 % (395401)Termination phase: Saturation % 21.57/3.33 % (395401)Time elapsed: 0.221 s % 21.57/3.33 % (395401)Peak memory usage: 20 MB % 21.57/3.33 % (395401)Instructions burned: 694 (million) % 21.57/3.33 % (395405)fmb+10_1_sil=64000:random_seed=1708088721:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.57/3.33 % (395393)Instruction limit reached! % 21.57/3.33 % (395393)------------------------------ % 21.57/3.33 % (395393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395393)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395393)Termination reason: Instruction limit % 21.57/3.33 % (395393)Termination phase: Saturation % 21.57/3.33 % (395393)Time elapsed: 0.293 s % 21.57/3.33 % (395393)Peak memory usage: 16 MB % 21.57/3.33 % (395393)Instructions burned: 477 (million) % 21.57/3.33 % (395405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.57/3.33 % (395405)Terminated due to inappropriate strategy. % 21.57/3.33 % (395405)------------------------------ % 21.57/3.33 % (395405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395405)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395405)Termination reason: Inappropriate % 21.57/3.33 % (395405)Time elapsed: 0.015 s % 21.57/3.33 % (395405)Peak memory usage: 12 MB % 21.57/3.33 % (395405)Instructions burned: 60 (million) % 21.57/3.33 % (395405)------------------------------ % 21.57/3.33 % (395405)------------------------------ % 21.57/3.33 % (395408)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3602767612:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 21.57/3.33 % (395407)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1378837641:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.57/3.33 % (395408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.57/3.33 % (395408)Terminated due to inappropriate strategy. % 21.57/3.33 % (395408)------------------------------ % 21.57/3.33 % (395408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395408)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395408)Termination reason: Inappropriate % 21.57/3.33 % (395408)Time elapsed: 0.015 s % 21.57/3.33 % (395408)Peak memory usage: 12 MB % 21.57/3.33 % (395408)Instructions burned: 60 (million) % 21.57/3.33 % (395408)------------------------------ % 21.57/3.33 % (395408)------------------------------ % 21.57/3.33 % (395389)Instruction limit reached! % 21.57/3.33 % (395389)------------------------------ % 21.57/3.33 % (395389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395389)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395389)Termination reason: Instruction limit % 21.57/3.33 % (395389)Termination phase: Saturation % 21.57/3.33 % (395389)Time elapsed: 0.354 s % 21.57/3.33 % (395389)Peak memory usage: 17 MB % 21.57/3.33 % (395389)Instructions burned: 684 (million) % 21.57/3.33 % (395407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.57/3.33 % (395407)Terminated due to inappropriate strategy. % 21.57/3.33 % (395407)------------------------------ % 21.57/3.33 % (395407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.57/3.33 % (395407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.57/3.33 % (395407)CaDiCaL version: 2.1.3 % 21.57/3.33 % (395407)Termination reason: Inappropriate % 21.57/3.33 % (395407)Time elapsed: 0.028 s % 21.57/3.33 % (395407)Peak memory usage: 12 MB % 21.57/3.33 % (395407)Instructions burned: 60 (million) % 21.57/3.33 % (395411)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2636960050:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 24.99/3.90 % (395407)------------------------------ % 24.99/3.90 % (395407)------------------------------ % 24.99/3.90 % (395412)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3070341344:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 24.99/3.90 % (395414)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3561057233:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 24.99/3.90 % (395414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.99/3.90 % (395414)Terminated due to inappropriate strategy. % 24.99/3.90 % (395414)------------------------------ % 24.99/3.90 % (395414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.99/3.90 % (395414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.99/3.90 % (395414)CaDiCaL version: 2.1.3 % 24.99/3.90 % (395414)Termination reason: Inappropriate % 24.99/3.90 % (395414)Time elapsed: 0.028 s % 24.99/3.90 % (395414)Peak memory usage: 12 MB % 24.99/3.90 % (395414)Instructions burned: 61 (million) % 24.99/3.90 % (395414)------------------------------ % 24.99/3.90 % (395414)------------------------------ % 24.99/3.90 % (395417)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1157921094:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.99/3.90 % (395417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.99/3.90 % (395417)Terminated due to inappropriate strategy. % 24.99/3.90 % (395417)------------------------------ % 24.99/3.90 % (395417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.99/3.90 % (395417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.99/3.90 % (395417)CaDiCaL version: 2.1.3 % 24.99/3.90 % (395417)Termination reason: Inappropriate % 24.99/3.90 % (395417)Time elapsed: 0.028 s % 24.99/3.90 % (395417)Peak memory usage: 12 MB % 24.99/3.90 % (395417)Instructions burned: 60 (million) % 24.99/3.90 % (395417)------------------------------ % 24.99/3.90 % (395417)------------------------------ % 24.99/3.90 % (395419)ott-2_1_sil=16000:newcnf=on:random_seed=2921452740:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.99/3.90 % (395403)Instruction limit reached! % 24.99/3.90 % (395403)------------------------------ % 24.99/3.90 % (395403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.99/3.90 % (395403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.99/3.90 % (395403)CaDiCaL version: 2.1.3 % 24.99/3.90 % (395403)Termination reason: Instruction limit % 24.99/3.90 % (395403)Termination phase: Saturation % 24.99/3.90 % (395403)Time elapsed: 0.490 s % 24.99/3.90 % (395403)Peak memory usage: 20 MB % 24.99/3.90 % (395403)Instructions burned: 879 (million) % 24.99/3.90 % (395421)ott+10_1_sil=32000:tgt=ground:random_seed=3331323982:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 24.99/3.90 % (395396)Instruction limit reached! % 24.99/3.90 % (395396)------------------------------ % 24.99/3.90 % (395396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.99/3.90 % (395396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.99/3.90 % (395396)CaDiCaL version: 2.1.3 % 24.99/3.90 % (395396)Termination reason: Instruction limit % 24.99/3.90 % (395396)Termination phase: Saturation % 24.99/3.90 % (395396)Time elapsed: 0.638 s % 24.99/3.90 % (395396)Peak memory usage: 23 MB % 24.99/3.90 % (395396)Instructions burned: 1179 (million) % 24.99/3.90 % (395423)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2413189650:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 24.99/3.90 % (395423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.99/3.90 % (395423)Terminated due to inappropriate strategy. % 24.99/3.90 % (395423)------------------------------ % 24.99/3.90 % (395423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.99/3.90 % (395423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.99/3.90 % (395423)CaDiCaL version: 2.1.3 % 24.99/3.90 % (395423)Termination reason: Inappropriate % 24.99/3.90 % (395423)Time elapsed: 0.028 s % 24.99/3.90 % (395423)Peak memory usage: 12 MB % 24.99/3.90 % (395423)Instructions burned: 61 (million) % 24.99/3.90 % (395423)------------------------------ % 24.99/3.90 % (395423)------------------------------ % 24.99/3.90 % (395425)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2488737036:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 24.99/3.90 % (395419)Instruction limit reached! % 114.70/16.43 % (395419)------------------------------ % 114.70/16.43 % (395419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395419)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395419)Termination reason: Instruction limit % 114.70/16.43 % (395419)Termination phase: Saturation % 114.70/16.43 % (395419)Time elapsed: 0.449 s % 114.70/16.43 % (395419)Peak memory usage: 18 MB % 114.70/16.43 % (395419)Instructions burned: 870 (million) % 114.70/16.43 % (395427)dis+21_1_sil=32000:sas=cadical:random_seed=1151442047:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 114.70/16.43 % (395412)Instruction limit reached! % 114.70/16.43 % (395412)------------------------------ % 114.70/16.43 % (395412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395412)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395412)Termination reason: Instruction limit % 114.70/16.43 % (395412)Termination phase: Saturation % 114.70/16.43 % (395412)Time elapsed: 0.799 s % 114.70/16.43 % (395412)Peak memory usage: 31 MB % 114.70/16.43 % (395412)Instructions burned: 1472 (million) % 114.70/16.43 % (395429)ott+11_1_sil=16000:gs=on:random_seed=3511853146:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 114.70/16.43 % (395411)Instruction limit reached! % 114.70/16.43 % (395411)------------------------------ % 114.70/16.43 % (395411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395411)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395411)Termination reason: Instruction limit % 114.70/16.43 % (395411)Termination phase: Saturation % 114.70/16.43 % (395411)Time elapsed: 1.518 s % 114.70/16.43 % (395411)Peak memory usage: 43 MB % 114.70/16.43 % (395411)Instructions burned: 5131 (million) % 114.70/16.43 % (395431)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=23553947:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 114.70/16.43 % (395431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.70/16.43 % (395431)Terminated due to inappropriate strategy. % 114.70/16.43 % (395431)------------------------------ % 114.70/16.43 % (395431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395431)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395431)Termination reason: Inappropriate % 114.70/16.43 % (395431)Time elapsed: 0.015 s % 114.70/16.43 % (395431)Peak memory usage: 12 MB % 114.70/16.43 % (395431)Instructions burned: 60 (million) % 114.70/16.43 % (395431)------------------------------ % 114.70/16.43 % (395431)------------------------------ % 114.70/16.43 % (395433)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1130832665:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 114.70/16.43 % (395429)Instruction limit reached! % 114.70/16.43 % (395429)------------------------------ % 114.70/16.43 % (395429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395429)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395429)Termination reason: Instruction limit % 114.70/16.43 % (395429)Termination phase: Saturation % 114.70/16.43 % (395429)Time elapsed: 1.322 s % 114.70/16.43 % (395429)Peak memory usage: 32 MB % 114.70/16.43 % (395429)Instructions burned: 2252 (million) % 114.70/16.43 % (395435)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2338225446:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 114.70/16.43 % (395425)Instruction limit reached! % 114.70/16.43 % (395425)------------------------------ % 114.70/16.43 % (395425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.70/16.43 % (395425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.70/16.43 % (395425)CaDiCaL version: 2.1.3 % 114.70/16.43 % (395425)Termination reason: Instruction limit % 114.70/16.43 % (395425)Termination phase: Saturation % 114.70/16.43 % (395425)Time elapsed: 1.870 s % 114.70/16.43 % (395425)Peak memory usage: 39 MB % 114.70/16.43 % (395425)Instructions burned: 3513 (million) % 114.70/16.43 % (395437)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=113549681:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 114.70/16.43 % (395427)Instruction limit reached! % 155.84/22.23 % (395427)------------------------------ % 155.84/22.23 % (395427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395427)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395427)Termination reason: Instruction limit % 155.84/22.23 % (395427)Termination phase: Saturation % 155.84/22.23 % (395427)Time elapsed: 2.006 s % 155.84/22.23 % (395427)Peak memory usage: 40 MB % 155.84/22.23 % (395427)Instructions burned: 3775 (million) % 155.84/22.23 % (395439)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3735619716:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 155.84/22.23 % (395439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.84/22.23 % (395439)Terminated due to inappropriate strategy. % 155.84/22.23 % (395439)------------------------------ % 155.84/22.23 % (395439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395439)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395439)Termination reason: Inappropriate % 155.84/22.23 % (395439)Time elapsed: 0.028 s % 155.84/22.23 % (395439)Peak memory usage: 12 MB % 155.84/22.23 % (395439)Instructions burned: 60 (million) % 155.84/22.23 % (395439)------------------------------ % 155.84/22.23 % (395439)------------------------------ % 155.84/22.23 % (395441)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3183682136:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 155.84/22.23 % (395441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.84/22.23 % (395441)Terminated due to inappropriate strategy. % 155.84/22.23 % (395441)------------------------------ % 155.84/22.23 % (395441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395441)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395441)Termination reason: Inappropriate % 155.84/22.23 % (395441)Time elapsed: 0.028 s % 155.84/22.23 % (395441)Peak memory usage: 12 MB % 155.84/22.23 % (395441)Instructions burned: 60 (million) % 155.84/22.23 % (395441)------------------------------ % 155.84/22.23 % (395441)------------------------------ % 155.84/22.23 % (395433)Instruction limit reached! % 155.84/22.23 % (395433)------------------------------ % 155.84/22.23 % (395433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395433)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395433)Termination reason: Instruction limit % 155.84/22.23 % (395433)Termination phase: Saturation % 155.84/22.23 % (395433)Time elapsed: 1.156 s % 155.84/22.23 % (395433)Peak memory usage: 52 MB % 155.84/22.23 % (395433)Instructions burned: 4594 (million) % 155.84/22.23 % (395443)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2144384726:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 155.84/22.23 % (395445)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=971616401:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 155.84/22.23 % (395443)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.84/22.23 % (395443)Terminated due to inappropriate strategy. % 155.84/22.23 % (395443)------------------------------ % 155.84/22.23 % (395443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395443)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395443)Termination reason: Inappropriate % 155.84/22.23 % (395443)Time elapsed: 0.028 s % 155.84/22.23 % (395443)Peak memory usage: 12 MB % 155.84/22.23 % (395443)Instructions burned: 60 (million) % 155.84/22.23 % (395443)------------------------------ % 155.84/22.23 % (395443)------------------------------ % 155.84/22.23 % (395447)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2246903444:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 155.84/22.23 % (395421)Instruction limit reached! % 155.84/22.23 % (395421)------------------------------ % 155.84/22.23 % (395421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.84/22.23 % (395421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.84/22.23 % (395421)CaDiCaL version: 2.1.3 % 155.84/22.23 % (395421)Termination reason: Instruction limit % 155.84/22.23 % (395421)Termination phase: Saturation % 157.24/22.44 % (395421)Time elapsed: 2.911 s % 157.24/22.44 % (395421)Peak memory usage: 49 MB % 157.24/22.44 % (395421)Instructions burned: 5116 (million) % 157.24/22.44 % (395449)dis+10_16:1_sil=16000:random_seed=214210989:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 157.24/22.44 % (395437)Instruction limit reached! % 157.24/22.44 % (395437)------------------------------ % 157.24/22.44 % (395437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395437)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395437)Termination reason: Instruction limit % 157.24/22.44 % (395437)Termination phase: Saturation % 157.24/22.44 % (395437)Time elapsed: 2.801 s % 157.24/22.44 % (395437)Peak memory usage: 47 MB % 157.24/22.44 % (395437)Instructions burned: 5212 (million) % 157.24/22.44 % (395451)ott-3_8_sil=64000:random_seed=1558113778:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 157.24/22.44 % (395447)Instruction limit reached! % 157.24/22.44 % (395447)------------------------------ % 157.24/22.44 % (395447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395447)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395447)Termination reason: Instruction limit % 157.24/22.44 % (395447)Termination phase: Saturation % 157.24/22.44 % (395447)Time elapsed: 4.698 s % 157.24/22.44 % (395447)Peak memory usage: 68 MB % 157.24/22.44 % (395447)Instructions burned: 8173 (million) % 157.24/22.44 % (395569)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=710864146:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 157.24/22.44 % (395569)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.24/22.44 % (395569)Terminated due to inappropriate strategy. % 157.24/22.44 % (395569)------------------------------ % 157.24/22.44 % (395569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395569)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395569)Termination reason: Inappropriate % 157.24/22.44 % (395569)Time elapsed: 0.028 s % 157.24/22.44 % (395569)Peak memory usage: 12 MB % 157.24/22.44 % (395569)Instructions burned: 61 (million) % 157.24/22.44 % (395569)------------------------------ % 157.24/22.44 % (395569)------------------------------ % 157.24/22.44 % (395571)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2067732221:i=11404_2919 on theBenchmark for (2919ds/11404Mi) % 157.24/22.44 % (395449)Instruction limit reached! % 157.24/22.44 % (395449)------------------------------ % 157.24/22.44 % (395449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395449)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395449)Termination reason: Instruction limit % 157.24/22.44 % (395449)Termination phase: Saturation % 157.24/22.44 % (395449)Time elapsed: 4.676 s % 157.24/22.44 % (395449)Peak memory usage: 58 MB % 157.24/22.44 % (395449)Instructions burned: 9157 (million) % 157.24/22.44 % (395633)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2884253832:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 157.24/22.44 % (395445)Instruction limit reached! % 157.24/22.44 % (395445)------------------------------ % 157.24/22.44 % (395445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395445)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395445)Termination reason: Instruction limit % 157.24/22.44 % (395445)Termination phase: Saturation % 157.24/22.44 % (395445)Time elapsed: 6.209 s % 157.24/22.44 % (395445)Peak memory usage: 379 MB % 157.24/22.44 % (395445)Instructions burned: 22567 (million) % 157.24/22.44 % (395735)dis+33_16_sil=32000:sac=on:random_seed=2431187333:i=15851:nm=0_2905 on theBenchmark for (2905ds/15851Mi) % 157.24/22.44 % (395735)Instruction limit reached! % 157.24/22.44 % (395735)------------------------------ % 157.24/22.44 % (395735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.24/22.44 % (395735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.44 % (395735)CaDiCaL version: 2.1.3 % 157.24/22.44 % (395735)Termination reason: Instruction limit % 157.24/22.44 % (395735)Termination phase: Saturation % 157.24/22.44 % (395735)Time elapsed: 6.650 s % 157.24/22.44 % (395735)Peak memory usage: 19 MB % 157.24/22.44 % (395735)Instructions burned: 15852 (million) % 157.24/22.44 % (395765)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=80175849:avsq=on:i=17627:add=on:amm=off_2838 on theBenchmark for (2838ds/17627Mi) % 180.71/25.73 % (395571)Instruction limit reached! % 180.71/25.73 % (395571)------------------------------ % 180.71/25.73 % (395571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395571)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395571)Termination reason: Instruction limit % 180.71/25.73 % (395571)Termination phase: Saturation % 180.71/25.73 % (395571)Time elapsed: 10.704 s % 180.71/25.73 % (395571)Peak memory usage: 87 MB % 180.71/25.73 % (395571)Instructions burned: 11405 (million) % 180.71/25.73 % (395771)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3218884513:s2a=on:i=53295_2812 on theBenchmark for (2812ds/53295Mi) % 180.71/25.73 % (395451)Instruction limit reached! % 180.71/25.73 % (395451)------------------------------ % 180.71/25.73 % (395451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395451)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395451)Termination reason: Instruction limit % 180.71/25.73 % (395451)Termination phase: Saturation % 180.71/25.73 % (395451)Time elapsed: 14.409 s % 180.71/25.73 % (395451)Peak memory usage: 56 MB % 180.71/25.73 % (395451)Instructions burned: 20139 (million) % 180.71/25.73 % (395779)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1444478223:i=26857:ins=20_2799 on theBenchmark for (2799ds/26857Mi) % 180.71/25.73 % (395779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.71/25.73 % (395779)Terminated due to inappropriate strategy. % 180.71/25.73 % (395779)------------------------------ % 180.71/25.73 % (395779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395779)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395779)Termination reason: Inappropriate % 180.71/25.73 % (395779)Time elapsed: 0.037 s % 180.71/25.73 % (395779)Peak memory usage: 12 MB % 180.71/25.73 % (395779)Instructions burned: 60 (million) % 180.71/25.73 % (395779)------------------------------ % 180.71/25.73 % (395779)------------------------------ % 180.71/25.73 % (395781)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1881529380:i=28120:bs=on:fsr=off_2798 on theBenchmark for (2798ds/28120Mi) % 180.71/25.73 % (395633)Instruction limit reached! % 180.71/25.73 % (395633)------------------------------ % 180.71/25.73 % (395633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395633)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395633)Termination reason: Instruction limit % 180.71/25.73 % (395633)Termination phase: Saturation % 180.71/25.73 % (395633)Time elapsed: 13.452 s % 180.71/25.73 % (395633)Peak memory usage: 91 MB % 180.71/25.73 % (395633)Instructions burned: 14134 (million) % 180.71/25.73 % (395783)fmb+10_1_sil=256000:fmbss=7:random_seed=2562470502:fmbsr=1.6:i=182295_2781 on theBenchmark for (2781ds/182295Mi) % 180.71/25.73 % (395783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.71/25.73 % (395783)Terminated due to inappropriate strategy. % 180.71/25.73 % (395783)------------------------------ % 180.71/25.73 % (395783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395783)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395783)Termination reason: Inappropriate % 180.71/25.73 % (395783)Time elapsed: 0.055 s % 180.71/25.73 % (395783)Peak memory usage: 12 MB % 180.71/25.73 % (395783)Instructions burned: 60 (million) % 180.71/25.73 % (395783)------------------------------ % 180.71/25.73 % (395783)------------------------------ % 180.71/25.73 % (395785)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1254164384:i=44625:gsp=on_2780 on theBenchmark for (2780ds/44625Mi) % 180.71/25.73 % (395435)Instruction limit reached! % 180.71/25.73 % (395435)------------------------------ % 180.71/25.73 % (395435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.71/25.73 % (395435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.71/25.73 % (395435)CaDiCaL version: 2.1.3 % 180.71/25.73 % (395435)Termination reason: Instruction limit % 180.71/25.73 % (395435)Termination phase: Saturation % 180.71/25.73 % (395435)Time elapsed: 19.319 s % 180.71/25.73 % (395435)Peak memory usage: 50 MB % 202.07/28.72 % (395435)Instructions burned: 29341 (million) % 202.07/28.72 % (395785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.07/28.72 % (395785)Terminated due to inappropriate strategy. % 202.07/28.72 % (395785)------------------------------ % 202.07/28.72 % (395785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.07/28.72 % (395785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.07/28.72 % (395785)CaDiCaL version: 2.1.3 % 202.07/28.72 % (395785)Termination reason: Inappropriate % 202.07/28.72 % (395785)Time elapsed: 0.033 s % 202.07/28.72 % (395785)Peak memory usage: 12 MB % 202.07/28.72 % (395785)Instructions burned: 64 (million) % 202.07/28.72 % (395785)------------------------------ % 202.07/28.72 % (395785)------------------------------ % 202.07/28.72 % (395787)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3417425921:i=160505_2779 on theBenchmark for (2779ds/160505Mi) % 202.07/28.72 % (395788)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1945305745:fmbsr=1.3:i=225729_2779 on theBenchmark for (2779ds/225729Mi) % 202.07/28.72 % (395788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.07/28.72 % (395788)Terminated due to inappropriate strategy. % 202.07/28.72 % (395788)------------------------------ % 202.07/28.72 % (395788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.07/28.72 % (395788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.07/28.72 % (395788)CaDiCaL version: 2.1.3 % 202.07/28.72 % (395788)Termination reason: Inappropriate % 202.07/28.72 % (395788)Time elapsed: 0.045 s % 202.07/28.72 % (395788)Peak memory usage: 12 MB % 202.07/28.72 % (395788)Instructions burned: 60 (million) % 202.07/28.72 % (395788)------------------------------ % 202.07/28.72 % (395788)------------------------------ % 202.07/28.72 % (395787)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.07/28.72 % (395787)Terminated due to inappropriate strategy. % 202.07/28.72 % (395787)------------------------------ % 202.07/28.72 % (395787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.07/28.72 % (395787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.07/28.72 % (395787)CaDiCaL version: 2.1.3 % 202.07/28.72 % (395787)Termination reason: Inappropriate % 202.07/28.72 % (395787)Time elapsed: 0.055 s % 202.07/28.72 % (395787)Peak memory usage: 12 MB % 202.07/28.72 % (395787)Instructions burned: 60 (million) % 202.07/28.72 % (395787)------------------------------ % 202.07/28.72 % (395787)------------------------------ % 202.07/28.72 % (395792)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3517551330:rtra=on_2778 on theBenchmark for (2778ds/0Mi) % 202.07/28.72 % (395791)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3758554489:fmbsr=2:i=185024:ins=7_2778 on theBenchmark for (2778ds/185024Mi) % 202.07/28.72 % (395792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.07/28.72 % (395792)Terminated due to inappropriate strategy. % 202.07/28.72 % (395792)------------------------------ % 202.07/28.72 % (395792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.07/28.72 % (395792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.07/28.72 % (395792)CaDiCaL version: 2.1.3 % 202.07/28.72 % (395792)Termination reason: Inappropriate % 202.07/28.72 % (395792)Time elapsed: 0.040 s % 202.07/28.72 % (395792)Peak memory usage: 12 MB % 202.07/28.72 % (395792)Instructions burned: 66 (million) % 202.07/28.72 % (395792)------------------------------ % 202.07/28.72 % (395792)------------------------------ % 202.07/28.72 % (395795)% WARNING: option uhcvi not known. % 202.07/28.72 % (395791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.07/28.72 % (395791)Terminated due to inappropriate strategy. % 202.07/28.72 % (395791)------------------------------ % 202.07/28.72 % (395791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.07/28.72 % (395791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.07/28.72 % (395791)CaDiCaL version: 2.1.3 % 202.07/28.72 % (395791)Termination reason: Inappropriate % 202.07/28.72 % (395791)Time elapsed: 0.064 s % 202.07/28.72 % (395791)Peak memory usage: 12 MB % 202.07/28.72 % (395791)Instructions burned: 60 (million) % 202.07/28.72 % (395795)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3332600848:i=271062:add=off:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/271062Mi) % 202.07/28.72 % (395791)------------------------------ % 202.07/28.72 % (395791)------------------------------ % 216.85/30.84 % (395797)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=50003408:i=176048:add=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/176048Mi) % 216.85/30.84 % (395765)Instruction limit reached! % 216.85/30.84 % (395765)------------------------------ % 216.85/30.84 % (395765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395765)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395765)Termination reason: Instruction limit % 216.85/30.84 % (395765)Termination phase: Saturation % 216.85/30.84 % (395765)Time elapsed: 8.427 s % 216.85/30.84 % (395765)Peak memory usage: 196 MB % 216.85/30.84 % (395765)Instructions burned: 17628 (million) % 216.85/30.84 % (395801)dis+10_1_sil=32000:si=on:sp=arity:random_seed=844410665:i=206:fgj=on:rtra=on_2753 on theBenchmark for (2753ds/206Mi) % 216.85/30.84 % (395801)Instruction limit reached! % 216.85/30.84 % (395801)------------------------------ % 216.85/30.84 % (395801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395801)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395801)Termination reason: Instruction limit % 216.85/30.84 % (395801)Termination phase: Saturation % 216.85/30.84 % (395801)Time elapsed: 0.143 s % 216.85/30.84 % (395801)Peak memory usage: 15 MB % 216.85/30.84 % (395801)Instructions burned: 207 (million) % 216.85/30.84 % (395803)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2447297940:i=232:rtra=on_2751 on theBenchmark for (2751ds/232Mi) % 216.85/30.84 % (395803)Instruction limit reached! % 216.85/30.84 % (395803)------------------------------ % 216.85/30.84 % (395803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395803)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395803)Termination reason: Instruction limit % 216.85/30.84 % (395803)Termination phase: Saturation % 216.85/30.84 % (395803)Time elapsed: 0.165 s % 216.85/30.84 % (395803)Peak memory usage: 15 MB % 216.85/30.84 % (395803)Instructions burned: 233 (million) % 216.85/30.84 % (395805)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=982532035:i=262:rtra=on_2749 on theBenchmark for (2749ds/262Mi) % 216.85/30.84 % (395805)Instruction limit reached! % 216.85/30.84 % (395805)------------------------------ % 216.85/30.84 % (395805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395805)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395805)Termination reason: Instruction limit % 216.85/30.84 % (395805)Termination phase: Saturation % 216.85/30.84 % (395805)Time elapsed: 0.143 s % 216.85/30.84 % (395805)Peak memory usage: 16 MB % 216.85/30.84 % (395805)Instructions burned: 264 (million) % 216.85/30.84 % (395807)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1421455549:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2748 on theBenchmark for (2748ds/318Mi) % 216.85/30.84 % (395807)Instruction limit reached! % 216.85/30.84 % (395807)------------------------------ % 216.85/30.84 % (395807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395807)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395807)Termination reason: Instruction limit % 216.85/30.84 % (395807)Termination phase: Saturation % 216.85/30.84 % (395807)Time elapsed: 0.179 s % 216.85/30.84 % (395807)Peak memory usage: 15 MB % 216.85/30.84 % (395807)Instructions burned: 320 (million) % 216.85/30.84 % (395809)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=458847929:i=1428:nm=2:rtra=on_2745 on theBenchmark for (2745ds/1428Mi) % 216.85/30.84 % (395809)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.85/30.84 % (395809)Terminated due to inappropriate strategy. % 216.85/30.84 % (395809)------------------------------ % 216.85/30.84 % (395809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.85/30.84 % (395809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.85/30.84 % (395809)CaDiCaL version: 2.1.3 % 216.85/30.84 % (395809)Termination reason: Inappropriate % 216.85/30.84 % (395809)Time elapsed: 0.042 s % 216.85/30.84 % (395809)Peak memory usage: 12 MB % 216.85/30.84 % (395809)Instructions burned: 65 (million) % 216.85/30.84 % (395809)------------------------------ % 273.01/38.79 % (395809)------------------------------ % 273.01/38.79 % (395811)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2006755156:i=262:bd=preordered:rtra=on:fsd=on_2745 on theBenchmark for (2745ds/262Mi) % 273.01/38.79 % (395811)Instruction limit reached! % 273.01/38.79 % (395811)------------------------------ % 273.01/38.79 % (395811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395811)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395811)Termination reason: Instruction limit % 273.01/38.79 % (395811)Termination phase: Saturation % 273.01/38.79 % (395811)Time elapsed: 0.157 s % 273.01/38.79 % (395811)Peak memory usage: 16 MB % 273.01/38.79 % (395811)Instructions burned: 262 (million) % 273.01/38.79 % (395813)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=2118365669:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1368Mi) % 273.01/38.79 % (395813)Instruction limit reached! % 273.01/38.79 % (395813)------------------------------ % 273.01/38.79 % (395813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395813)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395813)Termination reason: Instruction limit % 273.01/38.79 % (395813)Termination phase: Saturation % 273.01/38.79 % (395813)Time elapsed: 0.659 s % 273.01/38.79 % (395813)Peak memory usage: 20 MB % 273.01/38.79 % (395813)Instructions burned: 1368 (million) % 273.01/38.79 % (395815)ott-21_1_sil=16000:si=on:fs=off:random_seed=2931345136:i=360:av=off:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/360Mi) % 273.01/38.79 % (395815)Instruction limit reached! % 273.01/38.79 % (395815)------------------------------ % 273.01/38.79 % (395815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395815)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395815)Termination reason: Instruction limit % 273.01/38.79 % (395815)Termination phase: Saturation % 273.01/38.79 % (395815)Time elapsed: 0.187 s % 273.01/38.79 % (395815)Peak memory usage: 15 MB % 273.01/38.79 % (395815)Instructions burned: 361 (million) % 273.01/38.79 % (395817)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=767459284:i=954:bd=all:rtra=on_2733 on theBenchmark for (2733ds/954Mi) % 273.01/38.79 % (395817)Instruction limit reached! % 273.01/38.79 % (395817)------------------------------ % 273.01/38.79 % (395817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395817)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395817)Termination reason: Instruction limit % 273.01/38.79 % (395817)Termination phase: Saturation % 273.01/38.79 % (395817)Time elapsed: 0.574 s % 273.01/38.79 % (395817)Peak memory usage: 19 MB % 273.01/38.79 % (395817)Instructions burned: 955 (million) % 273.01/38.79 % (395819)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2238796277:fmbsr=1.3:i=1730:ins=25:rtra=on_2727 on theBenchmark for (2727ds/1730Mi) % 273.01/38.79 % (395819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 273.01/38.79 % (395819)Terminated due to inappropriate strategy. % 273.01/38.79 % (395819)------------------------------ % 273.01/38.79 % (395819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395819)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395819)Termination reason: Inappropriate % 273.01/38.79 % (395819)Time elapsed: 0.037 s % 273.01/38.79 % (395819)Peak memory usage: 12 MB % 273.01/38.79 % (395819)Instructions burned: 65 (million) % 273.01/38.79 % (395819)------------------------------ % 273.01/38.79 % (395819)------------------------------ % 273.01/38.79 % (395821)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2238058173:i=2358:rtra=on_2727 on theBenchmark for (2727ds/2358Mi) % 273.01/38.79 % (395821)Instruction limit reached! % 273.01/38.79 % (395821)------------------------------ % 273.01/38.79 % (395821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.01/38.79 % (395821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.01/38.79 % (395821)CaDiCaL version: 2.1.3 % 273.01/38.79 % (395821)Termination reason: Instruction limit % 273.01/38.79 % (395821)Termination phase: Saturation % 300.12/42.54 % (395821)Time elapsed: 1.180 s % 300.12/42.54 % (395821)Peak memory usage: 30 MB % 300.12/42.54 % (395821)Instructions burned: 2359 (million) % 300.12/42.54 % (395823)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1801921173:i=1778:ins=1:rtra=on_2715 on theBenchmark for (2715ds/1778Mi) % 300.12/42.54 % (395823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.12/42.54 % (395823)Terminated due to inappropriate strategy. % 300.12/42.54 % (395823)------------------------------ % 300.12/42.54 % (395823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.54 % (395823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.54 % (395823)CaDiCaL version: 2.1.3 % 300.12/42.54 % (395823)Termination reason: Inappropriate % 300.12/42.54 % (395823)Time elapsed: 0.043 s % 300.12/42.54 % (395823)Peak memory usage: 12 MB % 300.12/42.54 % (395823)Instructions burned: 66 (million) % 300.12/42.54 % (395823)------------------------------ % 300.12/42.54 % (395823)------------------------------ % 300.12/42.54 % (395825)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=874591356:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2714 on theBenchmark for (2714ds/1384Mi) % 300.12/42.54 % (395825)Instruction limit reached! % 300.12/42.54 % (395825)------------------------------ % 300.12/42.54 % (395825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.54 % (395825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.54 % (395825)CaDiCaL version: 2.1.3 % 300.12/42.54 % (395825)Termination reason: Instruction limit % 300.12/42.54 % (395825)Termination phase: Saturation % 300.12/42.54 % (395825)Time elapsed: 0.735 s % 300.12/42.54 % (395825)Peak memory usage: 24 MB % 300.12/42.54 % (395825)Instructions burned: 1386 (million) % 300.12/42.54 % (395831)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2912910556:i=1758:kws=inv_precedence:fsr=off:rtra=on_2706 on theBenchmark for (2706ds/1758Mi) % 300.12/42.54 % (395831)Instruction limit reached! % 300.12/42.54 % (395831)------------------------------ % 300.12/42.54 % (395831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.54 % (395831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.54 % (395831)CaDiCaL version: 2.1.3 % 300.12/42.54 % (395831)Termination reason: Instruction limit % 300.12/42.54 % (395831)Termination phase: Saturation % 300.12/42.54 % (395831)Time elapsed: 1.045 s % 300.12/42.54 % (395831)Peak memory usage: 25 MB % 300.12/42.54 % (395831)Instructions burned: 1758 (million) % 300.12/42.54 % (395833)fmb+10_1_sil=64000:si=on:random_seed=3111569916:i=44122:nm=2:rtra=on:gsp=on_2695 on theBenchmark for (2695ds/44122Mi) % 300.12/42.54 % (395833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.12/42.54 % (395833)Terminated due to inappropriate strategy. % 300.12/42.54 % (395833)------------------------------ % 300.12/42.54 % (395833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.54 % (395833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.54 % (395833)CaDiCaL version: 2.1.3 % 300.12/42.54 % (395833)Termination reason: Inappropriate % 300.12/42.54 % (395833)Time elapsed: 0.037 s % 300.12/42.54 % (395833)Peak memory usage: 12 MB % 300.12/42.54 % (395833)Instructions burned: 65 (million) % 300.12/42.54 % (395833)------------------------------ % 300.12/42.54 % (395833)------------------------------ % 300.12/42.54 % (395835)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1905643332:i=19030:nm=5:rtra=on_2695 on theBenchmark for (2695ds/19030Mi) % 300.12/42.54 % (395835)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.12/42.54 % (395835)Terminated due to inappropriate strategy. % 300.12/42.54 % (395835)------------------------------ % 300.12/42.54 % (395835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.54 % (395835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.54 % (395835)CaDiCaL version: 2.1.3 % 300.12/42.54 % (395835)Termination reason: Inappropriate % 300.12/42.54 % (395835)Time elapsed: 0.046 s % 300.12/42.54 % (395835)Peak memory usage: 12 MB % 300.12/42.54 % (395835)Instructions burned: 65 (million) % 300.12/42.54 % (395835)------------------------------ % 300.12/42.54 % (395835)------------------------------ % 300.12/42.54 % (395837)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=473175368:fmbsr=1.7:i % 300.12/42.54 Terminated % 300.12/42.54 % Vampire exiting % 300.12/42.54 Terminated %------------------------------------------------------------------------------