%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM093_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 : n011.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 09:40:17 AM UTC 2026 % Result : Timeout 295.83s 41.91s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM093_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.08/0.19 % Computer : n011.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 21:54:01 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/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 % 7.03/1.36 % (3819312)Will run a generic schedule for satisfiability detection. % 7.03/1.36 % (3819332)dis+10_1_sil=32000:sp=arity:random_seed=12890049:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.03/1.36 % (3819330)% WARNING: option uhcvi not known. % 7.03/1.36 % (3819329)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4204256677_2999 on theBenchmark for (2999ds/0Mi) % 7.03/1.36 % (3819330)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=491133168:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.03/1.36 % (3819331)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=144521943:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.03/1.36 % (3819334)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3152081424:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.03/1.36 % (3819335)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2048785515:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.03/1.36 % (3819333)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3690408183:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.03/1.36 % Exception at run slice level % 7.03/1.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.03/1.36 % (3819332)Instruction limit reached! % 7.03/1.36 % (3819332)------------------------------ % 7.03/1.36 % (3819332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.03/1.36 % (3819332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/1.36 % (3819332)CaDiCaL version: 2.1.3 % 7.03/1.36 % (3819332)Termination reason: Instruction limit % 7.03/1.36 % (3819332)Termination phase: Saturation % 7.03/1.36 % (3819332)Time elapsed: 0.034 s % 7.03/1.36 % (3819332)Peak memory usage: 12 MB % 7.03/1.36 % (3819332)Instructions burned: 104 (million) % 7.03/1.36 % (3819353)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1661474701:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.03/1.36 % (3819357)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=225963522:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.03/1.36 % Exception at run slice level % 7.03/1.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.03/1.36 % (3819364)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=760477106:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.03/1.36 % (3819334)Instruction limit reached! % 7.03/1.36 % (3819334)------------------------------ % 7.03/1.36 % (3819334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.03/1.36 % (3819334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/1.36 % (3819334)CaDiCaL version: 2.1.3 % 7.03/1.36 % (3819334)Termination reason: Instruction limit % 7.03/1.36 % (3819334)Termination phase: Saturation % 7.03/1.36 % (3819334)Time elapsed: 0.069 s % 7.03/1.36 % (3819334)Peak memory usage: 12 MB % 7.03/1.36 % (3819334)Instructions burned: 132 (million) % 7.03/1.36 % (3819333)Instruction limit reached! % 7.03/1.36 % (3819333)------------------------------ % 7.03/1.36 % (3819333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.03/1.36 % (3819333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/1.36 % (3819333)CaDiCaL version: 2.1.3 % 7.03/1.36 % (3819333)Termination reason: Instruction limit % 7.03/1.36 % (3819333)Termination phase: Saturation % 7.03/1.36 % (3819333)Time elapsed: 0.075 s % 7.03/1.36 % (3819333)Peak memory usage: 13 MB % 7.03/1.36 % (3819333)Instructions burned: 116 (million) % 7.03/1.36 % (3819357)Instruction limit reached! % 7.03/1.36 % (3819357)------------------------------ % 7.03/1.36 % (3819357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.03/1.36 % (3819357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/1.36 % (3819357)CaDiCaL version: 2.1.3 % 7.03/1.36 % (3819357)Termination reason: Instruction limit % 7.03/1.36 % (3819357)Termination phase: Saturation % 7.03/1.36 % (3819357)Time elapsed: 0.044 s % 7.03/1.36 % (3819357)Peak memory usage: 13 MB % 7.03/1.36 % (3819357)Instructions burned: 133 (million) % 7.03/1.36 % (3819376)ott-21_1_sil=16000:fs=off:random_seed=3106289257:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.03/1.36 % (3819335)Instruction limit reached! % 19.75/3.10 % (3819335)------------------------------ % 19.75/3.10 % (3819335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.10 % (3819335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.10 % (3819335)CaDiCaL version: 2.1.3 % 19.75/3.10 % (3819335)Termination reason: Instruction limit % 19.75/3.10 % (3819335)Termination phase: Saturation % 19.75/3.10 % (3819335)Time elapsed: 0.089 s % 19.75/3.10 % (3819335)Peak memory usage: 13 MB % 19.75/3.10 % (3819335)Instructions burned: 160 (million) % 19.75/3.10 % (3819383)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4087179682:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.75/3.10 % (3819379)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3790900487:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.75/3.10 % Exception at run slice level % 19.75/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.10 % (3819391)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2809919102:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.75/3.10 % (3819385)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2990372111:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.75/3.10 % Exception at run slice level % 19.75/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.10 % (3819401)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=3437820920:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 19.75/3.10 % (3819376)Instruction limit reached! % 19.75/3.10 % (3819376)------------------------------ % 19.75/3.10 % (3819376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.10 % (3819376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.10 % (3819376)CaDiCaL version: 2.1.3 % 19.75/3.10 % (3819376)Termination reason: Instruction limit % 19.75/3.10 % (3819376)Termination phase: Saturation % 19.75/3.10 % (3819376)Time elapsed: 0.088 s % 19.75/3.10 % (3819376)Peak memory usage: 12 MB % 19.75/3.10 % (3819376)Instructions burned: 180 (million) % 19.75/3.10 % (3819435)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1886629803:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.75/3.10 % (3819401)Instruction limit reached! % 19.75/3.10 % (3819401)------------------------------ % 19.75/3.10 % (3819401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.10 % (3819401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.10 % (3819401)CaDiCaL version: 2.1.3 % 19.75/3.10 % (3819401)Termination reason: Instruction limit % 19.75/3.10 % (3819401)Termination phase: Saturation % 19.75/3.10 % (3819401)Time elapsed: 0.209 s % 19.75/3.10 % (3819401)Peak memory usage: 24 MB % 19.75/3.10 % (3819401)Instructions burned: 695 (million) % 19.75/3.10 % (3819438)fmb+10_1_sil=64000:random_seed=1914899510:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.75/3.10 % (3819379)Instruction limit reached! % 19.75/3.10 % (3819379)------------------------------ % 19.75/3.10 % (3819379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.75/3.10 % (3819379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.10 % (3819379)CaDiCaL version: 2.1.3 % 19.75/3.10 % (3819379)Termination reason: Instruction limit % 19.75/3.10 % (3819379)Termination phase: Saturation % 19.75/3.10 % (3819379)Time elapsed: 0.251 s % 19.75/3.10 % (3819379)Peak memory usage: 13 MB % 19.75/3.10 % (3819379)Instructions burned: 479 (million) % 19.75/3.10 % (3819438)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.75/3.10 % Exception at run slice level % 19.75/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.10 % (3819441)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1230801159:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 19.75/3.10 % Exception at run slice level % 19.75/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.75/3.10 % (3819440)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=460633368:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.75/3.10 % (3819443)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1495651412:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 72.04/10.46 % Exception at run slice level % 72.04/10.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.04/10.46 % (3819364)Instruction limit reached! % 72.04/10.46 % (3819364)------------------------------ % 72.04/10.46 % (3819364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.04/10.46 % (3819364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.04/10.46 % (3819364)CaDiCaL version: 2.1.3 % 72.04/10.46 % (3819364)Termination reason: Instruction limit % 72.04/10.46 % (3819364)Termination phase: Saturation % 72.04/10.46 % (3819364)Time elapsed: 0.325 s % 72.04/10.46 % (3819364)Peak memory usage: 14 MB % 72.04/10.46 % (3819364)Instructions burned: 684 (million) % 72.04/10.46 % (3819446)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=724788224:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 72.04/10.46 % (3819446)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 72.04/10.46 % (3819447)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3249934425:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 72.04/10.46 % Exception at run slice level % 72.04/10.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.04/10.46 % (3819450)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=523572136:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 72.04/10.46 % Exception at run slice level % 72.04/10.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.04/10.46 % (3819452)ott-2_1_sil=16000:newcnf=on:random_seed=470545977:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 72.04/10.46 % (3819435)Instruction limit reached! % 72.04/10.46 % (3819435)------------------------------ % 72.04/10.46 % (3819435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.04/10.46 % (3819435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.04/10.46 % (3819435)CaDiCaL version: 2.1.3 % 72.04/10.46 % (3819435)Termination reason: Instruction limit % 72.04/10.46 % (3819435)Termination phase: Saturation % 72.04/10.46 % (3819435)Time elapsed: 0.496 s % 72.04/10.46 % (3819435)Peak memory usage: 19 MB % 72.04/10.46 % (3819435)Instructions burned: 881 (million) % 72.04/10.46 % (3819385)Instruction limit reached! % 72.04/10.46 % (3819385)------------------------------ % 72.04/10.46 % (3819385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.04/10.46 % (3819385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.04/10.46 % (3819385)CaDiCaL version: 2.1.3 % 72.04/10.46 % (3819385)Termination reason: Instruction limit % 72.04/10.46 % (3819385)Termination phase: Saturation % 72.04/10.46 % (3819385)Time elapsed: 0.599 s % 72.04/10.46 % (3819385)Peak memory usage: 16 MB % 72.04/10.46 % (3819385)Instructions burned: 1180 (million) % 72.04/10.46 % (3819454)ott+10_1_sil=32000:tgt=ground:random_seed=1592928900:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 72.04/10.46 % (3819455)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1010466164:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 72.04/10.46 % Exception at run slice level % 72.04/10.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.04/10.46 % (3819458)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2503171043:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 72.04/10.46 % (3819452)Instruction limit reached! % 72.04/10.46 % (3819452)------------------------------ % 72.04/10.46 % (3819452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.04/10.46 % (3819452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.04/10.46 % (3819452)CaDiCaL version: 2.1.3 % 72.04/10.46 % (3819452)Termination reason: Instruction limit % 72.04/10.46 % (3819452)Termination phase: Saturation % 72.04/10.46 % (3819452)Time elapsed: 0.394 s % 72.04/10.46 % (3819452)Peak memory usage: 13 MB % 72.04/10.46 % (3819452)Instructions burned: 870 (million) % 72.04/10.46 % (3819460)dis+21_1_sil=32000:sas=cadical:random_seed=4126340244:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 72.04/10.46 % (3819446)Instruction limit reached! % 72.04/10.46 % (3819446)------------------------------ % 72.04/10.46 % (3819446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819446)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819446)Termination reason: Instruction limit % 109.52/15.94 % (3819446)Termination phase: Saturation % 109.52/15.94 % (3819446)Time elapsed: 0.681 s % 109.52/15.94 % (3819446)Peak memory usage: 18 MB % 109.52/15.94 % (3819446)Instructions burned: 1473 (million) % 109.52/15.94 % (3819462)ott+11_1_sil=16000:gs=on:random_seed=4173785899:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 109.52/15.94 % (3819443)Instruction limit reached! % 109.52/15.94 % (3819443)------------------------------ % 109.52/15.94 % (3819443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819443)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819443)Termination reason: Instruction limit % 109.52/15.94 % (3819443)Termination phase: Saturation % 109.52/15.94 % (3819443)Time elapsed: 1.339 s % 109.52/15.94 % (3819443)Peak memory usage: 25 MB % 109.52/15.94 % (3819443)Instructions burned: 5146 (million) % 109.52/15.94 % (3819464)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2285806814:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 109.52/15.94 % Exception at run slice level % 109.52/15.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 109.52/15.94 % (3819466)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3119276229:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 109.52/15.94 % (3819462)Instruction limit reached! % 109.52/15.94 % (3819462)------------------------------ % 109.52/15.94 % (3819462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819462)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819462)Termination reason: Instruction limit % 109.52/15.94 % (3819462)Termination phase: Saturation % 109.52/15.94 % (3819462)Time elapsed: 1.174 s % 109.52/15.94 % (3819462)Peak memory usage: 21 MB % 109.52/15.94 % (3819462)Instructions burned: 2253 (million) % 109.52/15.94 % (3819468)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=415445742:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 109.52/15.94 % (3819458)Instruction limit reached! % 109.52/15.94 % (3819458)------------------------------ % 109.52/15.94 % (3819458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819458)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819458)Termination reason: Instruction limit % 109.52/15.94 % (3819458)Termination phase: Saturation % 109.52/15.94 % (3819458)Time elapsed: 1.787 s % 109.52/15.94 % (3819458)Peak memory usage: 26 MB % 109.52/15.94 % (3819458)Instructions burned: 3512 (million) % 109.52/15.94 % (3819470)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1564147804:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 109.52/15.94 % (3819466)Instruction limit reached! % 109.52/15.94 % (3819466)------------------------------ % 109.52/15.94 % (3819466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819466)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819466)Termination reason: Instruction limit % 109.52/15.94 % (3819466)Termination phase: Saturation % 109.52/15.94 % (3819466)Time elapsed: 1.052 s % 109.52/15.94 % (3819466)Peak memory usage: 34 MB % 109.52/15.94 % (3819466)Instructions burned: 4595 (million) % 109.52/15.94 % (3819460)Instruction limit reached! % 109.52/15.94 % (3819460)------------------------------ % 109.52/15.94 % (3819460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.52/15.94 % (3819460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.52/15.94 % (3819460)CaDiCaL version: 2.1.3 % 109.52/15.94 % (3819460)Termination reason: Instruction limit % 109.52/15.94 % (3819460)Termination phase: Saturation % 109.52/15.94 % (3819460)Time elapsed: 1.920 s % 109.52/15.94 % (3819460)Peak memory usage: 25 MB % 109.52/15.94 % (3819460)Instructions burned: 3775 (million) % 109.52/15.94 % (3819472)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2727702824:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 109.52/15.94 % Exception at run slice level % 109.52/15.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.07/25.99 % (3819473)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3651477991:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 182.07/25.99 % (3819475)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2032773160:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 182.07/25.99 % Exception at run slice level % 182.07/25.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.07/25.99 % Exception at run slice level % 182.07/25.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.07/25.99 % (3819479)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4087995888:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi) % 182.07/25.99 % (3819478)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4037636611:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 182.07/25.99 % (3819454)Instruction limit reached! % 182.07/25.99 % (3819454)------------------------------ % 182.07/25.99 % (3819454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.07/25.99 % (3819454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.07/25.99 % (3819454)CaDiCaL version: 2.1.3 % 182.07/25.99 % (3819454)Termination reason: Instruction limit % 182.07/25.99 % (3819454)Termination phase: Saturation % 182.07/25.99 % (3819454)Time elapsed: 2.597 s % 182.07/25.99 % (3819454)Peak memory usage: 23 MB % 182.07/25.99 % (3819454)Instructions burned: 5115 (million) % 182.07/25.99 % (3819482)dis+10_16:1_sil=16000:random_seed=3153964529:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 182.07/25.99 % (3819479)Instruction limit reached! % 182.07/25.99 % (3819479)------------------------------ % 182.07/25.99 % (3819479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.07/25.99 % (3819479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.07/25.99 % (3819479)CaDiCaL version: 2.1.3 % 182.07/25.99 % (3819479)Termination reason: Instruction limit % 182.07/25.99 % (3819479)Termination phase: Saturation % 182.07/25.99 % (3819479)Time elapsed: 2.298 s % 182.07/25.99 % (3819479)Peak memory usage: 34 MB % 182.07/25.99 % (3819479)Instructions burned: 8174 (million) % 182.07/25.99 % (3819484)ott-3_8_sil=64000:random_seed=3313741748:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 182.07/25.99 % (3819470)Instruction limit reached! % 182.07/25.99 % (3819470)------------------------------ % 182.07/25.99 % (3819470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.07/25.99 % (3819470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.07/25.99 % (3819470)CaDiCaL version: 2.1.3 % 182.07/25.99 % (3819470)Termination reason: Instruction limit % 182.07/25.99 % (3819470)Termination phase: Saturation % 182.07/25.99 % (3819470)Time elapsed: 2.729 s % 182.07/25.99 % (3819470)Peak memory usage: 39 MB % 182.07/25.99 % (3819470)Instructions burned: 5211 (million) % 182.07/25.99 % (3819486)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2839535773:fmbsr=2:i=32576_2946 on theBenchmark for (2946ds/32576Mi) % 182.07/25.99 % Exception at run slice level % 182.07/25.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.07/25.99 % (3819488)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=298099959:i=11404_2946 on theBenchmark for (2946ds/11404Mi) % 182.07/25.99 % (3819482)Instruction limit reached! % 182.07/25.99 % (3819482)------------------------------ % 182.07/25.99 % (3819482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.07/25.99 % (3819482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.07/25.99 % (3819482)CaDiCaL version: 2.1.3 % 182.07/25.99 % (3819482)Termination reason: Instruction limit % 182.07/25.99 % (3819482)Termination phase: Saturation % 182.07/25.99 % (3819482)Time elapsed: 4.929 s % 182.07/25.99 % (3819482)Peak memory usage: 50 MB % 182.07/25.99 % (3819482)Instructions burned: 9155 (million) % 182.07/25.99 % (3819490)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1170956032:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 182.07/25.99 % (3819484)Instruction limit reached! % 182.07/25.99 % (3819484)------------------------------ % 182.07/25.99 % (3819484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.07/25.99 % (3819484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.07/25.99 % (3819484)CaDiCaL version: 2.1.3 % 203.43/28.92 % (3819484)Termination reason: Instruction limit % 203.43/28.92 % (3819484)Termination phase: Saturation % 203.43/28.92 % (3819484)Time elapsed: 5.016 s % 203.43/28.92 % (3819484)Peak memory usage: 26 MB % 203.43/28.92 % (3819484)Instructions burned: 20143 (million) % 203.43/28.92 % (3819492)dis+33_16_sil=32000:sac=on:random_seed=2283410482:i=15851:nm=0_2897 on theBenchmark for (2897ds/15851Mi) % 203.43/28.92 % (3819488)Instruction limit reached! % 203.43/28.92 % (3819488)------------------------------ % 203.43/28.92 % (3819488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.43/28.92 % (3819488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.43/28.92 % (3819488)CaDiCaL version: 2.1.3 % 203.43/28.92 % (3819488)Termination reason: Instruction limit % 203.43/28.92 % (3819488)Termination phase: Saturation % 203.43/28.92 % (3819488)Time elapsed: 7.469 s % 203.43/28.92 % (3819488)Peak memory usage: 106 MB % 203.43/28.92 % (3819488)Instructions burned: 11405 (million) % 203.43/28.92 % (3819494)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3299351723:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 203.43/28.92 % (3819492)Instruction limit reached! % 203.43/28.93 % (3819492)------------------------------ % 203.43/28.93 % (3819492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.43/28.93 % (3819492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.43/28.93 % (3819492)CaDiCaL version: 2.1.3 % 203.43/28.93 % (3819492)Termination reason: Instruction limit % 203.43/28.93 % (3819492)Termination phase: Saturation % 203.43/28.93 % (3819492)Time elapsed: 4.567 s % 203.43/28.93 % (3819492)Peak memory usage: 345 MB % 203.43/28.93 % (3819492)Instructions burned: 15854 (million) % 203.43/28.93 % (3819661)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1558659726:s2a=on:i=53295_2851 on theBenchmark for (2851ds/53295Mi) % 203.43/28.93 % (3819478)Instruction limit reached! % 203.43/28.93 % (3819478)------------------------------ % 203.43/28.93 % (3819478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.43/28.93 % (3819478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.43/28.93 % (3819478)CaDiCaL version: 2.1.3 % 203.43/28.93 % (3819478)Termination reason: Instruction limit % 203.43/28.93 % (3819478)Termination phase: Saturation % 203.43/28.93 % (3819478)Time elapsed: 11.986 s % 203.43/28.93 % (3819478)Peak memory usage: 55 MB % 203.43/28.93 % (3819478)Instructions burned: 22565 (million) % 203.43/28.93 % (3819690)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2783402212:i=26857:ins=20_2851 on theBenchmark for (2851ds/26857Mi) % 203.43/28.93 % Exception at run slice level % 203.43/28.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.43/28.93 % (3819698)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=676656091:i=28120:bs=on:fsr=off_2850 on theBenchmark for (2850ds/28120Mi) % 203.43/28.93 % (3819490)Instruction limit reached! % 203.43/28.93 % (3819490)------------------------------ % 203.43/28.93 % (3819490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.43/28.93 % (3819490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.43/28.93 % (3819490)CaDiCaL version: 2.1.3 % 203.43/28.93 % (3819490)Termination reason: Instruction limit % 203.43/28.93 % (3819490)Termination phase: Saturation % 203.43/28.93 % (3819490)Time elapsed: 7.256 s % 203.43/28.93 % (3819490)Peak memory usage: 35 MB % 203.43/28.93 % (3819490)Instructions burned: 14134 (million) % 203.43/28.93 % (3819764)fmb+10_1_sil=256000:fmbss=7:random_seed=424859568:fmbsr=1.6:i=182295_2843 on theBenchmark for (2843ds/182295Mi) % 203.43/28.93 % Exception at run slice level % 203.43/28.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.43/28.93 % (3819766)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4195396445:i=44625:gsp=on_2843 on theBenchmark for (2843ds/44625Mi) % 203.43/28.93 % (3819766)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 203.43/28.93 % Exception at run slice level % 203.43/28.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.43/28.93 % (3819768)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3871515812:i=160505_2843 on theBenchmark for (2843ds/160505Mi) % 203.43/28.93 % Exception at run slice level % 203.43/28.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.43/28.93 % (3819770)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=323957083:fmbsr=1.3:i=225729_2843 on theBenchmark for (2843ds/225729Mi) % 237.15/33.77 % Exception at run slice level % 237.15/33.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 237.15/33.77 % (3819772)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1954909385:fmbsr=2:i=185024:ins=7_2842 on theBenchmark for (2842ds/185024Mi) % 237.15/33.77 % Exception at run slice level % 237.15/33.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 237.15/33.77 % (3819774)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3394218983:rtra=on_2842 on theBenchmark for (2842ds/0Mi) % 237.15/33.77 % Exception at run slice level % 237.15/33.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 237.15/33.77 % (3819776)% WARNING: option uhcvi not known. % 237.15/33.77 % (3819776)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3220366114:i=271062:add=off:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/271062Mi) % 237.15/33.77 % (3819468)Instruction limit reached! % 237.15/33.77 % (3819468)------------------------------ % 237.15/33.77 % (3819468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.15/33.77 % (3819468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.15/33.77 % (3819468)CaDiCaL version: 2.1.3 % 237.15/33.77 % (3819468)Termination reason: Instruction limit % 237.15/33.77 % (3819468)Termination phase: Saturation % 237.15/33.77 % (3819468)Time elapsed: 15.566 s % 237.15/33.77 % (3819468)Peak memory usage: 627 MB % 237.15/33.77 % (3819468)Instructions burned: 29340 (million) % 237.15/33.77 % (3819841)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=795333453:i=176048:add=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/176048Mi) % 237.15/33.77 % (3819494)Instruction limit reached! % 237.15/33.77 % (3819494)------------------------------ % 237.15/33.77 % (3819494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.15/33.77 % (3819494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.15/33.77 % (3819494)CaDiCaL version: 2.1.3 % 237.15/33.77 % (3819494)Termination reason: Instruction limit % 237.15/33.77 % (3819494)Termination phase: Saturation % 237.15/33.77 % (3819494)Time elapsed: 12.172 s % 237.15/33.77 % (3819494)Peak memory usage: 54 MB % 237.15/33.77 % (3819494)Instructions burned: 17627 (million) % 237.15/33.77 % (3819921)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1152891692:i=206:fgj=on:rtra=on_2749 on theBenchmark for (2749ds/206Mi) % 237.15/33.77 % (3819921)Instruction limit reached! % 237.15/33.77 % (3819921)------------------------------ % 237.15/33.77 % (3819921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.15/33.77 % (3819921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.15/33.77 % (3819921)CaDiCaL version: 2.1.3 % 237.15/33.77 % (3819921)Termination reason: Instruction limit % 237.15/33.77 % (3819921)Termination phase: Saturation % 237.15/33.77 % (3819921)Time elapsed: 0.195 s % 237.15/33.77 % (3819921)Peak memory usage: 13 MB % 237.15/33.77 % (3819921)Instructions burned: 207 (million) % 237.15/33.77 % (3819927)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2370047446:i=232:rtra=on_2746 on theBenchmark for (2746ds/232Mi) % 237.15/33.77 % (3819927)Instruction limit reached! % 237.15/33.77 % (3819927)------------------------------ % 237.15/33.77 % (3819927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.15/33.77 % (3819927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.15/33.77 % (3819927)CaDiCaL version: 2.1.3 % 237.15/33.77 % (3819927)Termination reason: Instruction limit % 237.15/33.77 % (3819927)Termination phase: Saturation % 237.15/33.77 % (3819927)Time elapsed: 0.212 s % 237.15/33.77 % (3819927)Peak memory usage: 14 MB % 237.15/33.77 % (3819927)Instructions burned: 232 (million) % 237.15/33.77 % (3819931)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2627285815:i=262:rtra=on_2744 on theBenchmark for (2744ds/262Mi) % 237.15/33.77 % (3819931)Instruction limit reached! % 237.15/33.77 % (3819931)------------------------------ % 237.15/33.77 % (3819931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.15/33.77 % (3819931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.15/33.77 % (3819931)CaDiCaL version: 2.1.3 % 237.15/33.77 % (3819931)Termination reason: Instruction limit % 237.15/33.77 % (3819931)Termination phase: Saturation % 295.83/41.91 % (3819931)Time elapsed: 0.156 s % 295.83/41.91 % (3819931)Peak memory usage: 13 MB % 295.83/41.91 % (3819931)Instructions burned: 262 (million) % 295.83/41.91 % (3819936)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2851579499:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2742 on theBenchmark for (2742ds/318Mi) % 295.83/41.91 % (3819936)Instruction limit reached! % 295.83/41.91 % (3819936)------------------------------ % 295.83/41.91 % (3819936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.83/41.91 % (3819936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.83/41.91 % (3819936)CaDiCaL version: 2.1.3 % 295.83/41.91 % (3819936)Termination reason: Instruction limit % 295.83/41.91 % (3819936)Termination phase: Saturation % 295.83/41.91 % (3819936)Time elapsed: 0.276 s % 295.83/41.91 % (3819936)Peak memory usage: 13 MB % 295.83/41.91 % (3819936)Instructions burned: 318 (million) % 295.83/41.91 % (3819942)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3246481743:i=1428:nm=2:rtra=on_2738 on theBenchmark for (2738ds/1428Mi) % 295.83/41.91 % Exception at run slice level % 295.83/41.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 295.83/41.91 % (3819944)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3698745206:i=262:bd=preordered:rtra=on:fsd=on_2738 on theBenchmark for (2738ds/262Mi) % 295.83/41.91 % (3819944)Instruction limit reached! % 295.83/41.91 % (3819944)------------------------------ % 295.83/41.91 % (3819944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.83/41.91 % (3819944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.83/41.91 % (3819944)CaDiCaL version: 2.1.3 % 295.83/41.91 % (3819944)Termination reason: Instruction limit % 295.83/41.91 % (3819944)Termination phase: Saturation % 295.83/41.91 % (3819944)Time elapsed: 0.279 s % 295.83/41.91 % (3819944)Peak memory usage: 15 MB % 295.83/41.91 % (3819944)Instructions burned: 263 (million) % 295.83/41.91 % (3819949)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=2255050325:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2735 on theBenchmark for (2735ds/1368Mi) % 295.83/41.91 % (3819949)Instruction limit reached! % 295.83/41.91 % (3819949)------------------------------ % 295.83/41.91 % (3819949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.83/41.91 % (3819949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.83/41.91 % (3819949)CaDiCaL version: 2.1.3 % 295.83/41.91 % (3819949)Termination reason: Instruction limit % 295.83/41.91 % (3819949)Termination phase: Saturation % 295.83/41.91 % (3819949)Time elapsed: 0.990 s % 295.83/41.91 % (3819949)Peak memory usage: 16 MB % 295.83/41.91 % (3819949)Instructions burned: 1369 (million) % 295.83/41.91 % (3819962)ott-21_1_sil=16000:si=on:fs=off:random_seed=3302902710:i=360:av=off:fsr=off:rtra=on_2725 on theBenchmark for (2725ds/360Mi) % 295.83/41.91 % (3819962)Instruction limit reached! % 295.83/41.91 % (3819962)------------------------------ % 295.83/41.91 % (3819962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.83/41.91 % (3819962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.83/41.91 % (3819962)CaDiCaL version: 2.1.3 % 295.83/41.91 % (3819962)Termination reason: Instruction limit % 295.83/41.91 % (3819962)Termination phase: Saturation % 295.83/41.91 % (3819962)Time elapsed: 0.266 s % 295.83/41.91 % (3819962)Peak memory usage: 13 MB % 295.83/41.91 % (3819962)Instructions burned: 360 (million) % 295.83/41.91 % (3819965)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1137114603:i=954:bd=all:rtra=on_2722 on theBenchmark for (2722ds/954Mi) % 295.83/41.91 % (3819965)Instruction limit reached! % 295.83/41.91 % (3819965)------------------------------ % 295.83/41.91 % (3819965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.83/41.91 % (3819965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.83/41.91 % (3819965)CaDiCaL version: 2.1.3 % 295.83/41.91 % (3819965)Termination reason: Instruction limit % 295.83/41.91 % (3819965)Termination phase: Saturation % 295.83/41.91 % (3819965)Time elapsed: 0.829 s % 295.83/41.91 % (3819965)Peak memory usage: 14 MB % 295.83/41.91 % (3819965)Instructions burned: 954 (million) % 295.83/41.91 % (3819973)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=303609016:fmbsr=1.3:i=1730:ins=25:rtra=on_2713 on theBenchmark for (2713ds/1730Mi) % 295.83/41.91 % Exception at run slice level % 295.83/41.91 User error: Finite model building is curreTerminated % 300.09/42.54 % Vampire exiting %------------------------------------------------------------------------------