%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW598_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 : n007.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:30 PM UTC 2026 % Result : Timeout 300.56s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW598_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.09/0.18 % Computer : n007.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:19:10 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/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.16/1.01 % (2413106)Will run a generic schedule for satisfiability detection. % 4.16/1.01 % (2413114)dis+10_1_sil=32000:sp=arity:random_seed=1772462038:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.16/1.01 % (2413112)% WARNING: option uhcvi not known. % 4.16/1.01 % (2413112)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3708693690:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.16/1.01 % (2413111)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3180690831_2999 on theBenchmark for (2999ds/0Mi) % 4.16/1.01 % (2413113)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1376751452:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.16/1.01 % (2413115)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1010324014:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.16/1.01 % (2413111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.16/1.01 % (2413111)Terminated due to inappropriate strategy. % 4.16/1.01 % (2413111)------------------------------ % 4.16/1.01 % (2413111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.16/1.01 % (2413111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.16/1.01 % (2413111)CaDiCaL version: 2.1.3 % 4.16/1.01 % (2413111)Termination reason: Inappropriate % 4.16/1.01 % (2413111)Time elapsed: 0.003 s % 4.16/1.01 % (2413111)Peak memory usage: 11 MB % 4.16/1.01 % (2413111)Instructions burned: 4 (million) % 4.16/1.01 % (2413111)------------------------------ % 4.16/1.01 % (2413111)------------------------------ % 4.16/1.01 % (2413117)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3354169282:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.16/1.01 % (2413123)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=365041085:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.16/1.01 % (2413116)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3216935065:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.16/1.01 % (2413123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.16/1.01 % (2413123)Terminated due to inappropriate strategy. % 4.16/1.01 % (2413123)------------------------------ % 4.16/1.01 % (2413123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.16/1.01 % (2413123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.16/1.01 % (2413123)CaDiCaL version: 2.1.3 % 4.16/1.01 % (2413123)Termination reason: Inappropriate % 4.16/1.01 % (2413123)Time elapsed: 0.002 s % 4.16/1.01 % (2413123)Peak memory usage: 10 MB % 4.16/1.01 % (2413123)Instructions burned: 3 (million) % 4.16/1.01 % (2413123)------------------------------ % 4.16/1.01 % (2413123)------------------------------ % 4.16/1.01 % (2413114)Instruction limit reached! % 4.16/1.01 % (2413114)------------------------------ % 4.16/1.01 % (2413114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.16/1.01 % (2413114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.16/1.01 % (2413114)CaDiCaL version: 2.1.3 % 4.16/1.01 % (2413114)Termination reason: Instruction limit % 4.16/1.01 % (2413114)Termination phase: Saturation % 4.16/1.01 % (2413114)Time elapsed: 0.036 s % 4.16/1.01 % (2413114)Peak memory usage: 13 MB % 4.16/1.01 % (2413114)Instructions burned: 107 (million) % 4.16/1.01 % (2413128)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=1511423860:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.16/1.01 % (2413127)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2734437376:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.16/1.01 % (2413115)Instruction limit reached! % 4.16/1.01 % (2413115)------------------------------ % 4.16/1.01 % (2413115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.16/1.01 % (2413115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.16/1.01 % (2413115)CaDiCaL version: 2.1.3 % 4.16/1.01 % (2413115)Termination reason: Instruction limit % 4.16/1.01 % (2413115)Termination phase: Saturation % 4.16/1.01 % (2413115)Time elapsed: 0.075 s % 4.16/1.01 % (2413115)Peak memory usage: 13 MB % 4.16/1.01 % (2413115)Instructions burned: 116 (million) % 4.16/1.01 % (2413131)ott-21_1_sil=16000:fs=off:random_seed=645996029:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.25/1.37 % (2413127)Instruction limit reached! % 7.25/1.37 % (2413127)------------------------------ % 7.25/1.37 % (2413127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413127)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413127)Termination reason: Instruction limit % 7.25/1.37 % (2413127)Termination phase: Saturation % 7.25/1.37 % (2413127)Time elapsed: 0.080 s % 7.25/1.37 % (2413127)Peak memory usage: 13 MB % 7.25/1.37 % (2413127)Instructions burned: 131 (million) % 7.25/1.37 % (2413133)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2524800857:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.25/1.37 % (2413117)Instruction limit reached! % 7.25/1.37 % (2413117)------------------------------ % 7.25/1.37 % (2413117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413117)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413117)Termination reason: Instruction limit % 7.25/1.37 % (2413117)Termination phase: Saturation % 7.25/1.37 % (2413117)Time elapsed: 0.129 s % 7.25/1.37 % (2413117)Peak memory usage: 13 MB % 7.25/1.37 % (2413117)Instructions burned: 159 (million) % 7.25/1.37 % (2413135)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=87814225:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.25/1.37 % (2413135)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.25/1.37 % (2413135)Terminated due to inappropriate strategy. % 7.25/1.37 % (2413135)------------------------------ % 7.25/1.37 % (2413135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413135)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413135)Termination reason: Inappropriate % 7.25/1.37 % (2413135)Time elapsed: 0.002 s % 7.25/1.37 % (2413135)Peak memory usage: 10 MB % 7.25/1.37 % (2413135)Instructions burned: 3 (million) % 7.25/1.37 % (2413135)------------------------------ % 7.25/1.37 % (2413135)------------------------------ % 7.25/1.37 % (2413116)Instruction limit reached! % 7.25/1.37 % (2413116)------------------------------ % 7.25/1.37 % (2413116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413116)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413116)Termination reason: Instruction limit % 7.25/1.37 % (2413116)Termination phase: Saturation % 7.25/1.37 % (2413116)Time elapsed: 0.153 s % 7.25/1.37 % (2413116)Peak memory usage: 13 MB % 7.25/1.37 % (2413116)Instructions burned: 131 (million) % 7.25/1.37 % (2413131)Instruction limit reached! % 7.25/1.37 % (2413131)------------------------------ % 7.25/1.37 % (2413131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413131)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413131)Termination reason: Instruction limit % 7.25/1.37 % (2413131)Termination phase: Saturation % 7.25/1.37 % (2413131)Time elapsed: 0.094 s % 7.25/1.37 % (2413131)Peak memory usage: 13 MB % 7.25/1.37 % (2413131)Instructions burned: 182 (million) % 7.25/1.37 % (2413137)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2527331922:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.25/1.37 % (2413138)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4007024307:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.25/1.37 % (2413138)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.25/1.37 % (2413138)Terminated due to inappropriate strategy. % 7.25/1.37 % (2413138)------------------------------ % 7.25/1.37 % (2413138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.37 % (2413138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.37 % (2413138)CaDiCaL version: 2.1.3 % 7.25/1.37 % (2413138)Termination reason: Inappropriate % 7.25/1.37 % (2413138)Time elapsed: 0.002 s % 7.25/1.37 % (2413138)Peak memory usage: 10 MB % 7.25/1.37 % (2413138)Instructions burned: 3 (million) % 7.25/1.37 % (2413138)------------------------------ % 7.25/1.37 % (2413138)------------------------------ % 7.25/1.37 % (2413140)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=2977481858: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) % 21.88/3.44 % (2413142)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4187826907:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.88/3.44 % (2413128)Instruction limit reached! % 21.88/3.44 % (2413128)------------------------------ % 21.88/3.44 % (2413128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.44 % (2413128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.44 % (2413128)CaDiCaL version: 2.1.3 % 21.88/3.44 % (2413128)Termination reason: Instruction limit % 21.88/3.44 % (2413128)Termination phase: Saturation % 21.88/3.44 % (2413128)Time elapsed: 0.206 s % 21.88/3.44 % (2413128)Peak memory usage: 19 MB % 21.88/3.44 % (2413128)Instructions burned: 690 (million) % 21.88/3.44 % (2413145)fmb+10_1_sil=64000:random_seed=3879729384:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.88/3.44 % (2413145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.44 % (2413145)Terminated due to inappropriate strategy. % 21.88/3.44 % (2413145)------------------------------ % 21.88/3.44 % (2413145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.44 % (2413145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.44 % (2413145)CaDiCaL version: 2.1.3 % 21.88/3.44 % (2413145)Termination reason: Inappropriate % 21.88/3.44 % (2413145)Time elapsed: 0.001 s % 21.88/3.44 % (2413145)Peak memory usage: 11 MB % 21.88/3.44 % (2413145)Instructions burned: 4 (million) % 21.88/3.44 % (2413145)------------------------------ % 21.88/3.44 % (2413145)------------------------------ % 21.88/3.44 % (2413147)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2865666320:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.88/3.44 % (2413147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.44 % (2413147)Terminated due to inappropriate strategy. % 21.88/3.44 % (2413147)------------------------------ % 21.88/3.44 % (2413147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.44 % (2413147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.44 % (2413147)CaDiCaL version: 2.1.3 % 21.88/3.44 % (2413147)Termination reason: Inappropriate % 21.88/3.44 % (2413147)Time elapsed: 0.005 s % 21.88/3.44 % (2413147)Peak memory usage: 10 MB % 21.88/3.44 % (2413147)Instructions burned: 3 (million) % 21.88/3.44 % (2413147)------------------------------ % 21.88/3.44 % (2413147)------------------------------ % 21.88/3.44 % (2413149)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2165587741:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.88/3.44 % (2413149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.44 % (2413149)Terminated due to inappropriate strategy. % 21.88/3.44 % (2413149)------------------------------ % 21.88/3.44 % (2413149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.44 % (2413149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.44 % (2413149)CaDiCaL version: 2.1.3 % 21.88/3.44 % (2413149)Termination reason: Inappropriate % 21.88/3.44 % (2413149)Time elapsed: 0.001 s % 21.88/3.44 % (2413149)Peak memory usage: 10 MB % 21.88/3.44 % (2413149)Instructions burned: 3 (million) % 21.88/3.44 % (2413149)------------------------------ % 21.88/3.44 % (2413149)------------------------------ % 21.88/3.44 % (2413151)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1825080140:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.88/3.44 % (2413133)Instruction limit reached! % 21.88/3.44 % (2413133)------------------------------ % 21.88/3.44 % (2413133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.44 % (2413133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.44 % (2413133)CaDiCaL version: 2.1.3 % 21.88/3.44 % (2413133)Termination reason: Instruction limit % 21.88/3.44 % (2413133)Termination phase: Saturation % 21.88/3.44 % (2413133)Time elapsed: 0.311 s % 21.88/3.44 % (2413133)Peak memory usage: 14 MB % 21.88/3.44 % (2413133)Instructions burned: 478 (million) % 21.88/3.44 % (2413153)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1126763567:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.88/3.44 % (2413140)Instruction limit reached! % 21.88/3.44 % (2413140)------------------------------ % 33.89/5.10 % (2413140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413140)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413140)Termination reason: Instruction limit % 33.89/5.10 % (2413140)Termination phase: Saturation % 33.89/5.10 % (2413140)Time elapsed: 0.542 s % 33.89/5.10 % (2413140)Peak memory usage: 18 MB % 33.89/5.10 % (2413140)Instructions burned: 692 (million) % 33.89/5.10 % (2413173)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=133405697:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 33.89/5.10 % (2413173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.89/5.10 % (2413173)Terminated due to inappropriate strategy. % 33.89/5.10 % (2413173)------------------------------ % 33.89/5.10 % (2413173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413173)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413173)Termination reason: Inappropriate % 33.89/5.10 % (2413173)Time elapsed: 0.005 s % 33.89/5.10 % (2413173)Peak memory usage: 10 MB % 33.89/5.10 % (2413173)Instructions burned: 4 (million) % 33.89/5.10 % (2413173)------------------------------ % 33.89/5.10 % (2413173)------------------------------ % 33.89/5.10 % (2413176)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=771708642:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 33.89/5.10 % (2413176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.89/5.10 % (2413176)Terminated due to inappropriate strategy. % 33.89/5.10 % (2413176)------------------------------ % 33.89/5.10 % (2413176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413176)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413176)Termination reason: Inappropriate % 33.89/5.10 % (2413176)Time elapsed: 0.004 s % 33.89/5.10 % (2413176)Peak memory usage: 10 MB % 33.89/5.10 % (2413176)Instructions burned: 3 (million) % 33.89/5.10 % (2413176)------------------------------ % 33.89/5.10 % (2413176)------------------------------ % 33.89/5.10 % (2413179)ott-2_1_sil=16000:newcnf=on:random_seed=3890952877:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 33.89/5.10 % (2413142)Instruction limit reached! % 33.89/5.10 % (2413142)------------------------------ % 33.89/5.10 % (2413142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413142)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413142)Termination reason: Instruction limit % 33.89/5.10 % (2413142)Termination phase: Saturation % 33.89/5.10 % (2413142)Time elapsed: 0.768 s % 33.89/5.10 % (2413142)Peak memory usage: 19 MB % 33.89/5.10 % (2413142)Instructions burned: 879 (million) % 33.89/5.10 % (2413188)ott+10_1_sil=32000:tgt=ground:random_seed=3907180763:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 33.89/5.10 % (2413137)Instruction limit reached! % 33.89/5.10 % (2413137)------------------------------ % 33.89/5.10 % (2413137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413137)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413137)Termination reason: Instruction limit % 33.89/5.10 % (2413137)Termination phase: Saturation % 33.89/5.10 % (2413137)Time elapsed: 0.879 s % 33.89/5.10 % (2413137)Peak memory usage: 20 MB % 33.89/5.10 % (2413137)Instructions burned: 1179 (million) % 33.89/5.10 % (2413192)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=35889538:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 33.89/5.10 % (2413192)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.89/5.10 % (2413192)Terminated due to inappropriate strategy. % 33.89/5.10 % (2413192)------------------------------ % 33.89/5.10 % (2413192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.89/5.10 % (2413192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.89/5.10 % (2413192)CaDiCaL version: 2.1.3 % 33.89/5.10 % (2413192)Termination reason: Inappropriate % 33.89/5.10 % (2413192)Time elapsed: 0.005 s % 33.89/5.10 % (2413192)Peak memory usage: 11 MB % 33.89/5.10 % (2413192)Instructions burned: 4 (million) % 111.06/15.93 % (2413192)------------------------------ % 111.06/15.93 % (2413192)------------------------------ % 111.06/15.93 % (2413196)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2413379131:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 111.06/15.93 % (2413179)Instruction limit reached! % 111.06/15.93 % (2413179)------------------------------ % 111.06/15.93 % (2413179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413179)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413179)Termination reason: Instruction limit % 111.06/15.93 % (2413179)Termination phase: Saturation % 111.06/15.93 % (2413179)Time elapsed: 0.730 s % 111.06/15.93 % (2413179)Peak memory usage: 19 MB % 111.06/15.93 % (2413179)Instructions burned: 870 (million) % 111.06/15.93 % (2413223)dis+21_1_sil=32000:sas=cadical:random_seed=787977261:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 111.06/15.93 % (2413153)Instruction limit reached! % 111.06/15.93 % (2413153)------------------------------ % 111.06/15.93 % (2413153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413153)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413153)Termination reason: Instruction limit % 111.06/15.93 % (2413153)Termination phase: Saturation % 111.06/15.93 % (2413153)Time elapsed: 1.314 s % 111.06/15.93 % (2413153)Peak memory usage: 27 MB % 111.06/15.93 % (2413153)Instructions burned: 1472 (million) % 111.06/15.93 % (2413232)ott+11_1_sil=16000:gs=on:random_seed=406066661:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 111.06/15.93 % (2413151)Instruction limit reached! % 111.06/15.93 % (2413151)------------------------------ % 111.06/15.93 % (2413151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413151)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413151)Termination reason: Instruction limit % 111.06/15.93 % (2413151)Termination phase: Saturation % 111.06/15.93 % (2413151)Time elapsed: 2.449 s % 111.06/15.93 % (2413151)Peak memory usage: 31 MB % 111.06/15.93 % (2413151)Instructions burned: 5131 (million) % 111.06/15.93 % (2413256)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2180406171:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 111.06/15.93 % (2413256)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.06/15.93 % (2413256)Terminated due to inappropriate strategy. % 111.06/15.93 % (2413256)------------------------------ % 111.06/15.93 % (2413256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413256)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413256)Termination reason: Inappropriate % 111.06/15.93 % (2413256)Time elapsed: 0.002 s % 111.06/15.93 % (2413256)Peak memory usage: 10 MB % 111.06/15.93 % (2413256)Instructions burned: 3 (million) % 111.06/15.93 % (2413256)------------------------------ % 111.06/15.93 % (2413256)------------------------------ % 111.06/15.93 % (2413258)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1700540386:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 111.06/15.93 % (2413223)Instruction limit reached! % 111.06/15.93 % (2413223)------------------------------ % 111.06/15.93 % (2413223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413223)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413223)Termination reason: Instruction limit % 111.06/15.93 % (2413223)Termination phase: Saturation % 111.06/15.93 % (2413223)Time elapsed: 1.347 s % 111.06/15.93 % (2413223)Peak memory usage: 32 MB % 111.06/15.93 % (2413223)Instructions burned: 3775 (million) % 111.06/15.93 % (2413334)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4265303438:i=29340_2969 on theBenchmark for (2969ds/29340Mi) % 111.06/15.93 % (2413232)Instruction limit reached! % 111.06/15.93 % (2413232)------------------------------ % 111.06/15.93 % (2413232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.06/15.93 % (2413232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.06/15.93 % (2413232)CaDiCaL version: 2.1.3 % 111.06/15.93 % (2413232)Termination reason: Instruction limit % 119.11/17.06 % (2413232)Termination phase: Saturation % 119.11/17.06 % (2413232)Time elapsed: 1.356 s % 119.11/17.06 % (2413232)Peak memory usage: 16 MB % 119.11/17.06 % (2413232)Instructions burned: 2251 (million) % 119.11/17.06 % (2413367)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3233234002:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 119.11/17.06 % (2413196)Instruction limit reached! % 119.11/17.06 % (2413196)------------------------------ % 119.11/17.06 % (2413196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.11/17.06 % (2413196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.11/17.06 % (2413196)CaDiCaL version: 2.1.3 % 119.11/17.06 % (2413196)Termination reason: Instruction limit % 119.11/17.06 % (2413196)Termination phase: Saturation % 119.11/17.06 % (2413196)Time elapsed: 2.298 s % 119.11/17.06 % (2413196)Peak memory usage: 30 MB % 119.11/17.06 % (2413196)Instructions burned: 3513 (million) % 119.11/17.06 % (2413416)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3038252349:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi) % 119.11/17.06 % (2413416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.11/17.06 % (2413416)Terminated due to inappropriate strategy. % 119.11/17.06 % (2413416)------------------------------ % 119.11/17.06 % (2413416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.11/17.06 % (2413416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.11/17.06 % (2413416)CaDiCaL version: 2.1.3 % 119.11/17.06 % (2413416)Termination reason: Inappropriate % 119.11/17.06 % (2413416)Time elapsed: 0.003 s % 119.11/17.06 % (2413416)Peak memory usage: 11 MB % 119.11/17.06 % (2413416)Instructions burned: 4 (million) % 119.11/17.06 % (2413416)------------------------------ % 119.11/17.06 % (2413416)------------------------------ % 119.11/17.06 % (2413418)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1131234858:fmbsr=2:i=46332_2964 on theBenchmark for (2964ds/46332Mi) % 119.11/17.06 % (2413418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.11/17.06 % (2413418)Terminated due to inappropriate strategy. % 119.11/17.06 % (2413418)------------------------------ % 119.11/17.06 % (2413418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.11/17.06 % (2413418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.11/17.06 % (2413418)CaDiCaL version: 2.1.3 % 119.11/17.06 % (2413418)Termination reason: Inappropriate % 119.11/17.06 % (2413418)Time elapsed: 0.002 s % 119.11/17.06 % (2413418)Peak memory usage: 10 MB % 119.11/17.06 % (2413418)Instructions burned: 3 (million) % 119.11/17.06 % (2413418)------------------------------ % 119.11/17.06 % (2413418)------------------------------ % 119.11/17.06 % (2413420)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1446316723:i=14071_2964 on theBenchmark for (2964ds/14071Mi) % 119.11/17.06 % (2413420)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.11/17.06 % (2413420)Terminated due to inappropriate strategy. % 119.11/17.06 % (2413420)------------------------------ % 119.11/17.06 % (2413420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.11/17.06 % (2413420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.11/17.06 % (2413420)CaDiCaL version: 2.1.3 % 119.11/17.06 % (2413420)Termination reason: Inappropriate % 119.11/17.06 % (2413420)Time elapsed: 0.002 s % 119.11/17.06 % (2413420)Peak memory usage: 10 MB % 119.11/17.06 % (2413420)Instructions burned: 3 (million) % 119.11/17.06 % (2413420)------------------------------ % 119.11/17.06 % (2413420)------------------------------ % 119.11/17.06 % (2413422)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3835336669:i=22565:add=on:rawr=on_2964 on theBenchmark for (2964ds/22565Mi) % 119.11/17.06 % (2413188)Instruction limit reached! % 119.11/17.06 % (2413188)------------------------------ % 119.11/17.06 % (2413188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.11/17.06 % (2413188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.11/17.06 % (2413188)CaDiCaL version: 2.1.3 % 119.11/17.06 % (2413188)Termination reason: Instruction limit % 119.11/17.06 % (2413188)Termination phase: Saturation % 119.11/17.06 % (2413188)Time elapsed: 3.530 s % 119.11/17.06 % (2413188)Peak memory usage: 39 MB % 119.11/17.06 % (2413188)Instructions burned: 5115 (million) % 119.11/17.06 % (2413424)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2631876104:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 119.11/17.06 % (2413258)Instruction limit reached! % 119.74/17.17 % (2413258)------------------------------ % 119.74/17.17 % (2413258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413258)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413258)Termination reason: Instruction limit % 119.74/17.17 % (2413258)Termination phase: Saturation % 119.74/17.17 % (2413258)Time elapsed: 2.020 s % 119.74/17.17 % (2413258)Peak memory usage: 37 MB % 119.74/17.17 % (2413258)Instructions burned: 4592 (million) % 119.74/17.17 % (2413426)dis+10_16:1_sil=16000:random_seed=1054364939:i=9155:fsr=off_2951 on theBenchmark for (2951ds/9155Mi) % 119.74/17.17 % (2413367)Instruction limit reached! % 119.74/17.17 % (2413367)------------------------------ % 119.74/17.17 % (2413367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413367)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413367)Termination reason: Instruction limit % 119.74/17.17 % (2413367)Termination phase: Saturation % 119.74/17.17 % (2413367)Time elapsed: 2.691 s % 119.74/17.17 % (2413367)Peak memory usage: 49 MB % 119.74/17.17 % (2413367)Instructions burned: 5214 (million) % 119.74/17.17 % (2413428)ott-3_8_sil=64000:random_seed=3349106094:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 119.74/17.17 % (2413424)Instruction limit reached! % 119.74/17.17 % (2413424)------------------------------ % 119.74/17.17 % (2413424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413424)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413424)Termination reason: Instruction limit % 119.74/17.17 % (2413424)Termination phase: Saturation % 119.74/17.17 % (2413424)Time elapsed: 4.824 s % 119.74/17.17 % (2413424)Peak memory usage: 55 MB % 119.74/17.17 % (2413424)Instructions burned: 8174 (million) % 119.74/17.17 % (2413430)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3720691796:fmbsr=2:i=32576_2905 on theBenchmark for (2905ds/32576Mi) % 119.74/17.17 % (2413430)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.74/17.17 % (2413430)Terminated due to inappropriate strategy. % 119.74/17.17 % (2413430)------------------------------ % 119.74/17.17 % (2413430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413430)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413430)Termination reason: Inappropriate % 119.74/17.17 % (2413430)Time elapsed: 0.003 s % 119.74/17.17 % (2413430)Peak memory usage: 11 MB % 119.74/17.17 % (2413430)Instructions burned: 4 (million) % 119.74/17.17 % (2413430)------------------------------ % 119.74/17.17 % (2413430)------------------------------ % 119.74/17.17 % (2413432)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1895947497:i=11404_2905 on theBenchmark for (2905ds/11404Mi) % 119.74/17.17 % (2413426)Instruction limit reached! % 119.74/17.17 % (2413426)------------------------------ % 119.74/17.17 % (2413426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413426)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413426)Termination reason: Instruction limit % 119.74/17.17 % (2413426)Termination phase: Saturation % 119.74/17.17 % (2413426)Time elapsed: 4.777 s % 119.74/17.17 % (2413426)Peak memory usage: 52 MB % 119.74/17.17 % (2413426)Instructions burned: 9157 (million) % 119.74/17.17 % (2413434)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=186740957:i=14134_2903 on theBenchmark for (2903ds/14134Mi) % 119.74/17.17 % (2413334)Instruction limit reached! % 119.74/17.17 % (2413334)------------------------------ % 119.74/17.17 % (2413334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.74/17.17 % (2413334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.74/17.17 % (2413334)CaDiCaL version: 2.1.3 % 119.74/17.17 % (2413334)Termination reason: Instruction limit % 119.74/17.17 % (2413334)Termination phase: Saturation % 119.74/17.17 % (2413334)Time elapsed: 8.048 s % 119.74/17.17 % (2413334)Peak memory usage: 173 MB % 119.74/17.17 % (2413334)Instructions burned: 29342 (million) % 119.74/17.17 % (2413436)dis+33_16_sil=32000:sac=on:random_seed=4135128296:i=15851:nm=0_2888 on theBenchmark for (2888ds/15851Mi) % 119.74/17.17 % (2413436)Instruction limit reached! % 119.74/17.17 % (2413436)------------------------------ % 119.74/17.17 % (2413436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413436)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413436)Termination reason: Instruction limit % 153.59/21.95 % (2413436)Termination phase: Saturation % 153.59/21.95 % (2413436)Time elapsed: 4.580 s % 153.59/21.95 % (2413436)Peak memory usage: 167 MB % 153.59/21.95 % (2413436)Instructions burned: 15853 (million) % 153.59/21.95 % (2413501)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3766408880:avsq=on:i=17627:add=on:amm=off_2842 on theBenchmark for (2842ds/17627Mi) % 153.59/21.95 % (2413422)Instruction limit reached! % 153.59/21.95 % (2413422)------------------------------ % 153.59/21.95 % (2413422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413422)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413422)Termination reason: Instruction limit % 153.59/21.95 % (2413422)Termination phase: Saturation % 153.59/21.95 % (2413422)Time elapsed: 13.122 s % 153.59/21.95 % (2413422)Peak memory usage: 694 MB % 153.59/21.95 % (2413422)Instructions burned: 22565 (million) % 153.59/21.95 % (2413428)Instruction limit reached! % 153.59/21.95 % (2413428)------------------------------ % 153.59/21.95 % (2413428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413428)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413428)Termination reason: Instruction limit % 153.59/21.95 % (2413428)Termination phase: Saturation % 153.59/21.95 % (2413428)Time elapsed: 10.758 s % 153.59/21.95 % (2413428)Peak memory usage: 96 MB % 153.59/21.95 % (2413428)Instructions burned: 20139 (million) % 153.59/21.95 % (2413503)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4024435066:s2a=on:i=53295_2832 on theBenchmark for (2832ds/53295Mi) % 153.59/21.95 % (2413432)Instruction limit reached! % 153.59/21.95 % (2413432)------------------------------ % 153.59/21.95 % (2413432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413432)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413432)Termination reason: Instruction limit % 153.59/21.95 % (2413432)Termination phase: Saturation % 153.59/21.95 % (2413432)Time elapsed: 7.267 s % 153.59/21.95 % (2413432)Peak memory usage: 65 MB % 153.59/21.95 % (2413432)Instructions burned: 11405 (million) % 153.59/21.95 % (2413505)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1541209791:i=26857:ins=20_2832 on theBenchmark for (2832ds/26857Mi) % 153.59/21.95 % (2413505)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.59/21.95 % (2413505)Terminated due to inappropriate strategy. % 153.59/21.95 % (2413505)------------------------------ % 153.59/21.95 % (2413505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413505)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413505)Termination reason: Inappropriate % 153.59/21.95 % (2413505)Time elapsed: 0.002 s % 153.59/21.95 % (2413505)Peak memory usage: 10 MB % 153.59/21.95 % (2413505)Instructions burned: 3 (million) % 153.59/21.95 % (2413505)------------------------------ % 153.59/21.95 % (2413505)------------------------------ % 153.59/21.95 % (2413506)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3500909315:i=28120:bs=on:fsr=off_2832 on theBenchmark for (2832ds/28120Mi) % 153.59/21.95 % (2413508)fmb+10_1_sil=256000:fmbss=7:random_seed=741769500:fmbsr=1.6:i=182295_2832 on theBenchmark for (2832ds/182295Mi) % 153.59/21.95 % (2413508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.59/21.95 % (2413508)Terminated due to inappropriate strategy. % 153.59/21.95 % (2413508)------------------------------ % 153.59/21.95 % (2413508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.59/21.95 % (2413508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.59/21.95 % (2413508)CaDiCaL version: 2.1.3 % 153.59/21.95 % (2413508)Termination reason: Inappropriate % 153.59/21.95 % (2413508)Time elapsed: 0.002 s % 153.59/21.95 % (2413508)Peak memory usage: 11 MB % 153.59/21.95 % (2413508)Instructions burned: 3 (million) % 153.59/21.95 % (2413508)------------------------------ % 153.59/21.95 % (2413508)------------------------------ % 153.59/21.95 % (2413511)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1710250903:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 160.45/22.95 % (2413511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.45/22.95 % (2413511)Terminated due to inappropriate strategy. % 160.45/22.95 % (2413511)------------------------------ % 160.45/22.95 % (2413511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.45/22.95 % (2413511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.45/22.95 % (2413511)CaDiCaL version: 2.1.3 % 160.45/22.95 % (2413511)Termination reason: Inappropriate % 160.45/22.95 % (2413511)Time elapsed: 0.004 s % 160.45/22.95 % (2413511)Peak memory usage: 11 MB % 160.45/22.95 % (2413511)Instructions burned: 8 (million) % 160.45/22.95 % (2413511)------------------------------ % 160.45/22.95 % (2413511)------------------------------ % 160.45/22.95 % (2413513)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2269650260:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 160.45/22.95 % (2413513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.45/22.95 % (2413513)Terminated due to inappropriate strategy. % 160.45/22.95 % (2413513)------------------------------ % 160.45/22.95 % (2413513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.45/22.95 % (2413513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.45/22.95 % (2413513)CaDiCaL version: 2.1.3 % 160.45/22.95 % (2413513)Termination reason: Inappropriate % 160.45/22.95 % (2413513)Time elapsed: 0.002 s % 160.45/22.95 % (2413513)Peak memory usage: 10 MB % 160.45/22.95 % (2413513)Instructions burned: 3 (million) % 160.45/22.95 % (2413513)------------------------------ % 160.45/22.95 % (2413513)------------------------------ % 160.45/22.95 % (2413515)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3730479458:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 160.45/22.95 % (2413515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.45/22.95 % (2413515)Terminated due to inappropriate strategy. % 160.45/22.95 % (2413515)------------------------------ % 160.45/22.95 % (2413515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.45/22.95 % (2413515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.45/22.95 % (2413515)CaDiCaL version: 2.1.3 % 160.45/22.95 % (2413515)Termination reason: Inappropriate % 160.45/22.95 % (2413515)Time elapsed: 0.002 s % 160.45/22.95 % (2413515)Peak memory usage: 10 MB % 160.45/22.95 % (2413515)Instructions burned: 3 (million) % 160.45/22.95 % (2413515)------------------------------ % 160.45/22.95 % (2413515)------------------------------ % 160.45/22.95 % (2413517)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=691161905:fmbsr=2:i=185024:ins=7_2831 on theBenchmark for (2831ds/185024Mi) % 160.45/22.95 % (2413517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.45/22.95 % (2413517)Terminated due to inappropriate strategy. % 160.45/22.95 % (2413517)------------------------------ % 160.45/22.95 % (2413517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.45/22.95 % (2413517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.45/22.95 % (2413517)CaDiCaL version: 2.1.3 % 160.45/22.95 % (2413517)Termination reason: Inappropriate % 160.45/22.95 % (2413517)Time elapsed: 0.002 s % 160.45/22.95 % (2413517)Peak memory usage: 10 MB % 160.45/22.95 % (2413517)Instructions burned: 3 (million) % 160.45/22.95 % (2413517)------------------------------ % 160.45/22.95 % (2413517)------------------------------ % 160.45/22.95 % (2413519)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3006430956:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 160.45/22.95 % (2413519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.45/22.95 % (2413519)Terminated due to inappropriate strategy. % 160.45/22.95 % (2413519)------------------------------ % 160.45/22.95 % (2413519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.45/22.95 % (2413519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.45/22.95 % (2413519)CaDiCaL version: 2.1.3 % 160.45/22.95 % (2413519)Termination reason: Inappropriate % 160.45/22.95 % (2413519)Time elapsed: 0.003 s % 160.45/22.95 % (2413519)Peak memory usage: 11 MB % 160.45/22.95 % (2413519)Instructions burned: 5 (million) % 160.45/22.95 % (2413519)------------------------------ % 160.45/22.95 % (2413519)------------------------------ % 160.45/22.95 % (2413521)% WARNING: option uhcvi not known. % 160.45/22.95 % (2413521)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1964947707:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 173.71/24.85 % (2413434)Instruction limit reached! % 173.71/24.85 % (2413434)------------------------------ % 173.71/24.85 % (2413434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413434)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413434)Termination reason: Instruction limit % 173.71/24.85 % (2413434)Termination phase: Saturation % 173.71/24.85 % (2413434)Time elapsed: 9.126 s % 173.71/24.85 % (2413434)Peak memory usage: 79 MB % 173.71/24.85 % (2413434)Instructions burned: 14135 (million) % 173.71/24.85 % (2413524)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1433488246:i=176048:add=on:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/176048Mi) % 173.71/24.85 % (2413501)Instruction limit reached! % 173.71/24.85 % (2413501)------------------------------ % 173.71/24.85 % (2413501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413501)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413501)Termination reason: Instruction limit % 173.71/24.85 % (2413501)Termination phase: Saturation % 173.71/24.85 % (2413501)Time elapsed: 5.576 s % 173.71/24.85 % (2413501)Peak memory usage: 271 MB % 173.71/24.85 % (2413501)Instructions burned: 17629 (million) % 173.71/24.85 % (2413526)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2126358506:i=206:fgj=on:rtra=on_2786 on theBenchmark for (2786ds/206Mi) % 173.71/24.85 % (2413526)Instruction limit reached! % 173.71/24.85 % (2413526)------------------------------ % 173.71/24.85 % (2413526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413526)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413526)Termination reason: Instruction limit % 173.71/24.85 % (2413526)Termination phase: Saturation % 173.71/24.85 % (2413526)Time elapsed: 0.069 s % 173.71/24.85 % (2413526)Peak memory usage: 13 MB % 173.71/24.85 % (2413526)Instructions burned: 207 (million) % 173.71/24.85 % (2413528)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4216833841:i=232:rtra=on_2785 on theBenchmark for (2785ds/232Mi) % 173.71/24.85 % (2413528)Instruction limit reached! % 173.71/24.85 % (2413528)------------------------------ % 173.71/24.85 % (2413528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413528)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413528)Termination reason: Instruction limit % 173.71/24.85 % (2413528)Termination phase: Saturation % 173.71/24.85 % (2413528)Time elapsed: 0.080 s % 173.71/24.85 % (2413528)Peak memory usage: 14 MB % 173.71/24.85 % (2413528)Instructions burned: 235 (million) % 173.71/24.85 % (2413530)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2238304595:i=262:rtra=on_2784 on theBenchmark for (2784ds/262Mi) % 173.71/24.85 % (2413530)Instruction limit reached! % 173.71/24.85 % (2413530)------------------------------ % 173.71/24.85 % (2413530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413530)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413530)Termination reason: Instruction limit % 173.71/24.85 % (2413530)Termination phase: Saturation % 173.71/24.85 % (2413530)Time elapsed: 0.079 s % 173.71/24.85 % (2413530)Peak memory usage: 13 MB % 173.71/24.85 % (2413530)Instructions burned: 265 (million) % 173.71/24.85 % (2413532)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=173547541:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2784 on theBenchmark for (2784ds/318Mi) % 173.71/24.85 % (2413532)Instruction limit reached! % 173.71/24.85 % (2413532)------------------------------ % 173.71/24.85 % (2413532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.71/24.85 % (2413532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.71/24.85 % (2413532)CaDiCaL version: 2.1.3 % 173.71/24.85 % (2413532)Termination reason: Instruction limit % 173.71/24.85 % (2413532)Termination phase: Saturation % 173.71/24.85 % (2413532)Time elapsed: 0.113 s % 173.71/24.85 % (2413532)Peak memory usage: 15 MB % 173.71/24.85 % (2413532)Instructions burned: 319 (million) % 173.71/24.85 % (2413534)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1446091798:i=1428:nm=2:rtra=on_2782 on theBenchmark for (2782ds/1428Mi) % 202.45/28.96 % (2413534)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.45/28.96 % (2413534)Terminated due to inappropriate strategy. % 202.45/28.96 % (2413534)------------------------------ % 202.45/28.96 % (2413534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413534)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413534)Termination reason: Inappropriate % 202.45/28.96 % (2413534)Time elapsed: 0.001 s % 202.45/28.96 % (2413534)Peak memory usage: 10 MB % 202.45/28.96 % (2413534)Instructions burned: 4 (million) % 202.45/28.96 % (2413534)------------------------------ % 202.45/28.96 % (2413534)------------------------------ % 202.45/28.96 % (2413536)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1170138147:i=262:bd=preordered:rtra=on:fsd=on_2782 on theBenchmark for (2782ds/262Mi) % 202.45/28.96 % (2413536)Instruction limit reached! % 202.45/28.96 % (2413536)------------------------------ % 202.45/28.96 % (2413536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413536)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413536)Termination reason: Instruction limit % 202.45/28.96 % (2413536)Termination phase: Saturation % 202.45/28.96 % (2413536)Time elapsed: 0.089 s % 202.45/28.96 % (2413536)Peak memory usage: 14 MB % 202.45/28.96 % (2413536)Instructions burned: 263 (million) % 202.45/28.96 % (2413538)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=2570633218:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/1368Mi) % 202.45/28.96 % (2413538)Instruction limit reached! % 202.45/28.96 % (2413538)------------------------------ % 202.45/28.96 % (2413538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413538)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413538)Termination reason: Instruction limit % 202.45/28.96 % (2413538)Termination phase: Saturation % 202.45/28.96 % (2413538)Time elapsed: 0.417 s % 202.45/28.96 % (2413538)Peak memory usage: 31 MB % 202.45/28.96 % (2413538)Instructions burned: 1370 (million) % 202.45/28.96 % (2413540)ott-21_1_sil=16000:si=on:fs=off:random_seed=3842878212:i=360:av=off:fsr=off:rtra=on_2777 on theBenchmark for (2777ds/360Mi) % 202.45/28.96 % (2413540)Instruction limit reached! % 202.45/28.96 % (2413540)------------------------------ % 202.45/28.96 % (2413540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413540)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413540)Termination reason: Instruction limit % 202.45/28.96 % (2413540)Termination phase: Saturation % 202.45/28.96 % (2413540)Time elapsed: 0.093 s % 202.45/28.96 % (2413540)Peak memory usage: 13 MB % 202.45/28.96 % (2413540)Instructions burned: 361 (million) % 202.45/28.96 % (2413542)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3636877179:i=954:bd=all:rtra=on_2776 on theBenchmark for (2776ds/954Mi) % 202.45/28.96 % (2413542)Instruction limit reached! % 202.45/28.96 % (2413542)------------------------------ % 202.45/28.96 % (2413542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413542)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413542)Termination reason: Instruction limit % 202.45/28.96 % (2413542)Termination phase: Saturation % 202.45/28.96 % (2413542)Time elapsed: 0.344 s % 202.45/28.96 % (2413542)Peak memory usage: 16 MB % 202.45/28.96 % (2413542)Instructions burned: 954 (million) % 202.45/28.96 % (2413544)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3253685581:fmbsr=1.3:i=1730:ins=25:rtra=on_2772 on theBenchmark for (2772ds/1730Mi) % 202.45/28.96 % (2413544)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.45/28.96 % (2413544)Terminated due to inappropriate strategy. % 202.45/28.96 % (2413544)------------------------------ % 202.45/28.96 % (2413544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.45/28.96 % (2413544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.45/28.96 % (2413544)CaDiCaL version: 2.1.3 % 202.45/28.96 % (2413544)Termination reason: Inappropriate % 202.45/28.96 % (2413544)Time elapsed: 0.001 s % 252.35/35.80 % (2413544)Peak memory usage: 10 MB % 252.35/35.80 % (2413544)Instructions burned: 3 (million) % 252.35/35.80 % (2413544)------------------------------ % 252.35/35.80 % (2413544)------------------------------ % 252.35/35.80 % (2413546)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2096651021:i=2358:rtra=on_2772 on theBenchmark for (2772ds/2358Mi) % 252.35/35.80 % (2413546)Instruction limit reached! % 252.35/35.80 % (2413546)------------------------------ % 252.35/35.80 % (2413546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.35/35.80 % (2413546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.35/35.80 % (2413546)CaDiCaL version: 2.1.3 % 252.35/35.80 % (2413546)Termination reason: Instruction limit % 252.35/35.80 % (2413546)Termination phase: Saturation % 252.35/35.80 % (2413546)Time elapsed: 0.811 s % 252.35/35.80 % (2413546)Peak memory usage: 26 MB % 252.35/35.80 % (2413546)Instructions burned: 2359 (million) % 252.35/35.80 % (2413548)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1287807272:i=1778:ins=1:rtra=on_2764 on theBenchmark for (2764ds/1778Mi) % 252.35/35.80 % (2413548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.35/35.80 % (2413548)Terminated due to inappropriate strategy. % 252.35/35.80 % (2413548)------------------------------ % 252.35/35.80 % (2413548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.35/35.80 % (2413548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.35/35.80 % (2413548)CaDiCaL version: 2.1.3 % 252.35/35.80 % (2413548)Termination reason: Inappropriate % 252.35/35.80 % (2413548)Time elapsed: 0.001 s % 252.35/35.80 % (2413548)Peak memory usage: 10 MB % 252.35/35.80 % (2413548)Instructions burned: 4 (million) % 252.35/35.80 % (2413548)------------------------------ % 252.35/35.80 % (2413548)------------------------------ % 252.35/35.80 % (2413550)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=861141488: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) % 252.35/35.80 % (2413550)Instruction limit reached! % 252.35/35.80 % (2413550)------------------------------ % 252.35/35.80 % (2413550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.35/35.80 % (2413550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.35/35.80 % (2413550)CaDiCaL version: 2.1.3 % 252.35/35.80 % (2413550)Termination reason: Instruction limit % 252.35/35.80 % (2413550)Termination phase: Saturation % 252.35/35.80 % (2413550)Time elapsed: 0.468 s % 252.35/35.80 % (2413550)Peak memory usage: 24 MB % 252.35/35.80 % (2413550)Instructions burned: 1387 (million) % 252.35/35.80 % (2413552)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3065703887:i=1758:kws=inv_precedence:fsr=off:rtra=on_2759 on theBenchmark for (2759ds/1758Mi) % 252.35/35.80 % (2413552)Instruction limit reached! % 252.35/35.80 % (2413552)------------------------------ % 252.35/35.80 % (2413552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.35/35.80 % (2413552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.35/35.80 % (2413552)CaDiCaL version: 2.1.3 % 252.35/35.80 % (2413552)Termination reason: Instruction limit % 252.35/35.80 % (2413552)Termination phase: Saturation % 252.35/35.80 % (2413552)Time elapsed: 0.540 s % 252.35/35.80 % (2413552)Peak memory usage: 27 MB % 252.35/35.80 % (2413552)Instructions burned: 1758 (million) % 252.35/35.80 % (2413554)fmb+10_1_sil=64000:si=on:random_seed=4000103455:i=44122:nm=2:rtra=on:gsp=on_2753 on theBenchmark for (2753ds/44122Mi) % 252.35/35.80 % (2413554)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.35/35.80 % (2413554)Terminated due to inappropriate strategy. % 252.35/35.80 % (2413554)------------------------------ % 252.35/35.80 % (2413554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.35/35.80 % (2413554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.35/35.80 % (2413554)CaDiCaL version: 2.1.3 % 252.35/35.80 % (2413554)Termination reason: Inappropriate % 252.35/35.80 % (2413554)Time elapsed: 0.001 s % 252.35/35.80 % (2413554)Peak memory usage: 10 MB % 252.35/35.80 % (2413554)Instructions burned: 4 (million) % 252.35/35.80 % (2413554)------------------------------ % 252.35/35.80 % (2413554)------------------------------ % 252.35/35.80 % (2413556)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3859962053:i=19030:nm=5:rtra=on_2753 on theBenchmark for (2753ds/19030Mi) % 284.90/40.48 % (2413556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.90/40.48 % (2413556)Terminated due to inappropriate strategy. % 284.90/40.48 % (2413556)------------------------------ % 284.90/40.48 % (2413556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.48 % (2413556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.48 % (2413556)CaDiCaL version: 2.1.3 % 284.90/40.48 % (2413556)Termination reason: Inappropriate % 284.90/40.48 % (2413556)Time elapsed: 0.001 s % 284.90/40.48 % (2413556)Peak memory usage: 10 MB % 284.90/40.48 % (2413556)Instructions burned: 4 (million) % 284.90/40.48 % (2413556)------------------------------ % 284.90/40.48 % (2413556)------------------------------ % 284.90/40.48 % (2413558)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3270798251:fmbsr=1.7:i=1840:rtra=on_2753 on theBenchmark for (2753ds/1840Mi) % 284.90/40.48 % (2413558)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.90/40.48 % (2413558)Terminated due to inappropriate strategy. % 284.90/40.48 % (2413558)------------------------------ % 284.90/40.48 % (2413558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.48 % (2413558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.48 % (2413558)CaDiCaL version: 2.1.3 % 284.90/40.48 % (2413558)Termination reason: Inappropriate % 284.90/40.48 % (2413558)Time elapsed: 0.001 s % 284.90/40.48 % (2413558)Peak memory usage: 10 MB % 284.90/40.48 % (2413558)Instructions burned: 4 (million) % 284.90/40.48 % (2413558)------------------------------ % 284.90/40.48 % (2413558)------------------------------ % 284.90/40.48 % (2413560)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2892815660:i=10262:rtra=on_2753 on theBenchmark for (2753ds/10262Mi) % 284.90/40.48 % (2413560)Instruction limit reached! % 284.90/40.48 % (2413560)------------------------------ % 284.90/40.48 % (2413560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.48 % (2413560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.48 % (2413560)CaDiCaL version: 2.1.3 % 284.90/40.48 % (2413560)Termination reason: Instruction limit % 284.90/40.48 % (2413560)Termination phase: Saturation % 284.90/40.48 % (2413560)Time elapsed: 3.124 s % 284.90/40.48 % (2413560)Peak memory usage: 54 MB % 284.90/40.48 % (2413560)Instructions burned: 10263 (million) % 284.90/40.48 % (2413562)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4006022818:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2722 on theBenchmark for (2722ds/2944Mi) % 284.90/40.48 % (2413562)Instruction limit reached! % 284.90/40.48 % (2413562)------------------------------ % 284.90/40.48 % (2413562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.48 % (2413562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.48 % (2413562)CaDiCaL version: 2.1.3 % 284.90/40.48 % (2413562)Termination reason: Instruction limit % 284.90/40.48 % (2413562)Termination phase: Saturation % 284.90/40.48 % (2413562)Time elapsed: 0.924 s % 284.90/40.48 % (2413562)Peak memory usage: 41 MB % 284.90/40.48 % (2413562)Instructions burned: 2946 (million) % 284.90/40.48 % (2413709)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4140553634:i=12648:rtra=on_2712 on theBenchmark for (2712ds/12648Mi) % 284.90/40.48 % (2413709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.90/40.48 % (2413709)Terminated due to inappropriate strategy. % 284.90/40.48 % (2413709)------------------------------ % 284.90/40.48 % (2413709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.48 % (2413709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.48 % (2413709)CaDiCaL version: 2.1.3 % 284.90/40.48 % (2413709)Termination reason: Inappropriate % 284.90/40.48 % (2413709)Time elapsed: 0.001 s % 284.90/40.48 % (2413709)Peak memory usage: 11 MB % 284.90/40.48 % (2413709)Instructions burned: 5 (million) % 284.90/40.48 % (2413709)------------------------------ % 284.90/40.48 % (2413709)------------------------------ % 284.90/40.48 % (2413711)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3253899897:fmbsr=2.30978:i=4348:rtra=on_2712 on theBenchmark for (2712ds/4348Mi) % 284.90/40.48 % (2413711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.90/40.48 % (2413711)Terminated due to inappropriate strategy. % 284.90/40.48 % (2413711)------------------------------ % 284.90/40.48 % (2413711)VersiTerminated % 300.56/42.63 % Vampire exiting %------------------------------------------------------------------------------