%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW591_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:29 PM UTC 2026 % Result : Timeout 300.66s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW591_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n002.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:22:52 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 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.67/0.84 % (382232)Will run a generic schedule for satisfiability detection. % 3.67/0.84 % (382243)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2085047428:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.67/0.84 % (382238)% WARNING: option uhcvi not known. % 3.67/0.84 % (382238)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2367729601:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.67/0.84 % (382237)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3779684399_2999 on theBenchmark for (2999ds/0Mi) % 3.67/0.84 % (382240)dis+10_1_sil=32000:sp=arity:random_seed=2560080628:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.67/0.84 % (382241)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=499161329:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.67/0.84 % (382239)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3112383349:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.67/0.84 % (382242)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1544243995:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.67/0.84 % (382237)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/0.84 % (382237)Terminated due to inappropriate strategy. % 3.67/0.84 % (382237)------------------------------ % 3.67/0.84 % (382237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.84 % (382237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.84 % (382237)CaDiCaL version: 2.1.3 % 3.67/0.84 % (382237)Termination reason: Inappropriate % 3.67/0.84 % (382237)Time elapsed: 0.002 s % 3.67/0.84 % (382237)Peak memory usage: 11 MB % 3.67/0.84 % (382237)Instructions burned: 3 (million) % 3.67/0.84 % (382237)------------------------------ % 3.67/0.84 % (382237)------------------------------ % 3.67/0.84 % (382251)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1841576750:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.67/0.84 % (382251)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/0.84 % (382251)Terminated due to inappropriate strategy. % 3.67/0.84 % (382251)------------------------------ % 3.67/0.84 % (382251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.84 % (382251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.84 % (382251)CaDiCaL version: 2.1.3 % 3.67/0.84 % (382251)Termination reason: Inappropriate % 3.67/0.84 % (382251)Time elapsed: 0.001 s % 3.67/0.84 % (382251)Peak memory usage: 10 MB % 3.67/0.84 % (382251)Instructions burned: 2 (million) % 3.67/0.84 % (382251)------------------------------ % 3.67/0.84 % (382251)------------------------------ % 3.67/0.84 % (382253)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=942604423:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.67/0.84 % (382243)Instruction limit reached! % 3.67/0.84 % (382243)------------------------------ % 3.67/0.84 % (382243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.84 % (382243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.84 % (382243)CaDiCaL version: 2.1.3 % 3.67/0.84 % (382243)Termination reason: Instruction limit % 3.67/0.84 % (382243)Termination phase: Saturation % 3.67/0.84 % (382243)Time elapsed: 0.064 s % 3.67/0.84 % (382243)Peak memory usage: 14 MB % 3.67/0.84 % (382243)Instructions burned: 162 (million) % 3.67/0.84 % (382240)Instruction limit reached! % 3.67/0.84 % (382240)------------------------------ % 3.67/0.84 % (382240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.84 % (382240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.84 % (382240)CaDiCaL version: 2.1.3 % 3.67/0.84 % (382240)Termination reason: Instruction limit % 3.67/0.84 % (382240)Termination phase: Saturation % 3.67/0.84 % (382240)Time elapsed: 0.067 s % 3.67/0.84 % (382240)Peak memory usage: 13 MB % 3.67/0.84 % (382240)Instructions burned: 104 (million) % 3.67/0.84 % (382255)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=108289091:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.67/0.84 % (382241)Instruction limit reached! % 3.67/0.84 % (382241)------------------------------ % 3.67/0.84 % (382241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382241)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382241)Termination reason: Instruction limit % 8.00/1.44 % (382241)Termination phase: Saturation % 8.00/1.44 % (382241)Time elapsed: 0.076 s % 8.00/1.44 % (382241)Peak memory usage: 13 MB % 8.00/1.44 % (382241)Instructions burned: 116 (million) % 8.00/1.44 % (382242)Instruction limit reached! % 8.00/1.44 % (382242)------------------------------ % 8.00/1.44 % (382242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382242)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382242)Termination reason: Instruction limit % 8.00/1.44 % (382242)Termination phase: Saturation % 8.00/1.44 % (382242)Time elapsed: 0.084 s % 8.00/1.44 % (382242)Peak memory usage: 13 MB % 8.00/1.44 % (382242)Instructions burned: 132 (million) % 8.00/1.44 % (382256)ott-21_1_sil=16000:fs=off:random_seed=839037014:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.00/1.44 % (382258)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1921192236:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.00/1.44 % (382259)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=792193353:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.00/1.44 % (382259)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.00/1.44 % (382259)Terminated due to inappropriate strategy. % 8.00/1.44 % (382259)------------------------------ % 8.00/1.44 % (382259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382259)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382259)Termination reason: Inappropriate % 8.00/1.44 % (382259)Time elapsed: 0.001 s % 8.00/1.44 % (382259)Peak memory usage: 10 MB % 8.00/1.44 % (382259)Instructions burned: 2 (million) % 8.00/1.44 % (382259)------------------------------ % 8.00/1.44 % (382259)------------------------------ % 8.00/1.44 % (382263)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4269496280:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.00/1.44 % (382253)Instruction limit reached! % 8.00/1.44 % (382253)------------------------------ % 8.00/1.44 % (382253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382253)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382253)Termination reason: Instruction limit % 8.00/1.44 % (382253)Termination phase: Saturation % 8.00/1.44 % (382253)Time elapsed: 0.091 s % 8.00/1.44 % (382253)Peak memory usage: 13 MB % 8.00/1.44 % (382253)Instructions burned: 131 (million) % 8.00/1.44 % (382265)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3041680487:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.00/1.44 % (382265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.00/1.44 % (382265)Terminated due to inappropriate strategy. % 8.00/1.44 % (382265)------------------------------ % 8.00/1.44 % (382265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382265)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382265)Termination reason: Inappropriate % 8.00/1.44 % (382265)Time elapsed: 0.001 s % 8.00/1.44 % (382265)Peak memory usage: 10 MB % 8.00/1.44 % (382265)Instructions burned: 2 (million) % 8.00/1.44 % (382265)------------------------------ % 8.00/1.44 % (382265)------------------------------ % 8.00/1.44 % (382256)Instruction limit reached! % 8.00/1.44 % (382256)------------------------------ % 8.00/1.44 % (382256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.00/1.44 % (382256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.00/1.44 % (382256)CaDiCaL version: 2.1.3 % 8.00/1.44 % (382256)Termination reason: Instruction limit % 8.00/1.44 % (382256)Termination phase: Saturation % 8.00/1.44 % (382256)Time elapsed: 0.086 s % 8.00/1.44 % (382256)Peak memory usage: 13 MB % 8.00/1.44 % (382256)Instructions burned: 180 (million) % 8.00/1.44 % (382267)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=1156655324: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) % 22.09/3.44 % (382268)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2945350475:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.09/3.44 % (382255)Instruction limit reached! % 22.09/3.44 % (382255)------------------------------ % 22.09/3.44 % (382255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.44 % (382255)CaDiCaL version: 2.1.3 % 22.09/3.44 % (382255)Termination reason: Instruction limit % 22.09/3.44 % (382255)Termination phase: Saturation % 22.09/3.44 % (382255)Time elapsed: 0.198 s % 22.09/3.44 % (382255)Peak memory usage: 17 MB % 22.09/3.44 % (382255)Instructions burned: 687 (million) % 22.09/3.44 % (382271)fmb+10_1_sil=64000:random_seed=3379637688:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 22.09/3.44 % (382271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.44 % (382271)Terminated due to inappropriate strategy. % 22.09/3.44 % (382271)------------------------------ % 22.09/3.44 % (382271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.44 % (382271)CaDiCaL version: 2.1.3 % 22.09/3.44 % (382271)Termination reason: Inappropriate % 22.09/3.44 % (382271)Time elapsed: 0.001 s % 22.09/3.44 % (382271)Peak memory usage: 11 MB % 22.09/3.44 % (382271)Instructions burned: 2 (million) % 22.09/3.44 % (382271)------------------------------ % 22.09/3.44 % (382271)------------------------------ % 22.09/3.44 % (382273)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2039979228:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 22.09/3.44 % (382273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.44 % (382273)Terminated due to inappropriate strategy. % 22.09/3.44 % (382273)------------------------------ % 22.09/3.44 % (382273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.44 % (382273)CaDiCaL version: 2.1.3 % 22.09/3.44 % (382273)Termination reason: Inappropriate % 22.09/3.44 % (382273)Time elapsed: 0.001 s % 22.09/3.44 % (382273)Peak memory usage: 11 MB % 22.09/3.44 % (382273)Instructions burned: 2 (million) % 22.09/3.44 % (382273)------------------------------ % 22.09/3.44 % (382273)------------------------------ % 22.09/3.44 % (382275)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=26284280:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 22.09/3.44 % (382275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.09/3.44 % (382275)Terminated due to inappropriate strategy. % 22.09/3.44 % (382275)------------------------------ % 22.09/3.44 % (382275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.44 % (382275)CaDiCaL version: 2.1.3 % 22.09/3.44 % (382275)Termination reason: Inappropriate % 22.09/3.44 % (382275)Time elapsed: 0.001 s % 22.09/3.44 % (382275)Peak memory usage: 11 MB % 22.09/3.44 % (382275)Instructions burned: 2 (million) % 22.09/3.44 % (382275)------------------------------ % 22.09/3.44 % (382275)------------------------------ % 22.09/3.44 % (382277)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=786752517:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 22.09/3.44 % (382258)Instruction limit reached! % 22.09/3.44 % (382258)------------------------------ % 22.09/3.44 % (382258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.09/3.44 % (382258)CaDiCaL version: 2.1.3 % 22.09/3.44 % (382258)Termination reason: Instruction limit % 22.09/3.44 % (382258)Termination phase: Saturation % 22.09/3.44 % (382258)Time elapsed: 0.315 s % 22.09/3.44 % (382258)Peak memory usage: 14 MB % 22.09/3.44 % (382258)Instructions burned: 478 (million) % 22.09/3.44 % (382279)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4261686862:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.09/3.44 % (382267)Instruction limit reached! % 22.09/3.44 % (382267)------------------------------ % 22.09/3.44 % (382267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.09/3.44 % (382267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.29 % (382267)CaDiCaL version: 2.1.3 % 28.12/4.29 % (382267)Termination reason: Instruction limit % 28.12/4.29 % (382267)Termination phase: Saturation % 28.12/4.29 % (382267)Time elapsed: 0.398 s % 28.12/4.29 % (382267)Peak memory usage: 17 MB % 28.12/4.29 % (382267)Instructions burned: 692 (million) % 28.12/4.29 % (382281)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1348987032:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.12/4.29 % (382281)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.12/4.29 % (382281)Terminated due to inappropriate strategy. % 28.12/4.29 % (382281)------------------------------ % 28.12/4.29 % (382281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.12/4.29 % (382281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.29 % (382281)CaDiCaL version: 2.1.3 % 28.12/4.29 % (382281)Termination reason: Inappropriate % 28.12/4.29 % (382281)Time elapsed: 0.002 s % 28.12/4.29 % (382281)Peak memory usage: 11 MB % 28.12/4.29 % (382281)Instructions burned: 2 (million) % 28.12/4.29 % (382281)------------------------------ % 28.12/4.29 % (382281)------------------------------ % 28.12/4.29 % (382283)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=353818795:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.12/4.29 % (382283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.12/4.29 % (382283)Terminated due to inappropriate strategy. % 28.12/4.29 % (382283)------------------------------ % 28.12/4.29 % (382283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.12/4.29 % (382283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.29 % (382283)CaDiCaL version: 2.1.3 % 28.12/4.29 % (382283)Termination reason: Inappropriate % 28.12/4.29 % (382283)Time elapsed: 0.001 s % 28.12/4.29 % (382283)Peak memory usage: 10 MB % 28.12/4.29 % (382283)Instructions burned: 2 (million) % 28.12/4.29 % (382283)------------------------------ % 28.12/4.29 % (382283)------------------------------ % 28.12/4.29 % (382285)ott-2_1_sil=16000:newcnf=on:random_seed=3170063885:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.12/4.29 % (382268)Instruction limit reached! % 28.12/4.29 % (382268)------------------------------ % 28.12/4.29 % (382268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.12/4.29 % (382268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.29 % (382268)CaDiCaL version: 2.1.3 % 28.12/4.29 % (382268)Termination reason: Instruction limit % 28.12/4.29 % (382268)Termination phase: Saturation % 28.12/4.29 % (382268)Time elapsed: 0.511 s % 28.12/4.29 % (382268)Peak memory usage: 19 MB % 28.12/4.29 % (382268)Instructions burned: 879 (million) % 28.12/4.29 % (382287)ott+10_1_sil=32000:tgt=ground:random_seed=1371790182:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.12/4.29 % (382263)Instruction limit reached! % 28.12/4.29 % (382263)------------------------------ % 28.12/4.29 % (382263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.12/4.29 % (382263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.29 % (382263)CaDiCaL version: 2.1.3 % 28.12/4.29 % (382263)Termination reason: Instruction limit % 28.12/4.29 % (382263)Termination phase: Saturation % 28.12/4.29 % (382263)Time elapsed: 0.707 s % 28.12/4.29 % (382263)Peak memory usage: 20 MB % 28.12/4.30 % (382263)Instructions burned: 1179 (million) % 28.12/4.30 % (382289)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2993717837:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.12/4.30 % (382289)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.12/4.30 % (382289)Terminated due to inappropriate strategy. % 28.12/4.30 % (382289)------------------------------ % 28.12/4.30 % (382289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.12/4.30 % (382289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.12/4.30 % (382289)CaDiCaL version: 2.1.3 % 28.12/4.30 % (382289)Termination reason: Inappropriate % 28.12/4.30 % (382289)Time elapsed: 0.002 s % 28.12/4.30 % (382289)Peak memory usage: 11 MB % 28.12/4.30 % (382289)Instructions burned: 3 (million) % 28.12/4.30 % (382289)------------------------------ % 28.12/4.30 % (382289)------------------------------ % 28.12/4.30 % (382291)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=750657412:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 28.12/4.30 % (382285)Instruction limit reached! % 87.04/12.51 % (382285)------------------------------ % 87.04/12.51 % (382285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382285)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382285)Termination reason: Instruction limit % 87.04/12.51 % (382285)Termination phase: Saturation % 87.04/12.51 % (382285)Time elapsed: 0.528 s % 87.04/12.51 % (382285)Peak memory usage: 16 MB % 87.04/12.51 % (382285)Instructions burned: 869 (million) % 87.04/12.51 % (382279)Instruction limit reached! % 87.04/12.51 % (382279)------------------------------ % 87.04/12.51 % (382279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382279)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382279)Termination reason: Instruction limit % 87.04/12.51 % (382279)Termination phase: Saturation % 87.04/12.51 % (382279)Time elapsed: 0.740 s % 87.04/12.51 % (382279)Peak memory usage: 24 MB % 87.04/12.51 % (382279)Instructions burned: 1473 (million) % 87.04/12.51 % (382293)dis+21_1_sil=32000:sas=cadical:random_seed=2633521921:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 87.04/12.51 % (382294)ott+11_1_sil=16000:gs=on:random_seed=1447135358:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 87.04/12.51 % (382277)Instruction limit reached! % 87.04/12.51 % (382277)------------------------------ % 87.04/12.51 % (382277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382277)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382277)Termination reason: Instruction limit % 87.04/12.51 % (382277)Termination phase: Saturation % 87.04/12.51 % (382277)Time elapsed: 1.509 s % 87.04/12.51 % (382277)Peak memory usage: 41 MB % 87.04/12.51 % (382277)Instructions burned: 5135 (million) % 87.04/12.51 % (382297)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=524185870:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 87.04/12.51 % (382297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.04/12.51 % (382297)Terminated due to inappropriate strategy. % 87.04/12.51 % (382297)------------------------------ % 87.04/12.51 % (382297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382297)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382297)Termination reason: Inappropriate % 87.04/12.51 % (382297)Time elapsed: 0.001 s % 87.04/12.51 % (382297)Peak memory usage: 10 MB % 87.04/12.51 % (382297)Instructions burned: 2 (million) % 87.04/12.51 % (382297)------------------------------ % 87.04/12.51 % (382297)------------------------------ % 87.04/12.51 % (382299)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=544871412:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 87.04/12.51 % (382294)Instruction limit reached! % 87.04/12.51 % (382294)------------------------------ % 87.04/12.51 % (382294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382294)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382294)Termination reason: Instruction limit % 87.04/12.51 % (382294)Termination phase: Saturation % 87.04/12.51 % (382294)Time elapsed: 1.284 s % 87.04/12.51 % (382294)Peak memory usage: 22 MB % 87.04/12.51 % (382294)Instructions burned: 2252 (million) % 87.04/12.51 % (382301)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=944115947:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 87.04/12.51 % (382291)Instruction limit reached! % 87.04/12.51 % (382291)------------------------------ % 87.04/12.51 % (382291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.04/12.51 % (382291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.04/12.51 % (382291)CaDiCaL version: 2.1.3 % 87.04/12.51 % (382291)Termination reason: Instruction limit % 87.04/12.51 % (382291)Termination phase: Saturation % 87.04/12.51 % (382291)Time elapsed: 1.879 s % 87.04/12.51 % (382291)Peak memory usage: 37 MB % 87.04/12.51 % (382291)Instructions burned: 3513 (million) % 87.04/12.51 % (382303)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3644271941:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 87.04/12.51 % (382299)Instruction limit reached! % 117.37/16.91 % (382299)------------------------------ % 117.37/16.91 % (382299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382299)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382299)Termination reason: Instruction limit % 117.37/16.91 % (382299)Termination phase: Saturation % 117.37/16.91 % (382299)Time elapsed: 1.322 s % 117.37/16.91 % (382299)Peak memory usage: 49 MB % 117.37/16.91 % (382299)Instructions burned: 4594 (million) % 117.37/16.91 % (382305)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4174438599:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 117.37/16.91 % (382305)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.37/16.91 % (382305)Terminated due to inappropriate strategy. % 117.37/16.91 % (382305)------------------------------ % 117.37/16.91 % (382305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382305)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382305)Termination reason: Inappropriate % 117.37/16.91 % (382305)Time elapsed: 0.001 s % 117.37/16.91 % (382305)Peak memory usage: 11 MB % 117.37/16.91 % (382305)Instructions burned: 2 (million) % 117.37/16.91 % (382305)------------------------------ % 117.37/16.91 % (382305)------------------------------ % 117.37/16.91 % (382307)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3539912312:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 117.37/16.91 % (382307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.37/16.91 % (382307)Terminated due to inappropriate strategy. % 117.37/16.91 % (382307)------------------------------ % 117.37/16.91 % (382307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382307)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382307)Termination reason: Inappropriate % 117.37/16.91 % (382307)Time elapsed: 0.001 s % 117.37/16.91 % (382307)Peak memory usage: 10 MB % 117.37/16.91 % (382307)Instructions burned: 2 (million) % 117.37/16.91 % (382307)------------------------------ % 117.37/16.91 % (382307)------------------------------ % 117.37/16.91 % (382309)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=200811372:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 117.37/16.91 % (382309)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.37/16.91 % (382309)Terminated due to inappropriate strategy. % 117.37/16.91 % (382309)------------------------------ % 117.37/16.91 % (382309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382309)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382309)Termination reason: Inappropriate % 117.37/16.91 % (382309)Time elapsed: 0.001 s % 117.37/16.91 % (382309)Peak memory usage: 10 MB % 117.37/16.91 % (382309)Instructions burned: 2 (million) % 117.37/16.91 % (382309)------------------------------ % 117.37/16.91 % (382309)------------------------------ % 117.37/16.91 % (382311)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3205495826:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 117.37/16.91 % (382293)Instruction limit reached! % 117.37/16.91 % (382293)------------------------------ % 117.37/16.91 % (382293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382293)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382293)Termination reason: Instruction limit % 117.37/16.91 % (382293)Termination phase: Saturation % 117.37/16.91 % (382293)Time elapsed: 2.061 s % 117.37/16.91 % (382293)Peak memory usage: 32 MB % 117.37/16.91 % (382293)Instructions burned: 3774 (million) % 117.37/16.91 % (382313)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4139225155:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 117.37/16.91 % (382287)Instruction limit reached! % 117.37/16.91 % (382287)------------------------------ % 117.37/16.91 % (382287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.37/16.91 % (382287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.37/16.91 % (382287)CaDiCaL version: 2.1.3 % 117.37/16.91 % (382287)Termination reason: Instruction limit % 117.37/16.91 % (382287)Termination phase: Saturation % 117.37/16.91 % (382287)Time elapsed: 3.302 s % 110.02/17.42 % (382287)Peak memory usage: 33 MB % 110.02/17.42 % (382287)Instructions burned: 5115 (million) % 110.02/17.42 % (382315)dis+10_16:1_sil=16000:random_seed=1343831114:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 110.02/17.42 % (382303)Instruction limit reached! % 110.02/17.42 % (382303)------------------------------ % 110.02/17.42 % (382303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382303)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382303)Termination reason: Instruction limit % 110.02/17.42 % (382303)Termination phase: Saturation % 110.02/17.42 % (382303)Time elapsed: 2.682 s % 110.02/17.42 % (382303)Peak memory usage: 43 MB % 110.02/17.42 % (382303)Instructions burned: 5211 (million) % 110.02/17.42 % (382317)ott-3_8_sil=64000:random_seed=1205224831:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 110.02/17.42 % (382311)Instruction limit reached! % 110.02/17.42 % (382311)------------------------------ % 110.02/17.42 % (382311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382311)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382311)Termination reason: Instruction limit % 110.02/17.42 % (382311)Termination phase: Saturation % 110.02/17.42 % (382311)Time elapsed: 5.086 s % 110.02/17.42 % (382311)Peak memory usage: 65 MB % 110.02/17.42 % (382311)Instructions burned: 22569 (million) % 110.02/17.42 % (382319)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3886996153:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 110.02/17.42 % (382319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.02/17.42 % (382319)Terminated due to inappropriate strategy. % 110.02/17.42 % (382319)------------------------------ % 110.02/17.42 % (382319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382319)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382319)Termination reason: Inappropriate % 110.02/17.42 % (382319)Time elapsed: 0.001 s % 110.02/17.42 % (382319)Peak memory usage: 11 MB % 110.02/17.42 % (382319)Instructions burned: 3 (million) % 110.02/17.42 % (382319)------------------------------ % 110.02/17.42 % (382319)------------------------------ % 110.02/17.42 % (382321)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2317755883:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 110.02/17.42 % (382313)Instruction limit reached! % 110.02/17.42 % (382313)------------------------------ % 110.02/17.42 % (382313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382313)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382313)Termination reason: Instruction limit % 110.02/17.42 % (382313)Termination phase: Saturation % 110.02/17.42 % (382313)Time elapsed: 5.224 s % 110.02/17.42 % (382313)Peak memory usage: 59 MB % 110.02/17.42 % (382313)Instructions burned: 8173 (million) % 110.02/17.42 % (382323)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4250502888:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 110.02/17.42 % (382315)Instruction limit reached! % 110.02/17.42 % (382315)------------------------------ % 110.02/17.42 % (382315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382315)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382315)Termination reason: Instruction limit % 110.02/17.42 % (382315)Termination phase: Saturation % 110.02/17.42 % (382315)Time elapsed: 4.661 s % 110.02/17.42 % (382315)Peak memory usage: 52 MB % 110.02/17.42 % (382315)Instructions burned: 9155 (million) % 110.02/17.42 % (382325)dis+33_16_sil=32000:sac=on:random_seed=697023407:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi) % 110.02/17.42 % (382321)Instruction limit reached! % 110.02/17.42 % (382321)------------------------------ % 110.02/17.42 % (382321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.02/17.42 % (382321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.02/17.42 % (382321)CaDiCaL version: 2.1.3 % 110.02/17.42 % (382321)Termination reason: Instruction limit % 110.02/17.42 % (382321)Termination phase: Saturation % 110.02/17.42 % (382321)Time elapsed: 3.897 s % 110.02/17.42 % (382321)Peak memory usage: 62 MB % 110.02/17.42 % (382321)Instructions burned: 11408 (million) % 110.02/17.42 % (382327)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=310131798:avsq=on:i=17627:add=on:amm=off_2877 on theBenchmark for (2877ds/17627Mi) % 129.62/18.50 % (382301)Instruction limit reached! % 129.62/18.50 % (382301)------------------------------ % 129.62/18.50 % (382301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382301)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382301)Termination reason: Instruction limit % 129.62/18.50 % (382301)Termination phase: Saturation % 129.62/18.50 % (382301)Time elapsed: 12.528 s % 129.62/18.50 % (382301)Peak memory usage: 118 MB % 129.62/18.50 % (382301)Instructions burned: 29342 (million) % 129.62/18.50 % (382391)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3939469867:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 129.62/18.50 % (382325)Instruction limit reached! % 129.62/18.50 % (382325)------------------------------ % 129.62/18.50 % (382325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382325)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382325)Termination reason: Instruction limit % 129.62/18.50 % (382325)Termination phase: Saturation % 129.62/18.50 % (382325)Time elapsed: 6.967 s % 129.62/18.50 % (382325)Peak memory usage: 208 MB % 129.62/18.50 % (382325)Instructions burned: 15853 (million) % 129.62/18.50 % (382393)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=407356915:i=26857:ins=20_2842 on theBenchmark for (2842ds/26857Mi) % 129.62/18.50 % (382393)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.62/18.50 % (382393)Terminated due to inappropriate strategy. % 129.62/18.50 % (382393)------------------------------ % 129.62/18.50 % (382393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382393)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382393)Termination reason: Inappropriate % 129.62/18.50 % (382393)Time elapsed: 0.002 s % 129.62/18.50 % (382393)Peak memory usage: 10 MB % 129.62/18.50 % (382393)Instructions burned: 2 (million) % 129.62/18.50 % (382393)------------------------------ % 129.62/18.50 % (382393)------------------------------ % 129.62/18.50 % (382395)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1679553755:i=28120:bs=on:fsr=off_2842 on theBenchmark for (2842ds/28120Mi) % 129.62/18.50 % (382327)Instruction limit reached! % 129.62/18.50 % (382327)------------------------------ % 129.62/18.50 % (382327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382327)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382327)Termination reason: Instruction limit % 129.62/18.50 % (382327)Termination phase: Saturation % 129.62/18.50 % (382327)Time elapsed: 4.352 s % 129.62/18.50 % (382327)Peak memory usage: 233 MB % 129.62/18.50 % (382327)Instructions burned: 17627 (million) % 129.62/18.50 % (382397)fmb+10_1_sil=256000:fmbss=7:random_seed=1796523428:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 129.62/18.50 % (382397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.62/18.50 % (382397)Terminated due to inappropriate strategy. % 129.62/18.50 % (382397)------------------------------ % 129.62/18.50 % (382397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382397)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382397)Termination reason: Inappropriate % 129.62/18.50 % (382397)Time elapsed: 0.001 s % 129.62/18.50 % (382397)Peak memory usage: 10 MB % 129.62/18.50 % (382397)Instructions burned: 2 (million) % 129.62/18.50 % (382397)------------------------------ % 129.62/18.50 % (382397)------------------------------ % 129.62/18.50 % (382399)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=964680803:i=44625:gsp=on_2833 on theBenchmark for (2833ds/44625Mi) % 129.62/18.50 % (382399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.62/18.50 % (382399)Terminated due to inappropriate strategy. % 129.62/18.50 % (382399)------------------------------ % 129.62/18.50 % (382399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.50 % (382399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.50 % (382399)CaDiCaL version: 2.1.3 % 129.62/18.50 % (382399)Termination reason: Inappropriate % 129.62/18.50 % (382399)Time elapsed: 0.001 s % 150.89/21.59 % (382399)Peak memory usage: 10 MB % 150.89/21.59 % (382399)Instructions burned: 2 (million) % 150.89/21.59 % (382399)------------------------------ % 150.89/21.59 % (382399)------------------------------ % 150.89/21.59 % (382401)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2327760430:i=160505_2833 on theBenchmark for (2833ds/160505Mi) % 150.89/21.59 % (382401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.89/21.59 % (382401)Terminated due to inappropriate strategy. % 150.89/21.59 % (382401)------------------------------ % 150.89/21.59 % (382401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.89/21.59 % (382401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.89/21.59 % (382401)CaDiCaL version: 2.1.3 % 150.89/21.59 % (382401)Termination reason: Inappropriate % 150.89/21.59 % (382401)Time elapsed: 0.001 s % 150.89/21.59 % (382401)Peak memory usage: 10 MB % 150.89/21.59 % (382401)Instructions burned: 2 (million) % 150.89/21.59 % (382401)------------------------------ % 150.89/21.59 % (382401)------------------------------ % 150.89/21.59 % (382403)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=899626690:fmbsr=1.3:i=225729_2833 on theBenchmark for (2833ds/225729Mi) % 150.89/21.59 % (382403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.89/21.59 % (382403)Terminated due to inappropriate strategy. % 150.89/21.59 % (382403)------------------------------ % 150.89/21.59 % (382403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.89/21.59 % (382403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.89/21.59 % (382403)CaDiCaL version: 2.1.3 % 150.89/21.59 % (382403)Termination reason: Inappropriate % 150.89/21.59 % (382403)Time elapsed: 0.001 s % 150.89/21.59 % (382403)Peak memory usage: 10 MB % 150.89/21.59 % (382403)Instructions burned: 2 (million) % 150.89/21.59 % (382403)------------------------------ % 150.89/21.59 % (382403)------------------------------ % 150.89/21.59 % (382405)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4109965324:fmbsr=2:i=185024:ins=7_2833 on theBenchmark for (2833ds/185024Mi) % 150.89/21.59 % (382405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.89/21.59 % (382405)Terminated due to inappropriate strategy. % 150.89/21.59 % (382405)------------------------------ % 150.89/21.59 % (382405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.89/21.59 % (382405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.89/21.59 % (382405)CaDiCaL version: 2.1.3 % 150.89/21.59 % (382405)Termination reason: Inappropriate % 150.89/21.59 % (382405)Time elapsed: 0.001 s % 150.89/21.59 % (382405)Peak memory usage: 10 MB % 150.89/21.59 % (382405)Instructions burned: 2 (million) % 150.89/21.59 % (382405)------------------------------ % 150.89/21.59 % (382405)------------------------------ % 150.89/21.59 % (382407)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=360740909:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 150.89/21.59 % (382407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.89/21.59 % (382407)Terminated due to inappropriate strategy. % 150.89/21.59 % (382407)------------------------------ % 150.89/21.59 % (382407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.89/21.59 % (382407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.89/21.59 % (382407)CaDiCaL version: 2.1.3 % 150.89/21.59 % (382407)Termination reason: Inappropriate % 150.89/21.59 % (382407)Time elapsed: 0.001 s % 150.89/21.59 % (382407)Peak memory usage: 11 MB % 150.89/21.59 % (382407)Instructions burned: 3 (million) % 150.89/21.59 % (382407)------------------------------ % 150.89/21.59 % (382407)------------------------------ % 150.89/21.59 % (382409)% WARNING: option uhcvi not known. % 150.89/21.59 % (382409)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1161560771:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 150.89/21.59 % (382317)Instruction limit reached! % 150.89/21.59 % (382317)------------------------------ % 150.89/21.59 % (382317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.89/21.59 % (382317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.89/21.59 % (382317)CaDiCaL version: 2.1.3 % 150.89/21.59 % (382317)Termination reason: Instruction limit % 150.89/21.59 % (382317)Termination phase: Saturation % 150.89/21.59 % (382317)Time elapsed: 11.642 s % 150.89/21.59 % (382317)Peak memory usage: 67 MB % 150.89/21.59 % (382317)Instructions burned: 20140 (million) % 150.89/21.59 % (382411)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2024117500:i=176048:add=on:rtra=on:rawr=on_2828 on theBenchmark for (2828ds/176048Mi) % 164.39/23.46 % (382323)Instruction limit reached! % 164.39/23.46 % (382323)------------------------------ % 164.39/23.46 % (382323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382323)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382323)Termination reason: Instruction limit % 164.39/23.46 % (382323)Termination phase: Saturation % 164.39/23.46 % (382323)Time elapsed: 8.929 s % 164.39/23.46 % (382323)Peak memory usage: 71 MB % 164.39/23.46 % (382323)Instructions burned: 14134 (million) % 164.39/23.46 % (382413)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1451420476:i=206:fgj=on:rtra=on_2825 on theBenchmark for (2825ds/206Mi) % 164.39/23.46 % (382413)Instruction limit reached! % 164.39/23.46 % (382413)------------------------------ % 164.39/23.46 % (382413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382413)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382413)Termination reason: Instruction limit % 164.39/23.46 % (382413)Termination phase: Saturation % 164.39/23.46 % (382413)Time elapsed: 0.133 s % 164.39/23.46 % (382413)Peak memory usage: 13 MB % 164.39/23.46 % (382413)Instructions burned: 207 (million) % 164.39/23.46 % (382415)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2194251883:i=232:rtra=on_2823 on theBenchmark for (2823ds/232Mi) % 164.39/23.46 % (382415)Instruction limit reached! % 164.39/23.46 % (382415)------------------------------ % 164.39/23.46 % (382415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382415)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382415)Termination reason: Instruction limit % 164.39/23.46 % (382415)Termination phase: Saturation % 164.39/23.46 % (382415)Time elapsed: 0.149 s % 164.39/23.46 % (382415)Peak memory usage: 14 MB % 164.39/23.46 % (382415)Instructions burned: 233 (million) % 164.39/23.46 % (382417)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1929128928:i=262:rtra=on_2821 on theBenchmark for (2821ds/262Mi) % 164.39/23.46 % (382417)Instruction limit reached! % 164.39/23.46 % (382417)------------------------------ % 164.39/23.46 % (382417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382417)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382417)Termination reason: Instruction limit % 164.39/23.46 % (382417)Termination phase: Saturation % 164.39/23.46 % (382417)Time elapsed: 0.170 s % 164.39/23.46 % (382417)Peak memory usage: 14 MB % 164.39/23.46 % (382417)Instructions burned: 262 (million) % 164.39/23.46 % (382419)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1324079250:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2819 on theBenchmark for (2819ds/318Mi) % 164.39/23.46 % (382419)Instruction limit reached! % 164.39/23.46 % (382419)------------------------------ % 164.39/23.46 % (382419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382419)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382419)Termination reason: Instruction limit % 164.39/23.46 % (382419)Termination phase: Saturation % 164.39/23.46 % (382419)Time elapsed: 0.218 s % 164.39/23.46 % (382419)Peak memory usage: 15 MB % 164.39/23.46 % (382419)Instructions burned: 318 (million) % 164.39/23.46 % (382421)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1653319238:i=1428:nm=2:rtra=on_2817 on theBenchmark for (2817ds/1428Mi) % 164.39/23.46 % (382421)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.39/23.46 % (382421)Terminated due to inappropriate strategy. % 164.39/23.46 % (382421)------------------------------ % 164.39/23.46 % (382421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.39/23.46 % (382421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.39/23.46 % (382421)CaDiCaL version: 2.1.3 % 164.39/23.46 % (382421)Termination reason: Inappropriate % 164.39/23.46 % (382421)Time elapsed: 0.002 s % 164.39/23.46 % (382421)Peak memory usage: 10 MB % 164.39/23.46 % (382421)Instructions burned: 3 (million) % 164.39/23.46 % (382421)------------------------------ % 164.39/23.46 % (382421)------------------------------ % 208.88/29.76 % (382423)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1666810080:i=262:bd=preordered:rtra=on:fsd=on_2817 on theBenchmark for (2817ds/262Mi) % 208.88/29.76 % (382423)Instruction limit reached! % 208.88/29.76 % (382423)------------------------------ % 208.88/29.76 % (382423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382423)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382423)Termination reason: Instruction limit % 208.88/29.76 % (382423)Termination phase: Saturation % 208.88/29.76 % (382423)Time elapsed: 0.182 s % 208.88/29.76 % (382423)Peak memory usage: 14 MB % 208.88/29.76 % (382423)Instructions burned: 262 (million) % 208.88/29.76 % (382425)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=4097014938:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/1368Mi) % 208.88/29.76 % (382425)Instruction limit reached! % 208.88/29.76 % (382425)------------------------------ % 208.88/29.76 % (382425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382425)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382425)Termination reason: Instruction limit % 208.88/29.76 % (382425)Termination phase: Saturation % 208.88/29.76 % (382425)Time elapsed: 0.752 s % 208.88/29.76 % (382425)Peak memory usage: 22 MB % 208.88/29.76 % (382425)Instructions burned: 1369 (million) % 208.88/29.76 % (382427)ott-21_1_sil=16000:si=on:fs=off:random_seed=3600765597:i=360:av=off:fsr=off:rtra=on_2807 on theBenchmark for (2807ds/360Mi) % 208.88/29.76 % (382427)Instruction limit reached! % 208.88/29.76 % (382427)------------------------------ % 208.88/29.76 % (382427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382427)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382427)Termination reason: Instruction limit % 208.88/29.76 % (382427)Termination phase: Saturation % 208.88/29.76 % (382427)Time elapsed: 0.167 s % 208.88/29.76 % (382427)Peak memory usage: 13 MB % 208.88/29.76 % (382427)Instructions burned: 362 (million) % 208.88/29.76 % (382429)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=996958865:i=954:bd=all:rtra=on_2805 on theBenchmark for (2805ds/954Mi) % 208.88/29.76 % (382429)Instruction limit reached! % 208.88/29.76 % (382429)------------------------------ % 208.88/29.76 % (382429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382429)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382429)Termination reason: Instruction limit % 208.88/29.76 % (382429)Termination phase: Saturation % 208.88/29.76 % (382429)Time elapsed: 0.594 s % 208.88/29.76 % (382429)Peak memory usage: 16 MB % 208.88/29.76 % (382429)Instructions burned: 956 (million) % 208.88/29.76 % (382431)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2360902804:fmbsr=1.3:i=1730:ins=25:rtra=on_2799 on theBenchmark for (2799ds/1730Mi) % 208.88/29.76 % (382431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.88/29.76 % (382431)Terminated due to inappropriate strategy. % 208.88/29.76 % (382431)------------------------------ % 208.88/29.76 % (382431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382431)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382431)Termination reason: Inappropriate % 208.88/29.76 % (382431)Time elapsed: 0.001 s % 208.88/29.76 % (382431)Peak memory usage: 10 MB % 208.88/29.76 % (382431)Instructions burned: 2 (million) % 208.88/29.76 % (382431)------------------------------ % 208.88/29.76 % (382431)------------------------------ % 208.88/29.76 % (382433)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1337479428:i=2358:rtra=on_2799 on theBenchmark for (2799ds/2358Mi) % 208.88/29.76 % (382433)Instruction limit reached! % 208.88/29.76 % (382433)------------------------------ % 208.88/29.76 % (382433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.88/29.76 % (382433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.88/29.76 % (382433)CaDiCaL version: 2.1.3 % 208.88/29.76 % (382433)Termination reason: Instruction limit % 208.88/29.76 % (382433)Termination phase: Saturation % 248.73/38.65 % (382433)Time elapsed: 1.273 s % 248.73/38.65 % (382433)Peak memory usage: 24 MB % 248.73/38.65 % (382433)Instructions burned: 2360 (million) % 248.73/38.65 % (382435)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2393513216:i=1778:ins=1:rtra=on_2786 on theBenchmark for (2786ds/1778Mi) % 248.73/38.65 % (382435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.73/38.65 % (382435)Terminated due to inappropriate strategy. % 248.73/38.65 % (382435)------------------------------ % 248.73/38.65 % (382435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.73/38.65 % (382435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.73/38.65 % (382435)CaDiCaL version: 2.1.3 % 248.73/38.65 % (382435)Termination reason: Inappropriate % 248.73/38.65 % (382435)Time elapsed: 0.002 s % 248.73/38.65 % (382435)Peak memory usage: 10 MB % 248.73/38.65 % (382435)Instructions burned: 3 (million) % 248.73/38.65 % (382435)------------------------------ % 248.73/38.65 % (382435)------------------------------ % 248.73/38.65 % (382437)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=2018449839:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1384Mi) % 248.73/38.65 % (382437)Instruction limit reached! % 248.73/38.65 % (382437)------------------------------ % 248.73/38.65 % (382437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.73/38.65 % (382437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.73/38.65 % (382437)CaDiCaL version: 2.1.3 % 248.73/38.65 % (382437)Termination reason: Instruction limit % 248.73/38.65 % (382437)Termination phase: Saturation % 248.73/38.65 % (382437)Time elapsed: 0.733 s % 248.73/38.65 % (382437)Peak memory usage: 32 MB % 248.73/38.65 % (382437)Instructions burned: 1384 (million) % 248.73/38.65 % (382439)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3882261363:i=1758:kws=inv_precedence:fsr=off:rtra=on_2778 on theBenchmark for (2778ds/1758Mi) % 248.73/38.65 % (382439)Instruction limit reached! % 248.73/38.65 % (382439)------------------------------ % 248.73/38.65 % (382439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.73/38.65 % (382439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.73/38.65 % (382439)CaDiCaL version: 2.1.3 % 248.73/38.65 % (382439)Termination reason: Instruction limit % 248.73/38.65 % (382439)Termination phase: Saturation % 248.73/38.65 % (382439)Time elapsed: 1.006 s % 248.73/38.65 % (382439)Peak memory usage: 24 MB % 248.73/38.65 % (382439)Instructions burned: 1761 (million) % 248.73/38.65 % (382441)fmb+10_1_sil=64000:si=on:random_seed=1484166684:i=44122:nm=2:rtra=on:gsp=on_2768 on theBenchmark for (2768ds/44122Mi) % 248.73/38.65 % (382441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.73/38.65 % (382441)Terminated due to inappropriate strategy. % 248.73/38.65 % (382441)------------------------------ % 248.73/38.65 % (382441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.73/38.65 % (382441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.73/38.65 % (382441)CaDiCaL version: 2.1.3 % 248.73/38.65 % (382441)Termination reason: Inappropriate % 248.73/38.65 % (382441)Time elapsed: 0.002 s % 248.73/38.65 % (382441)Peak memory usage: 10 MB % 248.73/38.65 % (382441)Instructions burned: 3 (million) % 248.73/38.65 % (382441)------------------------------ % 248.73/38.65 % (382441)------------------------------ % 248.73/38.65 % (382443)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4267240419:i=19030:nm=5:rtra=on_2768 on theBenchmark for (2768ds/19030Mi) % 248.73/38.65 % (382443)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.73/38.65 % (382443)Terminated due to inappropriate strategy. % 248.73/38.65 % (382443)------------------------------ % 248.73/38.65 % (382443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.73/38.65 % (382443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.73/38.65 % (382443)CaDiCaL version: 2.1.3 % 248.73/38.65 % (382443)Termination reason: Inappropriate % 248.73/38.65 % (382443)Time elapsed: 0.002 s % 248.73/38.65 % (382443)Peak memory usage: 10 MB % 248.73/38.65 % (382443)Instructions burned: 3 (million) % 248.73/38.65 % (382443)------------------------------ % 248.73/38.65 % (382443)------------------------------ % 248.73/38.65 % (382445)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1920184232:fmbsr=1.7:i=1840:rtra=on_2767 on theBenchmark for (2767ds/1840Mi) % 280.00/39.72 % (382445)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.00/39.72 % (382445)Terminated due to inappropriate strategy. % 280.00/39.72 % (382445)------------------------------ % 280.00/39.72 % (382445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.00/39.72 % (382445)CaDiCaL version: 2.1.3 % 280.00/39.72 % (382445)Termination reason: Inappropriate % 280.00/39.72 % (382445)Time elapsed: 0.002 s % 280.00/39.72 % (382445)Peak memory usage: 10 MB % 280.00/39.72 % (382445)Instructions burned: 3 (million) % 280.00/39.72 % (382445)------------------------------ % 280.00/39.72 % (382445)------------------------------ % 280.00/39.72 % (382447)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2977963075:i=10262:rtra=on_2767 on theBenchmark for (2767ds/10262Mi) % 280.00/39.72 % (382395)Instruction limit reached! % 280.00/39.72 % (382395)------------------------------ % 280.00/39.72 % (382395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.00/39.72 % (382395)CaDiCaL version: 2.1.3 % 280.00/39.72 % (382395)Termination reason: Instruction limit % 280.00/39.72 % (382395)Termination phase: Saturation % 280.00/39.72 % (382395)Time elapsed: 12.236 s % 280.00/39.72 % (382395)Peak memory usage: 27 MB % 280.00/39.72 % (382395)Instructions burned: 28120 (million) % 280.00/39.72 % (382449)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2227113704:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2719 on theBenchmark for (2719ds/2944Mi) % 280.00/39.72 % (382447)Instruction limit reached! % 280.00/39.72 % (382447)------------------------------ % 280.00/39.72 % (382447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.00/39.72 % (382447)CaDiCaL version: 2.1.3 % 280.00/39.72 % (382447)Termination reason: Instruction limit % 280.00/39.72 % (382447)Termination phase: Saturation % 280.00/39.72 % (382447)Time elapsed: 5.909 s % 280.00/39.72 % (382447)Peak memory usage: 68 MB % 280.00/39.72 % (382447)Instructions burned: 10263 (million) % 280.00/39.72 % (382451)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1779657156:i=12648:rtra=on_2708 on theBenchmark for (2708ds/12648Mi) % 280.00/39.72 % (382451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.00/39.72 % (382451)Terminated due to inappropriate strategy. % 280.00/39.72 % (382451)------------------------------ % 280.00/39.72 % (382451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.00/39.72 % (382451)CaDiCaL version: 2.1.3 % 280.00/39.72 % (382451)Termination reason: Inappropriate % 280.00/39.72 % (382451)Time elapsed: 0.002 s % 280.00/39.72 % (382451)Peak memory usage: 11 MB % 280.00/39.72 % (382451)Instructions burned: 3 (million) % 280.00/39.72 % (382451)------------------------------ % 280.00/39.72 % (382451)------------------------------ % 280.00/39.72 % (382453)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3744762295:fmbsr=2.30978:i=4348:rtra=on_2708 on theBenchmark for (2708ds/4348Mi) % 280.00/39.72 % (382453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.00/39.72 % (382453)Terminated due to inappropriate strategy. % 280.00/39.72 % (382453)------------------------------ % 280.00/39.72 % (382453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.00/39.72 % (382453)CaDiCaL version: 2.1.3 % 280.00/39.72 % (382453)Termination reason: Inappropriate % 280.00/39.72 % (382453)Time elapsed: 0.002 s % 280.00/39.72 % (382453)Peak memory usage: 10 MB % 280.00/39.72 % (382453)Instructions burned: 3 (million) % 280.00/39.72 % (382453)------------------------------ % 280.00/39.72 % (382453)------------------------------ % 280.00/39.72 % (382455)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=535338947:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2707 on theBenchmark for (2707ds/1738Mi) % 280.00/39.72 % (382449)Instruction limit reached! % 280.00/39.72 % (382449)------------------------------ % 280.00/39.72 % (382449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.00/39.72 % (382449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aTerminated % 300.66/42.64 % Vampire exiting %------------------------------------------------------------------------------