%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV665_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:26:13 PM UTC 2026 % Result : Timeout 300.32s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV665_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 % Computer : n013.cluster.edu % 0.08/0.21 % Model : x86_64 x86_64 % 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.21 % Memory : 8046.5625MB % 0.08/0.21 % OS : Linux 6.8.0-71-generic % 0.08/0.21 % CPULimit : 300 % 0.08/0.21 % WCLimit : 300 % 0.08/0.21 % DateTime : Mon Sep 28 12:11:07 UTC 2026 % 0.08/0.21 % CPUTime : % 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.24 Running first-order model finding % 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.34/1.51 % (1136323)Will run a generic schedule for satisfiability detection. % 8.34/1.51 % (1136328)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1392193362_2999 on theBenchmark for (2999ds/0Mi) % 8.34/1.51 % (1136330)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3127920658:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.34/1.51 % (1136334)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1906936991:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.34/1.51 % (1136331)dis+10_1_sil=32000:sp=arity:random_seed=2663322972:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.34/1.51 % (1136333)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2274958596:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.34/1.51 % (1136332)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=847639518:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.34/1.51 % (1136329)% WARNING: option uhcvi not known. % 8.34/1.51 % (1136329)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1431497852:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.34/1.51 % Exception at run slice level % 8.34/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.34/1.51 % (1136342)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1307839183:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.34/1.51 % Exception at run slice level % 8.34/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.34/1.51 % (1136344)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2926471101:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.34/1.51 % (1136331)Instruction limit reached! % 8.34/1.51 % (1136331)------------------------------ % 8.34/1.51 % (1136331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.34/1.51 % (1136331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.34/1.51 % (1136331)CaDiCaL version: 2.1.3 % 8.34/1.51 % (1136331)Termination reason: Instruction limit % 8.34/1.51 % (1136331)Termination phase: Saturation % 8.34/1.51 % (1136331)Time elapsed: 0.062 s % 8.34/1.51 % (1136331)Peak memory usage: 12 MB % 8.34/1.51 % (1136331)Instructions burned: 105 (million) % 8.34/1.51 % (1136332)Instruction limit reached! % 8.34/1.51 % (1136332)------------------------------ % 8.34/1.51 % (1136332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.34/1.51 % (1136332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.34/1.51 % (1136332)CaDiCaL version: 2.1.3 % 8.34/1.51 % (1136332)Termination reason: Instruction limit % 8.34/1.51 % (1136332)Termination phase: Saturation % 8.34/1.51 % (1136332)Time elapsed: 0.065 s % 8.34/1.51 % (1136332)Peak memory usage: 13 MB % 8.34/1.51 % (1136332)Instructions burned: 117 (million) % 8.34/1.51 % (1136333)Instruction limit reached! % 8.34/1.51 % (1136333)------------------------------ % 8.34/1.51 % (1136333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.34/1.51 % (1136333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.34/1.51 % (1136333)CaDiCaL version: 2.1.3 % 8.34/1.51 % (1136333)Termination reason: Instruction limit % 8.34/1.51 % (1136333)Termination phase: Saturation % 8.34/1.51 % (1136333)Time elapsed: 0.080 s % 8.34/1.51 % (1136333)Peak memory usage: 13 MB % 8.34/1.51 % (1136333)Instructions burned: 136 (million) % 8.34/1.51 % (1136346)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=777035983:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.34/1.51 % (1136347)ott-21_1_sil=16000:fs=off:random_seed=2259993290:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.34/1.51 % (1136344)Instruction limit reached! % 8.34/1.51 % (1136344)------------------------------ % 8.34/1.51 % (1136344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.34/1.51 % (1136344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.34/1.51 % (1136344)CaDiCaL version: 2.1.3 % 8.34/1.51 % (1136344)Termination reason: Instruction limit % 8.34/1.51 % (1136344)Termination phase: Saturation % 8.34/1.51 % (1136344)Time elapsed: 0.043 s % 8.34/1.51 % (1136344)Peak memory usage: 14 MB % 8.34/1.51 % (1136344)Instructions burned: 134 (million) % 8.34/1.51 % (1136351)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=799634671:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.95/3.30 % (1136348)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=62583373:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 20.95/3.30 % (1136334)Instruction limit reached! % 20.95/3.30 % (1136334)------------------------------ % 20.95/3.30 % (1136334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.30 % (1136334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.30 % (1136334)CaDiCaL version: 2.1.3 % 20.95/3.30 % (1136334)Termination reason: Instruction limit % 20.95/3.30 % (1136334)Termination phase: Saturation % 20.95/3.30 % (1136334)Time elapsed: 0.101 s % 20.95/3.30 % (1136334)Peak memory usage: 14 MB % 20.95/3.30 % (1136334)Instructions burned: 160 (million) % 20.95/3.30 % Exception at run slice level % 20.95/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.30 % (1136355)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3815601969:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.95/3.30 % Exception at run slice level % 20.95/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.30 % (1136354)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=49542778:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.95/3.30 % (1136357)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=670820401:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 20.95/3.30 % (1136347)Instruction limit reached! % 20.95/3.30 % (1136347)------------------------------ % 20.95/3.30 % (1136347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.30 % (1136347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.30 % (1136347)CaDiCaL version: 2.1.3 % 20.95/3.30 % (1136347)Termination reason: Instruction limit % 20.95/3.30 % (1136347)Termination phase: Saturation % 20.95/3.30 % (1136347)Time elapsed: 0.093 s % 20.95/3.30 % (1136347)Peak memory usage: 13 MB % 20.95/3.30 % (1136347)Instructions burned: 181 (million) % 20.95/3.30 % (1136360)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=393065853:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.95/3.30 % (1136357)Instruction limit reached! % 20.95/3.30 % (1136357)------------------------------ % 20.95/3.30 % (1136357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.30 % (1136357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.30 % (1136357)CaDiCaL version: 2.1.3 % 20.95/3.30 % (1136357)Termination reason: Instruction limit % 20.95/3.30 % (1136357)Termination phase: Saturation % 20.95/3.30 % (1136357)Time elapsed: 0.227 s % 20.95/3.30 % (1136357)Peak memory usage: 20 MB % 20.95/3.30 % (1136357)Instructions burned: 693 (million) % 20.95/3.30 % (1136362)fmb+10_1_sil=64000:random_seed=1690853647:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 20.95/3.30 % (1136362)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.95/3.30 % Exception at run slice level % 20.95/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.30 % (1136364)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=137537718:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 20.95/3.30 % Exception at run slice level % 20.95/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.30 % (1136366)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1832148414:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 20.95/3.30 % Exception at run slice level % 20.95/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.30 % (1136348)Instruction limit reached! % 20.95/3.30 % (1136348)------------------------------ % 20.95/3.30 % (1136348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.30 % (1136348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.30 % (1136348)CaDiCaL version: 2.1.3 % 20.95/3.30 % (1136348)Termination reason: Instruction limit % 20.95/3.30 % (1136348)Termination phase: Saturation % 20.95/3.30 % (1136348)Time elapsed: 0.312 s % 64.94/9.47 % (1136348)Peak memory usage: 14 MB % 64.94/9.47 % (1136348)Instructions burned: 478 (million) % 64.94/9.47 % (1136368)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=355340583:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 64.94/9.47 % (1136369)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3476131038:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 64.94/9.47 % (1136369)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.94/9.47 % (1136346)Instruction limit reached! % 64.94/9.47 % (1136346)------------------------------ % 64.94/9.47 % (1136346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.94/9.47 % (1136346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.94/9.47 % (1136346)CaDiCaL version: 2.1.3 % 64.94/9.47 % (1136346)Termination reason: Instruction limit % 64.94/9.47 % (1136346)Termination phase: Saturation % 64.94/9.47 % (1136346)Time elapsed: 0.389 s % 64.94/9.47 % (1136346)Peak memory usage: 17 MB % 64.94/9.47 % (1136346)Instructions burned: 685 (million) % 64.94/9.47 % (1136372)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3310941478:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 64.94/9.47 % Exception at run slice level % 64.94/9.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.94/9.47 % (1136374)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=191792123:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 64.94/9.47 % Exception at run slice level % 64.94/9.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.94/9.47 % (1136376)ott-2_1_sil=16000:newcnf=on:random_seed=1873148977:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 64.94/9.47 % (1136360)Instruction limit reached! % 64.94/9.47 % (1136360)------------------------------ % 64.94/9.47 % (1136360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.94/9.47 % (1136360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.94/9.47 % (1136360)CaDiCaL version: 2.1.3 % 64.94/9.47 % (1136360)Termination reason: Instruction limit % 64.94/9.47 % (1136360)Termination phase: Saturation % 64.94/9.47 % (1136360)Time elapsed: 0.496 s % 64.94/9.47 % (1136360)Peak memory usage: 18 MB % 64.94/9.47 % (1136360)Instructions burned: 880 (million) % 64.94/9.47 % (1136378)ott+10_1_sil=32000:tgt=ground:random_seed=4147748280:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.94/9.47 % (1136354)Instruction limit reached! % 64.94/9.47 % (1136354)------------------------------ % 64.94/9.47 % (1136354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.94/9.47 % (1136354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.94/9.47 % (1136354)CaDiCaL version: 2.1.3 % 64.94/9.47 % (1136354)Termination reason: Instruction limit % 64.94/9.47 % (1136354)Termination phase: Saturation % 64.94/9.47 % (1136354)Time elapsed: 0.704 s % 64.94/9.47 % (1136354)Peak memory usage: 28 MB % 64.94/9.47 % (1136354)Instructions burned: 1179 (million) % 64.94/9.47 % (1136380)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=319723429:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 64.94/9.47 % Exception at run slice level % 64.94/9.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.94/9.47 % (1136382)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1313354476:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 64.94/9.47 % (1136376)Instruction limit reached! % 64.94/9.47 % (1136376)------------------------------ % 64.94/9.47 % (1136376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.94/9.47 % (1136376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.94/9.47 % (1136376)CaDiCaL version: 2.1.3 % 64.94/9.47 % (1136376)Termination reason: Instruction limit % 64.94/9.47 % (1136376)Termination phase: Saturation % 64.94/9.47 % (1136376)Time elapsed: 0.505 s % 64.94/9.47 % (1136376)Peak memory usage: 21 MB % 64.94/9.47 % (1136376)Instructions burned: 870 (million) % 64.94/9.47 % (1136384)dis+21_1_sil=32000:sas=cadical:random_seed=453539752:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 64.94/9.47 % (1136369)Instruction limit reached! % 64.94/9.47 % (1136369)------------------------------ % 64.94/9.47 % (1136369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136369)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136369)Termination reason: Instruction limit % 126.91/18.17 % (1136369)Termination phase: Saturation % 126.91/18.17 % (1136369)Time elapsed: 0.795 s % 126.91/18.17 % (1136369)Peak memory usage: 30 MB % 126.91/18.17 % (1136369)Instructions burned: 1473 (million) % 126.91/18.17 % (1136386)ott+11_1_sil=16000:gs=on:random_seed=1482981772:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 126.91/18.17 % (1136368)Instruction limit reached! % 126.91/18.17 % (1136368)------------------------------ % 126.91/18.17 % (1136368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136368)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136368)Termination reason: Instruction limit % 126.91/18.17 % (1136368)Termination phase: Saturation % 126.91/18.17 % (1136368)Time elapsed: 1.417 s % 126.91/18.17 % (1136368)Peak memory usage: 47 MB % 126.91/18.17 % (1136368)Instructions burned: 5132 (million) % 126.91/18.17 % (1136388)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4036915029:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 126.91/18.17 % Exception at run slice level % 126.91/18.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.91/18.17 % (1136390)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=10502155:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 126.91/18.17 % (1136386)Instruction limit reached! % 126.91/18.17 % (1136386)------------------------------ % 126.91/18.17 % (1136386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136386)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136386)Termination reason: Instruction limit % 126.91/18.17 % (1136386)Termination phase: Saturation % 126.91/18.17 % (1136386)Time elapsed: 1.306 s % 126.91/18.17 % (1136386)Peak memory usage: 33 MB % 126.91/18.17 % (1136386)Instructions burned: 2252 (million) % 126.91/18.17 % (1136544)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3376768289:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 126.91/18.17 % (1136382)Instruction limit reached! % 126.91/18.17 % (1136382)------------------------------ % 126.91/18.17 % (1136382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136382)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136382)Termination reason: Instruction limit % 126.91/18.17 % (1136382)Termination phase: Saturation % 126.91/18.17 % (1136382)Time elapsed: 1.777 s % 126.91/18.17 % (1136382)Peak memory usage: 30 MB % 126.91/18.17 % (1136382)Instructions burned: 3513 (million) % 126.91/18.17 % (1136546)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3841283192:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 126.91/18.17 % (1136384)Instruction limit reached! % 126.91/18.17 % (1136384)------------------------------ % 126.91/18.17 % (1136384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136384)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136384)Termination reason: Instruction limit % 126.91/18.17 % (1136384)Termination phase: Saturation % 126.91/18.17 % (1136384)Time elapsed: 1.903 s % 126.91/18.17 % (1136384)Peak memory usage: 32 MB % 126.91/18.17 % (1136384)Instructions burned: 3775 (million) % 126.91/18.17 % (1136548)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=791880113:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 126.91/18.17 % Exception at run slice level % 126.91/18.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.91/18.17 % (1136390)Instruction limit reached! % 126.91/18.17 % (1136390)------------------------------ % 126.91/18.17 % (1136390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.91/18.17 % (1136390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/18.17 % (1136390)CaDiCaL version: 2.1.3 % 126.91/18.17 % (1136390)Termination reason: Instruction limit % 126.91/18.17 % (1136390)Termination phase: Saturation % 126.91/18.17 % (1136390)Time elapsed: 1.155 s % 126.91/18.17 % (1136390)Peak memory usage: 44 MB % 159.93/22.87 % (1136390)Instructions burned: 4593 (million) % 159.93/22.87 % (1136550)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=693563204:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 159.93/22.87 % (1136551)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3936534543:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 159.93/22.87 % Exception at run slice level % 159.93/22.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 159.93/22.87 % Exception at run slice level % 159.93/22.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 159.93/22.87 % (1136555)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=601221994:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 159.93/22.87 % (1136554)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3856238394:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 159.93/22.87 % (1136378)Instruction limit reached! % 159.93/22.87 % (1136378)------------------------------ % 159.93/22.87 % (1136378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.93/22.87 % (1136378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.93/22.87 % (1136378)CaDiCaL version: 2.1.3 % 159.93/22.87 % (1136378)Termination reason: Instruction limit % 159.93/22.87 % (1136378)Termination phase: Saturation % 159.93/22.87 % (1136378)Time elapsed: 2.942 s % 159.93/22.87 % (1136378)Peak memory usage: 51 MB % 159.93/22.87 % (1136378)Instructions burned: 5115 (million) % 159.93/22.87 % (1136558)dis+10_16:1_sil=16000:random_seed=927919678:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 159.93/22.87 % (1136546)Instruction limit reached! % 159.93/22.87 % (1136546)------------------------------ % 159.93/22.87 % (1136546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.93/22.87 % (1136546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.93/22.87 % (1136546)CaDiCaL version: 2.1.3 % 159.93/22.87 % (1136546)Termination reason: Instruction limit % 159.93/22.87 % (1136546)Termination phase: Saturation % 159.93/22.87 % (1136546)Time elapsed: 2.860 s % 159.93/22.87 % (1136546)Peak memory usage: 45 MB % 159.93/22.87 % (1136546)Instructions burned: 5212 (million) % 159.93/22.87 % (1136560)ott-3_8_sil=64000:random_seed=426376336:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 159.93/22.87 % (1136555)Instruction limit reached! % 159.93/22.87 % (1136555)------------------------------ % 159.93/22.87 % (1136555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.93/22.87 % (1136555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.93/22.87 % (1136555)CaDiCaL version: 2.1.3 % 159.93/22.87 % (1136555)Termination reason: Instruction limit % 159.93/22.87 % (1136555)Termination phase: Saturation % 159.93/22.87 % (1136555)Time elapsed: 2.551 s % 159.93/22.87 % (1136555)Peak memory usage: 62 MB % 159.93/22.87 % (1136555)Instructions burned: 8174 (million) % 159.93/22.87 % (1136562)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1302750466:fmbsr=2:i=32576_2943 on theBenchmark for (2943ds/32576Mi) % 159.93/22.87 % Exception at run slice level % 159.93/22.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 159.93/22.87 % (1136564)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=171725474:i=11404_2943 on theBenchmark for (2943ds/11404Mi) % 159.93/22.87 % (1136558)Instruction limit reached! % 159.93/22.87 % (1136558)------------------------------ % 159.93/22.87 % (1136558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.93/22.87 % (1136558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.93/22.87 % (1136558)CaDiCaL version: 2.1.3 % 159.93/22.87 % (1136558)Termination reason: Instruction limit % 159.93/22.87 % (1136558)Termination phase: Saturation % 159.93/22.87 % (1136558)Time elapsed: 4.401 s % 159.93/22.87 % (1136558)Peak memory usage: 45 MB % 159.93/22.87 % (1136558)Instructions burned: 9156 (million) % 159.93/22.87 % (1136566)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1372495080:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 159.93/22.87 % (1136564)Instruction limit reached! % 159.93/22.87 % (1136564)------------------------------ % 159.93/22.87 % (1136564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.93/22.87 % (1136564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.93/22.87 % (1136564)CaDiCaL version: 2.1.3 % 159.93/22.87 % (1136564)Termination reason: Instruction limit % 174.34/24.97 % (1136564)Termination phase: Saturation % 174.34/24.97 % (1136564)Time elapsed: 3.561 s % 174.34/24.97 % (1136564)Peak memory usage: 66 MB % 174.34/24.97 % (1136564)Instructions burned: 11406 (million) % 174.34/24.97 % (1136568)dis+33_16_sil=32000:sac=on:random_seed=2218009842:i=15851:nm=0_2907 on theBenchmark for (2907ds/15851Mi) % 174.34/24.97 % (1136554)Instruction limit reached! % 174.34/24.97 % (1136554)------------------------------ % 174.34/24.97 % (1136554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.34/24.97 % (1136554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/24.97 % (1136554)CaDiCaL version: 2.1.3 % 174.34/24.97 % (1136554)Termination reason: Instruction limit % 174.34/24.97 % (1136554)Termination phase: Saturation % 174.34/24.97 % (1136554)Time elapsed: 9.737 s % 174.34/24.97 % (1136554)Peak memory usage: 102 MB % 174.34/24.97 % (1136554)Instructions burned: 22566 (million) % 174.34/24.97 % (1136570)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3446021112:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 174.34/24.97 % (1136568)Instruction limit reached! % 174.34/24.97 % (1136568)------------------------------ % 174.34/24.97 % (1136568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.34/24.97 % (1136568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/24.97 % (1136568)CaDiCaL version: 2.1.3 % 174.34/24.97 % (1136568)Termination reason: Instruction limit % 174.34/24.97 % (1136568)Termination phase: Saturation % 174.34/24.97 % (1136568)Time elapsed: 4.330 s % 174.34/24.97 % (1136568)Peak memory usage: 104 MB % 174.34/24.97 % (1136568)Instructions burned: 15853 (million) % 174.34/24.97 % (1136704)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3080213995:s2a=on:i=53295_2864 on theBenchmark for (2864ds/53295Mi) % 174.34/24.97 % (1136566)Instruction limit reached! % 174.34/24.97 % (1136566)------------------------------ % 174.34/24.97 % (1136566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.34/24.97 % (1136566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/24.97 % (1136566)CaDiCaL version: 2.1.3 % 174.34/24.97 % (1136566)Termination reason: Instruction limit % 174.34/24.97 % (1136566)Termination phase: Saturation % 174.34/24.97 % (1136566)Time elapsed: 8.789 s % 174.34/24.97 % (1136566)Peak memory usage: 69 MB % 174.34/24.97 % (1136566)Instructions burned: 14134 (million) % 174.34/24.97 % (1136876)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4090180262:i=26857:ins=20_2830 on theBenchmark for (2830ds/26857Mi) % 174.34/24.97 % Exception at run slice level % 174.34/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.34/24.97 % (1136878)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3269863827:i=28120:bs=on:fsr=off_2830 on theBenchmark for (2830ds/28120Mi) % 174.34/24.97 % (1136560)Instruction limit reached! % 174.34/24.97 % (1136560)------------------------------ % 174.34/24.97 % (1136560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.34/24.97 % (1136560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/24.97 % (1136560)CaDiCaL version: 2.1.3 % 174.34/24.97 % (1136560)Termination reason: Instruction limit % 174.34/24.97 % (1136560)Termination phase: Saturation % 174.34/24.97 % (1136560)Time elapsed: 12.217 s % 174.34/24.97 % (1136560)Peak memory usage: 127 MB % 174.34/24.97 % (1136560)Instructions burned: 20140 (million) % 174.34/24.97 % (1137032)fmb+10_1_sil=256000:fmbss=7:random_seed=650462939:fmbsr=1.6:i=182295_2821 on theBenchmark for (2821ds/182295Mi) % 174.34/24.97 % Exception at run slice level % 174.34/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.34/24.97 % (1137034)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2411783240:i=44625:gsp=on_2821 on theBenchmark for (2821ds/44625Mi) % 174.34/24.97 % (1137034)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 174.34/24.97 % Exception at run slice level % 174.34/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.34/24.97 % (1137036)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1904745049:i=160505_2821 on theBenchmark for (2821ds/160505Mi) % 174.34/24.97 % Exception at run slice level % 174.34/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.34/24.97 % (1137038)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=436218183:fmbsr=1.3:i=225729_2820 on theBenchmark for (2820ds/225729Mi) % 199.75/28.46 % Exception at run slice level % 199.75/28.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 199.75/28.46 % (1137040)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1981708168:fmbsr=2:i=185024:ins=7_2820 on theBenchmark for (2820ds/185024Mi) % 199.75/28.46 % Exception at run slice level % 199.75/28.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 199.75/28.46 % (1137042)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1467826653:rtra=on_2820 on theBenchmark for (2820ds/0Mi) % 199.75/28.46 % Exception at run slice level % 199.75/28.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 199.75/28.46 % (1137044)% WARNING: option uhcvi not known. % 199.75/28.46 % (1137044)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3864688717:i=271062:add=off:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/271062Mi) % 199.75/28.46 % (1136544)Instruction limit reached! % 199.75/28.46 % (1136544)------------------------------ % 199.75/28.46 % (1136544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.75/28.46 % (1136544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.75/28.46 % (1136544)CaDiCaL version: 2.1.3 % 199.75/28.46 % (1136544)Termination reason: Instruction limit % 199.75/28.46 % (1136544)Termination phase: Saturation % 199.75/28.46 % (1136544)Time elapsed: 15.504 s % 199.75/28.46 % (1136544)Peak memory usage: 133 MB % 199.75/28.46 % (1136544)Instructions burned: 29341 (million) % 199.75/28.46 % (1137046)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2061343038:i=176048:add=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/176048Mi) % 199.75/28.46 % (1136570)Instruction limit reached! % 199.75/28.46 % (1136570)------------------------------ % 199.75/28.46 % (1136570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.75/28.46 % (1136570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.75/28.46 % (1136570)CaDiCaL version: 2.1.3 % 199.75/28.46 % (1136570)Termination reason: Instruction limit % 199.75/28.46 % (1136570)Termination phase: Saturation % 199.75/28.46 % (1136570)Time elapsed: 9.285 s % 199.75/28.46 % (1136570)Peak memory usage: 91 MB % 199.75/28.46 % (1136570)Instructions burned: 17628 (million) % 199.75/28.46 % (1137048)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2645585352:i=206:fgj=on:rtra=on_2778 on theBenchmark for (2778ds/206Mi) % 199.75/28.46 % (1137048)Instruction limit reached! % 199.75/28.46 % (1137048)------------------------------ % 199.75/28.46 % (1137048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.75/28.46 % (1137048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.75/28.46 % (1137048)CaDiCaL version: 2.1.3 % 199.75/28.46 % (1137048)Termination reason: Instruction limit % 199.75/28.46 % (1137048)Termination phase: Saturation % 199.75/28.46 % (1137048)Time elapsed: 0.122 s % 199.75/28.46 % (1137048)Peak memory usage: 13 MB % 199.75/28.46 % (1137048)Instructions burned: 206 (million) % 199.75/28.46 % (1137050)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2884983931:i=232:rtra=on_2777 on theBenchmark for (2777ds/232Mi) % 199.75/28.46 % (1137050)Instruction limit reached! % 199.75/28.46 % (1137050)------------------------------ % 199.75/28.46 % (1137050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.75/28.46 % (1137050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.75/28.46 % (1137050)CaDiCaL version: 2.1.3 % 199.75/28.46 % (1137050)Termination reason: Instruction limit % 199.75/28.46 % (1137050)Termination phase: Saturation % 199.75/28.46 % (1137050)Time elapsed: 0.134 s % 199.75/28.46 % (1137050)Peak memory usage: 14 MB % 199.75/28.46 % (1137050)Instructions burned: 232 (million) % 199.75/28.46 % (1137052)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2927352823:i=262:rtra=on_2775 on theBenchmark for (2775ds/262Mi) % 199.75/28.46 % (1137052)Instruction limit reached! % 199.75/28.46 % (1137052)------------------------------ % 199.75/28.46 % (1137052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.75/28.46 % (1137052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.75/28.46 % (1137052)CaDiCaL version: 2.1.3 % 199.75/28.46 % (1137052)Termination reason: Instruction limit % 199.75/28.46 % (1137052)Termination phase: Saturation % 237.35/33.79 % (1137052)Time elapsed: 0.151 s % 237.35/33.79 % (1137052)Peak memory usage: 14 MB % 237.35/33.79 % (1137052)Instructions burned: 263 (million) % 237.35/33.79 % (1137054)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2791029518:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2773 on theBenchmark for (2773ds/318Mi) % 237.35/33.79 % (1137054)Instruction limit reached! % 237.35/33.79 % (1137054)------------------------------ % 237.35/33.79 % (1137054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.35/33.79 % (1137054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.35/33.79 % (1137054)CaDiCaL version: 2.1.3 % 237.35/33.79 % (1137054)Termination reason: Instruction limit % 237.35/33.79 % (1137054)Termination phase: Saturation % 237.35/33.79 % (1137054)Time elapsed: 0.215 s % 237.35/33.79 % (1137054)Peak memory usage: 15 MB % 237.35/33.79 % (1137054)Instructions burned: 318 (million) % 237.35/33.79 % (1137056)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1985232211:i=1428:nm=2:rtra=on_2771 on theBenchmark for (2771ds/1428Mi) % 237.35/33.79 % Exception at run slice level % 237.35/33.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 237.35/33.79 % (1137058)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1861097970:i=262:bd=preordered:rtra=on:fsd=on_2771 on theBenchmark for (2771ds/262Mi) % 237.35/33.79 % (1137058)Instruction limit reached! % 237.35/33.79 % (1137058)------------------------------ % 237.35/33.79 % (1137058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.35/33.79 % (1137058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.35/33.79 % (1137058)CaDiCaL version: 2.1.3 % 237.35/33.79 % (1137058)Termination reason: Instruction limit % 237.35/33.79 % (1137058)Termination phase: Saturation % 237.35/33.79 % (1137058)Time elapsed: 0.152 s % 237.35/33.79 % (1137058)Peak memory usage: 14 MB % 237.35/33.79 % (1137058)Instructions burned: 263 (million) % 237.35/33.79 % (1137060)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=1095105730:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/1368Mi) % 237.35/33.79 % (1137060)Instruction limit reached! % 237.35/33.79 % (1137060)------------------------------ % 237.35/33.79 % (1137060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.35/33.79 % (1137060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.35/33.79 % (1137060)CaDiCaL version: 2.1.3 % 237.35/33.79 % (1137060)Termination reason: Instruction limit % 237.35/33.79 % (1137060)Termination phase: Saturation % 237.35/33.79 % (1137060)Time elapsed: 0.759 s % 237.35/33.79 % (1137060)Peak memory usage: 20 MB % 237.35/33.79 % (1137060)Instructions burned: 1369 (million) % 237.35/33.79 % (1137062)ott-21_1_sil=16000:si=on:fs=off:random_seed=3827518464:i=360:av=off:fsr=off:rtra=on_2761 on theBenchmark for (2761ds/360Mi) % 237.35/33.79 % (1137062)Instruction limit reached! % 237.35/33.79 % (1137062)------------------------------ % 237.35/33.79 % (1137062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.35/33.79 % (1137062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.35/33.79 % (1137062)CaDiCaL version: 2.1.3 % 237.35/33.79 % (1137062)Termination reason: Instruction limit % 237.35/33.79 % (1137062)Termination phase: Saturation % 237.35/33.79 % (1137062)Time elapsed: 0.188 s % 237.35/33.79 % (1137062)Peak memory usage: 13 MB % 237.35/33.79 % (1137062)Instructions burned: 361 (million) % 237.35/33.79 % (1137064)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1707690014:i=954:bd=all:rtra=on_2759 on theBenchmark for (2759ds/954Mi) % 237.35/33.79 % (1137064)Instruction limit reached! % 237.35/33.79 % (1137064)------------------------------ % 237.35/33.79 % (1137064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.35/33.79 % (1137064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.35/33.79 % (1137064)CaDiCaL version: 2.1.3 % 237.35/33.79 % (1137064)Termination reason: Instruction limit % 237.35/33.79 % (1137064)Termination phase: Saturation % 237.35/33.79 % (1137064)Time elapsed: 0.623 s % 237.35/33.79 % (1137064)Peak memory usage: 16 MB % 237.35/33.79 % (1137064)Instructions burned: 955 (million) % 237.35/33.79 % (1137066)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=828871033:fmbsr=1.3:i=1730:ins=25:rtra=on_2753 on theBenchmark for (2753ds/1730Mi) % 237.35/33.79 % Exception at run slice level % 237.35/33.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.95/38.15 % (1137068)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1064329026:i=2358:rtra=on_2752 on theBenchmark for (2752ds/2358Mi) % 268.95/38.15 % (1137068)Instruction limit reached! % 268.95/38.15 % (1137068)------------------------------ % 268.95/38.15 % (1137068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.95/38.15 % (1137068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.95/38.15 % (1137068)CaDiCaL version: 2.1.3 % 268.95/38.15 % (1137068)Termination reason: Instruction limit % 268.95/38.15 % (1137068)Termination phase: Saturation % 268.95/38.15 % (1137068)Time elapsed: 1.539 s % 268.95/38.15 % (1137068)Peak memory usage: 43 MB % 268.95/38.15 % (1137068)Instructions burned: 2358 (million) % 268.95/38.15 % (1137070)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1372833083:i=1778:ins=1:rtra=on_2737 on theBenchmark for (2737ds/1778Mi) % 268.95/38.15 % Exception at run slice level % 268.95/38.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.95/38.15 % (1137072)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=1351707483:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/1384Mi) % 268.95/38.15 % (1137072)Instruction limit reached! % 268.95/38.15 % (1137072)------------------------------ % 268.95/38.15 % (1137072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.95/38.15 % (1137072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.95/38.15 % (1137072)CaDiCaL version: 2.1.3 % 268.95/38.15 % (1137072)Termination reason: Instruction limit % 268.95/38.15 % (1137072)Termination phase: Saturation % 268.95/38.15 % (1137072)Time elapsed: 0.840 s % 268.95/38.15 % (1137072)Peak memory usage: 23 MB % 268.95/38.15 % (1137072)Instructions burned: 1385 (million) % 268.95/38.15 % (1137074)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2280281853:i=1758:kws=inv_precedence:fsr=off:rtra=on_2728 on theBenchmark for (2728ds/1758Mi) % 268.95/38.15 % (1136704)Instruction limit reached! % 268.95/38.15 % (1136704)------------------------------ % 268.95/38.15 % (1136704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.95/38.15 % (1136704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.95/38.15 % (1136704)CaDiCaL version: 2.1.3 % 268.95/38.15 % (1136704)Termination reason: Instruction limit % 268.95/38.15 % (1136704)Termination phase: Saturation % 268.95/38.15 % (1136704)Time elapsed: 14.453 s % 268.95/38.15 % (1136704)Peak memory usage: 247 MB % 268.95/38.15 % (1136704)Instructions burned: 53297 (million) % 268.95/38.15 % (1137076)fmb+10_1_sil=64000:si=on:random_seed=1224948770:i=44122:nm=2:rtra=on:gsp=on_2719 on theBenchmark for (2719ds/44122Mi) % 268.95/38.15 % (1137076)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 268.95/38.15 % Exception at run slice level % 268.95/38.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.95/38.15 % (1137078)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3981670550:i=19030:nm=5:rtra=on_2719 on theBenchmark for (2719ds/19030Mi) % 268.95/38.15 % Exception at run slice level % 268.95/38.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.95/38.15 % (1137081)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1877785287:fmbsr=1.7:i=1840:rtra=on_2719 on theBenchmark for (2719ds/1840Mi) % 268.95/38.15 % Exception at run slice level % 268.95/38.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.95/38.15 % (1137083)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3904172857:i=10262:rtra=on_2718 on theBenchmark for (2718ds/10262Mi) % 268.95/38.15 % (1137074)Instruction limit reached! % 268.95/38.15 % (1137074)------------------------------ % 268.95/38.15 % (1137074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.95/38.15 % (1137074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.95/38.15 % (1137074)CaDiCaL version: 2.1.3 % 268.95/38.15 % (1137074)Termination reason: Instruction limit % 268.95/38.15 % (1137074)Termination phase: Saturation % 268.95/38.15 % (1137074)Time elapsed: 1.022 s % 268.95/38.15 % (1137074)Peak memory usage: 23 MB % 268.95/38.15 % (11Terminated % 300.32/42.63 % Vampire exiting % 300.32/42.63 Terminated %------------------------------------------------------------------------------