%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW511_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 : n017.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:22 PM UTC 2026 % Result : Timeout 300.21s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW511_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n017.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:12:34 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 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 % 7.07/1.38 % (3577990)Will run a generic schedule for satisfiability detection. % 7.07/1.38 % (3578011)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=420772074:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.07/1.38 % (3578008)% WARNING: option uhcvi not known. % 7.07/1.38 % (3578007)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2064444542_2999 on theBenchmark for (2999ds/0Mi) % 7.07/1.38 % (3578008)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2501254993:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.07/1.38 % (3578012)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3593690747:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.07/1.38 % (3578010)dis+10_1_sil=32000:sp=arity:random_seed=1044366439:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.07/1.38 % (3578009)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=73829123:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.07/1.38 % (3578014)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1731954033:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.07/1.38 % Exception at run slice level % 7.07/1.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.07/1.38 % (3578029)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1914839068:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.07/1.38 % (3578011)Instruction limit reached! % 7.07/1.38 % (3578011)------------------------------ % 7.07/1.38 % (3578011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.38 % (3578011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.38 % (3578011)CaDiCaL version: 2.1.3 % 7.07/1.38 % (3578011)Termination reason: Instruction limit % 7.07/1.38 % (3578011)Termination phase: Saturation % 7.07/1.38 % (3578011)Time elapsed: 0.038 s % 7.07/1.38 % (3578011)Peak memory usage: 12 MB % 7.07/1.38 % (3578011)Instructions burned: 116 (million) % 7.07/1.38 % Exception at run slice level % 7.07/1.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.07/1.38 % (3578043)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1027411972:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.07/1.38 % (3578010)Instruction limit reached! % 7.07/1.38 % (3578010)------------------------------ % 7.07/1.38 % (3578010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.38 % (3578010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.38 % (3578010)CaDiCaL version: 2.1.3 % 7.07/1.38 % (3578010)Termination reason: Instruction limit % 7.07/1.38 % (3578010)Termination phase: Saturation % 7.07/1.38 % (3578010)Time elapsed: 0.052 s % 7.07/1.38 % (3578010)Peak memory usage: 12 MB % 7.07/1.38 % (3578010)Instructions burned: 103 (million) % 7.07/1.38 % (3578050)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=2686120613:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.07/1.38 % (3578060)ott-21_1_sil=16000:fs=off:random_seed=2549815602:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.07/1.38 % (3578012)Instruction limit reached! % 7.07/1.38 % (3578012)------------------------------ % 7.07/1.38 % (3578012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.38 % (3578012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.38 % (3578012)CaDiCaL version: 2.1.3 % 7.07/1.38 % (3578012)Termination reason: Instruction limit % 7.07/1.38 % (3578012)Termination phase: Saturation % 7.07/1.38 % (3578012)Time elapsed: 0.075 s % 7.07/1.38 % (3578012)Peak memory usage: 12 MB % 7.07/1.38 % (3578012)Instructions burned: 132 (million) % 7.07/1.38 % (3578043)Instruction limit reached! % 7.07/1.38 % (3578043)------------------------------ % 7.07/1.38 % (3578043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.38 % (3578043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.38 % (3578043)CaDiCaL version: 2.1.3 % 7.07/1.38 % (3578043)Termination reason: Instruction limit % 7.07/1.38 % (3578043)Termination phase: Saturation % 7.07/1.38 % (3578043)Time elapsed: 0.042 s % 7.07/1.38 % (3578043)Peak memory usage: 12 MB % 7.07/1.38 % (3578043)Instructions burned: 132 (million) % 7.07/1.38 % (3578014)Instruction limit reached! % 19.75/3.08 % (3578014)------------------------------ % 19.75/3.08 % (3578014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.08 % (3578014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.08 % (3578014)CaDiCaL version: 2.1.3 % 19.75/3.08 % (3578014)Termination reason: Instruction limit % 19.75/3.08 % (3578014)Termination phase: Saturation % 19.75/3.08 % (3578014)Time elapsed: 0.083 s % 19.75/3.08 % (3578014)Peak memory usage: 12 MB % 19.75/3.08 % (3578014)Instructions burned: 160 (million) % 19.75/3.08 % (3578071)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3684868532:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.75/3.08 % (3578076)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4176697955:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.75/3.08 % Exception at run slice level % 19.75/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.08 % (3578077)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1859177057:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.75/3.08 % (3578080)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3319413140:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.75/3.08 % Exception at run slice level % 19.75/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.08 % (3578083)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=1106569507: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) % 19.75/3.08 % (3578060)Instruction limit reached! % 19.75/3.08 % (3578060)------------------------------ % 19.75/3.08 % (3578060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.08 % (3578060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.08 % (3578060)CaDiCaL version: 2.1.3 % 19.75/3.08 % (3578060)Termination reason: Instruction limit % 19.75/3.08 % (3578060)Termination phase: Saturation % 19.75/3.08 % (3578060)Time elapsed: 0.097 s % 19.75/3.08 % (3578060)Peak memory usage: 13 MB % 19.75/3.08 % (3578060)Instructions burned: 182 (million) % 19.75/3.08 % (3578085)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3988050435:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.75/3.08 % (3578083)Instruction limit reached! % 19.75/3.08 % (3578083)------------------------------ % 19.75/3.08 % (3578083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.08 % (3578083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.08 % (3578083)CaDiCaL version: 2.1.3 % 19.75/3.08 % (3578083)Termination reason: Instruction limit % 19.75/3.08 % (3578083)Termination phase: Saturation % 19.75/3.08 % (3578083)Time elapsed: 0.221 s % 19.75/3.08 % (3578083)Peak memory usage: 17 MB % 19.75/3.08 % (3578083)Instructions burned: 695 (million) % 19.75/3.08 % (3578087)fmb+10_1_sil=64000:random_seed=122976480:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 19.75/3.08 % (3578071)Instruction limit reached! % 19.75/3.08 % (3578071)------------------------------ % 19.75/3.08 % (3578071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.08 % (3578071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.08 % (3578071)CaDiCaL version: 2.1.3 % 19.75/3.08 % (3578071)Termination reason: Instruction limit % 19.75/3.08 % (3578071)Termination phase: Saturation % 19.75/3.08 % (3578071)Time elapsed: 0.275 s % 19.75/3.08 % (3578071)Peak memory usage: 13 MB % 19.75/3.08 % (3578071)Instructions burned: 478 (million) % 19.75/3.08 % (3578087)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.75/3.08 % Exception at run slice level % 19.75/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.08 % (3578090)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=652668136:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.75/3.08 % Exception at run slice level % 19.75/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.08 % (3578050)Instruction limit reached! % 19.75/3.08 % (3578050)------------------------------ % 19.75/3.08 % (3578050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.24/9.36 % (3578050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.24/9.36 % (3578050)CaDiCaL version: 2.1.3 % 64.24/9.36 % (3578050)Termination reason: Instruction limit % 64.24/9.36 % (3578050)Termination phase: Saturation % 64.24/9.36 % (3578050)Time elapsed: 0.330 s % 64.24/9.36 % (3578050)Peak memory usage: 14 MB % 64.24/9.36 % (3578050)Instructions burned: 685 (million) % 64.24/9.36 % (3578089)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1218438244:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 64.24/9.36 % (3578092)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=922167563:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 64.24/9.36 % Exception at run slice level % 64.24/9.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.24/9.36 % (3578094)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=571636246:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 64.24/9.36 % (3578094)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.24/9.36 % (3578096)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=78450009:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 64.24/9.36 % Exception at run slice level % 64.24/9.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.24/9.36 % (3578099)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1055818515:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 64.24/9.36 % Exception at run slice level % 64.24/9.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.24/9.36 % (3578101)ott-2_1_sil=16000:newcnf=on:random_seed=1588910533:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 64.24/9.36 % (3578085)Instruction limit reached! % 64.24/9.36 % (3578085)------------------------------ % 64.24/9.36 % (3578085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.24/9.36 % (3578085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.24/9.36 % (3578085)CaDiCaL version: 2.1.3 % 64.24/9.36 % (3578085)Termination reason: Instruction limit % 64.24/9.36 % (3578085)Termination phase: Saturation % 64.24/9.36 % (3578085)Time elapsed: 0.494 s % 64.24/9.36 % (3578085)Peak memory usage: 18 MB % 64.24/9.36 % (3578085)Instructions burned: 880 (million) % 64.24/9.36 % (3578103)ott+10_1_sil=32000:tgt=ground:random_seed=3325945079:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.24/9.36 % (3578077)Instruction limit reached! % 64.24/9.36 % (3578077)------------------------------ % 64.24/9.36 % (3578077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.24/9.36 % (3578077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.24/9.36 % (3578077)CaDiCaL version: 2.1.3 % 64.24/9.36 % (3578077)Termination reason: Instruction limit % 64.24/9.36 % (3578077)Termination phase: Saturation % 64.24/9.36 % (3578077)Time elapsed: 0.606 s % 64.24/9.36 % (3578077)Peak memory usage: 16 MB % 64.24/9.36 % (3578077)Instructions burned: 1179 (million) % 64.24/9.36 % (3578105)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4145271124:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 64.24/9.36 % Exception at run slice level % 64.24/9.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.24/9.36 % (3578107)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=529193508:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 64.24/9.36 % (3578101)Instruction limit reached! % 64.24/9.36 % (3578101)------------------------------ % 64.24/9.36 % (3578101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.24/9.36 % (3578101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.24/9.36 % (3578101)CaDiCaL version: 2.1.3 % 64.24/9.36 % (3578101)Termination reason: Instruction limit % 64.24/9.36 % (3578101)Termination phase: Saturation % 64.24/9.36 % (3578101)Time elapsed: 0.423 s % 64.24/9.36 % (3578101)Peak memory usage: 14 MB % 64.24/9.36 % (3578101)Instructions burned: 870 (million) % 64.24/9.36 % (3578109)dis+21_1_sil=32000:sas=cadical:random_seed=4222216604:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 64.24/9.36 % (3578094)Instruction limit reached! % 64.24/9.36 % (3578094)------------------------------ % 64.24/9.36 % (3578094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.34/16.58 % (3578094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.34/16.58 % (3578094)CaDiCaL version: 2.1.3 % 115.34/16.58 % (3578094)Termination reason: Instruction limit % 115.34/16.58 % (3578094)Termination phase: Saturation % 115.34/16.58 % (3578094)Time elapsed: 0.686 s % 115.34/16.58 % (3578094)Peak memory usage: 18 MB % 115.34/16.58 % (3578094)Instructions burned: 1472 (million) % 115.34/16.58 % (3578111)ott+11_1_sil=16000:gs=on:random_seed=587093460:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 115.34/16.58 % (3578092)Instruction limit reached! % 115.34/16.58 % (3578092)------------------------------ % 115.34/16.58 % (3578092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.34/16.58 % (3578092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.34/16.58 % (3578092)CaDiCaL version: 2.1.3 % 115.34/16.58 % (3578092)Termination reason: Instruction limit % 115.34/16.58 % (3578092)Termination phase: Saturation % 115.34/16.58 % (3578092)Time elapsed: 1.334 s % 115.34/16.58 % (3578092)Peak memory usage: 27 MB % 115.34/16.58 % (3578092)Instructions burned: 5134 (million) % 115.34/16.58 % (3578113)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3326269194:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 115.34/16.58 % Exception at run slice level % 115.34/16.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.34/16.58 % (3578115)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2231679492:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 115.34/16.58 % (3578111)Instruction limit reached! % 115.34/16.58 % (3578111)------------------------------ % 115.34/16.58 % (3578111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.34/16.58 % (3578111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.34/16.58 % (3578111)CaDiCaL version: 2.1.3 % 115.34/16.58 % (3578111)Termination reason: Instruction limit % 115.34/16.58 % (3578111)Termination phase: Saturation % 115.34/16.58 % (3578111)Time elapsed: 1.119 s % 115.34/16.58 % (3578111)Peak memory usage: 18 MB % 115.34/16.58 % (3578111)Instructions burned: 2252 (million) % 115.34/16.58 % (3578117)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1887235844:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 115.34/16.58 % (3578115)Instruction limit reached! % 115.34/16.58 % (3578115)------------------------------ % 115.34/16.58 % (3578115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.34/16.58 % (3578115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.34/16.58 % (3578115)CaDiCaL version: 2.1.3 % 115.34/16.58 % (3578115)Termination reason: Instruction limit % 115.34/16.58 % (3578115)Termination phase: Saturation % 115.34/16.58 % (3578115)Time elapsed: 0.818 s % 115.34/16.58 % (3578115)Peak memory usage: 17 MB % 115.34/16.58 % (3578115)Instructions burned: 4597 (million) % 115.34/16.58 % (3578119)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4191234871:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 115.34/16.58 % (3578107)Instruction limit reached! % 115.34/16.58 % (3578107)------------------------------ % 115.34/16.58 % (3578107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.34/16.58 % (3578107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.34/16.58 % (3578107)CaDiCaL version: 2.1.3 % 115.34/16.58 % (3578107)Termination reason: Instruction limit % 115.34/16.58 % (3578107)Termination phase: Saturation % 115.34/16.58 % (3578107)Time elapsed: 1.945 s % 115.34/16.58 % (3578107)Peak memory usage: 27 MB % 115.34/16.58 % (3578107)Instructions burned: 3513 (million) % 115.34/16.58 % (3578121)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=431661768:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 115.34/16.58 % Exception at run slice level % 115.34/16.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.34/16.58 % (3578123)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3423168965:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 115.34/16.58 % Exception at run slice level % 115.34/16.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.34/16.58 % (3578125)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3195776808:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 115.34/16.58 % Exception at run slice level % 140.62/20.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.62/20.08 % (3578127)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1335576789:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 140.62/20.08 % (3578109)Instruction limit reached! % 140.62/20.08 % (3578109)------------------------------ % 140.62/20.08 % (3578109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578109)CaDiCaL version: 2.1.3 % 140.62/20.08 % (3578109)Termination reason: Instruction limit % 140.62/20.08 % (3578109)Termination phase: Saturation % 140.62/20.08 % (3578109)Time elapsed: 2.065 s % 140.62/20.08 % (3578109)Peak memory usage: 29 MB % 140.62/20.08 % (3578109)Instructions burned: 3774 (million) % 140.62/20.08 % (3578129)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2868548456:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 140.62/20.08 % (3578103)Instruction limit reached! % 140.62/20.08 % (3578103)------------------------------ % 140.62/20.08 % (3578103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578103)CaDiCaL version: 2.1.3 % 140.62/20.08 % (3578103)Termination reason: Instruction limit % 140.62/20.08 % (3578103)Termination phase: Saturation % 140.62/20.08 % (3578103)Time elapsed: 2.389 s % 140.62/20.08 % (3578103)Peak memory usage: 18 MB % 140.62/20.08 % (3578103)Instructions burned: 5115 (million) % 140.62/20.08 % (3578131)dis+10_16:1_sil=16000:random_seed=2208451303:i=9155:fsr=off_2968 on theBenchmark for (2968ds/9155Mi) % 140.62/20.08 % (3578119)Instruction limit reached! % 140.62/20.08 % (3578119)------------------------------ % 140.62/20.08 % (3578119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578119)CaDiCaL version: 2.1.3 % 140.62/20.08 % (3578119)Termination reason: Instruction limit % 140.62/20.08 % (3578119)Termination phase: Saturation % 140.62/20.08 % (3578119)Time elapsed: 1.536 s % 140.62/20.08 % (3578119)Peak memory usage: 47 MB % 140.62/20.08 % (3578119)Instructions burned: 5213 (million) % 140.62/20.08 % (3578133)ott-3_8_sil=64000:random_seed=1477976191:i=20139:bs=on_2958 on theBenchmark for (2958ds/20139Mi) % 140.62/20.08 % (3578129)Instruction limit reached! % 140.62/20.08 % (3578129)------------------------------ % 140.62/20.08 % (3578129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578129)CaDiCaL version: 2.1.3 % 140.62/20.08 % (3578129)Termination reason: Instruction limit % 140.62/20.08 % (3578129)Termination phase: Saturation % 140.62/20.08 % (3578129)Time elapsed: 3.947 s % 140.62/20.08 % (3578129)Peak memory usage: 22 MB % 140.62/20.08 % (3578129)Instructions burned: 8173 (million) % 140.62/20.08 % (3578135)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2344582563:fmbsr=2:i=32576_2929 on theBenchmark for (2929ds/32576Mi) % 140.62/20.08 % Exception at run slice level % 140.62/20.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.62/20.08 % (3578137)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1384404291:i=11404_2929 on theBenchmark for (2929ds/11404Mi) % 140.62/20.08 % (3578131)Instruction limit reached! % 140.62/20.08 % (3578131)------------------------------ % 140.62/20.08 % (3578131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578131)CaDiCaL version: 2.1.3 % 140.62/20.08 % (3578131)Termination reason: Instruction limit % 140.62/20.08 % (3578131)Termination phase: Saturation % 140.62/20.08 % (3578131)Time elapsed: 5.012 s % 140.62/20.08 % (3578131)Peak memory usage: 51 MB % 140.62/20.08 % (3578131)Instructions burned: 9156 (million) % 140.62/20.08 % (3578139)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3524955805:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 140.62/20.08 % (3578133)Instruction limit reached! % 140.62/20.08 % (3578133)------------------------------ % 140.62/20.08 % (3578133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.62/20.08 % (3578133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.62/20.08 % (3578133)CaDiCaL version: 2.1.3 % 153.71/21.93 % (3578133)Termination reason: Instruction limit % 153.71/21.93 % (3578133)Termination phase: Saturation % 153.71/21.93 % (3578133)Time elapsed: 4.932 s % 153.71/21.93 % (3578133)Peak memory usage: 25 MB % 153.71/21.93 % (3578133)Instructions burned: 20140 (million) % 153.71/21.93 % (3578141)dis+33_16_sil=32000:sac=on:random_seed=381204609:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 153.71/21.93 % (3578141)Instruction limit reached! % 153.71/21.93 % (3578141)------------------------------ % 153.71/21.93 % (3578141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.71/21.93 % (3578141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.71/21.93 % (3578141)CaDiCaL version: 2.1.3 % 153.71/21.93 % (3578141)Termination reason: Instruction limit % 153.71/21.93 % (3578141)Termination phase: Saturation % 153.71/21.93 % (3578141)Time elapsed: 3.818 s % 153.71/21.93 % (3578141)Peak memory usage: 38 MB % 153.71/21.93 % (3578141)Instructions burned: 15854 (million) % 153.71/21.93 % (3578143)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1895026291:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 153.71/21.93 % (3578137)Instruction limit reached! % 153.71/21.93 % (3578137)------------------------------ % 153.71/21.93 % (3578137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.71/21.93 % (3578137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.71/21.93 % (3578137)CaDiCaL version: 2.1.3 % 153.71/21.93 % (3578137)Termination reason: Instruction limit % 153.71/21.93 % (3578137)Termination phase: Saturation % 153.71/21.93 % (3578137)Time elapsed: 7.660 s % 153.71/21.93 % (3578137)Peak memory usage: 136 MB % 153.71/21.93 % (3578137)Instructions burned: 11404 (million) % 153.71/21.93 % (3578145)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=585609794:s2a=on:i=53295_2852 on theBenchmark for (2852ds/53295Mi) % 153.71/21.93 % (3578139)Instruction limit reached! % 153.71/21.93 % (3578139)------------------------------ % 153.71/21.93 % (3578139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.71/21.93 % (3578139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.71/21.93 % (3578139)CaDiCaL version: 2.1.3 % 153.71/21.93 % (3578139)Termination reason: Instruction limit % 153.71/21.93 % (3578139)Termination phase: Saturation % 153.71/21.93 % (3578139)Time elapsed: 6.946 s % 153.71/21.93 % (3578139)Peak memory usage: 32 MB % 153.71/21.93 % (3578139)Instructions burned: 14134 (million) % 153.71/21.93 % (3578147)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2166473529:i=26857:ins=20_2848 on theBenchmark for (2848ds/26857Mi) % 153.71/21.93 % Exception at run slice level % 153.71/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.71/21.93 % (3578149)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=213125454:i=28120:bs=on:fsr=off_2848 on theBenchmark for (2848ds/28120Mi) % 153.71/21.93 % (3578127)Instruction limit reached! % 153.71/21.93 % (3578127)------------------------------ % 153.71/21.93 % (3578127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.71/21.93 % (3578127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.71/21.93 % (3578127)CaDiCaL version: 2.1.3 % 153.71/21.93 % (3578127)Termination reason: Instruction limit % 153.71/21.93 % (3578127)Termination phase: Saturation % 153.71/21.93 % (3578127)Time elapsed: 13.361 s % 153.71/21.93 % (3578127)Peak memory usage: 80 MB % 153.71/21.93 % (3578127)Instructions burned: 22566 (million) % 153.71/21.93 % (3578267)fmb+10_1_sil=256000:fmbss=7:random_seed=2547058862:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 153.71/21.93 % Exception at run slice level % 153.71/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.71/21.93 % (3578269)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2113171085:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 153.71/21.93 % (3578269)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 153.71/21.93 % Exception at run slice level % 153.71/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.71/21.93 % (3578271)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=175251076:i=160505_2837 on theBenchmark for (2837ds/160505Mi) % 153.71/21.93 % Exception at run slice level % 153.71/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.71/21.93 % (3578285)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=536621868:fmbsr=1.3:i=225729_2836 on theBenchmark for (2836ds/225729Mi) % 210.63/29.99 % Exception at run slice level % 210.63/29.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 210.63/29.99 % (3578295)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2682199587:fmbsr=2:i=185024:ins=7_2836 on theBenchmark for (2836ds/185024Mi) % 210.63/29.99 % Exception at run slice level % 210.63/29.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 210.63/29.99 % (3578309)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=554613208:rtra=on_2836 on theBenchmark for (2836ds/0Mi) % 210.63/29.99 % Exception at run slice level % 210.63/29.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 210.63/29.99 % (3578327)% WARNING: option uhcvi not known. % 210.63/29.99 % (3578327)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=16614222:i=271062:add=off:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/271062Mi) % 210.63/29.99 % (3578117)Instruction limit reached! % 210.63/29.99 % (3578117)------------------------------ % 210.63/29.99 % (3578117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.63/29.99 % (3578117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/29.99 % (3578117)CaDiCaL version: 2.1.3 % 210.63/29.99 % (3578117)Termination reason: Instruction limit % 210.63/29.99 % (3578117)Termination phase: Saturation % 210.63/29.99 % (3578117)Time elapsed: 14.971 s % 210.63/29.99 % (3578117)Peak memory usage: 627 MB % 210.63/29.99 % (3578117)Instructions burned: 29341 (million) % 210.63/29.99 % (3578449)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1923981365:i=176048:add=on:rtra=on:rawr=on_2825 on theBenchmark for (2825ds/176048Mi) % 210.63/29.99 % (3578143)Instruction limit reached! % 210.63/29.99 % (3578143)------------------------------ % 210.63/29.99 % (3578143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.63/29.99 % (3578143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/29.99 % (3578143)CaDiCaL version: 2.1.3 % 210.63/29.99 % (3578143)Termination reason: Instruction limit % 210.63/29.99 % (3578143)Termination phase: Saturation % 210.63/29.99 % (3578143)Time elapsed: 6.369 s % 210.63/29.99 % (3578143)Peak memory usage: 45 MB % 210.63/29.99 % (3578143)Instructions burned: 17627 (million) % 210.63/29.99 % (3578473)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1175649178:i=206:fgj=on:rtra=on_2806 on theBenchmark for (2806ds/206Mi) % 210.63/29.99 % (3578473)Instruction limit reached! % 210.63/29.99 % (3578473)------------------------------ % 210.63/29.99 % (3578473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.63/29.99 % (3578473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/29.99 % (3578473)CaDiCaL version: 2.1.3 % 210.63/29.99 % (3578473)Termination reason: Instruction limit % 210.63/29.99 % (3578473)Termination phase: Saturation % 210.63/29.99 % (3578473)Time elapsed: 0.109 s % 210.63/29.99 % (3578473)Peak memory usage: 13 MB % 210.63/29.99 % (3578473)Instructions burned: 206 (million) % 210.63/29.99 % (3578475)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1871577836:i=232:rtra=on_2805 on theBenchmark for (2805ds/232Mi) % 210.63/29.99 % (3578475)Instruction limit reached! % 210.63/29.99 % (3578475)------------------------------ % 210.63/29.99 % (3578475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.63/29.99 % (3578475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/29.99 % (3578475)CaDiCaL version: 2.1.3 % 210.63/29.99 % (3578475)Termination reason: Instruction limit % 210.63/29.99 % (3578475)Termination phase: Saturation % 210.63/29.99 % (3578475)Time elapsed: 0.125 s % 210.63/29.99 % (3578475)Peak memory usage: 13 MB % 210.63/29.99 % (3578475)Instructions burned: 233 (million) % 210.63/29.99 % (3578477)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2235611804:i=262:rtra=on_2803 on theBenchmark for (2803ds/262Mi) % 210.63/29.99 % (3578477)Instruction limit reached! % 210.63/29.99 % (3578477)------------------------------ % 210.63/29.99 % (3578477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.63/29.99 % (3578477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/29.99 % (3578477)CaDiCaL version: 2.1.3 % 210.63/29.99 % (3578477)Termination reason: Instruction limit % 210.63/29.99 % (3578477)Termination phase: Saturation % 277.44/39.32 % (3578477)Time elapsed: 0.195 s % 277.44/39.32 % (3578477)Peak memory usage: 14 MB % 277.44/39.32 % (3578477)Instructions burned: 262 (million) % 277.44/39.32 % (3578479)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1185788401:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2801 on theBenchmark for (2801ds/318Mi) % 277.44/39.32 % (3578479)Instruction limit reached! % 277.44/39.32 % (3578479)------------------------------ % 277.44/39.32 % (3578479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.44/39.32 % (3578479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.44/39.32 % (3578479)CaDiCaL version: 2.1.3 % 277.44/39.32 % (3578479)Termination reason: Instruction limit % 277.44/39.32 % (3578479)Termination phase: Saturation % 277.44/39.32 % (3578479)Time elapsed: 0.157 s % 277.44/39.32 % (3578479)Peak memory usage: 13 MB % 277.44/39.32 % (3578479)Instructions burned: 320 (million) % 277.44/39.32 % (3578481)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3298020524:i=1428:nm=2:rtra=on_2799 on theBenchmark for (2799ds/1428Mi) % 277.44/39.32 % Exception at run slice level % 277.44/39.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.44/39.32 % (3578483)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3610049833:i=262:bd=preordered:rtra=on:fsd=on_2799 on theBenchmark for (2799ds/262Mi) % 277.44/39.32 % (3578483)Instruction limit reached! % 277.44/39.32 % (3578483)------------------------------ % 277.44/39.32 % (3578483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.44/39.32 % (3578483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.44/39.32 % (3578483)CaDiCaL version: 2.1.3 % 277.44/39.32 % (3578483)Termination reason: Instruction limit % 277.44/39.32 % (3578483)Termination phase: Saturation % 277.44/39.32 % (3578483)Time elapsed: 0.143 s % 277.44/39.32 % (3578483)Peak memory usage: 13 MB % 277.44/39.32 % (3578483)Instructions burned: 262 (million) % 277.44/39.32 % (3578485)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=3544352618:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/1368Mi) % 277.44/39.32 % (3578485)Instruction limit reached! % 277.44/39.32 % (3578485)------------------------------ % 277.44/39.32 % (3578485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.44/39.32 % (3578485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.44/39.32 % (3578485)CaDiCaL version: 2.1.3 % 277.44/39.32 % (3578485)Termination reason: Instruction limit % 277.44/39.32 % (3578485)Termination phase: Saturation % 277.44/39.32 % (3578485)Time elapsed: 0.716 s % 277.44/39.32 % (3578485)Peak memory usage: 17 MB % 277.44/39.32 % (3578485)Instructions burned: 1368 (million) % 277.44/39.32 % (3578490)ott-21_1_sil=16000:si=on:fs=off:random_seed=3182153317:i=360:av=off:fsr=off:rtra=on_2790 on theBenchmark for (2790ds/360Mi) % 277.44/39.32 % (3578490)Instruction limit reached! % 277.44/39.32 % (3578490)------------------------------ % 277.44/39.32 % (3578490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.44/39.32 % (3578490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.44/39.32 % (3578490)CaDiCaL version: 2.1.3 % 277.44/39.32 % (3578490)Termination reason: Instruction limit % 277.44/39.32 % (3578490)Termination phase: Saturation % 277.44/39.32 % (3578490)Time elapsed: 0.171 s % 277.44/39.32 % (3578490)Peak memory usage: 14 MB % 277.44/39.32 % (3578490)Instructions burned: 360 (million) % 277.44/39.32 % (3578493)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2197771807:i=954:bd=all:rtra=on_2788 on theBenchmark for (2788ds/954Mi) % 277.44/39.32 % (3578493)Instruction limit reached! % 277.44/39.32 % (3578493)------------------------------ % 277.44/39.32 % (3578493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.44/39.32 % (3578493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.44/39.32 % (3578493)CaDiCaL version: 2.1.3 % 277.44/39.32 % (3578493)Termination reason: Instruction limit % 277.44/39.32 % (3578493)Termination phase: Saturation % 277.44/39.32 % (3578493)Time elapsed: 0.468 s % 277.44/39.32 % (3578493)Peak memory usage: 14 MB % 277.44/39.32 % (3578493)Instructions burned: 955 (million) % 277.44/39.32 % (3578497)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3122888326:fmbsr=1.3:i=1730:ins=25:rtra=on_2783 on theBenchmark for (2783ds/1730Mi) % 277.44/39.32 % Exception at run slice level % 277.44/39.32 User error: Finite model building is currently Terminated % 300.21/42.54 % Vampire exiting % 300.21/42.54 Terminated %------------------------------------------------------------------------------