%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV718_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 : n026.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:17 PM UTC 2026 % Result : Timeout 300.53s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV718_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.10/0.19 % Computer : n026.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 12:23:56 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 Running first-order model finding % 0.10/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 % 8.28/1.50 % (3820162)Will run a generic schedule for satisfiability detection. % 8.28/1.50 % (3820167)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1375293095_2999 on theBenchmark for (2999ds/0Mi) % 8.28/1.50 % Exception at run slice level % 8.28/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.28/1.50 % (3820168)% WARNING: option uhcvi not known. % 8.28/1.50 % (3820168)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1035347656:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.28/1.50 % (3820169)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3809154958:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.28/1.50 % (3820170)dis+10_1_sil=32000:sp=arity:random_seed=3039668671:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.28/1.50 % (3820171)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=162229788:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.28/1.50 % (3820172)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=771525390:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.28/1.50 % (3820173)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=955903097:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.28/1.50 % (3820175)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1621018130:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.28/1.50 % Exception at run slice level % 8.28/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.28/1.50 % (3820183)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4141644163:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.28/1.50 % (3820183)Instruction limit reached! % 8.28/1.50 % (3820183)------------------------------ % 8.28/1.50 % (3820183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.50 % (3820183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.50 % (3820183)CaDiCaL version: 2.1.3 % 8.28/1.50 % (3820183)Termination reason: Instruction limit % 8.28/1.50 % (3820183)Termination phase: Saturation % 8.28/1.50 % (3820183)Time elapsed: 0.043 s % 8.28/1.50 % (3820183)Peak memory usage: 13 MB % 8.28/1.50 % (3820183)Instructions burned: 131 (million) % 8.28/1.50 % (3820170)Instruction limit reached! % 8.28/1.50 % (3820170)------------------------------ % 8.28/1.50 % (3820170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.50 % (3820170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.50 % (3820170)CaDiCaL version: 2.1.3 % 8.28/1.50 % (3820170)Termination reason: Instruction limit % 8.28/1.50 % (3820170)Termination phase: Saturation % 8.28/1.50 % (3820170)Time elapsed: 0.061 s % 8.28/1.50 % (3820170)Peak memory usage: 12 MB % 8.28/1.50 % (3820170)Instructions burned: 104 (million) % 8.28/1.50 % (3820171)Instruction limit reached! % 8.28/1.50 % (3820171)------------------------------ % 8.28/1.50 % (3820171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.50 % (3820171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.50 % (3820171)CaDiCaL version: 2.1.3 % 8.28/1.50 % (3820171)Termination reason: Instruction limit % 8.28/1.50 % (3820171)Termination phase: Saturation % 8.28/1.50 % (3820171)Time elapsed: 0.069 s % 8.28/1.50 % (3820171)Peak memory usage: 12 MB % 8.28/1.50 % (3820171)Instructions burned: 117 (million) % 8.28/1.50 % (3820185)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=3866473386:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.28/1.50 % (3820172)Instruction limit reached! % 8.28/1.50 % (3820172)------------------------------ % 8.28/1.50 % (3820172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.50 % (3820172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.50 % (3820172)CaDiCaL version: 2.1.3 % 8.28/1.50 % (3820172)Termination reason: Instruction limit % 8.28/1.50 % (3820172)Termination phase: Saturation % 8.28/1.50 % (3820172)Time elapsed: 0.077 s % 8.28/1.50 % (3820172)Peak memory usage: 12 MB % 8.28/1.50 % (3820172)Instructions burned: 131 (million) % 8.28/1.50 % (3820186)ott-21_1_sil=16000:fs=off:random_seed=2488548946:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.28/1.50 % (3820187)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4071476920:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 20.55/3.19 % (3820173)Instruction limit reached! % 20.55/3.19 % (3820173)------------------------------ % 20.55/3.19 % (3820173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.19 % (3820173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.19 % (3820173)CaDiCaL version: 2.1.3 % 20.55/3.19 % (3820173)Termination reason: Instruction limit % 20.55/3.19 % (3820173)Termination phase: Saturation % 20.55/3.19 % (3820173)Time elapsed: 0.090 s % 20.55/3.19 % (3820173)Peak memory usage: 13 MB % 20.55/3.19 % (3820173)Instructions burned: 159 (million) % 20.55/3.19 % (3820189)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1788915239:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.55/3.19 % Exception at run slice level % 20.55/3.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.55/3.19 % (3820192)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1893718826:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.55/3.19 % (3820194)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1113818201:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.55/3.19 % Exception at run slice level % 20.55/3.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.55/3.19 % (3820197)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=2307656700:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 20.55/3.19 % (3820186)Instruction limit reached! % 20.55/3.19 % (3820186)------------------------------ % 20.55/3.19 % (3820186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.19 % (3820186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.19 % (3820186)CaDiCaL version: 2.1.3 % 20.55/3.19 % (3820186)Termination reason: Instruction limit % 20.55/3.19 % (3820186)Termination phase: Saturation % 20.55/3.19 % (3820186)Time elapsed: 0.095 s % 20.55/3.19 % (3820186)Peak memory usage: 12 MB % 20.55/3.19 % (3820186)Instructions burned: 181 (million) % 20.55/3.19 % (3820199)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1608715477:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.55/3.19 % (3820185)Instruction limit reached! % 20.55/3.19 % (3820185)------------------------------ % 20.55/3.19 % (3820185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.19 % (3820185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.55/3.19 % (3820185)CaDiCaL version: 2.1.3 % 20.55/3.19 % (3820185)Termination reason: Instruction limit % 20.55/3.19 % (3820185)Termination phase: Saturation % 20.55/3.19 % (3820185)Time elapsed: 0.192 s % 20.55/3.19 % (3820185)Peak memory usage: 15 MB % 20.55/3.19 % (3820185)Instructions burned: 687 (million) % 20.55/3.19 % (3820201)fmb+10_1_sil=64000:random_seed=3840694587:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.55/3.19 % (3820201)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.55/3.19 % Exception at run slice level % 20.55/3.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.55/3.19 % (3820203)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2421589959:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.55/3.19 % Exception at run slice level % 20.55/3.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.55/3.19 % (3820205)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=980852855:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.55/3.19 % Exception at run slice level % 20.55/3.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.55/3.19 % (3820207)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=246440427:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.55/3.19 % (3820187)Instruction limit reached! % 20.55/3.19 % (3820187)------------------------------ % 20.55/3.19 % (3820187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.55/3.19 % (3820187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.46/8.27 % (3820187)CaDiCaL version: 2.1.3 % 56.46/8.27 % (3820187)Termination reason: Instruction limit % 56.46/8.27 % (3820187)Termination phase: Saturation % 56.46/8.27 % (3820187)Time elapsed: 0.277 s % 56.46/8.27 % (3820187)Peak memory usage: 14 MB % 56.46/8.27 % (3820187)Instructions burned: 478 (million) % 56.46/8.27 % (3820209)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=747335207:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 56.46/8.27 % (3820209)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 56.46/8.27 % (3820197)Instruction limit reached! % 56.46/8.27 % (3820197)------------------------------ % 56.46/8.27 % (3820197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.46/8.27 % (3820197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.46/8.27 % (3820197)CaDiCaL version: 2.1.3 % 56.46/8.27 % (3820197)Termination reason: Instruction limit % 56.46/8.27 % (3820197)Termination phase: Saturation % 56.46/8.27 % (3820197)Time elapsed: 0.356 s % 56.46/8.27 % (3820197)Peak memory usage: 17 MB % 56.46/8.27 % (3820197)Instructions burned: 693 (million) % 56.46/8.27 % (3820211)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3592825850:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 56.46/8.27 % Exception at run slice level % 56.46/8.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 56.46/8.27 % (3820213)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1997044098:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 56.46/8.27 % Exception at run slice level % 56.46/8.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 56.46/8.27 % (3820215)ott-2_1_sil=16000:newcnf=on:random_seed=1683044223:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 56.46/8.27 % (3820199)Instruction limit reached! % 56.46/8.27 % (3820199)------------------------------ % 56.46/8.27 % (3820199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.46/8.27 % (3820199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.46/8.27 % (3820199)CaDiCaL version: 2.1.3 % 56.46/8.27 % (3820199)Termination reason: Instruction limit % 56.46/8.27 % (3820199)Termination phase: Saturation % 56.46/8.27 % (3820199)Time elapsed: 0.484 s % 56.46/8.27 % (3820199)Peak memory usage: 18 MB % 56.46/8.27 % (3820199)Instructions burned: 880 (million) % 56.46/8.27 % (3820217)ott+10_1_sil=32000:tgt=ground:random_seed=915520947:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 56.46/8.27 % (3820192)Instruction limit reached! % 56.46/8.27 % (3820192)------------------------------ % 56.46/8.27 % (3820192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.46/8.27 % (3820192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.46/8.27 % (3820192)CaDiCaL version: 2.1.3 % 56.46/8.27 % (3820192)Termination reason: Instruction limit % 56.46/8.27 % (3820192)Termination phase: Saturation % 56.46/8.27 % (3820192)Time elapsed: 0.632 s % 56.46/8.27 % (3820192)Peak memory usage: 17 MB % 56.46/8.27 % (3820192)Instructions burned: 1180 (million) % 56.46/8.27 % (3820219)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=106547209:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 56.46/8.27 % Exception at run slice level % 56.46/8.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 56.46/8.27 % (3820221)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1589854826:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 56.46/8.27 % (3820215)Instruction limit reached! % 56.46/8.27 % (3820215)------------------------------ % 56.46/8.27 % (3820215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.46/8.27 % (3820215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.46/8.27 % (3820215)CaDiCaL version: 2.1.3 % 56.46/8.27 % (3820215)Termination reason: Instruction limit % 56.46/8.27 % (3820215)Termination phase: Saturation % 56.46/8.27 % (3820215)Time elapsed: 0.447 s % 56.46/8.27 % (3820215)Peak memory usage: 16 MB % 56.46/8.27 % (3820215)Instructions burned: 871 (million) % 56.46/8.27 % (3820223)dis+21_1_sil=32000:sas=cadical:random_seed=4268868021:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 56.46/8.27 % (3820209)Instruction limit reached! % 56.46/8.27 % (3820209)------------------------------ % 56.46/8.27 % (3820209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820209)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820209)Termination reason: Instruction limit % 115.32/16.55 % (3820209)Termination phase: Saturation % 115.32/16.55 % (3820209)Time elapsed: 0.839 s % 115.32/16.55 % (3820209)Peak memory usage: 31 MB % 115.32/16.55 % (3820209)Instructions burned: 1474 (million) % 115.32/16.55 % (3820225)ott+11_1_sil=16000:gs=on:random_seed=3055545523:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 115.32/16.55 % (3820207)Instruction limit reached! % 115.32/16.55 % (3820207)------------------------------ % 115.32/16.55 % (3820207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820207)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820207)Termination reason: Instruction limit % 115.32/16.55 % (3820207)Termination phase: Saturation % 115.32/16.55 % (3820207)Time elapsed: 1.326 s % 115.32/16.55 % (3820207)Peak memory usage: 30 MB % 115.32/16.55 % (3820207)Instructions burned: 5134 (million) % 115.32/16.55 % (3820227)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3555107299:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 115.32/16.55 % Exception at run slice level % 115.32/16.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.32/16.55 % (3820229)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1416370362:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 115.32/16.55 % (3820225)Instruction limit reached! % 115.32/16.55 % (3820225)------------------------------ % 115.32/16.55 % (3820225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820225)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820225)Termination reason: Instruction limit % 115.32/16.55 % (3820225)Termination phase: Saturation % 115.32/16.55 % (3820225)Time elapsed: 1.170 s % 115.32/16.55 % (3820225)Peak memory usage: 21 MB % 115.32/16.55 % (3820225)Instructions burned: 2251 (million) % 115.32/16.55 % (3820231)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1263537734:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 115.32/16.55 % (3820221)Instruction limit reached! % 115.32/16.55 % (3820221)------------------------------ % 115.32/16.55 % (3820221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820221)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820221)Termination reason: Instruction limit % 115.32/16.55 % (3820221)Termination phase: Saturation % 115.32/16.55 % (3820221)Time elapsed: 1.827 s % 115.32/16.55 % (3820221)Peak memory usage: 29 MB % 115.32/16.55 % (3820221)Instructions burned: 3512 (million) % 115.32/16.55 % (3820233)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2680977944:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 115.32/16.55 % (3820229)Instruction limit reached! % 115.32/16.55 % (3820229)------------------------------ % 115.32/16.55 % (3820229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820229)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820229)Termination reason: Instruction limit % 115.32/16.55 % (3820229)Termination phase: Saturation % 115.32/16.55 % (3820229)Time elapsed: 1.233 s % 115.32/16.55 % (3820229)Peak memory usage: 45 MB % 115.32/16.55 % (3820229)Instructions burned: 4595 (million) % 115.32/16.55 % (3820235)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3532362472:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 115.32/16.55 % (3820223)Instruction limit reached! % 115.32/16.55 % (3820223)------------------------------ % 115.32/16.55 % (3820223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.32/16.55 % (3820223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.32/16.55 % (3820223)CaDiCaL version: 2.1.3 % 115.32/16.55 % (3820223)Termination reason: Instruction limit % 115.32/16.55 % (3820223)Termination phase: Saturation % 115.32/16.55 % (3820223)Time elapsed: 1.882 s % 115.32/16.55 % (3820223)Peak memory usage: 25 MB % 115.32/16.55 % (3820223)Instructions burned: 3774 (million) % 115.32/16.55 % Exception at run slice level % 115.32/16.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.52/21.09 % (3820238)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3512241727:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 147.52/21.09 % Exception at run slice level % 147.52/21.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.52/21.09 % (3820237)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3548894519:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 147.52/21.09 % Exception at run slice level % 147.52/21.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.52/21.09 % (3820240)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=88413504:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 147.52/21.09 % (3820243)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=773958667:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi) % 147.52/21.09 % (3820217)Instruction limit reached! % 147.52/21.09 % (3820217)------------------------------ % 147.52/21.09 % (3820217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.52/21.09 % (3820217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.52/21.09 % (3820217)CaDiCaL version: 2.1.3 % 147.52/21.09 % (3820217)Termination reason: Instruction limit % 147.52/21.09 % (3820217)Termination phase: Saturation % 147.52/21.09 % (3820217)Time elapsed: 2.671 s % 147.52/21.09 % (3820217)Peak memory usage: 42 MB % 147.52/21.09 % (3820217)Instructions burned: 5114 (million) % 147.52/21.09 % (3820245)dis+10_16:1_sil=16000:random_seed=248033900:i=9155:fsr=off_2965 on theBenchmark for (2965ds/9155Mi) % 147.52/21.09 % (3820233)Instruction limit reached! % 147.52/21.09 % (3820233)------------------------------ % 147.52/21.09 % (3820233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.52/21.09 % (3820233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.52/21.09 % (3820233)CaDiCaL version: 2.1.3 % 147.52/21.09 % (3820233)Termination reason: Instruction limit % 147.52/21.09 % (3820233)Termination phase: Saturation % 147.52/21.09 % (3820233)Time elapsed: 2.737 s % 147.52/21.09 % (3820233)Peak memory usage: 43 MB % 147.52/21.09 % (3820233)Instructions burned: 5211 (million) % 147.52/21.09 % (3820247)ott-3_8_sil=64000:random_seed=12572883:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 147.52/21.09 % (3820243)Instruction limit reached! % 147.52/21.09 % (3820243)------------------------------ % 147.52/21.09 % (3820243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.52/21.09 % (3820243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.52/21.09 % (3820243)CaDiCaL version: 2.1.3 % 147.52/21.09 % (3820243)Termination reason: Instruction limit % 147.52/21.09 % (3820243)Termination phase: Saturation % 147.52/21.09 % (3820243)Time elapsed: 4.235 s % 147.52/21.09 % (3820243)Peak memory usage: 51 MB % 147.52/21.09 % (3820243)Instructions burned: 8175 (million) % 147.52/21.09 % (3820249)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1362024931:fmbsr=2:i=32576_2927 on theBenchmark for (2927ds/32576Mi) % 147.52/21.09 % Exception at run slice level % 147.52/21.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.52/21.09 % (3820251)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=816930452:i=11404_2927 on theBenchmark for (2927ds/11404Mi) % 147.52/21.09 % (3820245)Instruction limit reached! % 147.52/21.09 % (3820245)------------------------------ % 147.52/21.09 % (3820245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.52/21.09 % (3820245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.52/21.09 % (3820245)CaDiCaL version: 2.1.3 % 147.52/21.09 % (3820245)Termination reason: Instruction limit % 147.52/21.09 % (3820245)Termination phase: Saturation % 147.52/21.09 % (3820245)Time elapsed: 4.560 s % 147.52/21.09 % (3820245)Peak memory usage: 45 MB % 147.52/21.09 % (3820245)Instructions burned: 9155 (million) % 147.52/21.09 % (3820253)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3748914406:i=14134_2919 on theBenchmark for (2919ds/14134Mi) % 147.52/21.09 % (3820240)Instruction limit reached! % 147.52/21.09 % (3820240)------------------------------ % 147.52/21.09 % (3820240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.52/21.09 % (3820240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.52/21.09 % (3820240)CaDiCaL version: 2.1.3 % 161.69/23.07 % (3820240)Termination reason: Instruction limit % 161.69/23.07 % (3820240)Termination phase: Saturation % 161.69/23.07 % (3820240)Time elapsed: 5.062 s % 161.69/23.07 % (3820240)Peak memory usage: 71 MB % 161.69/23.07 % (3820240)Instructions burned: 22567 (million) % 161.69/23.07 % (3820255)dis+33_16_sil=32000:sac=on:random_seed=836325914:i=15851:nm=0_2919 on theBenchmark for (2919ds/15851Mi) % 161.69/23.07 % (3820255)Instruction limit reached! % 161.69/23.07 % (3820255)------------------------------ % 161.69/23.07 % (3820255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.69/23.07 % (3820255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.69/23.07 % (3820255)CaDiCaL version: 2.1.3 % 161.69/23.07 % (3820255)Termination reason: Instruction limit % 161.69/23.07 % (3820255)Termination phase: Saturation % 161.69/23.07 % (3820255)Time elapsed: 4.527 s % 161.69/23.07 % (3820255)Peak memory usage: 123 MB % 161.69/23.07 % (3820255)Instructions burned: 15851 (million) % 161.69/23.07 % (3820257)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3395544978:avsq=on:i=17627:add=on:amm=off_2873 on theBenchmark for (2873ds/17627Mi) % 161.69/23.07 % (3820251)Instruction limit reached! % 161.69/23.07 % (3820251)------------------------------ % 161.69/23.07 % (3820251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.69/23.07 % (3820251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.69/23.07 % (3820251)CaDiCaL version: 2.1.3 % 161.69/23.07 % (3820251)Termination reason: Instruction limit % 161.69/23.07 % (3820251)Termination phase: Saturation % 161.69/23.07 % (3820251)Time elapsed: 6.054 s % 161.69/23.07 % (3820251)Peak memory usage: 84 MB % 161.69/23.07 % (3820251)Instructions burned: 11406 (million) % 161.69/23.07 % (3820259)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2231662377:s2a=on:i=53295_2866 on theBenchmark for (2866ds/53295Mi) % 161.69/23.07 % (3820253)Instruction limit reached! % 161.69/23.07 % (3820253)------------------------------ % 161.69/23.07 % (3820253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.69/23.07 % (3820253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.69/23.07 % (3820253)CaDiCaL version: 2.1.3 % 161.69/23.07 % (3820253)Termination reason: Instruction limit % 161.69/23.07 % (3820253)Termination phase: Saturation % 161.69/23.07 % (3820253)Time elapsed: 7.392 s % 161.69/23.07 % (3820253)Peak memory usage: 88 MB % 161.69/23.07 % (3820253)Instructions burned: 14134 (million) % 161.69/23.07 % (3820261)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1023445239:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 161.69/23.07 % Exception at run slice level % 161.69/23.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.69/23.07 % (3820263)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=900216900:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 161.69/23.07 % (3820247)Instruction limit reached! % 161.69/23.07 % (3820247)------------------------------ % 161.69/23.07 % (3820247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.69/23.07 % (3820247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.69/23.07 % (3820247)CaDiCaL version: 2.1.3 % 161.69/23.07 % (3820247)Termination reason: Instruction limit % 161.69/23.07 % (3820247)Termination phase: Saturation % 161.69/23.07 % (3820247)Time elapsed: 10.781 s % 161.69/23.07 % (3820247)Peak memory usage: 65 MB % 161.69/23.07 % (3820247)Instructions burned: 20139 (million) % 161.69/23.07 % (3820265)fmb+10_1_sil=256000:fmbss=7:random_seed=3328765379:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 161.69/23.07 % Exception at run slice level % 161.69/23.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.69/23.07 % (3820267)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=543366503:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 161.69/23.07 % (3820267)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 161.69/23.07 % Exception at run slice level % 161.69/23.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.69/23.07 % (3820269)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=5882394:i=160505_2837 on theBenchmark for (2837ds/160505Mi) % 161.69/23.07 % Exception at run slice level % 161.69/23.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.69/23.07 % (3820271)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3699519919:fmbsr=1.3:i=225729_2837 on theBenchmark for (2837ds/225729Mi) % 213.27/30.38 % Exception at run slice level % 213.27/30.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 213.27/30.38 % (3820273)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2306244452:fmbsr=2:i=185024:ins=7_2836 on theBenchmark for (2836ds/185024Mi) % 213.27/30.38 % Exception at run slice level % 213.27/30.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 213.27/30.38 % (3820275)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4019807171:rtra=on_2836 on theBenchmark for (2836ds/0Mi) % 213.27/30.38 % Exception at run slice level % 213.27/30.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 213.27/30.38 % (3820277)% WARNING: option uhcvi not known. % 213.27/30.38 % (3820277)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2378909441:i=271062:add=off:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/271062Mi) % 213.27/30.38 % (3820231)Instruction limit reached! % 213.27/30.38 % (3820231)------------------------------ % 213.27/30.38 % (3820231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.27/30.38 % (3820231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.38 % (3820231)CaDiCaL version: 2.1.3 % 213.27/30.38 % (3820231)Termination reason: Instruction limit % 213.27/30.38 % (3820231)Termination phase: Saturation % 213.27/30.38 % (3820231)Time elapsed: 15.063 s % 213.27/30.38 % (3820231)Peak memory usage: 128 MB % 213.27/30.38 % (3820231)Instructions burned: 29340 (million) % 213.27/30.38 % (3820279)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1695502324:i=176048:add=on:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/176048Mi) % 213.27/30.38 % (3820257)Instruction limit reached! % 213.27/30.38 % (3820257)------------------------------ % 213.27/30.38 % (3820257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.27/30.38 % (3820257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.38 % (3820257)CaDiCaL version: 2.1.3 % 213.27/30.38 % (3820257)Termination reason: Instruction limit % 213.27/30.38 % (3820257)Termination phase: Saturation % 213.27/30.38 % (3820257)Time elapsed: 7.741 s % 213.27/30.38 % (3820257)Peak memory usage: 64 MB % 213.27/30.38 % (3820257)Instructions burned: 17628 (million) % 213.27/30.38 % (3820281)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3071914532:i=206:fgj=on:rtra=on_2796 on theBenchmark for (2796ds/206Mi) % 213.27/30.38 % (3820281)Instruction limit reached! % 213.27/30.38 % (3820281)------------------------------ % 213.27/30.38 % (3820281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.27/30.38 % (3820281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.38 % (3820281)CaDiCaL version: 2.1.3 % 213.27/30.38 % (3820281)Termination reason: Instruction limit % 213.27/30.38 % (3820281)Termination phase: Saturation % 213.27/30.38 % (3820281)Time elapsed: 0.121 s % 213.27/30.38 % (3820281)Peak memory usage: 13 MB % 213.27/30.38 % (3820281)Instructions burned: 206 (million) % 213.27/30.38 % (3820283)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4024271878:i=232:rtra=on_2794 on theBenchmark for (2794ds/232Mi) % 213.27/30.38 % (3820283)Instruction limit reached! % 213.27/30.38 % (3820283)------------------------------ % 213.27/30.38 % (3820283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.27/30.38 % (3820283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.38 % (3820283)CaDiCaL version: 2.1.3 % 213.27/30.38 % (3820283)Termination reason: Instruction limit % 213.27/30.38 % (3820283)Termination phase: Saturation % 213.27/30.38 % (3820283)Time elapsed: 0.142 s % 213.27/30.38 % (3820283)Peak memory usage: 14 MB % 213.27/30.38 % (3820283)Instructions burned: 232 (million) % 213.27/30.38 % (3820285)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=617326026:i=262:rtra=on_2793 on theBenchmark for (2793ds/262Mi) % 213.27/30.38 % (3820285)Instruction limit reached! % 213.27/30.38 % (3820285)------------------------------ % 213.27/30.38 % (3820285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.27/30.38 % (3820285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.38 % (3820285)CaDiCaL version: 2.1.3 % 213.27/30.38 % (3820285)Termination reason: Instruction limit % 213.27/30.38 % (3820285)Termination phase: Saturation % 252.97/35.97 % (3820285)Time elapsed: 0.152 s % 252.97/35.97 % (3820285)Peak memory usage: 13 MB % 252.97/35.97 % (3820285)Instructions burned: 262 (million) % 252.97/35.97 % (3820287)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2805257696:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2791 on theBenchmark for (2791ds/318Mi) % 252.97/35.97 % (3820287)Instruction limit reached! % 252.97/35.97 % (3820287)------------------------------ % 252.97/35.97 % (3820287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.97/35.97 % (3820287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.97/35.97 % (3820287)CaDiCaL version: 2.1.3 % 252.97/35.97 % (3820287)Termination reason: Instruction limit % 252.97/35.97 % (3820287)Termination phase: Saturation % 252.97/35.97 % (3820287)Time elapsed: 0.159 s % 252.97/35.97 % (3820287)Peak memory usage: 13 MB % 252.97/35.97 % (3820287)Instructions burned: 319 (million) % 252.97/35.97 % (3820289)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3035488826:i=1428:nm=2:rtra=on_2789 on theBenchmark for (2789ds/1428Mi) % 252.97/35.97 % Exception at run slice level % 252.97/35.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.97/35.97 % (3820291)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3837175046:i=262:bd=preordered:rtra=on:fsd=on_2789 on theBenchmark for (2789ds/262Mi) % 252.97/35.97 % (3820291)Instruction limit reached! % 252.97/35.97 % (3820291)------------------------------ % 252.97/35.97 % (3820291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.97/35.97 % (3820291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.97/35.97 % (3820291)CaDiCaL version: 2.1.3 % 252.97/35.97 % (3820291)Termination reason: Instruction limit % 252.97/35.97 % (3820291)Termination phase: Saturation % 252.97/35.97 % (3820291)Time elapsed: 0.164 s % 252.97/35.97 % (3820291)Peak memory usage: 14 MB % 252.97/35.97 % (3820291)Instructions burned: 263 (million) % 252.97/35.97 % (3820293)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=2864144784:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/1368Mi) % 252.97/35.97 % (3820293)Instruction limit reached! % 252.97/35.97 % (3820293)------------------------------ % 252.97/35.97 % (3820293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.97/35.97 % (3820293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.97/35.97 % (3820293)CaDiCaL version: 2.1.3 % 252.97/35.97 % (3820293)Termination reason: Instruction limit % 252.97/35.97 % (3820293)Termination phase: Saturation % 252.97/35.97 % (3820293)Time elapsed: 0.763 s % 252.97/35.97 % (3820293)Peak memory usage: 17 MB % 252.97/35.97 % (3820293)Instructions burned: 1369 (million) % 252.97/35.97 % (3820295)ott-21_1_sil=16000:si=on:fs=off:random_seed=3778166791:i=360:av=off:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/360Mi) % 252.97/35.97 % (3820295)Instruction limit reached! % 252.97/35.97 % (3820295)------------------------------ % 252.97/35.97 % (3820295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.97/35.97 % (3820295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.97/35.97 % (3820295)CaDiCaL version: 2.1.3 % 252.97/35.97 % (3820295)Termination reason: Instruction limit % 252.97/35.97 % (3820295)Termination phase: Saturation % 252.97/35.97 % (3820295)Time elapsed: 0.174 s % 252.97/35.97 % (3820295)Peak memory usage: 13 MB % 252.97/35.97 % (3820295)Instructions burned: 361 (million) % 252.97/35.97 % (3820297)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1717078571:i=954:bd=all:rtra=on_2777 on theBenchmark for (2777ds/954Mi) % 252.97/35.97 % (3820297)Instruction limit reached! % 252.97/35.97 % (3820297)------------------------------ % 252.97/35.97 % (3820297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.97/35.97 % (3820297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.97/35.97 % (3820297)CaDiCaL version: 2.1.3 % 252.97/35.97 % (3820297)Termination reason: Instruction limit % 252.97/35.97 % (3820297)Termination phase: Saturation % 252.97/35.97 % (3820297)Time elapsed: 0.571 s % 252.97/35.97 % (3820297)Peak memory usage: 16 MB % 252.97/35.97 % (3820297)Instructions burned: 954 (million) % 252.97/35.97 % (3820299)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2337312014:fmbsr=1.3:i=1730:ins=25:rtra=on_2771 on theBenchmark for (2771ds/1730Mi) % 252.97/35.97 % Exception at run slice level % 252.97/35.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.96/37.84 % (3820301)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4031986155:i=2358:rtra=on_2771 on theBenchmark for (2771ds/2358Mi) % 265.96/37.84 % (3820301)Instruction limit reached! % 265.96/37.84 % (3820301)------------------------------ % 265.96/37.84 % (3820301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.96/37.84 % (3820301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.96/37.84 % (3820301)CaDiCaL version: 2.1.3 % 265.96/37.84 % (3820301)Termination reason: Instruction limit % 265.96/37.84 % (3820301)Termination phase: Saturation % 265.96/37.84 % (3820301)Time elapsed: 1.414 s % 265.96/37.84 % (3820301)Peak memory usage: 27 MB % 265.96/37.84 % (3820301)Instructions burned: 2358 (million) % 265.96/37.84 % (3820303)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=234540131:i=1778:ins=1:rtra=on_2757 on theBenchmark for (2757ds/1778Mi) % 265.96/37.84 % Exception at run slice level % 265.96/37.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.96/37.84 % (3820305)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=936560138:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2757 on theBenchmark for (2757ds/1384Mi) % 265.96/37.84 % (3820305)Instruction limit reached! % 265.96/37.84 % (3820305)------------------------------ % 265.96/37.84 % (3820305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.96/37.84 % (3820305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.96/37.84 % (3820305)CaDiCaL version: 2.1.3 % 265.96/37.84 % (3820305)Termination reason: Instruction limit % 265.96/37.84 % (3820305)Termination phase: Saturation % 265.96/37.84 % (3820305)Time elapsed: 0.765 s % 265.96/37.84 % (3820305)Peak memory usage: 21 MB % 265.96/37.84 % (3820305)Instructions burned: 1385 (million) % 265.96/37.84 % (3820307)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=249381315:i=1758:kws=inv_precedence:fsr=off:rtra=on_2749 on theBenchmark for (2749ds/1758Mi) % 265.96/37.84 % (3820307)Instruction limit reached! % 265.96/37.84 % (3820307)------------------------------ % 265.96/37.84 % (3820307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.96/37.84 % (3820307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.96/37.84 % (3820307)CaDiCaL version: 2.1.3 % 265.96/37.84 % (3820307)Termination reason: Instruction limit % 265.96/37.84 % (3820307)Termination phase: Saturation % 265.96/37.84 % (3820307)Time elapsed: 0.970 s % 265.96/37.84 % (3820307)Peak memory usage: 23 MB % 265.96/37.84 % (3820307)Instructions burned: 1759 (million) % 265.96/37.84 % (3820309)fmb+10_1_sil=64000:si=on:random_seed=775466102:i=44122:nm=2:rtra=on:gsp=on_2739 on theBenchmark for (2739ds/44122Mi) % 265.96/37.84 % (3820309)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 265.96/37.84 % Exception at run slice level % 265.96/37.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.96/37.84 % (3820311)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1886606295:i=19030:nm=5:rtra=on_2738 on theBenchmark for (2738ds/19030Mi) % 265.96/37.84 % Exception at run slice level % 265.96/37.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.96/37.84 % (3820313)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3086893971:fmbsr=1.7:i=1840:rtra=on_2738 on theBenchmark for (2738ds/1840Mi) % 265.96/37.84 % Exception at run slice level % 265.96/37.84 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.96/37.84 % (3820315)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1156185123:i=10262:rtra=on_2738 on theBenchmark for (2738ds/10262Mi) % 265.96/37.84 % (3820263)Instruction limit reached! % 265.96/37.84 % (3820263)------------------------------ % 265.96/37.84 % (3820263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.96/37.84 % (3820263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.96/37.84 % (3820263)CaDiCaL version: 2.1.3 % 265.96/37.84 % (3820263)Termination reason: Instruction limit % 265.96/37.84 % (3820263)Termination phase: Saturation % 265.96/37.84 % (3820263)Time elapsed: 14.676 s % 265.96/37.84 % (3820263)Peak memory usage: 88 MB % 265.96/37.84 % (3820263)Instructions burned: 28121 (million) % 300.53/42.63 % (3820317)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3835106056:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2698 on theBenchmark for (2698ds/2944Mi) % 300.53/42.63 % (3820317)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.53/42.63 % (3820259)Instruction limit reached! % 300.53/42.63 % (3820259)------------------------------ % 300.53/42.63 % (3820259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.63 % (3820259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.63 % (3820259)CaDiCaL version: 2.1.3 % 300.53/42.63 % (3820259)Termination reason: Instruction limit % 300.53/42.63 % (3820259)Termination phase: Saturation % 300.53/42.63 % (3820259)Time elapsed: 17.734 s % 300.53/42.63 % (3820259)Peak memory usage: 152 MB % 300.53/42.63 % (3820259)Instructions burned: 53296 (million) % 300.53/42.63 % (3820319)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1122873662:i=12648:rtra=on_2688 on theBenchmark for (2688ds/12648Mi) % 300.53/42.63 % Exception at run slice level % 300.53/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.53/42.63 % (3820321)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4084932560:fmbsr=2.30978:i=4348:rtra=on_2688 on theBenchmark for (2688ds/4348Mi) % 300.53/42.63 % Exception at run slice level % 300.53/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.53/42.63 % (3820323)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1572012551:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2688 on theBenchmark for (2688ds/1738Mi) % 300.53/42.63 % (3820315)Instruction limit reached! % 300.53/42.63 % (3820315)------------------------------ % 300.53/42.63 % (3820315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.63 % (3820315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.63 % (3820315)CaDiCaL version: 2.1.3 % 300.53/42.63 % (3820315)Termination reason: Instruction limit % 300.53/42.63 % (3820315)Termination phase: Saturation % 300.53/42.63 % (3820315)Time elapsed: 5.490 s % 300.53/42.63 % (3820315)Peak memory usage: 48 MB % 300.53/42.63 % (3820315)Instructions burned: 10263 (million) % 300.53/42.63 % (3820325)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=94720353:i=10228:av=off:rtra=on_2683 on theBenchmark for (2683ds/10228Mi) % 300.53/42.63 % (3820317)Instruction limit reached! % 300.53/42.63 % (3820317)------------------------------ % 300.53/42.63 % (3820317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.63 % (3820317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.63 % (3820317)CaDiCaL version: 2.1.3 % 300.53/42.63 % (3820317)Termination reason: Instruction limit % 300.53/42.63 % (3820317)Termination phase: Saturation % 300.53/42.63 % (3820317)Time elapsed: 1.809 s % 300.53/42.63 % (3820317)Peak memory usage: 47 MB % 300.53/42.63 % (3820317)Instructions burned: 2945 (million) % 300.53/42.63 % (3820327)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2881213656:i=108564:rtra=on_2680 on theBenchmark for (2680ds/108564Mi) % 300.53/42.63 % Exception at run slice level % 300.53/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.53/42.63 % (3820329)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3042723079:i=7024:aac=none:rtra=on_2679 on theBenchmark for (2679ds/7024Mi) % 300.53/42.63 % (3820323)Instruction limit reached! % 300.53/42.63 % (3820323)------------------------------ % 300.53/42.63 % (3820323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.63 % (3820323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.63 % (3820323)CaDiCaL version: 2.1.3 % 300.53/42.63 % (3820323)Termination reason: Instruction limit % 300.53/42.63 % (3820323)Termination phase: Saturation % 300.53/42.63 % (3820323)Time elapsed: 0.980 s % 300.53/42.63 % (3820323)Peak memory usage: 18 MB % 300.53/42.63 % (3820323)Instructions burned: 1739 (million) % 300.53/42.63 % (3820331)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3541614018:i=7546:rtra=on:amm=off_2678 on theBenchmark for (2678ds/7546Mi) % 300.53/42.63 % (3820169)Instruction limit reached! % 300.53/42.63 % (3820169)------------------------------ % 300.53/42.63 % (3820169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.63 % (3820169)Linked with Z3 4.14.0.0 3c % 300.53/42.64 Terminated % 300.53/42.64 % Vampire exiting % 300.53/42.64 Terminated %------------------------------------------------------------------------------