%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW540_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:24 PM UTC 2026 % Result : Timeout 300.15s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW540_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n002.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 14:20:52 UTC 2026 % 0.07/0.17 % CPUTime : % 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 Running first-order model finding % 0.07/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.96/1.48 % (379319)Will run a generic schedule for satisfiability detection. % 7.96/1.48 % (379329)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=730846422:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.96/1.48 % (379325)% WARNING: option uhcvi not known. % 7.96/1.48 % (379324)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4188651986_2999 on theBenchmark for (2999ds/0Mi) % 7.96/1.48 % (379326)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1510184055:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.96/1.48 % (379327)dis+10_1_sil=32000:sp=arity:random_seed=765952595:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.96/1.48 % (379328)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=873825280:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.96/1.48 % (379330)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3448911696:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.96/1.48 % (379325)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1148266259:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.96/1.48 % Exception at run slice level % 7.96/1.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.96/1.48 % (379338)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1747110553:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.96/1.48 % Exception at run slice level % 7.96/1.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.96/1.48 % (379329)Instruction limit reached! % 7.96/1.48 % (379329)------------------------------ % 7.96/1.48 % (379329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.96/1.48 % (379329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.48 % (379329)CaDiCaL version: 2.1.3 % 7.96/1.48 % (379329)Termination reason: Instruction limit % 7.96/1.48 % (379329)Termination phase: Saturation % 7.96/1.48 % (379329)Time elapsed: 0.044 s % 7.96/1.48 % (379329)Peak memory usage: 13 MB % 7.96/1.48 % (379329)Instructions burned: 132 (million) % 7.96/1.48 % (379341)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=4077067045:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.96/1.48 % (379340)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3901381992:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.96/1.48 % (379327)Instruction limit reached! % 7.96/1.48 % (379327)------------------------------ % 7.96/1.48 % (379327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.96/1.48 % (379327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.48 % (379327)CaDiCaL version: 2.1.3 % 7.96/1.48 % (379327)Termination reason: Instruction limit % 7.96/1.48 % (379327)Termination phase: Saturation % 7.96/1.48 % (379327)Time elapsed: 0.059 s % 7.96/1.48 % (379327)Peak memory usage: 12 MB % 7.96/1.48 % (379327)Instructions burned: 103 (million) % 7.96/1.48 % (379328)Instruction limit reached! % 7.96/1.48 % (379328)------------------------------ % 7.96/1.48 % (379328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.96/1.48 % (379328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.48 % (379328)CaDiCaL version: 2.1.3 % 7.96/1.48 % (379328)Termination reason: Instruction limit % 7.96/1.48 % (379328)Termination phase: Saturation % 7.96/1.48 % (379328)Time elapsed: 0.065 s % 7.96/1.48 % (379328)Peak memory usage: 12 MB % 7.96/1.48 % (379328)Instructions burned: 117 (million) % 7.96/1.48 % (379344)ott-21_1_sil=16000:fs=off:random_seed=168615061:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.96/1.48 % (379345)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1745151046:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 7.96/1.48 % (379330)Instruction limit reached! % 7.96/1.48 % (379330)------------------------------ % 7.96/1.48 % (379330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.96/1.48 % (379330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.48 % (379330)CaDiCaL version: 2.1.3 % 7.96/1.48 % (379330)Termination reason: Instruction limit % 7.96/1.48 % (379330)Termination phase: Saturation % 7.96/1.48 % (379330)Time elapsed: 0.090 s % 7.96/1.48 % (379330)Peak memory usage: 13 MB % 19.98/3.08 % (379330)Instructions burned: 161 (million) % 19.98/3.08 % (379348)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1773281306:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.98/3.08 % Exception at run slice level % 19.98/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.98/3.08 % (379340)Instruction limit reached! % 19.98/3.08 % (379340)------------------------------ % 19.98/3.08 % (379340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.98/3.08 % (379340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.08 % (379340)CaDiCaL version: 2.1.3 % 19.98/3.08 % (379340)Termination reason: Instruction limit % 19.98/3.08 % (379340)Termination phase: Saturation % 19.98/3.08 % (379340)Time elapsed: 0.084 s % 19.98/3.08 % (379340)Peak memory usage: 13 MB % 19.98/3.08 % (379340)Instructions burned: 132 (million) % 19.98/3.08 % (379350)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1012122111:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.98/3.08 % (379351)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=368188782:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.98/3.08 % Exception at run slice level % 19.98/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.98/3.08 % (379344)Instruction limit reached! % 19.98/3.08 % (379344)------------------------------ % 19.98/3.08 % (379344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.98/3.08 % (379344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.08 % (379344)CaDiCaL version: 2.1.3 % 19.98/3.08 % (379344)Termination reason: Instruction limit % 19.98/3.08 % (379344)Termination phase: Saturation % 19.98/3.08 % (379344)Time elapsed: 0.089 s % 19.98/3.08 % (379344)Peak memory usage: 12 MB % 19.98/3.08 % (379344)Instructions burned: 181 (million) % 19.98/3.08 % (379354)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=3491623366: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.98/3.08 % (379355)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2533378751:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.98/3.08 % (379341)Instruction limit reached! % 19.98/3.08 % (379341)------------------------------ % 19.98/3.08 % (379341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.98/3.08 % (379341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.08 % (379341)CaDiCaL version: 2.1.3 % 19.98/3.08 % (379341)Termination reason: Instruction limit % 19.98/3.08 % (379341)Termination phase: Saturation % 19.98/3.08 % (379341)Time elapsed: 0.175 s % 19.98/3.08 % (379341)Peak memory usage: 15 MB % 19.98/3.08 % (379341)Instructions burned: 685 (million) % 19.98/3.08 % (379358)fmb+10_1_sil=64000:random_seed=2951630168:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 19.98/3.08 % (379358)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.98/3.08 % Exception at run slice level % 19.98/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.98/3.08 % (379360)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2739003114:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 19.98/3.08 % Exception at run slice level % 19.98/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.98/3.08 % (379362)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2789817743:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 19.98/3.08 % Exception at run slice level % 19.98/3.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.98/3.08 % (379364)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3061769549:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 19.98/3.08 % (379345)Instruction limit reached! % 19.98/3.08 % (379345)------------------------------ % 19.98/3.08 % (379345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.98/3.08 % (379345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.08 % (379345)CaDiCaL version: 2.1.3 % 19.98/3.08 % (379345)Termination reason: Instruction limit % 19.98/3.08 % (379345)Termination phase: Saturation % 63.74/9.29 % (379345)Time elapsed: 0.281 s % 63.74/9.29 % (379345)Peak memory usage: 15 MB % 63.74/9.29 % (379345)Instructions burned: 478 (million) % 63.74/9.29 % (379366)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2813889595:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 63.74/9.29 % (379366)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 63.74/9.29 % (379354)Instruction limit reached! % 63.74/9.29 % (379354)------------------------------ % 63.74/9.29 % (379354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.74/9.29 % (379354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.74/9.29 % (379354)CaDiCaL version: 2.1.3 % 63.74/9.29 % (379354)Termination reason: Instruction limit % 63.74/9.29 % (379354)Termination phase: Saturation % 63.74/9.29 % (379354)Time elapsed: 0.354 s % 63.74/9.29 % (379354)Peak memory usage: 16 MB % 63.74/9.29 % (379354)Instructions burned: 693 (million) % 63.74/9.29 % (379368)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1557789080:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 63.74/9.29 % Exception at run slice level % 63.74/9.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.74/9.29 % (379370)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=592825936:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 63.74/9.29 % Exception at run slice level % 63.74/9.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.74/9.29 % (379372)ott-2_1_sil=16000:newcnf=on:random_seed=1686481351:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 63.74/9.29 % (379355)Instruction limit reached! % 63.74/9.29 % (379355)------------------------------ % 63.74/9.29 % (379355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.74/9.29 % (379355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.74/9.29 % (379355)CaDiCaL version: 2.1.3 % 63.74/9.29 % (379355)Termination reason: Instruction limit % 63.74/9.29 % (379355)Termination phase: Saturation % 63.74/9.29 % (379355)Time elapsed: 0.503 s % 63.74/9.29 % (379355)Peak memory usage: 18 MB % 63.74/9.29 % (379355)Instructions burned: 880 (million) % 63.74/9.29 % (379374)ott+10_1_sil=32000:tgt=ground:random_seed=1667053767:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 63.74/9.29 % (379350)Instruction limit reached! % 63.74/9.29 % (379350)------------------------------ % 63.74/9.29 % (379350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.74/9.29 % (379350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.74/9.29 % (379350)CaDiCaL version: 2.1.3 % 63.74/9.29 % (379350)Termination reason: Instruction limit % 63.74/9.29 % (379350)Termination phase: Saturation % 63.74/9.29 % (379350)Time elapsed: 0.607 s % 63.74/9.29 % (379350)Peak memory usage: 17 MB % 63.74/9.29 % (379350)Instructions burned: 1181 (million) % 63.74/9.29 % (379376)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2525634625:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 63.74/9.29 % Exception at run slice level % 63.74/9.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.74/9.29 % (379378)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3726582550:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 63.74/9.29 % (379372)Instruction limit reached! % 63.74/9.29 % (379372)------------------------------ % 63.74/9.29 % (379372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.74/9.29 % (379372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.74/9.29 % (379372)CaDiCaL version: 2.1.3 % 63.74/9.29 % (379372)Termination reason: Instruction limit % 63.74/9.29 % (379372)Termination phase: Saturation % 63.74/9.29 % (379372)Time elapsed: 0.505 s % 63.74/9.29 % (379372)Peak memory usage: 16 MB % 63.74/9.29 % (379372)Instructions burned: 870 (million) % 63.74/9.29 % (379380)dis+21_1_sil=32000:sas=cadical:random_seed=2482207678:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 63.74/9.29 % (379366)Instruction limit reached! % 63.74/9.29 % (379366)------------------------------ % 63.74/9.29 % (379366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.74/9.29 % (379366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.74/9.29 % (379366)CaDiCaL version: 2.1.3 % 112.26/16.06 % (379366)Termination reason: Instruction limit % 112.26/16.06 % (379366)Termination phase: Saturation % 112.26/16.06 % (379366)Time elapsed: 0.849 s % 112.26/16.06 % (379366)Peak memory usage: 30 MB % 112.26/16.06 % (379366)Instructions burned: 1474 (million) % 112.26/16.06 % (379382)ott+11_1_sil=16000:gs=on:random_seed=1796679580:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 112.26/16.06 % (379364)Instruction limit reached! % 112.26/16.06 % (379364)------------------------------ % 112.26/16.06 % (379364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.26/16.06 % (379364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.06 % (379364)CaDiCaL version: 2.1.3 % 112.26/16.06 % (379364)Termination reason: Instruction limit % 112.26/16.06 % (379364)Termination phase: Saturation % 112.26/16.06 % (379364)Time elapsed: 1.405 s % 112.26/16.06 % (379364)Peak memory usage: 44 MB % 112.26/16.06 % (379364)Instructions burned: 5131 (million) % 112.26/16.06 % (379384)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3169815871:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 112.26/16.06 % Exception at run slice level % 112.26/16.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.26/16.06 % (379386)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=709470516:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 112.26/16.06 % (379382)Instruction limit reached! % 112.26/16.06 % (379382)------------------------------ % 112.26/16.06 % (379382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.26/16.06 % (379382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.06 % (379382)CaDiCaL version: 2.1.3 % 112.26/16.06 % (379382)Termination reason: Instruction limit % 112.26/16.06 % (379382)Termination phase: Saturation % 112.26/16.06 % (379382)Time elapsed: 1.097 s % 112.26/16.06 % (379382)Peak memory usage: 17 MB % 112.26/16.06 % (379382)Instructions burned: 2252 (million) % 112.26/16.06 % (379388)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1266638580:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 112.26/16.06 % (379378)Instruction limit reached! % 112.26/16.06 % (379378)------------------------------ % 112.26/16.06 % (379378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.26/16.06 % (379378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.06 % (379378)CaDiCaL version: 2.1.3 % 112.26/16.06 % (379378)Termination reason: Instruction limit % 112.26/16.06 % (379378)Termination phase: Saturation % 112.26/16.06 % (379378)Time elapsed: 1.838 s % 112.26/16.06 % (379378)Peak memory usage: 33 MB % 112.26/16.06 % (379378)Instructions burned: 3513 (million) % 112.26/16.06 % (379390)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2727769248:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 112.26/16.06 % (379386)Instruction limit reached! % 112.26/16.06 % (379386)------------------------------ % 112.26/16.06 % (379386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.26/16.06 % (379386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.06 % (379386)CaDiCaL version: 2.1.3 % 112.26/16.06 % (379386)Termination reason: Instruction limit % 112.26/16.06 % (379386)Termination phase: Saturation % 112.26/16.06 % (379386)Time elapsed: 1.044 s % 112.26/16.06 % (379386)Peak memory usage: 29 MB % 112.26/16.06 % (379386)Instructions burned: 4596 (million) % 112.26/16.06 % (379392)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3899458205:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 112.26/16.06 % Exception at run slice level % 112.26/16.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.26/16.06 % (379394)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=978047983:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 112.26/16.06 % Exception at run slice level % 112.26/16.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.26/16.06 % (379396)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=574168170:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 112.26/16.06 % Exception at run slice level % 112.26/16.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.26/16.06 % (379398)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3463932876:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 124.82/17.90 % (379380)Instruction limit reached! % 124.82/17.90 % (379380)------------------------------ % 124.82/17.90 % (379380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379380)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379380)Termination reason: Instruction limit % 124.82/17.90 % (379380)Termination phase: Saturation % 124.82/17.90 % (379380)Time elapsed: 1.965 s % 124.82/17.90 % (379380)Peak memory usage: 34 MB % 124.82/17.90 % (379380)Instructions burned: 3774 (million) % 124.82/17.90 % (379400)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3375544613:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 124.82/17.90 % (379374)Instruction limit reached! % 124.82/17.90 % (379374)------------------------------ % 124.82/17.90 % (379374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379374)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379374)Termination reason: Instruction limit % 124.82/17.90 % (379374)Termination phase: Saturation % 124.82/17.90 % (379374)Time elapsed: 2.830 s % 124.82/17.90 % (379374)Peak memory usage: 50 MB % 124.82/17.90 % (379374)Instructions burned: 5114 (million) % 124.82/17.90 % (379402)dis+10_16:1_sil=16000:random_seed=1111267960:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 124.82/17.90 % (379390)Instruction limit reached! % 124.82/17.90 % (379390)------------------------------ % 124.82/17.90 % (379390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379390)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379390)Termination reason: Instruction limit % 124.82/17.90 % (379390)Termination phase: Saturation % 124.82/17.90 % (379390)Time elapsed: 2.809 s % 124.82/17.90 % (379390)Peak memory usage: 45 MB % 124.82/17.90 % (379390)Instructions burned: 5212 (million) % 124.82/17.90 % (379404)ott-3_8_sil=64000:random_seed=147735443:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 124.82/17.90 % (379400)Instruction limit reached! % 124.82/17.90 % (379400)------------------------------ % 124.82/17.90 % (379400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379400)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379400)Termination reason: Instruction limit % 124.82/17.90 % (379400)Termination phase: Saturation % 124.82/17.90 % (379400)Time elapsed: 4.508 s % 124.82/17.90 % (379400)Peak memory usage: 70 MB % 124.82/17.90 % (379400)Instructions burned: 8173 (million) % 124.82/17.90 % (379406)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=161981432:fmbsr=2:i=32576_2923 on theBenchmark for (2923ds/32576Mi) % 124.82/17.90 % Exception at run slice level % 124.82/17.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.82/17.90 % (379408)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=898082209:i=11404_2923 on theBenchmark for (2923ds/11404Mi) % 124.82/17.90 % (379402)Instruction limit reached! % 124.82/17.90 % (379402)------------------------------ % 124.82/17.90 % (379402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379402)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379402)Termination reason: Instruction limit % 124.82/17.90 % (379402)Termination phase: Saturation % 124.82/17.90 % (379402)Time elapsed: 4.771 s % 124.82/17.90 % (379402)Peak memory usage: 52 MB % 124.82/17.90 % (379402)Instructions burned: 9156 (million) % 124.82/17.90 % (379410)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1068627266:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 124.82/17.90 % (379398)Instruction limit reached! % 124.82/17.90 % (379398)------------------------------ % 124.82/17.90 % (379398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.82/17.90 % (379398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.82/17.90 % (379398)CaDiCaL version: 2.1.3 % 124.82/17.90 % (379398)Termination reason: Instruction limit % 124.82/17.90 % (379398)Termination phase: Saturation % 124.82/17.90 % (379398)Time elapsed: 6.184 s % 124.82/17.90 % (379398)Peak memory usage: 115 MB % 124.82/17.90 % (379398)Instructions burned: 22567 (million) % 124.82/17.90 % (379412)dis+33_16_sil=32000:sac=on:random_seed=848178511:i=15851:nm=0_2909 on theBenchmark for (2909ds/15851Mi) % 136.15/19.47 % (379412)Instruction limit reached! % 136.15/19.47 % (379412)------------------------------ % 136.15/19.47 % (379412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.15/19.47 % (379412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.15/19.47 % (379412)CaDiCaL version: 2.1.3 % 136.15/19.47 % (379412)Termination reason: Instruction limit % 136.15/19.47 % (379412)Termination phase: Saturation % 136.15/19.47 % (379412)Time elapsed: 4.098 s % 136.15/19.47 % (379412)Peak memory usage: 88 MB % 136.15/19.47 % (379412)Instructions burned: 15855 (million) % 136.15/19.47 % (379414)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=325808278:avsq=on:i=17627:add=on:amm=off_2868 on theBenchmark for (2868ds/17627Mi) % 136.15/19.47 % (379404)Instruction limit reached! % 136.15/19.47 % (379404)------------------------------ % 136.15/19.47 % (379404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.15/19.47 % (379404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.15/19.47 % (379404)CaDiCaL version: 2.1.3 % 136.15/19.47 % (379404)Termination reason: Instruction limit % 136.15/19.47 % (379404)Termination phase: Saturation % 136.15/19.47 % (379404)Time elapsed: 9.036 s % 136.15/19.47 % (379404)Peak memory usage: 35 MB % 136.15/19.47 % (379404)Instructions burned: 20140 (million) % 136.15/19.47 % (379416)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3227530879:s2a=on:i=53295_2854 on theBenchmark for (2854ds/53295Mi) % 136.15/19.47 % (379408)Instruction limit reached! % 136.15/19.47 % (379408)------------------------------ % 136.15/19.47 % (379408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.15/19.47 % (379408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.15/19.47 % (379408)CaDiCaL version: 2.1.3 % 136.15/19.47 % (379408)Termination reason: Instruction limit % 136.15/19.47 % (379408)Termination phase: Saturation % 136.15/19.47 % (379408)Time elapsed: 7.018 s % 136.15/19.47 % (379408)Peak memory usage: 98 MB % 136.15/19.47 % (379408)Instructions burned: 11404 (million) % 136.15/19.47 % (379418)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2537828675:i=26857:ins=20_2852 on theBenchmark for (2852ds/26857Mi) % 136.15/19.47 % Exception at run slice level % 136.15/19.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 136.15/19.47 % (379420)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3775870086:i=28120:bs=on:fsr=off_2852 on theBenchmark for (2852ds/28120Mi) % 136.15/19.47 % (379410)Instruction limit reached! % 136.15/19.47 % (379410)------------------------------ % 136.15/19.47 % (379410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.15/19.47 % (379410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.15/19.47 % (379410)CaDiCaL version: 2.1.3 % 136.15/19.47 % (379410)Termination reason: Instruction limit % 136.15/19.47 % (379410)Termination phase: Saturation % 136.15/19.47 % (379410)Time elapsed: 7.327 s % 136.15/19.47 % (379410)Peak memory usage: 78 MB % 136.15/19.47 % (379410)Instructions burned: 14135 (million) % 136.15/19.47 % (379422)fmb+10_1_sil=256000:fmbss=7:random_seed=2097346671:fmbsr=1.6:i=182295_2842 on theBenchmark for (2842ds/182295Mi) % 136.15/19.47 % Exception at run slice level % 136.15/19.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 136.15/19.47 % (379424)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1666688299:i=44625:gsp=on_2842 on theBenchmark for (2842ds/44625Mi) % 136.15/19.47 % (379424)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 136.15/19.47 % Exception at run slice level % 136.15/19.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 136.15/19.47 % (379426)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1723886689:i=160505_2842 on theBenchmark for (2842ds/160505Mi) % 136.15/19.47 % Exception at run slice level % 136.15/19.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 136.15/19.47 % (379428)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1370589065:fmbsr=1.3:i=225729_2841 on theBenchmark for (2841ds/225729Mi) % 136.15/19.47 % Exception at run slice level % 136.15/19.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 136.15/19.47 % (379430)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3194059654:fmbsr=2:i=185024:ins=7_2841 on theBenchmark for (2841ds/185024Mi) % 169.05/24.11 % Exception at run slice level % 169.05/24.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.05/24.11 % (379432)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2646504821:rtra=on_2841 on theBenchmark for (2841ds/0Mi) % 169.05/24.11 % Exception at run slice level % 169.05/24.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.05/24.11 % (379434)% WARNING: option uhcvi not known. % 169.05/24.11 % (379434)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3145946845:i=271062:add=off:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/271062Mi) % 169.05/24.11 % (379388)Instruction limit reached! % 169.05/24.11 % (379388)------------------------------ % 169.05/24.11 % (379388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.05/24.11 % (379388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.05/24.11 % (379388)CaDiCaL version: 2.1.3 % 169.05/24.11 % (379388)Termination reason: Instruction limit % 169.05/24.11 % (379388)Termination phase: Saturation % 169.05/24.11 % (379388)Time elapsed: 13.841 s % 169.05/24.11 % (379388)Peak memory usage: 143 MB % 169.05/24.11 % (379388)Instructions burned: 29340 (million) % 169.05/24.11 % (379436)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1547572016:i=176048:add=on:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/176048Mi) % 169.05/24.11 % (379414)Instruction limit reached! % 169.05/24.11 % (379414)------------------------------ % 169.05/24.11 % (379414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.05/24.11 % (379414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.05/24.11 % (379414)CaDiCaL version: 2.1.3 % 169.05/24.11 % (379414)Termination reason: Instruction limit % 169.05/24.11 % (379414)Termination phase: Saturation % 169.05/24.11 % (379414)Time elapsed: 4.120 s % 169.05/24.11 % (379414)Peak memory usage: 72 MB % 169.05/24.11 % (379414)Instructions burned: 17632 (million) % 169.05/24.11 % (379438)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3261141421:i=206:fgj=on:rtra=on_2826 on theBenchmark for (2826ds/206Mi) % 169.05/24.11 % (379438)Instruction limit reached! % 169.05/24.11 % (379438)------------------------------ % 169.05/24.11 % (379438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.05/24.11 % (379438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.05/24.11 % (379438)CaDiCaL version: 2.1.3 % 169.05/24.11 % (379438)Termination reason: Instruction limit % 169.05/24.11 % (379438)Termination phase: Saturation % 169.05/24.11 % (379438)Time elapsed: 0.066 s % 169.05/24.11 % (379438)Peak memory usage: 13 MB % 169.05/24.11 % (379438)Instructions burned: 206 (million) % 169.05/24.11 % (379440)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=541048757:i=232:rtra=on_2826 on theBenchmark for (2826ds/232Mi) % 169.05/24.11 % (379440)Instruction limit reached! % 169.05/24.11 % (379440)------------------------------ % 169.05/24.11 % (379440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.05/24.11 % (379440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.05/24.11 % (379440)CaDiCaL version: 2.1.3 % 169.05/24.11 % (379440)Termination reason: Instruction limit % 169.05/24.11 % (379440)Termination phase: Saturation % 169.05/24.11 % (379440)Time elapsed: 0.069 s % 169.05/24.11 % (379440)Peak memory usage: 13 MB % 169.05/24.11 % (379440)Instructions burned: 235 (million) % 169.05/24.11 % (379442)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=398058222:i=262:rtra=on_2825 on theBenchmark for (2825ds/262Mi) % 169.05/24.11 % (379442)Instruction limit reached! % 169.05/24.11 % (379442)------------------------------ % 169.05/24.11 % (379442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.05/24.11 % (379442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.05/24.11 % (379442)CaDiCaL version: 2.1.3 % 169.05/24.11 % (379442)Termination reason: Instruction limit % 169.05/24.11 % (379442)Termination phase: Saturation % 169.05/24.11 % (379442)Time elapsed: 0.088 s % 169.05/24.11 % (379442)Peak memory usage: 14 MB % 169.05/24.11 % (379442)Instructions burned: 265 (million) % 169.05/24.11 % (379444)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=7388226:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2824 on theBenchmark for (2824ds/318Mi) % 169.05/24.11 % (379444)Instruction limit reached! % 169.05/24.11 % (379444)------------------------------ % 169.05/24.11 % (379444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.93/31.29 % (379444)CaDiCaL version: 2.1.3 % 219.93/31.29 % (379444)Termination reason: Instruction limit % 219.93/31.29 % (379444)Termination phase: Saturation % 219.93/31.29 % (379444)Time elapsed: 0.097 s % 219.93/31.29 % (379444)Peak memory usage: 13 MB % 219.93/31.29 % (379444)Instructions burned: 321 (million) % 219.93/31.29 % (379446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1478474028:i=1428:nm=2:rtra=on_2823 on theBenchmark for (2823ds/1428Mi) % 219.93/31.29 % Exception at run slice level % 219.93/31.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.93/31.29 % (379448)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2692207858:i=262:bd=preordered:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/262Mi) % 219.93/31.29 % (379448)Instruction limit reached! % 219.93/31.29 % (379448)------------------------------ % 219.93/31.29 % (379448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.93/31.29 % (379448)CaDiCaL version: 2.1.3 % 219.93/31.29 % (379448)Termination reason: Instruction limit % 219.93/31.29 % (379448)Termination phase: Saturation % 219.93/31.29 % (379448)Time elapsed: 0.083 s % 219.93/31.29 % (379448)Peak memory usage: 14 MB % 219.93/31.29 % (379448)Instructions burned: 264 (million) % 219.93/31.29 % (379450)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=1935285571:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/1368Mi) % 219.93/31.29 % (379450)Instruction limit reached! % 219.93/31.29 % (379450)------------------------------ % 219.93/31.29 % (379450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.93/31.29 % (379450)CaDiCaL version: 2.1.3 % 219.93/31.29 % (379450)Termination reason: Instruction limit % 219.93/31.29 % (379450)Termination phase: Saturation % 219.93/31.29 % (379450)Time elapsed: 0.363 s % 219.93/31.29 % (379450)Peak memory usage: 19 MB % 219.93/31.29 % (379450)Instructions burned: 1369 (million) % 219.93/31.29 % (379452)ott-21_1_sil=16000:si=on:fs=off:random_seed=2297485008:i=360:av=off:fsr=off:rtra=on_2818 on theBenchmark for (2818ds/360Mi) % 219.93/31.29 % (379452)Instruction limit reached! % 219.93/31.29 % (379452)------------------------------ % 219.93/31.29 % (379452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.93/31.29 % (379452)CaDiCaL version: 2.1.3 % 219.93/31.29 % (379452)Termination reason: Instruction limit % 219.93/31.29 % (379452)Termination phase: Saturation % 219.93/31.29 % (379452)Time elapsed: 0.086 s % 219.93/31.29 % (379452)Peak memory usage: 13 MB % 219.93/31.29 % (379452)Instructions burned: 362 (million) % 219.93/31.29 % (379454)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=323492604:i=954:bd=all:rtra=on_2817 on theBenchmark for (2817ds/954Mi) % 219.93/31.29 % (379454)Instruction limit reached! % 219.93/31.29 % (379454)------------------------------ % 219.93/31.29 % (379454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.93/31.29 % (379454)CaDiCaL version: 2.1.3 % 219.93/31.29 % (379454)Termination reason: Instruction limit % 219.93/31.29 % (379454)Termination phase: Saturation % 219.93/31.29 % (379454)Time elapsed: 0.307 s % 219.93/31.29 % (379454)Peak memory usage: 16 MB % 219.93/31.29 % (379454)Instructions burned: 956 (million) % 219.93/31.29 % (379456)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1759089085:fmbsr=1.3:i=1730:ins=25:rtra=on_2814 on theBenchmark for (2814ds/1730Mi) % 219.93/31.29 % Exception at run slice level % 219.93/31.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.93/31.29 % (379458)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=474945135:i=2358:rtra=on_2813 on theBenchmark for (2813ds/2358Mi) % 219.93/31.29 % (379458)Instruction limit reached! % 219.93/31.29 % (379458)------------------------------ % 219.93/31.29 % (379458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.93/31.29 % (379458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.42/39.36 % (379458)CaDiCaL version: 2.1.3 % 277.42/39.36 % (379458)Termination reason: Instruction limit % 277.42/39.36 % (379458)Termination phase: Saturation % 277.42/39.36 % (379458)Time elapsed: 0.646 s % 277.42/39.36 % (379458)Peak memory usage: 21 MB % 277.42/39.36 % (379458)Instructions burned: 2361 (million) % 277.42/39.36 % (379460)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3595770061:i=1778:ins=1:rtra=on_2807 on theBenchmark for (2807ds/1778Mi) % 277.42/39.36 % Exception at run slice level % 277.42/39.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.42/39.36 % (379462)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=4017575434:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/1384Mi) % 277.42/39.36 % (379462)Instruction limit reached! % 277.42/39.36 % (379462)------------------------------ % 277.42/39.36 % (379462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.42/39.36 % (379462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.42/39.36 % (379462)CaDiCaL version: 2.1.3 % 277.42/39.36 % (379462)Termination reason: Instruction limit % 277.42/39.36 % (379462)Termination phase: Saturation % 277.42/39.36 % (379462)Time elapsed: 0.353 s % 277.42/39.36 % (379462)Peak memory usage: 18 MB % 277.42/39.36 % (379462)Instructions burned: 1385 (million) % 277.42/39.36 % (379464)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=226457971:i=1758:kws=inv_precedence:fsr=off:rtra=on_2803 on theBenchmark for (2803ds/1758Mi) % 277.42/39.36 % (379464)Instruction limit reached! % 277.42/39.36 % (379464)------------------------------ % 277.42/39.36 % (379464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.42/39.36 % (379464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.42/39.36 % (379464)CaDiCaL version: 2.1.3 % 277.42/39.36 % (379464)Termination reason: Instruction limit % 277.42/39.36 % (379464)Termination phase: Saturation % 277.42/39.36 % (379464)Time elapsed: 0.535 s % 277.42/39.36 % (379464)Peak memory usage: 23 MB % 277.42/39.36 % (379464)Instructions burned: 1759 (million) % 277.42/39.36 % (379466)fmb+10_1_sil=64000:si=on:random_seed=1576562037:i=44122:nm=2:rtra=on:gsp=on_2798 on theBenchmark for (2798ds/44122Mi) % 277.42/39.36 % (379466)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 277.42/39.36 % Exception at run slice level % 277.42/39.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.42/39.36 % (379468)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2611198405:i=19030:nm=5:rtra=on_2798 on theBenchmark for (2798ds/19030Mi) % 277.42/39.36 % Exception at run slice level % 277.42/39.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.42/39.36 % (379470)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=329844710:fmbsr=1.7:i=1840:rtra=on_2797 on theBenchmark for (2797ds/1840Mi) % 277.42/39.36 % Exception at run slice level % 277.42/39.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.42/39.36 % (379472)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=442147032:i=10262:rtra=on_2797 on theBenchmark for (2797ds/10262Mi) % 277.42/39.36 % (379472)Instruction limit reached! % 277.42/39.36 % (379472)------------------------------ % 277.42/39.36 % (379472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.42/39.36 % (379472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.42/39.36 % (379472)CaDiCaL version: 2.1.3 % 277.42/39.36 % (379472)Termination reason: Instruction limit % 277.42/39.36 % (379472)Termination phase: Saturation % 277.42/39.36 % (379472)Time elapsed: 2.912 s % 277.42/39.36 % (379472)Peak memory usage: 60 MB % 277.42/39.36 % (379472)Instructions burned: 10265 (million) % 277.42/39.36 % (379474)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1335879323:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2768 on theBenchmark for (2768ds/2944Mi) % 277.42/39.36 % (379474)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 277.42/39.36 % (379474)Instruction limit reached! % 277.42/39.36 % (379474)------------------------------ % 277.42/39.36 % (379474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2Terminated % 300.15/42.54 % Vampire exiting %------------------------------------------------------------------------------