%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW838_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.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 290.98s 41.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW838_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.18 % Computer : n010.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 14:31:32 UTC 2026 % 0.10/0.18 % CPUTime : % 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 Running first-order model finding % 0.10/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.19/0.90 % (1967364)Will run a generic schedule for satisfiability detection. % 4.19/0.90 % (1967392)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2055902152:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.19/0.90 % (1967387)% WARNING: option uhcvi not known. % 4.19/0.90 % (1967386)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2613432106_2999 on theBenchmark for (2999ds/0Mi) % 4.19/0.90 % (1967391)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2977522681:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.19/0.90 % (1967387)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1417696914:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.19/0.90 % (1967388)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4202831684:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.19/0.90 % (1967390)dis+10_1_sil=32000:sp=arity:random_seed=2515471660:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.19/0.90 % (1967393)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4247154936:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.19/0.90 % (1967392)Instruction limit reached! % 4.19/0.90 % (1967392)------------------------------ % 4.19/0.90 % (1967392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/0.90 % (1967392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/0.90 % (1967392)CaDiCaL version: 2.1.3 % 4.19/0.90 % (1967392)Termination reason: Instruction limit % 4.19/0.90 % (1967392)Termination phase: Saturation % 4.19/0.90 % (1967392)Time elapsed: 0.038 s % 4.19/0.90 % (1967392)Peak memory usage: 14 MB % 4.19/0.90 % (1967392)Instructions burned: 133 (million) % 4.19/0.90 % (1967386)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.19/0.90 % (1967386)Terminated due to inappropriate strategy. % 4.19/0.90 % (1967386)------------------------------ % 4.19/0.90 % (1967386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/0.90 % (1967386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/0.90 % (1967386)CaDiCaL version: 2.1.3 % 4.19/0.90 % (1967386)Termination reason: Inappropriate % 4.19/0.90 % (1967386)Time elapsed: 0.031 s % 4.19/0.90 % (1967386)Peak memory usage: 12 MB % 4.19/0.90 % (1967386)Instructions burned: 67 (million) % 4.19/0.90 % (1967386)------------------------------ % 4.19/0.90 % (1967386)------------------------------ % 4.19/0.90 % (1967432)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=13296445:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.19/0.90 % (1967433)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=447081485:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.19/0.90 % (1967390)Instruction limit reached! % 4.19/0.90 % (1967390)------------------------------ % 4.19/0.90 % (1967390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/0.90 % (1967390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/0.90 % (1967390)CaDiCaL version: 2.1.3 % 4.19/0.90 % (1967390)Termination reason: Instruction limit % 4.19/0.90 % (1967390)Termination phase: Saturation % 4.19/0.90 % (1967390)Time elapsed: 0.054 s % 4.19/0.90 % (1967390)Peak memory usage: 13 MB % 4.19/0.90 % (1967390)Instructions burned: 104 (million) % 4.19/0.90 % (1967432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.19/0.90 % (1967432)Terminated due to inappropriate strategy. % 4.19/0.90 % (1967432)------------------------------ % 4.19/0.90 % (1967432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/0.90 % (1967432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/0.90 % (1967432)CaDiCaL version: 2.1.3 % 4.19/0.90 % (1967432)Termination reason: Inappropriate % 4.19/0.90 % (1967432)Time elapsed: 0.017 s % 4.19/0.90 % (1967432)Peak memory usage: 12 MB % 4.19/0.90 % (1967432)Instructions burned: 67 (million) % 4.19/0.90 % (1967432)------------------------------ % 4.19/0.90 % (1967432)------------------------------ % 4.19/0.90 % (1967391)Instruction limit reached! % 4.19/0.90 % (1967391)------------------------------ % 4.19/0.90 % (1967391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/0.90 % (1967391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/0.90 % (1967391)CaDiCaL version: 2.1.3 % 4.19/0.90 % (1967391)Termination reason: Instruction limit % 6.15/1.14 % (1967391)Termination phase: Saturation % 6.15/1.14 % (1967391)Time elapsed: 0.061 s % 6.15/1.14 % (1967391)Peak memory usage: 14 MB % 6.15/1.14 % (1967391)Instructions burned: 116 (million) % 6.15/1.14 % (1967442)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=406754221:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.15/1.14 % (1967440)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=1381989124:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.15/1.14 % (1967441)ott-21_1_sil=16000:fs=off:random_seed=2465173909:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.15/1.14 % (1967393)Instruction limit reached! % 6.15/1.14 % (1967393)------------------------------ % 6.15/1.14 % (1967393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.14 % (1967393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.14 % (1967393)CaDiCaL version: 2.1.3 % 6.15/1.14 % (1967393)Termination reason: Instruction limit % 6.15/1.14 % (1967393)Termination phase: Saturation % 6.15/1.14 % (1967393)Time elapsed: 0.088 s % 6.15/1.14 % (1967393)Peak memory usage: 14 MB % 6.15/1.14 % (1967393)Instructions burned: 161 (million) % 6.15/1.14 % (1967446)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2139465320:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.15/1.14 % (1967433)Instruction limit reached! % 6.15/1.14 % (1967433)------------------------------ % 6.15/1.14 % (1967433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.14 % (1967433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.14 % (1967433)CaDiCaL version: 2.1.3 % 6.15/1.14 % (1967433)Termination reason: Instruction limit % 6.15/1.14 % (1967433)Termination phase: Saturation % 6.15/1.14 % (1967433)Time elapsed: 0.071 s % 6.15/1.14 % (1967433)Peak memory usage: 14 MB % 6.15/1.14 % (1967433)Instructions burned: 131 (million) % 6.15/1.14 % (1967446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.15/1.14 % (1967446)Terminated due to inappropriate strategy. % 6.15/1.14 % (1967446)------------------------------ % 6.15/1.14 % (1967446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.14 % (1967446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.14 % (1967446)CaDiCaL version: 2.1.3 % 6.15/1.14 % (1967446)Termination reason: Inappropriate % 6.15/1.14 % (1967446)Time elapsed: 0.030 s % 6.15/1.14 % (1967446)Peak memory usage: 11 MB % 6.15/1.14 % (1967446)Instructions burned: 66 (million) % 6.15/1.14 % (1967446)------------------------------ % 6.15/1.14 % (1967446)------------------------------ % 6.15/1.14 % (1967448)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2257735309:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.15/1.14 % (1967449)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3529643640:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.15/1.14 % (1967441)Instruction limit reached! % 6.15/1.14 % (1967441)------------------------------ % 6.15/1.14 % (1967441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.14 % (1967441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.14 % (1967441)CaDiCaL version: 2.1.3 % 6.15/1.14 % (1967441)Termination reason: Instruction limit % 6.15/1.14 % (1967441)Termination phase: Saturation % 6.15/1.14 % (1967441)Time elapsed: 0.086 s % 6.15/1.14 % (1967441)Peak memory usage: 13 MB % 6.15/1.14 % (1967441)Instructions burned: 181 (million) % 6.15/1.14 % (1967452)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=3162527152:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.15/1.14 % (1967449)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.15/1.14 % (1967449)Terminated due to inappropriate strategy. % 6.15/1.14 % (1967449)------------------------------ % 6.15/1.14 % (1967449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.14 % (1967449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.14 % (1967449)CaDiCaL version: 2.1.3 % 6.15/1.14 % (1967449)Termination reason: Inappropriate % 6.15/1.14 % (1967449)Time elapsed: 0.031 s % 6.15/1.14 % (1967449)Peak memory usage: 12 MB % 17.85/2.99 % (1967449)Instructions burned: 68 (million) % 17.85/2.99 % (1967449)------------------------------ % 17.85/2.99 % (1967449)------------------------------ % 17.85/2.99 % (1967454)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3467595616:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.85/2.99 % (1967442)Instruction limit reached! % 17.85/2.99 % (1967442)------------------------------ % 17.85/2.99 % (1967442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.85/2.99 % (1967442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/2.99 % (1967442)CaDiCaL version: 2.1.3 % 17.85/2.99 % (1967442)Termination reason: Instruction limit % 17.85/2.99 % (1967442)Termination phase: Saturation % 17.85/2.99 % (1967442)Time elapsed: 0.162 s % 17.85/2.99 % (1967442)Peak memory usage: 15 MB % 17.85/2.99 % (1967442)Instructions burned: 477 (million) % 17.85/2.99 % (1967456)fmb+10_1_sil=64000:random_seed=3611219108:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.85/2.99 % (1967456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.85/2.99 % (1967456)Terminated due to inappropriate strategy. % 17.85/2.99 % (1967456)------------------------------ % 17.85/2.99 % (1967456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.85/2.99 % (1967456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/2.99 % (1967456)CaDiCaL version: 2.1.3 % 17.85/2.99 % (1967456)Termination reason: Inappropriate % 17.85/2.99 % (1967456)Time elapsed: 0.016 s % 17.85/2.99 % (1967456)Peak memory usage: 12 MB % 17.85/2.99 % (1967456)Instructions burned: 68 (million) % 17.85/2.99 % (1967456)------------------------------ % 17.85/2.99 % (1967456)------------------------------ % 17.85/2.99 % (1967458)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2751284042:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 17.85/2.99 % (1967458)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.85/2.99 % (1967458)Terminated due to inappropriate strategy. % 17.85/2.99 % (1967458)------------------------------ % 17.85/2.99 % (1967458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.85/2.99 % (1967458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/2.99 % (1967458)CaDiCaL version: 2.1.3 % 17.85/2.99 % (1967458)Termination reason: Inappropriate % 17.85/2.99 % (1967458)Time elapsed: 0.016 s % 17.85/2.99 % (1967458)Peak memory usage: 12 MB % 17.85/2.99 % (1967458)Instructions burned: 67 (million) % 17.85/2.99 % (1967458)------------------------------ % 17.85/2.99 % (1967458)------------------------------ % 17.85/2.99 % (1967460)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=377409096:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 17.85/2.99 % (1967460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.85/2.99 % (1967460)Terminated due to inappropriate strategy. % 17.85/2.99 % (1967460)------------------------------ % 17.85/2.99 % (1967460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.85/2.99 % (1967460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/2.99 % (1967460)CaDiCaL version: 2.1.3 % 17.85/2.99 % (1967460)Termination reason: Inappropriate % 17.85/2.99 % (1967460)Time elapsed: 0.016 s % 17.85/2.99 % (1967460)Peak memory usage: 12 MB % 17.85/2.99 % (1967460)Instructions burned: 67 (million) % 17.85/2.99 % (1967460)------------------------------ % 17.85/2.99 % (1967460)------------------------------ % 17.85/2.99 % (1967462)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2821510090:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.85/2.99 % (1967440)Instruction limit reached! % 17.85/2.99 % (1967440)------------------------------ % 17.85/2.99 % (1967440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.85/2.99 % (1967440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/2.99 % (1967440)CaDiCaL version: 2.1.3 % 17.85/2.99 % (1967440)Termination reason: Instruction limit % 17.85/2.99 % (1967440)Termination phase: Saturation % 17.85/2.99 % (1967440)Time elapsed: 0.404 s % 17.85/2.99 % (1967440)Peak memory usage: 18 MB % 17.85/2.99 % (1967440)Instructions burned: 684 (million) % 17.85/2.99 % (1967464)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1965015837:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 17.85/2.99 % (1967452)Instruction limit reached! % 17.85/2.99 % (1967452)------------------------------ % 26.86/4.11 % (1967452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967452)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967452)Termination reason: Instruction limit % 26.86/4.11 % (1967452)Termination phase: Saturation % 26.86/4.11 % (1967452)Time elapsed: 0.430 s % 26.86/4.11 % (1967452)Peak memory usage: 21 MB % 26.86/4.11 % (1967452)Instructions burned: 692 (million) % 26.86/4.11 % (1967466)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1537115315:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 26.86/4.11 % (1967466)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.11 % (1967466)Terminated due to inappropriate strategy. % 26.86/4.11 % (1967466)------------------------------ % 26.86/4.11 % (1967466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967466)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967466)Termination reason: Inappropriate % 26.86/4.11 % (1967466)Time elapsed: 0.031 s % 26.86/4.11 % (1967466)Peak memory usage: 12 MB % 26.86/4.11 % (1967466)Instructions burned: 67 (million) % 26.86/4.11 % (1967466)------------------------------ % 26.86/4.11 % (1967466)------------------------------ % 26.86/4.11 % (1967468)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4191349215:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 26.86/4.11 % (1967454)Instruction limit reached! % 26.86/4.11 % (1967454)------------------------------ % 26.86/4.11 % (1967454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967454)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967454)Termination reason: Instruction limit % 26.86/4.11 % (1967454)Termination phase: Saturation % 26.86/4.11 % (1967454)Time elapsed: 0.496 s % 26.86/4.11 % (1967454)Peak memory usage: 19 MB % 26.86/4.11 % (1967454)Instructions burned: 880 (million) % 26.86/4.11 % (1967468)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.11 % (1967468)Terminated due to inappropriate strategy. % 26.86/4.11 % (1967468)------------------------------ % 26.86/4.11 % (1967468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967468)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967468)Termination reason: Inappropriate % 26.86/4.11 % (1967468)Time elapsed: 0.031 s % 26.86/4.11 % (1967468)Peak memory usage: 12 MB % 26.86/4.11 % (1967468)Instructions burned: 67 (million) % 26.86/4.11 % (1967468)------------------------------ % 26.86/4.11 % (1967468)------------------------------ % 26.86/4.11 % (1967470)ott-2_1_sil=16000:newcnf=on:random_seed=325835776:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 26.86/4.11 % (1967471)ott+10_1_sil=32000:tgt=ground:random_seed=2752473912:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 26.86/4.11 % (1967448)Instruction limit reached! % 26.86/4.11 % (1967448)------------------------------ % 26.86/4.11 % (1967448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967448)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967448)Termination reason: Instruction limit % 26.86/4.11 % (1967448)Termination phase: Saturation % 26.86/4.11 % (1967448)Time elapsed: 0.662 s % 26.86/4.11 % (1967448)Peak memory usage: 23 MB % 26.86/4.11 % (1967448)Instructions burned: 1179 (million) % 26.86/4.11 % (1967474)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2662353090:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 26.86/4.11 % (1967474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.11 % (1967474)Terminated due to inappropriate strategy. % 26.86/4.11 % (1967474)------------------------------ % 26.86/4.11 % (1967474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.11 % (1967474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.11 % (1967474)CaDiCaL version: 2.1.3 % 26.86/4.11 % (1967474)Termination reason: Inappropriate % 26.86/4.11 % (1967474)Time elapsed: 0.031 s % 26.86/4.11 % (1967474)Peak memory usage: 12 MB % 26.86/4.11 % (1967474)Instructions burned: 67 (million) % 89.08/12.81 % (1967474)------------------------------ % 89.08/12.81 % (1967474)------------------------------ % 89.08/12.81 % (1967476)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3770543999:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 89.08/12.81 % (1967470)Instruction limit reached! % 89.08/12.81 % (1967470)------------------------------ % 89.08/12.81 % (1967470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967470)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967470)Termination reason: Instruction limit % 89.08/12.81 % (1967470)Termination phase: Saturation % 89.08/12.81 % (1967470)Time elapsed: 0.386 s % 89.08/12.81 % (1967470)Peak memory usage: 16 MB % 89.08/12.81 % (1967470)Instructions burned: 875 (million) % 89.08/12.81 % (1967478)dis+21_1_sil=32000:sas=cadical:random_seed=961855333:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 89.08/12.81 % (1967464)Instruction limit reached! % 89.08/12.81 % (1967464)------------------------------ % 89.08/12.81 % (1967464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967464)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967464)Termination reason: Instruction limit % 89.08/12.81 % (1967464)Termination phase: Saturation % 89.08/12.81 % (1967464)Time elapsed: 0.790 s % 89.08/12.81 % (1967464)Peak memory usage: 31 MB % 89.08/12.81 % (1967464)Instructions burned: 1472 (million) % 89.08/12.81 % (1967480)ott+11_1_sil=16000:gs=on:random_seed=1343737775:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 89.08/12.81 % (1967462)Instruction limit reached! % 89.08/12.81 % (1967462)------------------------------ % 89.08/12.81 % (1967462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967462)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967462)Termination reason: Instruction limit % 89.08/12.81 % (1967462)Termination phase: Saturation % 89.08/12.81 % (1967462)Time elapsed: 1.361 s % 89.08/12.81 % (1967462)Peak memory usage: 21 MB % 89.08/12.81 % (1967462)Instructions burned: 5132 (million) % 89.08/12.81 % (1967482)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=508868415:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 89.08/12.81 % (1967482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.08/12.81 % (1967482)Terminated due to inappropriate strategy. % 89.08/12.81 % (1967482)------------------------------ % 89.08/12.81 % (1967482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967482)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967482)Termination reason: Inappropriate % 89.08/12.81 % (1967482)Time elapsed: 0.016 s % 89.08/12.81 % (1967482)Peak memory usage: 12 MB % 89.08/12.81 % (1967482)Instructions burned: 67 (million) % 89.08/12.81 % (1967482)------------------------------ % 89.08/12.81 % (1967482)------------------------------ % 89.08/12.81 % (1967484)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3283255477:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 89.08/12.81 % (1967480)Instruction limit reached! % 89.08/12.81 % (1967480)------------------------------ % 89.08/12.81 % (1967480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967480)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967480)Termination reason: Instruction limit % 89.08/12.81 % (1967480)Termination phase: Saturation % 89.08/12.81 % (1967480)Time elapsed: 1.204 s % 89.08/12.81 % (1967480)Peak memory usage: 23 MB % 89.08/12.81 % (1967480)Instructions burned: 2252 (million) % 89.08/12.81 % (1967486)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1911943343:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 89.08/12.81 % (1967476)Instruction limit reached! % 89.08/12.81 % (1967476)------------------------------ % 89.08/12.81 % (1967476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.08/12.81 % (1967476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.08/12.81 % (1967476)CaDiCaL version: 2.1.3 % 89.08/12.81 % (1967476)Termination reason: Instruction limit % 115.55/16.61 % (1967476)Termination phase: Saturation % 115.55/16.61 % (1967476)Time elapsed: 1.824 s % 115.55/16.61 % (1967476)Peak memory usage: 36 MB % 115.55/16.61 % (1967476)Instructions burned: 3512 (million) % 115.55/16.61 % (1967488)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=550462570:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 115.55/16.61 % (1967484)Instruction limit reached! % 115.55/16.61 % (1967484)------------------------------ % 115.55/16.61 % (1967484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.55/16.61 % (1967484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.55/16.61 % (1967484)CaDiCaL version: 2.1.3 % 115.55/16.61 % (1967484)Termination reason: Instruction limit % 115.55/16.61 % (1967484)Termination phase: Saturation % 115.55/16.61 % (1967484)Time elapsed: 1.047 s % 115.55/16.61 % (1967484)Peak memory usage: 37 MB % 115.55/16.61 % (1967484)Instructions burned: 4593 (million) % 115.55/16.61 % (1967490)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2074817676:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 115.55/16.61 % (1967490)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.55/16.61 % (1967490)Terminated due to inappropriate strategy. % 115.55/16.61 % (1967490)------------------------------ % 115.55/16.61 % (1967490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.55/16.61 % (1967490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.55/16.61 % (1967490)CaDiCaL version: 2.1.3 % 115.55/16.61 % (1967490)Termination reason: Inappropriate % 115.55/16.61 % (1967490)Time elapsed: 0.017 s % 115.55/16.61 % (1967490)Peak memory usage: 12 MB % 115.55/16.61 % (1967490)Instructions burned: 68 (million) % 115.55/16.61 % (1967490)------------------------------ % 115.55/16.61 % (1967490)------------------------------ % 115.55/16.61 % (1967492)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1463286920:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 115.55/16.61 % (1967492)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.55/16.61 % (1967492)Terminated due to inappropriate strategy. % 115.55/16.61 % (1967492)------------------------------ % 115.55/16.61 % (1967492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.55/16.61 % (1967492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.55/16.61 % (1967492)CaDiCaL version: 2.1.3 % 115.55/16.61 % (1967492)Termination reason: Inappropriate % 115.55/16.61 % (1967492)Time elapsed: 0.017 s % 115.55/16.61 % (1967492)Peak memory usage: 12 MB % 115.55/16.61 % (1967492)Instructions burned: 67 (million) % 115.55/16.61 % (1967492)------------------------------ % 115.55/16.61 % (1967492)------------------------------ % 115.55/16.61 % (1967494)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=797404157:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 115.55/16.61 % (1967494)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.55/16.61 % (1967494)Terminated due to inappropriate strategy. % 115.55/16.61 % (1967494)------------------------------ % 115.55/16.61 % (1967494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.55/16.61 % (1967494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.55/16.61 % (1967494)CaDiCaL version: 2.1.3 % 115.55/16.61 % (1967494)Termination reason: Inappropriate % 115.55/16.61 % (1967494)Time elapsed: 0.017 s % 115.55/16.61 % (1967494)Peak memory usage: 12 MB % 115.55/16.61 % (1967494)Instructions burned: 67 (million) % 115.55/16.61 % (1967494)------------------------------ % 115.55/16.61 % (1967494)------------------------------ % 115.55/16.61 % (1967496)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1203783854:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 115.55/16.61 % (1967478)Instruction limit reached! % 115.55/16.61 % (1967478)------------------------------ % 115.55/16.61 % (1967478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.55/16.61 % (1967478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.55/16.61 % (1967478)CaDiCaL version: 2.1.3 % 115.55/16.61 % (1967478)Termination reason: Instruction limit % 115.55/16.61 % (1967478)Termination phase: Saturation % 115.55/16.61 % (1967478)Time elapsed: 1.915 s % 115.55/16.61 % (1967478)Peak memory usage: 23 MB % 115.55/16.61 % (1967478)Instructions burned: 3773 (million) % 115.55/16.61 % (1967498)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2103031464:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 117.29/17.06 % (1967471)Instruction limit reached! % 117.29/17.06 % (1967471)------------------------------ % 117.29/17.06 % (1967471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967471)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967471)Termination reason: Instruction limit % 117.29/17.06 % (1967471)Termination phase: Saturation % 117.29/17.06 % (1967471)Time elapsed: 3.082 s % 117.29/17.06 % (1967471)Peak memory usage: 56 MB % 117.29/17.06 % (1967471)Instructions burned: 5115 (million) % 117.29/17.06 % (1967500)dis+10_16:1_sil=16000:random_seed=269542603:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 117.29/17.06 % (1967488)Instruction limit reached! % 117.29/17.06 % (1967488)------------------------------ % 117.29/17.06 % (1967488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967488)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967488)Termination reason: Instruction limit % 117.29/17.06 % (1967488)Termination phase: Saturation % 117.29/17.06 % (1967488)Time elapsed: 2.745 s % 117.29/17.06 % (1967488)Peak memory usage: 44 MB % 117.29/17.06 % (1967488)Instructions burned: 5211 (million) % 117.29/17.06 % (1967502)ott-3_8_sil=64000:random_seed=836416717:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 117.29/17.06 % (1967498)Instruction limit reached! % 117.29/17.06 % (1967498)------------------------------ % 117.29/17.06 % (1967498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967498)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967498)Termination reason: Instruction limit % 117.29/17.06 % (1967498)Termination phase: Saturation % 117.29/17.06 % (1967498)Time elapsed: 4.963 s % 117.29/17.06 % (1967498)Peak memory usage: 81 MB % 117.29/17.06 % (1967498)Instructions burned: 8173 (million) % 117.29/17.06 % (1967504)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3005996594:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 117.29/17.06 % (1967504)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.29/17.06 % (1967504)Terminated due to inappropriate strategy. % 117.29/17.06 % (1967504)------------------------------ % 117.29/17.06 % (1967504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967504)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967504)Termination reason: Inappropriate % 117.29/17.06 % (1967504)Time elapsed: 0.032 s % 117.29/17.06 % (1967504)Peak memory usage: 12 MB % 117.29/17.06 % (1967504)Instructions burned: 67 (million) % 117.29/17.06 % (1967504)------------------------------ % 117.29/17.06 % (1967504)------------------------------ % 117.29/17.06 % (1967506)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3564241265:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 117.29/17.06 % (1967500)Instruction limit reached! % 117.29/17.06 % (1967500)------------------------------ % 117.29/17.06 % (1967500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967500)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967500)Termination reason: Instruction limit % 117.29/17.06 % (1967500)Termination phase: Saturation % 117.29/17.06 % (1967500)Time elapsed: 4.966 s % 117.29/17.06 % (1967500)Peak memory usage: 62 MB % 117.29/17.06 % (1967500)Instructions burned: 9155 (million) % 117.29/17.06 % (1967508)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1704425197:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 117.29/17.06 % (1967496)Instruction limit reached! % 117.29/17.06 % (1967496)------------------------------ % 117.29/17.06 % (1967496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.29/17.06 % (1967496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.29/17.06 % (1967496)CaDiCaL version: 2.1.3 % 117.29/17.06 % (1967496)Termination reason: Instruction limit % 117.29/17.06 % (1967496)Termination phase: Saturation % 117.29/17.06 % (1967496)Time elapsed: 6.127 s % 117.29/17.06 % (1967496)Peak memory usage: 522 MB % 117.29/17.06 % (1967496)Instructions burned: 22568 (million) % 117.29/17.06 % (1967510)dis+33_16_sil=32000:sac=on:random_seed=3992279005:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 117.29/17.06 % (1967510)Instruction limit reached! % 117.29/17.06 % (1967510)------------------------------ % 117.29/17.06 % (1967510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967510)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967510)Termination reason: Instruction limit % 144.30/20.65 % (1967510)Termination phase: Saturation % 144.30/20.65 % (1967510)Time elapsed: 3.458 s % 144.30/20.65 % (1967510)Peak memory usage: 18 MB % 144.30/20.65 % (1967510)Instructions burned: 15856 (million) % 144.30/20.65 % (1967512)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2466125032:avsq=on:i=17627:add=on:amm=off_2874 on theBenchmark for (2874ds/17627Mi) % 144.30/20.65 % (1967506)Instruction limit reached! % 144.30/20.65 % (1967506)------------------------------ % 144.30/20.65 % (1967506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967506)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967506)Termination reason: Instruction limit % 144.30/20.65 % (1967506)Termination phase: Saturation % 144.30/20.65 % (1967506)Time elapsed: 6.822 s % 144.30/20.65 % (1967506)Peak memory usage: 85 MB % 144.30/20.65 % (1967506)Instructions burned: 11405 (million) % 144.30/20.65 % (1967749)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2924324201:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 144.30/20.65 % (1967502)Instruction limit reached! % 144.30/20.65 % (1967502)------------------------------ % 144.30/20.65 % (1967502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967502)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967502)Termination reason: Instruction limit % 144.30/20.65 % (1967502)Termination phase: Saturation % 144.30/20.65 % (1967502)Time elapsed: 10.152 s % 144.30/20.65 % (1967502)Peak memory usage: 90 MB % 144.30/20.65 % (1967502)Instructions burned: 20139 (million) % 144.30/20.65 % (1967805)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=469390211:i=26857:ins=20_2842 on theBenchmark for (2842ds/26857Mi) % 144.30/20.65 % (1967805)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.30/20.65 % (1967805)Terminated due to inappropriate strategy. % 144.30/20.65 % (1967805)------------------------------ % 144.30/20.65 % (1967805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967805)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967805)Termination reason: Inappropriate % 144.30/20.65 % (1967805)Time elapsed: 0.044 s % 144.30/20.65 % (1967805)Peak memory usage: 12 MB % 144.30/20.65 % (1967805)Instructions burned: 67 (million) % 144.30/20.65 % (1967805)------------------------------ % 144.30/20.65 % (1967805)------------------------------ % 144.30/20.65 % (1967808)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=406749813:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 144.30/20.65 % (1967486)Instruction limit reached! % 144.30/20.65 % (1967486)------------------------------ % 144.30/20.65 % (1967486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967486)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967486)Termination reason: Instruction limit % 144.30/20.65 % (1967486)Termination phase: Saturation % 144.30/20.65 % (1967486)Time elapsed: 13.600 s % 144.30/20.65 % (1967486)Peak memory usage: 50 MB % 144.30/20.65 % (1967486)Instructions burned: 29341 (million) % 144.30/20.65 % (1967816)fmb+10_1_sil=256000:fmbss=7:random_seed=3040641829:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 144.30/20.65 % (1967816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.30/20.65 % (1967816)Terminated due to inappropriate strategy. % 144.30/20.65 % (1967816)------------------------------ % 144.30/20.65 % (1967816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.30/20.65 % (1967816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.30/20.65 % (1967816)CaDiCaL version: 2.1.3 % 144.30/20.65 % (1967816)Termination reason: Inappropriate % 144.30/20.65 % (1967816)Time elapsed: 0.075 s % 144.30/20.65 % (1967816)Peak memory usage: 12 MB % 144.30/20.65 % (1967816)Instructions burned: 67 (million) % 144.30/20.65 % (1967816)------------------------------ % 144.30/20.65 % (1967816)------------------------------ % 144.30/20.65 % (1967819)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=627946430:i=44625:gsp=on_2836 on theBenchmark for (2836ds/44625Mi) % 157.25/22.42 % (1967819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.25/22.42 % (1967819)Terminated due to inappropriate strategy. % 157.25/22.42 % (1967819)------------------------------ % 157.25/22.42 % (1967819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.25/22.42 % (1967819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.25/22.42 % (1967819)CaDiCaL version: 2.1.3 % 157.25/22.42 % (1967819)Termination reason: Inappropriate % 157.25/22.42 % (1967819)Time elapsed: 0.071 s % 157.25/22.42 % (1967819)Peak memory usage: 12 MB % 157.25/22.42 % (1967819)Instructions burned: 67 (million) % 157.25/22.42 % (1967819)------------------------------ % 157.25/22.42 % (1967819)------------------------------ % 157.25/22.42 % (1967821)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1389161920:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 157.25/22.42 % (1967821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.25/22.42 % (1967821)Terminated due to inappropriate strategy. % 157.25/22.42 % (1967821)------------------------------ % 157.25/22.42 % (1967821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.25/22.42 % (1967821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.25/22.42 % (1967821)CaDiCaL version: 2.1.3 % 157.25/22.42 % (1967821)Termination reason: Inappropriate % 157.25/22.42 % (1967821)Time elapsed: 0.063 s % 157.25/22.42 % (1967821)Peak memory usage: 12 MB % 157.25/22.42 % (1967821)Instructions burned: 67 (million) % 157.25/22.42 % (1967821)------------------------------ % 157.25/22.42 % (1967821)------------------------------ % 157.25/22.42 % (1967825)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1685970725:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 157.25/22.42 % (1967825)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.25/22.42 % (1967825)Terminated due to inappropriate strategy. % 157.25/22.42 % (1967825)------------------------------ % 157.25/22.42 % (1967825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.25/22.42 % (1967825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.25/22.42 % (1967825)CaDiCaL version: 2.1.3 % 157.25/22.42 % (1967825)Termination reason: Inappropriate % 157.25/22.42 % (1967825)Time elapsed: 0.032 s % 157.25/22.42 % (1967825)Peak memory usage: 12 MB % 157.25/22.42 % (1967825)Instructions burned: 67 (million) % 157.25/22.42 % (1967825)------------------------------ % 157.25/22.42 % (1967825)------------------------------ % 157.25/22.42 % (1967827)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1740862231:fmbsr=2:i=185024:ins=7_2833 on theBenchmark for (2833ds/185024Mi) % 157.25/22.42 % (1967827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.25/22.42 % (1967827)Terminated due to inappropriate strategy. % 157.25/22.42 % (1967827)------------------------------ % 157.25/22.42 % (1967827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.25/22.42 % (1967827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.25/22.42 % (1967827)CaDiCaL version: 2.1.3 % 157.25/22.42 % (1967827)Termination reason: Inappropriate % 157.25/22.42 % (1967827)Time elapsed: 0.033 s % 157.25/22.42 % (1967827)Peak memory usage: 12 MB % 157.25/22.42 % (1967827)Instructions burned: 67 (million) % 157.25/22.42 % (1967827)------------------------------ % 157.25/22.42 % (1967827)------------------------------ % 157.25/22.42 % (1967829)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1765596817:rtra=on_2833 on theBenchmark for (2833ds/0Mi) % 157.25/22.42 % (1967829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.25/22.42 % (1967829)Terminated due to inappropriate strategy. % 157.25/22.42 % (1967829)------------------------------ % 157.25/22.42 % (1967829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.25/22.42 % (1967829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.25/22.42 % (1967829)CaDiCaL version: 2.1.3 % 157.25/22.42 % (1967829)Termination reason: Inappropriate % 157.25/22.42 % (1967829)Time elapsed: 0.068 s % 157.25/22.42 % (1967829)Peak memory usage: 12 MB % 157.25/22.42 % (1967829)Instructions burned: 73 (million) % 157.25/22.42 % (1967829)------------------------------ % 157.25/22.42 % (1967829)------------------------------ % 157.25/22.42 % (1967833)% WARNING: option uhcvi not known. % 157.25/22.42 % (1967833)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1584465130:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 179.30/25.56 % (1967508)Instruction limit reached! % 179.30/25.56 % (1967508)------------------------------ % 179.30/25.56 % (1967508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967508)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967508)Termination reason: Instruction limit % 179.30/25.56 % (1967508)Termination phase: Saturation % 179.30/25.56 % (1967508)Time elapsed: 7.995 s % 179.30/25.56 % (1967508)Peak memory usage: 63 MB % 179.30/25.56 % (1967508)Instructions burned: 14135 (million) % 179.30/25.56 % (1967837)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=225594685:i=176048:add=on:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/176048Mi) % 179.30/25.56 % (1967512)Instruction limit reached! % 179.30/25.56 % (1967512)------------------------------ % 179.30/25.56 % (1967512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967512)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967512)Termination reason: Instruction limit % 179.30/25.56 % (1967512)Termination phase: Saturation % 179.30/25.56 % (1967512)Time elapsed: 7.072 s % 179.30/25.56 % (1967512)Peak memory usage: 180 MB % 179.30/25.56 % (1967512)Instructions burned: 17627 (million) % 179.30/25.56 % (1967847)dis+10_1_sil=32000:si=on:sp=arity:random_seed=727473093:i=206:fgj=on:rtra=on_2802 on theBenchmark for (2802ds/206Mi) % 179.30/25.56 % (1967847)Instruction limit reached! % 179.30/25.56 % (1967847)------------------------------ % 179.30/25.56 % (1967847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967847)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967847)Termination reason: Instruction limit % 179.30/25.56 % (1967847)Termination phase: Saturation % 179.30/25.56 % (1967847)Time elapsed: 0.111 s % 179.30/25.56 % (1967847)Peak memory usage: 15 MB % 179.30/25.56 % (1967847)Instructions burned: 207 (million) % 179.30/25.56 % (1967849)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2807638445:i=232:rtra=on_2801 on theBenchmark for (2801ds/232Mi) % 179.30/25.56 % (1967849)Instruction limit reached! % 179.30/25.56 % (1967849)------------------------------ % 179.30/25.56 % (1967849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967849)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967849)Termination reason: Instruction limit % 179.30/25.56 % (1967849)Termination phase: Saturation % 179.30/25.56 % (1967849)Time elapsed: 0.132 s % 179.30/25.56 % (1967849)Peak memory usage: 16 MB % 179.30/25.56 % (1967849)Instructions burned: 233 (million) % 179.30/25.56 % (1967851)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=367703615:i=262:rtra=on_2799 on theBenchmark for (2799ds/262Mi) % 179.30/25.56 % (1967851)Instruction limit reached! % 179.30/25.56 % (1967851)------------------------------ % 179.30/25.56 % (1967851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967851)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967851)Termination reason: Instruction limit % 179.30/25.56 % (1967851)Termination phase: Saturation % 179.30/25.56 % (1967851)Time elapsed: 0.139 s % 179.30/25.56 % (1967851)Peak memory usage: 16 MB % 179.30/25.56 % (1967851)Instructions burned: 263 (million) % 179.30/25.56 % (1967853)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=56029253:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2797 on theBenchmark for (2797ds/318Mi) % 179.30/25.56 % (1967853)Instruction limit reached! % 179.30/25.56 % (1967853)------------------------------ % 179.30/25.56 % (1967853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.30/25.56 % (1967853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.30/25.56 % (1967853)CaDiCaL version: 2.1.3 % 179.30/25.56 % (1967853)Termination reason: Instruction limit % 179.30/25.56 % (1967853)Termination phase: Saturation % 179.30/25.56 % (1967853)Time elapsed: 0.171 s % 179.30/25.56 % (1967853)Peak memory usage: 16 MB % 179.30/25.56 % (1967853)Instructions burned: 319 (million) % 179.30/25.56 % (1967855)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1047176508:i=1428:nm=2:rtra=on_2795 on theBenchmark for (2795ds/1428Mi) % 217.63/30.90 % (1967855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.63/30.90 % (1967855)Terminated due to inappropriate strategy. % 217.63/30.90 % (1967855)------------------------------ % 217.63/30.90 % (1967855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967855)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967855)Termination reason: Inappropriate % 217.63/30.90 % (1967855)Time elapsed: 0.036 s % 217.63/30.90 % (1967855)Peak memory usage: 12 MB % 217.63/30.90 % (1967855)Instructions burned: 73 (million) % 217.63/30.90 % (1967855)------------------------------ % 217.63/30.90 % (1967855)------------------------------ % 217.63/30.90 % (1967857)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=298459423:i=262:bd=preordered:rtra=on:fsd=on_2795 on theBenchmark for (2795ds/262Mi) % 217.63/30.90 % (1967857)Instruction limit reached! % 217.63/30.90 % (1967857)------------------------------ % 217.63/30.90 % (1967857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967857)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967857)Termination reason: Instruction limit % 217.63/30.90 % (1967857)Termination phase: Saturation % 217.63/30.90 % (1967857)Time elapsed: 0.148 s % 217.63/30.90 % (1967857)Peak memory usage: 16 MB % 217.63/30.90 % (1967857)Instructions burned: 262 (million) % 217.63/30.90 % (1967859)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=3788616215:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1368Mi) % 217.63/30.90 % (1967859)Instruction limit reached! % 217.63/30.90 % (1967859)------------------------------ % 217.63/30.90 % (1967859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967859)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967859)Termination reason: Instruction limit % 217.63/30.90 % (1967859)Termination phase: Saturation % 217.63/30.90 % (1967859)Time elapsed: 0.687 s % 217.63/30.90 % (1967859)Peak memory usage: 22 MB % 217.63/30.90 % (1967859)Instructions burned: 1369 (million) % 217.63/30.90 % (1967865)ott-21_1_sil=16000:si=on:fs=off:random_seed=4116469645:i=360:av=off:fsr=off:rtra=on_2786 on theBenchmark for (2786ds/360Mi) % 217.63/30.90 % (1967865)Instruction limit reached! % 217.63/30.90 % (1967865)------------------------------ % 217.63/30.90 % (1967865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967865)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967865)Termination reason: Instruction limit % 217.63/30.90 % (1967865)Termination phase: Saturation % 217.63/30.90 % (1967865)Time elapsed: 0.166 s % 217.63/30.90 % (1967865)Peak memory usage: 15 MB % 217.63/30.90 % (1967865)Instructions burned: 362 (million) % 217.63/30.90 % (1967869)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1522663572:i=954:bd=all:rtra=on_2784 on theBenchmark for (2784ds/954Mi) % 217.63/30.90 % (1967869)Instruction limit reached! % 217.63/30.90 % (1967869)------------------------------ % 217.63/30.90 % (1967869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967869)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967869)Termination reason: Instruction limit % 217.63/30.90 % (1967869)Termination phase: Saturation % 217.63/30.90 % (1967869)Time elapsed: 0.544 s % 217.63/30.90 % (1967869)Peak memory usage: 18 MB % 217.63/30.90 % (1967869)Instructions burned: 954 (million) % 217.63/30.90 % (1967871)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1704209060:fmbsr=1.3:i=1730:ins=25:rtra=on_2778 on theBenchmark for (2778ds/1730Mi) % 217.63/30.90 % (1967871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.63/30.90 % (1967871)Terminated due to inappropriate strategy. % 217.63/30.90 % (1967871)------------------------------ % 217.63/30.90 % (1967871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.63/30.90 % (1967871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.63/30.90 % (1967871)CaDiCaL version: 2.1.3 % 217.63/30.90 % (1967871)Termination reason: Inappropriate % 290.98/41.25 % (1967871)Time elapsed: 0.041 s % 290.98/41.25 % (1967871)Peak memory usage: 12 MB % 290.98/41.25 % (1967871)Instructions burned: 72 (million) % 290.98/41.25 % (1967871)------------------------------ % 290.98/41.25 % (1967871)------------------------------ % 290.98/41.25 % (1967873)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1202433916:i=2358:rtra=on_2777 on theBenchmark for (2777ds/2358Mi) % 290.98/41.25 % (1967873)Instruction limit reached! % 290.98/41.25 % (1967873)------------------------------ % 290.98/41.25 % (1967873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.25 % (1967873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.25 % (1967873)CaDiCaL version: 2.1.3 % 290.98/41.25 % (1967873)Termination reason: Instruction limit % 290.98/41.25 % (1967873)Termination phase: Saturation % 290.98/41.25 % (1967873)Time elapsed: 1.244 s % 290.98/41.25 % (1967873)Peak memory usage: 33 MB % 290.98/41.25 % (1967873)Instructions burned: 2358 (million) % 290.98/41.25 % (1967875)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=109392647:i=1778:ins=1:rtra=on_2765 on theBenchmark for (2765ds/1778Mi) % 290.98/41.25 % (1967875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.25 % (1967875)Terminated due to inappropriate strategy. % 290.98/41.25 % (1967875)------------------------------ % 290.98/41.25 % (1967875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.25 % (1967875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.25 % (1967875)CaDiCaL version: 2.1.3 % 290.98/41.25 % (1967875)Termination reason: Inappropriate % 290.98/41.25 % (1967875)Time elapsed: 0.050 s % 290.98/41.25 % (1967875)Peak memory usage: 13 MB % 290.98/41.25 % (1967875)Instructions burned: 74 (million) % 290.98/41.25 % (1967875)------------------------------ % 290.98/41.25 % (1967875)------------------------------ % 290.98/41.25 % (1967877)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=2114981324:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2764 on theBenchmark for (2764ds/1384Mi) % 290.98/41.25 % (1967877)Instruction limit reached! % 290.98/41.25 % (1967877)------------------------------ % 290.98/41.25 % (1967877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.25 % (1967877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.25 % (1967877)CaDiCaL version: 2.1.3 % 290.98/41.25 % (1967877)Termination reason: Instruction limit % 290.98/41.25 % (1967877)Termination phase: Saturation % 290.98/41.25 % (1967877)Time elapsed: 0.713 s % 290.98/41.25 % (1967877)Peak memory usage: 25 MB % 290.98/41.25 % (1967877)Instructions burned: 1386 (million) % 290.98/41.25 % (1967881)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3340704102:i=1758:kws=inv_precedence:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/1758Mi) % 290.98/41.25 % (1967881)Instruction limit reached! % 290.98/41.25 % (1967881)------------------------------ % 290.98/41.25 % (1967881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.25 % (1967881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.25 % (1967881)CaDiCaL version: 2.1.3 % 290.98/41.25 % (1967881)Termination reason: Instruction limit % 290.98/41.25 % (1967881)Termination phase: Saturation % 290.98/41.25 % (1967881)Time elapsed: 0.885 s % 290.98/41.25 % (1967881)Peak memory usage: 26 MB % 290.98/41.25 % (1967881)Instructions burned: 1760 (million) % 290.98/41.25 % (1967885)fmb+10_1_sil=64000:si=on:random_seed=395951406:i=44122:nm=2:rtra=on:gsp=on_2747 on theBenchmark for (2747ds/44122Mi) % 290.98/41.25 % (1967885)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.25 % (1967885)Terminated due to inappropriate strategy. % 290.98/41.25 % (1967885)------------------------------ % 290.98/41.25 % (1967885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.25 % (1967885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.25 % (1967885)CaDiCaL version: 2.1.3 % 290.98/41.25 % (1967885)Termination reason: Inappropriate % 290.98/41.25 % (1967885)Time elapsed: 0.040 s % 290.98/41.25 % (1967885)Peak memory usage: 13 MB % 290.98/41.25 % (1967885)Instructions burned: 74 (million) % 290.98/41.25 % (1967885)------------------------------ % 290.98/41.25 % (1967885)------------------------------ % 290.98/41.25 % (1967887)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4078807671:i=19030:nm=5:rtra=on_2746Terminated % 300.24/42.54 % Vampire exiting % 300.24/42.54 Terminated %------------------------------------------------------------------------------