%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW676_1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:40:37 PM UTC 2026 % Result : Timeout 286.87s 40.78s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW676_1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n005.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.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:24:47 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.20 Running first-order model finding % 0.08/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.98/0.88 % (819307)Will run a generic schedule for satisfiability detection. % 3.98/0.88 % (819315)dis+10_1_sil=32000:sp=arity:random_seed=2977965249:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.98/0.88 % (819312)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3208299602_2999 on theBenchmark for (2999ds/0Mi) % 3.98/0.88 % (819314)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1724794462:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.98/0.88 % (819316)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1005487013:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.98/0.88 % (819318)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1917449035:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.98/0.88 % (819312)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.98/0.88 % (819312)Terminated due to inappropriate strategy. % 3.98/0.88 % (819312)------------------------------ % 3.98/0.88 % (819312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.98/0.88 % (819312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.98/0.88 % (819312)CaDiCaL version: 2.1.3 % 3.98/0.88 % (819312)Termination reason: Inappropriate % 3.98/0.88 % (819312)Time elapsed: 0.002 s % 3.98/0.88 % (819312)Peak memory usage: 10 MB % 3.98/0.88 % (819312)Instructions burned: 3 (million) % 3.98/0.88 % (819313)% WARNING: option uhcvi not known. % 3.98/0.88 % (819312)------------------------------ % 3.98/0.88 % (819312)------------------------------ % 3.98/0.88 % (819317)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2681421045:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.98/0.88 % (819313)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4011922858:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.98/0.88 % (819324)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3404333613:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.98/0.88 % (819324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.98/0.88 % (819324)Terminated due to inappropriate strategy. % 3.98/0.88 % (819324)------------------------------ % 3.98/0.88 % (819324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.98/0.88 % (819324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.98/0.88 % (819324)CaDiCaL version: 2.1.3 % 3.98/0.88 % (819324)Termination reason: Inappropriate % 3.98/0.88 % (819324)Time elapsed: 0.001 s % 3.98/0.88 % (819324)Peak memory usage: 11 MB % 3.98/0.88 % (819324)Instructions burned: 2 (million) % 3.98/0.88 % (819324)------------------------------ % 3.98/0.88 % (819324)------------------------------ % 3.98/0.88 % (819315)Instruction limit reached! % 3.98/0.88 % (819315)------------------------------ % 3.98/0.88 % (819315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.98/0.88 % (819315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.98/0.88 % (819315)CaDiCaL version: 2.1.3 % 3.98/0.88 % (819315)Termination reason: Instruction limit % 3.98/0.88 % (819315)Termination phase: Saturation % 3.98/0.88 % (819315)Time elapsed: 0.035 s % 3.98/0.88 % (819315)Peak memory usage: 13 MB % 3.98/0.88 % (819315)Instructions burned: 106 (million) % 3.98/0.88 % (819329)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=3434977247:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.98/0.88 % (819328)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3343964092:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.98/0.88 % (819316)Instruction limit reached! % 3.98/0.88 % (819316)------------------------------ % 3.98/0.88 % (819316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.98/0.88 % (819316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.98/0.88 % (819316)CaDiCaL version: 2.1.3 % 3.98/0.88 % (819316)Termination reason: Instruction limit % 3.98/0.88 % (819316)Termination phase: Saturation % 3.98/0.88 % (819316)Time elapsed: 0.074 s % 3.98/0.88 % (819316)Peak memory usage: 13 MB % 3.98/0.88 % (819316)Instructions burned: 116 (million) % 3.98/0.88 % (819317)Instruction limit reached! % 3.98/0.88 % (819317)------------------------------ % 3.98/0.88 % (819317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819317)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819317)Termination reason: Instruction limit % 8.13/1.48 % (819317)Termination phase: Saturation % 8.13/1.48 % (819317)Time elapsed: 0.086 s % 8.13/1.48 % (819317)Peak memory usage: 13 MB % 8.13/1.48 % (819317)Instructions burned: 132 (million) % 8.13/1.48 % (819332)ott-21_1_sil=16000:fs=off:random_seed=1807428264:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.13/1.48 % (819333)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2131988773:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.13/1.48 % (819318)Instruction limit reached! % 8.13/1.48 % (819318)------------------------------ % 8.13/1.48 % (819318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819318)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819318)Termination reason: Instruction limit % 8.13/1.48 % (819318)Termination phase: Saturation % 8.13/1.48 % (819318)Time elapsed: 0.115 s % 8.13/1.48 % (819318)Peak memory usage: 13 MB % 8.13/1.48 % (819318)Instructions burned: 160 (million) % 8.13/1.48 % (819328)Instruction limit reached! % 8.13/1.48 % (819328)------------------------------ % 8.13/1.48 % (819328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819328)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819328)Termination reason: Instruction limit % 8.13/1.48 % (819328)Termination phase: Saturation % 8.13/1.48 % (819328)Time elapsed: 0.089 s % 8.13/1.48 % (819328)Peak memory usage: 13 MB % 8.13/1.48 % (819328)Instructions burned: 131 (million) % 8.13/1.48 % (819336)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3696294316:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.13/1.48 % (819336)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.13/1.48 % (819336)Terminated due to inappropriate strategy. % 8.13/1.48 % (819336)------------------------------ % 8.13/1.48 % (819336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819336)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819336)Termination reason: Inappropriate % 8.13/1.48 % (819336)Time elapsed: 0.001 s % 8.13/1.48 % (819336)Peak memory usage: 10 MB % 8.13/1.48 % (819336)Instructions burned: 1 (million) % 8.13/1.48 % (819336)------------------------------ % 8.13/1.48 % (819336)------------------------------ % 8.13/1.48 % (819337)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3672381178:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.13/1.48 % (819339)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4284479519:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.13/1.48 % (819339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.13/1.48 % (819339)Terminated due to inappropriate strategy. % 8.13/1.48 % (819339)------------------------------ % 8.13/1.48 % (819339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819339)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819339)Termination reason: Inappropriate % 8.13/1.48 % (819339)Time elapsed: 0.001 s % 8.13/1.48 % (819339)Peak memory usage: 10 MB % 8.13/1.48 % (819339)Instructions burned: 2 (million) % 8.13/1.48 % (819339)------------------------------ % 8.13/1.48 % (819339)------------------------------ % 8.13/1.48 % (819342)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=1945577016: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) % 8.13/1.48 % (819332)Instruction limit reached! % 8.13/1.48 % (819332)------------------------------ % 8.13/1.48 % (819332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.48 % (819332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.48 % (819332)CaDiCaL version: 2.1.3 % 8.13/1.48 % (819332)Termination reason: Instruction limit % 8.13/1.48 % (819332)Termination phase: Saturation % 8.13/1.48 % (819332)Time elapsed: 0.084 s % 8.13/1.48 % (819332)Peak memory usage: 12 MB % 8.13/1.48 % (819332)Instructions burned: 181 (million) % 21.14/3.28 % (819344)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=766346188:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.14/3.28 % (819329)Instruction limit reached! % 21.14/3.28 % (819329)------------------------------ % 21.14/3.28 % (819329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.14/3.28 % (819329)CaDiCaL version: 2.1.3 % 21.14/3.28 % (819329)Termination reason: Instruction limit % 21.14/3.28 % (819329)Termination phase: Saturation % 21.14/3.28 % (819329)Time elapsed: 0.167 s % 21.14/3.28 % (819329)Peak memory usage: 16 MB % 21.14/3.28 % (819329)Instructions burned: 686 (million) % 21.14/3.28 % (819346)fmb+10_1_sil=64000:random_seed=1927190329:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.14/3.28 % (819346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.14/3.28 % (819346)Terminated due to inappropriate strategy. % 21.14/3.28 % (819346)------------------------------ % 21.14/3.28 % (819346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.14/3.28 % (819346)CaDiCaL version: 2.1.3 % 21.14/3.28 % (819346)Termination reason: Inappropriate % 21.14/3.28 % (819346)Time elapsed: 0.001 s % 21.14/3.28 % (819346)Peak memory usage: 11 MB % 21.14/3.28 % (819346)Instructions burned: 2 (million) % 21.14/3.28 % (819346)------------------------------ % 21.14/3.28 % (819346)------------------------------ % 21.14/3.28 % (819348)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3645708395:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.14/3.28 % (819348)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.14/3.28 % (819348)Terminated due to inappropriate strategy. % 21.14/3.28 % (819348)------------------------------ % 21.14/3.28 % (819348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.14/3.28 % (819348)CaDiCaL version: 2.1.3 % 21.14/3.28 % (819348)Termination reason: Inappropriate % 21.14/3.28 % (819348)Time elapsed: 0.001 s % 21.14/3.28 % (819348)Peak memory usage: 11 MB % 21.14/3.28 % (819348)Instructions burned: 2 (million) % 21.14/3.28 % (819348)------------------------------ % 21.14/3.28 % (819348)------------------------------ % 21.14/3.28 % (819350)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4291137052:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.14/3.28 % (819350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.14/3.28 % (819350)Terminated due to inappropriate strategy. % 21.14/3.28 % (819350)------------------------------ % 21.14/3.28 % (819350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.14/3.28 % (819350)CaDiCaL version: 2.1.3 % 21.14/3.28 % (819350)Termination reason: Inappropriate % 21.14/3.28 % (819350)Time elapsed: 0.001 s % 21.14/3.28 % (819350)Peak memory usage: 10 MB % 21.14/3.28 % (819350)Instructions burned: 2 (million) % 21.14/3.28 % (819350)------------------------------ % 21.14/3.28 % (819350)------------------------------ % 21.14/3.28 % (819352)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1591412770:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 21.14/3.28 % (819333)Instruction limit reached! % 21.14/3.28 % (819333)------------------------------ % 21.14/3.28 % (819333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.14/3.28 % (819333)CaDiCaL version: 2.1.3 % 21.14/3.28 % (819333)Termination reason: Instruction limit % 21.14/3.28 % (819333)Termination phase: Saturation % 21.14/3.28 % (819333)Time elapsed: 0.311 s % 21.14/3.28 % (819333)Peak memory usage: 14 MB % 21.14/3.28 % (819333)Instructions burned: 477 (million) % 21.14/3.28 % (819354)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2943510113:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.14/3.28 % (819342)Instruction limit reached! % 21.14/3.28 % (819342)------------------------------ % 21.14/3.28 % (819342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.14/3.28 % (819342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819342)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819342)Termination reason: Instruction limit % 28.93/4.32 % (819342)Termination phase: Saturation % 28.93/4.32 % (819342)Time elapsed: 0.461 s % 28.93/4.32 % (819342)Peak memory usage: 19 MB % 28.93/4.32 % (819342)Instructions burned: 692 (million) % 28.93/4.32 % (819356)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3020288037:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.93/4.32 % (819356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.93/4.32 % (819356)Terminated due to inappropriate strategy. % 28.93/4.32 % (819356)------------------------------ % 28.93/4.32 % (819356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.93/4.32 % (819356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819356)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819356)Termination reason: Inappropriate % 28.93/4.32 % (819356)Time elapsed: 0.002 s % 28.93/4.32 % (819356)Peak memory usage: 11 MB % 28.93/4.32 % (819356)Instructions burned: 3 (million) % 28.93/4.32 % (819356)------------------------------ % 28.93/4.32 % (819356)------------------------------ % 28.93/4.32 % (819358)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=192070697:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.93/4.32 % (819358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.93/4.32 % (819358)Terminated due to inappropriate strategy. % 28.93/4.32 % (819358)------------------------------ % 28.93/4.32 % (819358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.93/4.32 % (819358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819358)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819358)Termination reason: Inappropriate % 28.93/4.32 % (819358)Time elapsed: 0.001 s % 28.93/4.32 % (819358)Peak memory usage: 10 MB % 28.93/4.32 % (819358)Instructions burned: 2 (million) % 28.93/4.32 % (819358)------------------------------ % 28.93/4.32 % (819358)------------------------------ % 28.93/4.32 % (819344)Instruction limit reached! % 28.93/4.32 % (819344)------------------------------ % 28.93/4.32 % (819344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.93/4.32 % (819344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819344)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819344)Termination reason: Instruction limit % 28.93/4.32 % (819344)Termination phase: Saturation % 28.93/4.32 % (819344)Time elapsed: 0.500 s % 28.93/4.32 % (819344)Peak memory usage: 20 MB % 28.93/4.32 % (819344)Instructions burned: 880 (million) % 28.93/4.32 % (819360)ott-2_1_sil=16000:newcnf=on:random_seed=2903810357:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 28.93/4.32 % (819362)ott+10_1_sil=32000:tgt=ground:random_seed=890127108:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.93/4.32 % (819337)Instruction limit reached! % 28.93/4.32 % (819337)------------------------------ % 28.93/4.32 % (819337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.93/4.32 % (819337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819337)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819337)Termination reason: Instruction limit % 28.93/4.32 % (819337)Termination phase: Saturation % 28.93/4.32 % (819337)Time elapsed: 0.734 s % 28.93/4.32 % (819337)Peak memory usage: 19 MB % 28.93/4.32 % (819337)Instructions burned: 1179 (million) % 28.93/4.32 % (819364)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3167209897:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 28.93/4.32 % (819364)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.93/4.32 % (819364)Terminated due to inappropriate strategy. % 28.93/4.32 % (819364)------------------------------ % 28.93/4.32 % (819364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.93/4.32 % (819364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.93/4.32 % (819364)CaDiCaL version: 2.1.3 % 28.93/4.32 % (819364)Termination reason: Inappropriate % 28.93/4.32 % (819364)Time elapsed: 0.002 s % 28.93/4.32 % (819364)Peak memory usage: 11 MB % 28.93/4.32 % (819364)Instructions burned: 3 (million) % 28.93/4.32 % (819364)------------------------------ % 28.93/4.32 % (819364)------------------------------ % 28.93/4.32 % (819366)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1176490323:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 28.93/4.32 % (819360)Instruction limit reached! % 99.24/14.25 % (819360)------------------------------ % 99.24/14.25 % (819360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819360)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819360)Termination reason: Instruction limit % 99.24/14.25 % (819360)Termination phase: Saturation % 99.24/14.25 % (819360)Time elapsed: 0.532 s % 99.24/14.25 % (819360)Peak memory usage: 17 MB % 99.24/14.25 % (819360)Instructions burned: 870 (million) % 99.24/14.25 % (819368)dis+21_1_sil=32000:sas=cadical:random_seed=3982366057:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 99.24/14.25 % (819354)Instruction limit reached! % 99.24/14.25 % (819354)------------------------------ % 99.24/14.25 % (819354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819354)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819354)Termination reason: Instruction limit % 99.24/14.25 % (819354)Termination phase: Saturation % 99.24/14.25 % (819354)Time elapsed: 0.905 s % 99.24/14.25 % (819354)Peak memory usage: 25 MB % 99.24/14.25 % (819354)Instructions burned: 1472 (million) % 99.24/14.25 % (819370)ott+11_1_sil=16000:gs=on:random_seed=2123932500:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 99.24/14.25 % (819352)Instruction limit reached! % 99.24/14.25 % (819352)------------------------------ % 99.24/14.25 % (819352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819352)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819352)Termination reason: Instruction limit % 99.24/14.25 % (819352)Termination phase: Saturation % 99.24/14.25 % (819352)Time elapsed: 1.509 s % 99.24/14.25 % (819352)Peak memory usage: 41 MB % 99.24/14.25 % (819352)Instructions burned: 5134 (million) % 99.24/14.25 % (819372)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3232938466:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 99.24/14.25 % (819372)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.24/14.25 % (819372)Terminated due to inappropriate strategy. % 99.24/14.25 % (819372)------------------------------ % 99.24/14.25 % (819372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819372)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819372)Termination reason: Inappropriate % 99.24/14.25 % (819372)Time elapsed: 0.001 s % 99.24/14.25 % (819372)Peak memory usage: 11 MB % 99.24/14.25 % (819372)Instructions burned: 2 (million) % 99.24/14.25 % (819372)------------------------------ % 99.24/14.25 % (819372)------------------------------ % 99.24/14.25 % (819374)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=704690864:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 99.24/14.25 % (819370)Instruction limit reached! % 99.24/14.25 % (819370)------------------------------ % 99.24/14.25 % (819370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819370)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819370)Termination reason: Instruction limit % 99.24/14.25 % (819370)Termination phase: Saturation % 99.24/14.25 % (819370)Time elapsed: 1.346 s % 99.24/14.25 % (819370)Peak memory usage: 25 MB % 99.24/14.25 % (819370)Instructions burned: 2251 (million) % 99.24/14.25 % (819377)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=463504995:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 99.24/14.25 % (819366)Instruction limit reached! % 99.24/14.25 % (819366)------------------------------ % 99.24/14.25 % (819366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.24/14.25 % (819366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.24/14.25 % (819366)CaDiCaL version: 2.1.3 % 99.24/14.25 % (819366)Termination reason: Instruction limit % 99.24/14.25 % (819366)Termination phase: Saturation % 99.24/14.25 % (819366)Time elapsed: 1.993 s % 99.24/14.25 % (819366)Peak memory usage: 31 MB % 99.24/14.25 % (819366)Instructions burned: 3513 (million) % 99.24/14.25 % (819379)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=404649859:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 99.24/14.25 % (819374)Instruction limit reached! % 128.33/18.31 % (819374)------------------------------ % 128.33/18.31 % (819374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819374)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819374)Termination reason: Instruction limit % 128.33/18.31 % (819374)Termination phase: Saturation % 128.33/18.31 % (819374)Time elapsed: 1.230 s % 128.33/18.31 % (819374)Peak memory usage: 41 MB % 128.33/18.31 % (819374)Instructions burned: 4593 (million) % 128.33/18.31 % (819381)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=189804016:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 128.33/18.31 % (819381)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.33/18.31 % (819381)Terminated due to inappropriate strategy. % 128.33/18.31 % (819381)------------------------------ % 128.33/18.31 % (819381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819381)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819381)Termination reason: Inappropriate % 128.33/18.31 % (819381)Time elapsed: 0.001 s % 128.33/18.31 % (819381)Peak memory usage: 11 MB % 128.33/18.31 % (819381)Instructions burned: 3 (million) % 128.33/18.31 % (819381)------------------------------ % 128.33/18.31 % (819381)------------------------------ % 128.33/18.31 % (819383)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3490527914:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 128.33/18.31 % (819383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.33/18.31 % (819383)Terminated due to inappropriate strategy. % 128.33/18.31 % (819383)------------------------------ % 128.33/18.31 % (819383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819383)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819383)Termination reason: Inappropriate % 128.33/18.31 % (819383)Time elapsed: 0.001 s % 128.33/18.31 % (819383)Peak memory usage: 10 MB % 128.33/18.31 % (819383)Instructions burned: 2 (million) % 128.33/18.31 % (819383)------------------------------ % 128.33/18.31 % (819383)------------------------------ % 128.33/18.31 % (819385)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1213773078:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 128.33/18.31 % (819385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.33/18.31 % (819385)Terminated due to inappropriate strategy. % 128.33/18.31 % (819385)------------------------------ % 128.33/18.31 % (819385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819385)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819385)Termination reason: Inappropriate % 128.33/18.31 % (819385)Time elapsed: 0.001 s % 128.33/18.31 % (819385)Peak memory usage: 10 MB % 128.33/18.31 % (819385)Instructions burned: 2 (million) % 128.33/18.31 % (819385)------------------------------ % 128.33/18.31 % (819385)------------------------------ % 128.33/18.31 % (819387)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=286926710:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 128.33/18.31 % (819368)Instruction limit reached! % 128.33/18.31 % (819368)------------------------------ % 128.33/18.31 % (819368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819368)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819368)Termination reason: Instruction limit % 128.33/18.31 % (819368)Termination phase: Saturation % 128.33/18.31 % (819368)Time elapsed: 2.106 s % 128.33/18.31 % (819368)Peak memory usage: 33 MB % 128.33/18.31 % (819368)Instructions burned: 3775 (million) % 128.33/18.31 % (819389)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3408668523:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 128.33/18.31 % (819362)Instruction limit reached! % 128.33/18.31 % (819362)------------------------------ % 128.33/18.31 % (819362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.33/18.31 % (819362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.33/18.31 % (819362)CaDiCaL version: 2.1.3 % 128.33/18.31 % (819362)Termination reason: Instruction limit % 128.33/18.31 % (819362)Termination phase: Saturation % 128.33/18.31 % (819362)Time elapsed: 3.350 s % 134.71/19.24 % (819362)Peak memory usage: 35 MB % 134.71/19.24 % (819362)Instructions burned: 5115 (million) % 134.71/19.24 % (819391)dis+10_16:1_sil=16000:random_seed=437731019:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi) % 134.71/19.24 % (819379)Instruction limit reached! % 134.71/19.24 % (819379)------------------------------ % 134.71/19.24 % (819379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.24 % (819379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.24 % (819379)CaDiCaL version: 2.1.3 % 134.71/19.24 % (819379)Termination reason: Instruction limit % 134.71/19.24 % (819379)Termination phase: Saturation % 134.71/19.24 % (819379)Time elapsed: 2.654 s % 134.71/19.24 % (819379)Peak memory usage: 44 MB % 134.71/19.24 % (819379)Instructions burned: 5211 (million) % 134.71/19.24 % (819393)ott-3_8_sil=64000:random_seed=3701551671:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 134.71/19.24 % (819389)Instruction limit reached! % 134.71/19.24 % (819389)------------------------------ % 134.71/19.24 % (819389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.24 % (819389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.24 % (819389)CaDiCaL version: 2.1.3 % 134.71/19.24 % (819389)Termination reason: Instruction limit % 134.71/19.24 % (819389)Termination phase: Saturation % 134.71/19.24 % (819389)Time elapsed: 5.306 s % 134.71/19.24 % (819389)Peak memory usage: 58 MB % 134.71/19.24 % (819389)Instructions burned: 8173 (million) % 134.71/19.24 % (819395)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4101690101:fmbsr=2:i=32576_2912 on theBenchmark for (2912ds/32576Mi) % 134.71/19.24 % (819395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.71/19.24 % (819395)Terminated due to inappropriate strategy. % 134.71/19.24 % (819395)------------------------------ % 134.71/19.24 % (819395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.24 % (819395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.24 % (819395)CaDiCaL version: 2.1.3 % 134.71/19.24 % (819395)Termination reason: Inappropriate % 134.71/19.24 % (819395)Time elapsed: 0.002 s % 134.71/19.24 % (819395)Peak memory usage: 11 MB % 134.71/19.24 % (819395)Instructions burned: 3 (million) % 134.71/19.24 % (819395)------------------------------ % 134.71/19.24 % (819395)------------------------------ % 134.71/19.24 % (819397)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2266131407:i=11404_2912 on theBenchmark for (2912ds/11404Mi) % 134.71/19.24 % (819391)Instruction limit reached! % 134.71/19.24 % (819391)------------------------------ % 134.71/19.24 % (819391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.24 % (819391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.24 % (819391)CaDiCaL version: 2.1.3 % 134.71/19.24 % (819391)Termination reason: Instruction limit % 134.71/19.24 % (819391)Termination phase: Saturation % 134.71/19.24 % (819391)Time elapsed: 4.715 s % 134.71/19.24 % (819391)Peak memory usage: 52 MB % 134.71/19.24 % (819391)Instructions burned: 9156 (million) % 134.71/19.24 % (819399)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2167066742:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 134.71/19.24 % (819387)Instruction limit reached! % 134.71/19.24 % (819387)------------------------------ % 134.71/19.24 % (819387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.24 % (819387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.25 % (819387)CaDiCaL version: 2.1.3 % 134.71/19.25 % (819387)Termination reason: Instruction limit % 134.71/19.25 % (819387)Termination phase: Saturation % 134.71/19.25 % (819387)Time elapsed: 6.254 s % 134.71/19.25 % (819387)Peak memory usage: 379 MB % 134.71/19.25 % (819387)Instructions burned: 22566 (million) % 134.71/19.25 % (819401)dis+33_16_sil=32000:sac=on:random_seed=2986407518:i=15851:nm=0_2906 on theBenchmark for (2906ds/15851Mi) % 134.71/19.25 % (819401)Instruction limit reached! % 134.71/19.25 % (819401)------------------------------ % 134.71/19.25 % (819401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.71/19.25 % (819401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.71/19.25 % (819401)CaDiCaL version: 2.1.3 % 134.71/19.25 % (819401)Termination reason: Instruction limit % 134.71/19.25 % (819401)Termination phase: Saturation % 134.71/19.25 % (819401)Time elapsed: 4.596 s % 134.71/19.25 % (819401)Peak memory usage: 123 MB % 134.71/19.25 % (819401)Instructions burned: 15854 (million) % 134.71/19.25 % (819456)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1516540361:avsq=on:i=17627:add=on:amm=off_2859 on theBenchmark for (2859ds/17627Mi) % 140.64/20.13 % (819397)Instruction limit reached! % 140.64/20.13 % (819397)------------------------------ % 140.64/20.13 % (819397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819397)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819397)Termination reason: Instruction limit % 140.64/20.13 % (819397)Termination phase: Saturation % 140.64/20.13 % (819397)Time elapsed: 7.277 s % 140.64/20.13 % (819397)Peak memory usage: 62 MB % 140.64/20.13 % (819397)Instructions burned: 11404 (million) % 140.64/20.13 % (819467)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=504336224:s2a=on:i=53295_2839 on theBenchmark for (2839ds/53295Mi) % 140.64/20.13 % (819377)Instruction limit reached! % 140.64/20.13 % (819377)------------------------------ % 140.64/20.13 % (819377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819377)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819377)Termination reason: Instruction limit % 140.64/20.13 % (819377)Termination phase: Saturation % 140.64/20.13 % (819377)Time elapsed: 14.231 s % 140.64/20.13 % (819377)Peak memory usage: 112 MB % 140.64/20.13 % (819377)Instructions burned: 29341 (million) % 140.64/20.13 % (819469)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1874884020:i=26857:ins=20_2829 on theBenchmark for (2829ds/26857Mi) % 140.64/20.13 % (819469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.64/20.13 % (819469)Terminated due to inappropriate strategy. % 140.64/20.13 % (819469)------------------------------ % 140.64/20.13 % (819469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819469)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819469)Termination reason: Inappropriate % 140.64/20.13 % (819469)Time elapsed: 0.001 s % 140.64/20.13 % (819469)Peak memory usage: 10 MB % 140.64/20.13 % (819469)Instructions burned: 2 (million) % 140.64/20.13 % (819469)------------------------------ % 140.64/20.13 % (819469)------------------------------ % 140.64/20.13 % (819471)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2478674704:i=28120:bs=on:fsr=off_2829 on theBenchmark for (2829ds/28120Mi) % 140.64/20.13 % (819399)Instruction limit reached! % 140.64/20.13 % (819399)------------------------------ % 140.64/20.13 % (819399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819399)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819399)Termination reason: Instruction limit % 140.64/20.13 % (819399)Termination phase: Saturation % 140.64/20.13 % (819399)Time elapsed: 9.174 s % 140.64/20.13 % (819399)Peak memory usage: 70 MB % 140.64/20.13 % (819399)Instructions burned: 14134 (million) % 140.64/20.13 % (819473)fmb+10_1_sil=256000:fmbss=7:random_seed=3037007579:fmbsr=1.6:i=182295_2819 on theBenchmark for (2819ds/182295Mi) % 140.64/20.13 % (819473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.64/20.13 % (819473)Terminated due to inappropriate strategy. % 140.64/20.13 % (819473)------------------------------ % 140.64/20.13 % (819473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819473)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819473)Termination reason: Inappropriate % 140.64/20.13 % (819473)Time elapsed: 0.001 s % 140.64/20.13 % (819473)Peak memory usage: 10 MB % 140.64/20.13 % (819473)Instructions burned: 2 (million) % 140.64/20.13 % (819473)------------------------------ % 140.64/20.13 % (819473)------------------------------ % 140.64/20.13 % (819475)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1765963767:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 140.64/20.13 % (819475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.64/20.13 % (819475)Terminated due to inappropriate strategy. % 140.64/20.13 % (819475)------------------------------ % 140.64/20.13 % (819475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.64/20.13 % (819475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.64/20.13 % (819475)CaDiCaL version: 2.1.3 % 140.64/20.13 % (819475)Termination reason: Inappropriate % 162.67/23.14 % (819475)Time elapsed: 0.002 s % 162.67/23.14 % (819475)Peak memory usage: 11 MB % 162.67/23.14 % (819475)Instructions burned: 4 (million) % 162.67/23.14 % (819475)------------------------------ % 162.67/23.14 % (819475)------------------------------ % 162.67/23.14 % (819477)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1484642993:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 162.67/23.14 % (819477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.67/23.14 % (819477)Terminated due to inappropriate strategy. % 162.67/23.14 % (819477)------------------------------ % 162.67/23.14 % (819477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.67/23.14 % (819477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.67/23.14 % (819477)CaDiCaL version: 2.1.3 % 162.67/23.14 % (819477)Termination reason: Inappropriate % 162.67/23.14 % (819477)Time elapsed: 0.001 s % 162.67/23.14 % (819477)Peak memory usage: 10 MB % 162.67/23.14 % (819477)Instructions burned: 2 (million) % 162.67/23.14 % (819477)------------------------------ % 162.67/23.14 % (819477)------------------------------ % 162.67/23.14 % (819479)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=577808799:fmbsr=1.3:i=225729_2818 on theBenchmark for (2818ds/225729Mi) % 162.67/23.14 % (819479)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.67/23.14 % (819479)Terminated due to inappropriate strategy. % 162.67/23.14 % (819479)------------------------------ % 162.67/23.14 % (819479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.67/23.14 % (819479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.67/23.14 % (819479)CaDiCaL version: 2.1.3 % 162.67/23.14 % (819479)Termination reason: Inappropriate % 162.67/23.14 % (819479)Time elapsed: 0.002 s % 162.67/23.14 % (819479)Peak memory usage: 10 MB % 162.67/23.14 % (819479)Instructions burned: 2 (million) % 162.67/23.14 % (819479)------------------------------ % 162.67/23.14 % (819479)------------------------------ % 162.67/23.14 % (819481)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=301818076:fmbsr=2:i=185024:ins=7_2818 on theBenchmark for (2818ds/185024Mi) % 162.67/23.14 % (819481)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.67/23.14 % (819481)Terminated due to inappropriate strategy. % 162.67/23.14 % (819481)------------------------------ % 162.67/23.14 % (819481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.67/23.14 % (819481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.67/23.14 % (819481)CaDiCaL version: 2.1.3 % 162.67/23.14 % (819481)Termination reason: Inappropriate % 162.67/23.14 % (819481)Time elapsed: 0.002 s % 162.67/23.14 % (819481)Peak memory usage: 10 MB % 162.67/23.14 % (819481)Instructions burned: 2 (million) % 162.67/23.14 % (819481)------------------------------ % 162.67/23.14 % (819481)------------------------------ % 162.67/23.14 % (819483)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3438430841:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 162.67/23.14 % (819483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.67/23.14 % (819483)Terminated due to inappropriate strategy. % 162.67/23.14 % (819483)------------------------------ % 162.67/23.14 % (819483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.67/23.14 % (819483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.67/23.14 % (819483)CaDiCaL version: 2.1.3 % 162.67/23.14 % (819483)Termination reason: Inappropriate % 162.67/23.14 % (819483)Time elapsed: 0.002 s % 162.67/23.14 % (819483)Peak memory usage: 11 MB % 162.67/23.14 % (819483)Instructions burned: 3 (million) % 162.67/23.14 % (819483)------------------------------ % 162.67/23.14 % (819483)------------------------------ % 162.67/23.14 % (819485)% WARNING: option uhcvi not known. % 162.67/23.14 % (819485)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2149931796:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 162.67/23.14 % (819456)Instruction limit reached! % 162.67/23.14 % (819456)------------------------------ % 162.67/23.14 % (819456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.67/23.14 % (819456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.67/23.14 % (819456)CaDiCaL version: 2.1.3 % 162.67/23.14 % (819456)Termination reason: Instruction limit % 162.67/23.14 % (819456)Termination phase: Saturation % 162.67/23.14 % (819456)Time elapsed: 4.968 s % 162.67/23.14 % (819456)Peak memory usage: 239 MB % 162.67/23.14 % (819456)Instructions burned: 17631 (million) % 162.67/23.14 % (819487)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1536816824:i=176048:add=on:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/176048Mi) % 176.85/25.19 % (819393)Instruction limit reached! % 176.85/25.19 % (819393)------------------------------ % 176.85/25.19 % (819393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819393)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819393)Termination reason: Instruction limit % 176.85/25.19 % (819393)Termination phase: Saturation % 176.85/25.19 % (819393)Time elapsed: 13.469 s % 176.85/25.19 % (819393)Peak memory usage: 84 MB % 176.85/25.19 % (819393)Instructions burned: 20140 (million) % 176.85/25.19 % (819489)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2381531797:i=206:fgj=on:rtra=on_2808 on theBenchmark for (2808ds/206Mi) % 176.85/25.19 % (819489)Instruction limit reached! % 176.85/25.19 % (819489)------------------------------ % 176.85/25.19 % (819489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819489)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819489)Termination reason: Instruction limit % 176.85/25.19 % (819489)Termination phase: Saturation % 176.85/25.19 % (819489)Time elapsed: 0.132 s % 176.85/25.19 % (819489)Peak memory usage: 14 MB % 176.85/25.19 % (819489)Instructions burned: 207 (million) % 176.85/25.19 % (819491)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2895002719:i=232:rtra=on_2807 on theBenchmark for (2807ds/232Mi) % 176.85/25.19 % (819491)Instruction limit reached! % 176.85/25.19 % (819491)------------------------------ % 176.85/25.19 % (819491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819491)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819491)Termination reason: Instruction limit % 176.85/25.19 % (819491)Termination phase: Saturation % 176.85/25.19 % (819491)Time elapsed: 0.147 s % 176.85/25.19 % (819491)Peak memory usage: 13 MB % 176.85/25.19 % (819491)Instructions burned: 232 (million) % 176.85/25.19 % (819493)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1233681243:i=262:rtra=on_2805 on theBenchmark for (2805ds/262Mi) % 176.85/25.19 % (819493)Instruction limit reached! % 176.85/25.19 % (819493)------------------------------ % 176.85/25.19 % (819493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819493)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819493)Termination reason: Instruction limit % 176.85/25.19 % (819493)Termination phase: Saturation % 176.85/25.19 % (819493)Time elapsed: 0.169 s % 176.85/25.19 % (819493)Peak memory usage: 14 MB % 176.85/25.19 % (819493)Instructions burned: 263 (million) % 176.85/25.19 % (819495)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=856346513:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2803 on theBenchmark for (2803ds/318Mi) % 176.85/25.19 % (819495)Instruction limit reached! % 176.85/25.19 % (819495)------------------------------ % 176.85/25.19 % (819495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819495)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819495)Termination reason: Instruction limit % 176.85/25.19 % (819495)Termination phase: Saturation % 176.85/25.19 % (819495)Time elapsed: 0.229 s % 176.85/25.19 % (819495)Peak memory usage: 15 MB % 176.85/25.19 % (819495)Instructions burned: 319 (million) % 176.85/25.19 % (819497)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3766621053:i=1428:nm=2:rtra=on_2801 on theBenchmark for (2801ds/1428Mi) % 176.85/25.19 % (819497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.85/25.19 % (819497)Terminated due to inappropriate strategy. % 176.85/25.19 % (819497)------------------------------ % 176.85/25.19 % (819497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.85/25.19 % (819497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.85/25.19 % (819497)CaDiCaL version: 2.1.3 % 176.85/25.19 % (819497)Termination reason: Inappropriate % 176.85/25.19 % (819497)Time elapsed: 0.002 s % 176.85/25.19 % (819497)Peak memory usage: 10 MB % 176.85/25.19 % (819497)Instructions burned: 2 (million) % 176.85/25.19 % (819497)------------------------------ % 176.85/25.19 % (819497)------------------------------ % 230.53/32.79 % (819499)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3417719246:i=262:bd=preordered:rtra=on:fsd=on_2800 on theBenchmark for (2800ds/262Mi) % 230.53/32.79 % (819499)Instruction limit reached! % 230.53/32.79 % (819499)------------------------------ % 230.53/32.79 % (819499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819499)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819499)Termination reason: Instruction limit % 230.53/32.79 % (819499)Termination phase: Saturation % 230.53/32.79 % (819499)Time elapsed: 0.186 s % 230.53/32.79 % (819499)Peak memory usage: 14 MB % 230.53/32.79 % (819499)Instructions burned: 263 (million) % 230.53/32.79 % (819501)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=2424189743:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/1368Mi) % 230.53/32.79 % (819501)Instruction limit reached! % 230.53/32.79 % (819501)------------------------------ % 230.53/32.79 % (819501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819501)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819501)Termination reason: Instruction limit % 230.53/32.79 % (819501)Termination phase: Saturation % 230.53/32.79 % (819501)Time elapsed: 0.625 s % 230.53/32.79 % (819501)Peak memory usage: 18 MB % 230.53/32.79 % (819501)Instructions burned: 1370 (million) % 230.53/32.79 % (819503)ott-21_1_sil=16000:si=on:fs=off:random_seed=2876344002:i=360:av=off:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/360Mi) % 230.53/32.79 % (819503)Instruction limit reached! % 230.53/32.79 % (819503)------------------------------ % 230.53/32.79 % (819503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819503)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819503)Termination reason: Instruction limit % 230.53/32.79 % (819503)Termination phase: Saturation % 230.53/32.79 % (819503)Time elapsed: 0.161 s % 230.53/32.79 % (819503)Peak memory usage: 13 MB % 230.53/32.79 % (819503)Instructions burned: 362 (million) % 230.53/32.79 % (819505)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1967676697:i=954:bd=all:rtra=on_2790 on theBenchmark for (2790ds/954Mi) % 230.53/32.79 % (819505)Instruction limit reached! % 230.53/32.79 % (819505)------------------------------ % 230.53/32.79 % (819505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819505)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819505)Termination reason: Instruction limit % 230.53/32.79 % (819505)Termination phase: Saturation % 230.53/32.79 % (819505)Time elapsed: 0.655 s % 230.53/32.79 % (819505)Peak memory usage: 16 MB % 230.53/32.79 % (819505)Instructions burned: 955 (million) % 230.53/32.79 % (819507)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3338597487:fmbsr=1.3:i=1730:ins=25:rtra=on_2783 on theBenchmark for (2783ds/1730Mi) % 230.53/32.79 % (819507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.53/32.79 % (819507)Terminated due to inappropriate strategy. % 230.53/32.79 % (819507)------------------------------ % 230.53/32.79 % (819507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819507)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819507)Termination reason: Inappropriate % 230.53/32.79 % (819507)Time elapsed: 0.001 s % 230.53/32.79 % (819507)Peak memory usage: 10 MB % 230.53/32.79 % (819507)Instructions burned: 2 (million) % 230.53/32.79 % (819507)------------------------------ % 230.53/32.79 % (819507)------------------------------ % 230.53/32.79 % (819509)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=364189485:i=2358:rtra=on_2783 on theBenchmark for (2783ds/2358Mi) % 230.53/32.79 % (819509)Instruction limit reached! % 230.53/32.79 % (819509)------------------------------ % 230.53/32.79 % (819509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.53/32.79 % (819509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.53/32.79 % (819509)CaDiCaL version: 2.1.3 % 230.53/32.79 % (819509)Termination reason: Instruction limit % 230.53/32.79 % (819509)Termination phase: Saturation % 286.87/40.78 % (819509)Time elapsed: 1.259 s % 286.87/40.78 % (819509)Peak memory usage: 21 MB % 286.87/40.78 % (819509)Instructions burned: 2358 (million) % 286.87/40.78 % (819511)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2431960792:i=1778:ins=1:rtra=on_2770 on theBenchmark for (2770ds/1778Mi) % 286.87/40.78 % (819511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.87/40.78 % (819511)Terminated due to inappropriate strategy. % 286.87/40.78 % (819511)------------------------------ % 286.87/40.78 % (819511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.87/40.78 % (819511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.87/40.78 % (819511)CaDiCaL version: 2.1.3 % 286.87/40.78 % (819511)Termination reason: Inappropriate % 286.87/40.78 % (819511)Time elapsed: 0.002 s % 286.87/40.78 % (819511)Peak memory usage: 10 MB % 286.87/40.78 % (819511)Instructions burned: 2 (million) % 286.87/40.78 % (819511)------------------------------ % 286.87/40.78 % (819511)------------------------------ % 286.87/40.78 % (819513)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=1890022171:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1384Mi) % 286.87/40.78 % (819513)Instruction limit reached! % 286.87/40.78 % (819513)------------------------------ % 286.87/40.78 % (819513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.87/40.78 % (819513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.87/40.78 % (819513)CaDiCaL version: 2.1.3 % 286.87/40.78 % (819513)Termination reason: Instruction limit % 286.87/40.78 % (819513)Termination phase: Saturation % 286.87/40.78 % (819513)Time elapsed: 0.899 s % 286.87/40.78 % (819513)Peak memory usage: 25 MB % 286.87/40.78 % (819513)Instructions burned: 1385 (million) % 286.87/40.78 % (819515)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=709781129:i=1758:kws=inv_precedence:fsr=off:rtra=on_2761 on theBenchmark for (2761ds/1758Mi) % 286.87/40.78 % (819515)Instruction limit reached! % 286.87/40.78 % (819515)------------------------------ % 286.87/40.78 % (819515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.87/40.78 % (819515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.87/40.78 % (819515)CaDiCaL version: 2.1.3 % 286.87/40.78 % (819515)Termination reason: Instruction limit % 286.87/40.78 % (819515)Termination phase: Saturation % 286.87/40.78 % (819515)Time elapsed: 1.010 s % 286.87/40.78 % (819515)Peak memory usage: 24 MB % 286.87/40.78 % (819515)Instructions burned: 1759 (million) % 286.87/40.78 % (819517)fmb+10_1_sil=64000:si=on:random_seed=3765952135:i=44122:nm=2:rtra=on:gsp=on_2750 on theBenchmark for (2750ds/44122Mi) % 286.87/40.78 % (819517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.87/40.78 % (819517)Terminated due to inappropriate strategy. % 286.87/40.78 % (819517)------------------------------ % 286.87/40.78 % (819517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.87/40.78 % (819517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.87/40.78 % (819517)CaDiCaL version: 2.1.3 % 286.87/40.78 % (819517)Termination reason: Inappropriate % 286.87/40.78 % (819517)Time elapsed: 0.002 s % 286.87/40.78 % (819517)Peak memory usage: 10 MB % 286.87/40.78 % (819517)Instructions burned: 3 (million) % 286.87/40.78 % (819517)------------------------------ % 286.87/40.78 % (819517)------------------------------ % 286.87/40.78 % (819519)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3910108852:i=19030:nm=5:rtra=on_2750 on theBenchmark for (2750ds/19030Mi) % 286.87/40.78 % (819519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.87/40.78 % (819519)Terminated due to inappropriate strategy. % 286.87/40.78 % (819519)------------------------------ % 286.87/40.78 % (819519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.87/40.78 % (819519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.87/40.78 % (819519)CaDiCaL version: 2.1.3 % 286.87/40.78 % (819519)Termination reason: Inappropriate % 286.87/40.78 % (819519)Time elapsed: 0.002 s % 286.87/40.78 % (819519)Peak memory usage: 11 MB % 286.87/40.78 % (819519)Instructions burned: 2 (million) % 286.87/40.78 % (819519)------------------------------ % 286.87/40.78 % (819519)------------------------------ % 286.87/40.78 % (819521)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2732909142:fmbsr=1.7:i=1840:rtra=on_2750 oTerminated % 300.29/42.63 % Vampire exiting %------------------------------------------------------------------------------