%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC451_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:01 PM UTC 2026 % Result : Timeout 300.63s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC451_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 % Computer : n016.cluster.edu % 0.07/0.20 % Model : x86_64 x86_64 % 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.20 % Memory : 8046.5625MB % 0.07/0.20 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 09:44:10 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 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.59/0.86 % (3513075)Will run a generic schedule for satisfiability detection. % 3.59/0.86 % (3513086)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1766809766:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.59/0.86 % (3513081)% WARNING: option uhcvi not known. % 3.59/0.86 % (3513080)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2134627128_2999 on theBenchmark for (2999ds/0Mi) % 3.59/0.86 % (3513081)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1401863502:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.59/0.86 % (3513082)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2419584220:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.59/0.86 % (3513083)dis+10_1_sil=32000:sp=arity:random_seed=3044690113:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.59/0.86 % (3513084)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2560923988:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.59/0.86 % (3513085)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=87978684:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.59/0.86 % (3513080)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.86 % (3513080)Terminated due to inappropriate strategy. % 3.59/0.86 % (3513080)------------------------------ % 3.59/0.86 % (3513080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.86 % (3513080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.86 % (3513080)CaDiCaL version: 2.1.3 % 3.59/0.86 % (3513080)Termination reason: Inappropriate % 3.59/0.86 % (3513080)Time elapsed: 0.001 s % 3.59/0.86 % (3513080)Peak memory usage: 10 MB % 3.59/0.86 % (3513080)Instructions burned: 2 (million) % 3.59/0.86 % (3513080)------------------------------ % 3.59/0.86 % (3513080)------------------------------ % 3.59/0.86 % (3513094)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2793149493:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.59/0.86 % (3513094)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.86 % (3513094)Terminated due to inappropriate strategy. % 3.59/0.86 % (3513094)------------------------------ % 3.59/0.86 % (3513094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.86 % (3513094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.86 % (3513094)CaDiCaL version: 2.1.3 % 3.59/0.86 % (3513094)Termination reason: Inappropriate % 3.59/0.86 % (3513094)Time elapsed: 0.001 s % 3.59/0.86 % (3513094)Peak memory usage: 10 MB % 3.59/0.86 % (3513094)Instructions burned: 2 (million) % 3.59/0.86 % (3513094)------------------------------ % 3.59/0.86 % (3513094)------------------------------ % 3.59/0.86 % (3513096)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2646297271:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.59/0.86 % (3513086)Instruction limit reached! % 3.59/0.86 % (3513086)------------------------------ % 3.59/0.86 % (3513086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.86 % (3513086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.86 % (3513086)CaDiCaL version: 2.1.3 % 3.59/0.86 % (3513086)Termination reason: Instruction limit % 3.59/0.86 % (3513086)Termination phase: Saturation % 3.59/0.86 % (3513086)Time elapsed: 0.056 s % 3.59/0.86 % (3513086)Peak memory usage: 13 MB % 3.59/0.86 % (3513086)Instructions burned: 161 (million) % 3.59/0.86 % (3513098)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=3759087976:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.59/0.86 % (3513083)Instruction limit reached! % 3.59/0.86 % (3513083)------------------------------ % 3.59/0.86 % (3513083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.86 % (3513083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.86 % (3513083)CaDiCaL version: 2.1.3 % 3.59/0.86 % (3513083)Termination reason: Instruction limit % 3.59/0.86 % (3513083)Termination phase: Saturation % 3.59/0.86 % (3513083)Time elapsed: 0.062 s % 3.59/0.86 % (3513083)Peak memory usage: 12 MB % 3.59/0.86 % (3513083)Instructions burned: 103 (million) % 3.59/0.86 % (3513084)Instruction limit reached! % 3.59/0.86 % (3513084)------------------------------ % 3.59/0.86 % (3513084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513084)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513084)Termination reason: Instruction limit % 4.10/1.03 % (3513084)Termination phase: Saturation % 4.10/1.03 % (3513084)Time elapsed: 0.070 s % 4.10/1.03 % (3513084)Peak memory usage: 12 MB % 4.10/1.03 % (3513084)Instructions burned: 117 (million) % 4.10/1.03 % (3513085)Instruction limit reached! % 4.10/1.03 % (3513085)------------------------------ % 4.10/1.03 % (3513085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513085)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513085)Termination reason: Instruction limit % 4.10/1.03 % (3513085)Termination phase: Saturation % 4.10/1.03 % (3513085)Time elapsed: 0.078 s % 4.10/1.03 % (3513085)Peak memory usage: 13 MB % 4.10/1.03 % (3513085)Instructions burned: 131 (million) % 4.10/1.03 % (3513100)ott-21_1_sil=16000:fs=off:random_seed=271296259:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.10/1.03 % (3513101)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1720543724:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.10/1.03 % (3513102)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1873608156:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.10/1.03 % (3513102)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.10/1.03 % (3513102)Terminated due to inappropriate strategy. % 4.10/1.03 % (3513102)------------------------------ % 4.10/1.03 % (3513102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513102)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513102)Termination reason: Inappropriate % 4.10/1.03 % (3513102)Time elapsed: 0.001 s % 4.10/1.03 % (3513102)Peak memory usage: 10 MB % 4.10/1.03 % (3513102)Instructions burned: 2 (million) % 4.10/1.03 % (3513102)------------------------------ % 4.10/1.03 % (3513102)------------------------------ % 4.10/1.03 % (3513106)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=550911669:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.10/1.03 % (3513096)Instruction limit reached! % 4.10/1.03 % (3513096)------------------------------ % 4.10/1.03 % (3513096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513096)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513096)Termination reason: Instruction limit % 4.10/1.03 % (3513096)Termination phase: Saturation % 4.10/1.03 % (3513096)Time elapsed: 0.077 s % 4.10/1.03 % (3513096)Peak memory usage: 12 MB % 4.10/1.03 % (3513096)Instructions burned: 131 (million) % 4.10/1.03 % (3513108)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=278566751:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.10/1.03 % (3513108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.10/1.03 % (3513108)Terminated due to inappropriate strategy. % 4.10/1.03 % (3513108)------------------------------ % 4.10/1.03 % (3513108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513108)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513108)Termination reason: Inappropriate % 4.10/1.03 % (3513108)Time elapsed: 0.001 s % 4.10/1.03 % (3513108)Peak memory usage: 10 MB % 4.10/1.03 % (3513108)Instructions burned: 2 (million) % 4.10/1.03 % (3513108)------------------------------ % 4.10/1.03 % (3513108)------------------------------ % 4.10/1.03 % (3513110)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=1556297412: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) % 4.10/1.03 % (3513100)Instruction limit reached! % 4.10/1.03 % (3513100)------------------------------ % 4.10/1.03 % (3513100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.10/1.03 % (3513100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.03 % (3513100)CaDiCaL version: 2.1.3 % 4.10/1.03 % (3513100)Termination reason: Instruction limit % 4.10/1.03 % (3513100)Termination phase: Saturation % 16.73/2.79 % (3513100)Time elapsed: 0.085 s % 16.73/2.79 % (3513100)Peak memory usage: 12 MB % 16.73/2.79 % (3513100)Instructions burned: 182 (million) % 16.73/2.79 % (3513112)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2621482134:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.73/2.79 % (3513098)Instruction limit reached! % 16.73/2.79 % (3513098)------------------------------ % 16.73/2.79 % (3513098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.73/2.79 % (3513098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.73/2.79 % (3513098)CaDiCaL version: 2.1.3 % 16.73/2.79 % (3513098)Termination reason: Instruction limit % 16.73/2.79 % (3513098)Termination phase: Saturation % 16.73/2.79 % (3513098)Time elapsed: 0.196 s % 16.73/2.79 % (3513098)Peak memory usage: 17 MB % 16.73/2.79 % (3513098)Instructions burned: 684 (million) % 16.73/2.79 % (3513114)fmb+10_1_sil=64000:random_seed=11193987:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 16.73/2.79 % (3513114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.73/2.79 % (3513114)Terminated due to inappropriate strategy. % 16.73/2.79 % (3513114)------------------------------ % 16.73/2.79 % (3513114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.73/2.79 % (3513114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.73/2.79 % (3513114)CaDiCaL version: 2.1.3 % 16.73/2.79 % (3513114)Termination reason: Inappropriate % 16.73/2.79 % (3513114)Time elapsed: 0.001 s % 16.73/2.79 % (3513114)Peak memory usage: 10 MB % 16.73/2.79 % (3513114)Instructions burned: 2 (million) % 16.73/2.79 % (3513114)------------------------------ % 16.73/2.79 % (3513114)------------------------------ % 16.73/2.79 % (3513116)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2108568917:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.73/2.79 % (3513116)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.73/2.79 % (3513116)Terminated due to inappropriate strategy. % 16.73/2.79 % (3513116)------------------------------ % 16.73/2.79 % (3513116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.73/2.79 % (3513116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.73/2.79 % (3513116)CaDiCaL version: 2.1.3 % 16.73/2.79 % (3513116)Termination reason: Inappropriate % 16.73/2.79 % (3513116)Time elapsed: 0.0000 s % 16.73/2.79 % (3513116)Peak memory usage: 10 MB % 16.73/2.79 % (3513116)Instructions burned: 2 (million) % 16.73/2.79 % (3513116)------------------------------ % 16.73/2.79 % (3513116)------------------------------ % 16.73/2.79 % (3513118)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1745169237:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.73/2.79 % (3513118)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.73/2.79 % (3513118)Terminated due to inappropriate strategy. % 16.73/2.79 % (3513118)------------------------------ % 16.73/2.79 % (3513118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.73/2.79 % (3513118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.73/2.79 % (3513118)CaDiCaL version: 2.1.3 % 16.73/2.79 % (3513118)Termination reason: Inappropriate % 16.73/2.79 % (3513118)Time elapsed: 0.0000 s % 16.73/2.79 % (3513118)Peak memory usage: 11 MB % 16.73/2.79 % (3513118)Instructions burned: 2 (million) % 16.73/2.79 % (3513118)------------------------------ % 16.73/2.79 % (3513118)------------------------------ % 16.73/2.79 % (3513120)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1448353353:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 16.73/2.79 % (3513101)Instruction limit reached! % 16.73/2.79 % (3513101)------------------------------ % 16.73/2.79 % (3513101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.73/2.79 % (3513101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.73/2.79 % (3513101)CaDiCaL version: 2.1.3 % 16.73/2.79 % (3513101)Termination reason: Instruction limit % 16.73/2.79 % (3513101)Termination phase: Saturation % 16.73/2.79 % (3513101)Time elapsed: 0.288 s % 16.73/2.79 % (3513101)Peak memory usage: 14 MB % 16.73/2.79 % (3513101)Instructions burned: 478 (million) % 16.73/2.79 % (3513122)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=337157142:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.73/2.79 % (3513110)Instruction limit reached! % 16.73/2.79 % (3513110)------------------------------ % 27.59/4.15 % (3513110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513110)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513110)Termination reason: Instruction limit % 27.59/4.15 % (3513110)Termination phase: Saturation % 27.59/4.15 % (3513110)Time elapsed: 0.430 s % 27.59/4.15 % (3513110)Peak memory usage: 19 MB % 27.59/4.15 % (3513110)Instructions burned: 692 (million) % 27.59/4.15 % (3513124)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=122136790:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.59/4.15 % (3513124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.59/4.15 % (3513124)Terminated due to inappropriate strategy. % 27.59/4.15 % (3513124)------------------------------ % 27.59/4.15 % (3513124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513124)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513124)Termination reason: Inappropriate % 27.59/4.15 % (3513124)Time elapsed: 0.001 s % 27.59/4.15 % (3513124)Peak memory usage: 10 MB % 27.59/4.15 % (3513124)Instructions burned: 2 (million) % 27.59/4.15 % (3513124)------------------------------ % 27.59/4.15 % (3513124)------------------------------ % 27.59/4.15 % (3513126)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3869119319:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.59/4.15 % (3513126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.59/4.15 % (3513126)Terminated due to inappropriate strategy. % 27.59/4.15 % (3513126)------------------------------ % 27.59/4.15 % (3513126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513126)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513126)Termination reason: Inappropriate % 27.59/4.15 % (3513126)Time elapsed: 0.001 s % 27.59/4.15 % (3513126)Peak memory usage: 10 MB % 27.59/4.15 % (3513126)Instructions burned: 2 (million) % 27.59/4.15 % (3513126)------------------------------ % 27.59/4.15 % (3513126)------------------------------ % 27.59/4.15 % (3513128)ott-2_1_sil=16000:newcnf=on:random_seed=866823007:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.59/4.15 % (3513112)Instruction limit reached! % 27.59/4.15 % (3513112)------------------------------ % 27.59/4.15 % (3513112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513112)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513112)Termination reason: Instruction limit % 27.59/4.15 % (3513112)Termination phase: Saturation % 27.59/4.15 % (3513112)Time elapsed: 0.515 s % 27.59/4.15 % (3513112)Peak memory usage: 20 MB % 27.59/4.15 % (3513112)Instructions burned: 879 (million) % 27.59/4.15 % (3513130)ott+10_1_sil=32000:tgt=ground:random_seed=2076878019:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.59/4.15 % (3513106)Instruction limit reached! % 27.59/4.15 % (3513106)------------------------------ % 27.59/4.15 % (3513106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513106)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513106)Termination reason: Instruction limit % 27.59/4.15 % (3513106)Termination phase: Saturation % 27.59/4.15 % (3513106)Time elapsed: 0.615 s % 27.59/4.15 % (3513106)Peak memory usage: 17 MB % 27.59/4.15 % (3513106)Instructions burned: 1180 (million) % 27.59/4.15 % (3513132)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4290219360:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 27.59/4.15 % (3513132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.59/4.15 % (3513132)Terminated due to inappropriate strategy. % 27.59/4.15 % (3513132)------------------------------ % 27.59/4.15 % (3513132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.59/4.15 % (3513132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.59/4.15 % (3513132)CaDiCaL version: 2.1.3 % 27.59/4.15 % (3513132)Termination reason: Inappropriate % 27.59/4.15 % (3513132)Time elapsed: 0.001 s % 27.59/4.15 % (3513132)Peak memory usage: 11 MB % 27.59/4.15 % (3513132)Instructions burned: 2 (million) % 91.96/13.25 % (3513132)------------------------------ % 91.96/13.25 % (3513132)------------------------------ % 91.96/13.25 % (3513134)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3607382076:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 91.96/13.25 % (3513128)Instruction limit reached! % 91.96/13.25 % (3513128)------------------------------ % 91.96/13.25 % (3513128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513128)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513128)Termination reason: Instruction limit % 91.96/13.25 % (3513128)Termination phase: Saturation % 91.96/13.25 % (3513128)Time elapsed: 0.516 s % 91.96/13.25 % (3513128)Peak memory usage: 17 MB % 91.96/13.25 % (3513128)Instructions burned: 869 (million) % 91.96/13.25 % (3513136)dis+21_1_sil=32000:sas=cadical:random_seed=167031451:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 91.96/13.25 % (3513122)Instruction limit reached! % 91.96/13.25 % (3513122)------------------------------ % 91.96/13.25 % (3513122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513122)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513122)Termination reason: Instruction limit % 91.96/13.25 % (3513122)Termination phase: Saturation % 91.96/13.25 % (3513122)Time elapsed: 0.855 s % 91.96/13.25 % (3513122)Peak memory usage: 29 MB % 91.96/13.25 % (3513122)Instructions burned: 1472 (million) % 91.96/13.25 % (3513138)ott+11_1_sil=16000:gs=on:random_seed=426426483:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 91.96/13.25 % (3513120)Instruction limit reached! % 91.96/13.25 % (3513120)------------------------------ % 91.96/13.25 % (3513120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513120)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513120)Termination reason: Instruction limit % 91.96/13.25 % (3513120)Termination phase: Saturation % 91.96/13.25 % (3513120)Time elapsed: 1.443 s % 91.96/13.25 % (3513120)Peak memory usage: 42 MB % 91.96/13.25 % (3513120)Instructions burned: 5137 (million) % 91.96/13.25 % (3513140)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1270590924:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 91.96/13.25 % (3513140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.96/13.25 % (3513140)Terminated due to inappropriate strategy. % 91.96/13.25 % (3513140)------------------------------ % 91.96/13.25 % (3513140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513140)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513140)Termination reason: Inappropriate % 91.96/13.25 % (3513140)Time elapsed: 0.001 s % 91.96/13.25 % (3513140)Peak memory usage: 10 MB % 91.96/13.25 % (3513140)Instructions burned: 2 (million) % 91.96/13.25 % (3513140)------------------------------ % 91.96/13.25 % (3513140)------------------------------ % 91.96/13.25 % (3513142)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1510123242:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 91.96/13.25 % (3513134)Instruction limit reached! % 91.96/13.25 % (3513134)------------------------------ % 91.96/13.25 % (3513134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513134)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513134)Termination reason: Instruction limit % 91.96/13.25 % (3513134)Termination phase: Saturation % 91.96/13.25 % (3513134)Time elapsed: 1.591 s % 91.96/13.25 % (3513134)Peak memory usage: 25 MB % 91.96/13.25 % (3513134)Instructions burned: 3514 (million) % 91.96/13.25 % (3513144)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4049611812:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 91.96/13.25 % (3513138)Instruction limit reached! % 91.96/13.25 % (3513138)------------------------------ % 91.96/13.25 % (3513138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.96/13.25 % (3513138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.96/13.25 % (3513138)CaDiCaL version: 2.1.3 % 91.96/13.25 % (3513138)Termination reason: Instruction limit % 113.27/16.21 % (3513138)Termination phase: Saturation % 113.27/16.21 % (3513138)Time elapsed: 1.235 s % 113.27/16.21 % (3513138)Peak memory usage: 22 MB % 113.27/16.21 % (3513138)Instructions burned: 2252 (million) % 113.27/16.21 % (3513146)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1845253761:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 113.27/16.21 % (3513142)Instruction limit reached! % 113.27/16.21 % (3513142)------------------------------ % 113.27/16.21 % (3513142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.27/16.21 % (3513142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.27/16.21 % (3513142)CaDiCaL version: 2.1.3 % 113.27/16.21 % (3513142)Termination reason: Instruction limit % 113.27/16.21 % (3513142)Termination phase: Saturation % 113.27/16.21 % (3513142)Time elapsed: 1.307 s % 113.27/16.21 % (3513142)Peak memory usage: 44 MB % 113.27/16.21 % (3513142)Instructions burned: 4593 (million) % 113.27/16.21 % (3513148)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1155626985:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 113.27/16.21 % (3513148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.27/16.21 % (3513148)Terminated due to inappropriate strategy. % 113.27/16.21 % (3513148)------------------------------ % 113.27/16.21 % (3513148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.27/16.21 % (3513148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.27/16.21 % (3513148)CaDiCaL version: 2.1.3 % 113.27/16.21 % (3513148)Termination reason: Inappropriate % 113.27/16.21 % (3513148)Time elapsed: 0.001 s % 113.27/16.21 % (3513148)Peak memory usage: 10 MB % 113.27/16.21 % (3513148)Instructions burned: 2 (million) % 113.27/16.21 % (3513148)------------------------------ % 113.27/16.21 % (3513148)------------------------------ % 113.27/16.21 % (3513150)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4225352324:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 113.27/16.21 % (3513150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.27/16.21 % (3513150)Terminated due to inappropriate strategy. % 113.27/16.21 % (3513150)------------------------------ % 113.27/16.21 % (3513150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.27/16.21 % (3513150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.27/16.21 % (3513150)CaDiCaL version: 2.1.3 % 113.27/16.21 % (3513150)Termination reason: Inappropriate % 113.27/16.21 % (3513150)Time elapsed: 0.0000 s % 113.27/16.21 % (3513150)Peak memory usage: 10 MB % 113.27/16.21 % (3513150)Instructions burned: 2 (million) % 113.27/16.21 % (3513150)------------------------------ % 113.27/16.21 % (3513150)------------------------------ % 113.27/16.21 % (3513152)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2646138557:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 113.27/16.21 % (3513152)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.27/16.21 % (3513152)Terminated due to inappropriate strategy. % 113.27/16.21 % (3513152)------------------------------ % 113.27/16.21 % (3513152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.27/16.21 % (3513152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.27/16.21 % (3513152)CaDiCaL version: 2.1.3 % 113.27/16.21 % (3513152)Termination reason: Inappropriate % 113.27/16.21 % (3513152)Time elapsed: 0.0000 s % 113.27/16.21 % (3513152)Peak memory usage: 10 MB % 113.27/16.21 % (3513152)Instructions burned: 2 (million) % 113.27/16.21 % (3513152)------------------------------ % 113.27/16.21 % (3513152)------------------------------ % 113.27/16.21 % (3513154)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4270879135:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 113.27/16.21 % (3513136)Instruction limit reached! % 113.27/16.21 % (3513136)------------------------------ % 113.27/16.21 % (3513136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.27/16.21 % (3513136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.27/16.21 % (3513136)CaDiCaL version: 2.1.3 % 113.27/16.21 % (3513136)Termination reason: Instruction limit % 113.27/16.21 % (3513136)Termination phase: Saturation % 113.27/16.21 % (3513136)Time elapsed: 2.018 s % 113.27/16.21 % (3513136)Peak memory usage: 31 MB % 113.27/16.21 % (3513136)Instructions burned: 3774 (million) % 113.27/16.21 % (3513156)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2981298267:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 113.27/16.21 % (3513130)Instruction limit reached! % 113.98/16.33 % (3513130)------------------------------ % 113.98/16.33 % (3513130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513130)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513130)Termination reason: Instruction limit % 113.98/16.33 % (3513130)Termination phase: Saturation % 113.98/16.33 % (3513130)Time elapsed: 3.150 s % 113.98/16.33 % (3513130)Peak memory usage: 34 MB % 113.98/16.33 % (3513130)Instructions burned: 5114 (million) % 113.98/16.33 % (3513158)dis+10_16:1_sil=16000:random_seed=3936767464:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 113.98/16.33 % (3513146)Instruction limit reached! % 113.98/16.33 % (3513146)------------------------------ % 113.98/16.33 % (3513146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513146)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513146)Termination reason: Instruction limit % 113.98/16.33 % (3513146)Termination phase: Saturation % 113.98/16.33 % (3513146)Time elapsed: 2.763 s % 113.98/16.33 % (3513146)Peak memory usage: 53 MB % 113.98/16.33 % (3513146)Instructions burned: 5212 (million) % 113.98/16.33 % (3513160)ott-3_8_sil=64000:random_seed=3590010215:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 113.98/16.33 % (3513154)Instruction limit reached! % 113.98/16.33 % (3513154)------------------------------ % 113.98/16.33 % (3513154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513154)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513154)Termination reason: Instruction limit % 113.98/16.33 % (3513154)Termination phase: Saturation % 113.98/16.33 % (3513154)Time elapsed: 5.176 s % 113.98/16.33 % (3513154)Peak memory usage: 74 MB % 113.98/16.33 % (3513154)Instructions burned: 22567 (million) % 113.98/16.33 % (3513156)Instruction limit reached! % 113.98/16.33 % (3513156)------------------------------ % 113.98/16.33 % (3513156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513156)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513156)Termination reason: Instruction limit % 113.98/16.33 % (3513156)Termination phase: Saturation % 113.98/16.33 % (3513156)Time elapsed: 5.087 s % 113.98/16.33 % (3513156)Peak memory usage: 55 MB % 113.98/16.33 % (3513156)Instructions burned: 8173 (million) % 113.98/16.33 % (3513162)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=433551314:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 113.98/16.33 % (3513162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.98/16.33 % (3513162)Terminated due to inappropriate strategy. % 113.98/16.33 % (3513162)------------------------------ % 113.98/16.33 % (3513162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513162)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513162)Termination reason: Inappropriate % 113.98/16.33 % (3513162)Time elapsed: 0.001 s % 113.98/16.33 % (3513162)Peak memory usage: 10 MB % 113.98/16.33 % (3513162)Instructions burned: 2 (million) % 113.98/16.33 % (3513162)------------------------------ % 113.98/16.33 % (3513162)------------------------------ % 113.98/16.33 % (3513165)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3608318641:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 113.98/16.33 % (3513163)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1086788225:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 113.98/16.33 % (3513158)Instruction limit reached! % 113.98/16.33 % (3513158)------------------------------ % 113.98/16.33 % (3513158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.98/16.33 % (3513158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.98/16.33 % (3513158)CaDiCaL version: 2.1.3 % 113.98/16.33 % (3513158)Termination reason: Instruction limit % 113.98/16.33 % (3513158)Termination phase: Saturation % 113.98/16.33 % (3513158)Time elapsed: 4.611 s % 113.98/16.33 % (3513158)Peak memory usage: 52 MB % 113.98/16.33 % (3513158)Instructions burned: 9156 (million) % 113.98/16.33 % (3513168)dis+33_16_sil=32000:sac=on:random_seed=1633108711:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 113.98/16.33 % (3513165)Instruction limit reached! % 113.98/16.33 % (3513165)------------------------------ % 113.98/16.33 % (3513165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513165)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513165)Termination reason: Instruction limit % 128.12/18.37 % (3513165)Termination phase: Saturation % 128.12/18.37 % (3513165)Time elapsed: 4.626 s % 128.12/18.37 % (3513165)Peak memory usage: 78 MB % 128.12/18.37 % (3513165)Instructions burned: 14136 (million) % 128.12/18.37 % (3513170)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1933033595:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 128.12/18.37 % (3513144)Instruction limit reached! % 128.12/18.37 % (3513144)------------------------------ % 128.12/18.37 % (3513144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513144)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513144)Termination reason: Instruction limit % 128.12/18.37 % (3513144)Termination phase: Saturation % 128.12/18.37 % (3513144)Time elapsed: 12.280 s % 128.12/18.37 % (3513144)Peak memory usage: 145 MB % 128.12/18.37 % (3513144)Instructions burned: 29342 (million) % 128.12/18.37 % (3513172)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1310573451:s2a=on:i=53295_2852 on theBenchmark for (2852ds/53295Mi) % 128.12/18.37 % (3513163)Instruction limit reached! % 128.12/18.37 % (3513163)------------------------------ % 128.12/18.37 % (3513163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513163)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513163)Termination reason: Instruction limit % 128.12/18.37 % (3513163)Termination phase: Saturation % 128.12/18.37 % (3513163)Time elapsed: 7.067 s % 128.12/18.37 % (3513163)Peak memory usage: 62 MB % 128.12/18.37 % (3513163)Instructions burned: 11405 (million) % 128.12/18.37 % (3513174)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1770862446:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 128.12/18.37 % (3513174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.12/18.37 % (3513174)Terminated due to inappropriate strategy. % 128.12/18.37 % (3513174)------------------------------ % 128.12/18.37 % (3513174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513174)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513174)Termination reason: Inappropriate % 128.12/18.37 % (3513174)Time elapsed: 0.001 s % 128.12/18.37 % (3513174)Peak memory usage: 10 MB % 128.12/18.37 % (3513174)Instructions burned: 2 (million) % 128.12/18.37 % (3513174)------------------------------ % 128.12/18.37 % (3513174)------------------------------ % 128.12/18.37 % (3513176)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1427893632:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 128.12/18.37 % (3513168)Instruction limit reached! % 128.12/18.37 % (3513168)------------------------------ % 128.12/18.37 % (3513168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513168)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513168)Termination reason: Instruction limit % 128.12/18.37 % (3513168)Termination phase: Saturation % 128.12/18.37 % (3513168)Time elapsed: 7.342 s % 128.12/18.37 % (3513168)Peak memory usage: 174 MB % 128.12/18.37 % (3513168)Instructions burned: 15851 (million) % 128.12/18.37 % (3513178)fmb+10_1_sil=256000:fmbss=7:random_seed=1320679725:fmbsr=1.6:i=182295_2840 on theBenchmark for (2840ds/182295Mi) % 128.12/18.37 % (3513178)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.12/18.37 % (3513178)Terminated due to inappropriate strategy. % 128.12/18.37 % (3513178)------------------------------ % 128.12/18.37 % (3513178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.12/18.37 % (3513178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.12/18.37 % (3513178)CaDiCaL version: 2.1.3 % 128.12/18.37 % (3513178)Termination reason: Inappropriate % 128.12/18.37 % (3513178)Time elapsed: 0.001 s % 128.12/18.37 % (3513178)Peak memory usage: 11 MB % 128.12/18.37 % (3513178)Instructions burned: 2 (million) % 128.12/18.37 % (3513178)------------------------------ % 128.12/18.37 % (3513178)------------------------------ % 128.12/18.37 % (3513180)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1151397318:i=44625:gsp=on_2840 on theBenchmark for (2840ds/44625Mi) % 135.23/19.32 % (3513180)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.23/19.32 % (3513180)Terminated due to inappropriate strategy. % 135.23/19.32 % (3513180)------------------------------ % 135.23/19.32 % (3513180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.23/19.32 % (3513180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.23/19.32 % (3513180)CaDiCaL version: 2.1.3 % 135.23/19.32 % (3513180)Termination reason: Inappropriate % 135.23/19.32 % (3513180)Time elapsed: 0.001 s % 135.23/19.32 % (3513180)Peak memory usage: 11 MB % 135.23/19.32 % (3513180)Instructions burned: 2 (million) % 135.23/19.32 % (3513180)------------------------------ % 135.23/19.32 % (3513180)------------------------------ % 135.23/19.32 % (3513182)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1071509875:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 135.23/19.32 % (3513182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.23/19.32 % (3513182)Terminated due to inappropriate strategy. % 135.23/19.32 % (3513182)------------------------------ % 135.23/19.32 % (3513182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.23/19.32 % (3513182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.23/19.32 % (3513182)CaDiCaL version: 2.1.3 % 135.23/19.32 % (3513182)Termination reason: Inappropriate % 135.23/19.32 % (3513182)Time elapsed: 0.001 s % 135.23/19.32 % (3513182)Peak memory usage: 10 MB % 135.23/19.32 % (3513182)Instructions burned: 2 (million) % 135.23/19.32 % (3513182)------------------------------ % 135.23/19.32 % (3513182)------------------------------ % 135.23/19.32 % (3513184)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1624242596:fmbsr=1.3:i=225729_2839 on theBenchmark for (2839ds/225729Mi) % 135.23/19.32 % (3513184)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.23/19.32 % (3513184)Terminated due to inappropriate strategy. % 135.23/19.32 % (3513184)------------------------------ % 135.23/19.32 % (3513184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.23/19.32 % (3513184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.23/19.32 % (3513184)CaDiCaL version: 2.1.3 % 135.23/19.32 % (3513184)Termination reason: Inappropriate % 135.23/19.32 % (3513184)Time elapsed: 0.001 s % 135.23/19.32 % (3513184)Peak memory usage: 10 MB % 135.23/19.32 % (3513184)Instructions burned: 2 (million) % 135.23/19.32 % (3513184)------------------------------ % 135.23/19.32 % (3513184)------------------------------ % 135.23/19.32 % (3513186)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=359782740:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 135.23/19.32 % (3513186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.23/19.32 % (3513186)Terminated due to inappropriate strategy. % 135.23/19.32 % (3513186)------------------------------ % 135.23/19.32 % (3513186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.23/19.32 % (3513186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.23/19.32 % (3513186)CaDiCaL version: 2.1.3 % 135.23/19.32 % (3513186)Termination reason: Inappropriate % 135.23/19.32 % (3513186)Time elapsed: 0.001 s % 135.23/19.32 % (3513186)Peak memory usage: 11 MB % 135.23/19.32 % (3513186)Instructions burned: 2 (million) % 135.23/19.32 % (3513186)------------------------------ % 135.23/19.32 % (3513186)------------------------------ % 135.23/19.32 % (3513188)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1282121619:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 135.23/19.32 % (3513188)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.23/19.32 % (3513188)Terminated due to inappropriate strategy. % 135.23/19.32 % (3513188)------------------------------ % 135.23/19.32 % (3513188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.23/19.32 % (3513188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.23/19.32 % (3513188)CaDiCaL version: 2.1.3 % 135.23/19.32 % (3513188)Termination reason: Inappropriate % 135.23/19.32 % (3513188)Time elapsed: 0.001 s % 135.23/19.32 % (3513188)Peak memory usage: 10 MB % 135.23/19.32 % (3513188)Instructions burned: 2 (million) % 135.23/19.32 % (3513188)------------------------------ % 135.23/19.32 % (3513188)------------------------------ % 135.23/19.32 % (3513190)% WARNING: option uhcvi not known. % 135.23/19.32 % (3513190)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4201925082:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi) % 147.02/21.08 % (3513160)Instruction limit reached! % 147.02/21.08 % (3513160)------------------------------ % 147.02/21.08 % (3513160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513160)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513160)Termination reason: Instruction limit % 147.02/21.08 % (3513160)Termination phase: Saturation % 147.02/21.08 % (3513160)Time elapsed: 10.839 s % 147.02/21.08 % (3513160)Peak memory usage: 73 MB % 147.02/21.08 % (3513160)Instructions burned: 20140 (million) % 147.02/21.08 % (3513192)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1390341864:i=176048:add=on:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/176048Mi) % 147.02/21.08 % (3513170)Instruction limit reached! % 147.02/21.08 % (3513170)------------------------------ % 147.02/21.08 % (3513170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513170)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513170)Termination reason: Instruction limit % 147.02/21.08 % (3513170)Termination phase: Saturation % 147.02/21.08 % (3513170)Time elapsed: 4.693 s % 147.02/21.08 % (3513170)Peak memory usage: 119 MB % 147.02/21.08 % (3513170)Instructions burned: 17629 (million) % 147.02/21.08 % (3513194)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2869981285:i=206:fgj=on:rtra=on_2822 on theBenchmark for (2822ds/206Mi) % 147.02/21.08 % (3513194)Instruction limit reached! % 147.02/21.08 % (3513194)------------------------------ % 147.02/21.08 % (3513194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513194)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513194)Termination reason: Instruction limit % 147.02/21.08 % (3513194)Termination phase: Saturation % 147.02/21.08 % (3513194)Time elapsed: 0.066 s % 147.02/21.08 % (3513194)Peak memory usage: 13 MB % 147.02/21.08 % (3513194)Instructions burned: 208 (million) % 147.02/21.08 % (3513196)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=833895698:i=232:rtra=on_2821 on theBenchmark for (2821ds/232Mi) % 147.02/21.08 % (3513196)Instruction limit reached! % 147.02/21.08 % (3513196)------------------------------ % 147.02/21.08 % (3513196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513196)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513196)Termination reason: Instruction limit % 147.02/21.08 % (3513196)Termination phase: Saturation % 147.02/21.08 % (3513196)Time elapsed: 0.077 s % 147.02/21.08 % (3513196)Peak memory usage: 13 MB % 147.02/21.08 % (3513196)Instructions burned: 232 (million) % 147.02/21.08 % (3513198)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2607694171:i=262:rtra=on_2821 on theBenchmark for (2821ds/262Mi) % 147.02/21.08 % (3513198)Instruction limit reached! % 147.02/21.08 % (3513198)------------------------------ % 147.02/21.08 % (3513198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513198)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513198)Termination reason: Instruction limit % 147.02/21.08 % (3513198)Termination phase: Saturation % 147.02/21.08 % (3513198)Time elapsed: 0.086 s % 147.02/21.08 % (3513198)Peak memory usage: 14 MB % 147.02/21.08 % (3513198)Instructions burned: 264 (million) % 147.02/21.08 % (3513200)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2210761608:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2820 on theBenchmark for (2820ds/318Mi) % 147.02/21.08 % (3513200)Instruction limit reached! % 147.02/21.08 % (3513200)------------------------------ % 147.02/21.08 % (3513200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.02/21.08 % (3513200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.02/21.08 % (3513200)CaDiCaL version: 2.1.3 % 147.02/21.08 % (3513200)Termination reason: Instruction limit % 147.02/21.08 % (3513200)Termination phase: Saturation % 147.02/21.08 % (3513200)Time elapsed: 0.113 s % 147.02/21.08 % (3513200)Peak memory usage: 15 MB % 147.02/21.08 % (3513200)Instructions burned: 320 (million) % 147.02/21.08 % (3513202)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3035748365:i=1428:nm=2:rtra=on_2818 on theBenchmark for (2818ds/1428Mi) % 176.84/25.34 % (3513202)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.84/25.34 % (3513202)Terminated due to inappropriate strategy. % 176.84/25.34 % (3513202)------------------------------ % 176.84/25.34 % (3513202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513202)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513202)Termination reason: Inappropriate % 176.84/25.34 % (3513202)Time elapsed: 0.001 s % 176.84/25.34 % (3513202)Peak memory usage: 10 MB % 176.84/25.34 % (3513202)Instructions burned: 2 (million) % 176.84/25.34 % (3513202)------------------------------ % 176.84/25.34 % (3513202)------------------------------ % 176.84/25.34 % (3513204)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2607638283:i=262:bd=preordered:rtra=on:fsd=on_2818 on theBenchmark for (2818ds/262Mi) % 176.84/25.34 % (3513204)Instruction limit reached! % 176.84/25.34 % (3513204)------------------------------ % 176.84/25.34 % (3513204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513204)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513204)Termination reason: Instruction limit % 176.84/25.34 % (3513204)Termination phase: Saturation % 176.84/25.34 % (3513204)Time elapsed: 0.083 s % 176.84/25.34 % (3513204)Peak memory usage: 13 MB % 176.84/25.34 % (3513204)Instructions burned: 264 (million) % 176.84/25.34 % (3513206)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=2190729642:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/1368Mi) % 176.84/25.34 % (3513206)Instruction limit reached! % 176.84/25.34 % (3513206)------------------------------ % 176.84/25.34 % (3513206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513206)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513206)Termination reason: Instruction limit % 176.84/25.34 % (3513206)Termination phase: Saturation % 176.84/25.34 % (3513206)Time elapsed: 0.400 s % 176.84/25.34 % (3513206)Peak memory usage: 21 MB % 176.84/25.34 % (3513206)Instructions burned: 1369 (million) % 176.84/25.34 % (3513208)ott-21_1_sil=16000:si=on:fs=off:random_seed=4272483246:i=360:av=off:fsr=off:rtra=on_2813 on theBenchmark for (2813ds/360Mi) % 176.84/25.34 % (3513208)Instruction limit reached! % 176.84/25.34 % (3513208)------------------------------ % 176.84/25.34 % (3513208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513208)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513208)Termination reason: Instruction limit % 176.84/25.34 % (3513208)Termination phase: Saturation % 176.84/25.34 % (3513208)Time elapsed: 0.086 s % 176.84/25.34 % (3513208)Peak memory usage: 13 MB % 176.84/25.34 % (3513208)Instructions burned: 364 (million) % 176.84/25.34 % (3513210)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1092528840:i=954:bd=all:rtra=on_2812 on theBenchmark for (2812ds/954Mi) % 176.84/25.34 % (3513210)Instruction limit reached! % 176.84/25.34 % (3513210)------------------------------ % 176.84/25.34 % (3513210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513210)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513210)Termination reason: Instruction limit % 176.84/25.34 % (3513210)Termination phase: Saturation % 176.84/25.34 % (3513210)Time elapsed: 0.326 s % 176.84/25.34 % (3513210)Peak memory usage: 15 MB % 176.84/25.34 % (3513210)Instructions burned: 957 (million) % 176.84/25.34 % (3513212)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3955259803:fmbsr=1.3:i=1730:ins=25:rtra=on_2809 on theBenchmark for (2809ds/1730Mi) % 176.84/25.34 % (3513212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.84/25.34 % (3513212)Terminated due to inappropriate strategy. % 176.84/25.34 % (3513212)------------------------------ % 176.84/25.34 % (3513212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.84/25.34 % (3513212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.84/25.34 % (3513212)CaDiCaL version: 2.1.3 % 176.84/25.34 % (3513212)Termination reason: Inappropriate % 176.84/25.34 % (3513212)Time elapsed: 0.001 s % 223.39/32.05 % (3513212)Peak memory usage: 10 MB % 223.39/32.05 % (3513212)Instructions burned: 2 (million) % 223.39/32.05 % (3513212)------------------------------ % 223.39/32.05 % (3513212)------------------------------ % 223.39/32.05 % (3513214)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2339462627:i=2358:rtra=on_2809 on theBenchmark for (2809ds/2358Mi) % 223.39/32.05 % (3513214)Instruction limit reached! % 223.39/32.05 % (3513214)------------------------------ % 223.39/32.05 % (3513214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.39/32.05 % (3513214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.39/32.05 % (3513214)CaDiCaL version: 2.1.3 % 223.39/32.05 % (3513214)Termination reason: Instruction limit % 223.39/32.05 % (3513214)Termination phase: Saturation % 223.39/32.05 % (3513214)Time elapsed: 0.675 s % 223.39/32.05 % (3513214)Peak memory usage: 21 MB % 223.39/32.05 % (3513214)Instructions burned: 2358 (million) % 223.39/32.05 % (3513216)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2314713517:i=1778:ins=1:rtra=on_2802 on theBenchmark for (2802ds/1778Mi) % 223.39/32.05 % (3513216)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.39/32.05 % (3513216)Terminated due to inappropriate strategy. % 223.39/32.05 % (3513216)------------------------------ % 223.39/32.05 % (3513216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.39/32.05 % (3513216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.39/32.05 % (3513216)CaDiCaL version: 2.1.3 % 223.39/32.05 % (3513216)Termination reason: Inappropriate % 223.39/32.05 % (3513216)Time elapsed: 0.001 s % 223.39/32.05 % (3513216)Peak memory usage: 10 MB % 223.39/32.05 % (3513216)Instructions burned: 2 (million) % 223.39/32.05 % (3513216)------------------------------ % 223.39/32.05 % (3513216)------------------------------ % 223.39/32.05 % (3513218)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=2919659319:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/1384Mi) % 223.39/32.05 % (3513218)Instruction limit reached! % 223.39/32.05 % (3513218)------------------------------ % 223.39/32.05 % (3513218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.39/32.05 % (3513218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.39/32.05 % (3513218)CaDiCaL version: 2.1.3 % 223.39/32.05 % (3513218)Termination reason: Instruction limit % 223.39/32.05 % (3513218)Termination phase: Saturation % 223.39/32.05 % (3513218)Time elapsed: 0.452 s % 223.39/32.05 % (3513218)Peak memory usage: 24 MB % 223.39/32.05 % (3513218)Instructions burned: 1385 (million) % 223.39/32.05 % (3513220)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=194145531:i=1758:kws=inv_precedence:fsr=off:rtra=on_2797 on theBenchmark for (2797ds/1758Mi) % 223.39/32.05 % (3513220)Instruction limit reached! % 223.39/32.05 % (3513220)------------------------------ % 223.39/32.05 % (3513220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.39/32.05 % (3513220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.39/32.05 % (3513220)CaDiCaL version: 2.1.3 % 223.39/32.05 % (3513220)Termination reason: Instruction limit % 223.39/32.05 % (3513220)Termination phase: Saturation % 223.39/32.05 % (3513220)Time elapsed: 0.532 s % 223.39/32.05 % (3513220)Peak memory usage: 27 MB % 223.39/32.05 % (3513220)Instructions burned: 1760 (million) % 223.39/32.05 % (3513222)fmb+10_1_sil=64000:si=on:random_seed=2508653984:i=44122:nm=2:rtra=on:gsp=on_2792 on theBenchmark for (2792ds/44122Mi) % 223.39/32.05 % (3513222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.39/32.05 % (3513222)Terminated due to inappropriate strategy. % 223.39/32.05 % (3513222)------------------------------ % 223.39/32.05 % (3513222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.39/32.05 % (3513222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.39/32.05 % (3513222)CaDiCaL version: 2.1.3 % 223.39/32.05 % (3513222)Termination reason: Inappropriate % 223.39/32.05 % (3513222)Time elapsed: 0.001 s % 223.39/32.05 % (3513222)Peak memory usage: 10 MB % 223.39/32.05 % (3513222)Instructions burned: 2 (million) % 223.39/32.05 % (3513222)------------------------------ % 223.39/32.05 % (3513222)------------------------------ % 223.39/32.05 % (3513224)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3852282208:i=19030:nm=5:rtra=on_2791 on theBenchmark for (2791ds/19030Mi) % 270.14/38.31 % (3513224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.14/38.31 % (3513224)Terminated due to inappropriate strategy. % 270.14/38.31 % (3513224)------------------------------ % 270.14/38.31 % (3513224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.14/38.31 % (3513224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.14/38.31 % (3513224)CaDiCaL version: 2.1.3 % 270.14/38.31 % (3513224)Termination reason: Inappropriate % 270.14/38.31 % (3513224)Time elapsed: 0.001 s % 270.14/38.31 % (3513224)Peak memory usage: 10 MB % 270.14/38.31 % (3513224)Instructions burned: 2 (million) % 270.14/38.31 % (3513224)------------------------------ % 270.14/38.31 % (3513224)------------------------------ % 270.14/38.31 % (3513226)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2043578976:fmbsr=1.7:i=1840:rtra=on_2791 on theBenchmark for (2791ds/1840Mi) % 270.14/38.31 % (3513226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.14/38.31 % (3513226)Terminated due to inappropriate strategy. % 270.14/38.31 % (3513226)------------------------------ % 270.14/38.31 % (3513226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.14/38.31 % (3513226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.14/38.31 % (3513226)CaDiCaL version: 2.1.3 % 270.14/38.31 % (3513226)Termination reason: Inappropriate % 270.14/38.31 % (3513226)Time elapsed: 0.001 s % 270.14/38.31 % (3513226)Peak memory usage: 10 MB % 270.14/38.31 % (3513226)Instructions burned: 2 (million) % 270.14/38.31 % (3513226)------------------------------ % 270.14/38.31 % (3513226)------------------------------ % 270.14/38.31 % (3513228)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3174096076:i=10262:rtra=on_2791 on theBenchmark for (2791ds/10262Mi) % 270.14/38.31 % (3513228)Instruction limit reached! % 270.14/38.31 % (3513228)------------------------------ % 270.14/38.31 % (3513228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.14/38.31 % (3513228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.14/38.31 % (3513228)CaDiCaL version: 2.1.3 % 270.14/38.31 % (3513228)Termination reason: Instruction limit % 270.14/38.31 % (3513228)Termination phase: Saturation % 270.14/38.32 % (3513228)Time elapsed: 3.192 s % 270.14/38.32 % (3513228)Peak memory usage: 68 MB % 270.14/38.32 % (3513228)Instructions burned: 10263 (million) % 270.14/38.32 % (3513230)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3836854690:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2759 on theBenchmark for (2759ds/2944Mi) % 270.14/38.32 % (3513230)Instruction limit reached! % 270.14/38.32 % (3513230)------------------------------ % 270.14/38.32 % (3513230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.14/38.32 % (3513230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.14/38.32 % (3513230)CaDiCaL version: 2.1.3 % 270.14/38.32 % (3513230)Termination reason: Instruction limit % 270.14/38.32 % (3513230)Termination phase: Saturation % 270.14/38.32 % (3513230)Time elapsed: 0.945 s % 270.14/38.32 % (3513230)Peak memory usage: 62 MB % 270.14/38.32 % (3513230)Instructions burned: 2946 (million) % 270.14/38.32 % (3513232)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3468700057:i=12648:rtra=on_2749 on theBenchmark for (2749ds/12648Mi) % 270.14/38.32 % (3513232)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.14/38.32 % (3513232)Terminated due to inappropriate strategy. % 270.14/38.32 % (3513232)------------------------------ % 270.14/38.32 % (3513232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.14/38.32 % (3513232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.14/38.32 % (3513232)CaDiCaL version: 2.1.3 % 270.14/38.32 % (3513232)Termination reason: Inappropriate % 270.14/38.32 % (3513232)Time elapsed: 0.001 s % 270.14/38.32 % (3513232)Peak memory usage: 11 MB % 270.14/38.32 % (3513232)Instructions burned: 2 (million) % 270.14/38.32 % (3513232)------------------------------ % 270.14/38.32 % (3513232)------------------------------ % 270.14/38.32 % (3513234)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=512068843:fmbsr=2.30978:i=4348:rtra=on_2749 on theBenchmark for (2749ds/4348Mi) % 270.14/38.32 % (3513234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.14/38.32 % (3513234)Terminated due to inappropriate strategy. % 270.14/38.32 % (3513234)------------------------------ % 270.14/38.32 % (3513234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3513234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3513234)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3513234)Termination reason: Inappropriate % 300.63/42.63 % (3513234)Time elapsed: 0.003 s % 300.63/42.63 % (3513234)Peak memory usage: 10 MB % 300.63/42.63 % (3513234)Instructions burned: 2 (million) % 300.63/42.63 % (3513234)------------------------------ % 300.63/42.63 % (3513234)------------------------------ % 300.63/42.63 % (3513236)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=318845922:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2748 on theBenchmark for (2748ds/1738Mi) % 300.63/42.63 % (3513236)Instruction limit reached! % 300.63/42.63 % (3513236)------------------------------ % 300.63/42.63 % (3513236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3513236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3513236)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3513236)Termination reason: Instruction limit % 300.63/42.63 % (3513236)Termination phase: Saturation % 300.63/42.64 % (3513236)Time elapsed: 0.576 s % 300.63/42.64 % (3513236)Peak memory usage: 19 MB % 300.63/42.64 % (3513236)Instructions burned: 1739 (million) % 300.63/42.64 % (3513238)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4056340425:i=10228:av=off:rtra=on_2743 on theBenchmark for (2743ds/10228Mi) % 300.63/42.64 % (3513176)Instruction limit reached! % 300.63/42.64 % (3513176)------------------------------ % 300.63/42.64 % (3513176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (3513176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (3513176)CaDiCaL version: 2.1.3 % 300.63/42.64 % (3513176)Termination reason: Instruction limit % 300.63/42.64 % (3513176)Termination phase: Saturation % 300.63/42.64 % (3513176)Time elapsed: 12.730 s % 300.63/42.64 % (3513176)Peak memory usage: 31 MB % 300.63/42.64 % (3513176)Instructions burned: 28120 (million) % 300.63/42.64 % (3513241)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1778445377:i=108564:rtra=on_2717 on theBenchmark for (2717ds/108564Mi) % 300.63/42.64 % (3513241)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.63/42.64 % (3513241)Terminated due to inappropriate strategy. % 300.63/42.64 % (3513241)------------------------------ % 300.63/42.64 % (3513241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (3513241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (3513241)CaDiCaL version: 2.1.3 % 300.63/42.64 % (3513241)Termination reason: Inappropriate % 300.63/42.64 % (3513241)Time elapsed: 0.002 s % 300.63/42.64 % (3513241)Peak memory usage: 10 MB % 300.63/42.64 % (3513241)Instructions burned: 2 (million) % 300.63/42.64 % (3513241)------------------------------ % 300.63/42.64 % (3513241)------------------------------ % 300.63/42.64 % (3513243)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3994082086:i=7024:aac=none:rtra=on_2717 on theBenchmark for (2717ds/7024Mi) % 300.63/42.64 % (3513238)Instruction limit reached! % 300.63/42.64 % (3513238)------------------------------ % 300.63/42.64 % (3513238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (3513238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (3513238)CaDiCaL version: 2.1.3 % 300.63/42.64 % (3513238)Termination reason: Instruction limit % 300.63/42.64 % (3513238)Termination phase: Saturation % 300.63/42.64 % (3513238)Time elapsed: 3.852 s % 300.63/42.64 % (3513238)Peak memory usage: 52 MB % 300.63/42.64 % (3513238)Instructions burned: 10230 (million) % 300.63/42.64 % (3513245)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1104048514:i=7546:rtra=on:amm=off_2704 on theBenchmark for (2704ds/7546Mi) % 300.63/42.64 % (3513245)Instruction limit reached! % 300.63/42.64 % (3513245)------------------------------ % 300.63/42.64 % (3513245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (3513245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (3513245)CaDiCaL version: 2.1.3 % 300.63/42.64 % (3513245)Termination reason: Instruction limit % 300.63/42.64 % (3513245)Termination phase: Saturation % 300.63/42.64 % (3513245)Time elapsed: 2.205 s % 300.63/42.64 % (3513245)Peak memory usage: 40 MB % 300.63/42.64 % (3513245)Instructions burned: 7550 (million) % 300.63/42.64 % (3513247)ott+11_1_sil=16000:si=on:gs=on:random_seed=2802595622:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2681 on theBenchmark % 300.63/42.64 Terminated % 300.63/42.64 % Vampire exiting % 300.63/42.64 Terminated %------------------------------------------------------------------------------