%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC431_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.01s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC431_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n003.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 09:38:57 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/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.68/0.82 % (1465364)Will run a generic schedule for satisfiability detection. % 3.68/0.82 % (1465374)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2923794343:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.82 % (1465370)% WARNING: option uhcvi not known. % 3.68/0.82 % (1465369)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1403542818_2999 on theBenchmark for (2999ds/0Mi) % 3.68/0.82 % (1465370)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2996666051:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.68/0.82 % (1465371)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1756127922:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.68/0.82 % (1465372)dis+10_1_sil=32000:sp=arity:random_seed=3675914919:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.68/0.82 % (1465373)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=285644610:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.68/0.82 % (1465375)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1747381139:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.68/0.82 % (1465369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.82 % (1465369)Terminated due to inappropriate strategy. % 3.68/0.82 % (1465369)------------------------------ % 3.68/0.82 % (1465369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.82 % (1465369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.82 % (1465369)CaDiCaL version: 2.1.3 % 3.68/0.82 % (1465369)Termination reason: Inappropriate % 3.68/0.82 % (1465369)Time elapsed: 0.001 s % 3.68/0.82 % (1465369)Peak memory usage: 10 MB % 3.68/0.82 % (1465369)Instructions burned: 1 (million) % 3.68/0.82 % (1465369)------------------------------ % 3.68/0.82 % (1465369)------------------------------ % 3.68/0.82 % (1465383)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3764085531:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.68/0.82 % (1465383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.82 % (1465383)Terminated due to inappropriate strategy. % 3.68/0.82 % (1465383)------------------------------ % 3.68/0.82 % (1465383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.82 % (1465383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.82 % (1465383)CaDiCaL version: 2.1.3 % 3.68/0.82 % (1465383)Termination reason: Inappropriate % 3.68/0.82 % (1465383)Time elapsed: 0.001 s % 3.68/0.82 % (1465383)Peak memory usage: 10 MB % 3.68/0.82 % (1465383)Instructions burned: 1 (million) % 3.68/0.82 % (1465383)------------------------------ % 3.68/0.82 % (1465383)------------------------------ % 3.68/0.82 % (1465374)Instruction limit reached! % 3.68/0.82 % (1465374)------------------------------ % 3.68/0.82 % (1465374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.82 % (1465374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.82 % (1465374)CaDiCaL version: 2.1.3 % 3.68/0.82 % (1465374)Termination reason: Instruction limit % 3.68/0.82 % (1465374)Termination phase: Saturation % 3.68/0.82 % (1465374)Time elapsed: 0.043 s % 3.68/0.82 % (1465374)Peak memory usage: 13 MB % 3.68/0.82 % (1465374)Instructions burned: 132 (million) % 3.68/0.82 % (1465385)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2871790678:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.82 % (1465386)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=442570519:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.68/0.82 % (1465372)Instruction limit reached! % 3.68/0.82 % (1465372)------------------------------ % 3.68/0.82 % (1465372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.82 % (1465372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.82 % (1465372)CaDiCaL version: 2.1.3 % 3.68/0.82 % (1465372)Termination reason: Instruction limit % 3.68/0.82 % (1465372)Termination phase: Saturation % 3.68/0.82 % (1465372)Time elapsed: 0.066 s % 3.68/0.82 % (1465372)Peak memory usage: 12 MB % 3.68/0.82 % (1465372)Instructions burned: 111 (million) % 3.68/0.82 % (1465373)Instruction limit reached! % 3.68/0.82 % (1465373)------------------------------ % 3.68/0.82 % (1465373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465373)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465373)Termination reason: Instruction limit % 5.84/1.12 % (1465373)Termination phase: Saturation % 5.84/1.12 % (1465373)Time elapsed: 0.071 s % 5.84/1.12 % (1465373)Peak memory usage: 12 MB % 5.84/1.12 % (1465373)Instructions burned: 117 (million) % 5.84/1.12 % (1465389)ott-21_1_sil=16000:fs=off:random_seed=879765597:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.84/1.12 % (1465390)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3783158523:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.84/1.12 % (1465375)Instruction limit reached! % 5.84/1.12 % (1465375)------------------------------ % 5.84/1.12 % (1465375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465375)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465375)Termination reason: Instruction limit % 5.84/1.12 % (1465375)Termination phase: Saturation % 5.84/1.12 % (1465375)Time elapsed: 0.104 s % 5.84/1.12 % (1465375)Peak memory usage: 13 MB % 5.84/1.12 % (1465375)Instructions burned: 159 (million) % 5.84/1.12 % (1465393)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2589568682:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.84/1.12 % (1465393)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.84/1.12 % (1465393)Terminated due to inappropriate strategy. % 5.84/1.12 % (1465393)------------------------------ % 5.84/1.12 % (1465393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465393)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465393)Termination reason: Inappropriate % 5.84/1.12 % (1465393)Time elapsed: 0.001 s % 5.84/1.12 % (1465393)Peak memory usage: 10 MB % 5.84/1.12 % (1465393)Instructions burned: 1 (million) % 5.84/1.12 % (1465393)------------------------------ % 5.84/1.12 % (1465393)------------------------------ % 5.84/1.12 % (1465385)Instruction limit reached! % 5.84/1.12 % (1465385)------------------------------ % 5.84/1.12 % (1465385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465385)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465385)Termination reason: Instruction limit % 5.84/1.12 % (1465385)Termination phase: Saturation % 5.84/1.12 % (1465385)Time elapsed: 0.085 s % 5.84/1.12 % (1465385)Peak memory usage: 12 MB % 5.84/1.12 % (1465385)Instructions burned: 132 (million) % 5.84/1.12 % (1465395)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1147397244:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.84/1.12 % (1465396)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1796863788:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.84/1.12 % (1465396)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.84/1.12 % (1465396)Terminated due to inappropriate strategy. % 5.84/1.12 % (1465396)------------------------------ % 5.84/1.12 % (1465396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465396)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465396)Termination reason: Inappropriate % 5.84/1.12 % (1465396)Time elapsed: 0.001 s % 5.84/1.12 % (1465396)Peak memory usage: 10 MB % 5.84/1.12 % (1465396)Instructions burned: 1 (million) % 5.84/1.12 % (1465396)------------------------------ % 5.84/1.12 % (1465396)------------------------------ % 5.84/1.12 % (1465399)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=4154226809:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.84/1.12 % (1465389)Instruction limit reached! % 5.84/1.12 % (1465389)------------------------------ % 5.84/1.12 % (1465389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.84/1.12 % (1465389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.12 % (1465389)CaDiCaL version: 2.1.3 % 5.84/1.12 % (1465389)Termination reason: Instruction limit % 5.84/1.12 % (1465389)Termination phase: Saturation % 18.10/3.00 % (1465389)Time elapsed: 0.085 s % 18.10/3.00 % (1465389)Peak memory usage: 12 MB % 18.10/3.00 % (1465389)Instructions burned: 188 (million) % 18.10/3.00 % (1465401)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1910420620:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.10/3.00 % (1465386)Instruction limit reached! % 18.10/3.00 % (1465386)------------------------------ % 18.10/3.00 % (1465386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.10/3.00 % (1465386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.00 % (1465386)CaDiCaL version: 2.1.3 % 18.10/3.00 % (1465386)Termination reason: Instruction limit % 18.10/3.00 % (1465386)Termination phase: Saturation % 18.10/3.00 % (1465386)Time elapsed: 0.208 s % 18.10/3.00 % (1465386)Peak memory usage: 18 MB % 18.10/3.00 % (1465386)Instructions burned: 685 (million) % 18.10/3.00 % (1465403)fmb+10_1_sil=64000:random_seed=3061713600:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 18.10/3.00 % (1465403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.10/3.00 % (1465403)Terminated due to inappropriate strategy. % 18.10/3.00 % (1465403)------------------------------ % 18.10/3.00 % (1465403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.10/3.00 % (1465403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.00 % (1465403)CaDiCaL version: 2.1.3 % 18.10/3.00 % (1465403)Termination reason: Inappropriate % 18.10/3.00 % (1465403)Time elapsed: 0.0000 s % 18.10/3.00 % (1465403)Peak memory usage: 10 MB % 18.10/3.00 % (1465403)Instructions burned: 1 (million) % 18.10/3.00 % (1465403)------------------------------ % 18.10/3.00 % (1465403)------------------------------ % 18.10/3.00 % (1465405)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2438340629:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.10/3.00 % (1465405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.10/3.00 % (1465405)Terminated due to inappropriate strategy. % 18.10/3.00 % (1465405)------------------------------ % 18.10/3.00 % (1465405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.10/3.00 % (1465405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.00 % (1465405)CaDiCaL version: 2.1.3 % 18.10/3.00 % (1465405)Termination reason: Inappropriate % 18.10/3.00 % (1465405)Time elapsed: 0.0000 s % 18.10/3.00 % (1465405)Peak memory usage: 11 MB % 18.10/3.00 % (1465405)Instructions burned: 1 (million) % 18.10/3.00 % (1465405)------------------------------ % 18.10/3.00 % (1465405)------------------------------ % 18.10/3.00 % (1465407)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=339416882:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.10/3.00 % (1465407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.10/3.00 % (1465407)Terminated due to inappropriate strategy. % 18.10/3.00 % (1465407)------------------------------ % 18.10/3.00 % (1465407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.10/3.00 % (1465407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.00 % (1465407)CaDiCaL version: 2.1.3 % 18.10/3.00 % (1465407)Termination reason: Inappropriate % 18.10/3.00 % (1465407)Time elapsed: 0.0000 s % 18.10/3.00 % (1465407)Peak memory usage: 11 MB % 18.10/3.00 % (1465407)Instructions burned: 1 (million) % 18.10/3.00 % (1465407)------------------------------ % 18.10/3.00 % (1465407)------------------------------ % 18.10/3.00 % (1465409)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=485736609:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.10/3.00 % (1465390)Instruction limit reached! % 18.10/3.00 % (1465390)------------------------------ % 18.10/3.00 % (1465390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.10/3.00 % (1465390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.00 % (1465390)CaDiCaL version: 2.1.3 % 18.10/3.00 % (1465390)Termination reason: Instruction limit % 18.10/3.00 % (1465390)Termination phase: Saturation % 18.10/3.00 % (1465390)Time elapsed: 0.307 s % 18.10/3.00 % (1465390)Peak memory usage: 14 MB % 18.10/3.00 % (1465390)Instructions burned: 477 (million) % 18.10/3.00 % (1465411)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=162387367:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.10/3.00 % (1465399)Instruction limit reached! % 18.10/3.00 % (1465399)------------------------------ % 27.88/4.18 % (1465399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465399)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465399)Termination reason: Instruction limit % 27.88/4.18 % (1465399)Termination phase: Saturation % 27.88/4.18 % (1465399)Time elapsed: 0.388 s % 27.88/4.18 % (1465399)Peak memory usage: 16 MB % 27.88/4.18 % (1465399)Instructions burned: 693 (million) % 27.88/4.18 % (1465413)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3119596783:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 27.88/4.18 % (1465413)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.88/4.18 % (1465413)Terminated due to inappropriate strategy. % 27.88/4.18 % (1465413)------------------------------ % 27.88/4.18 % (1465413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465413)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465413)Termination reason: Inappropriate % 27.88/4.18 % (1465413)Time elapsed: 0.001 s % 27.88/4.18 % (1465413)Peak memory usage: 10 MB % 27.88/4.18 % (1465413)Instructions burned: 1 (million) % 27.88/4.18 % (1465413)------------------------------ % 27.88/4.18 % (1465413)------------------------------ % 27.88/4.18 % (1465415)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2806819518:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.88/4.18 % (1465415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.88/4.18 % (1465415)Terminated due to inappropriate strategy. % 27.88/4.18 % (1465415)------------------------------ % 27.88/4.18 % (1465415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465415)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465415)Termination reason: Inappropriate % 27.88/4.18 % (1465415)Time elapsed: 0.001 s % 27.88/4.18 % (1465415)Peak memory usage: 10 MB % 27.88/4.18 % (1465415)Instructions burned: 1 (million) % 27.88/4.18 % (1465415)------------------------------ % 27.88/4.18 % (1465415)------------------------------ % 27.88/4.18 % (1465417)ott-2_1_sil=16000:newcnf=on:random_seed=3586604969:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.88/4.18 % (1465401)Instruction limit reached! % 27.88/4.18 % (1465401)------------------------------ % 27.88/4.18 % (1465401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465401)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465401)Termination reason: Instruction limit % 27.88/4.18 % (1465401)Termination phase: Saturation % 27.88/4.18 % (1465401)Time elapsed: 0.486 s % 27.88/4.18 % (1465401)Peak memory usage: 19 MB % 27.88/4.18 % (1465401)Instructions burned: 880 (million) % 27.88/4.18 % (1465419)ott+10_1_sil=32000:tgt=ground:random_seed=3645010630:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.88/4.18 % (1465395)Instruction limit reached! % 27.88/4.18 % (1465395)------------------------------ % 27.88/4.18 % (1465395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465395)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465395)Termination reason: Instruction limit % 27.88/4.18 % (1465395)Termination phase: Saturation % 27.88/4.18 % (1465395)Time elapsed: 0.682 s % 27.88/4.18 % (1465395)Peak memory usage: 18 MB % 27.88/4.18 % (1465395)Instructions burned: 1179 (million) % 27.88/4.18 % (1465421)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3038711808:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.88/4.18 % (1465421)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.88/4.18 % (1465421)Terminated due to inappropriate strategy. % 27.88/4.18 % (1465421)------------------------------ % 27.88/4.18 % (1465421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.88/4.18 % (1465421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.88/4.18 % (1465421)CaDiCaL version: 2.1.3 % 27.88/4.18 % (1465421)Termination reason: Inappropriate % 27.88/4.18 % (1465421)Time elapsed: 0.001 s % 27.88/4.18 % (1465421)Peak memory usage: 10 MB % 27.88/4.18 % (1465421)Instructions burned: 1 (million) % 85.64/12.32 % (1465421)------------------------------ % 85.64/12.32 % (1465421)------------------------------ % 85.64/12.32 % (1465423)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1895355710:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 85.64/12.32 % (1465417)Instruction limit reached! % 85.64/12.32 % (1465417)------------------------------ % 85.64/12.32 % (1465417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465417)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465417)Termination reason: Instruction limit % 85.64/12.32 % (1465417)Termination phase: Saturation % 85.64/12.32 % (1465417)Time elapsed: 0.508 s % 85.64/12.32 % (1465417)Peak memory usage: 15 MB % 85.64/12.32 % (1465417)Instructions burned: 869 (million) % 85.64/12.32 % (1465425)dis+21_1_sil=32000:sas=cadical:random_seed=722539244:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 85.64/12.32 % (1465411)Instruction limit reached! % 85.64/12.32 % (1465411)------------------------------ % 85.64/12.32 % (1465411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465411)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465411)Termination reason: Instruction limit % 85.64/12.32 % (1465411)Termination phase: Saturation % 85.64/12.32 % (1465411)Time elapsed: 0.926 s % 85.64/12.32 % (1465411)Peak memory usage: 27 MB % 85.64/12.32 % (1465411)Instructions burned: 1472 (million) % 85.64/12.32 % (1465427)ott+11_1_sil=16000:gs=on:random_seed=2964233064:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 85.64/12.32 % (1465409)Instruction limit reached! % 85.64/12.32 % (1465409)------------------------------ % 85.64/12.32 % (1465409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465409)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465409)Termination reason: Instruction limit % 85.64/12.32 % (1465409)Termination phase: Saturation % 85.64/12.32 % (1465409)Time elapsed: 1.505 s % 85.64/12.32 % (1465409)Peak memory usage: 43 MB % 85.64/12.32 % (1465409)Instructions burned: 5134 (million) % 85.64/12.32 % (1465429)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1568299212:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 85.64/12.32 % (1465429)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 85.64/12.32 % (1465429)Terminated due to inappropriate strategy. % 85.64/12.32 % (1465429)------------------------------ % 85.64/12.32 % (1465429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465429)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465429)Termination reason: Inappropriate % 85.64/12.32 % (1465429)Time elapsed: 0.0000 s % 85.64/12.32 % (1465429)Peak memory usage: 10 MB % 85.64/12.32 % (1465429)Instructions burned: 1 (million) % 85.64/12.32 % (1465429)------------------------------ % 85.64/12.32 % (1465429)------------------------------ % 85.64/12.32 % (1465431)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2950831890:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 85.64/12.32 % (1465427)Instruction limit reached! % 85.64/12.32 % (1465427)------------------------------ % 85.64/12.32 % (1465427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465427)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465427)Termination reason: Instruction limit % 85.64/12.32 % (1465427)Termination phase: Saturation % 85.64/12.32 % (1465427)Time elapsed: 1.245 s % 85.64/12.32 % (1465427)Peak memory usage: 22 MB % 85.64/12.32 % (1465427)Instructions burned: 2253 (million) % 85.64/12.32 % (1465433)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2300022496:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 85.64/12.32 % (1465423)Instruction limit reached! % 85.64/12.32 % (1465423)------------------------------ % 85.64/12.32 % (1465423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.64/12.32 % (1465423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.32 % (1465423)CaDiCaL version: 2.1.3 % 85.64/12.32 % (1465423)Termination reason: Instruction limit % 117.78/16.99 % (1465423)Termination phase: Saturation % 117.78/16.99 % (1465423)Time elapsed: 1.865 s % 117.78/16.99 % (1465423)Peak memory usage: 35 MB % 117.78/16.99 % (1465423)Instructions burned: 3517 (million) % 117.78/16.99 % (1465435)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=691628225:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 117.78/16.99 % (1465431)Instruction limit reached! % 117.78/16.99 % (1465431)------------------------------ % 117.78/16.99 % (1465431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.78/16.99 % (1465431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.78/16.99 % (1465431)CaDiCaL version: 2.1.3 % 117.78/16.99 % (1465431)Termination reason: Instruction limit % 117.78/16.99 % (1465431)Termination phase: Saturation % 117.78/16.99 % (1465431)Time elapsed: 1.168 s % 117.78/16.99 % (1465431)Peak memory usage: 46 MB % 117.78/16.99 % (1465431)Instructions burned: 4593 (million) % 117.78/16.99 % (1465437)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1636338504:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 117.78/16.99 % (1465437)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.78/16.99 % (1465437)Terminated due to inappropriate strategy. % 117.78/16.99 % (1465437)------------------------------ % 117.78/16.99 % (1465437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.78/16.99 % (1465437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.78/16.99 % (1465437)CaDiCaL version: 2.1.3 % 117.78/16.99 % (1465437)Termination reason: Inappropriate % 117.78/16.99 % (1465437)Time elapsed: 0.0000 s % 117.78/16.99 % (1465437)Peak memory usage: 10 MB % 117.78/16.99 % (1465437)Instructions burned: 1 (million) % 117.78/16.99 % (1465437)------------------------------ % 117.78/16.99 % (1465437)------------------------------ % 117.78/16.99 % (1465439)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1514087254:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 117.78/16.99 % (1465439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.78/16.99 % (1465439)Terminated due to inappropriate strategy. % 117.78/16.99 % (1465439)------------------------------ % 117.78/16.99 % (1465439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.78/16.99 % (1465439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.78/16.99 % (1465439)CaDiCaL version: 2.1.3 % 117.78/16.99 % (1465439)Termination reason: Inappropriate % 117.78/16.99 % (1465439)Time elapsed: 0.0000 s % 117.78/16.99 % (1465439)Peak memory usage: 10 MB % 117.78/16.99 % (1465439)Instructions burned: 1 (million) % 117.78/16.99 % (1465439)------------------------------ % 117.78/16.99 % (1465439)------------------------------ % 117.78/16.99 % (1465441)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1555662613:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 117.78/16.99 % (1465441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.78/16.99 % (1465441)Terminated due to inappropriate strategy. % 117.78/16.99 % (1465441)------------------------------ % 117.78/16.99 % (1465441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.78/16.99 % (1465441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.78/16.99 % (1465441)CaDiCaL version: 2.1.3 % 117.78/16.99 % (1465441)Termination reason: Inappropriate % 117.78/16.99 % (1465441)Time elapsed: 0.0000 s % 117.78/16.99 % (1465441)Peak memory usage: 10 MB % 117.78/16.99 % (1465441)Instructions burned: 1 (million) % 117.78/16.99 % (1465441)------------------------------ % 117.78/16.99 % (1465441)------------------------------ % 117.78/16.99 % (1465443)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2139410822:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 117.78/16.99 % (1465425)Instruction limit reached! % 117.78/16.99 % (1465425)------------------------------ % 117.78/16.99 % (1465425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.78/16.99 % (1465425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.78/16.99 % (1465425)CaDiCaL version: 2.1.3 % 117.78/16.99 % (1465425)Termination reason: Instruction limit % 117.78/16.99 % (1465425)Termination phase: Saturation % 117.78/16.99 % (1465425)Time elapsed: 2.060 s % 117.78/16.99 % (1465425)Peak memory usage: 31 MB % 117.78/16.99 % (1465425)Instructions burned: 3774 (million) % 117.78/16.99 % (1465445)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=543731669:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 117.78/16.99 % (1465419)Instruction limit reached! % 119.39/17.06 % (1465419)------------------------------ % 119.39/17.06 % (1465419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465419)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465419)Termination reason: Instruction limit % 119.39/17.06 % (1465419)Termination phase: Saturation % 119.39/17.06 % (1465419)Time elapsed: 3.221 s % 119.39/17.06 % (1465419)Peak memory usage: 41 MB % 119.39/17.06 % (1465419)Instructions burned: 5115 (million) % 119.39/17.06 % (1465447)dis+10_16:1_sil=16000:random_seed=1287677818:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 119.39/17.06 % (1465435)Instruction limit reached! % 119.39/17.06 % (1465435)------------------------------ % 119.39/17.06 % (1465435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465435)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465435)Termination reason: Instruction limit % 119.39/17.06 % (1465435)Termination phase: Saturation % 119.39/17.06 % (1465435)Time elapsed: 2.647 s % 119.39/17.06 % (1465435)Peak memory usage: 44 MB % 119.39/17.06 % (1465435)Instructions burned: 5211 (million) % 119.39/17.06 % (1465449)ott-3_8_sil=64000:random_seed=2531904432:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 119.39/17.06 % (1465443)Instruction limit reached! % 119.39/17.06 % (1465443)------------------------------ % 119.39/17.06 % (1465443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465443)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465443)Termination reason: Instruction limit % 119.39/17.06 % (1465443)Termination phase: Saturation % 119.39/17.06 % (1465443)Time elapsed: 5.137 s % 119.39/17.06 % (1465443)Peak memory usage: 71 MB % 119.39/17.06 % (1465443)Instructions burned: 22568 (million) % 119.39/17.06 % (1465451)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1507475209:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 119.39/17.06 % (1465451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.39/17.06 % (1465451)Terminated due to inappropriate strategy. % 119.39/17.06 % (1465451)------------------------------ % 119.39/17.06 % (1465451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465451)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465451)Termination reason: Inappropriate % 119.39/17.06 % (1465451)Time elapsed: 0.0000 s % 119.39/17.06 % (1465451)Peak memory usage: 10 MB % 119.39/17.06 % (1465451)Instructions burned: 1 (million) % 119.39/17.06 % (1465451)------------------------------ % 119.39/17.06 % (1465451)------------------------------ % 119.39/17.06 % (1465453)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1723370331:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 119.39/17.06 % (1465445)Instruction limit reached! % 119.39/17.06 % (1465445)------------------------------ % 119.39/17.06 % (1465445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465445)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465445)Termination reason: Instruction limit % 119.39/17.06 % (1465445)Termination phase: Saturation % 119.39/17.06 % (1465445)Time elapsed: 5.110 s % 119.39/17.06 % (1465445)Peak memory usage: 57 MB % 119.39/17.06 % (1465445)Instructions burned: 8173 (million) % 119.39/17.06 % (1465455)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2368064353:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 119.39/17.06 % (1465447)Instruction limit reached! % 119.39/17.06 % (1465447)------------------------------ % 119.39/17.06 % (1465447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.39/17.06 % (1465447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.39/17.06 % (1465447)CaDiCaL version: 2.1.3 % 119.39/17.06 % (1465447)Termination reason: Instruction limit % 119.39/17.06 % (1465447)Termination phase: Saturation % 119.39/17.06 % (1465447)Time elapsed: 4.623 s % 119.39/17.06 % (1465447)Peak memory usage: 52 MB % 119.39/17.06 % (1465447)Instructions burned: 9155 (million) % 119.39/17.06 % (1465457)dis+33_16_sil=32000:sac=on:random_seed=781854888:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 119.39/17.06 % (1465453)Instruction limit reached! % 119.39/17.06 % (1465453)------------------------------ % 119.39/17.06 % (1465453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465453)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465453)Termination reason: Instruction limit % 135.35/19.31 % (1465453)Termination phase: Saturation % 135.35/19.31 % (1465453)Time elapsed: 3.836 s % 135.35/19.31 % (1465453)Peak memory usage: 64 MB % 135.35/19.31 % (1465453)Instructions burned: 11406 (million) % 135.35/19.31 % (1465459)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2878283643:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi) % 135.35/19.31 % (1465433)Instruction limit reached! % 135.35/19.31 % (1465433)------------------------------ % 135.35/19.31 % (1465433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465433)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465433)Termination reason: Instruction limit % 135.35/19.31 % (1465433)Termination phase: Saturation % 135.35/19.31 % (1465433)Time elapsed: 11.899 s % 135.35/19.31 % (1465433)Peak memory usage: 119 MB % 135.35/19.31 % (1465433)Instructions burned: 29343 (million) % 135.35/19.31 % (1465461)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=642318488:s2a=on:i=53295_2854 on theBenchmark for (2854ds/53295Mi) % 135.35/19.31 % (1465457)Instruction limit reached! % 135.35/19.31 % (1465457)------------------------------ % 135.35/19.31 % (1465457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465457)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465457)Termination reason: Instruction limit % 135.35/19.31 % (1465457)Termination phase: Saturation % 135.35/19.31 % (1465457)Time elapsed: 7.459 s % 135.35/19.31 % (1465457)Peak memory usage: 180 MB % 135.35/19.31 % (1465457)Instructions burned: 15852 (million) % 135.35/19.31 % (1465463)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2339566231:i=26857:ins=20_2838 on theBenchmark for (2838ds/26857Mi) % 135.35/19.31 % (1465463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.35/19.31 % (1465463)Terminated due to inappropriate strategy. % 135.35/19.31 % (1465463)------------------------------ % 135.35/19.31 % (1465463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465463)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465463)Termination reason: Inappropriate % 135.35/19.31 % (1465463)Time elapsed: 0.001 s % 135.35/19.31 % (1465463)Peak memory usage: 10 MB % 135.35/19.31 % (1465463)Instructions burned: 1 (million) % 135.35/19.31 % (1465463)------------------------------ % 135.35/19.31 % (1465463)------------------------------ % 135.35/19.31 % (1465465)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3292091373:i=28120:bs=on:fsr=off_2838 on theBenchmark for (2838ds/28120Mi) % 135.35/19.31 % (1465459)Instruction limit reached! % 135.35/19.31 % (1465459)------------------------------ % 135.35/19.31 % (1465459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465459)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465459)Termination reason: Instruction limit % 135.35/19.31 % (1465459)Termination phase: Saturation % 135.35/19.31 % (1465459)Time elapsed: 4.623 s % 135.35/19.31 % (1465459)Peak memory usage: 131 MB % 135.35/19.31 % (1465459)Instructions burned: 17629 (million) % 135.35/19.31 % (1465467)fmb+10_1_sil=256000:fmbss=7:random_seed=378253369:fmbsr=1.6:i=182295_2832 on theBenchmark for (2832ds/182295Mi) % 135.35/19.31 % (1465467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.35/19.31 % (1465467)Terminated due to inappropriate strategy. % 135.35/19.31 % (1465467)------------------------------ % 135.35/19.31 % (1465467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.35/19.31 % (1465467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.35/19.31 % (1465467)CaDiCaL version: 2.1.3 % 135.35/19.31 % (1465467)Termination reason: Inappropriate % 135.35/19.31 % (1465467)Time elapsed: 0.0000 s % 135.35/19.31 % (1465467)Peak memory usage: 10 MB % 135.35/19.31 % (1465467)Instructions burned: 1 (million) % 135.35/19.31 % (1465467)------------------------------ % 135.35/19.31 % (1465467)------------------------------ % 135.35/19.31 % (1465469)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1501811399:i=44625:gsp=on_2832 on theBenchmark for (2832ds/44625Mi) % 148.83/21.23 % (1465469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.23 % (1465469)Terminated due to inappropriate strategy. % 148.83/21.23 % (1465469)------------------------------ % 148.83/21.23 % (1465469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.23 % (1465469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.23 % (1465469)CaDiCaL version: 2.1.3 % 148.83/21.23 % (1465469)Termination reason: Inappropriate % 148.83/21.23 % (1465469)Time elapsed: 0.0000 s % 148.83/21.23 % (1465469)Peak memory usage: 11 MB % 148.83/21.23 % (1465469)Instructions burned: 1 (million) % 148.83/21.23 % (1465469)------------------------------ % 148.83/21.23 % (1465469)------------------------------ % 148.83/21.23 % (1465471)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1873482499:i=160505_2832 on theBenchmark for (2832ds/160505Mi) % 148.83/21.23 % (1465471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.23 % (1465471)Terminated due to inappropriate strategy. % 148.83/21.23 % (1465471)------------------------------ % 148.83/21.23 % (1465471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.23 % (1465471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.23 % (1465471)CaDiCaL version: 2.1.3 % 148.83/21.23 % (1465471)Termination reason: Inappropriate % 148.83/21.23 % (1465471)Time elapsed: 0.0000 s % 148.83/21.23 % (1465471)Peak memory usage: 10 MB % 148.83/21.23 % (1465471)Instructions burned: 1 (million) % 148.83/21.23 % (1465471)------------------------------ % 148.83/21.23 % (1465471)------------------------------ % 148.83/21.23 % (1465473)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2787528255:fmbsr=1.3:i=225729_2832 on theBenchmark for (2832ds/225729Mi) % 148.83/21.23 % (1465473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.23 % (1465473)Terminated due to inappropriate strategy. % 148.83/21.23 % (1465473)------------------------------ % 148.83/21.23 % (1465473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.23 % (1465473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.23 % (1465473)CaDiCaL version: 2.1.3 % 148.83/21.23 % (1465473)Termination reason: Inappropriate % 148.83/21.23 % (1465473)Time elapsed: 0.0000 s % 148.83/21.23 % (1465473)Peak memory usage: 11 MB % 148.83/21.23 % (1465473)Instructions burned: 1 (million) % 148.83/21.23 % (1465473)------------------------------ % 148.83/21.23 % (1465473)------------------------------ % 148.83/21.23 % (1465475)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=822613921:fmbsr=2:i=185024:ins=7_2832 on theBenchmark for (2832ds/185024Mi) % 148.83/21.23 % (1465475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.23 % (1465475)Terminated due to inappropriate strategy. % 148.83/21.23 % (1465475)------------------------------ % 148.83/21.23 % (1465475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.23 % (1465475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.23 % (1465475)CaDiCaL version: 2.1.3 % 148.83/21.23 % (1465475)Termination reason: Inappropriate % 148.83/21.23 % (1465475)Time elapsed: 0.001 s % 148.83/21.23 % (1465475)Peak memory usage: 11 MB % 148.83/21.23 % (1465475)Instructions burned: 1 (million) % 148.83/21.23 % (1465475)------------------------------ % 148.83/21.23 % (1465475)------------------------------ % 148.83/21.23 % (1465477)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=388947030:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 148.83/21.23 % (1465477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.23 % (1465477)Terminated due to inappropriate strategy. % 148.83/21.23 % (1465477)------------------------------ % 148.83/21.23 % (1465477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.23 % (1465477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.23 % (1465477)CaDiCaL version: 2.1.3 % 148.83/21.23 % (1465477)Termination reason: Inappropriate % 148.83/21.23 % (1465477)Time elapsed: 0.0000 s % 148.83/21.23 % (1465477)Peak memory usage: 11 MB % 148.83/21.23 % (1465477)Instructions burned: 1 (million) % 148.83/21.23 % (1465477)------------------------------ % 148.83/21.23 % (1465477)------------------------------ % 148.83/21.23 % (1465479)% WARNING: option uhcvi not known. % 148.83/21.23 % (1465479)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2824002489:i=271062:add=off:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/271062Mi) % 172.26/24.59 % (1465455)Instruction limit reached! % 172.26/24.59 % (1465455)------------------------------ % 172.26/24.59 % (1465455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465455)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465455)Termination reason: Instruction limit % 172.26/24.59 % (1465455)Termination phase: Saturation % 172.26/24.59 % (1465455)Time elapsed: 8.750 s % 172.26/24.59 % (1465455)Peak memory usage: 78 MB % 172.26/24.59 % (1465455)Instructions burned: 14134 (million) % 172.26/24.59 % (1465481)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3227058:i=176048:add=on:rtra=on:rawr=on_2828 on theBenchmark for (2828ds/176048Mi) % 172.26/24.59 % (1465449)Instruction limit reached! % 172.26/24.59 % (1465449)------------------------------ % 172.26/24.59 % (1465449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465449)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465449)Termination reason: Instruction limit % 172.26/24.59 % (1465449)Termination phase: Saturation % 172.26/24.59 % (1465449)Time elapsed: 12.896 s % 172.26/24.59 % (1465449)Peak memory usage: 70 MB % 172.26/24.59 % (1465449)Instructions burned: 20140 (million) % 172.26/24.59 % (1465483)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3579152368:i=206:fgj=on:rtra=on_2816 on theBenchmark for (2816ds/206Mi) % 172.26/24.59 % (1465483)Instruction limit reached! % 172.26/24.59 % (1465483)------------------------------ % 172.26/24.59 % (1465483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465483)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465483)Termination reason: Instruction limit % 172.26/24.59 % (1465483)Termination phase: Saturation % 172.26/24.59 % (1465483)Time elapsed: 0.125 s % 172.26/24.59 % (1465483)Peak memory usage: 13 MB % 172.26/24.59 % (1465483)Instructions burned: 208 (million) % 172.26/24.59 % (1465485)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1558028761:i=232:rtra=on_2814 on theBenchmark for (2814ds/232Mi) % 172.26/24.59 % (1465485)Instruction limit reached! % 172.26/24.59 % (1465485)------------------------------ % 172.26/24.59 % (1465485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465485)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465485)Termination reason: Instruction limit % 172.26/24.59 % (1465485)Termination phase: Saturation % 172.26/24.59 % (1465485)Time elapsed: 0.147 s % 172.26/24.59 % (1465485)Peak memory usage: 13 MB % 172.26/24.59 % (1465485)Instructions burned: 234 (million) % 172.26/24.59 % (1465487)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1177121610:i=262:rtra=on_2813 on theBenchmark for (2813ds/262Mi) % 172.26/24.59 % (1465487)Instruction limit reached! % 172.26/24.59 % (1465487)------------------------------ % 172.26/24.59 % (1465487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465487)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465487)Termination reason: Instruction limit % 172.26/24.59 % (1465487)Termination phase: Saturation % 172.26/24.59 % (1465487)Time elapsed: 0.136 s % 172.26/24.59 % (1465487)Peak memory usage: 13 MB % 172.26/24.59 % (1465487)Instructions burned: 263 (million) % 172.26/24.59 % (1465489)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=368482767:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2811 on theBenchmark for (2811ds/318Mi) % 172.26/24.59 % (1465489)Instruction limit reached! % 172.26/24.59 % (1465489)------------------------------ % 172.26/24.59 % (1465489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (1465489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (1465489)CaDiCaL version: 2.1.3 % 172.26/24.59 % (1465489)Termination reason: Instruction limit % 172.26/24.59 % (1465489)Termination phase: Saturation % 172.26/24.59 % (1465489)Time elapsed: 0.202 s % 172.26/24.59 % (1465489)Peak memory usage: 14 MB % 172.26/24.59 % (1465489)Instructions burned: 319 (million) % 172.26/24.59 % (1465491)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2404695296:i=1428:nm=2:rtra=on_2809 on theBenchmark for (2809ds/1428Mi) % 212.49/30.45 % (1465491)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.49/30.45 % (1465491)Terminated due to inappropriate strategy. % 212.49/30.45 % (1465491)------------------------------ % 212.49/30.45 % (1465491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465491)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465491)Termination reason: Inappropriate % 212.49/30.45 % (1465491)Time elapsed: 0.001 s % 212.49/30.45 % (1465491)Peak memory usage: 10 MB % 212.49/30.45 % (1465491)Instructions burned: 1 (million) % 212.49/30.45 % (1465491)------------------------------ % 212.49/30.45 % (1465491)------------------------------ % 212.49/30.45 % (1465493)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1641959468:i=262:bd=preordered:rtra=on:fsd=on_2809 on theBenchmark for (2809ds/262Mi) % 212.49/30.45 % (1465493)Instruction limit reached! % 212.49/30.45 % (1465493)------------------------------ % 212.49/30.45 % (1465493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465493)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465493)Termination reason: Instruction limit % 212.49/30.45 % (1465493)Termination phase: Saturation % 212.49/30.45 % (1465493)Time elapsed: 0.171 s % 212.49/30.45 % (1465493)Peak memory usage: 14 MB % 212.49/30.45 % (1465493)Instructions burned: 262 (million) % 212.49/30.45 % (1465495)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=1468379639:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/1368Mi) % 212.49/30.45 % (1465495)Instruction limit reached! % 212.49/30.45 % (1465495)------------------------------ % 212.49/30.45 % (1465495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465495)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465495)Termination reason: Instruction limit % 212.49/30.45 % (1465495)Termination phase: Saturation % 212.49/30.45 % (1465495)Time elapsed: 0.856 s % 212.49/30.45 % (1465495)Peak memory usage: 20 MB % 212.49/30.45 % (1465495)Instructions burned: 1369 (million) % 212.49/30.45 % (1465497)ott-21_1_sil=16000:si=on:fs=off:random_seed=3719959804:i=360:av=off:fsr=off:rtra=on_2798 on theBenchmark for (2798ds/360Mi) % 212.49/30.45 % (1465497)Instruction limit reached! % 212.49/30.45 % (1465497)------------------------------ % 212.49/30.45 % (1465497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465497)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465497)Termination reason: Instruction limit % 212.49/30.45 % (1465497)Termination phase: Saturation % 212.49/30.45 % (1465497)Time elapsed: 0.165 s % 212.49/30.45 % (1465497)Peak memory usage: 13 MB % 212.49/30.45 % (1465497)Instructions burned: 360 (million) % 212.49/30.45 % (1465499)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1352554083:i=954:bd=all:rtra=on_2796 on theBenchmark for (2796ds/954Mi) % 212.49/30.45 % (1465499)Instruction limit reached! % 212.49/30.45 % (1465499)------------------------------ % 212.49/30.45 % (1465499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465499)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465499)Termination reason: Instruction limit % 212.49/30.45 % (1465499)Termination phase: Saturation % 212.49/30.45 % (1465499)Time elapsed: 0.621 s % 212.49/30.45 % (1465499)Peak memory usage: 16 MB % 212.49/30.45 % (1465499)Instructions burned: 954 (million) % 212.49/30.45 % (1465501)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=644490745:fmbsr=1.3:i=1730:ins=25:rtra=on_2790 on theBenchmark for (2790ds/1730Mi) % 212.49/30.45 % (1465501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.49/30.45 % (1465501)Terminated due to inappropriate strategy. % 212.49/30.45 % (1465501)------------------------------ % 212.49/30.45 % (1465501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.49/30.45 % (1465501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.49/30.45 % (1465501)CaDiCaL version: 2.1.3 % 212.49/30.45 % (1465501)Termination reason: Inappropriate % 268.54/38.10 % (1465501)Time elapsed: 0.001 s % 268.54/38.10 % (1465501)Peak memory usage: 10 MB % 268.54/38.10 % (1465501)Instructions burned: 1 (million) % 268.54/38.10 % (1465501)------------------------------ % 268.54/38.10 % (1465501)------------------------------ % 268.54/38.10 % (1465503)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2654735550:i=2358:rtra=on_2789 on theBenchmark for (2789ds/2358Mi) % 268.54/38.10 % (1465503)Instruction limit reached! % 268.54/38.10 % (1465503)------------------------------ % 268.54/38.10 % (1465503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.54/38.10 % (1465503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.54/38.10 % (1465503)CaDiCaL version: 2.1.3 % 268.54/38.10 % (1465503)Termination reason: Instruction limit % 268.54/38.10 % (1465503)Termination phase: Saturation % 268.54/38.10 % (1465503)Time elapsed: 1.437 s % 268.54/38.10 % (1465503)Peak memory usage: 24 MB % 268.54/38.10 % (1465503)Instructions burned: 2359 (million) % 268.54/38.10 % (1465505)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=753884700:i=1778:ins=1:rtra=on_2775 on theBenchmark for (2775ds/1778Mi) % 268.54/38.10 % (1465505)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.54/38.10 % (1465505)Terminated due to inappropriate strategy. % 268.54/38.10 % (1465505)------------------------------ % 268.54/38.10 % (1465505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.54/38.10 % (1465505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.54/38.10 % (1465505)CaDiCaL version: 2.1.3 % 268.54/38.10 % (1465505)Termination reason: Inappropriate % 268.54/38.10 % (1465505)Time elapsed: 0.001 s % 268.54/38.10 % (1465505)Peak memory usage: 10 MB % 268.54/38.10 % (1465505)Instructions burned: 1 (million) % 268.54/38.10 % (1465505)------------------------------ % 268.54/38.10 % (1465505)------------------------------ % 268.54/38.10 % (1465507)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=1900224603:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/1384Mi) % 268.54/38.10 % (1465507)Instruction limit reached! % 268.54/38.10 % (1465507)------------------------------ % 268.54/38.10 % (1465507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.54/38.10 % (1465507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.54/38.10 % (1465507)CaDiCaL version: 2.1.3 % 268.54/38.10 % (1465507)Termination reason: Instruction limit % 268.54/38.10 % (1465507)Termination phase: Saturation % 268.54/38.10 % (1465507)Time elapsed: 0.783 s % 268.54/38.10 % (1465507)Peak memory usage: 24 MB % 268.54/38.10 % (1465507)Instructions burned: 1385 (million) % 268.54/38.10 % (1465509)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2397190363:i=1758:kws=inv_precedence:fsr=off:rtra=on_2767 on theBenchmark for (2767ds/1758Mi) % 268.54/38.10 % (1465509)Instruction limit reached! % 268.54/38.10 % (1465509)------------------------------ % 268.54/38.10 % (1465509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.54/38.10 % (1465509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.54/38.10 % (1465509)CaDiCaL version: 2.1.3 % 268.54/38.10 % (1465509)Termination reason: Instruction limit % 268.54/38.10 % (1465509)Termination phase: Saturation % 268.54/38.10 % (1465509)Time elapsed: 0.997 s % 268.54/38.10 % (1465509)Peak memory usage: 25 MB % 268.54/38.10 % (1465509)Instructions burned: 1758 (million) % 268.54/38.10 % (1465511)fmb+10_1_sil=64000:si=on:random_seed=884333620:i=44122:nm=2:rtra=on:gsp=on_2756 on theBenchmark for (2756ds/44122Mi) % 268.54/38.10 % (1465511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.54/38.10 % (1465511)Terminated due to inappropriate strategy. % 268.54/38.10 % (1465511)------------------------------ % 268.54/38.10 % (1465511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.54/38.10 % (1465511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.54/38.10 % (1465511)CaDiCaL version: 2.1.3 % 268.54/38.10 % (1465511)Termination reason: Inappropriate % 268.54/38.10 % (1465511)Time elapsed: 0.001 s % 268.54/38.10 % (1465511)Peak memory usage: 10 MB % 268.54/38.10 % (1465511)Instructions burned: 1 (million) % 268.54/38.10 % (1465511)------------------------------ % 268.54/38.10 % (1465511)------------------------------ % 268.54/38.10 % (1465513)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2000581373:i=19030:nm=5:rtra=on_2756 on theBenchmark for (2756ds/19030Mi) % 300.01/42.54 % (1465513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1465513)Terminated due to inappropriate strategy. % 300.01/42.54 % (1465513)------------------------------ % 300.01/42.54 % (1465513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1465513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1465513)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1465513)Termination reason: Inappropriate % 300.01/42.54 % (1465513)Time elapsed: 0.001 s % 300.01/42.54 % (1465513)Peak memory usage: 10 MB % 300.01/42.54 % (1465513)Instructions burned: 1 (million) % 300.01/42.54 % (1465513)------------------------------ % 300.01/42.54 % (1465513)------------------------------ % 300.01/42.54 % (1465515)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4030955762:fmbsr=1.7:i=1840:rtra=on_2756 on theBenchmark for (2756ds/1840Mi) % 300.01/42.54 % (1465515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1465515)Terminated due to inappropriate strategy. % 300.01/42.54 % (1465515)------------------------------ % 300.01/42.54 % (1465515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1465515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1465515)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1465515)Termination reason: Inappropriate % 300.01/42.54 % (1465515)Time elapsed: 0.001 s % 300.01/42.54 % (1465515)Peak memory usage: 10 MB % 300.01/42.54 % (1465515)Instructions burned: 1 (million) % 300.01/42.54 % (1465515)------------------------------ % 300.01/42.54 % (1465515)------------------------------ % 300.01/42.54 % (1465517)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2168598908:i=10262:rtra=on_2756 on theBenchmark for (2756ds/10262Mi) % 300.01/42.54 % (1465465)Instruction limit reached! % 300.01/42.54 % (1465465)------------------------------ % 300.01/42.54 % (1465465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1465465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1465465)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1465465)Termination reason: Instruction limit % 300.01/42.54 % (1465465)Termination phase: Saturation % 300.01/42.54 % (1465465)Time elapsed: 12.354 s % 300.01/42.54 % (1465465)Peak memory usage: 26 MB % 300.01/42.54 % (1465465)Instructions burned: 28121 (million) % 300.01/42.54 % (1465519)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1122361490:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2714 on theBenchmark for (2714ds/2944Mi) % 300.01/42.54 % (1465519)Instruction limit reached! % 300.01/42.54 % (1465519)------------------------------ % 300.01/42.54 % (1465519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1465519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1465519)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1465519)Termination reason: Instruction limit % 300.01/42.54 % (1465519)Termination phase: Saturation % 300.01/42.54 % (1465519)Time elapsed: 1.637 s % 300.01/42.54 % (1465519)Peak memory usage: 61 MB % 300.01/42.54 % (1465519)Instructions burned: 2944 (million) % 300.01/42.54 % (1465521)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1526300948:i=12648:rtra=on_2698 on theBenchmark for (2698ds/12648Mi) % 300.01/42.54 % (1465521)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1465521)Terminated due to inappropriate strategy. % 300.01/42.54 % (1465521)------------------------------ % 300.01/42.54 % (1465521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1465521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1465521)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1465521)Termination reason: Inappropriate % 300.01/42.54 % (1465521)Time elapsed: 0.001 s % 300.01/42.54 % (1465521)Peak memory usage: 10 MB % 300.01/42.54 % (1465521)Instructions burned: 1 (million) % 300.01/42.54 % (1465521)------------------------------ % 300.01/42.54 % (1465521)------------------------------ % 300.01/42.54 % (1465523)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=118184244:fmbsr=2.30978:i=4348:rtra=on_2698 on theBenchmark for (2698ds/4348Mi) % 300.01/42.54 % (1465523)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1465523)Terminated due to inappropriate strategy. % 300.01/42.54 % (1465523)------------------------------ % 300.01/42.54 % (1465523 % 300.01/42.54 Terminated % 300.01/42.54 % Vampire exiting % 300.01/42.54 Terminated %------------------------------------------------------------------------------