%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW554_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 : n010.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:26 PM UTC 2026 % Result : Timeout 300.20s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW554_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.28 % Computer : n010.cluster.edu % 0.11/0.28 % Model : x86_64 x86_64 % 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.28 % Memory : 8046.5625MB % 0.11/0.28 % OS : Linux 6.8.0-71-generic % 0.11/0.28 % CPULimit : 300 % 0.11/0.28 % WCLimit : 300 % 0.11/0.28 % DateTime : Mon Sep 28 14:19:32 UTC 2026 % 0.12/0.28 % CPUTime : % 0.12/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.32 Running first-order model finding % 0.12/0.32 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 % 14.04/2.35 % (1949821)Will run a generic schedule for satisfiability detection. % 14.04/2.35 % (1949832)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1296985685:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.04/2.35 % (1949827)% WARNING: option uhcvi not known. % 14.04/2.35 % (1949827)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4152204772:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.04/2.35 % (1949828)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=47749464:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.04/2.35 % (1949829)dis+10_1_sil=32000:sp=arity:random_seed=249280723:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.04/2.35 % (1949826)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2597928754_2999 on theBenchmark for (2999ds/0Mi) % 14.04/2.35 % (1949830)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2319304526:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.04/2.35 % (1949831)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=823202295:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.04/2.35 % Exception at run slice level % 14.04/2.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.04/2.35 % (1949840)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1485250287:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.04/2.35 % Exception at run slice level % 14.04/2.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.04/2.35 % (1949842)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=979372886:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 14.04/2.35 % (1949832)Instruction limit reached! % 14.04/2.35 % (1949832)------------------------------ % 14.04/2.35 % (1949832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.04/2.35 % (1949832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.04/2.35 % (1949832)CaDiCaL version: 2.1.3 % 14.04/2.35 % (1949832)Termination reason: Instruction limit % 14.04/2.35 % (1949832)Termination phase: Saturation % 14.04/2.35 % (1949832)Time elapsed: 0.088 s % 14.04/2.35 % (1949832)Peak memory usage: 13 MB % 14.04/2.35 % (1949832)Instructions burned: 161 (million) % 14.04/2.35 % (1949829)Instruction limit reached! % 14.04/2.35 % (1949829)------------------------------ % 14.04/2.35 % (1949829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.04/2.35 % (1949829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.04/2.35 % (1949829)CaDiCaL version: 2.1.3 % 14.04/2.35 % (1949829)Termination reason: Instruction limit % 14.04/2.35 % (1949829)Termination phase: Saturation % 14.04/2.35 % (1949829)Time elapsed: 0.100 s % 14.04/2.35 % (1949829)Peak memory usage: 12 MB % 14.04/2.35 % (1949829)Instructions burned: 103 (million) % 14.04/2.35 % (1949845)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=365427199:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.04/2.35 % (1949830)Instruction limit reached! % 14.04/2.35 % (1949830)------------------------------ % 14.04/2.35 % (1949830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.04/2.35 % (1949830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.04/2.35 % (1949830)CaDiCaL version: 2.1.3 % 14.04/2.35 % (1949830)Termination reason: Instruction limit % 14.04/2.35 % (1949830)Termination phase: Saturation % 14.04/2.35 % (1949830)Time elapsed: 0.115 s % 14.04/2.35 % (1949830)Peak memory usage: 13 MB % 14.04/2.35 % (1949830)Instructions burned: 116 (million) % 14.04/2.35 % (1949831)Instruction limit reached! % 14.04/2.35 % (1949831)------------------------------ % 14.04/2.35 % (1949831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.04/2.35 % (1949831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.04/2.35 % (1949831)CaDiCaL version: 2.1.3 % 14.04/2.35 % (1949831)Termination reason: Instruction limit % 14.04/2.35 % (1949831)Termination phase: Saturation % 14.04/2.35 % (1949831)Time elapsed: 0.130 s % 14.04/2.35 % (1949831)Peak memory usage: 13 MB % 14.04/2.35 % (1949831)Instructions burned: 131 (million) % 14.04/2.35 % (1949847)ott-21_1_sil=16000:fs=off:random_seed=2885164293:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.04/2.35 % (1949850)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=827214676:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 36.84/5.60 % (1949851)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3001099551:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 36.84/5.60 % Exception at run slice level % 36.84/5.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 36.84/5.60 % (1949842)Instruction limit reached! % 36.84/5.60 % (1949842)------------------------------ % 36.84/5.60 % (1949842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.84/5.60 % (1949842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.84/5.60 % (1949842)CaDiCaL version: 2.1.3 % 36.84/5.60 % (1949842)Termination reason: Instruction limit % 36.84/5.60 % (1949842)Termination phase: Saturation % 36.84/5.60 % (1949842)Time elapsed: 0.127 s % 36.84/5.60 % (1949842)Peak memory usage: 12 MB % 36.84/5.60 % (1949842)Instructions burned: 131 (million) % 36.84/5.60 % (1949856)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3422068665:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 36.84/5.60 % (1949857)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3170421781:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 36.84/5.60 % Exception at run slice level % 36.84/5.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 36.84/5.60 % (1949861)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=2140539224:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 36.84/5.60 % (1949847)Instruction limit reached! % 36.84/5.60 % (1949847)------------------------------ % 36.84/5.60 % (1949847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.84/5.60 % (1949847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.84/5.60 % (1949847)CaDiCaL version: 2.1.3 % 36.84/5.60 % (1949847)Termination reason: Instruction limit % 36.84/5.60 % (1949847)Termination phase: Saturation % 36.84/5.60 % (1949847)Time elapsed: 0.162 s % 36.84/5.60 % (1949847)Peak memory usage: 13 MB % 36.84/5.60 % (1949847)Instructions burned: 181 (million) % 36.84/5.60 % (1949866)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=827565514:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 36.84/5.60 % (1949845)Instruction limit reached! % 36.84/5.60 % (1949845)------------------------------ % 36.84/5.60 % (1949845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.84/5.60 % (1949845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.84/5.60 % (1949845)CaDiCaL version: 2.1.3 % 36.84/5.60 % (1949845)Termination reason: Instruction limit % 36.84/5.60 % (1949845)Termination phase: Saturation % 36.84/5.60 % (1949845)Time elapsed: 0.321 s % 36.84/5.60 % (1949845)Peak memory usage: 15 MB % 36.84/5.60 % (1949845)Instructions burned: 684 (million) % 36.84/5.60 % (1949868)fmb+10_1_sil=64000:random_seed=3758154472:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 36.84/5.60 % (1949868)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 36.84/5.60 % Exception at run slice level % 36.84/5.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 36.84/5.60 % (1949870)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3304613464:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 36.84/5.60 % Exception at run slice level % 36.84/5.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 36.84/5.60 % (1949872)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1007172287:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 36.84/5.60 % Exception at run slice level % 36.84/5.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 36.84/5.60 % (1949874)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1499710424:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 36.84/5.60 % (1949850)Instruction limit reached! % 36.84/5.60 % (1949850)------------------------------ % 36.84/5.60 % (1949850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.84/5.60 % (1949850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.32/15.20 % (1949850)CaDiCaL version: 2.1.3 % 105.32/15.20 % (1949850)Termination reason: Instruction limit % 105.32/15.20 % (1949850)Termination phase: Saturation % 105.32/15.20 % (1949850)Time elapsed: 0.488 s % 105.32/15.20 % (1949850)Peak memory usage: 14 MB % 105.32/15.20 % (1949850)Instructions burned: 478 (million) % 105.32/15.20 % (1949876)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=753753434:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 105.32/15.20 % (1949876)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 105.32/15.20 % (1949861)Instruction limit reached! % 105.32/15.20 % (1949861)------------------------------ % 105.32/15.20 % (1949861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.32/15.20 % (1949861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.32/15.20 % (1949861)CaDiCaL version: 2.1.3 % 105.32/15.20 % (1949861)Termination reason: Instruction limit % 105.32/15.20 % (1949861)Termination phase: Saturation % 105.32/15.20 % (1949861)Time elapsed: 0.698 s % 105.32/15.20 % (1949861)Peak memory usage: 16 MB % 105.32/15.20 % (1949861)Instructions burned: 692 (million) % 105.32/15.20 % (1949878)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=294933644:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 105.32/15.20 % Exception at run slice level % 105.32/15.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.32/15.20 % (1949880)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1388063929:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 105.32/15.20 % Exception at run slice level % 105.32/15.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.32/15.20 % (1949882)ott-2_1_sil=16000:newcnf=on:random_seed=2424817888:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 105.32/15.20 % (1949866)Instruction limit reached! % 105.32/15.20 % (1949866)------------------------------ % 105.32/15.20 % (1949866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.32/15.20 % (1949866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.32/15.20 % (1949866)CaDiCaL version: 2.1.3 % 105.32/15.20 % (1949866)Termination reason: Instruction limit % 105.32/15.20 % (1949866)Termination phase: Saturation % 105.32/15.20 % (1949866)Time elapsed: 0.822 s % 105.32/15.20 % (1949866)Peak memory usage: 19 MB % 105.32/15.20 % (1949866)Instructions burned: 879 (million) % 105.32/15.20 % (1949884)ott+10_1_sil=32000:tgt=ground:random_seed=1767448732:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 105.32/15.20 % (1949856)Instruction limit reached! % 105.32/15.20 % (1949856)------------------------------ % 105.32/15.20 % (1949856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.32/15.20 % (1949856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.32/15.20 % (1949856)CaDiCaL version: 2.1.3 % 105.32/15.20 % (1949856)Termination reason: Instruction limit % 105.32/15.20 % (1949856)Termination phase: Saturation % 105.32/15.20 % (1949856)Time elapsed: 1.163 s % 105.32/15.20 % (1949856)Peak memory usage: 20 MB % 105.32/15.20 % (1949856)Instructions burned: 1179 (million) % 105.32/15.20 % (1949886)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3196190118:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 105.32/15.20 % Exception at run slice level % 105.32/15.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.32/15.20 % (1949888)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1429216574:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 105.32/15.20 % (1949882)Instruction limit reached! % 105.32/15.20 % (1949882)------------------------------ % 105.32/15.20 % (1949882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.32/15.20 % (1949882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.32/15.20 % (1949882)CaDiCaL version: 2.1.3 % 105.32/15.20 % (1949882)Termination reason: Instruction limit % 105.32/15.20 % (1949882)Termination phase: Saturation % 105.32/15.20 % (1949882)Time elapsed: 0.768 s % 105.32/15.20 % (1949882)Peak memory usage: 14 MB % 105.32/15.20 % (1949882)Instructions burned: 869 (million) % 105.32/15.20 % (1949892)dis+21_1_sil=32000:sas=cadical:random_seed=1029837432:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 105.32/15.20 % (1949876)Instruction limit reached! % 105.32/15.20 % (1949876)------------------------------ % 105.32/15.20 % (1949876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.75/21.46 % (1949876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.75/21.46 % (1949876)CaDiCaL version: 2.1.3 % 149.75/21.46 % (1949876)Termination reason: Instruction limit % 149.75/21.46 % (1949876)Termination phase: Saturation % 149.75/21.46 % (1949876)Time elapsed: 1.305 s % 149.75/21.46 % (1949876)Peak memory usage: 19 MB % 149.75/21.46 % (1949876)Instructions burned: 1473 (million) % 149.75/21.46 % (1949894)ott+11_1_sil=16000:gs=on:random_seed=3232674353:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 149.75/21.46 % (1949874)Instruction limit reached! % 149.75/21.46 % (1949874)------------------------------ % 149.75/21.46 % (1949874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.75/21.46 % (1949874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.75/21.46 % (1949874)CaDiCaL version: 2.1.3 % 149.75/21.46 % (1949874)Termination reason: Instruction limit % 149.75/21.46 % (1949874)Termination phase: Saturation % 149.75/21.46 % (1949874)Time elapsed: 2.561 s % 149.75/21.46 % (1949874)Peak memory usage: 36 MB % 149.75/21.46 % (1949874)Instructions burned: 5131 (million) % 149.75/21.46 % (1949904)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3298189724:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 149.75/21.46 % Exception at run slice level % 149.75/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.75/21.46 % (1949906)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1374885888:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 149.75/21.46 % (1949894)Instruction limit reached! % 149.75/21.46 % (1949894)------------------------------ % 149.75/21.46 % (1949894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.75/21.46 % (1949894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.75/21.46 % (1949894)CaDiCaL version: 2.1.3 % 149.75/21.46 % (1949894)Termination reason: Instruction limit % 149.75/21.46 % (1949894)Termination phase: Saturation % 149.75/21.46 % (1949894)Time elapsed: 1.813 s % 149.75/21.46 % (1949894)Peak memory usage: 14 MB % 149.75/21.46 % (1949894)Instructions burned: 2251 (million) % 149.75/21.46 % (1949910)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3736409460:i=29340_2961 on theBenchmark for (2961ds/29340Mi) % 149.75/21.46 % (1949888)Instruction limit reached! % 149.75/21.46 % (1949888)------------------------------ % 149.75/21.46 % (1949888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.75/21.46 % (1949888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.75/21.46 % (1949888)CaDiCaL version: 2.1.3 % 149.75/21.46 % (1949888)Termination reason: Instruction limit % 149.75/21.46 % (1949888)Termination phase: Saturation % 149.75/21.46 % (1949888)Time elapsed: 3.078 s % 149.75/21.46 % (1949888)Peak memory usage: 28 MB % 149.75/21.46 % (1949888)Instructions burned: 3512 (million) % 149.75/21.46 % (1949912)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2570116689:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 149.75/21.46 % (1949906)Instruction limit reached! % 149.75/21.46 % (1949906)------------------------------ % 149.75/21.46 % (1949906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.75/21.46 % (1949906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.75/21.46 % (1949906)CaDiCaL version: 2.1.3 % 149.75/21.46 % (1949906)Termination reason: Instruction limit % 149.75/21.46 % (1949906)Termination phase: Saturation % 149.75/21.46 % (1949906)Time elapsed: 1.979 s % 149.75/21.46 % (1949906)Peak memory usage: 29 MB % 149.75/21.46 % (1949906)Instructions burned: 4591 (million) % 149.75/21.46 % (1949914)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3219750547:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 149.75/21.46 % Exception at run slice level % 149.75/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.75/21.46 % (1949916)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1971359651:fmbsr=2:i=46332_2947 on theBenchmark for (2947ds/46332Mi) % 149.75/21.46 % Exception at run slice level % 149.75/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.75/21.46 % (1949918)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=755063122:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 149.75/21.46 % Exception at run slice level % 173.18/24.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 173.18/24.77 % (1949920)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2095520180:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 173.18/24.77 % (1949892)Instruction limit reached! % 173.18/24.77 % (1949892)------------------------------ % 173.18/24.77 % (1949892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949892)CaDiCaL version: 2.1.3 % 173.18/24.77 % (1949892)Termination reason: Instruction limit % 173.18/24.77 % (1949892)Termination phase: Saturation % 173.18/24.77 % (1949892)Time elapsed: 3.526 s % 173.18/24.77 % (1949892)Peak memory usage: 31 MB % 173.18/24.77 % (1949892)Instructions burned: 3773 (million) % 173.18/24.77 % (1949922)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1310688937:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi) % 173.18/24.77 % (1949884)Instruction limit reached! % 173.18/24.77 % (1949884)------------------------------ % 173.18/24.77 % (1949884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949884)CaDiCaL version: 2.1.3 % 173.18/24.77 % (1949884)Termination reason: Instruction limit % 173.18/24.77 % (1949884)Termination phase: Saturation % 173.18/24.77 % (1949884)Time elapsed: 4.759 s % 173.18/24.77 % (1949884)Peak memory usage: 35 MB % 173.18/24.77 % (1949884)Instructions burned: 5114 (million) % 173.18/24.77 % (1949924)dis+10_16:1_sil=16000:random_seed=2009751143:i=9155:fsr=off_2939 on theBenchmark for (2939ds/9155Mi) % 173.18/24.77 % (1949912)Instruction limit reached! % 173.18/24.77 % (1949912)------------------------------ % 173.18/24.77 % (1949912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949912)CaDiCaL version: 2.1.3 % 173.18/24.77 % (1949912)Termination reason: Instruction limit % 173.18/24.77 % (1949912)Termination phase: Saturation % 173.18/24.77 % (1949912)Time elapsed: 4.281 s % 173.18/24.77 % (1949912)Peak memory usage: 44 MB % 173.18/24.77 % (1949912)Instructions burned: 5211 (million) % 173.18/24.77 % (1949934)ott-3_8_sil=64000:random_seed=701592549:i=20139:bs=on_2911 on theBenchmark for (2911ds/20139Mi) % 173.18/24.77 % (1949922)Instruction limit reached! % 173.18/24.77 % (1949922)------------------------------ % 173.18/24.77 % (1949922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949922)CaDiCaL version: 2.1.3 % 173.18/24.77 % (1949922)Termination reason: Instruction limit % 173.18/24.77 % (1949922)Termination phase: Saturation % 173.18/24.77 % (1949922)Time elapsed: 7.799 s % 173.18/24.77 % (1949922)Peak memory usage: 72 MB % 173.18/24.77 % (1949922)Instructions burned: 8173 (million) % 173.18/24.77 % (1950095)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1321868587:fmbsr=2:i=32576_2867 on theBenchmark for (2867ds/32576Mi) % 173.18/24.77 % Exception at run slice level % 173.18/24.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 173.18/24.77 % (1950102)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2274567809:i=11404_2866 on theBenchmark for (2866ds/11404Mi) % 173.18/24.77 % (1949924)Instruction limit reached! % 173.18/24.77 % (1949924)------------------------------ % 173.18/24.77 % (1949924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949924)CaDiCaL version: 2.1.3 % 173.18/24.77 % (1949924)Termination reason: Instruction limit % 173.18/24.77 % (1949924)Termination phase: Saturation % 173.18/24.77 % (1949924)Time elapsed: 7.594 s % 173.18/24.77 % (1949924)Peak memory usage: 54 MB % 173.18/24.77 % (1949924)Instructions burned: 9155 (million) % 173.18/24.77 % (1950104)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2978810883:i=14134_2863 on theBenchmark for (2863ds/14134Mi) % 173.18/24.77 % (1949920)Instruction limit reached! % 173.18/24.77 % (1949920)------------------------------ % 173.18/24.77 % (1949920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.18/24.77 % (1949920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.18/24.77 % (1949920)CaDiCaL version: 2.1.3 % 180.70/25.84 % (1949920)Termination reason: Instruction limit % 180.70/25.84 % (1949920)Termination phase: Saturation % 180.70/25.84 % (1949920)Time elapsed: 9.585 s % 180.70/25.84 % (1949920)Peak memory usage: 73 MB % 180.70/25.84 % (1949920)Instructions burned: 22565 (million) % 180.70/25.84 % (1950106)dis+33_16_sil=32000:sac=on:random_seed=4167788315:i=15851:nm=0_2851 on theBenchmark for (2851ds/15851Mi) % 180.70/25.84 % (1950106)Instruction limit reached! % 180.70/25.84 % (1950106)------------------------------ % 180.70/25.84 % (1950106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.70/25.84 % (1950106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.70/25.84 % (1950106)CaDiCaL version: 2.1.3 % 180.70/25.84 % (1950106)Termination reason: Instruction limit % 180.70/25.84 % (1950106)Termination phase: Saturation % 180.70/25.84 % (1950106)Time elapsed: 4.049 s % 180.70/25.84 % (1950106)Peak memory usage: 38 MB % 180.70/25.84 % (1950106)Instructions burned: 15851 (million) % 180.70/25.84 % (1950110)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2521399283:avsq=on:i=17627:add=on:amm=off_2810 on theBenchmark for (2810ds/17627Mi) % 180.70/25.84 % (1949934)Instruction limit reached! % 180.70/25.84 % (1949934)------------------------------ % 180.70/25.84 % (1949934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.70/25.84 % (1949934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.70/25.84 % (1949934)CaDiCaL version: 2.1.3 % 180.70/25.84 % (1949934)Termination reason: Instruction limit % 180.70/25.84 % (1949934)Termination phase: Saturation % 180.70/25.84 % (1949934)Time elapsed: 11.125 s % 180.70/25.84 % (1949934)Peak memory usage: 24 MB % 180.70/25.84 % (1949934)Instructions burned: 20139 (million) % 180.70/25.84 % (1950112)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2861892319:s2a=on:i=53295_2799 on theBenchmark for (2799ds/53295Mi) % 180.70/25.84 % (1950102)Instruction limit reached! % 180.70/25.84 % (1950102)------------------------------ % 180.70/25.84 % (1950102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.70/25.84 % (1950102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.70/25.84 % (1950102)CaDiCaL version: 2.1.3 % 180.70/25.84 % (1950102)Termination reason: Instruction limit % 180.70/25.84 % (1950102)Termination phase: Saturation % 180.70/25.84 % (1950102)Time elapsed: 7.139 s % 180.70/25.84 % (1950102)Peak memory usage: 89 MB % 180.70/25.84 % (1950102)Instructions burned: 11404 (million) % 180.70/25.84 % (1950114)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4291519490:i=26857:ins=20_2795 on theBenchmark for (2795ds/26857Mi) % 180.70/25.84 % Exception at run slice level % 180.70/25.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.70/25.84 % (1950116)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2956258382:i=28120:bs=on:fsr=off_2794 on theBenchmark for (2794ds/28120Mi) % 180.70/25.84 % (1949910)Instruction limit reached! % 180.70/25.84 % (1949910)------------------------------ % 180.70/25.84 % (1949910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.70/25.84 % (1949910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.70/25.84 % (1949910)CaDiCaL version: 2.1.3 % 180.70/25.84 % (1949910)Termination reason: Instruction limit % 180.70/25.84 % (1949910)Termination phase: Saturation % 180.70/25.84 % (1949910)Time elapsed: 17.135 s % 180.70/25.84 % (1949910)Peak memory usage: 57 MB % 180.70/25.84 % (1949910)Instructions burned: 29341 (million) % 180.70/25.84 % (1950118)fmb+10_1_sil=256000:fmbss=7:random_seed=1700752973:fmbsr=1.6:i=182295_2789 on theBenchmark for (2789ds/182295Mi) % 180.70/25.84 % Exception at run slice level % 180.70/25.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.70/25.84 % (1950120)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2105363304:i=44625:gsp=on_2789 on theBenchmark for (2789ds/44625Mi) % 180.70/25.84 % (1950120)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 180.70/25.84 % Exception at run slice level % 180.70/25.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.70/25.84 % (1950122)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2450006002:i=160505_2789 on theBenchmark for (2789ds/160505Mi) % 180.70/25.84 % Exception at run slice level % 180.70/25.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.70/25.84 % (1950124)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1735884972:fmbsr=1.3:i=225729_2788 on theBenchmark for (2788ds/225729Mi) % 218.14/31.04 % Exception at run slice level % 218.14/31.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 218.14/31.04 % (1950126)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=623183012:fmbsr=2:i=185024:ins=7_2788 on theBenchmark for (2788ds/185024Mi) % 218.14/31.04 % Exception at run slice level % 218.14/31.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 218.14/31.04 % (1950128)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=811489099:rtra=on_2788 on theBenchmark for (2788ds/0Mi) % 218.14/31.04 % Exception at run slice level % 218.14/31.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 218.14/31.04 % (1950130)% WARNING: option uhcvi not known. % 218.14/31.04 % (1950130)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2966124835:i=271062:add=off:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/271062Mi) % 218.14/31.04 % (1950104)Instruction limit reached! % 218.14/31.04 % (1950104)------------------------------ % 218.14/31.04 % (1950104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.14/31.04 % (1950104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.14/31.04 % (1950104)CaDiCaL version: 2.1.3 % 218.14/31.04 % (1950104)Termination reason: Instruction limit % 218.14/31.04 % (1950104)Termination phase: Saturation % 218.14/31.04 % (1950104)Time elapsed: 8.193 s % 218.14/31.04 % (1950104)Peak memory usage: 66 MB % 218.14/31.04 % (1950104)Instructions burned: 14134 (million) % 218.14/31.04 % (1950132)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2999769692:i=176048:add=on:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/176048Mi) % 218.14/31.04 % (1950110)Instruction limit reached! % 218.14/31.04 % (1950110)------------------------------ % 218.14/31.04 % (1950110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.14/31.04 % (1950110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.14/31.04 % (1950110)CaDiCaL version: 2.1.3 % 218.14/31.04 % (1950110)Termination reason: Instruction limit % 218.14/31.04 % (1950110)Termination phase: Saturation % 218.14/31.04 % (1950110)Time elapsed: 5.210 s % 218.14/31.04 % (1950110)Peak memory usage: 42 MB % 218.14/31.04 % (1950110)Instructions burned: 17629 (million) % 218.14/31.04 % (1950134)dis+10_1_sil=32000:si=on:sp=arity:random_seed=757025569:i=206:fgj=on:rtra=on_2758 on theBenchmark for (2758ds/206Mi) % 218.14/31.04 % (1950134)Instruction limit reached! % 218.14/31.04 % (1950134)------------------------------ % 218.14/31.04 % (1950134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.14/31.04 % (1950134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.14/31.04 % (1950134)CaDiCaL version: 2.1.3 % 218.14/31.04 % (1950134)Termination reason: Instruction limit % 218.14/31.04 % (1950134)Termination phase: Saturation % 218.14/31.04 % (1950134)Time elapsed: 0.067 s % 218.14/31.04 % (1950134)Peak memory usage: 13 MB % 218.14/31.04 % (1950134)Instructions burned: 207 (million) % 218.14/31.04 % (1950136)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=81179552:i=232:rtra=on_2757 on theBenchmark for (2757ds/232Mi) % 218.14/31.04 % (1950136)Instruction limit reached! % 218.14/31.04 % (1950136)------------------------------ % 218.14/31.04 % (1950136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.14/31.04 % (1950136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.14/31.04 % (1950136)CaDiCaL version: 2.1.3 % 218.14/31.04 % (1950136)Termination reason: Instruction limit % 218.14/31.04 % (1950136)Termination phase: Saturation % 218.14/31.04 % (1950136)Time elapsed: 0.077 s % 218.14/31.04 % (1950136)Peak memory usage: 13 MB % 218.14/31.04 % (1950136)Instructions burned: 235 (million) % 218.14/31.04 % (1950138)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1213953736:i=262:rtra=on_2756 on theBenchmark for (2756ds/262Mi) % 218.14/31.04 % (1950138)Instruction limit reached! % 218.14/31.04 % (1950138)------------------------------ % 218.14/31.04 % (1950138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.14/31.04 % (1950138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.14/31.04 % (1950138)CaDiCaL version: 2.1.3 % 218.14/31.04 % (1950138)Termination reason: Instruction limit % 218.14/31.04 % (1950138)Termination phase: Saturation % 259.07/36.85 % (1950138)Time elapsed: 0.088 s % 259.07/36.85 % (1950138)Peak memory usage: 14 MB % 259.07/36.85 % (1950138)Instructions burned: 263 (million) % 259.07/36.85 % (1950140)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2589062183:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2755 on theBenchmark for (2755ds/318Mi) % 259.07/36.85 % (1950140)Instruction limit reached! % 259.07/36.85 % (1950140)------------------------------ % 259.07/36.85 % (1950140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.07/36.85 % (1950140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.07/36.85 % (1950140)CaDiCaL version: 2.1.3 % 259.07/36.85 % (1950140)Termination reason: Instruction limit % 259.07/36.85 % (1950140)Termination phase: Saturation % 259.07/36.85 % (1950140)Time elapsed: 0.097 s % 259.07/36.85 % (1950140)Peak memory usage: 13 MB % 259.07/36.85 % (1950140)Instructions burned: 319 (million) % 259.07/36.85 % (1950142)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=308724716:i=1428:nm=2:rtra=on_2754 on theBenchmark for (2754ds/1428Mi) % 259.07/36.85 % Exception at run slice level % 259.07/36.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.07/36.85 % (1950144)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3131429868:i=262:bd=preordered:rtra=on:fsd=on_2754 on theBenchmark for (2754ds/262Mi) % 259.07/36.85 % (1950144)Instruction limit reached! % 259.07/36.85 % (1950144)------------------------------ % 259.07/36.85 % (1950144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.07/36.85 % (1950144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.07/36.85 % (1950144)CaDiCaL version: 2.1.3 % 259.07/36.85 % (1950144)Termination reason: Instruction limit % 259.07/36.85 % (1950144)Termination phase: Saturation % 259.07/36.85 % (1950144)Time elapsed: 0.080 s % 259.07/36.85 % (1950144)Peak memory usage: 13 MB % 259.07/36.85 % (1950144)Instructions burned: 263 (million) % 259.07/36.85 % (1950146)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=2851297725:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2753 on theBenchmark for (2753ds/1368Mi) % 259.07/36.85 % (1950146)Instruction limit reached! % 259.07/36.85 % (1950146)------------------------------ % 259.07/36.85 % (1950146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.07/36.85 % (1950146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.07/36.85 % (1950146)CaDiCaL version: 2.1.3 % 259.07/36.85 % (1950146)Termination reason: Instruction limit % 259.07/36.85 % (1950146)Termination phase: Saturation % 259.07/36.85 % (1950146)Time elapsed: 0.387 s % 259.07/36.85 % (1950146)Peak memory usage: 17 MB % 259.07/36.85 % (1950146)Instructions burned: 1371 (million) % 259.07/36.85 % (1950148)ott-21_1_sil=16000:si=on:fs=off:random_seed=1257560377:i=360:av=off:fsr=off:rtra=on_2749 on theBenchmark for (2749ds/360Mi) % 259.07/36.85 % (1950148)Instruction limit reached! % 259.07/36.85 % (1950148)------------------------------ % 259.07/36.85 % (1950148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.07/36.85 % (1950148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.07/36.85 % (1950148)CaDiCaL version: 2.1.3 % 259.07/36.85 % (1950148)Termination reason: Instruction limit % 259.07/36.85 % (1950148)Termination phase: Saturation % 259.07/36.85 % (1950148)Time elapsed: 0.103 s % 259.07/36.85 % (1950148)Peak memory usage: 14 MB % 259.07/36.85 % (1950148)Instructions burned: 364 (million) % 259.07/36.85 % (1950150)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=407928434:i=954:bd=all:rtra=on_2748 on theBenchmark for (2748ds/954Mi) % 259.07/36.85 % (1950150)Instruction limit reached! % 259.07/36.85 % (1950150)------------------------------ % 259.07/36.85 % (1950150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.07/36.85 % (1950150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.07/36.85 % (1950150)CaDiCaL version: 2.1.3 % 259.07/36.85 % (1950150)Termination reason: Instruction limit % 259.07/36.85 % (1950150)Termination phase: Saturation % 259.07/36.85 % (1950150)Time elapsed: 0.312 s % 259.07/36.85 % (1950150)Peak memory usage: 15 MB % 259.07/36.85 % (1950150)Instructions burned: 954 (million) % 259.07/36.85 % (1950152)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4176763687:fmbsr=1.3:i=1730:ins=25:rtra=on_2745 on theBenchmark for (2745ds/1730Mi) % 259.07/36.85 % Exception at run slice level % 259.07/36.85 User error: Finite model building is currently nTerminated % 300.20/42.64 % Vampire exiting % 300.20/42.65 Terminated %------------------------------------------------------------------------------