%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW601_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:30 PM UTC 2026 % Result : Timeout 291.49s 41.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW601_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.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.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:23:52 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/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 % 3.68/0.84 % (383185)Will run a generic schedule for satisfiability detection. % 3.68/0.84 % (383194)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1952059123:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.68/0.84 % (383191)% WARNING: option uhcvi not known. % 3.68/0.84 % (383190)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3402295218_2999 on theBenchmark for (2999ds/0Mi) % 3.68/0.84 % (383191)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1154926073:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.68/0.84 % (383195)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4168782305:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.84 % (383192)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2883175085:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.68/0.84 % (383193)dis+10_1_sil=32000:sp=arity:random_seed=2017744282:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.68/0.84 % (383196)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3973708412:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.68/0.84 % (383190)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.84 % (383190)Terminated due to inappropriate strategy. % 3.68/0.84 % (383190)------------------------------ % 3.68/0.84 % (383190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.84 % (383190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.84 % (383190)CaDiCaL version: 2.1.3 % 3.68/0.84 % (383190)Termination reason: Inappropriate % 3.68/0.84 % (383190)Time elapsed: 0.005 s % 3.68/0.84 % (383190)Peak memory usage: 11 MB % 3.68/0.84 % (383190)Instructions burned: 8 (million) % 3.68/0.84 % (383190)------------------------------ % 3.68/0.84 % (383190)------------------------------ % 3.68/0.84 % (383204)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3484242962:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.68/0.84 % (383204)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.84 % (383204)Terminated due to inappropriate strategy. % 3.68/0.84 % (383204)------------------------------ % 3.68/0.84 % (383204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.84 % (383204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.84 % (383204)CaDiCaL version: 2.1.3 % 3.68/0.84 % (383204)Termination reason: Inappropriate % 3.68/0.84 % (383204)Time elapsed: 0.004 s % 3.68/0.84 % (383204)Peak memory usage: 10 MB % 3.68/0.84 % (383204)Instructions burned: 7 (million) % 3.68/0.84 % (383204)------------------------------ % 3.68/0.84 % (383204)------------------------------ % 3.68/0.84 % (383194)Instruction limit reached! % 3.68/0.84 % (383194)------------------------------ % 3.68/0.84 % (383194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.84 % (383194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.84 % (383194)CaDiCaL version: 2.1.3 % 3.68/0.84 % (383194)Termination reason: Instruction limit % 3.68/0.84 % (383194)Termination phase: Saturation % 3.68/0.84 % (383194)Time elapsed: 0.041 s % 3.68/0.84 % (383194)Peak memory usage: 13 MB % 3.68/0.84 % (383194)Instructions burned: 116 (million) % 3.68/0.84 % (383207)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=1830169128:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.68/0.84 % (383206)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3248111589:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.84 % (383193)Instruction limit reached! % 3.68/0.84 % (383193)------------------------------ % 3.68/0.84 % (383193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.84 % (383193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.84 % (383193)CaDiCaL version: 2.1.3 % 3.68/0.84 % (383193)Termination reason: Instruction limit % 3.68/0.84 % (383193)Termination phase: Saturation % 3.68/0.84 % (383193)Time elapsed: 0.066 s % 3.68/0.84 % (383193)Peak memory usage: 13 MB % 3.68/0.84 % (383193)Instructions burned: 105 (million) % 3.68/0.84 % (383195)Instruction limit reached! % 3.68/0.84 % (383195)------------------------------ % 3.68/0.84 % (383195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383195)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383195)Termination reason: Instruction limit % 8.01/1.48 % (383195)Termination phase: Saturation % 8.01/1.48 % (383195)Time elapsed: 0.084 s % 8.01/1.48 % (383195)Peak memory usage: 13 MB % 8.01/1.48 % (383195)Instructions burned: 132 (million) % 8.01/1.48 % (383210)ott-21_1_sil=16000:fs=off:random_seed=543230731:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.01/1.48 % (383212)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1099323180:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.01/1.48 % (383196)Instruction limit reached! % 8.01/1.48 % (383196)------------------------------ % 8.01/1.48 % (383196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383196)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383196)Termination reason: Instruction limit % 8.01/1.48 % (383196)Termination phase: Saturation % 8.01/1.48 % (383196)Time elapsed: 0.106 s % 8.01/1.48 % (383196)Peak memory usage: 14 MB % 8.01/1.48 % (383196)Instructions burned: 160 (million) % 8.01/1.48 % (383214)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1600812805:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.01/1.48 % (383214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.01/1.48 % (383214)Terminated due to inappropriate strategy. % 8.01/1.48 % (383214)------------------------------ % 8.01/1.48 % (383214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383214)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383214)Termination reason: Inappropriate % 8.01/1.48 % (383214)Time elapsed: 0.003 s % 8.01/1.48 % (383214)Peak memory usage: 10 MB % 8.01/1.48 % (383214)Instructions burned: 6 (million) % 8.01/1.48 % (383214)------------------------------ % 8.01/1.48 % (383214)------------------------------ % 8.01/1.48 % (383206)Instruction limit reached! % 8.01/1.48 % (383206)------------------------------ % 8.01/1.48 % (383206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383206)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383206)Termination reason: Instruction limit % 8.01/1.48 % (383206)Termination phase: Saturation % 8.01/1.48 % (383206)Time elapsed: 0.087 s % 8.01/1.48 % (383206)Peak memory usage: 13 MB % 8.01/1.48 % (383206)Instructions burned: 131 (million) % 8.01/1.48 % (383216)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1685017817:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.01/1.48 % (383217)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=150614215:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.01/1.48 % (383217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.01/1.48 % (383217)Terminated due to inappropriate strategy. % 8.01/1.48 % (383217)------------------------------ % 8.01/1.48 % (383217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383217)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383217)Termination reason: Inappropriate % 8.01/1.48 % (383217)Time elapsed: 0.004 s % 8.01/1.48 % (383217)Peak memory usage: 10 MB % 8.01/1.48 % (383217)Instructions burned: 7 (million) % 8.01/1.48 % (383217)------------------------------ % 8.01/1.48 % (383217)------------------------------ % 8.01/1.48 % (383210)Instruction limit reached! % 8.01/1.48 % (383210)------------------------------ % 8.01/1.48 % (383210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.01/1.48 % (383210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.01/1.48 % (383210)CaDiCaL version: 2.1.3 % 8.01/1.48 % (383210)Termination reason: Instruction limit % 8.01/1.48 % (383210)Termination phase: Saturation % 8.01/1.48 % (383210)Time elapsed: 0.088 s % 8.01/1.48 % (383210)Peak memory usage: 13 MB % 8.01/1.48 % (383210)Instructions burned: 180 (million) % 8.01/1.48 % (383220)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=593311438: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) % 20.55/3.16 % (383221)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1261700512:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.55/3.16 % (383207)Instruction limit reached! % 20.55/3.16 % (383207)------------------------------ % 20.55/3.16 % (383207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.16 % (383207)CaDiCaL version: 2.1.3 % 20.55/3.16 % (383207)Termination reason: Instruction limit % 20.55/3.16 % (383207)Termination phase: Saturation % 20.55/3.16 % (383207)Time elapsed: 0.219 s % 20.55/3.16 % (383207)Peak memory usage: 19 MB % 20.55/3.16 % (383207)Instructions burned: 695 (million) % 20.55/3.16 % (383224)fmb+10_1_sil=64000:random_seed=1805338143:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.55/3.16 % (383224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.55/3.16 % (383224)Terminated due to inappropriate strategy. % 20.55/3.16 % (383224)------------------------------ % 20.55/3.16 % (383224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.16 % (383224)CaDiCaL version: 2.1.3 % 20.55/3.16 % (383224)Termination reason: Inappropriate % 20.55/3.16 % (383224)Time elapsed: 0.002 s % 20.55/3.16 % (383224)Peak memory usage: 10 MB % 20.55/3.16 % (383224)Instructions burned: 8 (million) % 20.55/3.16 % (383224)------------------------------ % 20.55/3.16 % (383224)------------------------------ % 20.55/3.16 % (383226)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2401563339:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.55/3.16 % (383226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.55/3.16 % (383226)Terminated due to inappropriate strategy. % 20.55/3.16 % (383226)------------------------------ % 20.55/3.16 % (383226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.16 % (383226)CaDiCaL version: 2.1.3 % 20.55/3.16 % (383226)Termination reason: Inappropriate % 20.55/3.16 % (383226)Time elapsed: 0.002 s % 20.55/3.16 % (383226)Peak memory usage: 10 MB % 20.55/3.16 % (383226)Instructions burned: 7 (million) % 20.55/3.16 % (383226)------------------------------ % 20.55/3.16 % (383226)------------------------------ % 20.55/3.16 % (383228)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1325785911:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.55/3.16 % (383228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.55/3.16 % (383228)Terminated due to inappropriate strategy. % 20.55/3.16 % (383228)------------------------------ % 20.55/3.16 % (383228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.16 % (383228)CaDiCaL version: 2.1.3 % 20.55/3.16 % (383228)Termination reason: Inappropriate % 20.55/3.16 % (383228)Time elapsed: 0.002 s % 20.55/3.16 % (383228)Peak memory usage: 10 MB % 20.55/3.16 % (383228)Instructions burned: 7 (million) % 20.55/3.16 % (383228)------------------------------ % 20.55/3.16 % (383228)------------------------------ % 20.55/3.16 % (383230)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3575035321:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.55/3.16 % (383212)Instruction limit reached! % 20.55/3.16 % (383212)------------------------------ % 20.55/3.16 % (383212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.16 % (383212)CaDiCaL version: 2.1.3 % 20.55/3.16 % (383212)Termination reason: Instruction limit % 20.55/3.16 % (383212)Termination phase: Saturation % 20.55/3.16 % (383212)Time elapsed: 0.326 s % 20.55/3.16 % (383212)Peak memory usage: 14 MB % 20.55/3.16 % (383212)Instructions burned: 477 (million) % 20.55/3.16 % (383232)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=432988197:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.55/3.16 % (383220)Instruction limit reached! % 20.55/3.16 % (383220)------------------------------ % 20.55/3.16 % (383220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.16 % (383220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383220)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383220)Termination reason: Instruction limit % 24.31/4.03 % (383220)Termination phase: Saturation % 24.31/4.03 % (383220)Time elapsed: 0.394 s % 24.31/4.03 % (383220)Peak memory usage: 17 MB % 24.31/4.03 % (383220)Instructions burned: 693 (million) % 24.31/4.03 % (383234)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3636793859:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 24.31/4.03 % (383234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.31/4.03 % (383234)Terminated due to inappropriate strategy. % 24.31/4.03 % (383234)------------------------------ % 24.31/4.03 % (383234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.31/4.03 % (383234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383234)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383234)Termination reason: Inappropriate % 24.31/4.03 % (383234)Time elapsed: 0.005 s % 24.31/4.03 % (383234)Peak memory usage: 11 MB % 24.31/4.03 % (383234)Instructions burned: 8 (million) % 24.31/4.03 % (383234)------------------------------ % 24.31/4.03 % (383234)------------------------------ % 24.31/4.03 % (383236)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1140514339:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 24.31/4.03 % (383236)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.31/4.03 % (383236)Terminated due to inappropriate strategy. % 24.31/4.03 % (383236)------------------------------ % 24.31/4.03 % (383236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.31/4.03 % (383236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383236)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383236)Termination reason: Inappropriate % 24.31/4.03 % (383236)Time elapsed: 0.004 s % 24.31/4.03 % (383236)Peak memory usage: 10 MB % 24.31/4.03 % (383236)Instructions burned: 7 (million) % 24.31/4.03 % (383236)------------------------------ % 24.31/4.03 % (383236)------------------------------ % 24.31/4.03 % (383238)ott-2_1_sil=16000:newcnf=on:random_seed=1287204758:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.31/4.03 % (383221)Instruction limit reached! % 24.31/4.03 % (383221)------------------------------ % 24.31/4.03 % (383221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.31/4.03 % (383221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383221)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383221)Termination reason: Instruction limit % 24.31/4.03 % (383221)Termination phase: Saturation % 24.31/4.03 % (383221)Time elapsed: 0.501 s % 24.31/4.03 % (383221)Peak memory usage: 19 MB % 24.31/4.03 % (383221)Instructions burned: 879 (million) % 24.31/4.03 % (383240)ott+10_1_sil=32000:tgt=ground:random_seed=2778744425:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 24.31/4.03 % (383216)Instruction limit reached! % 24.31/4.03 % (383216)------------------------------ % 24.31/4.03 % (383216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.31/4.03 % (383216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383216)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383216)Termination reason: Instruction limit % 24.31/4.03 % (383216)Termination phase: Saturation % 24.31/4.03 % (383216)Time elapsed: 0.718 s % 24.31/4.03 % (383216)Peak memory usage: 22 MB % 24.31/4.03 % (383216)Instructions burned: 1180 (million) % 24.31/4.03 % (383242)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3390045884:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 24.31/4.03 % (383242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.31/4.03 % (383242)Terminated due to inappropriate strategy. % 24.31/4.03 % (383242)------------------------------ % 24.31/4.03 % (383242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.31/4.03 % (383242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.31/4.03 % (383242)CaDiCaL version: 2.1.3 % 24.31/4.03 % (383242)Termination reason: Inappropriate % 24.31/4.03 % (383242)Time elapsed: 0.005 s % 24.31/4.03 % (383242)Peak memory usage: 11 MB % 24.31/4.03 % (383242)Instructions burned: 8 (million) % 24.31/4.03 % (383242)------------------------------ % 24.31/4.03 % (383242)------------------------------ % 24.31/4.03 % (383244)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1619238018:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 24.31/4.03 % (383238)Instruction limit reached! % 87.76/12.62 % (383238)------------------------------ % 87.76/12.62 % (383238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383238)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383238)Termination reason: Instruction limit % 87.76/12.62 % (383238)Termination phase: Saturation % 87.76/12.62 % (383238)Time elapsed: 0.561 s % 87.76/12.62 % (383238)Peak memory usage: 18 MB % 87.76/12.62 % (383238)Instructions burned: 870 (million) % 87.76/12.62 % (383246)dis+21_1_sil=32000:sas=cadical:random_seed=2918051668:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 87.76/12.62 % (383232)Instruction limit reached! % 87.76/12.62 % (383232)------------------------------ % 87.76/12.62 % (383232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383232)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383232)Termination reason: Instruction limit % 87.76/12.62 % (383232)Termination phase: Saturation % 87.76/12.62 % (383232)Time elapsed: 0.849 s % 87.76/12.62 % (383232)Peak memory usage: 29 MB % 87.76/12.62 % (383232)Instructions burned: 1474 (million) % 87.76/12.62 % (383248)ott+11_1_sil=16000:gs=on:random_seed=611645965:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 87.76/12.62 % (383230)Instruction limit reached! % 87.76/12.62 % (383230)------------------------------ % 87.76/12.62 % (383230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383230)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383230)Termination reason: Instruction limit % 87.76/12.62 % (383230)Termination phase: Saturation % 87.76/12.62 % (383230)Time elapsed: 1.497 s % 87.76/12.62 % (383230)Peak memory usage: 41 MB % 87.76/12.62 % (383230)Instructions burned: 5134 (million) % 87.76/12.62 % (383250)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1639708133:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 87.76/12.62 % (383250)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.76/12.62 % (383250)Terminated due to inappropriate strategy. % 87.76/12.62 % (383250)------------------------------ % 87.76/12.62 % (383250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383250)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383250)Termination reason: Inappropriate % 87.76/12.62 % (383250)Time elapsed: 0.002 s % 87.76/12.62 % (383250)Peak memory usage: 10 MB % 87.76/12.62 % (383250)Instructions burned: 7 (million) % 87.76/12.62 % (383250)------------------------------ % 87.76/12.62 % (383250)------------------------------ % 87.76/12.62 % (383252)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1227997817: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.76/12.62 % (383248)Instruction limit reached! % 87.76/12.62 % (383248)------------------------------ % 87.76/12.62 % (383248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383248)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383248)Termination reason: Instruction limit % 87.76/12.62 % (383248)Termination phase: Saturation % 87.76/12.62 % (383248)Time elapsed: 1.150 s % 87.76/12.62 % (383248)Peak memory usage: 20 MB % 87.76/12.62 % (383248)Instructions burned: 2252 (million) % 87.76/12.62 % (383254)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=225170827:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 87.76/12.62 % (383252)Instruction limit reached! % 87.76/12.62 % (383252)------------------------------ % 87.76/12.62 % (383252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.76/12.62 % (383252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.76/12.62 % (383252)CaDiCaL version: 2.1.3 % 87.76/12.62 % (383252)Termination reason: Instruction limit % 87.76/12.62 % (383252)Termination phase: Saturation % 87.76/12.62 % (383252)Time elapsed: 1.037 s % 87.76/12.62 % (383252)Peak memory usage: 31 MB % 87.76/12.62 % (383252)Instructions burned: 4592 (million) % 87.76/12.62 % (383244)Instruction limit reached! % 87.76/12.62 % (383244)------------------------------ % 87.76/12.62 % (383244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383244)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383244)Termination reason: Instruction limit % 118.29/16.92 % (383244)Termination phase: Saturation % 118.29/16.92 % (383244)Time elapsed: 1.974 s % 118.29/16.92 % (383244)Peak memory usage: 31 MB % 118.29/16.92 % (383244)Instructions burned: 3512 (million) % 118.29/16.92 % (383256)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=576966052:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 118.29/16.92 % (383258)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1545847162:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 118.29/16.92 % (383258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.29/16.92 % (383258)Terminated due to inappropriate strategy. % 118.29/16.92 % (383258)------------------------------ % 118.29/16.92 % (383258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383258)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383258)Termination reason: Inappropriate % 118.29/16.92 % (383258)Time elapsed: 0.005 s % 118.29/16.92 % (383258)Peak memory usage: 11 MB % 118.29/16.92 % (383258)Instructions burned: 8 (million) % 118.29/16.92 % (383258)------------------------------ % 118.29/16.92 % (383258)------------------------------ % 118.29/16.92 % (383260)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3577371646:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 118.29/16.92 % (383260)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.29/16.92 % (383260)Terminated due to inappropriate strategy. % 118.29/16.92 % (383260)------------------------------ % 118.29/16.92 % (383260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383260)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383260)Termination reason: Inappropriate % 118.29/16.92 % (383260)Time elapsed: 0.004 s % 118.29/16.92 % (383260)Peak memory usage: 10 MB % 118.29/16.92 % (383260)Instructions burned: 7 (million) % 118.29/16.92 % (383260)------------------------------ % 118.29/16.92 % (383260)------------------------------ % 118.29/16.92 % (383262)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1113268508:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 118.29/16.92 % (383262)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.29/16.92 % (383262)Terminated due to inappropriate strategy. % 118.29/16.92 % (383262)------------------------------ % 118.29/16.92 % (383262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383262)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383262)Termination reason: Inappropriate % 118.29/16.92 % (383262)Time elapsed: 0.004 s % 118.29/16.92 % (383262)Peak memory usage: 10 MB % 118.29/16.92 % (383262)Instructions burned: 7 (million) % 118.29/16.92 % (383262)------------------------------ % 118.29/16.92 % (383262)------------------------------ % 118.29/16.92 % (383264)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3724789701:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 118.29/16.92 % (383246)Instruction limit reached! % 118.29/16.92 % (383246)------------------------------ % 118.29/16.92 % (383246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383246)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383246)Termination reason: Instruction limit % 118.29/16.92 % (383246)Termination phase: Saturation % 118.29/16.92 % (383246)Time elapsed: 2.122 s % 118.29/16.92 % (383246)Peak memory usage: 35 MB % 118.29/16.92 % (383246)Instructions burned: 3773 (million) % 118.29/16.92 % (383266)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=389816900:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 118.29/16.92 % (383240)Instruction limit reached! % 118.29/16.92 % (383240)------------------------------ % 118.29/16.92 % (383240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.29/16.92 % (383240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.29/16.92 % (383240)CaDiCaL version: 2.1.3 % 118.29/16.92 % (383240)Termination reason: Instruction limit % 118.29/16.92 % (383240)Termination phase: Saturation % 118.29/16.92 % (383240)Time elapsed: 3.041 s % 121.82/17.50 % (383240)Peak memory usage: 49 MB % 121.82/17.50 % (383240)Instructions burned: 5115 (million) % 121.82/17.50 % (383268)dis+10_16:1_sil=16000:random_seed=2301908065:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 121.82/17.50 % (383256)Instruction limit reached! % 121.82/17.50 % (383256)------------------------------ % 121.82/17.50 % (383256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383256)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383256)Termination reason: Instruction limit % 121.82/17.50 % (383256)Termination phase: Saturation % 121.82/17.50 % (383256)Time elapsed: 1.407 s % 121.82/17.50 % (383256)Peak memory usage: 43 MB % 121.82/17.50 % (383256)Instructions burned: 5215 (million) % 121.82/17.50 % (383270)ott-3_8_sil=64000:random_seed=1826185225:i=20139:bs=on_2956 on theBenchmark for (2956ds/20139Mi) % 121.82/17.50 % (383266)Instruction limit reached! % 121.82/17.50 % (383266)------------------------------ % 121.82/17.50 % (383266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383266)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383266)Termination reason: Instruction limit % 121.82/17.50 % (383266)Termination phase: Saturation % 121.82/17.50 % (383266)Time elapsed: 4.936 s % 121.82/17.50 % (383266)Peak memory usage: 70 MB % 121.82/17.50 % (383266)Instructions burned: 8174 (million) % 121.82/17.50 % (383272)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2079129247:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 121.82/17.50 % (383272)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.82/17.50 % (383272)Terminated due to inappropriate strategy. % 121.82/17.50 % (383272)------------------------------ % 121.82/17.50 % (383272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383272)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383272)Termination reason: Inappropriate % 121.82/17.50 % (383272)Time elapsed: 0.005 s % 121.82/17.50 % (383272)Peak memory usage: 11 MB % 121.82/17.50 % (383272)Instructions burned: 8 (million) % 121.82/17.50 % (383272)------------------------------ % 121.82/17.50 % (383272)------------------------------ % 121.82/17.50 % (383274)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1511736015:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 121.82/17.50 % (383268)Instruction limit reached! % 121.82/17.50 % (383268)------------------------------ % 121.82/17.50 % (383268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383268)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383268)Termination reason: Instruction limit % 121.82/17.50 % (383268)Termination phase: Saturation % 121.82/17.50 % (383268)Time elapsed: 4.708 s % 121.82/17.50 % (383268)Peak memory usage: 55 MB % 121.82/17.50 % (383268)Instructions burned: 9157 (million) % 121.82/17.50 % (383276)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1885117275:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 121.82/17.50 % (383270)Instruction limit reached! % 121.82/17.50 % (383270)------------------------------ % 121.82/17.50 % (383270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383270)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383270)Termination reason: Instruction limit % 121.82/17.50 % (383270)Termination phase: Saturation % 121.82/17.50 % (383270)Time elapsed: 7.315 s % 121.82/17.50 % (383270)Peak memory usage: 110 MB % 121.82/17.50 % (383270)Instructions burned: 20139 (million) % 121.82/17.50 % (383278)dis+33_16_sil=32000:sac=on:random_seed=3921558480:i=15851:nm=0_2883 on theBenchmark for (2883ds/15851Mi) % 121.82/17.50 % (383264)Instruction limit reached! % 121.82/17.50 % (383264)------------------------------ % 121.82/17.50 % (383264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.82/17.50 % (383264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.82/17.50 % (383264)CaDiCaL version: 2.1.3 % 121.82/17.50 % (383264)Termination reason: Instruction limit % 121.82/17.50 % (383264)Termination phase: Saturation % 121.82/17.50 % (383264)Time elapsed: 9.327 s % 121.82/17.50 % (383264)Peak memory usage: 96 MB % 121.82/17.50 % (383264)Instructions burned: 22565 (million) % 121.82/17.50 % (383280)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3347899817:avsq=on:i=17627:add=on:amm=off_2876 on theBenchmark for (2876ds/17627Mi) % 153.06/21.82 % (383254)Instruction limit reached! % 153.06/21.82 % (383254)------------------------------ % 153.06/21.82 % (383254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383254)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383254)Termination reason: Instruction limit % 153.06/21.82 % (383254)Termination phase: Saturation % 153.06/21.82 % (383254)Time elapsed: 12.279 s % 153.06/21.82 % (383254)Peak memory usage: 161 MB % 153.06/21.82 % (383254)Instructions burned: 29340 (million) % 153.06/21.82 % (383344)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=636125105:s2a=on:i=53295_2851 on theBenchmark for (2851ds/53295Mi) % 153.06/21.82 % (383274)Instruction limit reached! % 153.06/21.82 % (383274)------------------------------ % 153.06/21.82 % (383274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383274)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383274)Termination reason: Instruction limit % 153.06/21.82 % (383274)Termination phase: Saturation % 153.06/21.82 % (383274)Time elapsed: 7.163 s % 153.06/21.82 % (383274)Peak memory usage: 75 MB % 153.06/21.82 % (383274)Instructions burned: 11405 (million) % 153.06/21.82 % (383346)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3165446013:i=26857:ins=20_2844 on theBenchmark for (2844ds/26857Mi) % 153.06/21.82 % (383346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/21.82 % (383346)Terminated due to inappropriate strategy. % 153.06/21.82 % (383346)------------------------------ % 153.06/21.82 % (383346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383346)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383346)Termination reason: Inappropriate % 153.06/21.82 % (383346)Time elapsed: 0.004 s % 153.06/21.82 % (383346)Peak memory usage: 10 MB % 153.06/21.82 % (383346)Instructions burned: 7 (million) % 153.06/21.82 % (383346)------------------------------ % 153.06/21.82 % (383346)------------------------------ % 153.06/21.82 % (383348)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2245178255:i=28120:bs=on:fsr=off_2844 on theBenchmark for (2844ds/28120Mi) % 153.06/21.82 % (383278)Instruction limit reached! % 153.06/21.82 % (383278)------------------------------ % 153.06/21.82 % (383278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383278)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383278)Termination reason: Instruction limit % 153.06/21.82 % (383278)Termination phase: Saturation % 153.06/21.82 % (383278)Time elapsed: 4.952 s % 153.06/21.82 % (383278)Peak memory usage: 169 MB % 153.06/21.82 % (383278)Instructions burned: 15852 (million) % 153.06/21.82 % (383350)fmb+10_1_sil=256000:fmbss=7:random_seed=2302406171:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 153.06/21.82 % (383350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/21.82 % (383350)Terminated due to inappropriate strategy. % 153.06/21.82 % (383350)------------------------------ % 153.06/21.82 % (383350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383350)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383350)Termination reason: Inappropriate % 153.06/21.82 % (383350)Time elapsed: 0.002 s % 153.06/21.82 % (383350)Peak memory usage: 10 MB % 153.06/21.82 % (383350)Instructions burned: 7 (million) % 153.06/21.82 % (383350)------------------------------ % 153.06/21.82 % (383350)------------------------------ % 153.06/21.82 % (383352)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4115587714:i=44625:gsp=on_2833 on theBenchmark for (2833ds/44625Mi) % 153.06/21.82 % (383352)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/21.82 % (383352)Terminated due to inappropriate strategy. % 153.06/21.82 % (383352)------------------------------ % 153.06/21.82 % (383352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/21.82 % (383352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/21.82 % (383352)CaDiCaL version: 2.1.3 % 153.06/21.82 % (383352)Termination reason: Inappropriate % 177.88/25.35 % (383352)Time elapsed: 0.002 s % 177.88/25.35 % (383352)Peak memory usage: 10 MB % 177.88/25.35 % (383352)Instructions burned: 8 (million) % 177.88/25.35 % (383352)------------------------------ % 177.88/25.35 % (383352)------------------------------ % 177.88/25.35 % (383354)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1621154661:i=160505_2833 on theBenchmark for (2833ds/160505Mi) % 177.88/25.35 % (383354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.88/25.35 % (383354)Terminated due to inappropriate strategy. % 177.88/25.35 % (383354)------------------------------ % 177.88/25.35 % (383354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.88/25.35 % (383354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.88/25.35 % (383354)CaDiCaL version: 2.1.3 % 177.88/25.35 % (383354)Termination reason: Inappropriate % 177.88/25.35 % (383354)Time elapsed: 0.002 s % 177.88/25.35 % (383354)Peak memory usage: 10 MB % 177.88/25.35 % (383354)Instructions burned: 7 (million) % 177.88/25.35 % (383354)------------------------------ % 177.88/25.35 % (383354)------------------------------ % 177.88/25.35 % (383356)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1679563338:fmbsr=1.3:i=225729_2832 on theBenchmark for (2832ds/225729Mi) % 177.88/25.35 % (383356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.88/25.35 % (383356)Terminated due to inappropriate strategy. % 177.88/25.35 % (383356)------------------------------ % 177.88/25.35 % (383356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.88/25.35 % (383356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.88/25.35 % (383356)CaDiCaL version: 2.1.3 % 177.88/25.35 % (383356)Termination reason: Inappropriate % 177.88/25.35 % (383356)Time elapsed: 0.002 s % 177.88/25.35 % (383356)Peak memory usage: 10 MB % 177.88/25.35 % (383356)Instructions burned: 7 (million) % 177.88/25.35 % (383356)------------------------------ % 177.88/25.35 % (383356)------------------------------ % 177.88/25.35 % (383358)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1234437823:fmbsr=2:i=185024:ins=7_2832 on theBenchmark for (2832ds/185024Mi) % 177.88/25.35 % (383358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.88/25.35 % (383358)Terminated due to inappropriate strategy. % 177.88/25.35 % (383358)------------------------------ % 177.88/25.35 % (383358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.88/25.35 % (383358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.88/25.35 % (383358)CaDiCaL version: 2.1.3 % 177.88/25.35 % (383358)Termination reason: Inappropriate % 177.88/25.35 % (383358)Time elapsed: 0.004 s % 177.88/25.35 % (383358)Peak memory usage: 10 MB % 177.88/25.35 % (383358)Instructions burned: 7 (million) % 177.88/25.35 % (383358)------------------------------ % 177.88/25.35 % (383358)------------------------------ % 177.88/25.35 % (383360)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3252651119:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 177.88/25.35 % (383360)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.88/25.35 % (383360)Terminated due to inappropriate strategy. % 177.88/25.35 % (383360)------------------------------ % 177.88/25.35 % (383360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.88/25.35 % (383360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.88/25.35 % (383360)CaDiCaL version: 2.1.3 % 177.88/25.35 % (383360)Termination reason: Inappropriate % 177.88/25.35 % (383360)Time elapsed: 0.005 s % 177.88/25.35 % (383360)Peak memory usage: 11 MB % 177.88/25.35 % (383360)Instructions burned: 9 (million) % 177.88/25.35 % (383360)------------------------------ % 177.88/25.35 % (383360)------------------------------ % 177.88/25.35 % (383362)% WARNING: option uhcvi not known. % 177.88/25.35 % (383362)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1864963031:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 177.88/25.35 % (383276)Instruction limit reached! % 177.88/25.35 % (383276)------------------------------ % 177.88/25.35 % (383276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.88/25.35 % (383276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.88/25.35 % (383276)CaDiCaL version: 2.1.3 % 177.88/25.35 % (383276)Termination reason: Instruction limit % 177.88/25.35 % (383276)Termination phase: Saturation % 177.88/25.35 % (383276)Time elapsed: 8.680 s % 177.88/25.35 % (383276)Peak memory usage: 89 MB % 177.88/25.35 % (383276)Instructions burned: 14135 (million) % 177.88/25.35 % (383364)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2807193677:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 192.08/27.35 % (383280)Instruction limit reached! % 192.08/27.35 % (383280)------------------------------ % 192.08/27.35 % (383280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383280)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383280)Termination reason: Instruction limit % 192.08/27.35 % (383280)Termination phase: Saturation % 192.08/27.35 % (383280)Time elapsed: 8.385 s % 192.08/27.35 % (383280)Peak memory usage: 130 MB % 192.08/27.35 % (383280)Instructions burned: 17627 (million) % 192.08/27.35 % (383367)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2685220793:i=206:fgj=on:rtra=on_2792 on theBenchmark for (2792ds/206Mi) % 192.08/27.35 % (383367)Instruction limit reached! % 192.08/27.35 % (383367)------------------------------ % 192.08/27.35 % (383367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383367)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383367)Termination reason: Instruction limit % 192.08/27.35 % (383367)Termination phase: Saturation % 192.08/27.35 % (383367)Time elapsed: 0.134 s % 192.08/27.35 % (383367)Peak memory usage: 14 MB % 192.08/27.35 % (383367)Instructions burned: 206 (million) % 192.08/27.35 % (383369)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1756781494:i=232:rtra=on_2790 on theBenchmark for (2790ds/232Mi) % 192.08/27.35 % (383369)Instruction limit reached! % 192.08/27.35 % (383369)------------------------------ % 192.08/27.35 % (383369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383369)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383369)Termination reason: Instruction limit % 192.08/27.35 % (383369)Termination phase: Saturation % 192.08/27.35 % (383369)Time elapsed: 0.159 s % 192.08/27.35 % (383369)Peak memory usage: 14 MB % 192.08/27.35 % (383369)Instructions burned: 233 (million) % 192.08/27.35 % (383371)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2844794569:i=262:rtra=on_2788 on theBenchmark for (2788ds/262Mi) % 192.08/27.35 % (383371)Instruction limit reached! % 192.08/27.35 % (383371)------------------------------ % 192.08/27.35 % (383371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383371)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383371)Termination reason: Instruction limit % 192.08/27.35 % (383371)Termination phase: Saturation % 192.08/27.35 % (383371)Time elapsed: 0.179 s % 192.08/27.35 % (383371)Peak memory usage: 15 MB % 192.08/27.35 % (383371)Instructions burned: 262 (million) % 192.08/27.35 % (383373)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2863375920:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2786 on theBenchmark for (2786ds/318Mi) % 192.08/27.35 % (383373)Instruction limit reached! % 192.08/27.35 % (383373)------------------------------ % 192.08/27.35 % (383373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383373)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383373)Termination reason: Instruction limit % 192.08/27.35 % (383373)Termination phase: Saturation % 192.08/27.35 % (383373)Time elapsed: 0.220 s % 192.08/27.35 % (383373)Peak memory usage: 16 MB % 192.08/27.35 % (383373)Instructions burned: 318 (million) % 192.08/27.35 % (383375)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=418641512:i=1428:nm=2:rtra=on_2784 on theBenchmark for (2784ds/1428Mi) % 192.08/27.35 % (383375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.08/27.35 % (383375)Terminated due to inappropriate strategy. % 192.08/27.35 % (383375)------------------------------ % 192.08/27.35 % (383375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.08/27.35 % (383375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.08/27.35 % (383375)CaDiCaL version: 2.1.3 % 192.08/27.35 % (383375)Termination reason: Inappropriate % 192.08/27.35 % (383375)Time elapsed: 0.005 s % 192.08/27.35 % (383375)Peak memory usage: 10 MB % 192.08/27.35 % (383375)Instructions burned: 8 (million) % 192.08/27.35 % (383375)------------------------------ % 192.08/27.35 % (383375)------------------------------ % 242.51/34.43 % (383377)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2564225379:i=262:bd=preordered:rtra=on:fsd=on_2784 on theBenchmark for (2784ds/262Mi) % 242.51/34.43 % (383377)Instruction limit reached! % 242.51/34.43 % (383377)------------------------------ % 242.51/34.43 % (383377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383377)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383377)Termination reason: Instruction limit % 242.51/34.43 % (383377)Termination phase: Saturation % 242.51/34.43 % (383377)Time elapsed: 0.166 s % 242.51/34.43 % (383377)Peak memory usage: 14 MB % 242.51/34.43 % (383377)Instructions burned: 262 (million) % 242.51/34.43 % (383379)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=1198146678:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/1368Mi) % 242.51/34.43 % (383379)Instruction limit reached! % 242.51/34.43 % (383379)------------------------------ % 242.51/34.43 % (383379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383379)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383379)Termination reason: Instruction limit % 242.51/34.43 % (383379)Termination phase: Saturation % 242.51/34.43 % (383379)Time elapsed: 0.858 s % 242.51/34.43 % (383379)Peak memory usage: 26 MB % 242.51/34.43 % (383379)Instructions burned: 1368 (million) % 242.51/34.43 % (383381)ott-21_1_sil=16000:si=on:fs=off:random_seed=3313556152:i=360:av=off:fsr=off:rtra=on_2773 on theBenchmark for (2773ds/360Mi) % 242.51/34.43 % (383381)Instruction limit reached! % 242.51/34.43 % (383381)------------------------------ % 242.51/34.43 % (383381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383381)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383381)Termination reason: Instruction limit % 242.51/34.43 % (383381)Termination phase: Saturation % 242.51/34.43 % (383381)Time elapsed: 0.193 s % 242.51/34.43 % (383381)Peak memory usage: 14 MB % 242.51/34.43 % (383381)Instructions burned: 362 (million) % 242.51/34.43 % (383383)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1366468829:i=954:bd=all:rtra=on_2771 on theBenchmark for (2771ds/954Mi) % 242.51/34.43 % (383383)Instruction limit reached! % 242.51/34.43 % (383383)------------------------------ % 242.51/34.43 % (383383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383383)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383383)Termination reason: Instruction limit % 242.51/34.43 % (383383)Termination phase: Saturation % 242.51/34.43 % (383383)Time elapsed: 0.620 s % 242.51/34.43 % (383383)Peak memory usage: 16 MB % 242.51/34.43 % (383383)Instructions burned: 954 (million) % 242.51/34.43 % (383385)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2171237272:fmbsr=1.3:i=1730:ins=25:rtra=on_2764 on theBenchmark for (2764ds/1730Mi) % 242.51/34.43 % (383385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 242.51/34.43 % (383385)Terminated due to inappropriate strategy. % 242.51/34.43 % (383385)------------------------------ % 242.51/34.43 % (383385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383385)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383385)Termination reason: Inappropriate % 242.51/34.43 % (383385)Time elapsed: 0.004 s % 242.51/34.43 % (383385)Peak memory usage: 10 MB % 242.51/34.43 % (383385)Instructions burned: 7 (million) % 242.51/34.43 % (383385)------------------------------ % 242.51/34.43 % (383385)------------------------------ % 242.51/34.43 % (383387)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2962490729:i=2358:rtra=on_2764 on theBenchmark for (2764ds/2358Mi) % 242.51/34.43 % (383387)Instruction limit reached! % 242.51/34.43 % (383387)------------------------------ % 242.51/34.43 % (383387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.51/34.43 % (383387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.51/34.43 % (383387)CaDiCaL version: 2.1.3 % 242.51/34.43 % (383387)Termination reason: Instruction limit % 242.51/34.43 % (383387)Termination phase: Saturation % 291.49/41.31 % (383387)Time elapsed: 1.557 s % 291.49/41.31 % (383387)Peak memory usage: 33 MB % 291.49/41.31 % (383387)Instructions burned: 2358 (million) % 291.49/41.31 % (383389)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4128954728:i=1778:ins=1:rtra=on_2748 on theBenchmark for (2748ds/1778Mi) % 291.49/41.31 % (383389)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.49/41.31 % (383389)Terminated due to inappropriate strategy. % 291.49/41.31 % (383389)------------------------------ % 291.49/41.31 % (383389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.49/41.31 % (383389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.49/41.31 % (383389)CaDiCaL version: 2.1.3 % 291.49/41.31 % (383389)Termination reason: Inappropriate % 291.49/41.31 % (383389)Time elapsed: 0.005 s % 291.49/41.31 % (383389)Peak memory usage: 10 MB % 291.49/41.31 % (383389)Instructions burned: 8 (million) % 291.49/41.31 % (383389)------------------------------ % 291.49/41.31 % (383389)------------------------------ % 291.49/41.31 % (383391)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=125545209:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1384Mi) % 291.49/41.31 % (383391)Instruction limit reached! % 291.49/41.31 % (383391)------------------------------ % 291.49/41.31 % (383391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.49/41.31 % (383391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.49/41.31 % (383391)CaDiCaL version: 2.1.3 % 291.49/41.31 % (383391)Termination reason: Instruction limit % 291.49/41.31 % (383391)Termination phase: Saturation % 291.49/41.31 % (383391)Time elapsed: 0.863 s % 291.49/41.31 % (383391)Peak memory usage: 27 MB % 291.49/41.31 % (383391)Instructions burned: 1384 (million) % 291.49/41.31 % (383393)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3824313464:i=1758:kws=inv_precedence:fsr=off:rtra=on_2739 on theBenchmark for (2739ds/1758Mi) % 291.49/41.31 % (383393)Instruction limit reached! % 291.49/41.31 % (383393)------------------------------ % 291.49/41.31 % (383393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.49/41.31 % (383393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.49/41.31 % (383393)CaDiCaL version: 2.1.3 % 291.49/41.31 % (383393)Termination reason: Instruction limit % 291.49/41.31 % (383393)Termination phase: Saturation % 291.49/41.31 % (383393)Time elapsed: 0.989 s % 291.49/41.31 % (383393)Peak memory usage: 24 MB % 291.49/41.31 % (383393)Instructions burned: 1758 (million) % 291.49/41.31 % (383395)fmb+10_1_sil=64000:si=on:random_seed=1519943252:i=44122:nm=2:rtra=on:gsp=on_2729 on theBenchmark for (2729ds/44122Mi) % 291.49/41.31 % (383395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.49/41.31 % (383395)Terminated due to inappropriate strategy. % 291.49/41.31 % (383395)------------------------------ % 291.49/41.31 % (383395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.49/41.31 % (383395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.49/41.31 % (383395)CaDiCaL version: 2.1.3 % 291.49/41.31 % (383395)Termination reason: Inappropriate % 291.49/41.31 % (383395)Time elapsed: 0.005 s % 291.49/41.31 % (383395)Peak memory usage: 10 MB % 291.49/41.31 % (383395)Instructions burned: 9 (million) % 291.49/41.31 % (383395)------------------------------ % 291.49/41.31 % (383395)------------------------------ % 291.49/41.31 % (383397)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=795916588:i=19030:nm=5:rtra=on_2729 on theBenchmark for (2729ds/19030Mi) % 291.49/41.31 % (383397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.49/41.31 % (383397)Terminated due to inappropriate strategy. % 291.49/41.31 % (383397)------------------------------ % 291.49/41.31 % (383397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.49/41.31 % (383397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.49/41.31 % (383397)CaDiCaL version: 2.1.3 % 291.49/41.31 % (383397)Termination reason: Inappropriate % 291.49/41.31 % (383397)Time elapsed: 0.005 s % 291.49/41.31 % (383397)Peak memory usage: 10 MB % 291.49/41.31 % (383397)Instructions burned: 8 (million) % 291.49/41.31 % (383397)------------------------------ % 291.49/41.31 % (383397)------------------------------ % 291.49/41.31 % (383399)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1392822301:fmbsr=1.7:i=1840:rtra=on_2729 on theBenchmark for (2729ds/1840Mi) % 300.00/42.53 % (383399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.00/42.53 % (383399)Terminated due to inappropriate strategy. % 300.00/42.53 % (383399)------------------------------ % 300.00/42.53 % (383399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.00/42.53 % (383399)CaDiCaL version: 2.1.3 % 300.00/42.53 % (383399)Termination reason: Inappropriate % 300.00/42.53 % (383399)Time elapsed: 0.005 s % 300.00/42.53 % (383399)Peak memory usage: 10 MB % 300.00/42.53 % (383399)Instructions burned: 8 (million) % 300.00/42.53 % (383399)------------------------------ % 300.00/42.53 % (383399)------------------------------ % 300.00/42.53 % (383401)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3525678193:i=10262:rtra=on_2728 on theBenchmark for (2728ds/10262Mi) % 300.00/42.53 % (383348)Instruction limit reached! % 300.00/42.53 % (383348)------------------------------ % 300.00/42.53 % (383348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.00/42.53 % (383348)CaDiCaL version: 2.1.3 % 300.00/42.53 % (383348)Termination reason: Instruction limit % 300.00/42.53 % (383348)Termination phase: Saturation % 300.00/42.53 % (383348)Time elapsed: 16.751 s % 300.00/42.53 % (383348)Peak memory usage: 102 MB % 300.00/42.53 % (383348)Instructions burned: 28121 (million) % 300.00/42.53 % (383405)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2689814648:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2676 on theBenchmark for (2676ds/2944Mi) % 300.00/42.53 % (383401)Instruction limit reached! % 300.00/42.53 % (383401)------------------------------ % 300.00/42.53 % (383401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.00/42.53 % (383401)CaDiCaL version: 2.1.3 % 300.00/42.53 % (383401)Termination reason: Instruction limit % 300.00/42.53 % (383401)Termination phase: Saturation % 300.00/42.53 % (383401)Time elapsed: 6.132 s % 300.00/42.53 % (383401)Peak memory usage: 61 MB % 300.00/42.53 % (383401)Instructions burned: 10263 (million) % 300.00/42.53 % (383407)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3069320977:i=12648:rtra=on_2667 on theBenchmark for (2667ds/12648Mi) % 300.00/42.53 % (383407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.00/42.53 % (383407)Terminated due to inappropriate strategy. % 300.00/42.53 % (383407)------------------------------ % 300.00/42.53 % (383407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.00/42.53 % (383407)CaDiCaL version: 2.1.3 % 300.00/42.53 % (383407)Termination reason: Inappropriate % 300.00/42.53 % (383407)Time elapsed: 0.006 s % 300.00/42.53 % (383407)Peak memory usage: 11 MB % 300.00/42.53 % (383407)Instructions burned: 9 (million) % 300.00/42.53 % (383407)------------------------------ % 300.00/42.53 % (383407)------------------------------ % 300.00/42.53 % (383409)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4178752729:fmbsr=2.30978:i=4348:rtra=on_2666 on theBenchmark for (2666ds/4348Mi) % 300.00/42.53 % (383409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.00/42.53 % (383409)Terminated due to inappropriate strategy. % 300.00/42.53 % (383409)------------------------------ % 300.00/42.53 % (383409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.00/42.53 % (383409)CaDiCaL version: 2.1.3 % 300.00/42.53 % (383409)Termination reason: Inappropriate % 300.00/42.53 % (383409)Time elapsed: 0.005 s % 300.00/42.53 % (383409)Peak memory usage: 10 MB % 300.00/42.53 % (383409)Instructions burned: 8 (million) % 300.00/42.53 % (383409)------------------------------ % 300.00/42.53 % (383409)------------------------------ % 300.00/42.53 % (383411)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3816090360:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2666 on theBenchmark for (2666ds/1738Mi) % 300.00/42.53 % (383405)Instruction limit reached! % 300.00/42.53 % (383405)------------------------------ % 300.00/42.53 % (383405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.00/42.53 % (383405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819 % 300.00/42.54 Terminated % 300.00/42.54 % Vampire exiting % 300.00/42.54 Terminated %------------------------------------------------------------------------------