%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX104_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:29 PM UTC 2026 % Result : Timeout 286.60s 40.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX104_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n016.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 15:06:18 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.05/0.86 % (3689173)Will run a generic schedule for satisfiability detection. % 4.05/0.86 % (3689180)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1719876277:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.05/0.86 % (3689179)% WARNING: option uhcvi not known. % 4.05/0.86 % (3689178)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2580320394_2999 on theBenchmark for (2999ds/0Mi) % 4.05/0.86 % (3689179)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2116674217:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.05/0.86 % (3689181)dis+10_1_sil=32000:sp=arity:random_seed=3804898928:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.05/0.86 % (3689182)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3258334511:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.05/0.86 % (3689184)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1449132327:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.05/0.86 % (3689183)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2373344378:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.05/0.86 % (3689178)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.05/0.86 % (3689178)Terminated due to inappropriate strategy. % 4.05/0.86 % (3689178)------------------------------ % 4.05/0.86 % (3689178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.86 % (3689178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.86 % (3689178)CaDiCaL version: 2.1.3 % 4.05/0.86 % (3689178)Termination reason: Inappropriate % 4.05/0.86 % (3689178)Time elapsed: 0.004 s % 4.05/0.86 % (3689178)Peak memory usage: 10 MB % 4.05/0.86 % (3689178)Instructions burned: 6 (million) % 4.05/0.86 % (3689178)------------------------------ % 4.05/0.86 % (3689178)------------------------------ % 4.05/0.86 % (3689192)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2639982169:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.05/0.86 % (3689192)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.05/0.86 % (3689192)Terminated due to inappropriate strategy. % 4.05/0.86 % (3689192)------------------------------ % 4.05/0.86 % (3689192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.86 % (3689192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.86 % (3689192)CaDiCaL version: 2.1.3 % 4.05/0.86 % (3689192)Termination reason: Inappropriate % 4.05/0.86 % (3689192)Time elapsed: 0.003 s % 4.05/0.86 % (3689192)Peak memory usage: 11 MB % 4.05/0.86 % (3689192)Instructions burned: 5 (million) % 4.05/0.86 % (3689192)------------------------------ % 4.05/0.86 % (3689192)------------------------------ % 4.05/0.86 % (3689194)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=897075132:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.05/0.86 % (3689181)Instruction limit reached! % 4.05/0.86 % (3689181)------------------------------ % 4.05/0.86 % (3689181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.86 % (3689181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.86 % (3689181)CaDiCaL version: 2.1.3 % 4.05/0.86 % (3689181)Termination reason: Instruction limit % 4.05/0.86 % (3689181)Termination phase: Saturation % 4.05/0.86 % (3689181)Time elapsed: 0.068 s % 4.05/0.86 % (3689181)Peak memory usage: 13 MB % 4.05/0.86 % (3689181)Instructions burned: 103 (million) % 4.05/0.86 % (3689182)Instruction limit reached! % 4.05/0.86 % (3689182)------------------------------ % 4.05/0.86 % (3689182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.86 % (3689182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.86 % (3689182)CaDiCaL version: 2.1.3 % 4.05/0.86 % (3689182)Termination reason: Instruction limit % 4.05/0.86 % (3689182)Termination phase: Saturation % 4.05/0.86 % (3689182)Time elapsed: 0.072 s % 4.05/0.86 % (3689182)Peak memory usage: 13 MB % 4.05/0.86 % (3689182)Instructions burned: 117 (million) % 4.05/0.86 % (3689183)Instruction limit reached! % 4.05/0.86 % (3689183)------------------------------ % 4.05/0.86 % (3689183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.86 % (3689183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.86 % (3689183)CaDiCaL version: 2.1.3 % 4.05/0.86 % (3689183)Termination reason: Instruction limit % 6.48/1.15 % (3689183)Termination phase: Saturation % 6.48/1.15 % (3689183)Time elapsed: 0.084 s % 6.48/1.15 % (3689183)Peak memory usage: 13 MB % 6.48/1.15 % (3689183)Instructions burned: 133 (million) % 6.48/1.15 % (3689196)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=2544240948:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.48/1.15 % (3689197)ott-21_1_sil=16000:fs=off:random_seed=257769738:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.48/1.15 % (3689198)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=488163635:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.48/1.15 % (3689184)Instruction limit reached! % 6.48/1.15 % (3689184)------------------------------ % 6.48/1.15 % (3689184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.48/1.15 % (3689184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.48/1.15 % (3689184)CaDiCaL version: 2.1.3 % 6.48/1.15 % (3689184)Termination reason: Instruction limit % 6.48/1.15 % (3689184)Termination phase: Saturation % 6.48/1.15 % (3689184)Time elapsed: 0.110 s % 6.48/1.15 % (3689184)Peak memory usage: 14 MB % 6.48/1.15 % (3689184)Instructions burned: 159 (million) % 6.48/1.15 % (3689202)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3808801221:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.48/1.15 % (3689202)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.48/1.15 % (3689202)Terminated due to inappropriate strategy. % 6.48/1.15 % (3689202)------------------------------ % 6.48/1.15 % (3689202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.48/1.15 % (3689202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.48/1.15 % (3689202)CaDiCaL version: 2.1.3 % 6.48/1.15 % (3689202)Termination reason: Inappropriate % 6.48/1.15 % (3689202)Time elapsed: 0.002 s % 6.48/1.15 % (3689202)Peak memory usage: 10 MB % 6.48/1.15 % (3689202)Instructions burned: 3 (million) % 6.48/1.15 % (3689202)------------------------------ % 6.48/1.15 % (3689202)------------------------------ % 6.48/1.15 % (3689194)Instruction limit reached! % 6.48/1.15 % (3689194)------------------------------ % 6.48/1.15 % (3689194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.48/1.15 % (3689194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.48/1.15 % (3689194)CaDiCaL version: 2.1.3 % 6.48/1.15 % (3689194)Termination reason: Instruction limit % 6.48/1.15 % (3689194)Termination phase: Saturation % 6.48/1.15 % (3689194)Time elapsed: 0.092 s % 6.48/1.15 % (3689194)Peak memory usage: 13 MB % 6.48/1.15 % (3689194)Instructions burned: 131 (million) % 6.48/1.15 % (3689204)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1039178960:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.48/1.15 % (3689205)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3225776964:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.48/1.15 % (3689205)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.48/1.15 % (3689205)Terminated due to inappropriate strategy. % 6.48/1.15 % (3689205)------------------------------ % 6.48/1.15 % (3689205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.48/1.15 % (3689205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.48/1.15 % (3689205)CaDiCaL version: 2.1.3 % 6.48/1.15 % (3689205)Termination reason: Inappropriate % 6.48/1.15 % (3689205)Time elapsed: 0.003 s % 6.48/1.15 % (3689205)Peak memory usage: 10 MB % 6.48/1.15 % (3689205)Instructions burned: 4 (million) % 6.48/1.15 % (3689205)------------------------------ % 6.48/1.15 % (3689205)------------------------------ % 6.48/1.15 % (3689197)Instruction limit reached! % 6.48/1.15 % (3689197)------------------------------ % 6.48/1.15 % (3689197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.48/1.15 % (3689197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.48/1.15 % (3689197)CaDiCaL version: 2.1.3 % 6.48/1.15 % (3689197)Termination reason: Instruction limit % 6.48/1.15 % (3689197)Termination phase: Saturation % 6.48/1.15 % (3689197)Time elapsed: 0.084 s % 6.48/1.15 % (3689197)Peak memory usage: 12 MB % 6.48/1.15 % (3689197)Instructions burned: 181 (million) % 6.48/1.15 % (3689208)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=1712498802: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) % 21.63/3.37 % (3689209)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=326602588:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.63/3.37 % (3689198)Instruction limit reached! % 21.63/3.37 % (3689198)------------------------------ % 21.63/3.37 % (3689198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.63/3.37 % (3689198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.37 % (3689198)CaDiCaL version: 2.1.3 % 21.63/3.37 % (3689198)Termination reason: Instruction limit % 21.63/3.37 % (3689198)Termination phase: Saturation % 21.63/3.37 % (3689198)Time elapsed: 0.330 s % 21.63/3.37 % (3689198)Peak memory usage: 14 MB % 21.63/3.37 % (3689198)Instructions burned: 477 (million) % 21.63/3.37 % (3689212)fmb+10_1_sil=64000:random_seed=1462478335:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.63/3.37 % (3689212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.63/3.37 % (3689212)Terminated due to inappropriate strategy. % 21.63/3.37 % (3689212)------------------------------ % 21.63/3.37 % (3689212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.63/3.37 % (3689212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.37 % (3689212)CaDiCaL version: 2.1.3 % 21.63/3.37 % (3689212)Termination reason: Inappropriate % 21.63/3.37 % (3689212)Time elapsed: 0.003 s % 21.63/3.37 % (3689212)Peak memory usage: 10 MB % 21.63/3.37 % (3689212)Instructions burned: 5 (million) % 21.63/3.37 % (3689212)------------------------------ % 21.63/3.37 % (3689212)------------------------------ % 21.63/3.37 % (3689214)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=161146435:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.63/3.37 % (3689214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.63/3.37 % (3689214)Terminated due to inappropriate strategy. % 21.63/3.37 % (3689214)------------------------------ % 21.63/3.37 % (3689214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.63/3.37 % (3689214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.37 % (3689214)CaDiCaL version: 2.1.3 % 21.63/3.37 % (3689214)Termination reason: Inappropriate % 21.63/3.37 % (3689214)Time elapsed: 0.003 s % 21.63/3.37 % (3689214)Peak memory usage: 10 MB % 21.63/3.37 % (3689214)Instructions burned: 5 (million) % 21.63/3.37 % (3689214)------------------------------ % 21.63/3.37 % (3689214)------------------------------ % 21.63/3.37 % (3689216)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2762896175:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 21.63/3.37 % (3689216)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.63/3.37 % (3689216)Terminated due to inappropriate strategy. % 21.63/3.37 % (3689216)------------------------------ % 21.63/3.37 % (3689216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.63/3.37 % (3689216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.37 % (3689216)CaDiCaL version: 2.1.3 % 21.63/3.37 % (3689216)Termination reason: Inappropriate % 21.63/3.37 % (3689216)Time elapsed: 0.003 s % 21.63/3.37 % (3689216)Peak memory usage: 10 MB % 21.63/3.37 % (3689216)Instructions burned: 5 (million) % 21.63/3.37 % (3689216)------------------------------ % 21.63/3.37 % (3689216)------------------------------ % 21.63/3.37 % (3689196)Instruction limit reached! % 21.63/3.37 % (3689196)------------------------------ % 21.63/3.37 % (3689196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.63/3.37 % (3689196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.37 % (3689196)CaDiCaL version: 2.1.3 % 21.63/3.37 % (3689196)Termination reason: Instruction limit % 21.63/3.37 % (3689196)Termination phase: Saturation % 21.63/3.37 % (3689196)Time elapsed: 0.434 s % 21.63/3.37 % (3689196)Peak memory usage: 18 MB % 21.63/3.37 % (3689196)Instructions burned: 684 (million) % 21.63/3.37 % (3689218)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=501720923:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 21.63/3.37 % (3689219)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2138721103:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 21.63/3.37 % (3689208)Instruction limit reached! % 21.63/3.37 % (3689208)------------------------------ % 31.76/4.77 % (3689208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689208)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689208)Termination reason: Instruction limit % 31.76/4.77 % (3689208)Termination phase: Saturation % 31.76/4.77 % (3689208)Time elapsed: 0.422 s % 31.76/4.77 % (3689208)Peak memory usage: 17 MB % 31.76/4.77 % (3689208)Instructions burned: 692 (million) % 31.76/4.77 % (3689222)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4066946044:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 31.76/4.77 % (3689222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.76/4.77 % (3689222)Terminated due to inappropriate strategy. % 31.76/4.77 % (3689222)------------------------------ % 31.76/4.77 % (3689222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689222)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689222)Termination reason: Inappropriate % 31.76/4.77 % (3689222)Time elapsed: 0.004 s % 31.76/4.77 % (3689222)Peak memory usage: 10 MB % 31.76/4.77 % (3689222)Instructions burned: 6 (million) % 31.76/4.77 % (3689222)------------------------------ % 31.76/4.77 % (3689222)------------------------------ % 31.76/4.77 % (3689224)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1546149832:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 31.76/4.77 % (3689224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.76/4.77 % (3689224)Terminated due to inappropriate strategy. % 31.76/4.77 % (3689224)------------------------------ % 31.76/4.77 % (3689224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689224)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689224)Termination reason: Inappropriate % 31.76/4.77 % (3689224)Time elapsed: 0.003 s % 31.76/4.77 % (3689224)Peak memory usage: 10 MB % 31.76/4.77 % (3689224)Instructions burned: 5 (million) % 31.76/4.77 % (3689224)------------------------------ % 31.76/4.77 % (3689224)------------------------------ % 31.76/4.77 % (3689226)ott-2_1_sil=16000:newcnf=on:random_seed=1103274972:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 31.76/4.77 % (3689209)Instruction limit reached! % 31.76/4.77 % (3689209)------------------------------ % 31.76/4.77 % (3689209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689209)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689209)Termination reason: Instruction limit % 31.76/4.77 % (3689209)Termination phase: Saturation % 31.76/4.77 % (3689209)Time elapsed: 0.495 s % 31.76/4.77 % (3689209)Peak memory usage: 19 MB % 31.76/4.77 % (3689209)Instructions burned: 880 (million) % 31.76/4.77 % (3689228)ott+10_1_sil=32000:tgt=ground:random_seed=765179130:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 31.76/4.77 % (3689204)Instruction limit reached! % 31.76/4.77 % (3689204)------------------------------ % 31.76/4.77 % (3689204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689204)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689204)Termination reason: Instruction limit % 31.76/4.77 % (3689204)Termination phase: Saturation % 31.76/4.77 % (3689204)Time elapsed: 0.721 s % 31.76/4.77 % (3689204)Peak memory usage: 20 MB % 31.76/4.77 % (3689204)Instructions burned: 1180 (million) % 31.76/4.77 % (3689230)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1955171466:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 31.76/4.77 % (3689230)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.76/4.77 % (3689230)Terminated due to inappropriate strategy. % 31.76/4.77 % (3689230)------------------------------ % 31.76/4.77 % (3689230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.76/4.77 % (3689230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.76/4.77 % (3689230)CaDiCaL version: 2.1.3 % 31.76/4.77 % (3689230)Termination reason: Inappropriate % 31.76/4.77 % (3689230)Time elapsed: 0.004 s % 31.76/4.77 % (3689230)Peak memory usage: 10 MB % 31.76/4.77 % (3689230)Instructions burned: 6 (million) % 111.27/15.97 % (3689230)------------------------------ % 111.27/15.97 % (3689230)------------------------------ % 111.27/15.97 % (3689232)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4006878474:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 111.27/15.97 % (3689226)Instruction limit reached! % 111.27/15.97 % (3689226)------------------------------ % 111.27/15.97 % (3689226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689226)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689226)Termination reason: Instruction limit % 111.27/15.97 % (3689226)Termination phase: Saturation % 111.27/15.97 % (3689226)Time elapsed: 0.512 s % 111.27/15.97 % (3689226)Peak memory usage: 19 MB % 111.27/15.97 % (3689226)Instructions burned: 869 (million) % 111.27/15.97 % (3689234)dis+21_1_sil=32000:sas=cadical:random_seed=4001263359:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 111.27/15.97 % (3689219)Instruction limit reached! % 111.27/15.97 % (3689219)------------------------------ % 111.27/15.97 % (3689219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689219)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689219)Termination reason: Instruction limit % 111.27/15.97 % (3689219)Termination phase: Saturation % 111.27/15.97 % (3689219)Time elapsed: 0.838 s % 111.27/15.97 % (3689219)Peak memory usage: 30 MB % 111.27/15.97 % (3689219)Instructions burned: 1473 (million) % 111.27/15.97 % (3689236)ott+11_1_sil=16000:gs=on:random_seed=2824101401:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 111.27/15.97 % (3689236)Instruction limit reached! % 111.27/15.97 % (3689236)------------------------------ % 111.27/15.97 % (3689236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689236)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689236)Termination reason: Instruction limit % 111.27/15.97 % (3689236)Termination phase: Saturation % 111.27/15.97 % (3689236)Time elapsed: 1.306 s % 111.27/15.97 % (3689236)Peak memory usage: 27 MB % 111.27/15.97 % (3689236)Instructions burned: 2251 (million) % 111.27/15.97 % (3689238)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2193114879:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi) % 111.27/15.97 % (3689238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.27/15.97 % (3689238)Terminated due to inappropriate strategy. % 111.27/15.97 % (3689238)------------------------------ % 111.27/15.97 % (3689238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689238)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689238)Termination reason: Inappropriate % 111.27/15.97 % (3689238)Time elapsed: 0.003 s % 111.27/15.97 % (3689238)Peak memory usage: 10 MB % 111.27/15.97 % (3689238)Instructions burned: 5 (million) % 111.27/15.97 % (3689238)------------------------------ % 111.27/15.97 % (3689238)------------------------------ % 111.27/15.97 % (3689240)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3448165777:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi) % 111.27/15.97 % (3689232)Instruction limit reached! % 111.27/15.97 % (3689232)------------------------------ % 111.27/15.97 % (3689232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689232)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689232)Termination reason: Instruction limit % 111.27/15.97 % (3689232)Termination phase: Saturation % 111.27/15.97 % (3689232)Time elapsed: 1.934 s % 111.27/15.97 % (3689232)Peak memory usage: 34 MB % 111.27/15.97 % (3689232)Instructions burned: 3512 (million) % 111.27/15.97 % (3689242)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=934973374:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 111.27/15.97 % (3689218)Instruction limit reached! % 111.27/15.97 % (3689218)------------------------------ % 111.27/15.97 % (3689218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.27/15.97 % (3689218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.27/15.97 % (3689218)CaDiCaL version: 2.1.3 % 111.27/15.97 % (3689218)Termination reason: Instruction limit % 130.20/18.63 % (3689218)Termination phase: Saturation % 130.20/18.63 % (3689218)Time elapsed: 2.594 s % 130.20/18.63 % (3689218)Peak memory usage: 22 MB % 130.20/18.63 % (3689218)Instructions burned: 5132 (million) % 130.20/18.63 % (3689245)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1603478872:i=5211_2968 on theBenchmark for (2968ds/5211Mi) % 130.20/18.63 % (3689234)Instruction limit reached! % 130.20/18.63 % (3689234)------------------------------ % 130.20/18.63 % (3689234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.20/18.63 % (3689234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.20/18.63 % (3689234)CaDiCaL version: 2.1.3 % 130.20/18.63 % (3689234)Termination reason: Instruction limit % 130.20/18.63 % (3689234)Termination phase: Saturation % 130.20/18.63 % (3689234)Time elapsed: 2.049 s % 130.20/18.63 % (3689234)Peak memory usage: 35 MB % 130.20/18.63 % (3689234)Instructions burned: 3774 (million) % 130.20/18.63 % (3689247)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1039222447:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 130.20/18.63 % (3689247)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.20/18.63 % (3689247)Terminated due to inappropriate strategy. % 130.20/18.63 % (3689247)------------------------------ % 130.20/18.63 % (3689247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.20/18.63 % (3689247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.20/18.63 % (3689247)CaDiCaL version: 2.1.3 % 130.20/18.63 % (3689247)Termination reason: Inappropriate % 130.20/18.63 % (3689247)Time elapsed: 0.004 s % 130.20/18.63 % (3689247)Peak memory usage: 10 MB % 130.20/18.63 % (3689247)Instructions burned: 6 (million) % 130.20/18.63 % (3689247)------------------------------ % 130.20/18.63 % (3689247)------------------------------ % 130.20/18.63 % (3689249)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2446056748:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 130.20/18.63 % (3689249)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.20/18.63 % (3689249)Terminated due to inappropriate strategy. % 130.20/18.63 % (3689249)------------------------------ % 130.20/18.63 % (3689249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.20/18.63 % (3689249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.20/18.63 % (3689249)CaDiCaL version: 2.1.3 % 130.20/18.63 % (3689249)Termination reason: Inappropriate % 130.20/18.63 % (3689249)Time elapsed: 0.003 s % 130.20/18.63 % (3689249)Peak memory usage: 10 MB % 130.20/18.63 % (3689249)Instructions burned: 5 (million) % 130.20/18.63 % (3689249)------------------------------ % 130.20/18.63 % (3689249)------------------------------ % 130.20/18.63 % (3689251)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=815409555:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 130.20/18.63 % (3689251)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.20/18.63 % (3689251)Terminated due to inappropriate strategy. % 130.20/18.63 % (3689251)------------------------------ % 130.20/18.63 % (3689251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.20/18.63 % (3689251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.20/18.63 % (3689251)CaDiCaL version: 2.1.3 % 130.20/18.63 % (3689251)Termination reason: Inappropriate % 130.20/18.63 % (3689251)Time elapsed: 0.003 s % 130.20/18.63 % (3689251)Peak memory usage: 10 MB % 130.20/18.63 % (3689251)Instructions burned: 5 (million) % 130.20/18.63 % (3689251)------------------------------ % 130.20/18.63 % (3689251)------------------------------ % 130.20/18.63 % (3689253)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2134913452:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 130.20/18.63 % (3689228)Instruction limit reached! % 130.20/18.63 % (3689228)------------------------------ % 130.20/18.63 % (3689228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.20/18.63 % (3689228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.20/18.63 % (3689228)CaDiCaL version: 2.1.3 % 130.20/18.63 % (3689228)Termination reason: Instruction limit % 130.20/18.63 % (3689228)Termination phase: Saturation % 130.20/18.63 % (3689228)Time elapsed: 2.835 s % 130.20/18.63 % (3689228)Peak memory usage: 30 MB % 130.20/18.63 % (3689228)Instructions burned: 5114 (million) % 130.20/18.63 % (3689255)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1151709268:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi) % 130.20/18.63 % (3689240)Instruction limit reached! % 130.70/18.75 % (3689240)------------------------------ % 130.70/18.75 % (3689240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689240)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689240)Termination reason: Instruction limit % 130.70/18.75 % (3689240)Termination phase: Saturation % 130.70/18.75 % (3689240)Time elapsed: 1.759 s % 130.70/18.75 % (3689240)Peak memory usage: 35 MB % 130.70/18.75 % (3689240)Instructions burned: 4592 (million) % 130.70/18.75 % (3689257)dis+10_16:1_sil=16000:random_seed=914911118:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 130.70/18.75 % (3689245)Instruction limit reached! % 130.70/18.75 % (3689245)------------------------------ % 130.70/18.75 % (3689245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689245)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689245)Termination reason: Instruction limit % 130.70/18.75 % (3689245)Termination phase: Saturation % 130.70/18.75 % (3689245)Time elapsed: 2.645 s % 130.70/18.75 % (3689245)Peak memory usage: 45 MB % 130.70/18.75 % (3689245)Instructions burned: 5213 (million) % 130.70/18.75 % (3689259)ott-3_8_sil=64000:random_seed=2001608722:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi) % 130.70/18.75 % (3689255)Instruction limit reached! % 130.70/18.75 % (3689255)------------------------------ % 130.70/18.75 % (3689255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689255)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689255)Termination reason: Instruction limit % 130.70/18.75 % (3689255)Termination phase: Saturation % 130.70/18.75 % (3689255)Time elapsed: 4.879 s % 130.70/18.75 % (3689255)Peak memory usage: 53 MB % 130.70/18.75 % (3689255)Instructions burned: 8173 (million) % 130.70/18.75 % (3689261)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=956081381:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 130.70/18.75 % (3689261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.70/18.75 % (3689261)Terminated due to inappropriate strategy. % 130.70/18.75 % (3689261)------------------------------ % 130.70/18.75 % (3689261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689261)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689261)Termination reason: Inappropriate % 130.70/18.75 % (3689261)Time elapsed: 0.004 s % 130.70/18.75 % (3689261)Peak memory usage: 10 MB % 130.70/18.75 % (3689261)Instructions burned: 6 (million) % 130.70/18.75 % (3689261)------------------------------ % 130.70/18.75 % (3689261)------------------------------ % 130.70/18.75 % (3689263)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2863332824:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 130.70/18.75 % (3689257)Instruction limit reached! % 130.70/18.75 % (3689257)------------------------------ % 130.70/18.75 % (3689257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689257)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689257)Termination reason: Instruction limit % 130.70/18.75 % (3689257)Termination phase: Saturation % 130.70/18.75 % (3689257)Time elapsed: 4.738 s % 130.70/18.75 % (3689257)Peak memory usage: 54 MB % 130.70/18.75 % (3689257)Instructions burned: 9155 (million) % 130.70/18.75 % (3689265)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2900067002:i=14134_2906 on theBenchmark for (2906ds/14134Mi) % 130.70/18.75 % (3689253)Instruction limit reached! % 130.70/18.75 % (3689253)------------------------------ % 130.70/18.75 % (3689253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.70/18.75 % (3689253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.70/18.75 % (3689253)CaDiCaL version: 2.1.3 % 130.70/18.75 % (3689253)Termination reason: Instruction limit % 130.70/18.75 % (3689253)Termination phase: Saturation % 130.70/18.75 % (3689253)Time elapsed: 9.503 s % 130.70/18.75 % (3689253)Peak memory usage: 85 MB % 130.70/18.75 % (3689253)Instructions burned: 22567 (million) % 130.70/18.75 % (3689267)dis+33_16_sil=32000:sac=on:random_seed=2994786329:i=15851:nm=0_2871 on theBenchmark for (2871ds/15851Mi) % 130.70/18.75 % (3689263)Instruction limit reached! % 130.70/18.75 % (3689263)------------------------------ % 130.70/18.75 % (3689263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689263)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689263)Termination reason: Instruction limit % 155.82/22.28 % (3689263)Termination phase: Saturation % 155.82/22.28 % (3689263)Time elapsed: 7.217 s % 155.82/22.28 % (3689263)Peak memory usage: 67 MB % 155.82/22.28 % (3689263)Instructions burned: 11405 (million) % 155.82/22.28 % (3689269)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1223067841:avsq=on:i=17627:add=on:amm=off_2842 on theBenchmark for (2842ds/17627Mi) % 155.82/22.28 % (3689259)Instruction limit reached! % 155.82/22.28 % (3689259)------------------------------ % 155.82/22.28 % (3689259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689259)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689259)Termination reason: Instruction limit % 155.82/22.28 % (3689259)Termination phase: Saturation % 155.82/22.28 % (3689259)Time elapsed: 12.290 s % 155.82/22.28 % (3689259)Peak memory usage: 82 MB % 155.82/22.28 % (3689259)Instructions burned: 20139 (million) % 155.82/22.28 % (3689271)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=698676631:s2a=on:i=53295_2818 on theBenchmark for (2818ds/53295Mi) % 155.82/22.28 % (3689265)Instruction limit reached! % 155.82/22.28 % (3689265)------------------------------ % 155.82/22.28 % (3689265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689265)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689265)Termination reason: Instruction limit % 155.82/22.28 % (3689265)Termination phase: Saturation % 155.82/22.28 % (3689265)Time elapsed: 9.0000 s % 155.82/22.28 % (3689265)Peak memory usage: 73 MB % 155.82/22.28 % (3689265)Instructions burned: 14134 (million) % 155.82/22.28 % (3689242)Instruction limit reached! % 155.82/22.28 % (3689242)------------------------------ % 155.82/22.28 % (3689242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689242)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689242)Termination reason: Instruction limit % 155.82/22.28 % (3689242)Termination phase: Saturation % 155.82/22.28 % (3689242)Time elapsed: 15.433 s % 155.82/22.28 % (3689242)Peak memory usage: 78 MB % 155.82/22.28 % (3689242)Instructions burned: 29340 (million) % 155.82/22.28 % (3689273)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2900202342:i=26857:ins=20_2816 on theBenchmark for (2816ds/26857Mi) % 155.82/22.28 % (3689273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.82/22.28 % (3689273)Terminated due to inappropriate strategy. % 155.82/22.28 % (3689273)------------------------------ % 155.82/22.28 % (3689273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689273)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689273)Termination reason: Inappropriate % 155.82/22.28 % (3689273)Time elapsed: 0.003 s % 155.82/22.28 % (3689273)Peak memory usage: 10 MB % 155.82/22.28 % (3689273)Instructions burned: 5 (million) % 155.82/22.28 % (3689274)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2073033955:i=28120:bs=on:fsr=off_2816 on theBenchmark for (2816ds/28120Mi) % 155.82/22.28 % (3689273)------------------------------ % 155.82/22.28 % (3689273)------------------------------ % 155.82/22.28 % (3689277)fmb+10_1_sil=256000:fmbss=7:random_seed=1980231654:fmbsr=1.6:i=182295_2816 on theBenchmark for (2816ds/182295Mi) % 155.82/22.28 % (3689277)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.82/22.28 % (3689277)Terminated due to inappropriate strategy. % 155.82/22.28 % (3689277)------------------------------ % 155.82/22.28 % (3689277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.82/22.28 % (3689277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.82/22.28 % (3689277)CaDiCaL version: 2.1.3 % 155.82/22.28 % (3689277)Termination reason: Inappropriate % 155.82/22.28 % (3689277)Time elapsed: 0.003 s % 155.82/22.28 % (3689277)Peak memory usage: 10 MB % 155.82/22.28 % (3689277)Instructions burned: 5 (million) % 155.82/22.28 % (3689277)------------------------------ % 155.82/22.28 % (3689277)------------------------------ % 155.82/22.28 % (3689279)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1299169064:i=44625:gsp=on_2816 on theBenchmark for (2816ds/44625Mi) % 170.21/24.21 % (3689279)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.21/24.21 % (3689279)Terminated due to inappropriate strategy. % 170.21/24.21 % (3689279)------------------------------ % 170.21/24.21 % (3689279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.21/24.21 % (3689279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.21/24.21 % (3689279)CaDiCaL version: 2.1.3 % 170.21/24.21 % (3689279)Termination reason: Inappropriate % 170.21/24.21 % (3689279)Time elapsed: 0.003 s % 170.21/24.21 % (3689279)Peak memory usage: 10 MB % 170.21/24.21 % (3689279)Instructions burned: 5 (million) % 170.21/24.21 % (3689279)------------------------------ % 170.21/24.21 % (3689279)------------------------------ % 170.21/24.21 % (3689281)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1440638603:i=160505_2815 on theBenchmark for (2815ds/160505Mi) % 170.21/24.21 % (3689281)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.21/24.21 % (3689281)Terminated due to inappropriate strategy. % 170.21/24.21 % (3689281)------------------------------ % 170.21/24.21 % (3689281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.21/24.21 % (3689281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.21/24.21 % (3689281)CaDiCaL version: 2.1.3 % 170.21/24.21 % (3689281)Termination reason: Inappropriate % 170.21/24.21 % (3689281)Time elapsed: 0.003 s % 170.21/24.21 % (3689281)Peak memory usage: 10 MB % 170.21/24.21 % (3689281)Instructions burned: 5 (million) % 170.21/24.21 % (3689281)------------------------------ % 170.21/24.21 % (3689281)------------------------------ % 170.21/24.21 % (3689283)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3830838248:fmbsr=1.3:i=225729_2815 on theBenchmark for (2815ds/225729Mi) % 170.21/24.21 % (3689283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.21/24.21 % (3689283)Terminated due to inappropriate strategy. % 170.21/24.21 % (3689283)------------------------------ % 170.21/24.21 % (3689283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.21/24.21 % (3689283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.21/24.21 % (3689283)CaDiCaL version: 2.1.3 % 170.21/24.21 % (3689283)Termination reason: Inappropriate % 170.21/24.21 % (3689283)Time elapsed: 0.003 s % 170.21/24.21 % (3689283)Peak memory usage: 10 MB % 170.21/24.21 % (3689283)Instructions burned: 5 (million) % 170.21/24.21 % (3689283)------------------------------ % 170.21/24.21 % (3689283)------------------------------ % 170.21/24.21 % (3689285)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1520650084:fmbsr=2:i=185024:ins=7_2815 on theBenchmark for (2815ds/185024Mi) % 170.21/24.21 % (3689285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.21/24.21 % (3689285)Terminated due to inappropriate strategy. % 170.21/24.21 % (3689285)------------------------------ % 170.21/24.21 % (3689285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.21/24.21 % (3689285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.21/24.21 % (3689285)CaDiCaL version: 2.1.3 % 170.21/24.21 % (3689285)Termination reason: Inappropriate % 170.21/24.21 % (3689285)Time elapsed: 0.003 s % 170.21/24.21 % (3689285)Peak memory usage: 10 MB % 170.21/24.21 % (3689285)Instructions burned: 5 (million) % 170.21/24.21 % (3689285)------------------------------ % 170.21/24.21 % (3689285)------------------------------ % 170.21/24.21 % (3689287)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=510353974:rtra=on_2815 on theBenchmark for (2815ds/0Mi) % 170.21/24.21 % (3689287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.21/24.21 % (3689287)Terminated due to inappropriate strategy. % 170.21/24.21 % (3689287)------------------------------ % 170.21/24.21 % (3689287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.21/24.21 % (3689287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.21/24.21 % (3689287)CaDiCaL version: 2.1.3 % 170.21/24.21 % (3689287)Termination reason: Inappropriate % 170.21/24.21 % (3689287)Time elapsed: 0.004 s % 170.21/24.21 % (3689287)Peak memory usage: 10 MB % 170.21/24.21 % (3689287)Instructions burned: 7 (million) % 170.21/24.21 % (3689287)------------------------------ % 170.21/24.21 % (3689287)------------------------------ % 170.21/24.21 % (3689289)% WARNING: option uhcvi not known. % 170.21/24.21 % (3689289)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3586637822:i=271062:add=off:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/271062Mi) % 183.95/26.18 % (3689180)Instruction limit reached! % 183.95/26.18 % (3689180)------------------------------ % 183.95/26.18 % (3689180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689180)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689180)Termination reason: Instruction limit % 183.95/26.18 % (3689180)Termination phase: Saturation % 183.95/26.18 % (3689180)Time elapsed: 18.819 s % 183.95/26.18 % (3689180)Peak memory usage: 140 MB % 183.95/26.18 % (3689180)Instructions burned: 88030 (million) % 183.95/26.18 % (3689291)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1610189904:i=176048:add=on:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/176048Mi) % 183.95/26.18 % (3689267)Instruction limit reached! % 183.95/26.18 % (3689267)------------------------------ % 183.95/26.18 % (3689267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689267)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689267)Termination reason: Instruction limit % 183.95/26.18 % (3689267)Termination phase: Saturation % 183.95/26.18 % (3689267)Time elapsed: 8.359 s % 183.95/26.18 % (3689267)Peak memory usage: 121 MB % 183.95/26.18 % (3689267)Instructions burned: 15852 (million) % 183.95/26.18 % (3689293)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4072930024:i=206:fgj=on:rtra=on_2787 on theBenchmark for (2787ds/206Mi) % 183.95/26.18 % (3689293)Instruction limit reached! % 183.95/26.18 % (3689293)------------------------------ % 183.95/26.18 % (3689293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689293)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689293)Termination reason: Instruction limit % 183.95/26.18 % (3689293)Termination phase: Saturation % 183.95/26.18 % (3689293)Time elapsed: 0.132 s % 183.95/26.18 % (3689293)Peak memory usage: 14 MB % 183.95/26.18 % (3689293)Instructions burned: 206 (million) % 183.95/26.18 % (3689295)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4194527024:i=232:rtra=on_2785 on theBenchmark for (2785ds/232Mi) % 183.95/26.18 % (3689295)Instruction limit reached! % 183.95/26.18 % (3689295)------------------------------ % 183.95/26.18 % (3689295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689295)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689295)Termination reason: Instruction limit % 183.95/26.18 % (3689295)Termination phase: Saturation % 183.95/26.18 % (3689295)Time elapsed: 0.148 s % 183.95/26.18 % (3689295)Peak memory usage: 14 MB % 183.95/26.18 % (3689295)Instructions burned: 233 (million) % 183.95/26.18 % (3689297)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3623990889:i=262:rtra=on_2783 on theBenchmark for (2783ds/262Mi) % 183.95/26.18 % (3689297)Instruction limit reached! % 183.95/26.18 % (3689297)------------------------------ % 183.95/26.18 % (3689297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689297)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689297)Termination reason: Instruction limit % 183.95/26.18 % (3689297)Termination phase: Saturation % 183.95/26.18 % (3689297)Time elapsed: 0.162 s % 183.95/26.18 % (3689297)Peak memory usage: 14 MB % 183.95/26.18 % (3689297)Instructions burned: 263 (million) % 183.95/26.18 % (3689299)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3179621408:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2782 on theBenchmark for (2782ds/318Mi) % 183.95/26.18 % (3689299)Instruction limit reached! % 183.95/26.18 % (3689299)------------------------------ % 183.95/26.18 % (3689299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.95/26.18 % (3689299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.95/26.18 % (3689299)CaDiCaL version: 2.1.3 % 183.95/26.18 % (3689299)Termination reason: Instruction limit % 183.95/26.18 % (3689299)Termination phase: Saturation % 183.95/26.18 % (3689299)Time elapsed: 0.226 s % 183.95/26.18 % (3689299)Peak memory usage: 16 MB % 183.95/26.18 % (3689299)Instructions burned: 319 (million) % 183.95/26.18 % (3689301)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1240182235:i=1428:nm=2:rtra=on_2779 on theBenchmark for (2779ds/1428Mi) % 200.16/28.75 % (3689301)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.16/28.75 % (3689301)Terminated due to inappropriate strategy. % 200.16/28.75 % (3689301)------------------------------ % 200.16/28.75 % (3689301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689301)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689301)Termination reason: Inappropriate % 200.16/28.75 % (3689301)Time elapsed: 0.003 s % 200.16/28.75 % (3689301)Peak memory usage: 10 MB % 200.16/28.75 % (3689301)Instructions burned: 5 (million) % 200.16/28.75 % (3689301)------------------------------ % 200.16/28.75 % (3689301)------------------------------ % 200.16/28.75 % (3689303)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=507730303:i=262:bd=preordered:rtra=on:fsd=on_2779 on theBenchmark for (2779ds/262Mi) % 200.16/28.75 % (3689303)Instruction limit reached! % 200.16/28.75 % (3689303)------------------------------ % 200.16/28.75 % (3689303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689303)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689303)Termination reason: Instruction limit % 200.16/28.75 % (3689303)Termination phase: Saturation % 200.16/28.75 % (3689303)Time elapsed: 0.150 s % 200.16/28.75 % (3689303)Peak memory usage: 13 MB % 200.16/28.75 % (3689303)Instructions burned: 263 (million) % 200.16/28.75 % (3689305)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=3644808790:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/1368Mi) % 200.16/28.75 % (3689305)Instruction limit reached! % 200.16/28.75 % (3689305)------------------------------ % 200.16/28.75 % (3689305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689305)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689305)Termination reason: Instruction limit % 200.16/28.75 % (3689305)Termination phase: Saturation % 200.16/28.75 % (3689305)Time elapsed: 0.857 s % 200.16/28.75 % (3689305)Peak memory usage: 24 MB % 200.16/28.75 % (3689305)Instructions burned: 1368 (million) % 200.16/28.75 % (3689307)ott-21_1_sil=16000:si=on:fs=off:random_seed=317105243:i=360:av=off:fsr=off:rtra=on_2768 on theBenchmark for (2768ds/360Mi) % 200.16/28.75 % (3689307)Instruction limit reached! % 200.16/28.75 % (3689307)------------------------------ % 200.16/28.75 % (3689307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689307)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689307)Termination reason: Instruction limit % 200.16/28.75 % (3689307)Termination phase: Saturation % 200.16/28.75 % (3689307)Time elapsed: 0.165 s % 200.16/28.75 % (3689307)Peak memory usage: 13 MB % 200.16/28.75 % (3689307)Instructions burned: 362 (million) % 200.16/28.75 % (3689309)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=211860222:i=954:bd=all:rtra=on_2767 on theBenchmark for (2767ds/954Mi) % 200.16/28.75 % (3689309)Instruction limit reached! % 200.16/28.75 % (3689309)------------------------------ % 200.16/28.75 % (3689309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689309)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689309)Termination reason: Instruction limit % 200.16/28.75 % (3689309)Termination phase: Saturation % 200.16/28.75 % (3689309)Time elapsed: 0.653 s % 200.16/28.75 % (3689309)Peak memory usage: 17 MB % 200.16/28.75 % (3689309)Instructions burned: 954 (million) % 200.16/28.75 % (3689311)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2095681526:fmbsr=1.3:i=1730:ins=25:rtra=on_2760 on theBenchmark for (2760ds/1730Mi) % 200.16/28.75 % (3689311)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.16/28.75 % (3689311)Terminated due to inappropriate strategy. % 200.16/28.75 % (3689311)------------------------------ % 200.16/28.75 % (3689311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.16/28.75 % (3689311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.16/28.75 % (3689311)CaDiCaL version: 2.1.3 % 200.16/28.75 % (3689311)Termination reason: Inappropriate % 200.16/28.75 % (3689311)Time elapsed: 0.003 s % 254.92/36.15 % (3689311)Peak memory usage: 10 MB % 254.92/36.15 % (3689311)Instructions burned: 4 (million) % 254.92/36.15 % (3689311)------------------------------ % 254.92/36.15 % (3689311)------------------------------ % 254.92/36.15 % (3689313)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2795421495:i=2358:rtra=on_2760 on theBenchmark for (2760ds/2358Mi) % 254.92/36.15 % (3689269)Instruction limit reached! % 254.92/36.15 % (3689269)------------------------------ % 254.92/36.15 % (3689269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.92/36.15 % (3689269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.92/36.15 % (3689269)CaDiCaL version: 2.1.3 % 254.92/36.15 % (3689269)Termination reason: Instruction limit % 254.92/36.15 % (3689269)Termination phase: Saturation % 254.92/36.15 % (3689269)Time elapsed: 9.305 s % 254.92/36.15 % (3689269)Peak memory usage: 143 MB % 254.92/36.15 % (3689269)Instructions burned: 17627 (million) % 254.92/36.15 % (3689315)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=620458417:i=1778:ins=1:rtra=on_2748 on theBenchmark for (2748ds/1778Mi) % 254.92/36.15 % (3689315)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 254.92/36.15 % (3689315)Terminated due to inappropriate strategy. % 254.92/36.15 % (3689315)------------------------------ % 254.92/36.15 % (3689315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.92/36.15 % (3689315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.92/36.15 % (3689315)CaDiCaL version: 2.1.3 % 254.92/36.15 % (3689315)Termination reason: Inappropriate % 254.92/36.15 % (3689315)Time elapsed: 0.003 s % 254.92/36.15 % (3689315)Peak memory usage: 10 MB % 254.92/36.15 % (3689315)Instructions burned: 5 (million) % 254.92/36.15 % (3689315)------------------------------ % 254.92/36.15 % (3689315)------------------------------ % 254.92/36.15 % (3689317)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=3144578225:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1384Mi) % 254.92/36.15 % (3689313)Instruction limit reached! % 254.92/36.15 % (3689313)------------------------------ % 254.92/36.15 % (3689313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.92/36.15 % (3689313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.92/36.15 % (3689313)CaDiCaL version: 2.1.3 % 254.92/36.15 % (3689313)Termination reason: Instruction limit % 254.92/36.15 % (3689313)Termination phase: Saturation % 254.92/36.15 % (3689313)Time elapsed: 1.507 s % 254.92/36.15 % (3689313)Peak memory usage: 26 MB % 254.92/36.15 % (3689313)Instructions burned: 2359 (million) % 254.92/36.15 % (3689319)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=328027295:i=1758:kws=inv_precedence:fsr=off:rtra=on_2744 on theBenchmark for (2744ds/1758Mi) % 254.92/36.15 % (3689317)Instruction limit reached! % 254.92/36.15 % (3689317)------------------------------ % 254.92/36.15 % (3689317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.92/36.15 % (3689317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.92/36.15 % (3689317)CaDiCaL version: 2.1.3 % 254.92/36.15 % (3689317)Termination reason: Instruction limit % 254.92/36.15 % (3689317)Termination phase: Saturation % 254.92/36.15 % (3689317)Time elapsed: 0.772 s % 254.92/36.15 % (3689317)Peak memory usage: 33 MB % 254.92/36.15 % (3689317)Instructions burned: 1385 (million) % 254.92/36.15 % (3689321)fmb+10_1_sil=64000:si=on:random_seed=2576774194:i=44122:nm=2:rtra=on:gsp=on_2740 on theBenchmark for (2740ds/44122Mi) % 254.92/36.15 % (3689321)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 254.92/36.15 % (3689321)Terminated due to inappropriate strategy. % 254.92/36.15 % (3689321)------------------------------ % 254.92/36.15 % (3689321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.92/36.15 % (3689321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.92/36.15 % (3689321)CaDiCaL version: 2.1.3 % 254.92/36.15 % (3689321)Termination reason: Inappropriate % 254.92/36.15 % (3689321)Time elapsed: 0.003 s % 254.92/36.15 % (3689321)Peak memory usage: 10 MB % 254.92/36.15 % (3689321)Instructions burned: 6 (million) % 254.92/36.15 % (3689321)------------------------------ % 254.92/36.15 % (3689321)------------------------------ % 254.92/36.15 % (3689323)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=51861040:i=19030:nm=5:rtra=on_2740 on theBenchmark for (2740ds/19030Mi) % 286.60/40.65 % (3689323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.60/40.65 % (3689323)Terminated due to inappropriate strategy. % 286.60/40.65 % (3689323)------------------------------ % 286.60/40.65 % (3689323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.60/40.65 % (3689323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.60/40.65 % (3689323)CaDiCaL version: 2.1.3 % 286.60/40.65 % (3689323)Termination reason: Inappropriate % 286.60/40.65 % (3689323)Time elapsed: 0.003 s % 286.60/40.65 % (3689323)Peak memory usage: 10 MB % 286.60/40.65 % (3689323)Instructions burned: 5 (million) % 286.60/40.65 % (3689323)------------------------------ % 286.60/40.65 % (3689323)------------------------------ % 286.60/40.65 % (3689325)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=256405342:fmbsr=1.7:i=1840:rtra=on_2740 on theBenchmark for (2740ds/1840Mi) % 286.60/40.65 % (3689325)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.60/40.65 % (3689325)Terminated due to inappropriate strategy. % 286.60/40.65 % (3689325)------------------------------ % 286.60/40.65 % (3689325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.60/40.65 % (3689325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.60/40.65 % (3689325)CaDiCaL version: 2.1.3 % 286.60/40.65 % (3689325)Termination reason: Inappropriate % 286.60/40.65 % (3689325)Time elapsed: 0.003 s % 286.60/40.65 % (3689325)Peak memory usage: 10 MB % 286.60/40.65 % (3689325)Instructions burned: 5 (million) % 286.60/40.65 % (3689325)------------------------------ % 286.60/40.65 % (3689325)------------------------------ % 286.60/40.65 % (3689327)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=837491311:i=10262:rtra=on_2740 on theBenchmark for (2740ds/10262Mi) % 286.60/40.65 % (3689319)Instruction limit reached! % 286.60/40.65 % (3689319)------------------------------ % 286.60/40.65 % (3689319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.60/40.65 % (3689319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.60/40.65 % (3689319)CaDiCaL version: 2.1.3 % 286.60/40.65 % (3689319)Termination reason: Instruction limit % 286.60/40.65 % (3689319)Termination phase: Saturation % 286.60/40.65 % (3689319)Time elapsed: 0.983 s % 286.60/40.65 % (3689319)Peak memory usage: 25 MB % 286.60/40.65 % (3689319)Instructions burned: 1759 (million) % 286.60/40.65 % (3689329)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1563638019:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2734 on theBenchmark for (2734ds/2944Mi) % 286.60/40.65 % (3689329)Instruction limit reached! % 286.60/40.65 % (3689329)------------------------------ % 286.60/40.65 % (3689329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.60/40.65 % (3689329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.60/40.65 % (3689329)CaDiCaL version: 2.1.3 % 286.60/40.65 % (3689329)Termination reason: Instruction limit % 286.60/40.65 % (3689329)Termination phase: Saturation % 286.60/40.65 % (3689329)Time elapsed: 1.925 s % 286.60/40.65 % (3689329)Peak memory usage: 46 MB % 286.60/40.65 % (3689329)Instructions burned: 2945 (million) % 286.60/40.65 % (3689331)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=822960973:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 286.60/40.65 % (3689331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.60/40.65 % (3689331)Terminated due to inappropriate strategy. % 286.60/40.65 % (3689331)------------------------------ % 286.60/40.65 % (3689331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.60/40.65 % (3689331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.60/40.65 % (3689331)CaDiCaL version: 2.1.3 % 286.60/40.65 % (3689331)Termination reason: Inappropriate % 286.60/40.65 % (3689331)Time elapsed: 0.004 s % 286.60/40.65 % (3689331)Peak memory usage: 10 MB % 286.60/40.65 % (3689331)Instructions burned: 6 (million) % 286.60/40.65 % (3689331)------------------------------ % 286.60/40.65 % (3689331)------------------------------ % 286.60/40.65 % (3689333)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2106172098:fmbsr=2.30978:i=4348:rtra=on_2714 on theBenchmark for (2714ds/4348Mi) % 286.60/40.65 % (3689333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.60/40.65 % (3689333)Terminated due to inappropriate strategy. % 286.60/40.65 % (3689333)------------------------------ % 286.60/40.65 % (3689333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.53 % (3689333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.53 % (3689333)CaDiCaL version: 2.1.3 % 300.08/42.53 % (3689333)Termination reason: Inappropriate % 300.08/42.53 % (3689333)Time elapsed: 0.003 s % 300.08/42.53 % (3689333)Peak memory usage: 10 MB % 300.08/42.53 % (3689333)Instructions burned: 5 (million) % 300.08/42.53 % (3689333)------------------------------ % 300.08/42.53 % (3689333)------------------------------ % 300.08/42.53 % (3689335)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1278427050:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2714 on theBenchmark for (2714ds/1738Mi) % 300.08/42.53 % (3689335)Instruction limit reached! % 300.08/42.53 % (3689335)------------------------------ % 300.08/42.53 % (3689335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.53 % (3689335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.53 % (3689335)CaDiCaL version: 2.1.3 % 300.08/42.53 % (3689335)Termination reason: Instruction limit % 300.08/42.53 % (3689335)Termination phase: Saturation % 300.08/42.53 % (3689335)Time elapsed: 1.091 s % 300.08/42.54 % (3689335)Peak memory usage: 26 MB % 300.08/42.54 % (3689335)Instructions burned: 1740 (million) % 300.08/42.54 % (3689337)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2330060800:i=10228:av=off:rtra=on_2703 on theBenchmark for (2703ds/10228Mi) % 300.08/42.54 % (3689274)Instruction limit reached! % 300.08/42.54 % (3689274)------------------------------ % 300.08/42.54 % (3689274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.54 % (3689274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.54 % (3689274)CaDiCaL version: 2.1.3 % 300.08/42.54 % (3689274)Termination reason: Instruction limit % 300.08/42.54 % (3689274)Termination phase: Saturation % 300.08/42.54 % (3689274)Time elapsed: 13.381 s % 300.08/42.54 % (3689274)Peak memory usage: 57 MB % 300.08/42.54 % (3689274)Instructions burned: 28120 (million) % 300.08/42.54 % (3689339)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3610985618:i=108564:rtra=on_2682 on theBenchmark for (2682ds/108564Mi) % 300.08/42.54 % (3689339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.08/42.54 % (3689339)Terminated due to inappropriate strategy. % 300.08/42.54 % (3689339)------------------------------ % 300.08/42.54 % (3689339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.54 % (3689339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.54 % (3689339)CaDiCaL version: 2.1.3 % 300.08/42.54 % (3689339)Termination reason: Inappropriate % 300.08/42.54 % (3689339)Time elapsed: 0.004 s % 300.08/42.54 % (3689339)Peak memory usage: 10 MB % 300.08/42.54 % (3689339)Instructions burned: 6 (million) % 300.08/42.54 % (3689339)------------------------------ % 300.08/42.54 % (3689339)------------------------------ % 300.08/42.54 % (3689341)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2219937523:i=7024:aac=none:rtra=on_2682 on theBenchmark for (2682ds/7024Mi) % 300.08/42.54 % (3689327)Instruction limit reached! % 300.08/42.54 % (3689327)------------------------------ % 300.08/42.54 % (3689327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.54 % (3689327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.54 % (3689327)CaDiCaL version: 2.1.3 % 300.08/42.54 % (3689327)Termination reason: Instruction limit % 300.08/42.54 % (3689327)Termination phase: Saturation % 300.08/42.54 % (3689327)Time elapsed: 5.923 s % 300.08/42.54 % (3689327)Peak memory usage: 62 MB % 300.08/42.54 % (3689327)Instructions burned: 10264 (million) % 300.08/42.54 % (3689343)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3956729747:i=7546:rtra=on:amm=off_2680 on theBenchmark for (2680ds/7546Mi) % 300.08/42.54 % (3689341)Instruction limit reached! % 300.08/42.54 % (3689341)------------------------------ % 300.08/42.54 % (3689341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.54 % (3689341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.54 % (3689341)CaDiCaL version: 2.1.3 % 300.08/42.54 % (3689341)Termination reason: Instruction limit % 300.08/42.54 % (3689341)Termination phase: Saturation % 300.08/42.54 % (3689341)Time elapsed: 4.095 s % 300.08/42.54 % (3689341)Peak memory usage: 62 MB % 300.08/42.54 % (3689341)Instructions burned: 7025 (million) % 300.08/42.54 % (3689345)ott+11_1_sil=16000:si=on:gs=on:random_seed=1849316640:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2640 on theBenchmark for (2 % 300.08/42.54 Terminated % 300.08/42.54 % Vampire exiting %------------------------------------------------------------------------------