%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW501_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:20 PM UTC 2026 % Result : Timeout 300.15s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW501_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.17 % Computer : n008.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 14:15:54 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.62/1.51 % (2275954)Will run a generic schedule for satisfiability detection. % 8.62/1.51 % (2275965)dis+10_1_sil=32000:sp=arity:random_seed=2015537364:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.62/1.51 % (2275963)% WARNING: option uhcvi not known. % 8.62/1.51 % (2275964)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=757625109:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.62/1.51 % (2275963)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4220444637:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.62/1.51 % (2275966)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1642327328:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.62/1.51 % (2275967)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2943905903:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.62/1.51 % (2275968)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=463910512:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.62/1.51 % (2275962)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4009187274_2999 on theBenchmark for (2999ds/0Mi) % 8.62/1.51 % Exception at run slice level % 8.62/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.62/1.51 % (2275965)Instruction limit reached! % 8.62/1.51 % (2275965)------------------------------ % 8.62/1.51 % (2275965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.62/1.51 % (2275965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/1.51 % (2275965)CaDiCaL version: 2.1.3 % 8.62/1.51 % (2275965)Termination reason: Instruction limit % 8.62/1.51 % (2275965)Termination phase: Saturation % 8.62/1.51 % (2275965)Time elapsed: 0.034 s % 8.62/1.51 % (2275965)Peak memory usage: 12 MB % 8.62/1.51 % (2275965)Instructions burned: 103 (million) % 8.62/1.51 % (2275976)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1648842727:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.62/1.51 % (2275977)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3995293933:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.62/1.51 % Exception at run slice level % 8.62/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.62/1.51 % (2275980)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=1552550626:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.62/1.51 % (2275966)Instruction limit reached! % 8.62/1.51 % (2275966)------------------------------ % 8.62/1.51 % (2275966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.62/1.51 % (2275966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/1.51 % (2275966)CaDiCaL version: 2.1.3 % 8.62/1.51 % (2275966)Termination reason: Instruction limit % 8.62/1.51 % (2275966)Termination phase: Saturation % 8.62/1.51 % (2275966)Time elapsed: 0.073 s % 8.62/1.51 % (2275966)Peak memory usage: 13 MB % 8.62/1.51 % (2275966)Instructions burned: 116 (million) % 8.62/1.51 % (2275967)Instruction limit reached! % 8.62/1.51 % (2275967)------------------------------ % 8.62/1.51 % (2275967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.62/1.51 % (2275967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/1.51 % (2275967)CaDiCaL version: 2.1.3 % 8.62/1.51 % (2275967)Termination reason: Instruction limit % 8.62/1.51 % (2275967)Termination phase: Saturation % 8.62/1.51 % (2275967)Time elapsed: 0.074 s % 8.62/1.51 % (2275967)Peak memory usage: 12 MB % 8.62/1.51 % (2275967)Instructions burned: 131 (million) % 8.62/1.51 % (2275977)Instruction limit reached! % 8.62/1.51 % (2275977)------------------------------ % 8.62/1.51 % (2275977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.62/1.51 % (2275977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/1.51 % (2275977)CaDiCaL version: 2.1.3 % 8.62/1.51 % (2275977)Termination reason: Instruction limit % 8.62/1.51 % (2275977)Termination phase: Saturation % 8.62/1.51 % (2275977)Time elapsed: 0.042 s % 8.62/1.51 % (2275977)Peak memory usage: 13 MB % 8.62/1.51 % (2275977)Instructions burned: 136 (million) % 8.62/1.51 % (2275984)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=586473037:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 18.83/3.27 % Exception at run slice level % 18.83/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.83/3.27 % (2275982)ott-21_1_sil=16000:fs=off:random_seed=1524815020:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 18.83/3.27 % (2275983)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=55784951:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 18.83/3.27 % (2275968)Instruction limit reached! % 18.83/3.27 % (2275968)------------------------------ % 18.83/3.27 % (2275968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.83/3.27 % (2275968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.83/3.27 % (2275968)CaDiCaL version: 2.1.3 % 18.83/3.27 % (2275968)Termination reason: Instruction limit % 18.83/3.27 % (2275968)Termination phase: Saturation % 18.83/3.27 % (2275968)Time elapsed: 0.099 s % 18.83/3.27 % (2275968)Peak memory usage: 13 MB % 18.83/3.27 % (2275968)Instructions burned: 159 (million) % 18.83/3.27 % (2275987)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2198660623:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 18.83/3.27 % (2275989)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=455446617:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 18.83/3.27 % Exception at run slice level % 18.83/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.83/3.27 % (2275992)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=1169303360: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) % 18.83/3.27 % (2275982)Instruction limit reached! % 18.83/3.27 % (2275982)------------------------------ % 18.83/3.27 % (2275982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.83/3.27 % (2275982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.83/3.27 % (2275982)CaDiCaL version: 2.1.3 % 18.83/3.27 % (2275982)Termination reason: Instruction limit % 18.83/3.27 % (2275982)Termination phase: Saturation % 18.83/3.27 % (2275982)Time elapsed: 0.086 s % 18.83/3.27 % (2275982)Peak memory usage: 12 MB % 18.83/3.27 % (2275982)Instructions burned: 180 (million) % 18.83/3.27 % (2275994)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3831449206:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.83/3.27 % (2275980)Instruction limit reached! % 18.83/3.27 % (2275980)------------------------------ % 18.83/3.27 % (2275980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.83/3.27 % (2275980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.83/3.27 % (2275980)CaDiCaL version: 2.1.3 % 18.83/3.27 % (2275980)Termination reason: Instruction limit % 18.83/3.27 % (2275980)Termination phase: Saturation % 18.83/3.27 % (2275980)Time elapsed: 0.304 s % 18.83/3.27 % (2275980)Peak memory usage: 14 MB % 18.83/3.27 % (2275980)Instructions burned: 685 (million) % 18.83/3.27 % (2275996)fmb+10_1_sil=64000:random_seed=13120186:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.83/3.27 % (2275996)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.83/3.27 % Exception at run slice level % 18.83/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.83/3.27 % (2275983)Instruction limit reached! % 18.83/3.27 % (2275983)------------------------------ % 18.83/3.27 % (2275983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.83/3.27 % (2275983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.83/3.27 % (2275983)CaDiCaL version: 2.1.3 % 18.83/3.27 % (2275983)Termination reason: Instruction limit % 18.83/3.27 % (2275983)Termination phase: Saturation % 18.83/3.27 % (2275983)Time elapsed: 0.310 s % 18.83/3.27 % (2275983)Peak memory usage: 14 MB % 18.83/3.27 % (2275983)Instructions burned: 478 (million) % 18.83/3.27 % (2275998)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2985316284:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.83/3.27 % Exception at run slice level % 18.83/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.83/3.27 % (2276000)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1531509769:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.83/3.27 % (2276001)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3559363454:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 73.63/10.63 % Exception at run slice level % 73.63/10.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.63/10.63 % (2276004)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=140263350:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 73.63/10.63 % (2276004)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 73.63/10.63 % (2275992)Instruction limit reached! % 73.63/10.63 % (2275992)------------------------------ % 73.63/10.63 % (2275992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.63/10.63 % (2275992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.63/10.63 % (2275992)CaDiCaL version: 2.1.3 % 73.63/10.63 % (2275992)Termination reason: Instruction limit % 73.63/10.63 % (2275992)Termination phase: Saturation % 73.63/10.63 % (2275992)Time elapsed: 0.328 s % 73.63/10.63 % (2275992)Peak memory usage: 16 MB % 73.63/10.63 % (2275992)Instructions burned: 694 (million) % 73.63/10.63 % (2275987)Instruction limit reached! % 73.63/10.63 % (2275987)------------------------------ % 73.63/10.63 % (2275987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.63/10.63 % (2275987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.63/10.63 % (2275987)CaDiCaL version: 2.1.3 % 73.63/10.63 % (2275987)Termination reason: Instruction limit % 73.63/10.63 % (2275987)Termination phase: Saturation % 73.63/10.63 % (2275987)Time elapsed: 0.379 s % 73.63/10.63 % (2275987)Peak memory usage: 19 MB % 73.63/10.63 % (2275987)Instructions burned: 1180 (million) % 73.63/10.63 % (2276006)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1889786191:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 73.63/10.63 % (2276007)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2825422861:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 73.63/10.63 % Exception at run slice level % 73.63/10.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.63/10.63 % Exception at run slice level % 73.63/10.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.63/10.63 % (2276010)ott-2_1_sil=16000:newcnf=on:random_seed=2253703936:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 73.63/10.63 % (2276011)ott+10_1_sil=32000:tgt=ground:random_seed=785232385:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 73.63/10.63 % (2275994)Instruction limit reached! % 73.63/10.63 % (2275994)------------------------------ % 73.63/10.63 % (2275994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.63/10.63 % (2275994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.63/10.63 % (2275994)CaDiCaL version: 2.1.3 % 73.63/10.63 % (2275994)Termination reason: Instruction limit % 73.63/10.63 % (2275994)Termination phase: Saturation % 73.63/10.63 % (2275994)Time elapsed: 0.481 s % 73.63/10.63 % (2275994)Peak memory usage: 19 MB % 73.63/10.63 % (2275994)Instructions burned: 879 (million) % 73.63/10.63 % (2276014)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4003536606:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 73.63/10.63 % Exception at run slice level % 73.63/10.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.63/10.63 % (2276016)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3066082961:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 73.63/10.63 % (2276010)Instruction limit reached! % 73.63/10.63 % (2276010)------------------------------ % 73.63/10.63 % (2276010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.63/10.63 % (2276010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.63/10.63 % (2276010)CaDiCaL version: 2.1.3 % 73.63/10.63 % (2276010)Termination reason: Instruction limit % 73.63/10.63 % (2276010)Termination phase: Saturation % 73.63/10.63 % (2276010)Time elapsed: 0.288 s % 73.63/10.63 % (2276010)Peak memory usage: 14 MB % 73.63/10.63 % (2276010)Instructions burned: 872 (million) % 73.63/10.63 % (2276018)dis+21_1_sil=32000:sas=cadical:random_seed=1102027963:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 73.63/10.63 % (2276004)Instruction limit reached! % 73.63/10.63 % (2276004)------------------------------ % 73.63/10.63 % (2276004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.65/18.29 % (2276004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/18.29 % (2276004)CaDiCaL version: 2.1.3 % 117.65/18.29 % (2276004)Termination reason: Instruction limit % 117.65/18.29 % (2276004)Termination phase: Saturation % 117.65/18.29 % (2276004)Time elapsed: 0.807 s % 117.65/18.29 % (2276004)Peak memory usage: 30 MB % 117.65/18.29 % (2276004)Instructions burned: 1474 (million) % 117.65/18.29 % (2276020)ott+11_1_sil=16000:gs=on:random_seed=3391103126:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 117.65/18.29 % (2276011)Instruction limit reached! % 117.65/18.29 % (2276011)------------------------------ % 117.65/18.29 % (2276011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.65/18.29 % (2276011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/18.29 % (2276011)CaDiCaL version: 2.1.3 % 117.65/18.29 % (2276011)Termination reason: Instruction limit % 117.65/18.29 % (2276011)Termination phase: Saturation % 117.65/18.29 % (2276011)Time elapsed: 1.680 s % 117.65/18.29 % (2276011)Peak memory usage: 32 MB % 117.65/18.29 % (2276011)Instructions burned: 5114 (million) % 117.65/18.29 % (2276022)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=500747837:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi) % 117.65/18.29 % Exception at run slice level % 117.65/18.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.65/18.29 % (2276024)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=160754404:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi) % 117.65/18.29 % (2276020)Instruction limit reached! % 117.65/18.29 % (2276020)------------------------------ % 117.65/18.29 % (2276020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.65/18.29 % (2276020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/18.29 % (2276020)CaDiCaL version: 2.1.3 % 117.65/18.29 % (2276020)Termination reason: Instruction limit % 117.65/18.29 % (2276020)Termination phase: Saturation % 117.65/18.29 % (2276020)Time elapsed: 1.143 s % 117.65/18.29 % (2276020)Peak memory usage: 22 MB % 117.65/18.29 % (2276020)Instructions burned: 2251 (million) % 117.65/18.29 % (2276026)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3980484053:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 117.65/18.29 % (2276016)Instruction limit reached! % 117.65/18.29 % (2276016)------------------------------ % 117.65/18.29 % (2276016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.65/18.29 % (2276016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/18.29 % (2276016)CaDiCaL version: 2.1.3 % 117.65/18.29 % (2276016)Termination reason: Instruction limit % 117.65/18.29 % (2276016)Termination phase: Saturation % 117.65/18.29 % (2276016)Time elapsed: 2.076 s % 117.65/18.29 % (2276016)Peak memory usage: 27 MB % 117.65/18.29 % (2276016)Instructions burned: 3513 (million) % 117.65/18.29 % (2276028)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1335826371:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 117.65/18.29 % (2276018)Instruction limit reached! % 117.65/18.29 % (2276018)------------------------------ % 117.65/18.29 % (2276018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.65/18.29 % (2276018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/18.29 % (2276018)CaDiCaL version: 2.1.3 % 117.65/18.29 % (2276018)Termination reason: Instruction limit % 117.65/18.29 % (2276018)Termination phase: Saturation % 117.65/18.29 % (2276018)Time elapsed: 2.122 s % 117.65/18.29 % (2276018)Peak memory usage: 29 MB % 117.65/18.29 % (2276018)Instructions burned: 3774 (million) % 117.65/18.29 % (2276030)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=255144579:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 117.65/18.29 % Exception at run slice level % 117.65/18.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.65/18.29 % (2276032)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=73014042:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 117.65/18.29 % Exception at run slice level % 117.65/18.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.65/18.29 % (2276034)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=680225500:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 117.65/18.29 % Exception at run slice level % 155.87/22.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 155.87/22.20 % (2276036)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=605410170:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 155.87/22.20 % (2276001)Instruction limit reached! % 155.87/22.20 % (2276001)------------------------------ % 155.87/22.20 % (2276001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276001)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276001)Termination reason: Instruction limit % 155.87/22.20 % (2276001)Termination phase: Saturation % 155.87/22.20 % (2276001)Time elapsed: 2.939 s % 155.87/22.20 % (2276001)Peak memory usage: 33 MB % 155.87/22.20 % (2276001)Instructions burned: 5132 (million) % 155.87/22.20 % (2276038)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1412890295:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 155.87/22.20 % (2276024)Instruction limit reached! % 155.87/22.20 % (2276024)------------------------------ % 155.87/22.20 % (2276024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276024)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276024)Termination reason: Instruction limit % 155.87/22.20 % (2276024)Termination phase: Saturation % 155.87/22.20 % (2276024)Time elapsed: 1.376 s % 155.87/22.20 % (2276024)Peak memory usage: 54 MB % 155.87/22.20 % (2276024)Instructions burned: 4591 (million) % 155.87/22.20 % (2276040)dis+10_16:1_sil=16000:random_seed=3900621440:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 155.87/22.20 % (2276028)Instruction limit reached! % 155.87/22.20 % (2276028)------------------------------ % 155.87/22.20 % (2276028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276028)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276028)Termination reason: Instruction limit % 155.87/22.20 % (2276028)Termination phase: Saturation % 155.87/22.20 % (2276028)Time elapsed: 2.745 s % 155.87/22.20 % (2276028)Peak memory usage: 47 MB % 155.87/22.20 % (2276028)Instructions burned: 5211 (million) % 155.87/22.20 % (2276042)ott-3_8_sil=64000:random_seed=896735124:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 155.87/22.20 % (2276040)Instruction limit reached! % 155.87/22.20 % (2276040)------------------------------ % 155.87/22.20 % (2276040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276040)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276040)Termination reason: Instruction limit % 155.87/22.20 % (2276040)Termination phase: Saturation % 155.87/22.20 % (2276040)Time elapsed: 2.652 s % 155.87/22.20 % (2276040)Peak memory usage: 68 MB % 155.87/22.20 % (2276040)Instructions burned: 9157 (million) % 155.87/22.20 % (2276044)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1586919447:fmbsr=2:i=32576_2936 on theBenchmark for (2936ds/32576Mi) % 155.87/22.20 % Exception at run slice level % 155.87/22.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 155.87/22.20 % (2276046)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2900648785:i=11404_2936 on theBenchmark for (2936ds/11404Mi) % 155.87/22.20 % (2276038)Instruction limit reached! % 155.87/22.20 % (2276038)------------------------------ % 155.87/22.20 % (2276038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276038)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276038)Termination reason: Instruction limit % 155.87/22.20 % (2276038)Termination phase: Saturation % 155.87/22.20 % (2276038)Time elapsed: 4.680 s % 155.87/22.20 % (2276038)Peak memory usage: 65 MB % 155.87/22.20 % (2276038)Instructions burned: 8173 (million) % 155.87/22.20 % (2276048)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2353834375:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 155.87/22.20 % (2276046)Instruction limit reached! % 155.87/22.20 % (2276046)------------------------------ % 155.87/22.20 % (2276046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.87/22.20 % (2276046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.87/22.20 % (2276046)CaDiCaL version: 2.1.3 % 155.87/22.20 % (2276046)Termination reason: Instruction limit % 169.75/24.16 % (2276046)Termination phase: Saturation % 169.75/24.16 % (2276046)Time elapsed: 4.066 s % 169.75/24.16 % (2276046)Peak memory usage: 76 MB % 169.75/24.16 % (2276046)Instructions burned: 11406 (million) % 169.75/24.16 % (2276050)dis+33_16_sil=32000:sac=on:random_seed=1278328427:i=15851:nm=0_2895 on theBenchmark for (2895ds/15851Mi) % 169.75/24.16 % (2276036)Instruction limit reached! % 169.75/24.16 % (2276036)------------------------------ % 169.75/24.16 % (2276036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.75/24.16 % (2276036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.75/24.16 % (2276036)CaDiCaL version: 2.1.3 % 169.75/24.16 % (2276036)Termination reason: Instruction limit % 169.75/24.16 % (2276036)Termination phase: Saturation % 169.75/24.16 % (2276036)Time elapsed: 7.395 s % 169.75/24.16 % (2276036)Peak memory usage: 56 MB % 169.75/24.16 % (2276036)Instructions burned: 22566 (million) % 169.75/24.16 % (2276052)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1244093178:avsq=on:i=17627:add=on:amm=off_2895 on theBenchmark for (2895ds/17627Mi) % 169.75/24.16 % (2276050)Instruction limit reached! % 169.75/24.16 % (2276050)------------------------------ % 169.75/24.16 % (2276050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.75/24.16 % (2276050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.75/24.16 % (2276050)CaDiCaL version: 2.1.3 % 169.75/24.16 % (2276050)Termination reason: Instruction limit % 169.75/24.16 % (2276050)Termination phase: Saturation % 169.75/24.16 % (2276050)Time elapsed: 4.632 s % 169.75/24.16 % (2276050)Peak memory usage: 82 MB % 169.75/24.16 % (2276050)Instructions burned: 15854 (million) % 169.75/24.16 % (2276296)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2126134331:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 169.75/24.16 % (2276026)Instruction limit reached! % 169.75/24.16 % (2276026)------------------------------ % 169.75/24.16 % (2276026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.75/24.16 % (2276026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.75/24.16 % (2276026)CaDiCaL version: 2.1.3 % 169.75/24.16 % (2276026)Termination reason: Instruction limit % 169.75/24.16 % (2276026)Termination phase: Saturation % 169.75/24.16 % (2276026)Time elapsed: 13.844 s % 169.75/24.16 % (2276026)Peak memory usage: 283 MB % 169.75/24.16 % (2276026)Instructions burned: 29340 (million) % 169.75/24.16 % (2276331)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=745225113:i=26857:ins=20_2836 on theBenchmark for (2836ds/26857Mi) % 169.75/24.16 % Exception at run slice level % 169.75/24.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.75/24.16 % (2276335)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1891702919:i=28120:bs=on:fsr=off_2835 on theBenchmark for (2835ds/28120Mi) % 169.75/24.16 % (2276048)Instruction limit reached! % 169.75/24.16 % (2276048)------------------------------ % 169.75/24.16 % (2276048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.75/24.16 % (2276048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.75/24.16 % (2276048)CaDiCaL version: 2.1.3 % 169.75/24.16 % (2276048)Termination reason: Instruction limit % 169.75/24.16 % (2276048)Termination phase: Saturation % 169.75/24.16 % (2276048)Time elapsed: 9.843 s % 169.75/24.16 % (2276048)Peak memory usage: 77 MB % 169.75/24.16 % (2276048)Instructions burned: 14135 (million) % 169.75/24.16 % (2276463)fmb+10_1_sil=256000:fmbss=7:random_seed=3297019924:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 169.75/24.16 % Exception at run slice level % 169.75/24.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.75/24.16 % (2276477)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1469956527:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 169.75/24.16 % (2276477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 169.75/24.16 % Exception at run slice level % 169.75/24.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.75/24.16 % (2276492)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2982697301:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 169.75/24.16 % Exception at run slice level % 169.75/24.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.75/24.16 % (2276503)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=48144075:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 188.21/27.02 % Exception at run slice level % 188.21/27.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 188.21/27.02 % (2276511)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3851416373:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 188.21/27.02 % Exception at run slice level % 188.21/27.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 188.21/27.02 % (2276513)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3878426869:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 188.21/27.02 % Exception at run slice level % 188.21/27.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 188.21/27.02 % (2276515)% WARNING: option uhcvi not known. % 188.21/27.02 % (2276515)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=957826798:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 188.21/27.02 % (2276042)Instruction limit reached! % 188.21/27.02 % (2276042)------------------------------ % 188.21/27.02 % (2276042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.21/27.02 % (2276042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.21/27.02 % (2276042)CaDiCaL version: 2.1.3 % 188.21/27.02 % (2276042)Termination reason: Instruction limit % 188.21/27.02 % (2276042)Termination phase: Saturation % 188.21/27.02 % (2276042)Time elapsed: 13.343 s % 188.21/27.02 % (2276042)Peak memory usage: 50 MB % 188.21/27.02 % (2276042)Instructions burned: 20139 (million) % 188.21/27.02 % (2276517)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=759206559:i=176048:add=on:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/176048Mi) % 188.21/27.02 % (2276052)Instruction limit reached! % 188.21/27.02 % (2276052)------------------------------ % 188.21/27.02 % (2276052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.21/27.02 % (2276052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.21/27.02 % (2276052)CaDiCaL version: 2.1.3 % 188.21/27.02 % (2276052)Termination reason: Instruction limit % 188.21/27.02 % (2276052)Termination phase: Saturation % 188.21/27.02 % (2276052)Time elapsed: 10.969 s % 188.21/27.02 % (2276052)Peak memory usage: 223 MB % 188.21/27.02 % (2276052)Instructions burned: 17628 (million) % 188.21/27.02 % (2276519)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2876660728:i=206:fgj=on:rtra=on_2785 on theBenchmark for (2785ds/206Mi) % 188.21/27.02 % (2276519)Instruction limit reached! % 188.21/27.02 % (2276519)------------------------------ % 188.21/27.02 % (2276519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.21/27.02 % (2276519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.21/27.02 % (2276519)CaDiCaL version: 2.1.3 % 188.21/27.02 % (2276519)Termination reason: Instruction limit % 188.21/27.02 % (2276519)Termination phase: Saturation % 188.21/27.02 % (2276519)Time elapsed: 0.123 s % 188.21/27.02 % (2276519)Peak memory usage: 13 MB % 188.21/27.02 % (2276519)Instructions burned: 206 (million) % 188.21/27.02 % (2276521)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1998414480:i=232:rtra=on_2783 on theBenchmark for (2783ds/232Mi) % 188.21/27.02 % (2276521)Instruction limit reached! % 188.21/27.02 % (2276521)------------------------------ % 188.21/27.02 % (2276521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.21/27.02 % (2276521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.21/27.02 % (2276521)CaDiCaL version: 2.1.3 % 188.21/27.02 % (2276521)Termination reason: Instruction limit % 188.21/27.02 % (2276521)Termination phase: Saturation % 188.21/27.02 % (2276521)Time elapsed: 0.153 s % 188.21/27.02 % (2276521)Peak memory usage: 14 MB % 188.21/27.02 % (2276521)Instructions burned: 233 (million) % 188.21/27.02 % (2276523)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1940046460:i=262:rtra=on_2781 on theBenchmark for (2781ds/262Mi) % 188.21/27.02 % (2276523)Instruction limit reached! % 188.21/27.02 % (2276523)------------------------------ % 188.21/27.02 % (2276523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.21/27.02 % (2276523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.21/27.02 % (2276523)CaDiCaL version: 2.1.3 % 188.21/27.02 % (2276523)Termination reason: Instruction limit % 188.21/27.02 % (2276523)Termination phase: Saturation % 232.95/33.07 % (2276523)Time elapsed: 0.160 s % 232.95/33.07 % (2276523)Peak memory usage: 14 MB % 232.95/33.07 % (2276523)Instructions burned: 262 (million) % 232.95/33.07 % (2276525)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2961997180:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2780 on theBenchmark for (2780ds/318Mi) % 232.95/33.07 % (2276525)Instruction limit reached! % 232.95/33.07 % (2276525)------------------------------ % 232.95/33.07 % (2276525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.95/33.07 % (2276525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.95/33.07 % (2276525)CaDiCaL version: 2.1.3 % 232.95/33.07 % (2276525)Termination reason: Instruction limit % 232.95/33.07 % (2276525)Termination phase: Saturation % 232.95/33.07 % (2276525)Time elapsed: 0.164 s % 232.95/33.07 % (2276525)Peak memory usage: 13 MB % 232.95/33.07 % (2276525)Instructions burned: 318 (million) % 232.95/33.07 % (2276527)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1382452225:i=1428:nm=2:rtra=on_2778 on theBenchmark for (2778ds/1428Mi) % 232.95/33.07 % Exception at run slice level % 232.95/33.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 232.95/33.07 % (2276529)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1931607176:i=262:bd=preordered:rtra=on:fsd=on_2778 on theBenchmark for (2778ds/262Mi) % 232.95/33.07 % (2276529)Instruction limit reached! % 232.95/33.07 % (2276529)------------------------------ % 232.95/33.07 % (2276529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.95/33.07 % (2276529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.95/33.07 % (2276529)CaDiCaL version: 2.1.3 % 232.95/33.07 % (2276529)Termination reason: Instruction limit % 232.95/33.07 % (2276529)Termination phase: Saturation % 232.95/33.07 % (2276529)Time elapsed: 0.163 s % 232.95/33.07 % (2276529)Peak memory usage: 14 MB % 232.95/33.07 % (2276529)Instructions burned: 263 (million) % 232.95/33.07 % (2276531)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=2963484001:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/1368Mi) % 232.95/33.07 % (2276531)Instruction limit reached! % 232.95/33.07 % (2276531)------------------------------ % 232.95/33.07 % (2276531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.95/33.07 % (2276531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.95/33.07 % (2276531)CaDiCaL version: 2.1.3 % 232.95/33.07 % (2276531)Termination reason: Instruction limit % 232.95/33.07 % (2276531)Termination phase: Saturation % 232.95/33.07 % (2276531)Time elapsed: 0.731 s % 232.95/33.07 % (2276531)Peak memory usage: 20 MB % 232.95/33.07 % (2276531)Instructions burned: 1369 (million) % 232.95/33.07 % (2276533)ott-21_1_sil=16000:si=on:fs=off:random_seed=1875208024:i=360:av=off:fsr=off:rtra=on_2768 on theBenchmark for (2768ds/360Mi) % 232.95/33.07 % (2276533)Instruction limit reached! % 232.95/33.07 % (2276533)------------------------------ % 232.95/33.07 % (2276533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.95/33.07 % (2276533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.95/33.07 % (2276533)CaDiCaL version: 2.1.3 % 232.95/33.07 % (2276533)Termination reason: Instruction limit % 232.95/33.07 % (2276533)Termination phase: Saturation % 232.95/33.07 % (2276533)Time elapsed: 0.177 s % 232.95/33.07 % (2276533)Peak memory usage: 13 MB % 232.95/33.07 % (2276533)Instructions burned: 360 (million) % 232.95/33.07 % (2276535)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2690200490:i=954:bd=all:rtra=on_2766 on theBenchmark for (2766ds/954Mi) % 232.95/33.07 % (2276535)Instruction limit reached! % 232.95/33.07 % (2276535)------------------------------ % 232.95/33.07 % (2276535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.95/33.07 % (2276535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.95/33.07 % (2276535)CaDiCaL version: 2.1.3 % 232.95/33.07 % (2276535)Termination reason: Instruction limit % 232.95/33.07 % (2276535)Termination phase: Saturation % 232.95/33.07 % (2276535)Time elapsed: 0.569 s % 232.95/33.07 % (2276535)Peak memory usage: 15 MB % 232.95/33.07 % (2276535)Instructions burned: 955 (million) % 232.95/33.07 % (2276537)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1081926336:fmbsr=1.3:i=1730:ins=25:rtra=on_2760 on theBenchmark for (2760ds/1730Mi) % 232.95/33.07 % Exception at run slice level % 232.95/33.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.67/36.90 % (2276539)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4055153787:i=2358:rtra=on_2760 on theBenchmark for (2760ds/2358Mi) % 259.67/36.90 % (2276539)Instruction limit reached! % 259.67/36.90 % (2276539)------------------------------ % 259.67/36.90 % (2276539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.67/36.90 % (2276539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.67/36.90 % (2276539)CaDiCaL version: 2.1.3 % 259.67/36.90 % (2276539)Termination reason: Instruction limit % 259.67/36.90 % (2276539)Termination phase: Saturation % 259.67/36.90 % (2276539)Time elapsed: 1.620 s % 259.67/36.90 % (2276539)Peak memory usage: 24 MB % 259.67/36.90 % (2276539)Instructions burned: 2358 (million) % 259.67/36.90 % (2276541)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=35074204:i=1778:ins=1:rtra=on_2744 on theBenchmark for (2744ds/1778Mi) % 259.67/36.90 % Exception at run slice level % 259.67/36.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.67/36.90 % (2276543)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=219717019:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1384Mi) % 259.67/36.90 % (2275964)Instruction limit reached! % 259.67/36.90 % (2275964)------------------------------ % 259.67/36.90 % (2275964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.67/36.90 % (2275964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.67/36.90 % (2275964)CaDiCaL version: 2.1.3 % 259.67/36.90 % (2275964)Termination reason: Instruction limit % 259.67/36.90 % (2275964)Termination phase: Saturation % 259.67/36.90 % (2275964)Time elapsed: 25.737 s % 259.67/36.90 % (2275964)Peak memory usage: 81 MB % 259.67/36.90 % (2275964)Instructions burned: 88027 (million) % 259.67/36.90 % (2276545)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1536165715:i=1758:kws=inv_precedence:fsr=off:rtra=on_2742 on theBenchmark for (2742ds/1758Mi) % 259.67/36.90 % (2276543)Instruction limit reached! % 259.67/36.90 % (2276543)------------------------------ % 259.67/36.90 % (2276543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.67/36.90 % (2276543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.67/36.90 % (2276543)CaDiCaL version: 2.1.3 % 259.67/36.90 % (2276543)Termination reason: Instruction limit % 259.67/36.90 % (2276543)Termination phase: Saturation % 259.67/36.90 % (2276543)Time elapsed: 0.674 s % 259.67/36.90 % (2276543)Peak memory usage: 22 MB % 259.67/36.90 % (2276543)Instructions burned: 1385 (million) % 259.67/36.90 % (2276547)fmb+10_1_sil=64000:si=on:random_seed=3439052700:i=44122:nm=2:rtra=on:gsp=on_2736 on theBenchmark for (2736ds/44122Mi) % 259.67/36.90 % (2276547)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 259.67/36.90 % Exception at run slice level % 259.67/36.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.67/36.90 % (2276549)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1823635642:i=19030:nm=5:rtra=on_2736 on theBenchmark for (2736ds/19030Mi) % 259.67/36.90 % Exception at run slice level % 259.67/36.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.67/36.90 % (2276551)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=135500666:fmbsr=1.7:i=1840:rtra=on_2736 on theBenchmark for (2736ds/1840Mi) % 259.67/36.90 % Exception at run slice level % 259.67/36.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.67/36.90 % (2276553)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3744343980:i=10262:rtra=on_2736 on theBenchmark for (2736ds/10262Mi) % 259.67/36.90 % (2276545)Instruction limit reached! % 259.67/36.90 % (2276545)------------------------------ % 259.67/36.90 % (2276545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.67/36.90 % (2276545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.67/36.90 % (2276545)CaDiCaL version: 2.1.3 % 259.67/36.90 % (2276545)Termination reason: Instruction limit % 259.67/36.90 % (2276545)Termination phase: Saturation % 259.67/36.90 % (2276545)Time elapsed: 0.999 s % 259.67/36.90 % (2276545)Peak memory usage: 26 MB % 259.67/36.90 % (2276545)Instructions burned: 1758 (million) % 300.15/42.54 % (2276555)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1422119111:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2731 on theBenchmark for (2731ds/2944Mi) % 300.15/42.54 % (2276555)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.15/42.54 % (2276555)Instruction limit reached! % 300.15/42.54 % (2276555)------------------------------ % 300.15/42.54 % (2276555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276555)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276555)Termination reason: Instruction limit % 300.15/42.54 % (2276555)Termination phase: Saturation % 300.15/42.54 % (2276555)Time elapsed: 1.777 s % 300.15/42.54 % (2276555)Peak memory usage: 48 MB % 300.15/42.54 % (2276555)Instructions burned: 2944 (million) % 300.15/42.54 % (2276557)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3973948338:i=12648:rtra=on_2713 on theBenchmark for (2713ds/12648Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276559)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=338827744:fmbsr=2.30978:i=4348:rtra=on_2713 on theBenchmark for (2713ds/4348Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276561)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1790432318:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2713 on theBenchmark for (2713ds/1738Mi) % 300.15/42.54 % (2276296)Instruction limit reached! % 300.15/42.54 % (2276296)------------------------------ % 300.15/42.54 % (2276296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276296)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276296)Termination reason: Instruction limit % 300.15/42.54 % (2276296)Termination phase: Saturation % 300.15/42.54 % (2276296)Time elapsed: 14.072 s % 300.15/42.54 % (2276296)Peak memory usage: 239 MB % 300.15/42.54 % (2276296)Instructions burned: 53301 (million) % 300.15/42.54 % (2276656)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1147241384:i=10228:av=off:rtra=on_2708 on theBenchmark for (2708ds/10228Mi) % 300.15/42.54 % (2276561)Instruction limit reached! % 300.15/42.54 % (2276561)------------------------------ % 300.15/42.54 % (2276561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276561)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276561)Termination reason: Instruction limit % 300.15/42.54 % (2276561)Termination phase: Saturation % 300.15/42.54 % (2276561)Time elapsed: 1.108 s % 300.15/42.54 % (2276561)Peak memory usage: 19 MB % 300.15/42.54 % (2276561)Instructions burned: 1739 (million) % 300.15/42.54 % (2276801)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3488810919:i=108564:rtra=on_2702 on theBenchmark for (2702ds/108564Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276813)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=256791320:i=7024:aac=none:rtra=on_2701 on theBenchmark for (2701ds/7024Mi) % 300.15/42.54 % (2276335)Instruction limit reached! % 300.15/42.54 % (2276335)------------------------------ % 300.15/42.54 % (2276335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276335)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276335)Termination reason: Instruction limit % 300.15/42.54 % (2276335)Termination phase: Saturation % 300.15/42.54 % (2276335)Time elapsed: 15.900 s % 300.15/42.54 % (2276335)Peak memory usage: 340 MB % 300.15/42.54 % (2276335)Instructions burned: 28120 (million) % 300.15/42.54 % (2276913)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4006862827:i=7546:rtra=on:amm=off_2675 on theBenchmark for (2675ds/7546Mi) % 300.15/42.54 % (2276656)Instruction limit reached! % 300.15/42.54 % (2276656)------------------------------ % 300.15/42.54 % (2276656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276656)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276656)Termination reason: Instruction limit % 300.15/42.54 % (2276656)Termination phase: Saturation % 300.15/42.54 % (2276656)Time elapsed: 3.665 s % 300.15/42.54 % (2276656)Peak memory usage: 49 MB % 300.15/42.54 % (2276656)Instructions burned: 10228 (million) % 300.15/42.54 % (2276553)Instruction limit reached! % 300.15/42.54 % (2276553)------------------------------ % 300.15/42.54 % (2276553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276553)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276553)Termination reason: Instruction limit % 300.15/42.54 % (2276553)Termination phase: Saturation % 300.15/42.54 % (2276553)Time elapsed: 6.452 s % 300.15/42.54 % (2276553)Peak memory usage: 50 MB % 300.15/42.54 % (2276553)Instructions burned: 10262 (million) % 300.15/42.54 % (2276915)ott+11_1_sil=16000:si=on:gs=on:random_seed=41372057:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2671 on theBenchmark for (2671ds/4502Mi) % 300.15/42.54 % (2276916)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3178565356:fmbsr=1.6:i=135068:rtra=on_2671 on theBenchmark for (2671ds/135068Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276919)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3254363982:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2671 on theBenchmark for (2671ds/9182Mi) % 300.15/42.54 % (2276915)Instruction limit reached! % 300.15/42.54 % (2276915)------------------------------ % 300.15/42.54 % (2276915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276915)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276915)Termination reason: Instruction limit % 300.15/42.54 % (2276915)Termination phase: Saturation % 300.15/42.54 % (2276915)Time elapsed: 1.167 s % 300.15/42.54 % (2276915)Peak memory usage: 25 MB % 300.15/42.54 % (2276915)Instructions burned: 4506 (million) % 300.15/42.54 % (2276921)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=3812718280:i=58680:rtra=on_2659 on theBenchmark for (2659ds/58680Mi) % 300.15/42.54 % (2276813)Instruction limit reached! % 300.15/42.54 % (2276813)------------------------------ % 300.15/42.54 % (2276813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276813)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276813)Termination reason: Instruction limit % 300.15/42.54 % (2276813)Termination phase: Saturation % 300.15/42.54 % (2276813)Time elapsed: 4.360 s % 300.15/42.54 % (2276813)Peak memory usage: 43 MB % 300.15/42.54 % (2276813)Instructions burned: 7025 (million) % 300.15/42.54 % (2276923)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3198060872:i=10422:rtra=on_2657 on theBenchmark for (2657ds/10422Mi) % 300.15/42.54 % (2276913)Instruction limit reached! % 300.15/42.54 % (2276913)------------------------------ % 300.15/42.54 % (2276913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.54 % (2276913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.54 % (2276913)CaDiCaL version: 2.1.3 % 300.15/42.54 % (2276913)Termination reason: Instruction limit % 300.15/42.54 % (2276913)Termination phase: Saturation % 300.15/42.54 % (2276913)Time elapsed: 4.172 s % 300.15/42.54 % (2276913)Peak memory usage: 41 MB % 300.15/42.54 % (2276913)Instructions burned: 7546 (million) % 300.15/42.54 % (2276925)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=2031353399:i=10994:nm=2:rtra=on_2633 on theBenchmark for (2633ds/10994Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276927)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=3995190858:fmbsr=2:i=92664:rtra=on_2633 on theBenchmark for (2633ds/92664Mi) % 300.15/42.54 % Exception at run slice level % 300.15/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.15/42.54 % (2276929)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=2828957928:i=28142:rtra=on_2633 on theBe % 300.15/42.54 Terminated % 300.15/42.54 % Vampire exiting %------------------------------------------------------------------------------