%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW622_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.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:32 PM UTC 2026 % Result : Timeout 300.46s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW622_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n002.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:25:37 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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 % 6.44/1.19 % (384401)Will run a generic schedule for satisfiability detection. % 6.44/1.19 % (384407)% WARNING: option uhcvi not known. % 6.44/1.19 % (384407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2386739308:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.44/1.19 % (384406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3290146721_2999 on theBenchmark for (2999ds/0Mi) % 6.44/1.19 % (384408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1389090141:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.44/1.19 % (384409)dis+10_1_sil=32000:sp=arity:random_seed=1276745830:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.44/1.19 % (384410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3833860991:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.44/1.19 % (384406)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.44/1.19 % (384406)Terminated due to inappropriate strategy. % 6.44/1.19 % (384406)------------------------------ % 6.44/1.19 % (384406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.19 % (384406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.19 % (384406)CaDiCaL version: 2.1.3 % 6.44/1.19 % (384406)Termination reason: Inappropriate % 6.44/1.19 % (384406)Time elapsed: 0.007 s % 6.44/1.19 % (384406)Peak memory usage: 11 MB % 6.44/1.19 % (384406)Instructions burned: 12 (million) % 6.44/1.19 % (384406)------------------------------ % 6.44/1.19 % (384406)------------------------------ % 6.44/1.19 % (384411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1502131797:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.44/1.19 % (384412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3883131183:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.44/1.19 % (384418)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2465855930:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.44/1.19 % (384418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.44/1.19 % (384418)Terminated due to inappropriate strategy. % 6.44/1.19 % (384418)------------------------------ % 6.44/1.19 % (384418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.19 % (384418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.19 % (384418)CaDiCaL version: 2.1.3 % 6.44/1.19 % (384418)Termination reason: Inappropriate % 6.44/1.19 % (384418)Time elapsed: 0.005 s % 6.44/1.19 % (384418)Peak memory usage: 11 MB % 6.44/1.19 % (384418)Instructions burned: 10 (million) % 6.44/1.19 % (384418)------------------------------ % 6.44/1.19 % (384418)------------------------------ % 6.44/1.19 % (384422)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=230011272:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.44/1.19 % (384409)Instruction limit reached! % 6.44/1.19 % (384409)------------------------------ % 6.44/1.19 % (384409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.19 % (384409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.19 % (384409)CaDiCaL version: 2.1.3 % 6.44/1.19 % (384409)Termination reason: Instruction limit % 6.44/1.19 % (384409)Termination phase: Saturation % 6.44/1.19 % (384409)Time elapsed: 0.063 s % 6.44/1.19 % (384409)Peak memory usage: 13 MB % 6.44/1.19 % (384409)Instructions burned: 103 (million) % 6.44/1.19 % (384410)Instruction limit reached! % 6.44/1.19 % (384410)------------------------------ % 6.44/1.19 % (384410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.19 % (384410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.19 % (384410)CaDiCaL version: 2.1.3 % 6.44/1.19 % (384410)Termination reason: Instruction limit % 6.44/1.19 % (384410)Termination phase: Saturation % 6.44/1.19 % (384410)Time elapsed: 0.073 s % 6.44/1.19 % (384410)Peak memory usage: 13 MB % 6.44/1.19 % (384410)Instructions burned: 116 (million) % 6.44/1.19 % (384424)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=127430334:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.44/1.19 % (384426)ott-21_1_sil=16000:fs=off:random_seed=532598626:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.44/1.19 % (384411)Instruction limit reached! % 6.44/1.19 % (384411)------------------------------ % 10.59/2.07 % (384411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384411)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384411)Termination reason: Instruction limit % 10.59/2.07 % (384411)Termination phase: Saturation % 10.59/2.07 % (384411)Time elapsed: 0.090 s % 10.59/2.07 % (384411)Peak memory usage: 14 MB % 10.59/2.07 % (384411)Instructions burned: 131 (million) % 10.59/2.07 % (384436)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1987913982:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 10.59/2.07 % (384412)Instruction limit reached! % 10.59/2.07 % (384412)------------------------------ % 10.59/2.07 % (384412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384412)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384412)Termination reason: Instruction limit % 10.59/2.07 % (384412)Termination phase: Saturation % 10.59/2.07 % (384412)Time elapsed: 0.149 s % 10.59/2.07 % (384412)Peak memory usage: 14 MB % 10.59/2.07 % (384412)Instructions burned: 159 (million) % 10.59/2.07 % (384422)Instruction limit reached! % 10.59/2.07 % (384422)------------------------------ % 10.59/2.07 % (384422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384422)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384422)Termination reason: Instruction limit % 10.59/2.07 % (384422)Termination phase: Saturation % 10.59/2.07 % (384422)Time elapsed: 0.118 s % 10.59/2.07 % (384422)Peak memory usage: 13 MB % 10.59/2.07 % (384422)Instructions burned: 132 (million) % 10.59/2.07 % (384438)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2947472009:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 10.59/2.07 % (384438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 10.59/2.07 % (384438)Terminated due to inappropriate strategy. % 10.59/2.07 % (384438)------------------------------ % 10.59/2.07 % (384438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384438)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384438)Termination reason: Inappropriate % 10.59/2.07 % (384438)Time elapsed: 0.006 s % 10.59/2.07 % (384438)Peak memory usage: 10 MB % 10.59/2.07 % (384438)Instructions burned: 11 (million) % 10.59/2.07 % (384438)------------------------------ % 10.59/2.07 % (384438)------------------------------ % 10.59/2.07 % (384441)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3875199400:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 10.59/2.07 % (384441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 10.59/2.07 % (384441)Terminated due to inappropriate strategy. % 10.59/2.07 % (384441)------------------------------ % 10.59/2.07 % (384441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384441)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384441)Termination reason: Inappropriate % 10.59/2.07 % (384441)Time elapsed: 0.006 s % 10.59/2.07 % (384441)Peak memory usage: 10 MB % 10.59/2.07 % (384441)Instructions burned: 10 (million) % 10.59/2.07 % (384441)------------------------------ % 10.59/2.07 % (384441)------------------------------ % 10.59/2.07 % (384439)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2852193677:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 10.59/2.07 % (384443)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=845533181:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 10.59/2.07 % (384426)Instruction limit reached! % 10.59/2.07 % (384426)------------------------------ % 10.59/2.07 % (384426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.59/2.07 % (384426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.59/2.07 % (384426)CaDiCaL version: 2.1.3 % 10.59/2.07 % (384426)Termination reason: Instruction limit % 10.59/2.07 % (384426)Termination phase: Saturation % 10.59/2.07 % (384426)Time elapsed: 0.152 s % 10.59/2.07 % (384426)Peak memory usage: 13 MB % 10.59/2.07 % (384426)Instructions burned: 181 (million) % 35.69/5.35 % (384446)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3447756910:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.69/5.35 % (384436)Instruction limit reached! % 35.69/5.35 % (384436)------------------------------ % 35.69/5.35 % (384436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.35 % (384436)CaDiCaL version: 2.1.3 % 35.69/5.35 % (384436)Termination reason: Instruction limit % 35.69/5.35 % (384436)Termination phase: Saturation % 35.69/5.35 % (384436)Time elapsed: 0.424 s % 35.69/5.35 % (384436)Peak memory usage: 13 MB % 35.69/5.35 % (384436)Instructions burned: 477 (million) % 35.69/5.35 % (384464)fmb+10_1_sil=64000:random_seed=3915497819:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 35.69/5.35 % (384464)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.35 % (384464)Terminated due to inappropriate strategy. % 35.69/5.35 % (384464)------------------------------ % 35.69/5.35 % (384464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.35 % (384464)CaDiCaL version: 2.1.3 % 35.69/5.35 % (384464)Termination reason: Inappropriate % 35.69/5.35 % (384464)Time elapsed: 0.006 s % 35.69/5.35 % (384464)Peak memory usage: 11 MB % 35.69/5.35 % (384464)Instructions burned: 11 (million) % 35.69/5.35 % (384464)------------------------------ % 35.69/5.35 % (384464)------------------------------ % 35.69/5.35 % (384469)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3435783478:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 35.69/5.35 % (384469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.35 % (384469)Terminated due to inappropriate strategy. % 35.69/5.35 % (384469)------------------------------ % 35.69/5.35 % (384469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.35 % (384469)CaDiCaL version: 2.1.3 % 35.69/5.35 % (384469)Termination reason: Inappropriate % 35.69/5.35 % (384469)Time elapsed: 0.006 s % 35.69/5.35 % (384469)Peak memory usage: 11 MB % 35.69/5.35 % (384469)Instructions burned: 10 (million) % 35.69/5.35 % (384469)------------------------------ % 35.69/5.35 % (384469)------------------------------ % 35.69/5.35 % (384475)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3809887860:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 35.69/5.35 % (384475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.35 % (384475)Terminated due to inappropriate strategy. % 35.69/5.35 % (384475)------------------------------ % 35.69/5.35 % (384475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.35 % (384475)CaDiCaL version: 2.1.3 % 35.69/5.35 % (384475)Termination reason: Inappropriate % 35.69/5.35 % (384475)Time elapsed: 0.008 s % 35.69/5.35 % (384475)Peak memory usage: 11 MB % 35.69/5.35 % (384475)Instructions burned: 10 (million) % 35.69/5.35 % (384475)------------------------------ % 35.69/5.35 % (384475)------------------------------ % 35.69/5.35 % (384424)Instruction limit reached! % 35.69/5.35 % (384424)------------------------------ % 35.69/5.35 % (384424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.35 % (384424)CaDiCaL version: 2.1.3 % 35.69/5.35 % (384424)Termination reason: Instruction limit % 35.69/5.35 % (384424)Termination phase: Saturation % 35.69/5.35 % (384424)Time elapsed: 0.622 s % 35.69/5.35 % (384424)Peak memory usage: 17 MB % 35.69/5.35 % (384424)Instructions burned: 684 (million) % 35.69/5.35 % (384478)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2670576258:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 35.69/5.35 % (384479)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=529712943:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 35.69/5.35 % (384443)Instruction limit reached! % 35.69/5.35 % (384443)------------------------------ % 35.69/5.35 % (384443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.35 % (384443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384443)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384443)Termination reason: Instruction limit % 56.06/8.20 % (384443)Termination phase: Saturation % 56.06/8.20 % (384443)Time elapsed: 0.672 s % 56.06/8.20 % (384443)Peak memory usage: 21 MB % 56.06/8.20 % (384443)Instructions burned: 692 (million) % 56.06/8.20 % (384493)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=661608753:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 56.06/8.20 % (384493)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.06/8.20 % (384493)Terminated due to inappropriate strategy. % 56.06/8.20 % (384493)------------------------------ % 56.06/8.20 % (384493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.06/8.20 % (384493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384493)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384493)Termination reason: Inappropriate % 56.06/8.20 % (384493)Time elapsed: 0.007 s % 56.06/8.20 % (384493)Peak memory usage: 11 MB % 56.06/8.20 % (384493)Instructions burned: 12 (million) % 56.06/8.20 % (384493)------------------------------ % 56.06/8.20 % (384493)------------------------------ % 56.06/8.20 % (384497)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1133290622:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 56.06/8.20 % (384497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.06/8.20 % (384497)Terminated due to inappropriate strategy. % 56.06/8.20 % (384497)------------------------------ % 56.06/8.20 % (384497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.06/8.20 % (384497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384497)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384497)Termination reason: Inappropriate % 56.06/8.20 % (384497)Time elapsed: 0.006 s % 56.06/8.20 % (384497)Peak memory usage: 11 MB % 56.06/8.20 % (384497)Instructions burned: 10 (million) % 56.06/8.20 % (384497)------------------------------ % 56.06/8.20 % (384497)------------------------------ % 56.06/8.20 % (384501)ott-2_1_sil=16000:newcnf=on:random_seed=2849075197:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 56.06/8.20 % (384446)Instruction limit reached! % 56.06/8.20 % (384446)------------------------------ % 56.06/8.20 % (384446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.06/8.20 % (384446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384446)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384446)Termination reason: Instruction limit % 56.06/8.20 % (384446)Termination phase: Saturation % 56.06/8.20 % (384446)Time elapsed: 0.750 s % 56.06/8.20 % (384446)Peak memory usage: 19 MB % 56.06/8.20 % (384446)Instructions burned: 879 (million) % 56.06/8.20 % (384504)ott+10_1_sil=32000:tgt=ground:random_seed=2624015655:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 56.06/8.20 % (384439)Instruction limit reached! % 56.06/8.20 % (384439)------------------------------ % 56.06/8.20 % (384439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.06/8.20 % (384439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384439)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384439)Termination reason: Instruction limit % 56.06/8.20 % (384439)Termination phase: Saturation % 56.06/8.20 % (384439)Time elapsed: 1.121 s % 56.06/8.20 % (384439)Peak memory usage: 20 MB % 56.06/8.20 % (384439)Instructions burned: 1179 (million) % 56.06/8.20 % (384522)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=339011145:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 56.06/8.20 % (384522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.06/8.20 % (384522)Terminated due to inappropriate strategy. % 56.06/8.20 % (384522)------------------------------ % 56.06/8.20 % (384522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.06/8.20 % (384522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.06/8.20 % (384522)CaDiCaL version: 2.1.3 % 56.06/8.20 % (384522)Termination reason: Inappropriate % 56.06/8.20 % (384522)Time elapsed: 0.010 s % 56.06/8.20 % (384522)Peak memory usage: 11 MB % 56.06/8.20 % (384522)Instructions burned: 12 (million) % 56.06/8.20 % (384522)------------------------------ % 56.06/8.20 % (384522)------------------------------ % 56.06/8.20 % (384524)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1677631850:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 56.06/8.20 % (384501)Instruction limit reached! % 169.15/25.74 % (384501)------------------------------ % 169.15/25.74 % (384501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.74 % (384501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.74 % (384501)CaDiCaL version: 2.1.3 % 169.15/25.74 % (384501)Termination reason: Instruction limit % 169.15/25.74 % (384501)Termination phase: Saturation % 169.15/25.74 % (384501)Time elapsed: 0.789 s % 169.15/25.74 % (384501)Peak memory usage: 17 MB % 169.15/25.74 % (384501)Instructions burned: 869 (million) % 169.15/25.74 % (384539)dis+21_1_sil=32000:sas=cadical:random_seed=2021632494:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 169.15/25.74 % (384479)Instruction limit reached! % 169.15/25.74 % (384479)------------------------------ % 169.15/25.74 % (384479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.74 % (384479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.74 % (384479)CaDiCaL version: 2.1.3 % 169.15/25.74 % (384479)Termination reason: Instruction limit % 169.15/25.74 % (384479)Termination phase: Saturation % 169.15/25.74 % (384479)Time elapsed: 1.336 s % 169.15/25.74 % (384479)Peak memory usage: 28 MB % 169.15/25.74 % (384479)Instructions burned: 1472 (million) % 169.15/25.74 % (384551)ott+11_1_sil=16000:gs=on:random_seed=710869233:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 169.15/25.74 % (384551)Instruction limit reached! % 169.15/25.74 % (384551)------------------------------ % 169.15/25.74 % (384551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.74 % (384551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.74 % (384551)CaDiCaL version: 2.1.3 % 169.15/25.74 % (384551)Termination reason: Instruction limit % 169.15/25.74 % (384551)Termination phase: Saturation % 169.15/25.74 % (384551)Time elapsed: 2.044 s % 169.15/25.74 % (384551)Peak memory usage: 19 MB % 169.15/25.74 % (384551)Instructions burned: 2251 (million) % 169.15/25.74 % (384603)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4079899093:fmbsr=1.6:i=67534_2957 on theBenchmark for (2957ds/67534Mi) % 169.15/25.74 % (384603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.15/25.74 % (384603)Terminated due to inappropriate strategy. % 169.15/25.74 % (384603)------------------------------ % 169.15/25.74 % (384603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.74 % (384603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.74 % (384603)CaDiCaL version: 2.1.3 % 169.15/25.74 % (384603)Termination reason: Inappropriate % 169.15/25.74 % (384603)Time elapsed: 0.010 s % 169.15/25.74 % (384603)Peak memory usage: 11 MB % 169.15/25.74 % (384603)Instructions burned: 11 (million) % 169.15/25.74 % (384603)------------------------------ % 169.15/25.74 % (384603)------------------------------ % 169.15/25.74 % (384606)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3293855036:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2957 on theBenchmark for (2957ds/4591Mi) % 169.15/25.74 % (384524)Instruction limit reached! % 169.15/25.74 % (384524)------------------------------ % 169.15/25.74 % (384524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.74 % (384524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.75 % (384524)CaDiCaL version: 2.1.3 % 169.15/25.75 % (384524)Termination reason: Instruction limit % 169.15/25.75 % (384524)Termination phase: Saturation % 169.15/25.75 % (384524)Time elapsed: 3.223 s % 169.15/25.75 % (384524)Peak memory usage: 35 MB % 169.15/25.75 % (384524)Instructions burned: 3512 (million) % 169.15/25.75 % (384619)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=48747067:i=29340_2952 on theBenchmark for (2952ds/29340Mi) % 169.15/25.75 % (384539)Instruction limit reached! % 169.15/25.75 % (384539)------------------------------ % 169.15/25.75 % (384539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.15/25.75 % (384539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.15/25.75 % (384539)CaDiCaL version: 2.1.3 % 169.15/25.75 % (384539)Termination reason: Instruction limit % 169.15/25.75 % (384539)Termination phase: Saturation % 169.15/25.75 % (384539)Time elapsed: 3.132 s % 169.15/25.75 % (384539)Peak memory usage: 34 MB % 169.15/25.75 % (384539)Instructions burned: 3773 (million) % 169.15/25.75 % (384627)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3292342865:i=5211_2949 on theBenchmark for (2949ds/5211Mi) % 169.15/25.75 % (384478)Instruction limit reached! % 222.14/31.56 % (384478)------------------------------ % 222.14/31.56 % (384478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384478)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384478)Termination reason: Instruction limit % 222.14/31.56 % (384478)Termination phase: Saturation % 222.14/31.56 % (384478)Time elapsed: 4.361 s % 222.14/31.56 % (384478)Peak memory usage: 44 MB % 222.14/31.56 % (384478)Instructions burned: 5132 (million) % 222.14/31.56 % (384631)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1202681664:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 222.14/31.56 % (384631)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.14/31.56 % (384631)Terminated due to inappropriate strategy. % 222.14/31.56 % (384631)------------------------------ % 222.14/31.56 % (384631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384631)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384631)Termination reason: Inappropriate % 222.14/31.56 % (384631)Time elapsed: 0.012 s % 222.14/31.56 % (384631)Peak memory usage: 11 MB % 222.14/31.56 % (384631)Instructions burned: 12 (million) % 222.14/31.56 % (384631)------------------------------ % 222.14/31.56 % (384631)------------------------------ % 222.14/31.56 % (384634)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2062052829:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 222.14/31.56 % (384634)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.14/31.56 % (384634)Terminated due to inappropriate strategy. % 222.14/31.56 % (384634)------------------------------ % 222.14/31.56 % (384634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384634)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384634)Termination reason: Inappropriate % 222.14/31.56 % (384634)Time elapsed: 0.012 s % 222.14/31.56 % (384634)Peak memory usage: 11 MB % 222.14/31.56 % (384634)Instructions burned: 11 (million) % 222.14/31.56 % (384634)------------------------------ % 222.14/31.56 % (384634)------------------------------ % 222.14/31.56 % (384637)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1191369148:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 222.14/31.56 % (384637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.14/31.56 % (384637)Terminated due to inappropriate strategy. % 222.14/31.56 % (384637)------------------------------ % 222.14/31.56 % (384637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384637)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384637)Termination reason: Inappropriate % 222.14/31.56 % (384637)Time elapsed: 0.009 s % 222.14/31.56 % (384637)Peak memory usage: 11 MB % 222.14/31.56 % (384637)Instructions burned: 11 (million) % 222.14/31.56 % (384637)------------------------------ % 222.14/31.56 % (384637)------------------------------ % 222.14/31.56 % (384639)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=183438598:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 222.14/31.56 % (384504)Instruction limit reached! % 222.14/31.56 % (384504)------------------------------ % 222.14/31.56 % (384504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384504)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384504)Termination reason: Instruction limit % 222.14/31.56 % (384504)Termination phase: Saturation % 222.14/31.56 % (384504)Time elapsed: 4.497 s % 222.14/31.56 % (384504)Peak memory usage: 41 MB % 222.14/31.56 % (384504)Instructions burned: 5115 (million) % 222.14/31.56 % (384645)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1503996388:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 222.14/31.56 % (384606)Instruction limit reached! % 222.14/31.56 % (384606)------------------------------ % 222.14/31.56 % (384606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.14/31.56 % (384606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.14/31.56 % (384606)CaDiCaL version: 2.1.3 % 222.14/31.56 % (384606)Termination reason: Instruction limit % 222.14/31.56 % (384606)Termination phase: Saturation % 223.49/31.71 % (384606)Time elapsed: 3.679 s % 223.49/31.71 % (384606)Peak memory usage: 37 MB % 223.49/31.71 % (384606)Instructions burned: 4591 (million) % 223.49/31.71 % (384681)dis+10_16:1_sil=16000:random_seed=910705157:i=9155:fsr=off_2920 on theBenchmark for (2920ds/9155Mi) % 223.49/31.71 % (384627)Instruction limit reached! % 223.49/31.71 % (384627)------------------------------ % 223.49/31.71 % (384627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384627)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384627)Termination reason: Instruction limit % 223.49/31.71 % (384627)Termination phase: Saturation % 223.49/31.71 % (384627)Time elapsed: 4.290 s % 223.49/31.71 % (384627)Peak memory usage: 45 MB % 223.49/31.71 % (384627)Instructions burned: 5211 (million) % 223.49/31.71 % (384694)ott-3_8_sil=64000:random_seed=3020780618:i=20139:bs=on_2906 on theBenchmark for (2906ds/20139Mi) % 223.49/31.71 % (384645)Instruction limit reached! % 223.49/31.71 % (384645)------------------------------ % 223.49/31.71 % (384645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384645)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384645)Termination reason: Instruction limit % 223.49/31.71 % (384645)Termination phase: Saturation % 223.49/31.71 % (384645)Time elapsed: 8.249 s % 223.49/31.71 % (384645)Peak memory usage: 75 MB % 223.49/31.71 % (384645)Instructions burned: 8174 (million) % 223.49/31.71 % (384712)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1612563916:fmbsr=2:i=32576_2860 on theBenchmark for (2860ds/32576Mi) % 223.49/31.71 % (384712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.49/31.71 % (384712)Terminated due to inappropriate strategy. % 223.49/31.71 % (384712)------------------------------ % 223.49/31.71 % (384712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384712)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384712)Termination reason: Inappropriate % 223.49/31.71 % (384712)Time elapsed: 0.007 s % 223.49/31.71 % (384712)Peak memory usage: 11 MB % 223.49/31.71 % (384712)Instructions burned: 13 (million) % 223.49/31.71 % (384712)------------------------------ % 223.49/31.71 % (384712)------------------------------ % 223.49/31.71 % (384714)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1096615946:i=11404_2860 on theBenchmark for (2860ds/11404Mi) % 223.49/31.71 % (384681)Instruction limit reached! % 223.49/31.71 % (384681)------------------------------ % 223.49/31.71 % (384681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384681)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384681)Termination reason: Instruction limit % 223.49/31.71 % (384681)Termination phase: Saturation % 223.49/31.71 % (384681)Time elapsed: 8.450 s % 223.49/31.71 % (384681)Peak memory usage: 52 MB % 223.49/31.71 % (384681)Instructions burned: 9157 (million) % 223.49/31.71 % (384729)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=468566908:i=14134_2835 on theBenchmark for (2835ds/14134Mi) % 223.49/31.71 % (384639)Instruction limit reached! % 223.49/31.71 % (384639)------------------------------ % 223.49/31.71 % (384639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384639)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384639)Termination reason: Instruction limit % 223.49/31.71 % (384639)Termination phase: Saturation % 223.49/31.71 % (384639)Time elapsed: 18.536 s % 223.49/31.71 % (384639)Peak memory usage: 80 MB % 223.49/31.71 % (384639)Instructions burned: 22566 (million) % 223.49/31.71 % (384738)dis+33_16_sil=32000:sac=on:random_seed=3165115215:i=15851:nm=0_2761 on theBenchmark for (2761ds/15851Mi) % 223.49/31.71 % (384714)Instruction limit reached! % 223.49/31.71 % (384714)------------------------------ % 223.49/31.71 % (384714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.49/31.71 % (384714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.49/31.71 % (384714)CaDiCaL version: 2.1.3 % 223.49/31.71 % (384714)Termination reason: Instruction limit % 223.49/31.71 % (384714)Termination phase: Saturation % 223.49/31.71 % (384714)Time elapsed: 11.490 s % 223.49/31.71 % (384714)Peak memory usage: 106 MB % 223.49/31.71 % (384714)Instructions burned: 11405 (million) % 223.49/31.71 % (384742)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2124642619:avsq=on:i=17627:add=on:amm=off_2745 on theBenchmark for (2745ds/17627Mi) % 300.46/42.54 % (384619)Instruction limit reached! % 300.46/42.54 % (384619)------------------------------ % 300.46/42.54 % (384619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384619)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384619)Termination reason: Instruction limit % 300.46/42.54 % (384619)Termination phase: Saturation % 300.46/42.54 % (384619)Time elapsed: 24.901 s % 300.46/42.54 % (384619)Peak memory usage: 164 MB % 300.46/42.54 % (384619)Instructions burned: 29341 (million) % 300.46/42.54 % (384754)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=240145097:s2a=on:i=53295_2703 on theBenchmark for (2703ds/53295Mi) % 300.46/42.54 % (384694)Instruction limit reached! % 300.46/42.54 % (384694)------------------------------ % 300.46/42.54 % (384694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384694)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384694)Termination reason: Instruction limit % 300.46/42.54 % (384694)Termination phase: Saturation % 300.46/42.54 % (384694)Time elapsed: 21.293 s % 300.46/42.54 % (384694)Peak memory usage: 127 MB % 300.46/42.54 % (384694)Instructions burned: 20139 (million) % 300.46/42.54 % (384759)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2301555318:i=26857:ins=20_2692 on theBenchmark for (2692ds/26857Mi) % 300.46/42.54 % (384759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.46/42.54 % (384759)Terminated due to inappropriate strategy. % 300.46/42.54 % (384759)------------------------------ % 300.46/42.54 % (384759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384759)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384759)Termination reason: Inappropriate % 300.46/42.54 % (384759)Time elapsed: 0.010 s % 300.46/42.54 % (384759)Peak memory usage: 11 MB % 300.46/42.54 % (384759)Instructions burned: 10 (million) % 300.46/42.54 % (384759)------------------------------ % 300.46/42.54 % (384759)------------------------------ % 300.46/42.54 % (384761)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3477233364:i=28120:bs=on:fsr=off_2692 on theBenchmark for (2692ds/28120Mi) % 300.46/42.54 % (384729)Instruction limit reached! % 300.46/42.54 % (384729)------------------------------ % 300.46/42.54 % (384729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384729)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384729)Termination reason: Instruction limit % 300.46/42.54 % (384729)Termination phase: Saturation % 300.46/42.54 % (384729)Time elapsed: 14.705 s % 300.46/42.54 % (384729)Peak memory usage: 89 MB % 300.46/42.54 % (384729)Instructions burned: 14134 (million) % 300.46/42.54 % (384765)fmb+10_1_sil=256000:fmbss=7:random_seed=3701093514:fmbsr=1.6:i=182295_2687 on theBenchmark for (2687ds/182295Mi) % 300.46/42.54 % (384765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.46/42.54 % (384765)Terminated due to inappropriate strategy. % 300.46/42.54 % (384765)------------------------------ % 300.46/42.54 % (384765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384765)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384765)Termination reason: Inappropriate % 300.46/42.54 % (384765)Time elapsed: 0.014 s % 300.46/42.54 % (384765)Peak memory usage: 11 MB % 300.46/42.54 % (384765)Instructions burned: 10 (million) % 300.46/42.54 % (384765)------------------------------ % 300.46/42.54 % (384765)------------------------------ % 300.46/42.54 % (384767)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=652976318:i=44625:gsp=on_2687 on theBenchmark for (2687ds/44625Mi) % 300.46/42.54 % (384767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.46/42.54 % (384767)Terminated due to inappropriate strategy. % 300.46/42.54 % (384767)------------------------------ % 300.46/42.54 % (384767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.54 % (384767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.54 % (384767)CaDiCaL version: 2.1.3 % 300.46/42.54 % (384767)Termination % 300.46/42.54 Terminated % 300.46/42.54 % Vampire exiting % 300.46/42.54 Terminated %------------------------------------------------------------------------------