%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW620_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:40:32 PM UTC 2026 % Result : Timeout 300.22s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW620_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.18 % Computer : n019.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 14:23:03 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.21 Running first-order model finding % 0.06/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 % 3.76/0.83 % (4030601)Will run a generic schedule for satisfiability detection. % 3.76/0.83 % (4030620)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2239115416:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.76/0.83 % (4030615)% WARNING: option uhcvi not known. % 3.76/0.83 % (4030614)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3054720866_2999 on theBenchmark for (2999ds/0Mi) % 3.76/0.83 % (4030616)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3660683944:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.76/0.83 % (4030618)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3405832395:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.76/0.83 % (4030617)dis+10_1_sil=32000:sp=arity:random_seed=1374510833:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.76/0.83 % (4030615)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2614541440:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.76/0.83 % (4030619)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=170903662:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.76/0.83 % (4030614)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.76/0.83 % (4030614)Terminated due to inappropriate strategy. % 3.76/0.83 % (4030614)------------------------------ % 3.76/0.83 % (4030614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.76/0.83 % (4030614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/0.83 % (4030614)CaDiCaL version: 2.1.3 % 3.76/0.83 % (4030614)Termination reason: Inappropriate % 3.76/0.83 % (4030614)Time elapsed: 0.006 s % 3.76/0.83 % (4030614)Peak memory usage: 11 MB % 3.76/0.83 % (4030614)Instructions burned: 11 (million) % 3.76/0.83 % (4030614)------------------------------ % 3.76/0.83 % (4030614)------------------------------ % 3.76/0.83 % (4030641)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=31646884:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.76/0.83 % (4030641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.76/0.83 % (4030641)Terminated due to inappropriate strategy. % 3.76/0.83 % (4030641)------------------------------ % 3.76/0.83 % (4030641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.76/0.83 % (4030641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/0.83 % (4030641)CaDiCaL version: 2.1.3 % 3.76/0.83 % (4030641)Termination reason: Inappropriate % 3.76/0.83 % (4030641)Time elapsed: 0.005 s % 3.76/0.83 % (4030641)Peak memory usage: 11 MB % 3.76/0.83 % (4030641)Instructions burned: 9 (million) % 3.76/0.83 % (4030641)------------------------------ % 3.76/0.83 % (4030641)------------------------------ % 3.76/0.83 % (4030620)Instruction limit reached! % 3.76/0.83 % (4030620)------------------------------ % 3.76/0.83 % (4030620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.76/0.83 % (4030620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/0.83 % (4030620)CaDiCaL version: 2.1.3 % 3.76/0.83 % (4030620)Termination reason: Instruction limit % 3.76/0.83 % (4030620)Termination phase: Saturation % 3.76/0.83 % (4030620)Time elapsed: 0.056 s % 3.76/0.83 % (4030620)Peak memory usage: 14 MB % 3.76/0.83 % (4030620)Instructions burned: 162 (million) % 3.76/0.83 % (4030644)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1703607212:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.76/0.83 % (4030651)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=815862472:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.76/0.83 % (4030617)Instruction limit reached! % 3.76/0.83 % (4030617)------------------------------ % 3.76/0.83 % (4030617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.76/0.83 % (4030617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/0.83 % (4030617)CaDiCaL version: 2.1.3 % 3.76/0.83 % (4030617)Termination reason: Instruction limit % 3.76/0.83 % (4030617)Termination phase: Saturation % 3.76/0.83 % (4030617)Time elapsed: 0.065 s % 3.76/0.83 % (4030617)Peak memory usage: 13 MB % 3.76/0.83 % (4030617)Instructions burned: 105 (million) % 3.76/0.83 % (4030618)Instruction limit reached! % 3.76/0.83 % (4030618)------------------------------ % 3.76/0.83 % (4030618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030618)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030618)Termination reason: Instruction limit % 5.72/1.12 % (4030618)Termination phase: Saturation % 5.72/1.12 % (4030618)Time elapsed: 0.078 s % 5.72/1.12 % (4030618)Peak memory usage: 13 MB % 5.72/1.12 % (4030618)Instructions burned: 121 (million) % 5.72/1.12 % (4030619)Instruction limit reached! % 5.72/1.12 % (4030619)------------------------------ % 5.72/1.12 % (4030619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030619)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030619)Termination reason: Instruction limit % 5.72/1.12 % (4030619)Termination phase: Saturation % 5.72/1.12 % (4030619)Time elapsed: 0.083 s % 5.72/1.12 % (4030619)Peak memory usage: 14 MB % 5.72/1.12 % (4030619)Instructions burned: 132 (million) % 5.72/1.12 % (4030655)ott-21_1_sil=16000:fs=off:random_seed=1897288381:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.72/1.12 % (4030658)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1329981144:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.72/1.12 % (4030661)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1253356513:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.72/1.12 % (4030661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.72/1.12 % (4030661)Terminated due to inappropriate strategy. % 5.72/1.12 % (4030661)------------------------------ % 5.72/1.12 % (4030661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030661)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030661)Termination reason: Inappropriate % 5.72/1.12 % (4030661)Time elapsed: 0.005 s % 5.72/1.12 % (4030661)Peak memory usage: 11 MB % 5.72/1.12 % (4030661)Instructions burned: 9 (million) % 5.72/1.12 % (4030661)------------------------------ % 5.72/1.12 % (4030661)------------------------------ % 5.72/1.12 % (4030672)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3665478174:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.72/1.12 % (4030644)Instruction limit reached! % 5.72/1.12 % (4030644)------------------------------ % 5.72/1.12 % (4030644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030644)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030644)Termination reason: Instruction limit % 5.72/1.12 % (4030644)Termination phase: Saturation % 5.72/1.12 % (4030644)Time elapsed: 0.080 s % 5.72/1.12 % (4030644)Peak memory usage: 13 MB % 5.72/1.12 % (4030644)Instructions burned: 131 (million) % 5.72/1.12 % (4030680)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3841746631:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.72/1.12 % (4030680)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.72/1.12 % (4030680)Terminated due to inappropriate strategy. % 5.72/1.12 % (4030680)------------------------------ % 5.72/1.12 % (4030680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030680)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030680)Termination reason: Inappropriate % 5.72/1.12 % (4030680)Time elapsed: 0.005 s % 5.72/1.12 % (4030680)Peak memory usage: 11 MB % 5.72/1.12 % (4030680)Instructions burned: 9 (million) % 5.72/1.12 % (4030680)------------------------------ % 5.72/1.12 % (4030680)------------------------------ % 5.72/1.12 % (4030685)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=2796427228: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.72/1.12 % (4030655)Instruction limit reached! % 5.72/1.12 % (4030655)------------------------------ % 5.72/1.12 % (4030655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.72/1.12 % (4030655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.72/1.12 % (4030655)CaDiCaL version: 2.1.3 % 5.72/1.12 % (4030655)Termination reason: Instruction limit % 5.72/1.12 % (4030655)Termination phase: Saturation % 19.92/3.04 % (4030655)Time elapsed: 0.096 s % 19.92/3.04 % (4030655)Peak memory usage: 13 MB % 19.92/3.04 % (4030655)Instructions burned: 181 (million) % 19.92/3.04 % (4030690)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2823014240:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.92/3.04 % (4030651)Instruction limit reached! % 19.92/3.04 % (4030651)------------------------------ % 19.92/3.04 % (4030651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.04 % (4030651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.04 % (4030651)CaDiCaL version: 2.1.3 % 19.92/3.04 % (4030651)Termination reason: Instruction limit % 19.92/3.04 % (4030651)Termination phase: Saturation % 19.92/3.04 % (4030651)Time elapsed: 0.209 s % 19.92/3.04 % (4030651)Peak memory usage: 18 MB % 19.92/3.04 % (4030651)Instructions burned: 686 (million) % 19.92/3.04 % (4030724)fmb+10_1_sil=64000:random_seed=1469853957:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.92/3.04 % (4030724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.92/3.04 % (4030724)Terminated due to inappropriate strategy. % 19.92/3.04 % (4030724)------------------------------ % 19.92/3.04 % (4030724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.04 % (4030724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.04 % (4030724)CaDiCaL version: 2.1.3 % 19.92/3.04 % (4030724)Termination reason: Inappropriate % 19.92/3.04 % (4030724)Time elapsed: 0.003 s % 19.92/3.04 % (4030724)Peak memory usage: 11 MB % 19.92/3.04 % (4030724)Instructions burned: 9 (million) % 19.92/3.04 % (4030724)------------------------------ % 19.92/3.04 % (4030724)------------------------------ % 19.92/3.04 % (4030734)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3136245380:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.92/3.04 % (4030734)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.92/3.04 % (4030734)Terminated due to inappropriate strategy. % 19.92/3.04 % (4030734)------------------------------ % 19.92/3.04 % (4030734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.04 % (4030734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.04 % (4030734)CaDiCaL version: 2.1.3 % 19.92/3.04 % (4030734)Termination reason: Inappropriate % 19.92/3.04 % (4030734)Time elapsed: 0.002 s % 19.92/3.04 % (4030734)Peak memory usage: 11 MB % 19.92/3.04 % (4030734)Instructions burned: 9 (million) % 19.92/3.04 % (4030734)------------------------------ % 19.92/3.04 % (4030734)------------------------------ % 19.92/3.04 % (4030743)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3478225488:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 19.92/3.04 % (4030743)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.92/3.04 % (4030743)Terminated due to inappropriate strategy. % 19.92/3.04 % (4030743)------------------------------ % 19.92/3.04 % (4030743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.04 % (4030743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.04 % (4030743)CaDiCaL version: 2.1.3 % 19.92/3.04 % (4030743)Termination reason: Inappropriate % 19.92/3.04 % (4030743)Time elapsed: 0.002 s % 19.92/3.04 % (4030743)Peak memory usage: 11 MB % 19.92/3.04 % (4030743)Instructions burned: 9 (million) % 19.92/3.04 % (4030743)------------------------------ % 19.92/3.04 % (4030743)------------------------------ % 19.92/3.04 % (4030748)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1681224372:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 19.92/3.04 % (4030658)Instruction limit reached! % 19.92/3.04 % (4030658)------------------------------ % 19.92/3.04 % (4030658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.92/3.04 % (4030658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.04 % (4030658)CaDiCaL version: 2.1.3 % 19.92/3.04 % (4030658)Termination reason: Instruction limit % 19.92/3.04 % (4030658)Termination phase: Saturation % 19.92/3.04 % (4030658)Time elapsed: 0.318 s % 19.92/3.04 % (4030658)Peak memory usage: 14 MB % 19.92/3.04 % (4030658)Instructions burned: 477 (million) % 19.92/3.04 % (4030755)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1812733610:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 19.92/3.04 % (4030685)Instruction limit reached! % 19.92/3.04 % (4030685)------------------------------ % 24.13/4.03 % (4030685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030685)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030685)Termination reason: Instruction limit % 24.13/4.03 % (4030685)Termination phase: Saturation % 24.13/4.03 % (4030685)Time elapsed: 0.394 s % 24.13/4.03 % (4030685)Peak memory usage: 19 MB % 24.13/4.03 % (4030685)Instructions burned: 693 (million) % 24.13/4.03 % (4030757)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2067415300:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 24.13/4.03 % (4030757)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.13/4.03 % (4030757)Terminated due to inappropriate strategy. % 24.13/4.03 % (4030757)------------------------------ % 24.13/4.03 % (4030757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030757)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030757)Termination reason: Inappropriate % 24.13/4.03 % (4030757)Time elapsed: 0.006 s % 24.13/4.03 % (4030757)Peak memory usage: 11 MB % 24.13/4.03 % (4030757)Instructions burned: 11 (million) % 24.13/4.03 % (4030757)------------------------------ % 24.13/4.03 % (4030757)------------------------------ % 24.13/4.03 % (4030759)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3037249032:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 24.13/4.03 % (4030759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.13/4.03 % (4030759)Terminated due to inappropriate strategy. % 24.13/4.03 % (4030759)------------------------------ % 24.13/4.03 % (4030759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030759)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030759)Termination reason: Inappropriate % 24.13/4.03 % (4030759)Time elapsed: 0.005 s % 24.13/4.03 % (4030759)Peak memory usage: 11 MB % 24.13/4.03 % (4030759)Instructions burned: 9 (million) % 24.13/4.03 % (4030759)------------------------------ % 24.13/4.03 % (4030759)------------------------------ % 24.13/4.03 % (4030761)ott-2_1_sil=16000:newcnf=on:random_seed=4041340268:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.13/4.03 % (4030690)Instruction limit reached! % 24.13/4.03 % (4030690)------------------------------ % 24.13/4.03 % (4030690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030690)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030690)Termination reason: Instruction limit % 24.13/4.03 % (4030690)Termination phase: Saturation % 24.13/4.03 % (4030690)Time elapsed: 0.520 s % 24.13/4.03 % (4030690)Peak memory usage: 19 MB % 24.13/4.03 % (4030690)Instructions burned: 880 (million) % 24.13/4.03 % (4030763)ott+10_1_sil=32000:tgt=ground:random_seed=187997273:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 24.13/4.03 % (4030672)Instruction limit reached! % 24.13/4.03 % (4030672)------------------------------ % 24.13/4.03 % (4030672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030672)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030672)Termination reason: Instruction limit % 24.13/4.03 % (4030672)Termination phase: Saturation % 24.13/4.03 % (4030672)Time elapsed: 0.713 s % 24.13/4.03 % (4030672)Peak memory usage: 22 MB % 24.13/4.03 % (4030672)Instructions burned: 1180 (million) % 24.13/4.03 % (4030765)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2036533241:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 24.13/4.03 % (4030765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.13/4.03 % (4030765)Terminated due to inappropriate strategy. % 24.13/4.03 % (4030765)------------------------------ % 24.13/4.03 % (4030765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.13/4.03 % (4030765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.13/4.03 % (4030765)CaDiCaL version: 2.1.3 % 24.13/4.03 % (4030765)Termination reason: Inappropriate % 24.13/4.03 % (4030765)Time elapsed: 0.006 s % 24.13/4.03 % (4030765)Peak memory usage: 11 MB % 24.13/4.03 % (4030765)Instructions burned: 11 (million) % 113.42/16.29 % (4030765)------------------------------ % 113.42/16.29 % (4030765)------------------------------ % 113.42/16.29 % (4030767)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=791294005:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 113.42/16.29 % (4030761)Instruction limit reached! % 113.42/16.29 % (4030761)------------------------------ % 113.42/16.29 % (4030761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030761)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030761)Termination reason: Instruction limit % 113.42/16.29 % (4030761)Termination phase: Saturation % 113.42/16.29 % (4030761)Time elapsed: 0.505 s % 113.42/16.29 % (4030761)Peak memory usage: 18 MB % 113.42/16.29 % (4030761)Instructions burned: 870 (million) % 113.42/16.29 % (4030769)dis+21_1_sil=32000:sas=cadical:random_seed=1865081468:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 113.42/16.29 % (4030755)Instruction limit reached! % 113.42/16.29 % (4030755)------------------------------ % 113.42/16.29 % (4030755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030755)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030755)Termination reason: Instruction limit % 113.42/16.29 % (4030755)Termination phase: Saturation % 113.42/16.29 % (4030755)Time elapsed: 0.810 s % 113.42/16.29 % (4030755)Peak memory usage: 28 MB % 113.42/16.29 % (4030755)Instructions burned: 1474 (million) % 113.42/16.29 % (4030771)ott+11_1_sil=16000:gs=on:random_seed=3942374545:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 113.42/16.29 % (4030748)Instruction limit reached! % 113.42/16.29 % (4030748)------------------------------ % 113.42/16.29 % (4030748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030748)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030748)Termination reason: Instruction limit % 113.42/16.29 % (4030748)Termination phase: Saturation % 113.42/16.29 % (4030748)Time elapsed: 1.440 s % 113.42/16.29 % (4030748)Peak memory usage: 43 MB % 113.42/16.29 % (4030748)Instructions burned: 5131 (million) % 113.42/16.29 % (4030773)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3641671750:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 113.42/16.29 % (4030773)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.42/16.29 % (4030773)Terminated due to inappropriate strategy. % 113.42/16.29 % (4030773)------------------------------ % 113.42/16.29 % (4030773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030773)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030773)Termination reason: Inappropriate % 113.42/16.29 % (4030773)Time elapsed: 0.002 s % 113.42/16.29 % (4030773)Peak memory usage: 11 MB % 113.42/16.29 % (4030773)Instructions burned: 9 (million) % 113.42/16.29 % (4030773)------------------------------ % 113.42/16.29 % (4030773)------------------------------ % 113.42/16.29 % (4030775)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3129073506:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 113.42/16.29 % (4030771)Instruction limit reached! % 113.42/16.29 % (4030771)------------------------------ % 113.42/16.29 % (4030771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030771)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030771)Termination reason: Instruction limit % 113.42/16.29 % (4030771)Termination phase: Saturation % 113.42/16.29 % (4030771)Time elapsed: 1.076 s % 113.42/16.29 % (4030771)Peak memory usage: 17 MB % 113.42/16.29 % (4030771)Instructions burned: 2251 (million) % 113.42/16.29 % (4030778)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1211552975:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 113.42/16.29 % (4030767)Instruction limit reached! % 113.42/16.29 % (4030767)------------------------------ % 113.42/16.29 % (4030767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.42/16.29 % (4030767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.42/16.29 % (4030767)CaDiCaL version: 2.1.3 % 113.42/16.29 % (4030767)Termination reason: Instruction limit % 135.42/19.34 % (4030767)Termination phase: Saturation % 135.42/19.34 % (4030767)Time elapsed: 1.891 s % 135.42/19.34 % (4030767)Peak memory usage: 33 MB % 135.42/19.34 % (4030767)Instructions burned: 3514 (million) % 135.42/19.34 % (4030780)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2294656143:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 135.42/19.34 % (4030775)Instruction limit reached! % 135.42/19.34 % (4030775)------------------------------ % 135.42/19.34 % (4030775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.34 % (4030775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.34 % (4030775)CaDiCaL version: 2.1.3 % 135.42/19.34 % (4030775)Termination reason: Instruction limit % 135.42/19.34 % (4030775)Termination phase: Saturation % 135.42/19.34 % (4030775)Time elapsed: 1.055 s % 135.42/19.34 % (4030775)Peak memory usage: 42 MB % 135.42/19.34 % (4030775)Instructions burned: 4597 (million) % 135.42/19.34 % (4030782)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1218202689:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 135.42/19.34 % (4030782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.42/19.34 % (4030782)Terminated due to inappropriate strategy. % 135.42/19.34 % (4030782)------------------------------ % 135.42/19.34 % (4030782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.34 % (4030782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.34 % (4030782)CaDiCaL version: 2.1.3 % 135.42/19.34 % (4030782)Termination reason: Inappropriate % 135.42/19.34 % (4030782)Time elapsed: 0.006 s % 135.42/19.34 % (4030782)Peak memory usage: 11 MB % 135.42/19.34 % (4030782)Instructions burned: 10 (million) % 135.42/19.34 % (4030782)------------------------------ % 135.42/19.34 % (4030782)------------------------------ % 135.42/19.34 % (4030784)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1506777731:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 135.42/19.34 % (4030784)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.42/19.34 % (4030784)Terminated due to inappropriate strategy. % 135.42/19.34 % (4030784)------------------------------ % 135.42/19.34 % (4030784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.34 % (4030784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.34 % (4030784)CaDiCaL version: 2.1.3 % 135.42/19.34 % (4030784)Termination reason: Inappropriate % 135.42/19.34 % (4030784)Time elapsed: 0.005 s % 135.42/19.34 % (4030784)Peak memory usage: 11 MB % 135.42/19.34 % (4030784)Instructions burned: 9 (million) % 135.42/19.34 % (4030784)------------------------------ % 135.42/19.34 % (4030784)------------------------------ % 135.42/19.34 % (4030786)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2857401396:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 135.42/19.34 % (4030786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.42/19.34 % (4030786)Terminated due to inappropriate strategy. % 135.42/19.34 % (4030786)------------------------------ % 135.42/19.34 % (4030786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.34 % (4030786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.34 % (4030786)CaDiCaL version: 2.1.3 % 135.42/19.34 % (4030786)Termination reason: Inappropriate % 135.42/19.34 % (4030786)Time elapsed: 0.005 s % 135.42/19.34 % (4030786)Peak memory usage: 11 MB % 135.42/19.34 % (4030786)Instructions burned: 9 (million) % 135.42/19.34 % (4030786)------------------------------ % 135.42/19.34 % (4030786)------------------------------ % 135.42/19.34 % (4030788)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3504589996:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 135.42/19.34 % (4030769)Instruction limit reached! % 135.42/19.34 % (4030769)------------------------------ % 135.42/19.34 % (4030769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.34 % (4030769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.34 % (4030769)CaDiCaL version: 2.1.3 % 135.42/19.34 % (4030769)Termination reason: Instruction limit % 135.42/19.34 % (4030769)Termination phase: Saturation % 135.42/19.34 % (4030769)Time elapsed: 2.069 s % 135.42/19.34 % (4030769)Peak memory usage: 33 MB % 135.42/19.34 % (4030769)Instructions burned: 3773 (million) % 135.42/19.34 % (4030790)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2710157868:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 135.42/19.34 % (4030763)Instruction limit reached! % 136.84/19.54 % (4030763)------------------------------ % 136.84/19.54 % (4030763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030763)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030763)Termination reason: Instruction limit % 136.84/19.54 % (4030763)Termination phase: Saturation % 136.84/19.54 % (4030763)Time elapsed: 3.028 s % 136.84/19.54 % (4030763)Peak memory usage: 41 MB % 136.84/19.54 % (4030763)Instructions burned: 5114 (million) % 136.84/19.54 % (4030792)dis+10_16:1_sil=16000:random_seed=3164195087:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 136.84/19.54 % (4030780)Instruction limit reached! % 136.84/19.54 % (4030780)------------------------------ % 136.84/19.54 % (4030780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030780)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030780)Termination reason: Instruction limit % 136.84/19.54 % (4030780)Termination phase: Saturation % 136.84/19.54 % (4030780)Time elapsed: 1.522 s % 136.84/19.54 % (4030780)Peak memory usage: 54 MB % 136.84/19.54 % (4030780)Instructions burned: 5213 (million) % 136.84/19.54 % (4030794)ott-3_8_sil=64000:random_seed=3992528904:i=20139:bs=on_2956 on theBenchmark for (2956ds/20139Mi) % 136.84/19.54 % (4030790)Instruction limit reached! % 136.84/19.54 % (4030790)------------------------------ % 136.84/19.54 % (4030790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030790)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030790)Termination reason: Instruction limit % 136.84/19.54 % (4030790)Termination phase: Saturation % 136.84/19.54 % (4030790)Time elapsed: 4.894 s % 136.84/19.54 % (4030790)Peak memory usage: 86 MB % 136.84/19.54 % (4030790)Instructions burned: 8174 (million) % 136.84/19.54 % (4030796)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2368083313:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 136.84/19.54 % (4030796)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.84/19.54 % (4030796)Terminated due to inappropriate strategy. % 136.84/19.54 % (4030796)------------------------------ % 136.84/19.54 % (4030796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030796)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030796)Termination reason: Inappropriate % 136.84/19.54 % (4030796)Time elapsed: 0.006 s % 136.84/19.54 % (4030796)Peak memory usage: 11 MB % 136.84/19.54 % (4030796)Instructions burned: 11 (million) % 136.84/19.54 % (4030796)------------------------------ % 136.84/19.54 % (4030796)------------------------------ % 136.84/19.54 % (4030798)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2548217427:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 136.84/19.54 % (4030792)Instruction limit reached! % 136.84/19.54 % (4030792)------------------------------ % 136.84/19.54 % (4030792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030792)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030792)Termination reason: Instruction limit % 136.84/19.54 % (4030792)Termination phase: Saturation % 136.84/19.54 % (4030792)Time elapsed: 4.819 s % 136.84/19.54 % (4030792)Peak memory usage: 48 MB % 136.84/19.54 % (4030792)Instructions burned: 9156 (million) % 136.84/19.54 % (4030800)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2459796265:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 136.84/19.54 % (4030794)Instruction limit reached! % 136.84/19.54 % (4030794)------------------------------ % 136.84/19.54 % (4030794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.84/19.54 % (4030794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.84/19.54 % (4030794)CaDiCaL version: 2.1.3 % 136.84/19.54 % (4030794)Termination reason: Instruction limit % 136.84/19.54 % (4030794)Termination phase: Saturation % 136.84/19.54 % (4030794)Time elapsed: 6.791 s % 136.84/19.54 % (4030794)Peak memory usage: 134 MB % 136.84/19.54 % (4030794)Instructions burned: 20139 (million) % 136.84/19.54 % (4030802)dis+33_16_sil=32000:sac=on:random_seed=3417608597:i=15851:nm=0_2888 on theBenchmark for (2888ds/15851Mi) % 136.84/19.54 % (4030798)Instruction limit reached! % 136.84/19.54 % (4030798)------------------------------ % 136.84/19.54 % (4030798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4030798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4030798)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4030798)Termination reason: Instruction limit % 177.15/25.26 % (4030798)Termination phase: Saturation % 177.15/25.26 % (4030798)Time elapsed: 7.814 s % 177.15/25.26 % (4030798)Peak memory usage: 81 MB % 177.15/25.26 % (4030798)Instructions burned: 11404 (million) % 177.15/25.26 % (4031118)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1659429592:avsq=on:i=17627:add=on:amm=off_2839 on theBenchmark for (2839ds/17627Mi) % 177.15/25.26 % (4030802)Instruction limit reached! % 177.15/25.26 % (4030802)------------------------------ % 177.15/25.26 % (4030802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4030802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4030802)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4030802)Termination reason: Instruction limit % 177.15/25.26 % (4030802)Termination phase: Saturation % 177.15/25.26 % (4030802)Time elapsed: 5.544 s % 177.15/25.26 % (4030802)Peak memory usage: 151 MB % 177.15/25.26 % (4030802)Instructions burned: 15851 (million) % 177.15/25.26 % (4031126)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1253229818:s2a=on:i=53295_2832 on theBenchmark for (2832ds/53295Mi) % 177.15/25.26 % (4030788)Instruction limit reached! % 177.15/25.26 % (4030788)------------------------------ % 177.15/25.26 % (4030788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4030788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4030788)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4030788)Termination reason: Instruction limit % 177.15/25.26 % (4030788)Termination phase: Saturation % 177.15/25.26 % (4030788)Time elapsed: 13.957 s % 177.15/25.26 % (4030788)Peak memory usage: 167 MB % 177.15/25.26 % (4030788)Instructions burned: 22565 (million) % 177.15/25.26 % (4031130)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4172865329:i=26857:ins=20_2830 on theBenchmark for (2830ds/26857Mi) % 177.15/25.26 % (4031130)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.15/25.26 % (4031130)Terminated due to inappropriate strategy. % 177.15/25.26 % (4031130)------------------------------ % 177.15/25.26 % (4031130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4031130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4031130)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4031130)Termination reason: Inappropriate % 177.15/25.26 % (4031130)Time elapsed: 0.009 s % 177.15/25.26 % (4031130)Peak memory usage: 11 MB % 177.15/25.26 % (4031130)Instructions burned: 9 (million) % 177.15/25.26 % (4031130)------------------------------ % 177.15/25.26 % (4031130)------------------------------ % 177.15/25.26 % (4031132)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1562805285:i=28120:bs=on:fsr=off_2829 on theBenchmark for (2829ds/28120Mi) % 177.15/25.26 % (4030800)Instruction limit reached! % 177.15/25.26 % (4030800)------------------------------ % 177.15/25.26 % (4030800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4030800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4030800)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4030800)Termination reason: Instruction limit % 177.15/25.26 % (4030800)Termination phase: Saturation % 177.15/25.26 % (4030800)Time elapsed: 10.354 s % 177.15/25.26 % (4030800)Peak memory usage: 85 MB % 177.15/25.26 % (4030800)Instructions burned: 14134 (million) % 177.15/25.26 % (4031140)fmb+10_1_sil=256000:fmbss=7:random_seed=1067850968:fmbsr=1.6:i=182295_2809 on theBenchmark for (2809ds/182295Mi) % 177.15/25.26 % (4031140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.15/25.26 % (4031140)Terminated due to inappropriate strategy. % 177.15/25.26 % (4031140)------------------------------ % 177.15/25.26 % (4031140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.26 % (4031140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.26 % (4031140)CaDiCaL version: 2.1.3 % 177.15/25.26 % (4031140)Termination reason: Inappropriate % 177.15/25.26 % (4031140)Time elapsed: 0.009 s % 177.15/25.26 % (4031140)Peak memory usage: 11 MB % 177.15/25.26 % (4031140)Instructions burned: 9 (million) % 177.15/25.26 % (4031140)------------------------------ % 177.15/25.26 % (4031140)------------------------------ % 177.15/25.26 % (4031142)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1375457542:i=44625:gsp=on_2809 on theBenchmark for (2809ds/44625Mi) % 191.03/27.17 % (4031142)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.03/27.17 % (4031142)Terminated due to inappropriate strategy. % 191.03/27.17 % (4031142)------------------------------ % 191.03/27.17 % (4031142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.03/27.17 % (4031142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.03/27.17 % (4031142)CaDiCaL version: 2.1.3 % 191.03/27.17 % (4031142)Termination reason: Inappropriate % 191.03/27.17 % (4031142)Time elapsed: 0.006 s % 191.03/27.17 % (4031142)Peak memory usage: 11 MB % 191.03/27.17 % (4031142)Instructions burned: 9 (million) % 191.03/27.17 % (4031142)------------------------------ % 191.03/27.17 % (4031142)------------------------------ % 191.03/27.17 % (4031144)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=550655537:i=160505_2808 on theBenchmark for (2808ds/160505Mi) % 191.03/27.17 % (4031144)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.03/27.17 % (4031144)Terminated due to inappropriate strategy. % 191.03/27.17 % (4031144)------------------------------ % 191.03/27.17 % (4031144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.03/27.17 % (4031144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.03/27.17 % (4031144)CaDiCaL version: 2.1.3 % 191.03/27.17 % (4031144)Termination reason: Inappropriate % 191.03/27.17 % (4031144)Time elapsed: 0.011 s % 191.03/27.17 % (4031144)Peak memory usage: 11 MB % 191.03/27.17 % (4031144)Instructions burned: 9 (million) % 191.03/27.17 % (4031144)------------------------------ % 191.03/27.17 % (4031144)------------------------------ % 191.03/27.17 % (4031146)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=150707290:fmbsr=1.3:i=225729_2808 on theBenchmark for (2808ds/225729Mi) % 191.03/27.17 % (4031146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.03/27.17 % (4031146)Terminated due to inappropriate strategy. % 191.03/27.17 % (4031146)------------------------------ % 191.03/27.17 % (4031146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.03/27.17 % (4031146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.03/27.17 % (4031146)CaDiCaL version: 2.1.3 % 191.03/27.17 % (4031146)Termination reason: Inappropriate % 191.03/27.17 % (4031146)Time elapsed: 0.010 s % 191.03/27.17 % (4031146)Peak memory usage: 11 MB % 191.03/27.17 % (4031146)Instructions burned: 9 (million) % 191.03/27.17 % (4031146)------------------------------ % 191.03/27.17 % (4031146)------------------------------ % 191.03/27.17 % (4031148)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2121783262:fmbsr=2:i=185024:ins=7_2807 on theBenchmark for (2807ds/185024Mi) % 191.03/27.17 % (4031148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.03/27.17 % (4031148)Terminated due to inappropriate strategy. % 191.03/27.17 % (4031148)------------------------------ % 191.03/27.17 % (4031148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.03/27.17 % (4031148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.03/27.17 % (4031148)CaDiCaL version: 2.1.3 % 191.03/27.17 % (4031148)Termination reason: Inappropriate % 191.03/27.17 % (4031148)Time elapsed: 0.005 s % 191.03/27.17 % (4031148)Peak memory usage: 11 MB % 191.03/27.17 % (4031148)Instructions burned: 9 (million) % 191.03/27.17 % (4031148)------------------------------ % 191.03/27.17 % (4031148)------------------------------ % 191.03/27.17 % (4031150)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3262477078:rtra=on_2807 on theBenchmark for (2807ds/0Mi) % 191.03/27.17 % (4031150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.03/27.17 % (4031150)Terminated due to inappropriate strategy. % 191.03/27.17 % (4031150)------------------------------ % 191.03/27.17 % (4031150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.03/27.17 % (4031150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.03/27.17 % (4031150)CaDiCaL version: 2.1.3 % 191.03/27.17 % (4031150)Termination reason: Inappropriate % 191.03/27.17 % (4031150)Time elapsed: 0.014 s % 191.03/27.17 % (4031150)Peak memory usage: 11 MB % 191.03/27.17 % (4031150)Instructions burned: 12 (million) % 191.03/27.17 % (4031150)------------------------------ % 191.03/27.17 % (4031150)------------------------------ % 191.03/27.17 % (4031152)% WARNING: option uhcvi not known. % 191.03/27.17 % (4031152)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=322373521:i=271062:add=off:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/271062Mi) % 217.76/30.91 % (4030778)Instruction limit reached! % 217.76/30.91 % (4030778)------------------------------ % 217.76/30.91 % (4030778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4030778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4030778)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4030778)Termination reason: Instruction limit % 217.76/30.91 % (4030778)Termination phase: Saturation % 217.76/30.91 % (4030778)Time elapsed: 18.139 s % 217.76/30.91 % (4030778)Peak memory usage: 688 MB % 217.76/30.91 % (4030778)Instructions burned: 29341 (million) % 217.76/30.91 % (4031230)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1069006665:i=176048:add=on:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/176048Mi) % 217.76/30.91 % (4031118)Instruction limit reached! % 217.76/30.91 % (4031118)------------------------------ % 217.76/30.91 % (4031118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4031118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4031118)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4031118)Termination reason: Instruction limit % 217.76/30.91 % (4031118)Termination phase: Saturation % 217.76/30.91 % (4031118)Time elapsed: 8.155 s % 217.76/30.91 % (4031118)Peak memory usage: 60 MB % 217.76/30.91 % (4031118)Instructions burned: 17628 (million) % 217.76/30.91 % (4031311)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4150011056:i=206:fgj=on:rtra=on_2757 on theBenchmark for (2757ds/206Mi) % 217.76/30.91 % (4031311)Instruction limit reached! % 217.76/30.91 % (4031311)------------------------------ % 217.76/30.91 % (4031311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4031311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4031311)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4031311)Termination reason: Instruction limit % 217.76/30.91 % (4031311)Termination phase: Saturation % 217.76/30.91 % (4031311)Time elapsed: 0.134 s % 217.76/30.91 % (4031311)Peak memory usage: 14 MB % 217.76/30.91 % (4031311)Instructions burned: 207 (million) % 217.76/30.91 % (4031313)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=681098703:i=232:rtra=on_2755 on theBenchmark for (2755ds/232Mi) % 217.76/30.91 % (4031313)Instruction limit reached! % 217.76/30.91 % (4031313)------------------------------ % 217.76/30.91 % (4031313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4031313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4031313)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4031313)Termination reason: Instruction limit % 217.76/30.91 % (4031313)Termination phase: Saturation % 217.76/30.91 % (4031313)Time elapsed: 0.155 s % 217.76/30.91 % (4031313)Peak memory usage: 15 MB % 217.76/30.91 % (4031313)Instructions burned: 232 (million) % 217.76/30.91 % (4031315)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2419623929:i=262:rtra=on_2753 on theBenchmark for (2753ds/262Mi) % 217.76/30.91 % (4031315)Instruction limit reached! % 217.76/30.91 % (4031315)------------------------------ % 217.76/30.91 % (4031315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4031315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4031315)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4031315)Termination reason: Instruction limit % 217.76/30.91 % (4031315)Termination phase: Saturation % 217.76/30.91 % (4031315)Time elapsed: 0.162 s % 217.76/30.91 % (4031315)Peak memory usage: 14 MB % 217.76/30.91 % (4031315)Instructions burned: 263 (million) % 217.76/30.91 % (4031317)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=277014970:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2752 on theBenchmark for (2752ds/318Mi) % 217.76/30.91 % (4031317)Instruction limit reached! % 217.76/30.91 % (4031317)------------------------------ % 217.76/30.91 % (4031317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.76/30.91 % (4031317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.76/30.91 % (4031317)CaDiCaL version: 2.1.3 % 217.76/30.91 % (4031317)Termination reason: Instruction limit % 217.76/30.91 % (4031317)Termination phase: Saturation % 217.76/30.91 % (4031317)Time elapsed: 0.216 s % 217.76/30.91 % (4031317)Peak memory usage: 15 MB % 217.76/30.91 % (4031317)Instructions burned: 319 (million) % 217.76/30.91 % (4031319)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3658606270:i=1428:nm=2:rtra=on_2749 on theBenchmark for (2749ds/1428Mi) % 245.48/34.89 % (4031319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.48/34.89 % (4031319)Terminated due to inappropriate strategy. % 245.48/34.89 % (4031319)------------------------------ % 245.48/34.89 % (4031319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031319)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031319)Termination reason: Inappropriate % 245.48/34.89 % (4031319)Time elapsed: 0.006 s % 245.48/34.89 % (4031319)Peak memory usage: 11 MB % 245.48/34.89 % (4031319)Instructions burned: 10 (million) % 245.48/34.89 % (4031319)------------------------------ % 245.48/34.89 % (4031319)------------------------------ % 245.48/34.89 % (4031321)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3677402513:i=262:bd=preordered:rtra=on:fsd=on_2749 on theBenchmark for (2749ds/262Mi) % 245.48/34.89 % (4031321)Instruction limit reached! % 245.48/34.89 % (4031321)------------------------------ % 245.48/34.89 % (4031321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031321)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031321)Termination reason: Instruction limit % 245.48/34.89 % (4031321)Termination phase: Saturation % 245.48/34.89 % (4031321)Time elapsed: 0.160 s % 245.48/34.89 % (4031321)Peak memory usage: 14 MB % 245.48/34.89 % (4031321)Instructions burned: 262 (million) % 245.48/34.89 % (4031323)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=325358089:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2747 on theBenchmark for (2747ds/1368Mi) % 245.48/34.89 % (4031323)Instruction limit reached! % 245.48/34.89 % (4031323)------------------------------ % 245.48/34.89 % (4031323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031323)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031323)Termination reason: Instruction limit % 245.48/34.89 % (4031323)Termination phase: Saturation % 245.48/34.89 % (4031323)Time elapsed: 0.805 s % 245.48/34.89 % (4031323)Peak memory usage: 23 MB % 245.48/34.89 % (4031323)Instructions burned: 1369 (million) % 245.48/34.89 % (4031325)ott-21_1_sil=16000:si=on:fs=off:random_seed=290931907:i=360:av=off:fsr=off:rtra=on_2739 on theBenchmark for (2739ds/360Mi) % 245.48/34.89 % (4031325)Instruction limit reached! % 245.48/34.89 % (4031325)------------------------------ % 245.48/34.89 % (4031325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031325)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031325)Termination reason: Instruction limit % 245.48/34.89 % (4031325)Termination phase: Saturation % 245.48/34.89 % (4031325)Time elapsed: 0.193 s % 245.48/34.89 % (4031325)Peak memory usage: 15 MB % 245.48/34.89 % (4031325)Instructions burned: 360 (million) % 245.48/34.89 % (4031327)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2732010195:i=954:bd=all:rtra=on_2737 on theBenchmark for (2737ds/954Mi) % 245.48/34.89 % (4031327)Instruction limit reached! % 245.48/34.89 % (4031327)------------------------------ % 245.48/34.89 % (4031327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031327)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031327)Termination reason: Instruction limit % 245.48/34.89 % (4031327)Termination phase: Saturation % 245.48/34.89 % (4031327)Time elapsed: 0.632 s % 245.48/34.89 % (4031327)Peak memory usage: 17 MB % 245.48/34.89 % (4031327)Instructions burned: 955 (million) % 245.48/34.89 % (4031329)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2036047161:fmbsr=1.3:i=1730:ins=25:rtra=on_2730 on theBenchmark for (2730ds/1730Mi) % 245.48/34.89 % (4031329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.48/34.89 % (4031329)Terminated due to inappropriate strategy. % 245.48/34.89 % (4031329)------------------------------ % 245.48/34.89 % (4031329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.48/34.89 % (4031329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.48/34.89 % (4031329)CaDiCaL version: 2.1.3 % 245.48/34.89 % (4031329)Termination reason: InappropTerminated % 300.22/42.54 % Vampire exiting % 300.22/42.54 Terminated %------------------------------------------------------------------------------