%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV581_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 : n015.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:04 PM UTC 2026 % Result : Timeout 299.56s 42.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV581_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.07/0.19 % Computer : n015.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 11:59:26 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.65/1.29 % (2577272)Will run a generic schedule for satisfiability detection. % 6.65/1.29 % (2577277)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3061937459_2999 on theBenchmark for (2999ds/0Mi) % 6.65/1.29 % Exception at run slice level % 6.65/1.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.65/1.29 % (2577278)% WARNING: option uhcvi not known. % 6.65/1.29 % (2577278)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1412712604:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.65/1.29 % (2577279)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2536867739:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.65/1.29 % (2577280)dis+10_1_sil=32000:sp=arity:random_seed=2419314050:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.65/1.29 % (2577281)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=770885608:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.65/1.29 % (2577282)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2042051573:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.65/1.29 % (2577283)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3254009802:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.65/1.29 % (2577285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=327749129:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.65/1.29 % Exception at run slice level % 6.65/1.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.65/1.29 % (2577293)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=305637659:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.65/1.29 % (2577280)Instruction limit reached! % 6.65/1.29 % (2577280)------------------------------ % 6.65/1.29 % (2577280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.29 % (2577280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.29 % (2577280)CaDiCaL version: 2.1.3 % 6.65/1.29 % (2577280)Termination reason: Instruction limit % 6.65/1.29 % (2577280)Termination phase: Saturation % 6.65/1.29 % (2577280)Time elapsed: 0.061 s % 6.65/1.29 % (2577280)Peak memory usage: 12 MB % 6.65/1.29 % (2577280)Instructions burned: 104 (million) % 6.65/1.29 % (2577293)Instruction limit reached! % 6.65/1.29 % (2577293)------------------------------ % 6.65/1.29 % (2577293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.29 % (2577293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.29 % (2577293)CaDiCaL version: 2.1.3 % 6.65/1.29 % (2577293)Termination reason: Instruction limit % 6.65/1.29 % (2577293)Termination phase: Saturation % 6.65/1.29 % (2577293)Time elapsed: 0.045 s % 6.65/1.29 % (2577293)Peak memory usage: 13 MB % 6.65/1.29 % (2577293)Instructions burned: 133 (million) % 6.65/1.29 % (2577281)Instruction limit reached! % 6.65/1.29 % (2577281)------------------------------ % 6.65/1.29 % (2577281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.29 % (2577281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.29 % (2577281)CaDiCaL version: 2.1.3 % 6.65/1.29 % (2577281)Termination reason: Instruction limit % 6.65/1.29 % (2577281)Termination phase: Saturation % 6.65/1.29 % (2577281)Time elapsed: 0.068 s % 6.65/1.29 % (2577281)Peak memory usage: 12 MB % 6.65/1.29 % (2577281)Instructions burned: 116 (million) % 6.65/1.29 % (2577296)ott-21_1_sil=16000:fs=off:random_seed=1254082665:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.65/1.29 % (2577295)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=72274351:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.65/1.29 % (2577282)Instruction limit reached! % 6.65/1.29 % (2577282)------------------------------ % 6.65/1.29 % (2577282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.29 % (2577282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.29 % (2577282)CaDiCaL version: 2.1.3 % 6.65/1.29 % (2577282)Termination reason: Instruction limit % 6.65/1.29 % (2577282)Termination phase: Saturation % 6.65/1.29 % (2577282)Time elapsed: 0.080 s % 6.65/1.29 % (2577282)Peak memory usage: 13 MB % 6.65/1.29 % (2577282)Instructions burned: 131 (million) % 6.65/1.29 % (2577297)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2470422906:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.87/3.07 % (2577283)Instruction limit reached! % 19.87/3.07 % (2577283)------------------------------ % 19.87/3.07 % (2577283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.87/3.07 % (2577283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.07 % (2577283)CaDiCaL version: 2.1.3 % 19.87/3.07 % (2577283)Termination reason: Instruction limit % 19.87/3.07 % (2577283)Termination phase: Saturation % 19.87/3.07 % (2577283)Time elapsed: 0.096 s % 19.87/3.07 % (2577283)Peak memory usage: 13 MB % 19.87/3.07 % (2577283)Instructions burned: 160 (million) % 19.87/3.07 % (2577300)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2802445168:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.87/3.07 % Exception at run slice level % 19.87/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.87/3.07 % (2577302)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1933970016:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.87/3.07 % (2577304)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1672060729:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.87/3.07 % (2577296)Instruction limit reached! % 19.87/3.07 % (2577296)------------------------------ % 19.87/3.07 % (2577296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.87/3.07 % (2577296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.07 % (2577296)CaDiCaL version: 2.1.3 % 19.87/3.07 % (2577296)Termination reason: Instruction limit % 19.87/3.07 % (2577296)Termination phase: Saturation % 19.87/3.07 % (2577296)Time elapsed: 0.050 s % 19.87/3.07 % (2577296)Peak memory usage: 13 MB % 19.87/3.07 % (2577296)Instructions burned: 182 (million) % 19.87/3.07 % Exception at run slice level % 19.87/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.87/3.07 % (2577307)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=672688688: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.87/3.07 % (2577308)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1998419504:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 19.87/3.07 % (2577307)Instruction limit reached! % 19.87/3.07 % (2577307)------------------------------ % 19.87/3.07 % (2577307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.87/3.07 % (2577307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.07 % (2577307)CaDiCaL version: 2.1.3 % 19.87/3.07 % (2577307)Termination reason: Instruction limit % 19.87/3.07 % (2577307)Termination phase: Saturation % 19.87/3.07 % (2577307)Time elapsed: 0.223 s % 19.87/3.07 % (2577307)Peak memory usage: 17 MB % 19.87/3.07 % (2577307)Instructions burned: 694 (million) % 19.87/3.07 % (2577297)Instruction limit reached! % 19.87/3.07 % (2577297)------------------------------ % 19.87/3.07 % (2577297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.87/3.07 % (2577297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.07 % (2577297)CaDiCaL version: 2.1.3 % 19.87/3.07 % (2577297)Termination reason: Instruction limit % 19.87/3.07 % (2577297)Termination phase: Saturation % 19.87/3.07 % (2577297)Time elapsed: 0.275 s % 19.87/3.07 % (2577297)Peak memory usage: 15 MB % 19.87/3.07 % (2577297)Instructions burned: 478 (million) % 19.87/3.07 % (2577311)fmb+10_1_sil=64000:random_seed=1144101175:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 19.87/3.07 % (2577311)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.87/3.07 % Exception at run slice level % 19.87/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.87/3.07 % (2577314)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=677238852:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.87/3.07 % Exception at run slice level % 19.87/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.87/3.07 % (2577312)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=155865650:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 19.87/3.07 % Exception at run slice level % 19.87/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.20/8.61 % (2577316)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1119640905:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 58.20/8.61 % (2577318)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2255007217:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 58.20/8.61 % (2577318)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.20/8.61 % (2577295)Instruction limit reached! % 58.20/8.61 % (2577295)------------------------------ % 58.20/8.61 % (2577295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.20/8.61 % (2577295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.20/8.61 % (2577295)CaDiCaL version: 2.1.3 % 58.20/8.61 % (2577295)Termination reason: Instruction limit % 58.20/8.61 % (2577295)Termination phase: Saturation % 58.20/8.61 % (2577295)Time elapsed: 0.361 s % 58.20/8.61 % (2577295)Peak memory usage: 16 MB % 58.20/8.61 % (2577295)Instructions burned: 685 (million) % 58.20/8.61 % (2577321)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4114727175:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 58.20/8.61 % Exception at run slice level % 58.20/8.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.20/8.61 % (2577323)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=256617429:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 58.20/8.61 % Exception at run slice level % 58.20/8.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.20/8.61 % (2577325)ott-2_1_sil=16000:newcnf=on:random_seed=2688317417:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 58.20/8.61 % (2577308)Instruction limit reached! % 58.20/8.61 % (2577308)------------------------------ % 58.20/8.61 % (2577308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.20/8.61 % (2577308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.20/8.61 % (2577308)CaDiCaL version: 2.1.3 % 58.20/8.61 % (2577308)Termination reason: Instruction limit % 58.20/8.61 % (2577308)Termination phase: Saturation % 58.20/8.61 % (2577308)Time elapsed: 0.463 s % 58.20/8.61 % (2577308)Peak memory usage: 19 MB % 58.20/8.61 % (2577308)Instructions burned: 879 (million) % 58.20/8.61 % (2577327)ott+10_1_sil=32000:tgt=ground:random_seed=834867734:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 58.20/8.61 % (2577302)Instruction limit reached! % 58.20/8.61 % (2577302)------------------------------ % 58.20/8.61 % (2577302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.20/8.61 % (2577302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.20/8.61 % (2577302)CaDiCaL version: 2.1.3 % 58.20/8.61 % (2577302)Termination reason: Instruction limit % 58.20/8.61 % (2577302)Termination phase: Saturation % 58.20/8.61 % (2577302)Time elapsed: 0.684 s % 58.20/8.61 % (2577302)Peak memory usage: 17 MB % 58.20/8.61 % (2577302)Instructions burned: 1180 (million) % 58.20/8.61 % (2577329)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1343308187:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 58.20/8.61 % Exception at run slice level % 58.20/8.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.20/8.61 % (2577331)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3434077176:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 58.20/8.61 % (2577318)Instruction limit reached! % 58.20/8.61 % (2577318)------------------------------ % 58.20/8.61 % (2577318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.20/8.61 % (2577318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.20/8.61 % (2577318)CaDiCaL version: 2.1.3 % 58.20/8.61 % (2577318)Termination reason: Instruction limit % 58.20/8.61 % (2577318)Termination phase: Saturation % 58.20/8.61 % (2577318)Time elapsed: 0.600 s % 58.20/8.61 % (2577318)Peak memory usage: 21 MB % 58.20/8.61 % (2577318)Instructions burned: 1475 (million) % 58.20/8.61 % (2577325)Instruction limit reached! % 58.20/8.61 % (2577325)------------------------------ % 58.20/8.61 % (2577325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.20/8.61 % (2577325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.74/17.10 % (2577325)CaDiCaL version: 2.1.3 % 113.74/17.10 % (2577325)Termination reason: Instruction limit % 113.74/17.10 % (2577325)Termination phase: Saturation % 113.74/17.10 % (2577325)Time elapsed: 0.505 s % 113.74/17.10 % (2577325)Peak memory usage: 17 MB % 113.74/17.10 % (2577325)Instructions burned: 870 (million) % 113.74/17.10 % (2577333)dis+21_1_sil=32000:sas=cadical:random_seed=1574144183:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 113.74/17.10 % (2577334)ott+11_1_sil=16000:gs=on:random_seed=3989360157:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 113.74/17.10 % (2577316)Instruction limit reached! % 113.74/17.10 % (2577316)------------------------------ % 113.74/17.10 % (2577316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.74/17.10 % (2577316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.74/17.10 % (2577316)CaDiCaL version: 2.1.3 % 113.74/17.10 % (2577316)Termination reason: Instruction limit % 113.74/17.10 % (2577316)Termination phase: Saturation % 113.74/17.10 % (2577316)Time elapsed: 1.388 s % 113.74/17.10 % (2577316)Peak memory usage: 31 MB % 113.74/17.10 % (2577316)Instructions burned: 5133 (million) % 113.74/17.10 % (2577337)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2909056834:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 113.74/17.10 % Exception at run slice level % 113.74/17.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.74/17.10 % (2577339)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3375927929:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 113.74/17.10 % (2577334)Instruction limit reached! % 113.74/17.10 % (2577334)------------------------------ % 113.74/17.10 % (2577334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.74/17.10 % (2577334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.74/17.10 % (2577334)CaDiCaL version: 2.1.3 % 113.74/17.10 % (2577334)Termination reason: Instruction limit % 113.74/17.10 % (2577334)Termination phase: Saturation % 113.74/17.10 % (2577334)Time elapsed: 1.173 s % 113.74/17.10 % (2577334)Peak memory usage: 20 MB % 113.74/17.10 % (2577334)Instructions burned: 2251 (million) % 113.74/17.10 % (2577341)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3406587539:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 113.74/17.10 % (2577331)Instruction limit reached! % 113.74/17.10 % (2577331)------------------------------ % 113.74/17.10 % (2577331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.74/17.10 % (2577331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.74/17.10 % (2577331)CaDiCaL version: 2.1.3 % 113.74/17.10 % (2577331)Termination reason: Instruction limit % 113.74/17.10 % (2577331)Termination phase: Saturation % 113.74/17.10 % (2577331)Time elapsed: 1.851 s % 113.74/17.10 % (2577331)Peak memory usage: 25 MB % 113.74/17.10 % (2577331)Instructions burned: 3513 (million) % 113.74/17.10 % (2577343)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3658506483:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 113.74/17.10 % (2577339)Instruction limit reached! % 113.74/17.10 % (2577339)------------------------------ % 113.74/17.10 % (2577339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.74/17.10 % (2577339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.74/17.10 % (2577339)CaDiCaL version: 2.1.3 % 113.74/17.10 % (2577339)Termination reason: Instruction limit % 113.74/17.10 % (2577339)Termination phase: Saturation % 113.74/17.10 % (2577339)Time elapsed: 0.922 s % 113.74/17.10 % (2577339)Peak memory usage: 29 MB % 113.74/17.10 % (2577339)Instructions burned: 4607 (million) % 113.74/17.10 % (2577345)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=567047493:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 113.74/17.10 % Exception at run slice level % 113.74/17.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.74/17.10 % (2577347)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3256475855:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 113.74/17.10 % Exception at run slice level % 113.74/17.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.74/17.10 % (2577349)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1759614391:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 113.74/17.10 % Exception at run slice level % 126.27/18.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.27/18.05 % (2577351)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1980425537:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 126.27/18.05 % (2577333)Instruction limit reached! % 126.27/18.05 % (2577333)------------------------------ % 126.27/18.05 % (2577333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577333)CaDiCaL version: 2.1.3 % 126.27/18.05 % (2577333)Termination reason: Instruction limit % 126.27/18.05 % (2577333)Termination phase: Saturation % 126.27/18.05 % (2577333)Time elapsed: 2.011 s % 126.27/18.05 % (2577333)Peak memory usage: 27 MB % 126.27/18.05 % (2577333)Instructions burned: 3774 (million) % 126.27/18.05 % (2577353)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=438968445:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 126.27/18.05 % (2577327)Instruction limit reached! % 126.27/18.05 % (2577327)------------------------------ % 126.27/18.05 % (2577327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577327)CaDiCaL version: 2.1.3 % 126.27/18.05 % (2577327)Termination reason: Instruction limit % 126.27/18.05 % (2577327)Termination phase: Saturation % 126.27/18.05 % (2577327)Time elapsed: 2.978 s % 126.27/18.05 % (2577327)Peak memory usage: 28 MB % 126.27/18.05 % (2577327)Instructions burned: 5115 (million) % 126.27/18.05 % (2577355)dis+10_16:1_sil=16000:random_seed=816687848:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 126.27/18.05 % (2577343)Instruction limit reached! % 126.27/18.05 % (2577343)------------------------------ % 126.27/18.05 % (2577343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577343)CaDiCaL version: 2.1.3 % 126.27/18.05 % (2577343)Termination reason: Instruction limit % 126.27/18.05 % (2577343)Termination phase: Saturation % 126.27/18.05 % (2577343)Time elapsed: 2.781 s % 126.27/18.05 % (2577343)Peak memory usage: 41 MB % 126.27/18.05 % (2577343)Instructions burned: 5212 (million) % 126.27/18.05 % (2577357)ott-3_8_sil=64000:random_seed=913478464:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 126.27/18.05 % (2577351)Instruction limit reached! % 126.27/18.05 % (2577351)------------------------------ % 126.27/18.05 % (2577351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577351)CaDiCaL version: 2.1.3 % 126.27/18.05 % (2577351)Termination reason: Instruction limit % 126.27/18.05 % (2577351)Termination phase: Saturation % 126.27/18.05 % (2577351)Time elapsed: 4.913 s % 126.27/18.05 % (2577351)Peak memory usage: 27 MB % 126.27/18.05 % (2577351)Instructions burned: 22568 (million) % 126.27/18.05 % (2577359)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2493758233:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 126.27/18.05 % Exception at run slice level % 126.27/18.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.27/18.05 % (2577361)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3299445587:i=11404_2922 on theBenchmark for (2922ds/11404Mi) % 126.27/18.05 % (2577353)Instruction limit reached! % 126.27/18.05 % (2577353)------------------------------ % 126.27/18.05 % (2577353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577353)CaDiCaL version: 2.1.3 % 126.27/18.05 % (2577353)Termination reason: Instruction limit % 126.27/18.05 % (2577353)Termination phase: Saturation % 126.27/18.05 % (2577353)Time elapsed: 4.749 s % 126.27/18.05 % (2577353)Peak memory usage: 35 MB % 126.27/18.05 % (2577353)Instructions burned: 8175 (million) % 126.27/18.05 % (2577363)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1841054061:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 126.27/18.05 % (2577355)Instruction limit reached! % 126.27/18.05 % (2577355)------------------------------ % 126.27/18.05 % (2577355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.05 % (2577355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.05 % (2577355)CaDiCaL version: 2.1.3 % 140.44/20.08 % (2577355)Termination reason: Instruction limit % 140.44/20.08 % (2577355)Termination phase: Saturation % 140.44/20.08 % (2577355)Time elapsed: 4.704 s % 140.44/20.08 % (2577355)Peak memory usage: 65 MB % 140.44/20.08 % (2577355)Instructions burned: 9155 (million) % 140.44/20.08 % (2577365)dis+33_16_sil=32000:sac=on:random_seed=1857639599:i=15851:nm=0_2916 on theBenchmark for (2916ds/15851Mi) % 140.44/20.08 % (2577361)Instruction limit reached! % 140.44/20.08 % (2577361)------------------------------ % 140.44/20.08 % (2577361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.44/20.08 % (2577361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.44/20.08 % (2577361)CaDiCaL version: 2.1.3 % 140.44/20.08 % (2577361)Termination reason: Instruction limit % 140.44/20.08 % (2577361)Termination phase: Saturation % 140.44/20.08 % (2577361)Time elapsed: 3.645 s % 140.44/20.08 % (2577361)Peak memory usage: 44 MB % 140.44/20.08 % (2577361)Instructions burned: 11404 (million) % 140.44/20.08 % (2577367)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1229839035:avsq=on:i=17627:add=on:amm=off_2885 on theBenchmark for (2885ds/17627Mi) % 140.44/20.08 % (2577341)Instruction limit reached! % 140.44/20.09 % (2577341)------------------------------ % 140.44/20.09 % (2577341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.44/20.09 % (2577341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.44/20.09 % (2577341)CaDiCaL version: 2.1.3 % 140.44/20.09 % (2577341)Termination reason: Instruction limit % 140.44/20.09 % (2577341)Termination phase: Saturation % 140.44/20.09 % (2577341)Time elapsed: 12.354 s % 140.44/20.09 % (2577341)Peak memory usage: 165 MB % 140.44/20.09 % (2577341)Instructions burned: 29342 (million) % 140.44/20.09 % (2577369)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=229055723:s2a=on:i=53295_2853 on theBenchmark for (2853ds/53295Mi) % 140.44/20.09 % (2577363)Instruction limit reached! % 140.44/20.09 % (2577363)------------------------------ % 140.44/20.09 % (2577363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.44/20.09 % (2577363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.44/20.09 % (2577363)CaDiCaL version: 2.1.3 % 140.44/20.09 % (2577363)Termination reason: Instruction limit % 140.44/20.09 % (2577363)Termination phase: Saturation % 140.44/20.09 % (2577363)Time elapsed: 8.482 s % 140.44/20.09 % (2577363)Peak memory usage: 45 MB % 140.44/20.09 % (2577363)Instructions burned: 14134 (million) % 140.44/20.09 % (2577371)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4064209134:i=26857:ins=20_2836 on theBenchmark for (2836ds/26857Mi) % 140.44/20.09 % Exception at run slice level % 140.44/20.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.44/20.09 % (2577373)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=146108733:i=28120:bs=on:fsr=off_2836 on theBenchmark for (2836ds/28120Mi) % 140.44/20.09 % (2577367)Instruction limit reached! % 140.44/20.09 % (2577367)------------------------------ % 140.44/20.09 % (2577367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.44/20.09 % (2577367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.44/20.09 % (2577367)CaDiCaL version: 2.1.3 % 140.44/20.09 % (2577367)Termination reason: Instruction limit % 140.44/20.09 % (2577367)Termination phase: Saturation % 140.44/20.09 % (2577367)Time elapsed: 5.353 s % 140.44/20.09 % (2577367)Peak memory usage: 216 MB % 140.44/20.09 % (2577367)Instructions burned: 17628 (million) % 140.44/20.09 % (2577375)fmb+10_1_sil=256000:fmbss=7:random_seed=139310091:fmbsr=1.6:i=182295_2831 on theBenchmark for (2831ds/182295Mi) % 140.44/20.09 % Exception at run slice level % 140.44/20.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.44/20.09 % (2577377)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3596909513:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 140.44/20.09 % (2577377)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 140.44/20.09 % Exception at run slice level % 140.44/20.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.44/20.09 % (2577379)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3642964111:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 140.44/20.09 % Exception at run slice level % 140.44/20.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 140.44/20.09 % (2577381)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2519239359:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 208.40/29.60 % Exception at run slice level % 208.40/29.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.40/29.60 % (2577383)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2303722969:fmbsr=2:i=185024:ins=7_2831 on theBenchmark for (2831ds/185024Mi) % 208.40/29.60 % Exception at run slice level % 208.40/29.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.40/29.60 % (2577385)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3404042150:rtra=on_2831 on theBenchmark for (2831ds/0Mi) % 208.40/29.60 % Exception at run slice level % 208.40/29.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.40/29.60 % (2577387)% WARNING: option uhcvi not known. % 208.40/29.60 % (2577387)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=222192173:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 208.40/29.60 % (2577365)Instruction limit reached! % 208.40/29.60 % (2577365)------------------------------ % 208.40/29.60 % (2577365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.40/29.60 % (2577365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.40/29.60 % (2577365)CaDiCaL version: 2.1.3 % 208.40/29.60 % (2577365)Termination reason: Instruction limit % 208.40/29.60 % (2577365)Termination phase: Saturation % 208.40/29.60 % (2577365)Time elapsed: 8.575 s % 208.40/29.60 % (2577365)Peak memory usage: 60 MB % 208.40/29.60 % (2577365)Instructions burned: 15852 (million) % 208.40/29.60 % (2577389)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4090095376:i=176048:add=on:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/176048Mi) % 208.40/29.60 % (2577357)Instruction limit reached! % 208.40/29.60 % (2577357)------------------------------ % 208.40/29.60 % (2577357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.40/29.60 % (2577357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.40/29.60 % (2577357)CaDiCaL version: 2.1.3 % 208.40/29.60 % (2577357)Termination reason: Instruction limit % 208.40/29.60 % (2577357)Termination phase: Saturation % 208.40/29.60 % (2577357)Time elapsed: 11.750 s % 208.40/29.60 % (2577357)Peak memory usage: 31 MB % 208.40/29.60 % (2577357)Instructions burned: 20139 (million) % 208.40/29.60 % (2577391)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2690202649:i=206:fgj=on:rtra=on_2826 on theBenchmark for (2826ds/206Mi) % 208.40/29.60 % (2577391)Instruction limit reached! % 208.40/29.60 % (2577391)------------------------------ % 208.40/29.60 % (2577391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.40/29.60 % (2577391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.40/29.60 % (2577391)CaDiCaL version: 2.1.3 % 208.40/29.60 % (2577391)Termination reason: Instruction limit % 208.40/29.60 % (2577391)Termination phase: Saturation % 208.40/29.60 % (2577391)Time elapsed: 0.125 s % 208.40/29.60 % (2577391)Peak memory usage: 13 MB % 208.40/29.60 % (2577391)Instructions burned: 206 (million) % 208.40/29.60 % (2577393)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4025761682:i=232:rtra=on_2825 on theBenchmark for (2825ds/232Mi) % 208.40/29.60 % (2577393)Instruction limit reached! % 208.40/29.60 % (2577393)------------------------------ % 208.40/29.60 % (2577393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.40/29.60 % (2577393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.40/29.60 % (2577393)CaDiCaL version: 2.1.3 % 208.40/29.60 % (2577393)Termination reason: Instruction limit % 208.40/29.60 % (2577393)Termination phase: Saturation % 208.40/29.60 % (2577393)Time elapsed: 0.141 s % 208.40/29.60 % (2577393)Peak memory usage: 13 MB % 208.40/29.60 % (2577393)Instructions burned: 232 (million) % 208.40/29.60 % (2577395)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=79838731:i=262:rtra=on_2823 on theBenchmark for (2823ds/262Mi) % 208.40/29.60 % (2577395)Instruction limit reached! % 208.40/29.60 % (2577395)------------------------------ % 208.40/29.60 % (2577395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.40/29.60 % (2577395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.40/29.60 % (2577395)CaDiCaL version: 2.1.3 % 208.40/29.60 % (2577395)Termination reason: Instruction limit % 208.40/29.60 % (2577395)Termination phase: Saturation % 273.72/38.87 % (2577395)Time elapsed: 0.166 s % 273.72/38.87 % (2577395)Peak memory usage: 14 MB % 273.72/38.87 % (2577395)Instructions burned: 263 (million) % 273.72/38.87 % (2577397)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2853860181:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2821 on theBenchmark for (2821ds/318Mi) % 273.72/38.87 % (2577397)Instruction limit reached! % 273.72/38.87 % (2577397)------------------------------ % 273.72/38.87 % (2577397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.72/38.87 % (2577397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.72/38.87 % (2577397)CaDiCaL version: 2.1.3 % 273.72/38.87 % (2577397)Termination reason: Instruction limit % 273.72/38.87 % (2577397)Termination phase: Saturation % 273.72/38.87 % (2577397)Time elapsed: 0.205 s % 273.72/38.87 % (2577397)Peak memory usage: 14 MB % 273.72/38.87 % (2577397)Instructions burned: 320 (million) % 273.72/38.87 % (2577399)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4020458722:i=1428:nm=2:rtra=on_2819 on theBenchmark for (2819ds/1428Mi) % 273.72/38.87 % Exception at run slice level % 273.72/38.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 273.72/38.87 % (2577401)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=378829474:i=262:bd=preordered:rtra=on:fsd=on_2819 on theBenchmark for (2819ds/262Mi) % 273.72/38.87 % (2577401)Instruction limit reached! % 273.72/38.87 % (2577401)------------------------------ % 273.72/38.87 % (2577401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.72/38.87 % (2577401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.72/38.87 % (2577401)CaDiCaL version: 2.1.3 % 273.72/38.87 % (2577401)Termination reason: Instruction limit % 273.72/38.87 % (2577401)Termination phase: Saturation % 273.72/38.87 % (2577401)Time elapsed: 0.174 s % 273.72/38.87 % (2577401)Peak memory usage: 14 MB % 273.72/38.87 % (2577401)Instructions burned: 264 (million) % 273.72/38.87 % (2577403)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=2052283754:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/1368Mi) % 273.72/38.87 % (2577403)Instruction limit reached! % 273.72/38.87 % (2577403)------------------------------ % 273.72/38.87 % (2577403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.72/38.87 % (2577403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.72/38.87 % (2577403)CaDiCaL version: 2.1.3 % 273.72/38.87 % (2577403)Termination reason: Instruction limit % 273.72/38.87 % (2577403)Termination phase: Saturation % 273.72/38.87 % (2577403)Time elapsed: 0.749 s % 273.72/38.87 % (2577403)Peak memory usage: 19 MB % 273.72/38.87 % (2577403)Instructions burned: 1369 (million) % 273.72/38.87 % (2577405)ott-21_1_sil=16000:si=on:fs=off:random_seed=3141660732:i=360:av=off:fsr=off:rtra=on_2809 on theBenchmark for (2809ds/360Mi) % 273.72/38.87 % (2577405)Instruction limit reached! % 273.72/38.87 % (2577405)------------------------------ % 273.72/38.87 % (2577405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.72/38.87 % (2577405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.72/38.87 % (2577405)CaDiCaL version: 2.1.3 % 273.72/38.87 % (2577405)Termination reason: Instruction limit % 273.72/38.87 % (2577405)Termination phase: Saturation % 273.72/38.87 % (2577405)Time elapsed: 0.182 s % 273.72/38.87 % (2577405)Peak memory usage: 15 MB % 273.72/38.87 % (2577405)Instructions burned: 360 (million) % 273.72/38.87 % (2577407)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1041966604:i=954:bd=all:rtra=on_2807 on theBenchmark for (2807ds/954Mi) % 273.72/38.87 % (2577407)Instruction limit reached! % 273.72/38.87 % (2577407)------------------------------ % 273.72/38.87 % (2577407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.72/38.87 % (2577407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.72/38.87 % (2577407)CaDiCaL version: 2.1.3 % 273.72/38.87 % (2577407)Termination reason: Instruction limit % 273.72/38.87 % (2577407)Termination phase: Saturation % 273.72/38.87 % (2577407)Time elapsed: 0.565 s % 273.72/38.87 % (2577407)Peak memory usage: 16 MB % 273.72/38.87 % (2577407)Instructions burned: 955 (million) % 273.72/38.87 % (2577409)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1161078629:fmbsr=1.3:i=1730:ins=25:rtra=on_2801 on theBenchmark for (2801ds/1730Mi) % 273.72/38.87 % Exception at run slice level % 273.72/38.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.56/42.52 % (2577411)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3335619355:i=2358:rtra=on_2801 on theBenchmark for (2801ds/2358Mi) % 299.56/42.52 % (2577411)Instruction limit reached! % 299.56/42.52 % (2577411)------------------------------ % 299.56/42.52 % (2577411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.56/42.52 % (2577411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.56/42.52 % (2577411)CaDiCaL version: 2.1.3 % 299.56/42.52 % (2577411)Termination reason: Instruction limit % 299.56/42.52 % (2577411)Termination phase: Saturation % 299.56/42.52 % (2577411)Time elapsed: 1.454 s % 299.56/42.52 % (2577411)Peak memory usage: 18 MB % 299.56/42.52 % (2577411)Instructions burned: 2358 (million) % 299.56/42.52 % (2577413)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=379295709:i=1778:ins=1:rtra=on_2786 on theBenchmark for (2786ds/1778Mi) % 299.56/42.52 % Exception at run slice level % 299.56/42.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.56/42.52 % (2577415)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=1780123339:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1384Mi) % 299.56/42.52 % (2577415)Instruction limit reached! % 299.56/42.52 % (2577415)------------------------------ % 299.56/42.52 % (2577415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.56/42.52 % (2577415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.56/42.52 % (2577415)CaDiCaL version: 2.1.3 % 299.56/42.52 % (2577415)Termination reason: Instruction limit % 299.56/42.52 % (2577415)Termination phase: Saturation % 299.56/42.52 % (2577415)Time elapsed: 0.875 s % 299.56/42.52 % (2577415)Peak memory usage: 20 MB % 299.56/42.52 % (2577415)Instructions burned: 1384 (million) % 299.56/42.52 % (2577417)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2345395888:i=1758:kws=inv_precedence:fsr=off:rtra=on_2777 on theBenchmark for (2777ds/1758Mi) % 299.56/42.52 % (2577417)Instruction limit reached! % 299.56/42.52 % (2577417)------------------------------ % 299.56/42.52 % (2577417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.56/42.52 % (2577417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.56/42.52 % (2577417)CaDiCaL version: 2.1.3 % 299.56/42.52 % (2577417)Termination reason: Instruction limit % 299.56/42.52 % (2577417)Termination phase: Saturation % 299.56/42.52 % (2577417)Time elapsed: 0.969 s % 299.56/42.52 % (2577417)Peak memory usage: 24 MB % 299.56/42.52 % (2577417)Instructions burned: 1758 (million) % 299.56/42.52 % (2577419)fmb+10_1_sil=64000:si=on:random_seed=1759238130:i=44122:nm=2:rtra=on:gsp=on_2767 on theBenchmark for (2767ds/44122Mi) % 299.56/42.52 % (2577419)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 299.56/42.52 % Exception at run slice level % 299.56/42.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.56/42.52 % (2577421)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3361130425:i=19030:nm=5:rtra=on_2767 on theBenchmark for (2767ds/19030Mi) % 299.56/42.52 % Exception at run slice level % 299.56/42.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.56/42.52 % (2577423)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2140564387:fmbsr=1.7:i=1840:rtra=on_2767 on theBenchmark for (2767ds/1840Mi) % 299.56/42.52 % Exception at run slice level % 299.56/42.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.56/42.52 % (2577425)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4156836723:i=10262:rtra=on_2766 on theBenchmark for (2766ds/10262Mi) % 299.56/42.52 % (2577425)Instruction limit reached! % 299.56/42.52 % (2577425)------------------------------ % 299.56/42.52 % (2577425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.56/42.52 % (2577425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.56/42.52 % (2577425)CaDiCaL version: 2.1.3 % 299.56/42.52 % (2577425)Termination reason: Instruction limit % 299.56/42.52 % (2577425)Termination phase: Saturation % 299.56/42.52 % (2577425)Time elapsed: 6.035 s % 299.56/42.52 % (2577425)Peak memory usage: 42 MB % 299.56/42.52 % (2577Terminated % 300.12/42.63 % Vampire exiting %------------------------------------------------------------------------------