%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW843_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:03 PM UTC 2026 % Result : Timeout 300.01s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW843_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n013.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 14:31:57 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.23/0.74 % (1226962)Will run a generic schedule for satisfiability detection. % 3.23/0.74 % (1226971)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2883669656:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.23/0.74 % (1226968)% WARNING: option uhcvi not known. % 3.23/0.74 % (1226967)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3992120439_2999 on theBenchmark for (2999ds/0Mi) % 3.23/0.74 % (1226968)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=942145155:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.23/0.74 % (1226969)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3131127811:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.23/0.74 % (1226970)dis+10_1_sil=32000:sp=arity:random_seed=1197892660:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.23/0.74 % (1226972)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=883635462:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.23/0.74 % (1226973)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3987267761:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.23/0.74 % (1226967)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.74 % (1226967)Terminated due to inappropriate strategy. % 3.23/0.74 % (1226967)------------------------------ % 3.23/0.74 % (1226967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.74 % (1226967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.74 % (1226967)CaDiCaL version: 2.1.3 % 3.23/0.74 % (1226967)Termination reason: Inappropriate % 3.23/0.74 % (1226967)Time elapsed: 0.025 s % 3.23/0.74 % (1226967)Peak memory usage: 11 MB % 3.23/0.74 % (1226967)Instructions burned: 55 (million) % 3.23/0.74 % (1226967)------------------------------ % 3.23/0.74 % (1226967)------------------------------ % 3.23/0.74 % (1226971)Instruction limit reached! % 3.23/0.74 % (1226971)------------------------------ % 3.23/0.74 % (1226971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.74 % (1226971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.74 % (1226971)CaDiCaL version: 2.1.3 % 3.23/0.74 % (1226971)Termination reason: Instruction limit % 3.23/0.74 % (1226971)Termination phase: Saturation % 3.23/0.74 % (1226971)Time elapsed: 0.036 s % 3.23/0.74 % (1226971)Peak memory usage: 13 MB % 3.23/0.74 % (1226971)Instructions burned: 119 (million) % 3.23/0.74 % (1226982)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=909976283:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.23/0.74 % (1226981)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1565337038:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.23/0.74 % (1226970)Instruction limit reached! % 3.23/0.74 % (1226970)------------------------------ % 3.23/0.74 % (1226970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.74 % (1226970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.74 % (1226970)CaDiCaL version: 2.1.3 % 3.23/0.74 % (1226970)Termination reason: Instruction limit % 3.23/0.74 % (1226970)Termination phase: Saturation % 3.23/0.74 % (1226970)Time elapsed: 0.056 s % 3.23/0.74 % (1226970)Peak memory usage: 13 MB % 3.23/0.74 % (1226970)Instructions burned: 104 (million) % 3.23/0.74 % (1226972)Instruction limit reached! % 3.23/0.74 % (1226972)------------------------------ % 3.23/0.74 % (1226972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.74 % (1226972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.74 % (1226972)CaDiCaL version: 2.1.3 % 3.23/0.74 % (1226972)Termination reason: Instruction limit % 3.23/0.74 % (1226972)Termination phase: Saturation % 3.23/0.74 % (1226972)Time elapsed: 0.070 s % 3.23/0.74 % (1226972)Peak memory usage: 14 MB % 3.23/0.74 % (1226972)Instructions burned: 132 (million) % 3.23/0.74 % (1226981)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.74 % (1226981)Terminated due to inappropriate strategy. % 3.23/0.74 % (1226981)------------------------------ % 3.23/0.74 % (1226981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.74 % (1226981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.74 % (1226981)CaDiCaL version: 2.1.3 % 3.23/0.74 % (1226981)Termination reason: Inappropriate % 3.23/0.74 % (1226981)Time elapsed: 0.025 s % 5.59/1.08 % (1226981)Peak memory usage: 11 MB % 5.59/1.08 % (1226981)Instructions burned: 55 (million) % 5.59/1.08 % (1226981)------------------------------ % 5.59/1.08 % (1226981)------------------------------ % 5.59/1.08 % (1226985)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=2247181571:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.59/1.08 % (1226982)Instruction limit reached! % 5.59/1.08 % (1226982)------------------------------ % 5.59/1.08 % (1226982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.59/1.08 % (1226982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.08 % (1226982)CaDiCaL version: 2.1.3 % 5.59/1.08 % (1226982)Termination reason: Instruction limit % 5.59/1.08 % (1226982)Termination phase: Saturation % 5.59/1.08 % (1226982)Time elapsed: 0.040 s % 5.59/1.08 % (1226982)Peak memory usage: 14 MB % 5.59/1.08 % (1226982)Instructions burned: 131 (million) % 5.59/1.08 % (1226973)Instruction limit reached! % 5.59/1.08 % (1226973)------------------------------ % 5.59/1.08 % (1226973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.59/1.08 % (1226973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.08 % (1226973)CaDiCaL version: 2.1.3 % 5.59/1.08 % (1226973)Termination reason: Instruction limit % 5.59/1.08 % (1226973)Termination phase: Saturation % 5.59/1.08 % (1226973)Time elapsed: 0.087 s % 5.59/1.08 % (1226973)Peak memory usage: 14 MB % 5.59/1.08 % (1226973)Instructions burned: 159 (million) % 5.59/1.08 % (1226989)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1218567988:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.59/1.08 % (1226986)ott-21_1_sil=16000:fs=off:random_seed=3896665375:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.59/1.08 % (1226987)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=585662199:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.59/1.08 % (1226989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.59/1.08 % (1226989)Terminated due to inappropriate strategy. % 5.59/1.08 % (1226989)------------------------------ % 5.59/1.08 % (1226989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.59/1.08 % (1226989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.08 % (1226989)CaDiCaL version: 2.1.3 % 5.59/1.08 % (1226989)Termination reason: Inappropriate % 5.59/1.08 % (1226989)Time elapsed: 0.013 s % 5.59/1.08 % (1226989)Peak memory usage: 11 MB % 5.59/1.08 % (1226989)Instructions burned: 55 (million) % 5.59/1.08 % (1226989)------------------------------ % 5.59/1.08 % (1226989)------------------------------ % 5.59/1.08 % (1226990)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4260243642:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.59/1.08 % (1226994)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3883651483:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.59/1.08 % (1226994)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.59/1.08 % (1226994)Terminated due to inappropriate strategy. % 5.59/1.08 % (1226994)------------------------------ % 5.59/1.08 % (1226994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.59/1.08 % (1226994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.08 % (1226994)CaDiCaL version: 2.1.3 % 5.59/1.08 % (1226994)Termination reason: Inappropriate % 5.59/1.08 % (1226994)Time elapsed: 0.013 s % 5.59/1.08 % (1226994)Peak memory usage: 11 MB % 5.59/1.08 % (1226994)Instructions burned: 55 (million) % 5.59/1.08 % (1226994)------------------------------ % 5.59/1.08 % (1226994)------------------------------ % 5.59/1.08 % (1226997)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=1638930169: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.59/1.08 % (1226986)Instruction limit reached! % 5.59/1.08 % (1226986)------------------------------ % 5.59/1.08 % (1226986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.59/1.08 % (1226986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.08 % (1226986)CaDiCaL version: 2.1.3 % 5.59/1.08 % (1226986)Termination reason: Instruction limit % 5.59/1.08 % (1226986)Termination phase: Saturation % 18.15/2.94 % (1226986)Time elapsed: 0.084 s % 18.15/2.94 % (1226986)Peak memory usage: 13 MB % 18.15/2.94 % (1226986)Instructions burned: 181 (million) % 18.15/2.94 % (1226999)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4290410843:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.15/2.94 % (1226997)Instruction limit reached! % 18.15/2.94 % (1226997)------------------------------ % 18.15/2.94 % (1226997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/2.94 % (1226997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/2.94 % (1226997)CaDiCaL version: 2.1.3 % 18.15/2.94 % (1226997)Termination reason: Instruction limit % 18.15/2.94 % (1226997)Termination phase: Saturation % 18.15/2.94 % (1226997)Time elapsed: 0.224 s % 18.15/2.94 % (1226997)Peak memory usage: 20 MB % 18.15/2.94 % (1226997)Instructions burned: 695 (million) % 18.15/2.94 % (1227001)fmb+10_1_sil=64000:random_seed=499195096:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.15/2.94 % (1227001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/2.94 % (1227001)Terminated due to inappropriate strategy. % 18.15/2.94 % (1227001)------------------------------ % 18.15/2.94 % (1227001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/2.94 % (1227001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/2.94 % (1227001)CaDiCaL version: 2.1.3 % 18.15/2.94 % (1227001)Termination reason: Inappropriate % 18.15/2.94 % (1227001)Time elapsed: 0.014 s % 18.15/2.94 % (1227001)Peak memory usage: 11 MB % 18.15/2.94 % (1227001)Instructions burned: 56 (million) % 18.15/2.94 % (1226987)Instruction limit reached! % 18.15/2.94 % (1226987)------------------------------ % 18.15/2.94 % (1226987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/2.94 % (1226987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/2.94 % (1226987)CaDiCaL version: 2.1.3 % 18.15/2.94 % (1226987)Termination reason: Instruction limit % 18.15/2.94 % (1226987)Termination phase: Saturation % 18.15/2.94 % (1226987)Time elapsed: 0.297 s % 18.15/2.94 % (1226987)Peak memory usage: 15 MB % 18.15/2.94 % (1226987)Instructions burned: 478 (million) % 18.15/2.94 % (1227001)------------------------------ % 18.15/2.94 % (1227001)------------------------------ % 18.15/2.94 % (1227003)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3862220282:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.15/2.94 % (1227004)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1454692615:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.15/2.94 % (1227003)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/2.94 % (1227003)Terminated due to inappropriate strategy. % 18.15/2.94 % (1227003)------------------------------ % 18.15/2.94 % (1227003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/2.94 % (1227003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/2.94 % (1227003)CaDiCaL version: 2.1.3 % 18.15/2.94 % (1227003)Termination reason: Inappropriate % 18.15/2.94 % (1227003)Time elapsed: 0.013 s % 18.15/2.94 % (1227003)Peak memory usage: 11 MB % 18.15/2.94 % (1227003)Instructions burned: 55 (million) % 18.15/2.94 % (1227003)------------------------------ % 18.15/2.94 % (1227003)------------------------------ % 18.15/2.94 % (1227004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/2.94 % (1227004)Terminated due to inappropriate strategy. % 18.15/2.94 % (1227004)------------------------------ % 18.15/2.94 % (1227004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/2.94 % (1227004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/2.94 % (1227004)CaDiCaL version: 2.1.3 % 18.15/2.94 % (1227004)Termination reason: Inappropriate % 18.15/2.94 % (1227004)Time elapsed: 0.025 s % 18.15/2.94 % (1227004)Peak memory usage: 11 MB % 18.15/2.94 % (1227004)Instructions burned: 55 (million) % 18.15/2.94 % (1227007)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2847630862:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 18.15/2.94 % (1227004)------------------------------ % 18.15/2.94 % (1227004)------------------------------ % 18.15/2.94 % (1227009)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=857332502:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.15/2.94 % (1226985)Instruction limit reached! % 18.15/2.94 % (1226985)------------------------------ % 22.39/3.50 % (1226985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1226985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1226985)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1226985)Termination reason: Instruction limit % 22.39/3.50 % (1226985)Termination phase: Saturation % 22.39/3.50 % (1226985)Time elapsed: 0.382 s % 22.39/3.50 % (1226985)Peak memory usage: 17 MB % 22.39/3.50 % (1226985)Instructions burned: 685 (million) % 22.39/3.50 % (1227011)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4064194947:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 22.39/3.50 % (1227011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.39/3.50 % (1227011)Terminated due to inappropriate strategy. % 22.39/3.50 % (1227011)------------------------------ % 22.39/3.50 % (1227011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1227011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1227011)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1227011)Termination reason: Inappropriate % 22.39/3.50 % (1227011)Time elapsed: 0.025 s % 22.39/3.50 % (1227011)Peak memory usage: 11 MB % 22.39/3.50 % (1227011)Instructions burned: 55 (million) % 22.39/3.50 % (1227011)------------------------------ % 22.39/3.50 % (1227011)------------------------------ % 22.39/3.50 % (1227013)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1980000216:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 22.39/3.50 % (1227013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.39/3.50 % (1227013)Terminated due to inappropriate strategy. % 22.39/3.50 % (1227013)------------------------------ % 22.39/3.50 % (1227013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1227013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1227013)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1227013)Termination reason: Inappropriate % 22.39/3.50 % (1227013)Time elapsed: 0.025 s % 22.39/3.50 % (1227013)Peak memory usage: 11 MB % 22.39/3.50 % (1227013)Instructions burned: 55 (million) % 22.39/3.50 % (1227013)------------------------------ % 22.39/3.50 % (1227013)------------------------------ % 22.39/3.50 % (1227015)ott-2_1_sil=16000:newcnf=on:random_seed=3522690639:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 22.39/3.50 % (1226999)Instruction limit reached! % 22.39/3.50 % (1226999)------------------------------ % 22.39/3.50 % (1226999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1226999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1226999)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1226999)Termination reason: Instruction limit % 22.39/3.50 % (1226999)Termination phase: Saturation % 22.39/3.50 % (1226999)Time elapsed: 0.488 s % 22.39/3.50 % (1226999)Peak memory usage: 19 MB % 22.39/3.50 % (1226999)Instructions burned: 881 (million) % 22.39/3.50 % (1227017)ott+10_1_sil=32000:tgt=ground:random_seed=918570173:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 22.39/3.50 % (1226990)Instruction limit reached! % 22.39/3.50 % (1226990)------------------------------ % 22.39/3.50 % (1226990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1226990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1226990)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1226990)Termination reason: Instruction limit % 22.39/3.50 % (1226990)Termination phase: Saturation % 22.39/3.50 % (1226990)Time elapsed: 0.646 s % 22.39/3.50 % (1226990)Peak memory usage: 22 MB % 22.39/3.50 % (1226990)Instructions burned: 1179 (million) % 22.39/3.50 % (1227019)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1964652043:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 22.39/3.50 % (1227019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.39/3.50 % (1227019)Terminated due to inappropriate strategy. % 22.39/3.50 % (1227019)------------------------------ % 22.39/3.50 % (1227019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.39/3.50 % (1227019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.39/3.50 % (1227019)CaDiCaL version: 2.1.3 % 22.39/3.50 % (1227019)Termination reason: Inappropriate % 22.39/3.50 % (1227019)Time elapsed: 0.025 s % 22.39/3.50 % (1227019)Peak memory usage: 11 MB % 22.39/3.50 % (1227019)Instructions burned: 55 (million) % 89.13/12.80 % (1227019)------------------------------ % 89.13/12.80 % (1227019)------------------------------ % 89.13/12.80 % (1227021)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=402027667:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 89.13/12.80 % (1227015)Instruction limit reached! % 89.13/12.80 % (1227015)------------------------------ % 89.13/12.80 % (1227015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227015)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227015)Termination reason: Instruction limit % 89.13/12.80 % (1227015)Termination phase: Saturation % 89.13/12.80 % (1227015)Time elapsed: 0.488 s % 89.13/12.80 % (1227015)Peak memory usage: 19 MB % 89.13/12.80 % (1227015)Instructions burned: 870 (million) % 89.13/12.80 % (1227023)dis+21_1_sil=32000:sas=cadical:random_seed=2984028031:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 89.13/12.80 % (1227009)Instruction limit reached! % 89.13/12.80 % (1227009)------------------------------ % 89.13/12.80 % (1227009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227009)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227009)Termination reason: Instruction limit % 89.13/12.80 % (1227009)Termination phase: Saturation % 89.13/12.80 % (1227009)Time elapsed: 0.751 s % 89.13/12.80 % (1227009)Peak memory usage: 28 MB % 89.13/12.80 % (1227009)Instructions burned: 1473 (million) % 89.13/12.80 % (1227025)ott+11_1_sil=16000:gs=on:random_seed=2234108597:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 89.13/12.80 % (1227007)Instruction limit reached! % 89.13/12.80 % (1227007)------------------------------ % 89.13/12.80 % (1227007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227007)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227007)Termination reason: Instruction limit % 89.13/12.80 % (1227007)Termination phase: Saturation % 89.13/12.80 % (1227007)Time elapsed: 1.531 s % 89.13/12.80 % (1227007)Peak memory usage: 44 MB % 89.13/12.80 % (1227007)Instructions burned: 5133 (million) % 89.13/12.80 % (1227027)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2738877323:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 89.13/12.80 % (1227027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.13/12.80 % (1227027)Terminated due to inappropriate strategy. % 89.13/12.80 % (1227027)------------------------------ % 89.13/12.80 % (1227027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227027)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227027)Termination reason: Inappropriate % 89.13/12.80 % (1227027)Time elapsed: 0.013 s % 89.13/12.80 % (1227027)Peak memory usage: 11 MB % 89.13/12.80 % (1227027)Instructions burned: 55 (million) % 89.13/12.80 % (1227027)------------------------------ % 89.13/12.80 % (1227027)------------------------------ % 89.13/12.80 % (1227029)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4104867193:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 89.13/12.80 % (1227025)Instruction limit reached! % 89.13/12.80 % (1227025)------------------------------ % 89.13/12.80 % (1227025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227025)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227025)Termination reason: Instruction limit % 89.13/12.80 % (1227025)Termination phase: Saturation % 89.13/12.80 % (1227025)Time elapsed: 1.297 s % 89.13/12.80 % (1227025)Peak memory usage: 32 MB % 89.13/12.80 % (1227025)Instructions burned: 2252 (million) % 89.13/12.80 % (1227031)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1822191851:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 89.13/12.80 % (1227021)Instruction limit reached! % 89.13/12.80 % (1227021)------------------------------ % 89.13/12.80 % (1227021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.13/12.80 % (1227021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.13/12.80 % (1227021)CaDiCaL version: 2.1.3 % 89.13/12.80 % (1227021)Termination reason: Instruction limit % 108.34/15.60 % (1227021)Termination phase: Saturation % 108.34/15.60 % (1227021)Time elapsed: 1.840 s % 108.34/15.60 % (1227021)Peak memory usage: 37 MB % 108.34/15.60 % (1227021)Instructions burned: 3513 (million) % 108.34/15.60 % (1227033)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=773369805:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 108.34/15.60 % (1227023)Instruction limit reached! % 108.34/15.60 % (1227023)------------------------------ % 108.34/15.60 % (1227023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.34/15.60 % (1227023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.34/15.60 % (1227023)CaDiCaL version: 2.1.3 % 108.34/15.60 % (1227023)Termination reason: Instruction limit % 108.34/15.60 % (1227023)Termination phase: Saturation % 108.34/15.60 % (1227023)Time elapsed: 2.015 s % 108.34/15.60 % (1227023)Peak memory usage: 40 MB % 108.34/15.60 % (1227023)Instructions burned: 3775 (million) % 108.34/15.60 % (1227035)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3000573639:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 108.34/15.60 % (1227035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.34/15.60 % (1227035)Terminated due to inappropriate strategy. % 108.34/15.60 % (1227035)------------------------------ % 108.34/15.60 % (1227035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.34/15.60 % (1227035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.34/15.60 % (1227035)CaDiCaL version: 2.1.3 % 108.34/15.60 % (1227035)Termination reason: Inappropriate % 108.34/15.60 % (1227035)Time elapsed: 0.025 s % 108.34/15.60 % (1227035)Peak memory usage: 12 MB % 108.34/15.60 % (1227035)Instructions burned: 55 (million) % 108.34/15.60 % (1227035)------------------------------ % 108.34/15.60 % (1227035)------------------------------ % 108.34/15.60 % (1227037)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1359559293:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 108.34/15.60 % (1227029)Instruction limit reached! % 108.34/15.60 % (1227029)------------------------------ % 108.34/15.60 % (1227029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.34/15.60 % (1227029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.34/15.60 % (1227029)CaDiCaL version: 2.1.3 % 108.34/15.60 % (1227029)Termination reason: Instruction limit % 108.34/15.60 % (1227029)Termination phase: Saturation % 108.34/15.60 % (1227029)Time elapsed: 1.161 s % 108.34/15.60 % (1227029)Peak memory usage: 49 MB % 108.34/15.60 % (1227029)Instructions burned: 4592 (million) % 108.34/15.60 % (1227039)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3846033974:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 108.34/15.60 % (1227037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.34/15.60 % (1227037)Terminated due to inappropriate strategy. % 108.34/15.60 % (1227037)------------------------------ % 108.34/15.60 % (1227037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.34/15.60 % (1227037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.34/15.60 % (1227037)CaDiCaL version: 2.1.3 % 108.34/15.60 % (1227037)Termination reason: Inappropriate % 108.34/15.60 % (1227037)Time elapsed: 0.025 s % 108.34/15.60 % (1227037)Peak memory usage: 11 MB % 108.34/15.60 % (1227037)Instructions burned: 55 (million) % 108.34/15.60 % (1227037)------------------------------ % 108.34/15.60 % (1227037)------------------------------ % 108.34/15.60 % (1227039)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.34/15.60 % (1227039)Terminated due to inappropriate strategy. % 108.34/15.60 % (1227039)------------------------------ % 108.34/15.60 % (1227039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.34/15.60 % (1227039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.34/15.60 % (1227039)CaDiCaL version: 2.1.3 % 108.34/15.60 % (1227039)Termination reason: Inappropriate % 108.34/15.60 % (1227039)Time elapsed: 0.013 s % 108.34/15.60 % (1227039)Peak memory usage: 11 MB % 108.34/15.60 % (1227039)Instructions burned: 55 (million) % 108.34/15.60 % (1227039)------------------------------ % 108.34/15.60 % (1227039)------------------------------ % 108.34/15.60 % (1227042)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1576737320:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 108.34/15.60 % (1227041)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2608343208:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 110.43/15.84 % (1227017)Instruction limit reached! % 110.43/15.84 % (1227017)------------------------------ % 110.43/15.84 % (1227017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227017)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227017)Termination reason: Instruction limit % 110.43/15.84 % (1227017)Termination phase: Saturation % 110.43/15.84 % (1227017)Time elapsed: 2.888 s % 110.43/15.84 % (1227017)Peak memory usage: 49 MB % 110.43/15.84 % (1227017)Instructions burned: 5114 (million) % 110.43/15.84 % (1227045)dis+10_16:1_sil=16000:random_seed=3774855968:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 110.43/15.84 % (1227033)Instruction limit reached! % 110.43/15.84 % (1227033)------------------------------ % 110.43/15.84 % (1227033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227033)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227033)Termination reason: Instruction limit % 110.43/15.84 % (1227033)Termination phase: Saturation % 110.43/15.84 % (1227033)Time elapsed: 2.805 s % 110.43/15.84 % (1227033)Peak memory usage: 46 MB % 110.43/15.84 % (1227033)Instructions burned: 5211 (million) % 110.43/15.84 % (1227047)ott-3_8_sil=64000:random_seed=3471316402:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 110.43/15.84 % (1227042)Instruction limit reached! % 110.43/15.84 % (1227042)------------------------------ % 110.43/15.84 % (1227042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227042)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227042)Termination reason: Instruction limit % 110.43/15.84 % (1227042)Termination phase: Saturation % 110.43/15.84 % (1227042)Time elapsed: 2.559 s % 110.43/15.84 % (1227042)Peak memory usage: 77 MB % 110.43/15.84 % (1227042)Instructions burned: 8173 (million) % 110.43/15.84 % (1227049)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2417602912:fmbsr=2:i=32576_2941 on theBenchmark for (2941ds/32576Mi) % 110.43/15.84 % (1227049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.43/15.84 % (1227049)Terminated due to inappropriate strategy. % 110.43/15.84 % (1227049)------------------------------ % 110.43/15.84 % (1227049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227049)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227049)Termination reason: Inappropriate % 110.43/15.84 % (1227049)Time elapsed: 0.014 s % 110.43/15.84 % (1227049)Peak memory usage: 11 MB % 110.43/15.84 % (1227049)Instructions burned: 55 (million) % 110.43/15.84 % (1227049)------------------------------ % 110.43/15.84 % (1227049)------------------------------ % 110.43/15.84 % (1227051)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=260374760:i=11404_2941 on theBenchmark for (2941ds/11404Mi) % 110.43/15.84 % (1227045)Instruction limit reached! % 110.43/15.84 % (1227045)------------------------------ % 110.43/15.84 % (1227045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227045)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227045)Termination reason: Instruction limit % 110.43/15.84 % (1227045)Termination phase: Saturation % 110.43/15.84 % (1227045)Time elapsed: 4.675 s % 110.43/15.84 % (1227045)Peak memory usage: 58 MB % 110.43/15.84 % (1227045)Instructions burned: 9156 (million) % 110.43/15.84 % (1227053)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1690015314:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 110.43/15.84 % (1227051)Instruction limit reached! % 110.43/15.84 % (1227051)------------------------------ % 110.43/15.84 % (1227051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.43/15.84 % (1227051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.43/15.84 % (1227051)CaDiCaL version: 2.1.3 % 110.43/15.84 % (1227051)Termination reason: Instruction limit % 110.43/15.84 % (1227051)Termination phase: Saturation % 110.43/15.84 % (1227051)Time elapsed: 3.564 s % 110.43/15.84 % (1227051)Peak memory usage: 85 MB % 110.43/15.84 % (1227051)Instructions burned: 11406 (million) % 110.43/15.84 % (1227055)dis+33_16_sil=32000:sac=on:random_seed=3430698723:i=15851:nm=0_2905 on theBenchmark for (2905ds/15851Mi) % 110.43/15.84 % (1227041)Instruction limit reached! % 110.43/15.84 % (1227041)------------------------------ % 110.43/15.84 % (1227041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227041)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227041)Termination reason: Instruction limit % 153.63/21.99 % (1227041)Termination phase: Saturation % 153.63/21.99 % (1227041)Time elapsed: 9.303 s % 153.63/21.99 % (1227041)Peak memory usage: 23 MB % 153.63/21.99 % (1227041)Instructions burned: 22566 (million) % 153.63/21.99 % (1227059)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=674842663:avsq=on:i=17627:add=on:amm=off_2874 on theBenchmark for (2874ds/17627Mi) % 153.63/21.99 % (1227055)Instruction limit reached! % 153.63/21.99 % (1227055)------------------------------ % 153.63/21.99 % (1227055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227055)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227055)Termination reason: Instruction limit % 153.63/21.99 % (1227055)Termination phase: Saturation % 153.63/21.99 % (1227055)Time elapsed: 3.527 s % 153.63/21.99 % (1227055)Peak memory usage: 18 MB % 153.63/21.99 % (1227055)Instructions burned: 15851 (million) % 153.63/21.99 % (1227061)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=646084485:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi) % 153.63/21.99 % (1227047)Instruction limit reached! % 153.63/21.99 % (1227047)------------------------------ % 153.63/21.99 % (1227047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227047)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227047)Termination reason: Instruction limit % 153.63/21.99 % (1227047)Termination phase: Saturation % 153.63/21.99 % (1227047)Time elapsed: 8.703 s % 153.63/21.99 % (1227047)Peak memory usage: 62 MB % 153.63/21.99 % (1227047)Instructions burned: 20146 (million) % 153.63/21.99 % (1227063)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1086132658:i=26857:ins=20_2857 on theBenchmark for (2857ds/26857Mi) % 153.63/21.99 % (1227063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.63/21.99 % (1227063)Terminated due to inappropriate strategy. % 153.63/21.99 % (1227063)------------------------------ % 153.63/21.99 % (1227063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227063)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227063)Termination reason: Inappropriate % 153.63/21.99 % (1227063)Time elapsed: 0.025 s % 153.63/21.99 % (1227063)Peak memory usage: 11 MB % 153.63/21.99 % (1227063)Instructions burned: 55 (million) % 153.63/21.99 % (1227063)------------------------------ % 153.63/21.99 % (1227063)------------------------------ % 153.63/21.99 % (1227065)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1801447032:i=28120:bs=on:fsr=off_2856 on theBenchmark for (2856ds/28120Mi) % 153.63/21.99 % (1227031)Instruction limit reached! % 153.63/21.99 % (1227031)------------------------------ % 153.63/21.99 % (1227031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227031)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227031)Termination reason: Instruction limit % 153.63/21.99 % (1227031)Termination phase: Saturation % 153.63/21.99 % (1227031)Time elapsed: 12.695 s % 153.63/21.99 % (1227031)Peak memory usage: 35 MB % 153.63/21.99 % (1227031)Instructions burned: 29341 (million) % 153.63/21.99 % (1227067)fmb+10_1_sil=256000:fmbss=7:random_seed=3272810254:fmbsr=1.6:i=182295_2846 on theBenchmark for (2846ds/182295Mi) % 153.63/21.99 % (1227067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.63/21.99 % (1227067)Terminated due to inappropriate strategy. % 153.63/21.99 % (1227067)------------------------------ % 153.63/21.99 % (1227067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.63/21.99 % (1227067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.63/21.99 % (1227067)CaDiCaL version: 2.1.3 % 153.63/21.99 % (1227067)Termination reason: Inappropriate % 153.63/21.99 % (1227067)Time elapsed: 0.025 s % 153.63/21.99 % (1227067)Peak memory usage: 11 MB % 153.63/21.99 % (1227067)Instructions burned: 55 (million) % 153.63/21.99 % (1227067)------------------------------ % 153.63/21.99 % (1227067)------------------------------ % 153.63/21.99 % (1227069)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2725236339:i=44625:gsp=on_2846 on theBenchmark for (2846ds/44625Mi) % 166.67/23.88 % (1227069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.67/23.88 % (1227069)Terminated due to inappropriate strategy. % 166.67/23.88 % (1227069)------------------------------ % 166.67/23.88 % (1227069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.67/23.88 % (1227069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.67/23.88 % (1227069)CaDiCaL version: 2.1.3 % 166.67/23.88 % (1227069)Termination reason: Inappropriate % 166.67/23.88 % (1227069)Time elapsed: 0.025 s % 166.67/23.88 % (1227069)Peak memory usage: 12 MB % 166.67/23.88 % (1227069)Instructions burned: 55 (million) % 166.67/23.88 % (1227069)------------------------------ % 166.67/23.88 % (1227069)------------------------------ % 166.67/23.88 % (1227071)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4209472442:i=160505_2846 on theBenchmark for (2846ds/160505Mi) % 166.67/23.88 % (1227071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.67/23.88 % (1227071)Terminated due to inappropriate strategy. % 166.67/23.88 % (1227071)------------------------------ % 166.67/23.88 % (1227071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.67/23.88 % (1227071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.67/23.88 % (1227071)CaDiCaL version: 2.1.3 % 166.67/23.88 % (1227071)Termination reason: Inappropriate % 166.67/23.88 % (1227071)Time elapsed: 0.025 s % 166.67/23.88 % (1227071)Peak memory usage: 11 MB % 166.67/23.88 % (1227071)Instructions burned: 55 (million) % 166.67/23.88 % (1227071)------------------------------ % 166.67/23.88 % (1227071)------------------------------ % 166.67/23.88 % (1227073)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2231037778:fmbsr=1.3:i=225729_2845 on theBenchmark for (2845ds/225729Mi) % 166.67/23.88 % (1227073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.67/23.88 % (1227073)Terminated due to inappropriate strategy. % 166.67/23.88 % (1227073)------------------------------ % 166.67/23.88 % (1227073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.67/23.88 % (1227073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.67/23.88 % (1227073)CaDiCaL version: 2.1.3 % 166.67/23.88 % (1227073)Termination reason: Inappropriate % 166.67/23.88 % (1227073)Time elapsed: 0.025 s % 166.67/23.88 % (1227073)Peak memory usage: 11 MB % 166.67/23.88 % (1227073)Instructions burned: 55 (million) % 166.67/23.88 % (1227073)------------------------------ % 166.67/23.88 % (1227073)------------------------------ % 166.67/23.88 % (1227075)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1851553538:fmbsr=2:i=185024:ins=7_2845 on theBenchmark for (2845ds/185024Mi) % 166.67/23.88 % (1227075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.67/23.88 % (1227075)Terminated due to inappropriate strategy. % 166.67/23.88 % (1227075)------------------------------ % 166.67/23.88 % (1227075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.67/23.88 % (1227075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.67/23.88 % (1227075)CaDiCaL version: 2.1.3 % 166.67/23.88 % (1227075)Termination reason: Inappropriate % 166.67/23.88 % (1227075)Time elapsed: 0.025 s % 166.67/23.88 % (1227075)Peak memory usage: 11 MB % 166.67/23.88 % (1227075)Instructions burned: 55 (million) % 166.67/23.88 % (1227075)------------------------------ % 166.67/23.88 % (1227075)------------------------------ % 166.67/23.88 % (1227077)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2079747309:rtra=on_2844 on theBenchmark for (2844ds/0Mi) % 166.67/23.88 % (1227077)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.67/23.88 % (1227077)Terminated due to inappropriate strategy. % 166.67/23.88 % (1227077)------------------------------ % 166.67/23.88 % (1227077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.67/23.88 % (1227077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.67/23.88 % (1227077)CaDiCaL version: 2.1.3 % 166.67/23.88 % (1227077)Termination reason: Inappropriate % 166.67/23.88 % (1227077)Time elapsed: 0.029 s % 166.67/23.88 % (1227077)Peak memory usage: 12 MB % 166.67/23.88 % (1227077)Instructions burned: 60 (million) % 166.67/23.88 % (1227077)------------------------------ % 166.67/23.88 % (1227077)------------------------------ % 166.67/23.88 % (1227079)% WARNING: option uhcvi not known. % 166.67/23.88 % (1227079)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1878090834:i=271062:add=off:rtra=on:rawr=on_2844 on theBenchmark for (2844ds/271062Mi) % 184.10/26.26 % (1227053)Instruction limit reached! % 184.10/26.26 % (1227053)------------------------------ % 184.10/26.26 % (1227053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227053)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227053)Termination reason: Instruction limit % 184.10/26.26 % (1227053)Termination phase: Saturation % 184.10/26.26 % (1227053)Time elapsed: 8.204 s % 184.10/26.26 % (1227053)Peak memory usage: 97 MB % 184.10/26.26 % (1227053)Instructions burned: 14136 (million) % 184.10/26.26 % (1227081)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1476388971:i=176048:add=on:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/176048Mi) % 184.10/26.26 % (1227059)Instruction limit reached! % 184.10/26.26 % (1227059)------------------------------ % 184.10/26.26 % (1227059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227059)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227059)Termination reason: Instruction limit % 184.10/26.26 % (1227059)Termination phase: Saturation % 184.10/26.26 % (1227059)Time elapsed: 8.431 s % 184.10/26.26 % (1227059)Peak memory usage: 162 MB % 184.10/26.26 % (1227059)Instructions burned: 17629 (million) % 184.10/26.26 % (1227083)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1620603726:i=206:fgj=on:rtra=on_2789 on theBenchmark for (2789ds/206Mi) % 184.10/26.26 % (1227083)Instruction limit reached! % 184.10/26.26 % (1227083)------------------------------ % 184.10/26.26 % (1227083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227083)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227083)Termination reason: Instruction limit % 184.10/26.26 % (1227083)Termination phase: Saturation % 184.10/26.26 % (1227083)Time elapsed: 0.121 s % 184.10/26.26 % (1227083)Peak memory usage: 15 MB % 184.10/26.26 % (1227083)Instructions burned: 206 (million) % 184.10/26.26 % (1227085)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3009040392:i=232:rtra=on_2788 on theBenchmark for (2788ds/232Mi) % 184.10/26.26 % (1227085)Instruction limit reached! % 184.10/26.26 % (1227085)------------------------------ % 184.10/26.26 % (1227085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227085)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227085)Termination reason: Instruction limit % 184.10/26.26 % (1227085)Termination phase: Saturation % 184.10/26.26 % (1227085)Time elapsed: 0.138 s % 184.10/26.26 % (1227085)Peak memory usage: 15 MB % 184.10/26.26 % (1227085)Instructions burned: 232 (million) % 184.10/26.26 % (1227087)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=850800896:i=262:rtra=on_2786 on theBenchmark for (2786ds/262Mi) % 184.10/26.26 % (1227087)Instruction limit reached! % 184.10/26.26 % (1227087)------------------------------ % 184.10/26.26 % (1227087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227087)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227087)Termination reason: Instruction limit % 184.10/26.26 % (1227087)Termination phase: Saturation % 184.10/26.26 % (1227087)Time elapsed: 0.155 s % 184.10/26.26 % (1227087)Peak memory usage: 15 MB % 184.10/26.26 % (1227087)Instructions burned: 263 (million) % 184.10/26.26 % (1227089)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=533267647:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2784 on theBenchmark for (2784ds/318Mi) % 184.10/26.26 % (1227089)Instruction limit reached! % 184.10/26.26 % (1227089)------------------------------ % 184.10/26.26 % (1227089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.10/26.26 % (1227089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.10/26.26 % (1227089)CaDiCaL version: 2.1.3 % 184.10/26.26 % (1227089)Termination reason: Instruction limit % 184.10/26.26 % (1227089)Termination phase: Saturation % 184.10/26.26 % (1227089)Time elapsed: 0.190 s % 184.10/26.26 % (1227089)Peak memory usage: 15 MB % 184.10/26.26 % (1227089)Instructions burned: 319 (million) % 184.10/26.26 % (1227091)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1313391417:i=1428:nm=2:rtra=on_2782 on theBenchmark for (2782ds/1428Mi) % 192.81/27.50 % (1227091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.81/27.50 % (1227091)Terminated due to inappropriate strategy. % 192.81/27.50 % (1227091)------------------------------ % 192.81/27.50 % (1227091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227091)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227091)Termination reason: Inappropriate % 192.81/27.50 % (1227091)Time elapsed: 0.032 s % 192.81/27.50 % (1227091)Peak memory usage: 12 MB % 192.81/27.50 % (1227091)Instructions burned: 60 (million) % 192.81/27.50 % (1227091)------------------------------ % 192.81/27.50 % (1227091)------------------------------ % 192.81/27.50 % (1227093)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2296916148:i=262:bd=preordered:rtra=on:fsd=on_2782 on theBenchmark for (2782ds/262Mi) % 192.81/27.50 % (1227093)Instruction limit reached! % 192.81/27.50 % (1227093)------------------------------ % 192.81/27.50 % (1227093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227093)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227093)Termination reason: Instruction limit % 192.81/27.50 % (1227093)Termination phase: Saturation % 192.81/27.50 % (1227093)Time elapsed: 0.172 s % 192.81/27.50 % (1227093)Peak memory usage: 16 MB % 192.81/27.50 % (1227093)Instructions burned: 262 (million) % 192.81/27.50 % (1227095)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=137747474:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1368Mi) % 192.81/27.50 % (1227095)Instruction limit reached! % 192.81/27.50 % (1227095)------------------------------ % 192.81/27.50 % (1227095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227095)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227095)Termination reason: Instruction limit % 192.81/27.50 % (1227095)Termination phase: Saturation % 192.81/27.50 % (1227095)Time elapsed: 0.789 s % 192.81/27.50 % (1227095)Peak memory usage: 21 MB % 192.81/27.50 % (1227095)Instructions burned: 1369 (million) % 192.81/27.50 % (1227097)ott-21_1_sil=16000:si=on:fs=off:random_seed=269628643:i=360:av=off:fsr=off:rtra=on_2772 on theBenchmark for (2772ds/360Mi) % 192.81/27.50 % (1227097)Instruction limit reached! % 192.81/27.50 % (1227097)------------------------------ % 192.81/27.50 % (1227097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227097)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227097)Termination reason: Instruction limit % 192.81/27.50 % (1227097)Termination phase: Saturation % 192.81/27.50 % (1227097)Time elapsed: 0.170 s % 192.81/27.50 % (1227097)Peak memory usage: 15 MB % 192.81/27.50 % (1227097)Instructions burned: 361 (million) % 192.81/27.50 % (1227099)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3343394916:i=954:bd=all:rtra=on_2770 on theBenchmark for (2770ds/954Mi) % 192.81/27.50 % (1227099)Instruction limit reached! % 192.81/27.50 % (1227099)------------------------------ % 192.81/27.50 % (1227099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227099)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227099)Termination reason: Instruction limit % 192.81/27.50 % (1227099)Termination phase: Saturation % 192.81/27.50 % (1227099)Time elapsed: 0.591 s % 192.81/27.50 % (1227099)Peak memory usage: 19 MB % 192.81/27.50 % (1227099)Instructions burned: 954 (million) % 192.81/27.50 % (1227101)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=73040126:fmbsr=1.3:i=1730:ins=25:rtra=on_2763 on theBenchmark for (2763ds/1730Mi) % 192.81/27.50 % (1227101)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.81/27.50 % (1227101)Terminated due to inappropriate strategy. % 192.81/27.50 % (1227101)------------------------------ % 192.81/27.50 % (1227101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.50 % (1227101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.50 % (1227101)CaDiCaL version: 2.1.3 % 192.81/27.50 % (1227101)Termination reason: Inappropriate % 224.77/31.98 % (1227101)Time elapsed: 0.029 s % 224.77/31.98 % (1227101)Peak memory usage: 12 MB % 224.77/31.98 % (1227101)Instructions burned: 59 (million) % 224.77/31.98 % (1227101)------------------------------ % 224.77/31.98 % (1227101)------------------------------ % 224.77/31.98 % (1227103)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3452151650:i=2358:rtra=on_2763 on theBenchmark for (2763ds/2358Mi) % 224.77/31.98 % (1227103)Instruction limit reached! % 224.77/31.98 % (1227103)------------------------------ % 224.77/31.98 % (1227103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.77/31.98 % (1227103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.77/31.98 % (1227103)CaDiCaL version: 2.1.3 % 224.77/31.98 % (1227103)Termination reason: Instruction limit % 224.77/31.98 % (1227103)Termination phase: Saturation % 224.77/31.98 % (1227103)Time elapsed: 1.352 s % 224.77/31.98 % (1227103)Peak memory usage: 33 MB % 224.77/31.98 % (1227103)Instructions burned: 2358 (million) % 224.77/31.98 % (1227105)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3665673561:i=1778:ins=1:rtra=on_2749 on theBenchmark for (2749ds/1778Mi) % 224.77/31.98 % (1227105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.77/31.98 % (1227105)Terminated due to inappropriate strategy. % 224.77/31.98 % (1227105)------------------------------ % 224.77/31.98 % (1227105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.77/31.98 % (1227105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.77/31.98 % (1227105)CaDiCaL version: 2.1.3 % 224.77/31.98 % (1227105)Termination reason: Inappropriate % 224.77/31.98 % (1227105)Time elapsed: 0.030 s % 224.77/31.98 % (1227105)Peak memory usage: 12 MB % 224.77/31.98 % (1227105)Instructions burned: 60 (million) % 224.77/31.98 % (1227105)------------------------------ % 224.77/31.98 % (1227105)------------------------------ % 224.77/31.98 % (1227107)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=2010294151:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2749 on theBenchmark for (2749ds/1384Mi) % 224.77/31.98 % (1227061)Instruction limit reached! % 224.77/31.98 % (1227061)------------------------------ % 224.77/31.98 % (1227061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.77/31.98 % (1227061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.77/31.98 % (1227061)CaDiCaL version: 2.1.3 % 224.77/31.98 % (1227061)Termination reason: Instruction limit % 224.77/31.98 % (1227061)Termination phase: Saturation % 224.77/31.98 % (1227061)Time elapsed: 12.761 s % 224.77/31.98 % (1227061)Peak memory usage: 411 MB % 224.77/31.98 % (1227061)Instructions burned: 53299 (million) % 224.77/31.98 % (1227109)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1577345947:i=1758:kws=inv_precedence:fsr=off:rtra=on_2742 on theBenchmark for (2742ds/1758Mi) % 224.77/31.98 % (1227107)Instruction limit reached! % 224.77/31.98 % (1227107)------------------------------ % 224.77/31.98 % (1227107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.77/31.98 % (1227107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.77/31.98 % (1227107)CaDiCaL version: 2.1.3 % 224.77/31.98 % (1227107)Termination reason: Instruction limit % 224.77/31.98 % (1227107)Termination phase: Saturation % 224.77/31.98 % (1227107)Time elapsed: 0.852 s % 224.77/31.98 % (1227107)Peak memory usage: 25 MB % 224.77/31.98 % (1227107)Instructions burned: 1384 (million) % 224.77/31.98 % (1227111)fmb+10_1_sil=64000:si=on:random_seed=1578156048:i=44122:nm=2:rtra=on:gsp=on_2740 on theBenchmark for (2740ds/44122Mi) % 224.77/31.98 % (1227111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.77/31.98 % (1227111)Terminated due to inappropriate strategy. % 224.77/31.98 % (1227111)------------------------------ % 224.77/31.98 % (1227111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.77/31.98 % (1227111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.77/31.98 % (1227111)CaDiCaL version: 2.1.3 % 224.77/31.98 % (1227111)Termination reason: Inappropriate % 224.77/31.98 % (1227111)Time elapsed: 0.029 s % 224.77/31.98 % (1227111)Peak memory usage: 12 MB % 224.77/31.98 % (1227111)Instructions burned: 60 (million) % 224.77/31.98 % (1227111)------------------------------ % 224.77/31.98 % (1227111)------------------------------ % 224.77/31.98 % (1227113)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=945601798:i=19030:nm=5:rtra=on_2739 on theBenchmark for (2739ds/19030Mi) % 265.20/37.69 % (1227113)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.20/37.69 % (1227113)Terminated due to inappropriate strategy. % 265.20/37.69 % (1227113)------------------------------ % 265.20/37.69 % (1227113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.20/37.69 % (1227113)CaDiCaL version: 2.1.3 % 265.20/37.69 % (1227113)Termination reason: Inappropriate % 265.20/37.69 % (1227113)Time elapsed: 0.029 s % 265.20/37.69 % (1227113)Peak memory usage: 12 MB % 265.20/37.69 % (1227113)Instructions burned: 60 (million) % 265.20/37.69 % (1227113)------------------------------ % 265.20/37.69 % (1227113)------------------------------ % 265.20/37.69 % (1227115)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2967454540:fmbsr=1.7:i=1840:rtra=on_2739 on theBenchmark for (2739ds/1840Mi) % 265.20/37.69 % (1227115)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.20/37.69 % (1227115)Terminated due to inappropriate strategy. % 265.20/37.69 % (1227115)------------------------------ % 265.20/37.69 % (1227115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.20/37.69 % (1227115)CaDiCaL version: 2.1.3 % 265.20/37.69 % (1227115)Termination reason: Inappropriate % 265.20/37.69 % (1227115)Time elapsed: 0.029 s % 265.20/37.69 % (1227115)Peak memory usage: 12 MB % 265.20/37.69 % (1227115)Instructions burned: 60 (million) % 265.20/37.69 % (1227115)------------------------------ % 265.20/37.69 % (1227115)------------------------------ % 265.20/37.69 % (1227117)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3093449749:i=10262:rtra=on_2738 on theBenchmark for (2738ds/10262Mi) % 265.20/37.69 % (1227109)Instruction limit reached! % 265.20/37.69 % (1227109)------------------------------ % 265.20/37.69 % (1227109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.20/37.69 % (1227109)CaDiCaL version: 2.1.3 % 265.20/37.69 % (1227109)Termination reason: Instruction limit % 265.20/37.69 % (1227109)Termination phase: Saturation % 265.20/37.69 % (1227109)Time elapsed: 0.522 s % 265.20/37.69 % (1227109)Peak memory usage: 25 MB % 265.20/37.69 % (1227109)Instructions burned: 1760 (million) % 265.20/37.69 % (1227119)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4057404674:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2736 on theBenchmark for (2736ds/2944Mi) % 265.20/37.69 % (1227065)Instruction limit reached! % 265.20/37.69 % (1227065)------------------------------ % 265.20/37.69 % (1227065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.20/37.69 % (1227065)CaDiCaL version: 2.1.3 % 265.20/37.69 % (1227065)Termination reason: Instruction limit % 265.20/37.69 % (1227065)Termination phase: Saturation % 265.20/37.69 % (1227065)Time elapsed: 12.860 s % 265.20/37.69 % (1227065)Peak memory usage: 85 MB % 265.20/37.69 % (1227065)Instructions burned: 28121 (million) % 265.20/37.69 % (1227121)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2895325382:i=12648:rtra=on_2727 on theBenchmark for (2727ds/12648Mi) % 265.20/37.69 % (1227119)Instruction limit reached! % 265.20/37.69 % (1227119)------------------------------ % 265.20/37.69 % (1227119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.20/37.69 % (1227119)CaDiCaL version: 2.1.3 % 265.20/37.69 % (1227119)Termination reason: Instruction limit % 265.20/37.69 % (1227119)Termination phase: Saturation % 265.20/37.69 % (1227119)Time elapsed: 0.914 s % 265.20/37.69 % (1227119)Peak memory usage: 45 MB % 265.20/37.69 % (1227119)Instructions burned: 2946 (million) % 265.20/37.69 % (1227123)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2656000600:fmbsr=2.30978:i=4348:rtra=on_2727 on theBenchmark for (2727ds/4348Mi) % 265.20/37.69 % (1227121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.20/37.69 % (1227121)Terminated due to inappropriate strategy. % 265.20/37.69 % (1227121)------------------------------ % 265.20/37.69 % (1227121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.20/37.69 % (1227121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227121)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227121)Termination reason: Inappropriate % 300.01/42.54 % (1227121)Time elapsed: 0.029 s % 300.01/42.54 % (1227121)Peak memory usage: 12 MB % 300.01/42.54 % (1227121)Instructions burned: 60 (million) % 300.01/42.54 % (1227121)------------------------------ % 300.01/42.54 % (1227121)------------------------------ % 300.01/42.54 % (1227123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1227123)Terminated due to inappropriate strategy. % 300.01/42.54 % (1227123)------------------------------ % 300.01/42.54 % (1227123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1227123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227123)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227123)Termination reason: Inappropriate % 300.01/42.54 % (1227123)Time elapsed: 0.020 s % 300.01/42.54 % (1227123)Peak memory usage: 12 MB % 300.01/42.54 % (1227123)Instructions burned: 60 (million) % 300.01/42.54 % (1227123)------------------------------ % 300.01/42.54 % (1227123)------------------------------ % 300.01/42.54 % (1227125)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3578876409:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2727 on theBenchmark for (2727ds/1738Mi) % 300.01/42.54 % (1227127)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3987989022:i=10228:av=off:rtra=on_2727 on theBenchmark for (2727ds/10228Mi) % 300.01/42.54 % (1227125)Instruction limit reached! % 300.01/42.54 % (1227125)------------------------------ % 300.01/42.54 % (1227125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1227125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227125)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227125)Termination reason: Instruction limit % 300.01/42.54 % (1227125)Termination phase: Saturation % 300.01/42.54 % (1227125)Time elapsed: 1.025 s % 300.01/42.54 % (1227125)Peak memory usage: 24 MB % 300.01/42.54 % (1227125)Instructions burned: 1739 (million) % 300.01/42.54 % (1227129)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=364951189:i=108564:rtra=on_2716 on theBenchmark for (2716ds/108564Mi) % 300.01/42.54 % (1227129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.01/42.54 % (1227129)Terminated due to inappropriate strategy. % 300.01/42.54 % (1227129)------------------------------ % 300.01/42.54 % (1227129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1227129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227129)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227129)Termination reason: Inappropriate % 300.01/42.54 % (1227129)Time elapsed: 0.029 s % 300.01/42.54 % (1227129)Peak memory usage: 12 MB % 300.01/42.54 % (1227129)Instructions burned: 60 (million) % 300.01/42.54 % (1227129)------------------------------ % 300.01/42.54 % (1227129)------------------------------ % 300.01/42.54 % (1227131)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2869507654:i=7024:aac=none:rtra=on_2716 on theBenchmark for (2716ds/7024Mi) % 300.01/42.54 % (1227127)Instruction limit reached! % 300.01/42.54 % (1227127)------------------------------ % 300.01/42.54 % (1227127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1227127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227127)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227127)Termination reason: Instruction limit % 300.01/42.54 % (1227127)Termination phase: Saturation % 300.01/42.54 % (1227127)Time elapsed: 3.373 s % 300.01/42.54 % (1227127)Peak memory usage: 79 MB % 300.01/42.54 % (1227127)Instructions burned: 10229 (million) % 300.01/42.54 % (1227133)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=879433028:i=7546:rtra=on:amm=off_2693 on theBenchmark for (2693ds/7546Mi) % 300.01/42.54 % (1227117)Instruction limit reached! % 300.01/42.54 % (1227117)------------------------------ % 300.01/42.54 % (1227117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.54 % (1227117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.54 % (1227117)CaDiCaL version: 2.1.3 % 300.01/42.54 % (1227117)Termination reason: Instruction limit % 300.01/42.54 % (1227117)Termination phase: Saturation % 300.01/42.54 % (1227117)Time elapsed: 5.590 s % 300.01/42.54 % (1227117)Peak memory usage: 70 MB % 300.01/42.54 % (1227117)Instructions burned: 10263 (million) % 300.01/42.54 % (1227135)ott+11_1_sil=16000:si=on:gs=on:random_seed=863541150:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd= % 300.01/42.54 Terminated % 300.01/42.54 % Vampire exiting %------------------------------------------------------------------------------