%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX134_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:46:32 PM UTC 2026 % Result : Timeout 300.28s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX134_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.27 % Computer : n013.cluster.edu % 0.10/0.27 % Model : x86_64 x86_64 % 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.27 % Memory : 8046.5625MB % 0.10/0.27 % OS : Linux 6.8.0-71-generic % 0.10/0.27 % CPULimit : 300 % 0.10/0.27 % WCLimit : 300 % 0.10/0.27 % DateTime : Mon Sep 28 15:02:36 UTC 2026 % 0.10/0.27 % CPUTime : % 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.27/0.32 Running first-order model finding % 0.27/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.15/1.30 % (1250425)Will run a generic schedule for satisfiability detection. % 6.15/1.30 % (1250434)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=463049222:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 6.15/1.30 % (1250433)% WARNING: option uhcvi not known. % 6.15/1.30 % (1250433)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3512772309:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 6.15/1.30 % (1250435)dis+10_1_sil=32000:sp=arity:random_seed=1760260696:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 6.15/1.30 % (1250436)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2121495248:i=116_2998 on theBenchmark for (2998ds/116Mi) % 6.15/1.30 % (1250432)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1584593370_2998 on theBenchmark for (2998ds/0Mi) % 6.15/1.30 % (1250437)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1431566703:i=131_2998 on theBenchmark for (2998ds/131Mi) % 6.15/1.30 % (1250438)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2865244829:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 6.15/1.31 % (1250435)Instruction limit reached! % 6.15/1.31 % (1250435)------------------------------ % 6.15/1.31 % (1250435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.31 % (1250435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.31 % (1250435)CaDiCaL version: 2.1.3 % 6.15/1.31 % (1250435)Termination reason: Instruction limit % 6.15/1.31 % (1250435)Termination phase: Property scanning % 6.15/1.31 % (1250435)Time elapsed: 0.057 s % 6.15/1.31 % (1250435)Peak memory usage: 10 MB % 6.15/1.31 % (1250435)Instructions burned: 103 (million) % 6.15/1.31 % (1250448)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1315445108:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 6.15/1.31 % (1250436)Instruction limit reached! % 6.15/1.31 % (1250436)------------------------------ % 6.15/1.31 % (1250436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.31 % (1250436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.31 % (1250436)CaDiCaL version: 2.1.3 % 6.15/1.31 % (1250436)Termination reason: Instruction limit % 6.15/1.31 % (1250436)Termination phase: Property scanning % 6.15/1.31 % (1250436)Time elapsed: 0.094 s % 6.15/1.31 % (1250436)Peak memory usage: 10 MB % 6.15/1.31 % (1250436)Instructions burned: 116 (million) % 6.15/1.31 % (1250432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.15/1.31 % (1250432)Terminated due to inappropriate strategy. % 6.15/1.31 % (1250432)------------------------------ % 6.15/1.31 % (1250432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.31 % (1250432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.31 % (1250432)CaDiCaL version: 2.1.3 % 6.15/1.31 % (1250432)Termination reason: Inappropriate % 6.15/1.31 % (1250432)Time elapsed: 0.096 s % 6.15/1.31 % (1250432)Peak memory usage: 10 MB % 6.15/1.31 % (1250432)Instructions burned: 118 (million) % 6.15/1.31 % (1250432)------------------------------ % 6.15/1.31 % (1250432)------------------------------ % 6.15/1.31 % (1250437)Instruction limit reached! % 6.15/1.31 % (1250437)------------------------------ % 6.15/1.31 % (1250437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.31 % (1250437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.31 % (1250437)CaDiCaL version: 2.1.3 % 6.15/1.31 % (1250437)Termination reason: Instruction limit % 6.15/1.31 % (1250437)Termination phase: Saturation % 6.15/1.31 % (1250437)Time elapsed: 0.103 s % 6.15/1.31 % (1250437)Peak memory usage: 11 MB % 6.15/1.31 % (1250437)Instructions burned: 131 (million) % 6.15/1.31 % (1250451)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3014845988:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 6.15/1.31 % (1250438)Instruction limit reached! % 6.15/1.31 % (1250438)------------------------------ % 6.15/1.31 % (1250438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.15/1.31 % (1250438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.31 % (1250438)CaDiCaL version: 2.1.3 % 6.15/1.31 % (1250438)Termination reason: Instruction limit % 6.15/1.31 % (1250438)Termination phase: Saturation % 6.15/1.31 % (1250438)Time elapsed: 0.126 s % 6.15/1.31 % (1250438)Peak memory usage: 12 MB % 7.47/1.65 % (1250438)Instructions burned: 160 (million) % 7.47/1.65 % (1250452)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=1792926624:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 7.47/1.65 % (1250453)ott-21_1_sil=16000:fs=off:random_seed=3411182406:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 7.47/1.65 % (1250455)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=324093208:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 7.47/1.65 % (1250448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.47/1.65 % (1250448)Terminated due to inappropriate strategy. % 7.47/1.65 % (1250448)------------------------------ % 7.47/1.65 % (1250448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.65 % (1250448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.65 % (1250448)CaDiCaL version: 2.1.3 % 7.47/1.65 % (1250448)Termination reason: Inappropriate % 7.47/1.65 % (1250448)Time elapsed: 0.083 s % 7.47/1.66 % (1250448)Peak memory usage: 10 MB % 7.47/1.66 % (1250448)Instructions burned: 118 (million) % 7.47/1.66 % (1250448)------------------------------ % 7.47/1.66 % (1250448)------------------------------ % 7.47/1.66 % (1250451)Instruction limit reached! % 7.47/1.66 % (1250451)------------------------------ % 7.47/1.66 % (1250451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.66 % (1250451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.66 % (1250451)CaDiCaL version: 2.1.3 % 7.47/1.66 % (1250451)Termination reason: Instruction limit % 7.47/1.66 % (1250451)Termination phase: Saturation % 7.47/1.66 % (1250451)Time elapsed: 0.074 s % 7.47/1.66 % (1250451)Peak memory usage: 12 MB % 7.47/1.66 % (1250451)Instructions burned: 131 (million) % 7.47/1.66 % (1250459)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3267202305:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 7.47/1.66 % (1250460)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3216513879:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 7.47/1.66 % (1250459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.47/1.66 % (1250459)Terminated due to inappropriate strategy. % 7.47/1.66 % (1250459)------------------------------ % 7.47/1.66 % (1250459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.66 % (1250459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.66 % (1250459)CaDiCaL version: 2.1.3 % 7.47/1.66 % (1250459)Termination reason: Inappropriate % 7.47/1.66 % (1250459)Time elapsed: 0.073 s % 7.47/1.66 % (1250459)Peak memory usage: 10 MB % 7.47/1.66 % (1250459)Instructions burned: 89 (million) % 7.47/1.66 % (1250459)------------------------------ % 7.47/1.66 % (1250459)------------------------------ % 7.47/1.66 % (1250453)Instruction limit reached! % 7.47/1.66 % (1250453)------------------------------ % 7.47/1.66 % (1250453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.66 % (1250453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.66 % (1250453)CaDiCaL version: 2.1.3 % 7.47/1.66 % (1250453)Termination reason: Instruction limit % 7.47/1.66 % (1250453)Termination phase: Saturation % 7.47/1.66 % (1250453)Time elapsed: 0.144 s % 7.47/1.66 % (1250453)Peak memory usage: 11 MB % 7.47/1.66 % (1250453)Instructions burned: 181 (million) % 7.47/1.66 % (1250463)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3389741634:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 7.47/1.66 % (1250465)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=842255381:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 7.47/1.66 % (1250463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.47/1.66 % (1250463)Terminated due to inappropriate strategy. % 7.47/1.66 % (1250463)------------------------------ % 7.47/1.66 % (1250463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.66 % (1250463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.66 % (1250463)CaDiCaL version: 2.1.3 % 7.47/1.66 % (1250463)Termination reason: Inappropriate % 7.47/1.66 % (1250463)Time elapsed: 0.062 s % 7.47/1.66 % (1250463)Peak memory usage: 10 MB % 30.88/4.92 % (1250463)Instructions burned: 89 (million) % 30.88/4.92 % (1250463)------------------------------ % 30.88/4.92 % (1250463)------------------------------ % 30.88/4.92 % (1250468)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3765176624:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 30.88/4.92 % (1250455)Instruction limit reached! % 30.88/4.92 % (1250455)------------------------------ % 30.88/4.92 % (1250455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.88/4.92 % (1250455)CaDiCaL version: 2.1.3 % 30.88/4.92 % (1250455)Termination reason: Instruction limit % 30.88/4.92 % (1250455)Termination phase: Saturation % 30.88/4.92 % (1250455)Time elapsed: 0.314 s % 30.88/4.92 % (1250455)Peak memory usage: 13 MB % 30.88/4.92 % (1250455)Instructions burned: 478 (million) % 30.88/4.92 % (1250470)fmb+10_1_sil=64000:random_seed=27489127:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 30.88/4.92 % (1250470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.88/4.92 % (1250470)Terminated due to inappropriate strategy. % 30.88/4.92 % (1250470)------------------------------ % 30.88/4.92 % (1250470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.88/4.92 % (1250470)CaDiCaL version: 2.1.3 % 30.88/4.92 % (1250470)Termination reason: Inappropriate % 30.88/4.92 % (1250470)Time elapsed: 0.089 s % 30.88/4.92 % (1250470)Peak memory usage: 10 MB % 30.88/4.92 % (1250470)Instructions burned: 118 (million) % 30.88/4.92 % (1250470)------------------------------ % 30.88/4.92 % (1250470)------------------------------ % 30.88/4.92 % (1250472)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4106184480:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 30.88/4.92 % (1250452)Instruction limit reached! % 30.88/4.92 % (1250452)------------------------------ % 30.88/4.92 % (1250452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.88/4.92 % (1250452)CaDiCaL version: 2.1.3 % 30.88/4.92 % (1250452)Termination reason: Instruction limit % 30.88/4.92 % (1250452)Termination phase: Saturation % 30.88/4.92 % (1250452)Time elapsed: 0.521 s % 30.88/4.92 % (1250452)Peak memory usage: 15 MB % 30.88/4.92 % (1250452)Instructions burned: 685 (million) % 30.88/4.92 % (1250472)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.88/4.92 % (1250472)Terminated due to inappropriate strategy. % 30.88/4.92 % (1250472)------------------------------ % 30.88/4.92 % (1250472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.88/4.92 % (1250472)CaDiCaL version: 2.1.3 % 30.88/4.92 % (1250472)Termination reason: Inappropriate % 30.88/4.92 % (1250472)Time elapsed: 0.073 s % 30.88/4.92 % (1250472)Peak memory usage: 10 MB % 30.88/4.92 % (1250472)Instructions burned: 118 (million) % 30.88/4.92 % (1250472)------------------------------ % 30.88/4.92 % (1250472)------------------------------ % 30.88/4.92 % (1250474)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1926330238:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 30.88/4.92 % (1250475)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3597399752:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 30.88/4.92 % (1250474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.88/4.92 % (1250474)Terminated due to inappropriate strategy. % 30.88/4.92 % (1250474)------------------------------ % 30.88/4.92 % (1250474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.88/4.92 % (1250474)CaDiCaL version: 2.1.3 % 30.88/4.92 % (1250474)Termination reason: Inappropriate % 30.88/4.92 % (1250474)Time elapsed: 0.110 s % 30.88/4.92 % (1250474)Peak memory usage: 10 MB % 30.88/4.92 % (1250474)Instructions burned: 118 (million) % 30.88/4.92 % (1250474)------------------------------ % 30.88/4.92 % (1250474)------------------------------ % 30.88/4.92 % (1250465)Instruction limit reached! % 30.88/4.92 % (1250465)------------------------------ % 30.88/4.92 % (1250465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.88/4.92 % (1250465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250465)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250465)Termination reason: Instruction limit % 33.70/5.29 % (1250465)Termination phase: Saturation % 33.70/5.29 % (1250465)Time elapsed: 0.491 s % 33.70/5.29 % (1250465)Peak memory usage: 17 MB % 33.70/5.29 % (1250465)Instructions burned: 693 (million) % 33.70/5.29 % (1250478)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2149637197:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 33.70/5.29 % (1250479)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3455453282:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 33.70/5.29 % (1250479)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.70/5.29 % (1250479)Terminated due to inappropriate strategy. % 33.70/5.29 % (1250479)------------------------------ % 33.70/5.29 % (1250479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.70/5.29 % (1250479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250479)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250479)Termination reason: Inappropriate % 33.70/5.29 % (1250479)Time elapsed: 0.107 s % 33.70/5.29 % (1250479)Peak memory usage: 11 MB % 33.70/5.29 % (1250479)Instructions burned: 118 (million) % 33.70/5.29 % (1250479)------------------------------ % 33.70/5.29 % (1250479)------------------------------ % 33.70/5.29 % (1250483)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4172487148:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 33.70/5.29 % (1250460)Instruction limit reached! % 33.70/5.29 % (1250460)------------------------------ % 33.70/5.29 % (1250460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.70/5.29 % (1250460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250460)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250460)Termination reason: Instruction limit % 33.70/5.29 % (1250460)Termination phase: Saturation % 33.70/5.29 % (1250460)Time elapsed: 0.798 s % 33.70/5.29 % (1250460)Peak memory usage: 16 MB % 33.70/5.29 % (1250460)Instructions burned: 1179 (million) % 33.70/5.29 % (1250468)Instruction limit reached! % 33.70/5.29 % (1250468)------------------------------ % 33.70/5.29 % (1250468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.70/5.29 % (1250468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250468)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250468)Termination reason: Instruction limit % 33.70/5.29 % (1250468)Termination phase: Saturation % 33.70/5.29 % (1250468)Time elapsed: 0.638 s % 33.70/5.29 % (1250468)Peak memory usage: 14 MB % 33.70/5.29 % (1250468)Instructions burned: 880 (million) % 33.70/5.29 % (1250485)ott-2_1_sil=16000:newcnf=on:random_seed=2741017435:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 33.70/5.29 % (1250486)ott+10_1_sil=32000:tgt=ground:random_seed=3533929676:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 33.70/5.29 % (1250483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.70/5.29 % (1250483)Terminated due to inappropriate strategy. % 33.70/5.29 % (1250483)------------------------------ % 33.70/5.29 % (1250483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.70/5.29 % (1250483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250483)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250483)Termination reason: Inappropriate % 33.70/5.29 % (1250483)Time elapsed: 0.071 s % 33.70/5.29 % (1250483)Peak memory usage: 10 MB % 33.70/5.29 % (1250483)Instructions burned: 118 (million) % 33.70/5.29 % (1250483)------------------------------ % 33.70/5.29 % (1250483)------------------------------ % 33.70/5.29 % (1250489)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2510766592:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 33.70/5.29 % (1250489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.70/5.29 % (1250489)Terminated due to inappropriate strategy. % 33.70/5.29 % (1250489)------------------------------ % 33.70/5.29 % (1250489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.70/5.29 % (1250489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.70/5.29 % (1250489)CaDiCaL version: 2.1.3 % 33.70/5.29 % (1250489)Termination reason: Inappropriate % 33.70/5.29 % (1250489)Time elapsed: 0.074 s % 33.70/5.29 % (1250489)Peak memory usage: 10 MB % 33.70/5.29 % (1250489)Instructions burned: 118 (million) % 144.04/20.74 % (1250489)------------------------------ % 144.04/20.74 % (1250489)------------------------------ % 144.04/20.74 % (1250491)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1601776184:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 144.04/20.74 % (1250485)Instruction limit reached! % 144.04/20.74 % (1250485)------------------------------ % 144.04/20.74 % (1250485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250485)CaDiCaL version: 2.1.3 % 144.04/20.74 % (1250485)Termination reason: Instruction limit % 144.04/20.74 % (1250485)Termination phase: Saturation % 144.04/20.74 % (1250485)Time elapsed: 0.771 s % 144.04/20.74 % (1250485)Peak memory usage: 19 MB % 144.04/20.74 % (1250485)Instructions burned: 869 (million) % 144.04/20.74 % (1250497)dis+21_1_sil=32000:sas=cadical:random_seed=2888691235:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 144.04/20.74 % (1250478)Instruction limit reached! % 144.04/20.74 % (1250478)------------------------------ % 144.04/20.74 % (1250478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250478)CaDiCaL version: 2.1.3 % 144.04/20.74 % (1250478)Termination reason: Instruction limit % 144.04/20.74 % (1250478)Termination phase: Saturation % 144.04/20.74 % (1250478)Time elapsed: 1.030 s % 144.04/20.74 % (1250478)Peak memory usage: 15 MB % 144.04/20.74 % (1250478)Instructions burned: 1472 (million) % 144.04/20.74 % (1250499)ott+11_1_sil=16000:gs=on:random_seed=1070400480:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 144.04/20.74 % (1250499)Instruction limit reached! % 144.04/20.74 % (1250499)------------------------------ % 144.04/20.74 % (1250499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250499)CaDiCaL version: 2.1.3 % 144.04/20.74 % (1250499)Termination reason: Instruction limit % 144.04/20.74 % (1250499)Termination phase: Saturation % 144.04/20.74 % (1250499)Time elapsed: 1.488 s % 144.04/20.74 % (1250499)Peak memory usage: 15 MB % 144.04/20.74 % (1250499)Instructions burned: 2252 (million) % 144.04/20.74 % (1250507)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4005802499:fmbsr=1.6:i=67534_2964 on theBenchmark for (2964ds/67534Mi) % 144.04/20.74 % (1250507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.04/20.74 % (1250507)Terminated due to inappropriate strategy. % 144.04/20.74 % (1250507)------------------------------ % 144.04/20.74 % (1250507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250507)CaDiCaL version: 2.1.3 % 144.04/20.74 % (1250507)Termination reason: Inappropriate % 144.04/20.74 % (1250507)Time elapsed: 0.059 s % 144.04/20.74 % (1250507)Peak memory usage: 10 MB % 144.04/20.74 % (1250507)Instructions burned: 118 (million) % 144.04/20.74 % (1250507)------------------------------ % 144.04/20.74 % (1250507)------------------------------ % 144.04/20.74 % (1250510)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1469403403:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2963 on theBenchmark for (2963ds/4591Mi) % 144.04/20.74 % (1250491)Instruction limit reached! % 144.04/20.74 % (1250491)------------------------------ % 144.04/20.74 % (1250491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250491)CaDiCaL version: 2.1.3 % 144.04/20.74 % (1250491)Termination reason: Instruction limit % 144.04/20.74 % (1250491)Termination phase: Saturation % 144.04/20.74 % (1250491)Time elapsed: 2.333 s % 144.04/20.74 % (1250491)Peak memory usage: 15 MB % 144.04/20.74 % (1250491)Instructions burned: 3512 (million) % 144.04/20.74 % (1250512)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3324011839:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 144.04/20.74 % (1250475)Instruction limit reached! % 144.04/20.74 % (1250475)------------------------------ % 144.04/20.74 % (1250475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.04/20.74 % (1250475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.04/20.74 % (1250475)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250475)Termination reason: Instruction limit % 173.06/24.88 % (1250475)Termination phase: Saturation % 173.06/24.88 % (1250475)Time elapsed: 3.720 s % 173.06/24.88 % (1250475)Peak memory usage: 15 MB % 173.06/24.88 % (1250475)Instructions burned: 5132 (million) % 173.06/24.88 % (1250516)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=50407345:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 173.06/24.88 % (1250497)Instruction limit reached! % 173.06/24.88 % (1250497)------------------------------ % 173.06/24.88 % (1250497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.06/24.88 % (1250497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/24.88 % (1250497)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250497)Termination reason: Instruction limit % 173.06/24.88 % (1250497)Termination phase: Saturation % 173.06/24.88 % (1250497)Time elapsed: 2.692 s % 173.06/24.88 % (1250497)Peak memory usage: 15 MB % 173.06/24.88 % (1250497)Instructions burned: 3773 (million) % 173.06/24.88 % (1250518)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3744202508:i=5497:nm=2_2952 on theBenchmark for (2952ds/5497Mi) % 173.06/24.88 % (1250486)Instruction limit reached! % 173.06/24.88 % (1250486)------------------------------ % 173.06/24.88 % (1250486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.06/24.88 % (1250486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/24.88 % (1250486)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250486)Termination reason: Instruction limit % 173.06/24.88 % (1250486)Termination phase: Saturation % 173.06/24.88 % (1250486)Time elapsed: 3.562 s % 173.06/24.88 % (1250486)Peak memory usage: 15 MB % 173.06/24.88 % (1250486)Instructions burned: 5114 (million) % 173.06/24.88 % (1250518)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.06/24.88 % (1250518)Terminated due to inappropriate strategy. % 173.06/24.88 % (1250518)------------------------------ % 173.06/24.88 % (1250518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.06/24.88 % (1250518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/24.88 % (1250518)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250518)Termination reason: Inappropriate % 173.06/24.88 % (1250518)Time elapsed: 0.062 s % 173.06/24.88 % (1250518)Peak memory usage: 10 MB % 173.06/24.88 % (1250518)Instructions burned: 118 (million) % 173.06/24.88 % (1250518)------------------------------ % 173.06/24.88 % (1250518)------------------------------ % 173.06/24.88 % (1250521)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3479801469:fmbsr=2:i=46332_2952 on theBenchmark for (2952ds/46332Mi) % 173.06/24.88 % (1250522)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1798716979:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 173.06/24.88 % (1250521)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.06/24.88 % (1250521)Terminated due to inappropriate strategy. % 173.06/24.88 % (1250521)------------------------------ % 173.06/24.88 % (1250521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.06/24.88 % (1250521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/24.88 % (1250521)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250521)Termination reason: Inappropriate % 173.06/24.88 % (1250521)Time elapsed: 0.097 s % 173.06/24.88 % (1250521)Peak memory usage: 10 MB % 173.06/24.88 % (1250521)Instructions burned: 118 (million) % 173.06/24.88 % (1250521)------------------------------ % 173.06/24.88 % (1250521)------------------------------ % 173.06/24.88 % (1250522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.06/24.88 % (1250522)Terminated due to inappropriate strategy. % 173.06/24.88 % (1250522)------------------------------ % 173.06/24.88 % (1250522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.06/24.88 % (1250522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/24.88 % (1250522)CaDiCaL version: 2.1.3 % 173.06/24.88 % (1250522)Termination reason: Inappropriate % 173.06/24.88 % (1250522)Time elapsed: 0.075 s % 173.06/24.88 % (1250522)Peak memory usage: 10 MB % 173.06/24.88 % (1250522)Instructions burned: 118 (million) % 173.06/24.88 % (1250522)------------------------------ % 173.06/24.88 % (1250522)------------------------------ % 173.06/24.88 % (1250525)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1233303407:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi) % 173.06/24.88 % (1250526)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1391908692:i=8173:av=off_2950 on theBenchmark for (2950ds/8173Mi) % 177.43/25.41 % (1250510)Instruction limit reached! % 177.43/25.41 % (1250510)------------------------------ % 177.43/25.41 % (1250510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250510)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250510)Termination reason: Instruction limit % 177.43/25.41 % (1250510)Termination phase: Saturation % 177.43/25.41 % (1250510)Time elapsed: 4.325 s % 177.43/25.41 % (1250510)Peak memory usage: 41 MB % 177.43/25.41 % (1250510)Instructions burned: 4592 (million) % 177.43/25.41 % (1250536)dis+10_16:1_sil=16000:random_seed=4003490870:i=9155:fsr=off_2920 on theBenchmark for (2920ds/9155Mi) % 177.43/25.41 % (1250516)Instruction limit reached! % 177.43/25.41 % (1250516)------------------------------ % 177.43/25.41 % (1250516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250516)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250516)Termination reason: Instruction limit % 177.43/25.41 % (1250516)Termination phase: Saturation % 177.43/25.41 % (1250516)Time elapsed: 3.762 s % 177.43/25.41 % (1250516)Peak memory usage: 17 MB % 177.43/25.41 % (1250516)Instructions burned: 5212 (million) % 177.43/25.41 % (1250540)ott-3_8_sil=64000:random_seed=2382886515:i=20139:bs=on_2916 on theBenchmark for (2916ds/20139Mi) % 177.43/25.41 % (1250526)Instruction limit reached! % 177.43/25.41 % (1250526)------------------------------ % 177.43/25.41 % (1250526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250526)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250526)Termination reason: Instruction limit % 177.43/25.41 % (1250526)Termination phase: Saturation % 177.43/25.41 % (1250526)Time elapsed: 5.685 s % 177.43/25.41 % (1250526)Peak memory usage: 16 MB % 177.43/25.41 % (1250526)Instructions burned: 8174 (million) % 177.43/25.41 % (1250542)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2926133968:fmbsr=2:i=32576_2893 on theBenchmark for (2893ds/32576Mi) % 177.43/25.41 % (1250542)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.43/25.41 % (1250542)Terminated due to inappropriate strategy. % 177.43/25.41 % (1250542)------------------------------ % 177.43/25.41 % (1250542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250542)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250542)Termination reason: Inappropriate % 177.43/25.41 % (1250542)Time elapsed: 0.080 s % 177.43/25.41 % (1250542)Peak memory usage: 11 MB % 177.43/25.41 % (1250542)Instructions burned: 118 (million) % 177.43/25.41 % (1250542)------------------------------ % 177.43/25.41 % (1250542)------------------------------ % 177.43/25.41 % (1250544)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4000398107:i=11404_2892 on theBenchmark for (2892ds/11404Mi) % 177.43/25.41 % (1250536)Instruction limit reached! % 177.43/25.41 % (1250536)------------------------------ % 177.43/25.41 % (1250536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250536)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250536)Termination reason: Instruction limit % 177.43/25.41 % (1250536)Termination phase: Saturation % 177.43/25.41 % (1250536)Time elapsed: 6.517 s % 177.43/25.41 % (1250536)Peak memory usage: 16 MB % 177.43/25.41 % (1250536)Instructions burned: 9155 (million) % 177.43/25.41 % (1250546)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=647375553:i=14134_2854 on theBenchmark for (2854ds/14134Mi) % 177.43/25.41 % (1250544)Instruction limit reached! % 177.43/25.41 % (1250544)------------------------------ % 177.43/25.41 % (1250544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.43/25.41 % (1250544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.43/25.41 % (1250544)CaDiCaL version: 2.1.3 % 177.43/25.41 % (1250544)Termination reason: Instruction limit % 177.43/25.41 % (1250544)Termination phase: Saturation % 177.43/25.41 % (1250544)Time elapsed: 8.031 s % 177.43/25.41 % (1250544)Peak memory usage: 16 MB % 177.43/25.41 % (1250544)Instructions burned: 11405 (million) % 177.43/25.41 % (1250559)dis+33_16_sil=32000:sac=on:random_seed=1552229922:i=15851:nm=0_2811 on theBenchmark for (2811ds/15851Mi) % 177.43/25.41 % (1250525)Instruction limit reached! % 177.43/25.41 % (1250525)------------------------------ % 218.18/31.20 % (1250525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250525)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250525)Termination reason: Instruction limit % 218.18/31.20 % (1250525)Termination phase: Saturation % 218.18/31.20 % (1250525)Time elapsed: 15.464 s % 218.18/31.20 % (1250525)Peak memory usage: 17 MB % 218.18/31.20 % (1250525)Instructions burned: 22566 (million) % 218.18/31.20 % (1250566)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2248539979:avsq=on:i=17627:add=on:amm=off_2795 on theBenchmark for (2795ds/17627Mi) % 218.18/31.20 % (1250540)Instruction limit reached! % 218.18/31.20 % (1250540)------------------------------ % 218.18/31.20 % (1250540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250540)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250540)Termination reason: Instruction limit % 218.18/31.20 % (1250540)Termination phase: Saturation % 218.18/31.20 % (1250540)Time elapsed: 14.113 s % 218.18/31.20 % (1250540)Peak memory usage: 18 MB % 218.18/31.20 % (1250540)Instructions burned: 20140 (million) % 218.18/31.20 % (1250569)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3832236638:s2a=on:i=53295_2774 on theBenchmark for (2774ds/53295Mi) % 218.18/31.20 % (1250512)Instruction limit reached! % 218.18/31.20 % (1250512)------------------------------ % 218.18/31.20 % (1250512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250512)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250512)Termination reason: Instruction limit % 218.18/31.20 % (1250512)Termination phase: Saturation % 218.18/31.20 % (1250512)Time elapsed: 20.530 s % 218.18/31.20 % (1250512)Peak memory usage: 15 MB % 218.18/31.20 % (1250512)Instructions burned: 29340 (million) % 218.18/31.20 % (1250573)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4185133285:i=26857:ins=20_2757 on theBenchmark for (2757ds/26857Mi) % 218.18/31.20 % (1250573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.18/31.20 % (1250573)Terminated due to inappropriate strategy. % 218.18/31.20 % (1250573)------------------------------ % 218.18/31.20 % (1250573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250573)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250573)Termination reason: Inappropriate % 218.18/31.20 % (1250573)Time elapsed: 0.059 s % 218.18/31.20 % (1250573)Peak memory usage: 10 MB % 218.18/31.20 % (1250573)Instructions burned: 118 (million) % 218.18/31.20 % (1250573)------------------------------ % 218.18/31.20 % (1250573)------------------------------ % 218.18/31.20 % (1250575)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3300026253:i=28120:bs=on:fsr=off_2756 on theBenchmark for (2756ds/28120Mi) % 218.18/31.20 % (1250546)Instruction limit reached! % 218.18/31.20 % (1250546)------------------------------ % 218.18/31.20 % (1250546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250546)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250546)Termination reason: Instruction limit % 218.18/31.20 % (1250546)Termination phase: Saturation % 218.18/31.20 % (1250546)Time elapsed: 9.821 s % 218.18/31.20 % (1250546)Peak memory usage: 16 MB % 218.18/31.20 % (1250546)Instructions burned: 14135 (million) % 218.18/31.20 % (1250577)fmb+10_1_sil=256000:fmbss=7:random_seed=4240924000:fmbsr=1.6:i=182295_2756 on theBenchmark for (2756ds/182295Mi) % 218.18/31.20 % (1250577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.18/31.20 % (1250577)Terminated due to inappropriate strategy. % 218.18/31.20 % (1250577)------------------------------ % 218.18/31.20 % (1250577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.18/31.20 % (1250577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.18/31.20 % (1250577)CaDiCaL version: 2.1.3 % 218.18/31.20 % (1250577)Termination reason: Inappropriate % 218.18/31.20 % (1250577)Time elapsed: 0.099 s % 218.18/31.20 % (1250577)Peak memory usage: 10 MB % 218.18/31.20 % (1250577)Instructions burned: 118 (million) % 218.18/31.20 % (1250577)------------------------------ % 218.18/31.20 % (1250577)------------------------------ % 218.18/31.20 % (1250579)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4128648059:i=44625:gsp=on_2754 on theBenchmark for (2754ds/44625Mi) % 222.82/31.88 % (1250579)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.82/31.88 % (1250579)Terminated due to inappropriate strategy. % 222.82/31.88 % (1250579)------------------------------ % 222.82/31.88 % (1250579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.82/31.88 % (1250579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.82/31.88 % (1250579)CaDiCaL version: 2.1.3 % 222.82/31.88 % (1250579)Termination reason: Inappropriate % 222.82/31.88 % (1250579)Time elapsed: 0.054 s % 222.82/31.88 % (1250579)Peak memory usage: 11 MB % 222.82/31.88 % (1250579)Instructions burned: 118 (million) % 222.82/31.88 % (1250579)------------------------------ % 222.82/31.88 % (1250579)------------------------------ % 222.82/31.88 % (1250581)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2092978562:i=160505_2753 on theBenchmark for (2753ds/160505Mi) % 222.82/31.88 % (1250581)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.82/31.88 % (1250581)Terminated due to inappropriate strategy. % 222.82/31.88 % (1250581)------------------------------ % 222.82/31.88 % (1250581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.82/31.88 % (1250581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.82/31.88 % (1250581)CaDiCaL version: 2.1.3 % 222.82/31.88 % (1250581)Termination reason: Inappropriate % 222.82/31.88 % (1250581)Time elapsed: 0.057 s % 222.82/31.88 % (1250581)Peak memory usage: 10 MB % 222.82/31.88 % (1250581)Instructions burned: 118 (million) % 222.82/31.88 % (1250581)------------------------------ % 222.82/31.88 % (1250581)------------------------------ % 222.82/31.88 % (1250583)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=896520396:fmbsr=1.3:i=225729_2753 on theBenchmark for (2753ds/225729Mi) % 222.82/31.88 % (1250583)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.82/31.88 % (1250583)Terminated due to inappropriate strategy. % 222.82/31.88 % (1250583)------------------------------ % 222.82/31.88 % (1250583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.82/31.88 % (1250583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.82/31.88 % (1250583)CaDiCaL version: 2.1.3 % 222.82/31.88 % (1250583)Termination reason: Inappropriate % 222.82/31.88 % (1250583)Time elapsed: 0.110 s % 222.82/31.88 % (1250583)Peak memory usage: 11 MB % 222.82/31.88 % (1250583)Instructions burned: 118 (million) % 222.82/31.88 % (1250583)------------------------------ % 222.82/31.88 % (1250583)------------------------------ % 222.82/31.88 % (1250585)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=563898089:fmbsr=2:i=185024:ins=7_2751 on theBenchmark for (2751ds/185024Mi) % 222.82/31.88 % (1250585)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.82/31.88 % (1250585)Terminated due to inappropriate strategy. % 222.82/31.88 % (1250585)------------------------------ % 222.82/31.88 % (1250585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.82/31.88 % (1250585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.82/31.88 % (1250585)CaDiCaL version: 2.1.3 % 222.82/31.88 % (1250585)Termination reason: Inappropriate % 222.82/31.88 % (1250585)Time elapsed: 0.059 s % 222.82/31.88 % (1250585)Peak memory usage: 10 MB % 222.82/31.88 % (1250585)Instructions burned: 118 (million) % 222.82/31.88 % (1250585)------------------------------ % 222.82/31.88 % (1250585)------------------------------ % 222.82/31.88 % (1250587)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=488188122:rtra=on_2750 on theBenchmark for (2750ds/0Mi) % 222.82/31.88 % (1250587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.82/31.88 % (1250587)Terminated due to inappropriate strategy. % 222.82/31.88 % (1250587)------------------------------ % 222.82/31.88 % (1250587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.82/31.88 % (1250587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.82/31.88 % (1250587)CaDiCaL version: 2.1.3 % 222.82/31.88 % (1250587)Termination reason: Inappropriate % 222.82/31.88 % (1250587)Time elapsed: 0.096 s % 222.82/31.88 % (1250587)Peak memory usage: 11 MB % 222.82/31.88 % (1250587)Instructions burned: 118 (million) % 222.82/31.88 % (1250587)------------------------------ % 222.82/31.88 % (1250587)------------------------------ % 222.82/31.88 % (1250591)% WARNING: option uhcvi not known. % 222.82/31.88 % (1250591)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1153724380:i=271062:add=off:rtra=on:rawr=on_2749 on theBenchmark for (2749ds/271062Mi) % 228.59/32.63 % (1250559)Instruction limit reached! % 228.59/32.63 % (1250559)------------------------------ % 228.59/32.63 % (1250559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250559)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250559)Termination reason: Instruction limit % 228.59/32.63 % (1250559)Termination phase: Saturation % 228.59/32.63 % (1250559)Time elapsed: 10.371 s % 228.59/32.63 % (1250559)Peak memory usage: 20 MB % 228.59/32.63 % (1250559)Instructions burned: 15854 (million) % 228.59/32.63 % (1250643)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3377595053:i=176048:add=on:rtra=on:rawr=on_2707 on theBenchmark for (2707ds/176048Mi) % 228.59/32.63 % (1250434)Instruction limit reached! % 228.59/32.63 % (1250434)------------------------------ % 228.59/32.63 % (1250434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250434)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250434)Termination reason: Instruction limit % 228.59/32.63 % (1250434)Termination phase: Saturation % 228.59/32.63 % (1250434)Time elapsed: 30.439 s % 228.59/32.63 % (1250434)Peak memory usage: 22 MB % 228.59/32.63 % (1250434)Instructions burned: 88028 (million) % 228.59/32.63 % (1250645)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3610258321:i=206:fgj=on:rtra=on_2694 on theBenchmark for (2694ds/206Mi) % 228.59/32.63 % (1250645)Instruction limit reached! % 228.59/32.63 % (1250645)------------------------------ % 228.59/32.63 % (1250645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250645)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250645)Termination reason: Instruction limit % 228.59/32.63 % (1250645)Termination phase: Saturation % 228.59/32.63 % (1250645)Time elapsed: 0.045 s % 228.59/32.63 % (1250645)Peak memory usage: 13 MB % 228.59/32.63 % (1250645)Instructions burned: 210 (million) % 228.59/32.63 % (1250647)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1666834120:i=232:rtra=on_2693 on theBenchmark for (2693ds/232Mi) % 228.59/32.63 % (1250647)Instruction limit reached! % 228.59/32.63 % (1250647)------------------------------ % 228.59/32.63 % (1250647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250647)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250647)Termination reason: Instruction limit % 228.59/32.63 % (1250647)Termination phase: Saturation % 228.59/32.63 % (1250647)Time elapsed: 0.048 s % 228.59/32.63 % (1250647)Peak memory usage: 12 MB % 228.59/32.63 % (1250647)Instructions burned: 233 (million) % 228.59/32.63 % (1250649)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1887276616:i=262:rtra=on_2692 on theBenchmark for (2692ds/262Mi) % 228.59/32.63 % (1250649)Instruction limit reached! % 228.59/32.63 % (1250649)------------------------------ % 228.59/32.63 % (1250649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250649)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250649)Termination reason: Instruction limit % 228.59/32.63 % (1250649)Termination phase: Saturation % 228.59/32.63 % (1250649)Time elapsed: 0.056 s % 228.59/32.63 % (1250649)Peak memory usage: 13 MB % 228.59/32.63 % (1250649)Instructions burned: 267 (million) % 228.59/32.63 % (1250651)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3329502918:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2692 on theBenchmark for (2692ds/318Mi) % 228.59/32.63 % (1250651)Instruction limit reached! % 228.59/32.63 % (1250651)------------------------------ % 228.59/32.63 % (1250651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.59/32.63 % (1250651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.59/32.63 % (1250651)CaDiCaL version: 2.1.3 % 228.59/32.63 % (1250651)Termination reason: Instruction limit % 228.59/32.63 % (1250651)Termination phase: Saturation % 228.59/32.63 % (1250651)Time elapsed: 0.074 s % 228.59/32.63 % (1250651)Peak memory usage: 14 MB % 228.59/32.63 % (1250651)Instructions burned: 322 (million) % 228.59/32.63 % (1250653)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=301716577:i=1428:nm=2:rtra=on_2691 on theBenchmark for (2691ds/1428Mi) % 234.27/33.49 % (1250653)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 234.27/33.49 % (1250653)Terminated due to inappropriate strategy. % 234.27/33.49 % (1250653)------------------------------ % 234.27/33.49 % (1250653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250653)CaDiCaL version: 2.1.3 % 234.27/33.49 % (1250653)Termination reason: Inappropriate % 234.27/33.49 % (1250653)Time elapsed: 0.024 s % 234.27/33.49 % (1250653)Peak memory usage: 10 MB % 234.27/33.49 % (1250653)Instructions burned: 118 (million) % 234.27/33.49 % (1250653)------------------------------ % 234.27/33.49 % (1250653)------------------------------ % 234.27/33.49 % (1250655)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3821600967:i=262:bd=preordered:rtra=on:fsd=on_2691 on theBenchmark for (2691ds/262Mi) % 234.27/33.49 % (1250655)Instruction limit reached! % 234.27/33.49 % (1250655)------------------------------ % 234.27/33.49 % (1250655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250655)CaDiCaL version: 2.1.3 % 234.27/33.49 % (1250655)Termination reason: Instruction limit % 234.27/33.49 % (1250655)Termination phase: Saturation % 234.27/33.49 % (1250655)Time elapsed: 0.058 s % 234.27/33.49 % (1250655)Peak memory usage: 14 MB % 234.27/33.49 % (1250655)Instructions burned: 262 (million) % 234.27/33.49 % (1250657)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=664373379:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2690 on theBenchmark for (2690ds/1368Mi) % 234.27/33.49 % (1250657)Instruction limit reached! % 234.27/33.49 % (1250657)------------------------------ % 234.27/33.49 % (1250657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250657)CaDiCaL version: 2.1.3 % 234.27/33.49 % (1250657)Termination reason: Instruction limit % 234.27/33.49 % (1250657)Termination phase: Saturation % 234.27/33.49 % (1250657)Time elapsed: 0.299 s % 234.27/33.49 % (1250657)Peak memory usage: 16 MB % 234.27/33.49 % (1250657)Instructions burned: 1373 (million) % 234.27/33.49 % (1250659)ott-21_1_sil=16000:si=on:fs=off:random_seed=4230182212:i=360:av=off:fsr=off:rtra=on_2687 on theBenchmark for (2687ds/360Mi) % 234.27/33.49 % (1250659)Instruction limit reached! % 234.27/33.49 % (1250659)------------------------------ % 234.27/33.49 % (1250659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250659)CaDiCaL version: 2.1.3 % 234.27/33.49 % (1250659)Termination reason: Instruction limit % 234.27/33.49 % (1250659)Termination phase: Saturation % 234.27/33.49 % (1250659)Time elapsed: 0.072 s % 234.27/33.49 % (1250659)Peak memory usage: 12 MB % 234.27/33.49 % (1250659)Instructions burned: 361 (million) % 234.27/33.49 % (1250661)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2326029955:i=954:bd=all:rtra=on_2686 on theBenchmark for (2686ds/954Mi) % 234.27/33.49 % (1250566)Instruction limit reached! % 234.27/33.49 % (1250566)------------------------------ % 234.27/33.49 % (1250566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250566)CaDiCaL version: 2.1.3 % 234.27/33.49 % (1250566)Termination reason: Instruction limit % 234.27/33.49 % (1250566)Termination phase: Saturation % 234.27/33.49 % (1250566)Time elapsed: 11.046 s % 234.27/33.49 % (1250566)Peak memory usage: 115 MB % 234.27/33.49 % (1250566)Instructions burned: 17628 (million) % 234.27/33.49 % (1250663)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3199599400:fmbsr=1.3:i=1730:ins=25:rtra=on_2684 on theBenchmark for (2684ds/1730Mi) % 234.27/33.49 % (1250663)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 234.27/33.49 % (1250663)Terminated due to inappropriate strategy. % 234.27/33.49 % (1250663)------------------------------ % 234.27/33.49 % (1250663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.27/33.49 % (1250663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.27/33.49 % (1250663)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250663)Termination reason: Inappropriate % 257.95/36.91 % (1250663)Time elapsed: 0.035 s % 257.95/36.91 % (1250663)Peak memory usage: 10 MB % 257.95/36.91 % (1250663)Instructions burned: 90 (million) % 257.95/36.91 % (1250663)------------------------------ % 257.95/36.91 % (1250663)------------------------------ % 257.95/36.91 % (1250661)Instruction limit reached! % 257.95/36.91 % (1250661)------------------------------ % 257.95/36.91 % (1250661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.95/36.91 % (1250661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.95/36.91 % (1250661)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250661)Termination reason: Instruction limit % 257.95/36.91 % (1250661)Termination phase: Saturation % 257.95/36.91 % (1250661)Time elapsed: 0.203 s % 257.95/36.91 % (1250661)Peak memory usage: 14 MB % 257.95/36.91 % (1250661)Instructions burned: 955 (million) % 257.95/36.91 % (1250665)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1217964351:i=2358:rtra=on_2684 on theBenchmark for (2684ds/2358Mi) % 257.95/36.91 % (1250667)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=666255263:i=1778:ins=1:rtra=on_2684 on theBenchmark for (2684ds/1778Mi) % 257.95/36.91 % (1250667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.95/36.91 % (1250667)Terminated due to inappropriate strategy. % 257.95/36.91 % (1250667)------------------------------ % 257.95/36.91 % (1250667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.95/36.91 % (1250667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.95/36.91 % (1250667)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250667)Termination reason: Inappropriate % 257.95/36.91 % (1250667)Time elapsed: 0.018 s % 257.95/36.91 % (1250667)Peak memory usage: 10 MB % 257.95/36.91 % (1250667)Instructions burned: 90 (million) % 257.95/36.91 % (1250667)------------------------------ % 257.95/36.91 % (1250667)------------------------------ % 257.95/36.91 % (1250669)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=2424371097:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2683 on theBenchmark for (2683ds/1384Mi) % 257.95/36.91 % (1250669)Instruction limit reached! % 257.95/36.91 % (1250669)------------------------------ % 257.95/36.91 % (1250669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.95/36.91 % (1250669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.95/36.91 % (1250669)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250669)Termination reason: Instruction limit % 257.95/36.91 % (1250669)Termination phase: Saturation % 257.95/36.91 % (1250669)Time elapsed: 0.278 s % 257.95/36.91 % (1250669)Peak memory usage: 14 MB % 257.95/36.91 % (1250669)Instructions burned: 1389 (million) % 257.95/36.91 % (1250671)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2837406050:i=1758:kws=inv_precedence:fsr=off:rtra=on_2681 on theBenchmark for (2681ds/1758Mi) % 257.95/36.91 % (1250671)Instruction limit reached! % 257.95/36.91 % (1250671)------------------------------ % 257.95/36.91 % (1250671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.95/36.91 % (1250671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.95/36.91 % (1250671)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250671)Termination reason: Instruction limit % 257.95/36.91 % (1250671)Termination phase: Saturation % 257.95/36.91 % (1250671)Time elapsed: 0.354 s % 257.95/36.91 % (1250671)Peak memory usage: 15 MB % 257.95/36.91 % (1250671)Instructions burned: 1760 (million) % 257.95/36.91 % (1250673)fmb+10_1_sil=64000:si=on:random_seed=912352344:i=44122:nm=2:rtra=on:gsp=on_2677 on theBenchmark for (2677ds/44122Mi) % 257.95/36.91 % (1250673)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.95/36.91 % (1250673)Terminated due to inappropriate strategy. % 257.95/36.91 % (1250673)------------------------------ % 257.95/36.91 % (1250673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.95/36.91 % (1250673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.95/36.91 % (1250673)CaDiCaL version: 2.1.3 % 257.95/36.91 % (1250673)Termination reason: Inappropriate % 257.95/36.91 % (1250673)Time elapsed: 0.024 s % 257.95/36.91 % (1250673)Peak memory usage: 10 MB % 257.95/36.91 % (1250673)Instructions burned: 118 (million) % 257.95/36.91 % (1250673)------------------------------ % 257.95/36.91 % (1250673)------------------------------ % 257.95/36.91 % (1250675)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2375783826:i=19030:nm=5:rtra=on_2677 on theBenchmark for (2677ds/19030Mi) % 277.46/39.52 % (1250675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.46/39.52 % (1250675)Terminated due to inappropriate strategy. % 277.46/39.52 % (1250675)------------------------------ % 277.46/39.52 % (1250675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.46/39.52 % (1250675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.46/39.52 % (1250675)CaDiCaL version: 2.1.3 % 277.46/39.52 % (1250675)Termination reason: Inappropriate % 277.46/39.52 % (1250675)Time elapsed: 0.024 s % 277.46/39.52 % (1250675)Peak memory usage: 10 MB % 277.46/39.52 % (1250675)Instructions burned: 118 (million) % 277.46/39.52 % (1250675)------------------------------ % 277.46/39.52 % (1250675)------------------------------ % 277.46/39.52 % (1250677)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=881976984:fmbsr=1.7:i=1840:rtra=on_2676 on theBenchmark for (2676ds/1840Mi) % 277.46/39.52 % (1250677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.46/39.52 % (1250677)Terminated due to inappropriate strategy. % 277.46/39.52 % (1250677)------------------------------ % 277.46/39.52 % (1250677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.46/39.52 % (1250677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.46/39.52 % (1250677)CaDiCaL version: 2.1.3 % 277.46/39.52 % (1250677)Termination reason: Inappropriate % 277.46/39.52 % (1250677)Time elapsed: 0.038 s % 277.46/39.52 % (1250677)Peak memory usage: 10 MB % 277.46/39.52 % (1250677)Instructions burned: 118 (million) % 277.46/39.52 % (1250677)------------------------------ % 277.46/39.52 % (1250677)------------------------------ % 277.46/39.52 % (1250679)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2946086091:i=10262:rtra=on_2676 on theBenchmark for (2676ds/10262Mi) % 277.46/39.52 % (1250665)Instruction limit reached! % 277.46/39.52 % (1250665)------------------------------ % 277.46/39.52 % (1250665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.46/39.52 % (1250665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.46/39.52 % (1250665)CaDiCaL version: 2.1.3 % 277.46/39.52 % (1250665)Termination reason: Instruction limit % 277.46/39.52 % (1250665)Termination phase: Saturation % 277.46/39.52 % (1250665)Time elapsed: 0.883 s % 277.46/39.52 % (1250665)Peak memory usage: 13 MB % 277.46/39.52 % (1250665)Instructions burned: 2358 (million) % 277.46/39.52 % (1250681)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2878579313:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2675 on theBenchmark for (2675ds/2944Mi) % 277.46/39.52 % (1250681)Instruction limit reached! % 277.46/39.52 % (1250681)------------------------------ % 277.46/39.52 % (1250681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.46/39.52 % (1250681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.46/39.52 % (1250681)CaDiCaL version: 2.1.3 % 277.46/39.52 % (1250681)Termination reason: Instruction limit % 277.46/39.52 % (1250681)Termination phase: Saturation % 277.46/39.52 % (1250681)Time elapsed: 0.590 s % 277.46/39.52 % (1250681)Peak memory usage: 15 MB % 277.46/39.52 % (1250681)Instructions burned: 2947 (million) % 277.46/39.52 % (1250683)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2636802378:i=12648:rtra=on_2669 on theBenchmark for (2669ds/12648Mi) % 277.46/39.52 % (1250683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.46/39.52 % (1250683)Terminated due to inappropriate strategy. % 277.46/39.52 % (1250683)------------------------------ % 277.46/39.52 % (1250683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.46/39.52 % (1250683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.46/39.52 % (1250683)CaDiCaL version: 2.1.3 % 277.46/39.52 % (1250683)Termination reason: Inappropriate % 277.46/39.52 % (1250683)Time elapsed: 0.024 s % 277.46/39.52 % (1250683)Peak memory usage: 10 MB % 277.46/39.52 % (1250683)Instructions burned: 118 (million) % 277.46/39.52 % (1250683)------------------------------ % 277.46/39.52 % (1250683)------------------------------ % 277.46/39.52 % (1250685)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2369256590:fmbsr=2.30978:i=4348:rtra=on_2668 on theBenchmark for (2668ds/4348Mi) % 277.46/39.52 % (1250685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.46/39.52 % (1250685)Terminated due to inappropriate Terminated % 300.28/42.74 % Vampire exiting %------------------------------------------------------------------------------