%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC463_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 : n018.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:02 PM UTC 2026 % Result : Timeout 300.44s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC463_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 % Computer : n018.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 09:41:54 UTC 2026 % 0.10/0.21 % CPUTime : % 0.10/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.24 Running first-order model finding % 0.10/0.24 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.55/0.88 % (3257432)Will run a generic schedule for satisfiability detection. % 3.55/0.88 % (3257440)dis+10_1_sil=32000:sp=arity:random_seed=818567320:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.55/0.88 % (3257438)% WARNING: option uhcvi not known. % 3.55/0.88 % (3257437)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3327105110_2999 on theBenchmark for (2999ds/0Mi) % 3.55/0.88 % (3257438)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=56419432:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.55/0.88 % (3257439)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1547847681:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.55/0.88 % (3257441)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3273218466:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.55/0.88 % (3257442)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=918400228:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.55/0.88 % (3257443)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1922544708:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.55/0.88 % (3257437)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.55/0.88 % (3257437)Terminated due to inappropriate strategy. % 3.55/0.88 % (3257437)------------------------------ % 3.55/0.88 % (3257437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (3257437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (3257437)CaDiCaL version: 2.1.3 % 3.55/0.88 % (3257437)Termination reason: Inappropriate % 3.55/0.88 % (3257437)Time elapsed: 0.001 s % 3.55/0.88 % (3257437)Peak memory usage: 10 MB % 3.55/0.88 % (3257437)Instructions burned: 2 (million) % 3.55/0.88 % (3257437)------------------------------ % 3.55/0.88 % (3257437)------------------------------ % 3.55/0.88 % (3257451)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=38397127:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.55/0.88 % (3257451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.55/0.88 % (3257451)Terminated due to inappropriate strategy. % 3.55/0.88 % (3257451)------------------------------ % 3.55/0.88 % (3257451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (3257451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (3257451)CaDiCaL version: 2.1.3 % 3.55/0.88 % (3257451)Termination reason: Inappropriate % 3.55/0.88 % (3257451)Time elapsed: 0.001 s % 3.55/0.88 % (3257451)Peak memory usage: 10 MB % 3.55/0.88 % (3257451)Instructions burned: 2 (million) % 3.55/0.88 % (3257451)------------------------------ % 3.55/0.88 % (3257451)------------------------------ % 3.55/0.88 % (3257440)Instruction limit reached! % 3.55/0.88 % (3257440)------------------------------ % 3.55/0.88 % (3257440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (3257440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (3257440)CaDiCaL version: 2.1.3 % 3.55/0.88 % (3257440)Termination reason: Instruction limit % 3.55/0.88 % (3257440)Termination phase: Saturation % 3.55/0.88 % (3257440)Time elapsed: 0.038 s % 3.55/0.88 % (3257440)Peak memory usage: 13 MB % 3.55/0.88 % (3257440)Instructions burned: 116 (million) % 3.55/0.88 % (3257454)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=4073841168:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.55/0.88 % (3257453)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=230550610:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.55/0.88 % (3257441)Instruction limit reached! % 3.55/0.88 % (3257441)------------------------------ % 3.55/0.88 % (3257441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (3257441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (3257441)CaDiCaL version: 2.1.3 % 3.55/0.88 % (3257441)Termination reason: Instruction limit % 3.55/0.88 % (3257441)Termination phase: Saturation % 3.55/0.88 % (3257441)Time elapsed: 0.074 s % 3.55/0.88 % (3257441)Peak memory usage: 13 MB % 3.55/0.88 % (3257441)Instructions burned: 119 (million) % 3.55/0.88 % (3257442)Instruction limit reached! % 3.55/0.88 % (3257442)------------------------------ % 3.55/0.88 % (3257442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257442)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257442)Termination reason: Instruction limit % 5.68/1.07 % (3257442)Termination phase: Saturation % 5.68/1.07 % (3257442)Time elapsed: 0.075 s % 5.68/1.07 % (3257442)Peak memory usage: 12 MB % 5.68/1.07 % (3257442)Instructions burned: 131 (million) % 5.68/1.07 % (3257458)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=973743691:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.68/1.07 % (3257457)ott-21_1_sil=16000:fs=off:random_seed=3037441038:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.68/1.07 % (3257443)Instruction limit reached! % 5.68/1.07 % (3257443)------------------------------ % 5.68/1.07 % (3257443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257443)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257443)Termination reason: Instruction limit % 5.68/1.07 % (3257443)Termination phase: Saturation % 5.68/1.07 % (3257443)Time elapsed: 0.107 s % 5.68/1.07 % (3257443)Peak memory usage: 13 MB % 5.68/1.07 % (3257443)Instructions burned: 159 (million) % 5.68/1.07 % (3257453)Instruction limit reached! % 5.68/1.07 % (3257453)------------------------------ % 5.68/1.07 % (3257453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257453)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257453)Termination reason: Instruction limit % 5.68/1.07 % (3257453)Termination phase: Saturation % 5.68/1.07 % (3257453)Time elapsed: 0.078 s % 5.68/1.07 % (3257453)Peak memory usage: 12 MB % 5.68/1.07 % (3257453)Instructions burned: 132 (million) % 5.68/1.07 % (3257461)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=582309823:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.68/1.07 % (3257461)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.68/1.07 % (3257461)Terminated due to inappropriate strategy. % 5.68/1.07 % (3257461)------------------------------ % 5.68/1.07 % (3257461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257461)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257461)Termination reason: Inappropriate % 5.68/1.07 % (3257461)Time elapsed: 0.001 s % 5.68/1.07 % (3257461)Peak memory usage: 10 MB % 5.68/1.07 % (3257461)Instructions burned: 2 (million) % 5.68/1.07 % (3257461)------------------------------ % 5.68/1.07 % (3257461)------------------------------ % 5.68/1.07 % (3257462)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=691208395:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.68/1.07 % (3257464)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3008628995:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.68/1.07 % (3257464)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.68/1.07 % (3257464)Terminated due to inappropriate strategy. % 5.68/1.07 % (3257464)------------------------------ % 5.68/1.07 % (3257464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257464)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257464)Termination reason: Inappropriate % 5.68/1.07 % (3257464)Time elapsed: 0.001 s % 5.68/1.07 % (3257464)Peak memory usage: 10 MB % 5.68/1.07 % (3257464)Instructions burned: 2 (million) % 5.68/1.07 % (3257464)------------------------------ % 5.68/1.07 % (3257464)------------------------------ % 5.68/1.07 % (3257467)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=3941256154:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.68/1.07 % (3257457)Instruction limit reached! % 5.68/1.07 % (3257457)------------------------------ % 5.68/1.07 % (3257457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.07 % (3257457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.07 % (3257457)CaDiCaL version: 2.1.3 % 5.68/1.07 % (3257457)Termination reason: Instruction limit % 5.68/1.07 % (3257457)Termination phase: Saturation % 23.75/3.66 % (3257457)Time elapsed: 0.086 s % 23.75/3.66 % (3257457)Peak memory usage: 12 MB % 23.75/3.66 % (3257457)Instructions burned: 181 (million) % 23.75/3.66 % (3257469)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1552003251:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.75/3.66 % (3257454)Instruction limit reached! % 23.75/3.66 % (3257454)------------------------------ % 23.75/3.66 % (3257454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.75/3.66 % (3257454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.75/3.66 % (3257454)CaDiCaL version: 2.1.3 % 23.75/3.66 % (3257454)Termination reason: Instruction limit % 23.75/3.66 % (3257454)Termination phase: Saturation % 23.75/3.66 % (3257454)Time elapsed: 0.193 s % 23.75/3.66 % (3257454)Peak memory usage: 17 MB % 23.75/3.66 % (3257454)Instructions burned: 685 (million) % 23.75/3.66 % (3257480)fmb+10_1_sil=64000:random_seed=1840119012:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 23.75/3.66 % (3257480)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.75/3.66 % (3257480)Terminated due to inappropriate strategy. % 23.75/3.66 % (3257480)------------------------------ % 23.75/3.66 % (3257480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.75/3.66 % (3257480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.75/3.66 % (3257480)CaDiCaL version: 2.1.3 % 23.75/3.66 % (3257480)Termination reason: Inappropriate % 23.75/3.66 % (3257480)Time elapsed: 0.0000 s % 23.75/3.66 % (3257480)Peak memory usage: 10 MB % 23.75/3.66 % (3257480)Instructions burned: 2 (million) % 23.75/3.66 % (3257480)------------------------------ % 23.75/3.66 % (3257480)------------------------------ % 23.75/3.66 % (3257482)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2396041733:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 23.75/3.66 % (3257482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.75/3.66 % (3257482)Terminated due to inappropriate strategy. % 23.75/3.66 % (3257482)------------------------------ % 23.75/3.66 % (3257482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.75/3.66 % (3257482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.75/3.66 % (3257482)CaDiCaL version: 2.1.3 % 23.75/3.66 % (3257482)Termination reason: Inappropriate % 23.75/3.66 % (3257482)Time elapsed: 0.0000 s % 23.75/3.66 % (3257482)Peak memory usage: 10 MB % 23.75/3.66 % (3257482)Instructions burned: 2 (million) % 23.75/3.66 % (3257482)------------------------------ % 23.75/3.66 % (3257482)------------------------------ % 23.75/3.66 % (3257489)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4167205165:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 23.75/3.66 % (3257489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.75/3.66 % (3257489)Terminated due to inappropriate strategy. % 23.75/3.66 % (3257489)------------------------------ % 23.75/3.66 % (3257489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.75/3.66 % (3257489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.75/3.66 % (3257489)CaDiCaL version: 2.1.3 % 23.75/3.66 % (3257489)Termination reason: Inappropriate % 23.75/3.66 % (3257489)Time elapsed: 0.0000 s % 23.75/3.66 % (3257489)Peak memory usage: 11 MB % 23.75/3.66 % (3257489)Instructions burned: 2 (million) % 23.75/3.66 % (3257489)------------------------------ % 23.75/3.66 % (3257489)------------------------------ % 23.75/3.66 % (3257494)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2396877530:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 23.75/3.66 % (3257458)Instruction limit reached! % 23.75/3.66 % (3257458)------------------------------ % 23.75/3.66 % (3257458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.75/3.66 % (3257458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.75/3.66 % (3257458)CaDiCaL version: 2.1.3 % 23.75/3.66 % (3257458)Termination reason: Instruction limit % 23.75/3.66 % (3257458)Termination phase: Saturation % 23.75/3.66 % (3257458)Time elapsed: 0.285 s % 23.75/3.66 % (3257458)Peak memory usage: 13 MB % 23.75/3.66 % (3257458)Instructions burned: 478 (million) % 23.75/3.66 % (3257522)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3888739642:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 23.75/3.66 % (3257467)Instruction limit reached! % 23.75/3.66 % (3257467)------------------------------ % 43.66/6.44 % (3257467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257467)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257467)Termination reason: Instruction limit % 43.66/6.44 % (3257467)Termination phase: Saturation % 43.66/6.44 % (3257467)Time elapsed: 0.426 s % 43.66/6.44 % (3257467)Peak memory usage: 17 MB % 43.66/6.44 % (3257467)Instructions burned: 692 (million) % 43.66/6.44 % (3257580)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3211253910:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 43.66/6.44 % (3257580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.66/6.44 % (3257580)Terminated due to inappropriate strategy. % 43.66/6.44 % (3257580)------------------------------ % 43.66/6.44 % (3257580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257580)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257580)Termination reason: Inappropriate % 43.66/6.44 % (3257580)Time elapsed: 0.001 s % 43.66/6.44 % (3257580)Peak memory usage: 10 MB % 43.66/6.44 % (3257580)Instructions burned: 2 (million) % 43.66/6.44 % (3257580)------------------------------ % 43.66/6.44 % (3257580)------------------------------ % 43.66/6.44 % (3257586)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=26228240:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 43.66/6.44 % (3257586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.66/6.44 % (3257586)Terminated due to inappropriate strategy. % 43.66/6.44 % (3257586)------------------------------ % 43.66/6.44 % (3257586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257586)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257586)Termination reason: Inappropriate % 43.66/6.44 % (3257586)Time elapsed: 0.001 s % 43.66/6.44 % (3257586)Peak memory usage: 10 MB % 43.66/6.44 % (3257586)Instructions burned: 2 (million) % 43.66/6.44 % (3257586)------------------------------ % 43.66/6.44 % (3257586)------------------------------ % 43.66/6.44 % (3257592)ott-2_1_sil=16000:newcnf=on:random_seed=122713937:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 43.66/6.44 % (3257469)Instruction limit reached! % 43.66/6.44 % (3257469)------------------------------ % 43.66/6.44 % (3257469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257469)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257469)Termination reason: Instruction limit % 43.66/6.44 % (3257469)Termination phase: Saturation % 43.66/6.44 % (3257469)Time elapsed: 0.503 s % 43.66/6.44 % (3257469)Peak memory usage: 19 MB % 43.66/6.44 % (3257469)Instructions burned: 879 (million) % 43.66/6.44 % (3257608)ott+10_1_sil=32000:tgt=ground:random_seed=3082467888:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 43.66/6.44 % (3257462)Instruction limit reached! % 43.66/6.44 % (3257462)------------------------------ % 43.66/6.44 % (3257462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257462)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257462)Termination reason: Instruction limit % 43.66/6.44 % (3257462)Termination phase: Saturation % 43.66/6.44 % (3257462)Time elapsed: 0.621 s % 43.66/6.44 % (3257462)Peak memory usage: 17 MB % 43.66/6.44 % (3257462)Instructions burned: 1179 (million) % 43.66/6.44 % (3257619)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=208096780:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 43.66/6.44 % (3257619)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.66/6.44 % (3257619)Terminated due to inappropriate strategy. % 43.66/6.44 % (3257619)------------------------------ % 43.66/6.44 % (3257619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.66/6.44 % (3257619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.66/6.44 % (3257619)CaDiCaL version: 2.1.3 % 43.66/6.44 % (3257619)Termination reason: Inappropriate % 43.66/6.44 % (3257619)Time elapsed: 0.001 s % 43.66/6.44 % (3257619)Peak memory usage: 11 MB % 43.66/6.44 % (3257619)Instructions burned: 2 (million) % 147.60/21.11 % (3257619)------------------------------ % 147.60/21.11 % (3257619)------------------------------ % 147.60/21.11 % (3257621)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2262281372:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 147.60/21.11 % (3257522)Instruction limit reached! % 147.60/21.11 % (3257522)------------------------------ % 147.60/21.11 % (3257522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257522)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257522)Termination reason: Instruction limit % 147.60/21.11 % (3257522)Termination phase: Saturation % 147.60/21.11 % (3257522)Time elapsed: 0.904 s % 147.60/21.11 % (3257522)Peak memory usage: 27 MB % 147.60/21.11 % (3257522)Instructions burned: 1472 (million) % 147.60/21.11 % (3257592)Instruction limit reached! % 147.60/21.11 % (3257592)------------------------------ % 147.60/21.11 % (3257592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257592)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257592)Termination reason: Instruction limit % 147.60/21.11 % (3257592)Termination phase: Saturation % 147.60/21.11 % (3257592)Time elapsed: 0.639 s % 147.60/21.11 % (3257592)Peak memory usage: 17 MB % 147.60/21.11 % (3257592)Instructions burned: 869 (million) % 147.60/21.11 % (3257623)dis+21_1_sil=32000:sas=cadical:random_seed=1811422533:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 147.60/21.11 % (3257624)ott+11_1_sil=16000:gs=on:random_seed=2939407033:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 147.60/21.11 % (3257494)Instruction limit reached! % 147.60/21.11 % (3257494)------------------------------ % 147.60/21.11 % (3257494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257494)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257494)Termination reason: Instruction limit % 147.60/21.11 % (3257494)Termination phase: Saturation % 147.60/21.11 % (3257494)Time elapsed: 1.690 s % 147.60/21.11 % (3257494)Peak memory usage: 41 MB % 147.60/21.11 % (3257494)Instructions burned: 5131 (million) % 147.60/21.11 % (3257660)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3576981911:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 147.60/21.11 % (3257660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.60/21.11 % (3257660)Terminated due to inappropriate strategy. % 147.60/21.11 % (3257660)------------------------------ % 147.60/21.11 % (3257660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257660)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257660)Termination reason: Inappropriate % 147.60/21.11 % (3257660)Time elapsed: 0.002 s % 147.60/21.11 % (3257660)Peak memory usage: 10 MB % 147.60/21.11 % (3257660)Instructions burned: 2 (million) % 147.60/21.11 % (3257660)------------------------------ % 147.60/21.11 % (3257660)------------------------------ % 147.60/21.11 % (3257664)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2345858912:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 147.60/21.11 % (3257621)Instruction limit reached! % 147.60/21.11 % (3257621)------------------------------ % 147.60/21.11 % (3257621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257621)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257621)Termination reason: Instruction limit % 147.60/21.11 % (3257621)Termination phase: Saturation % 147.60/21.11 % (3257621)Time elapsed: 1.873 s % 147.60/21.11 % (3257621)Peak memory usage: 29 MB % 147.60/21.11 % (3257621)Instructions burned: 3512 (million) % 147.60/21.11 % (3257696)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2738965827:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 147.60/21.11 % (3257624)Instruction limit reached! % 147.60/21.11 % (3257624)------------------------------ % 147.60/21.11 % (3257624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.60/21.11 % (3257624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.60/21.11 % (3257624)CaDiCaL version: 2.1.3 % 147.60/21.11 % (3257624)Termination reason: Instruction limit % 186.74/26.55 % (3257624)Termination phase: Saturation % 186.74/26.55 % (3257624)Time elapsed: 2.050 s % 186.74/26.55 % (3257624)Peak memory usage: 22 MB % 186.74/26.55 % (3257624)Instructions burned: 2251 (million) % 186.74/26.55 % (3257721)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2418056695:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 186.74/26.55 % (3257623)Instruction limit reached! % 186.74/26.55 % (3257623)------------------------------ % 186.74/26.55 % (3257623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.74/26.55 % (3257623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.74/26.55 % (3257623)CaDiCaL version: 2.1.3 % 186.74/26.55 % (3257623)Termination reason: Instruction limit % 186.74/26.55 % (3257623)Termination phase: Saturation % 186.74/26.55 % (3257623)Time elapsed: 3.048 s % 186.74/26.55 % (3257623)Peak memory usage: 30 MB % 186.74/26.55 % (3257623)Instructions burned: 3774 (million) % 186.74/26.55 % (3257750)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1818574409:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 186.74/26.55 % (3257750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.74/26.55 % (3257750)Terminated due to inappropriate strategy. % 186.74/26.55 % (3257750)------------------------------ % 186.74/26.55 % (3257750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.74/26.55 % (3257750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.74/26.55 % (3257750)CaDiCaL version: 2.1.3 % 186.74/26.55 % (3257750)Termination reason: Inappropriate % 186.74/26.55 % (3257750)Time elapsed: 0.002 s % 186.74/26.55 % (3257750)Peak memory usage: 10 MB % 186.74/26.55 % (3257750)Instructions burned: 2 (million) % 186.74/26.55 % (3257750)------------------------------ % 186.74/26.55 % (3257750)------------------------------ % 186.74/26.55 % (3257753)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3775433816:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 186.74/26.55 % (3257753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.74/26.55 % (3257753)Terminated due to inappropriate strategy. % 186.74/26.55 % (3257753)------------------------------ % 186.74/26.55 % (3257753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.74/26.55 % (3257753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.74/26.55 % (3257753)CaDiCaL version: 2.1.3 % 186.74/26.55 % (3257753)Termination reason: Inappropriate % 186.74/26.55 % (3257753)Time elapsed: 0.002 s % 186.74/26.55 % (3257753)Peak memory usage: 10 MB % 186.74/26.55 % (3257753)Instructions burned: 2 (million) % 186.74/26.55 % (3257753)------------------------------ % 186.74/26.55 % (3257753)------------------------------ % 186.74/26.55 % (3257756)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2976600742:i=14071_2954 on theBenchmark for (2954ds/14071Mi) % 186.74/26.55 % (3257756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.74/26.55 % (3257756)Terminated due to inappropriate strategy. % 186.74/26.55 % (3257756)------------------------------ % 186.74/26.55 % (3257756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.74/26.55 % (3257756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.74/26.55 % (3257756)CaDiCaL version: 2.1.3 % 186.74/26.55 % (3257756)Termination reason: Inappropriate % 186.74/26.55 % (3257756)Time elapsed: 0.002 s % 186.74/26.55 % (3257756)Peak memory usage: 10 MB % 186.74/26.55 % (3257756)Instructions burned: 2 (million) % 186.74/26.55 % (3257756)------------------------------ % 186.74/26.55 % (3257756)------------------------------ % 186.74/26.55 % (3257760)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3675875288:i=22565:add=on:rawr=on_2954 on theBenchmark for (2954ds/22565Mi) % 186.74/26.55 % (3257608)Instruction limit reached! % 186.74/26.55 % (3257608)------------------------------ % 186.74/26.55 % (3257608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.74/26.55 % (3257608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.74/26.55 % (3257608)CaDiCaL version: 2.1.3 % 186.74/26.55 % (3257608)Termination reason: Instruction limit % 186.74/26.55 % (3257608)Termination phase: Saturation % 186.74/26.55 % (3257608)Time elapsed: 4.640 s % 186.74/26.55 % (3257608)Peak memory usage: 33 MB % 186.74/26.55 % (3257608)Instructions burned: 5114 (million) % 186.74/26.55 % (3257783)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=630376065:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi) % 186.74/26.55 % (3257664)Instruction limit reached! % 188.12/26.72 % (3257664)------------------------------ % 188.12/26.72 % (3257664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257664)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257664)Termination reason: Instruction limit % 188.12/26.72 % (3257664)Termination phase: Saturation % 188.12/26.72 % (3257664)Time elapsed: 4.082 s % 188.12/26.72 % (3257664)Peak memory usage: 45 MB % 188.12/26.72 % (3257664)Instructions burned: 4592 (million) % 188.12/26.72 % (3257803)dis+10_16:1_sil=16000:random_seed=1765660138:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi) % 188.12/26.72 % (3257721)Instruction limit reached! % 188.12/26.72 % (3257721)------------------------------ % 188.12/26.72 % (3257721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257721)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257721)Termination reason: Instruction limit % 188.12/26.72 % (3257721)Termination phase: Saturation % 188.12/26.72 % (3257721)Time elapsed: 4.616 s % 188.12/26.72 % (3257721)Peak memory usage: 55 MB % 188.12/26.72 % (3257721)Instructions burned: 5212 (million) % 188.12/26.72 % (3257840)ott-3_8_sil=64000:random_seed=2006257957:i=20139:bs=on_2919 on theBenchmark for (2919ds/20139Mi) % 188.12/26.72 % (3257783)Instruction limit reached! % 188.12/26.72 % (3257783)------------------------------ % 188.12/26.72 % (3257783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257783)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257783)Termination reason: Instruction limit % 188.12/26.72 % (3257783)Termination phase: Saturation % 188.12/26.72 % (3257783)Time elapsed: 8.299 s % 188.12/26.72 % (3257783)Peak memory usage: 61 MB % 188.12/26.72 % (3257783)Instructions burned: 8173 (million) % 188.12/26.72 % (3257887)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1596899340:fmbsr=2:i=32576_2862 on theBenchmark for (2862ds/32576Mi) % 188.12/26.72 % (3257887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.12/26.72 % (3257887)Terminated due to inappropriate strategy. % 188.12/26.72 % (3257887)------------------------------ % 188.12/26.72 % (3257887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257887)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257887)Termination reason: Inappropriate % 188.12/26.72 % (3257887)Time elapsed: 0.002 s % 188.12/26.72 % (3257887)Peak memory usage: 11 MB % 188.12/26.72 % (3257887)Instructions burned: 2 (million) % 188.12/26.72 % (3257887)------------------------------ % 188.12/26.72 % (3257887)------------------------------ % 188.12/26.72 % (3257889)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=211670741:i=11404_2862 on theBenchmark for (2862ds/11404Mi) % 188.12/26.72 % (3257803)Instruction limit reached! % 188.12/26.72 % (3257803)------------------------------ % 188.12/26.72 % (3257803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257803)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257803)Termination reason: Instruction limit % 188.12/26.72 % (3257803)Termination phase: Saturation % 188.12/26.72 % (3257803)Time elapsed: 7.905 s % 188.12/26.72 % (3257803)Peak memory usage: 50 MB % 188.12/26.72 % (3257803)Instructions burned: 9156 (million) % 188.12/26.72 % (3257893)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1555554469:i=14134_2858 on theBenchmark for (2858ds/14134Mi) % 188.12/26.72 % (3257696)Instruction limit reached! % 188.12/26.72 % (3257696)------------------------------ % 188.12/26.72 % (3257696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.12/26.72 % (3257696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.12/26.72 % (3257696)CaDiCaL version: 2.1.3 % 188.12/26.72 % (3257696)Termination reason: Instruction limit % 188.12/26.72 % (3257696)Termination phase: Saturation % 188.12/26.72 % (3257696)Time elapsed: 11.664 s % 188.12/26.72 % (3257696)Peak memory usage: 174 MB % 188.12/26.72 % (3257696)Instructions burned: 29342 (million) % 188.12/26.72 % (3257896)dis+33_16_sil=32000:sac=on:random_seed=1907906932:i=15851:nm=0_2855 on theBenchmark for (2855ds/15851Mi) % 188.12/26.72 % (3257760)Instruction limit reached! % 188.12/26.72 % (3257760)------------------------------ % 188.12/26.72 % (3257760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257760)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257760)Termination reason: Instruction limit % 255.89/36.26 % (3257760)Termination phase: Saturation % 255.89/36.26 % (3257760)Time elapsed: 16.256 s % 255.89/36.26 % (3257760)Peak memory usage: 80 MB % 255.89/36.26 % (3257760)Instructions burned: 22566 (million) % 255.89/36.26 % (3257917)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3831048895:avsq=on:i=17627:add=on:amm=off_2791 on theBenchmark for (2791ds/17627Mi) % 255.89/36.26 % (3257896)Instruction limit reached! % 255.89/36.26 % (3257896)------------------------------ % 255.89/36.26 % (3257896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257896)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257896)Termination reason: Instruction limit % 255.89/36.26 % (3257896)Termination phase: Saturation % 255.89/36.26 % (3257896)Time elapsed: 7.126 s % 255.89/36.26 % (3257896)Peak memory usage: 199 MB % 255.89/36.26 % (3257896)Instructions burned: 15853 (million) % 255.89/36.26 % (3257924)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4106390946:s2a=on:i=53295_2783 on theBenchmark for (2783ds/53295Mi) % 255.89/36.26 % (3257889)Instruction limit reached! % 255.89/36.26 % (3257889)------------------------------ % 255.89/36.26 % (3257889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257889)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257889)Termination reason: Instruction limit % 255.89/36.26 % (3257889)Termination phase: Saturation % 255.89/36.26 % (3257889)Time elapsed: 11.377 s % 255.89/36.26 % (3257889)Peak memory usage: 61 MB % 255.89/36.26 % (3257889)Instructions burned: 11405 (million) % 255.89/36.26 % (3257946)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1451253839:i=26857:ins=20_2747 on theBenchmark for (2747ds/26857Mi) % 255.89/36.26 % (3257946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.89/36.26 % (3257946)Terminated due to inappropriate strategy. % 255.89/36.26 % (3257946)------------------------------ % 255.89/36.26 % (3257946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257946)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257946)Termination reason: Inappropriate % 255.89/36.26 % (3257946)Time elapsed: 0.002 s % 255.89/36.26 % (3257946)Peak memory usage: 11 MB % 255.89/36.26 % (3257946)Instructions burned: 2 (million) % 255.89/36.26 % (3257946)------------------------------ % 255.89/36.26 % (3257946)------------------------------ % 255.89/36.26 % (3257948)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=466609394:i=28120:bs=on:fsr=off_2747 on theBenchmark for (2747ds/28120Mi) % 255.89/36.26 % (3257840)Instruction limit reached! % 255.89/36.26 % (3257840)------------------------------ % 255.89/36.26 % (3257840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257840)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257840)Termination reason: Instruction limit % 255.89/36.26 % (3257840)Termination phase: Saturation % 255.89/36.26 % (3257840)Time elapsed: 18.107 s % 255.89/36.26 % (3257840)Peak memory usage: 82 MB % 255.89/36.26 % (3257840)Instructions burned: 20140 (million) % 255.89/36.26 % (3257952)fmb+10_1_sil=256000:fmbss=7:random_seed=4080250246:fmbsr=1.6:i=182295_2737 on theBenchmark for (2737ds/182295Mi) % 255.89/36.26 % (3257952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.89/36.26 % (3257952)Terminated due to inappropriate strategy. % 255.89/36.26 % (3257952)------------------------------ % 255.89/36.26 % (3257952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.89/36.26 % (3257952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.89/36.26 % (3257952)CaDiCaL version: 2.1.3 % 255.89/36.26 % (3257952)Termination reason: Inappropriate % 255.89/36.26 % (3257952)Time elapsed: 0.003 s % 255.89/36.26 % (3257952)Peak memory usage: 10 MB % 255.89/36.26 % (3257952)Instructions burned: 2 (million) % 255.89/36.26 % (3257952)------------------------------ % 255.89/36.26 % (3257952)------------------------------ % 255.89/36.26 % (3257954)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1015741802:i=44625:gsp=on_2737 on theBenchmark for (2737ds/44625Mi) % 277.25/39.28 % (3257954)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.25/39.28 % (3257954)Terminated due to inappropriate strategy. % 277.25/39.28 % (3257954)------------------------------ % 277.25/39.28 % (3257954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.25/39.28 % (3257954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.25/39.28 % (3257954)CaDiCaL version: 2.1.3 % 277.25/39.28 % (3257954)Termination reason: Inappropriate % 277.25/39.28 % (3257954)Time elapsed: 0.002 s % 277.25/39.28 % (3257954)Peak memory usage: 11 MB % 277.25/39.28 % (3257954)Instructions burned: 2 (million) % 277.25/39.28 % (3257954)------------------------------ % 277.25/39.28 % (3257954)------------------------------ % 277.25/39.28 % (3257956)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=672788689:i=160505_2736 on theBenchmark for (2736ds/160505Mi) % 277.25/39.28 % (3257956)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.25/39.28 % (3257956)Terminated due to inappropriate strategy. % 277.25/39.28 % (3257956)------------------------------ % 277.25/39.28 % (3257956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.25/39.28 % (3257956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.25/39.28 % (3257956)CaDiCaL version: 2.1.3 % 277.25/39.28 % (3257956)Termination reason: Inappropriate % 277.25/39.28 % (3257956)Time elapsed: 0.001 s % 277.25/39.28 % (3257956)Peak memory usage: 11 MB % 277.25/39.28 % (3257956)Instructions burned: 2 (million) % 277.25/39.28 % (3257956)------------------------------ % 277.25/39.28 % (3257956)------------------------------ % 277.25/39.28 % (3257958)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2865246588:fmbsr=1.3:i=225729_2736 on theBenchmark for (2736ds/225729Mi) % 277.25/39.28 % (3257958)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.25/39.28 % (3257958)Terminated due to inappropriate strategy. % 277.25/39.28 % (3257958)------------------------------ % 277.25/39.28 % (3257958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.25/39.28 % (3257958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.25/39.28 % (3257958)CaDiCaL version: 2.1.3 % 277.25/39.28 % (3257958)Termination reason: Inappropriate % 277.25/39.28 % (3257958)Time elapsed: 0.003 s % 277.25/39.28 % (3257958)Peak memory usage: 10 MB % 277.25/39.28 % (3257958)Instructions burned: 2 (million) % 277.25/39.28 % (3257958)------------------------------ % 277.25/39.28 % (3257958)------------------------------ % 277.25/39.28 % (3257960)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1406457030:fmbsr=2:i=185024:ins=7_2736 on theBenchmark for (2736ds/185024Mi) % 277.25/39.28 % (3257960)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.25/39.28 % (3257960)Terminated due to inappropriate strategy. % 277.25/39.28 % (3257960)------------------------------ % 277.25/39.28 % (3257960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.25/39.28 % (3257960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.25/39.28 % (3257960)CaDiCaL version: 2.1.3 % 277.25/39.28 % (3257960)Termination reason: Inappropriate % 277.25/39.28 % (3257960)Time elapsed: 0.001 s % 277.25/39.28 % (3257960)Peak memory usage: 11 MB % 277.25/39.28 % (3257960)Instructions burned: 2 (million) % 277.25/39.28 % (3257960)------------------------------ % 277.25/39.28 % (3257960)------------------------------ % 277.25/39.28 % (3257962)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2951601324:rtra=on_2735 on theBenchmark for (2735ds/0Mi) % 277.25/39.28 % (3257962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.25/39.28 % (3257962)Terminated due to inappropriate strategy. % 277.25/39.28 % (3257962)------------------------------ % 277.25/39.28 % (3257962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.25/39.28 % (3257962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.25/39.28 % (3257962)CaDiCaL version: 2.1.3 % 277.25/39.28 % (3257962)Termination reason: Inappropriate % 277.25/39.28 % (3257962)Time elapsed: 0.002 s % 277.25/39.28 % (3257962)Peak memory usage: 11 MB % 277.25/39.28 % (3257962)Instructions burned: 2 (million) % 277.25/39.28 % (3257962)------------------------------ % 277.25/39.28 % (3257962)------------------------------ % 277.25/39.28 % (3257964)% WARNING: option uhcvi not known. % 277.25/39.28 % (3257964)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1007089077:i=27106Terminated % 300.44/42.54 % Vampire exiting %------------------------------------------------------------------------------