%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW491_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 : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:19 PM UTC 2026 % Result : Timeout 300.07s 42.55s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW491_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n020.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:15:35 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/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.25/1.35 % (187237)Will run a generic schedule for satisfiability detection. % 7.25/1.35 % (187246)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2918076313:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.25/1.35 % (187243)% WARNING: option uhcvi not known. % 7.25/1.35 % (187242)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2662878557_2999 on theBenchmark for (2999ds/0Mi) % 7.25/1.35 % (187247)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3890352829:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.25/1.35 % (187243)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2163116373:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.25/1.35 % (187244)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4225566839:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.25/1.35 % (187248)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=727454985:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.25/1.35 % (187245)dis+10_1_sil=32000:sp=arity:random_seed=2269305046:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.25/1.35 % Exception at run slice level % 7.25/1.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.25/1.35 % (187256)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3603910027:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.25/1.35 % Exception at run slice level % 7.25/1.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.25/1.35 % (187246)Instruction limit reached! % 7.25/1.35 % (187246)------------------------------ % 7.25/1.35 % (187246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.35 % (187246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.35 % (187246)CaDiCaL version: 2.1.3 % 7.25/1.35 % (187246)Termination reason: Instruction limit % 7.25/1.35 % (187246)Termination phase: Saturation % 7.25/1.35 % (187246)Time elapsed: 0.037 s % 7.25/1.35 % (187246)Peak memory usage: 12 MB % 7.25/1.35 % (187246)Instructions burned: 119 (million) % 7.25/1.35 % (187259)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=382804672:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.25/1.35 % (187258)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2424678215:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.25/1.35 % (187245)Instruction limit reached! % 7.25/1.35 % (187245)------------------------------ % 7.25/1.35 % (187245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.35 % (187245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.35 % (187245)CaDiCaL version: 2.1.3 % 7.25/1.35 % (187245)Termination reason: Instruction limit % 7.25/1.35 % (187245)Termination phase: Saturation % 7.25/1.35 % (187245)Time elapsed: 0.061 s % 7.25/1.35 % (187245)Peak memory usage: 12 MB % 7.25/1.35 % (187245)Instructions burned: 105 (million) % 7.25/1.35 % (187247)Instruction limit reached! % 7.25/1.35 % (187247)------------------------------ % 7.25/1.35 % (187247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.35 % (187247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.35 % (187247)CaDiCaL version: 2.1.3 % 7.25/1.35 % (187247)Termination reason: Instruction limit % 7.25/1.35 % (187247)Termination phase: Saturation % 7.25/1.35 % (187247)Time elapsed: 0.073 s % 7.25/1.35 % (187247)Peak memory usage: 13 MB % 7.25/1.35 % (187247)Instructions burned: 131 (million) % 7.25/1.35 % (187262)ott-21_1_sil=16000:fs=off:random_seed=1879818264:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.25/1.35 % (187263)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3063468567:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.25/1.35 % (187248)Instruction limit reached! % 7.25/1.35 % (187248)------------------------------ % 7.25/1.35 % (187248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.35 % (187248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.35 % (187248)CaDiCaL version: 2.1.3 % 7.25/1.35 % (187248)Termination reason: Instruction limit % 7.25/1.35 % (187248)Termination phase: Saturation % 7.25/1.35 % (187248)Time elapsed: 0.099 s % 7.25/1.35 % (187248)Peak memory usage: 13 MB % 20.97/3.25 % (187248)Instructions burned: 160 (million) % 20.97/3.25 % (187266)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3911521978:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.97/3.25 % Exception at run slice level % 20.97/3.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.97/3.25 % (187258)Instruction limit reached! % 20.97/3.25 % (187258)------------------------------ % 20.97/3.25 % (187258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.97/3.25 % (187258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.25 % (187258)CaDiCaL version: 2.1.3 % 20.97/3.25 % (187258)Termination reason: Instruction limit % 20.97/3.25 % (187258)Termination phase: Saturation % 20.97/3.25 % (187258)Time elapsed: 0.078 s % 20.97/3.25 % (187258)Peak memory usage: 13 MB % 20.97/3.25 % (187258)Instructions burned: 131 (million) % 20.97/3.25 % (187268)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1562002319:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.97/3.25 % (187269)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3139214381:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.97/3.25 % Exception at run slice level % 20.97/3.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.97/3.25 % (187272)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=2262625431: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.97/3.25 % (187262)Instruction limit reached! % 20.97/3.25 % (187262)------------------------------ % 20.97/3.25 % (187262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.97/3.25 % (187262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.25 % (187262)CaDiCaL version: 2.1.3 % 20.97/3.25 % (187262)Termination reason: Instruction limit % 20.97/3.25 % (187262)Termination phase: Saturation % 20.97/3.25 % (187262)Time elapsed: 0.085 s % 20.97/3.25 % (187262)Peak memory usage: 13 MB % 20.97/3.25 % (187262)Instructions burned: 181 (million) % 20.97/3.25 % (187274)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=370276626:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.97/3.25 % (187259)Instruction limit reached! % 20.97/3.25 % (187259)------------------------------ % 20.97/3.25 % (187259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.97/3.25 % (187259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.25 % (187259)CaDiCaL version: 2.1.3 % 20.97/3.25 % (187259)Termination reason: Instruction limit % 20.97/3.25 % (187259)Termination phase: Saturation % 20.97/3.25 % (187259)Time elapsed: 0.175 s % 20.97/3.25 % (187259)Peak memory usage: 14 MB % 20.97/3.25 % (187259)Instructions burned: 688 (million) % 20.97/3.25 % (187276)fmb+10_1_sil=64000:random_seed=3184942013:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.97/3.25 % (187276)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.97/3.25 % Exception at run slice level % 20.97/3.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.97/3.25 % (187278)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3291522477:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.97/3.25 % Exception at run slice level % 20.97/3.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.97/3.25 % (187280)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1527412544:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 20.97/3.25 % Exception at run slice level % 20.97/3.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.97/3.25 % (187282)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3298309351:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 20.97/3.25 % (187263)Instruction limit reached! % 20.97/3.25 % (187263)------------------------------ % 20.97/3.25 % (187263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.97/3.25 % (187263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.25 % (187263)CaDiCaL version: 2.1.3 % 20.97/3.25 % (187263)Termination reason: Instruction limit % 74.22/10.71 % (187263)Termination phase: Saturation % 74.22/10.71 % (187263)Time elapsed: 0.281 s % 74.22/10.71 % (187263)Peak memory usage: 14 MB % 74.22/10.71 % (187263)Instructions burned: 478 (million) % 74.22/10.71 % (187284)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1767106346:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 74.22/10.71 % (187284)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 74.22/10.71 % (187272)Instruction limit reached! % 74.22/10.71 % (187272)------------------------------ % 74.22/10.71 % (187272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.22/10.71 % (187272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.22/10.71 % (187272)CaDiCaL version: 2.1.3 % 74.22/10.71 % (187272)Termination reason: Instruction limit % 74.22/10.71 % (187272)Termination phase: Saturation % 74.22/10.71 % (187272)Time elapsed: 0.379 s % 74.22/10.71 % (187272)Peak memory usage: 15 MB % 74.22/10.71 % (187272)Instructions burned: 692 (million) % 74.22/10.71 % (187286)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2822586948:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 74.22/10.71 % Exception at run slice level % 74.22/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.22/10.71 % (187288)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2679541378:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 74.22/10.71 % Exception at run slice level % 74.22/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.22/10.71 % (187290)ott-2_1_sil=16000:newcnf=on:random_seed=1514615667:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 74.22/10.71 % (187274)Instruction limit reached! % 74.22/10.71 % (187274)------------------------------ % 74.22/10.71 % (187274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.22/10.71 % (187274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.22/10.71 % (187274)CaDiCaL version: 2.1.3 % 74.22/10.71 % (187274)Termination reason: Instruction limit % 74.22/10.71 % (187274)Termination phase: Saturation % 74.22/10.71 % (187274)Time elapsed: 0.488 s % 74.22/10.71 % (187274)Peak memory usage: 17 MB % 74.22/10.71 % (187274)Instructions burned: 880 (million) % 74.22/10.71 % (187292)ott+10_1_sil=32000:tgt=ground:random_seed=3238275525:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 74.22/10.71 % (187268)Instruction limit reached! % 74.22/10.71 % (187268)------------------------------ % 74.22/10.71 % (187268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.22/10.71 % (187268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.22/10.71 % (187268)CaDiCaL version: 2.1.3 % 74.22/10.71 % (187268)Termination reason: Instruction limit % 74.22/10.71 % (187268)Termination phase: Saturation % 74.22/10.71 % (187268)Time elapsed: 0.626 s % 74.22/10.71 % (187268)Peak memory usage: 17 MB % 74.22/10.71 % (187268)Instructions burned: 1180 (million) % 74.22/10.71 % (187294)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2073951708:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 74.22/10.71 % Exception at run slice level % 74.22/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.22/10.71 % (187296)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2636107105:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 74.22/10.71 % (187290)Instruction limit reached! % 74.22/10.71 % (187290)------------------------------ % 74.22/10.71 % (187290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.22/10.71 % (187290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.22/10.71 % (187290)CaDiCaL version: 2.1.3 % 74.22/10.71 % (187290)Termination reason: Instruction limit % 74.22/10.71 % (187290)Termination phase: Saturation % 74.22/10.71 % (187290)Time elapsed: 0.451 s % 74.22/10.71 % (187290)Peak memory usage: 16 MB % 74.22/10.71 % (187290)Instructions burned: 870 (million) % 74.22/10.71 % (187284)Instruction limit reached! % 74.22/10.71 % (187284)------------------------------ % 74.22/10.71 % (187284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.22/10.71 % (187284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.22/10.71 % (187284)CaDiCaL version: 2.1.3 % 74.22/10.71 % (187284)Termination reason: Instruction limit % 74.22/10.71 % (187284)Termination phase: Saturation % 106.15/15.29 % (187284)Time elapsed: 0.684 s % 106.15/15.29 % (187284)Peak memory usage: 25 MB % 106.15/15.29 % (187284)Instructions burned: 1473 (million) % 106.15/15.29 % (187298)dis+21_1_sil=32000:sas=cadical:random_seed=3109517672:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 106.15/15.29 % (187299)ott+11_1_sil=16000:gs=on:random_seed=2388592078:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 106.15/15.29 % (187282)Instruction limit reached! % 106.15/15.29 % (187282)------------------------------ % 106.15/15.29 % (187282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.15/15.29 % (187282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.15/15.29 % (187282)CaDiCaL version: 2.1.3 % 106.15/15.29 % (187282)Termination reason: Instruction limit % 106.15/15.29 % (187282)Termination phase: Saturation % 106.15/15.29 % (187282)Time elapsed: 1.355 s % 106.15/15.29 % (187282)Peak memory usage: 29 MB % 106.15/15.29 % (187282)Instructions burned: 5135 (million) % 106.15/15.29 % (187302)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2742317751:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 106.15/15.29 % Exception at run slice level % 106.15/15.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.15/15.29 % (187304)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3231282195:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 106.15/15.29 % (187299)Instruction limit reached! % 106.15/15.29 % (187299)------------------------------ % 106.15/15.29 % (187299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.15/15.29 % (187299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.15/15.29 % (187299)CaDiCaL version: 2.1.3 % 106.15/15.29 % (187299)Termination reason: Instruction limit % 106.15/15.29 % (187299)Termination phase: Saturation % 106.15/15.29 % (187299)Time elapsed: 1.138 s % 106.15/15.29 % (187299)Peak memory usage: 21 MB % 106.15/15.29 % (187299)Instructions burned: 2251 (million) % 106.15/15.29 % (187306)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=919005598:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 106.15/15.29 % (187296)Instruction limit reached! % 106.15/15.29 % (187296)------------------------------ % 106.15/15.29 % (187296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.15/15.29 % (187296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.15/15.29 % (187296)CaDiCaL version: 2.1.3 % 106.15/15.29 % (187296)Termination reason: Instruction limit % 106.15/15.29 % (187296)Termination phase: Saturation % 106.15/15.29 % (187296)Time elapsed: 1.744 s % 106.15/15.29 % (187296)Peak memory usage: 26 MB % 106.15/15.29 % (187296)Instructions burned: 3514 (million) % 106.15/15.29 % (187308)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4083218256:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 106.15/15.29 % (187298)Instruction limit reached! % 106.15/15.29 % (187298)------------------------------ % 106.15/15.29 % (187298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.15/15.29 % (187298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.15/15.29 % (187298)CaDiCaL version: 2.1.3 % 106.15/15.29 % (187298)Termination reason: Instruction limit % 106.15/15.29 % (187298)Termination phase: Saturation % 106.15/15.29 % (187298)Time elapsed: 1.846 s % 106.15/15.29 % (187298)Peak memory usage: 25 MB % 106.15/15.29 % (187298)Instructions burned: 3774 (million) % 106.15/15.29 % (187310)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2360131027:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 106.15/15.29 % Exception at run slice level % 106.15/15.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.15/15.29 % (187304)Instruction limit reached! % 106.15/15.29 % (187304)------------------------------ % 106.15/15.29 % (187304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.15/15.29 % (187304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.15/15.29 % (187304)CaDiCaL version: 2.1.3 % 106.15/15.29 % (187304)Termination reason: Instruction limit % 106.15/15.29 % (187304)Termination phase: Saturation % 106.15/15.29 % (187304)Time elapsed: 1.323 s % 106.15/15.29 % (187304)Peak memory usage: 61 MB % 106.15/15.29 % (187304)Instructions burned: 4593 (million) % 106.15/15.29 % (187312)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3709547621:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 137.94/19.76 % Exception at run slice level % 137.94/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 137.94/19.76 % (187313)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2637896860:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 137.94/19.76 % Exception at run slice level % 137.94/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 137.94/19.76 % (187317)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=971474705:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 137.94/19.76 % (187315)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=479764319:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 137.94/19.76 % (187292)Instruction limit reached! % 137.94/19.76 % (187292)------------------------------ % 137.94/19.76 % (187292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.94/19.76 % (187292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.94/19.76 % (187292)CaDiCaL version: 2.1.3 % 137.94/19.76 % (187292)Termination reason: Instruction limit % 137.94/19.76 % (187292)Termination phase: Saturation % 137.94/19.76 % (187292)Time elapsed: 2.692 s % 137.94/19.76 % (187292)Peak memory usage: 26 MB % 137.94/19.76 % (187292)Instructions burned: 5115 (million) % 137.94/19.76 % (187320)dis+10_16:1_sil=16000:random_seed=1843098832:i=9155:fsr=off_2965 on theBenchmark for (2965ds/9155Mi) % 137.94/19.76 % (187317)Instruction limit reached! % 137.94/19.76 % (187317)------------------------------ % 137.94/19.76 % (187317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.94/19.76 % (187317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.94/19.76 % (187317)CaDiCaL version: 2.1.3 % 137.94/19.76 % (187317)Termination reason: Instruction limit % 137.94/19.76 % (187317)Termination phase: Saturation % 137.94/19.76 % (187317)Time elapsed: 2.063 s % 137.94/19.76 % (187317)Peak memory usage: 33 MB % 137.94/19.76 % (187317)Instructions burned: 8177 (million) % 137.94/19.76 % (187322)ott-3_8_sil=64000:random_seed=2711805327:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 137.94/19.76 % (187308)Instruction limit reached! % 137.94/19.76 % (187308)------------------------------ % 137.94/19.76 % (187308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.94/19.76 % (187308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.94/19.76 % (187308)CaDiCaL version: 2.1.3 % 137.94/19.76 % (187308)Termination reason: Instruction limit % 137.94/19.76 % (187308)Termination phase: Saturation % 137.94/19.76 % (187308)Time elapsed: 2.758 s % 137.94/19.76 % (187308)Peak memory usage: 45 MB % 137.94/19.76 % (187308)Instructions burned: 5211 (million) % 137.94/19.76 % (187324)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1464427618:fmbsr=2:i=32576_2946 on theBenchmark for (2946ds/32576Mi) % 137.94/19.76 % Exception at run slice level % 137.94/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 137.94/19.76 % (187326)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2504590865:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 137.94/19.76 % (187320)Instruction limit reached! % 137.94/19.76 % (187320)------------------------------ % 137.94/19.76 % (187320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.94/19.76 % (187320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.94/19.76 % (187320)CaDiCaL version: 2.1.3 % 137.94/19.76 % (187320)Termination reason: Instruction limit % 137.94/19.76 % (187320)Termination phase: Saturation % 137.94/19.76 % (187320)Time elapsed: 4.103 s % 137.94/19.76 % (187320)Peak memory usage: 38 MB % 137.94/19.76 % (187320)Instructions burned: 9155 (million) % 137.94/19.76 % (187328)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=829806792:i=14134_2924 on theBenchmark for (2924ds/14134Mi) % 137.94/19.76 % (187322)Instruction limit reached! % 137.94/19.76 % (187322)------------------------------ % 137.94/19.76 % (187322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.94/19.76 % (187322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.94/19.76 % (187322)CaDiCaL version: 2.1.3 % 137.94/19.76 % (187322)Termination reason: Instruction limit % 137.94/19.76 % (187322)Termination phase: Saturation % 137.94/19.76 % (187322)Time elapsed: 5.341 s % 137.94/19.76 % (187322)Peak memory usage: 46 MB % 137.94/19.76 % (187322)Instructions burned: 20145 (million) % 137.94/19.76 % (187330)dis+33_16_sil=32000:sac=on:random_seed=1346097637:i=15851:nm=0_2895 on theBenchmark for (2895ds/15851Mi) % 142.97/20.48 % (187326)Instruction limit reached! % 142.97/20.48 % (187326)------------------------------ % 142.97/20.48 % (187326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.97/20.48 % (187326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.97/20.48 % (187326)CaDiCaL version: 2.1.3 % 142.97/20.48 % (187326)Termination reason: Instruction limit % 142.97/20.48 % (187326)Termination phase: Saturation % 142.97/20.48 % (187326)Time elapsed: 5.950 s % 142.97/20.48 % (187326)Peak memory usage: 41 MB % 142.97/20.48 % (187326)Instructions burned: 11404 (million) % 142.97/20.48 % (187332)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=53277294:avsq=on:i=17627:add=on:amm=off_2886 on theBenchmark for (2886ds/17627Mi) % 142.97/20.48 % (187306)Instruction limit reached! % 142.97/20.48 % (187306)------------------------------ % 142.97/20.48 % (187306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.97/20.48 % (187306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.97/20.48 % (187306)CaDiCaL version: 2.1.3 % 142.97/20.48 % (187306)Termination reason: Instruction limit % 142.97/20.48 % (187306)Termination phase: Saturation % 142.97/20.48 % (187306)Time elapsed: 11.556 s % 142.97/20.48 % (187306)Peak memory usage: 92 MB % 142.97/20.48 % (187306)Instructions burned: 29342 (million) % 142.97/20.48 % (187441)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=936583903:s2a=on:i=53295_2861 on theBenchmark for (2861ds/53295Mi) % 142.97/20.48 % (187330)Instruction limit reached! % 142.97/20.48 % (187330)------------------------------ % 142.97/20.48 % (187330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.97/20.48 % (187330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.97/20.48 % (187330)CaDiCaL version: 2.1.3 % 142.97/20.48 % (187330)Termination reason: Instruction limit % 142.97/20.48 % (187330)Termination phase: Saturation % 142.97/20.48 % (187330)Time elapsed: 3.856 s % 142.97/20.48 % (187330)Peak memory usage: 38 MB % 142.97/20.48 % (187330)Instructions burned: 15854 (million) % 142.97/20.48 % (187477)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2546472384:i=26857:ins=20_2856 on theBenchmark for (2856ds/26857Mi) % 142.97/20.48 % Exception at run slice level % 142.97/20.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.97/20.48 % (187484)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=357023964:i=28120:bs=on:fsr=off_2856 on theBenchmark for (2856ds/28120Mi) % 142.97/20.48 % (187315)Instruction limit reached! % 142.97/20.48 % (187315)------------------------------ % 142.97/20.48 % (187315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.97/20.48 % (187315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.97/20.48 % (187315)CaDiCaL version: 2.1.3 % 142.97/20.48 % (187315)Termination reason: Instruction limit % 142.97/20.48 % (187315)Termination phase: Saturation % 142.97/20.48 % (187315)Time elapsed: 11.838 s % 142.97/20.48 % (187315)Peak memory usage: 486 MB % 142.97/20.48 % (187315)Instructions burned: 22566 (million) % 142.97/20.48 % (187640)fmb+10_1_sil=256000:fmbss=7:random_seed=203819998:fmbsr=1.6:i=182295_2850 on theBenchmark for (2850ds/182295Mi) % 142.97/20.48 % Exception at run slice level % 142.97/20.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.97/20.48 % (187654)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2112975620:i=44625:gsp=on_2850 on theBenchmark for (2850ds/44625Mi) % 142.97/20.48 % (187654)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 142.97/20.48 % Exception at run slice level % 142.97/20.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.97/20.48 % (187662)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3011176003:i=160505_2850 on theBenchmark for (2850ds/160505Mi) % 142.97/20.48 % Exception at run slice level % 142.97/20.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.97/20.48 % (187673)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3113344193:fmbsr=1.3:i=225729_2849 on theBenchmark for (2849ds/225729Mi) % 142.97/20.48 % Exception at run slice level % 142.97/20.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.97/20.48 % (187685)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=825777253:fmbsr=2:i=185024:ins=7_2849 on theBenchmark for (2849ds/185024Mi) % 156.54/22.39 % Exception at run slice level % 156.54/22.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 156.54/22.39 % (187695)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1035827715:rtra=on_2849 on theBenchmark for (2849ds/0Mi) % 156.54/22.39 % Exception at run slice level % 156.54/22.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 156.54/22.39 % (187706)% WARNING: option uhcvi not known. % 156.54/22.39 % (187706)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4248516967:i=271062:add=off:rtra=on:rawr=on_2849 on theBenchmark for (2849ds/271062Mi) % 156.54/22.39 % (187328)Instruction limit reached! % 156.54/22.39 % (187328)------------------------------ % 156.54/22.39 % (187328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.54/22.39 % (187328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.54/22.39 % (187328)CaDiCaL version: 2.1.3 % 156.54/22.39 % (187328)Termination reason: Instruction limit % 156.54/22.39 % (187328)Termination phase: Saturation % 156.54/22.39 % (187328)Time elapsed: 7.713 s % 156.54/22.39 % (187328)Peak memory usage: 44 MB % 156.54/22.39 % (187328)Instructions burned: 14134 (million) % 156.54/22.39 % (187745)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=780486199:i=176048:add=on:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/176048Mi) % 156.54/22.39 % (187332)Instruction limit reached! % 156.54/22.39 % (187332)------------------------------ % 156.54/22.39 % (187332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.54/22.39 % (187332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.54/22.39 % (187332)CaDiCaL version: 2.1.3 % 156.54/22.39 % (187332)Termination reason: Instruction limit % 156.54/22.39 % (187332)Termination phase: Saturation % 156.54/22.39 % (187332)Time elapsed: 7.437 s % 156.54/22.39 % (187332)Peak memory usage: 81 MB % 156.54/22.39 % (187332)Instructions burned: 17629 (million) % 156.54/22.39 % (187787)dis+10_1_sil=32000:si=on:sp=arity:random_seed=310452946:i=206:fgj=on:rtra=on_2811 on theBenchmark for (2811ds/206Mi) % 156.54/22.39 % (187787)Instruction limit reached! % 156.54/22.39 % (187787)------------------------------ % 156.54/22.39 % (187787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.54/22.39 % (187787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.54/22.39 % (187787)CaDiCaL version: 2.1.3 % 156.54/22.39 % (187787)Termination reason: Instruction limit % 156.54/22.39 % (187787)Termination phase: Saturation % 156.54/22.39 % (187787)Time elapsed: 0.122 s % 156.54/22.39 % (187787)Peak memory usage: 13 MB % 156.54/22.39 % (187787)Instructions burned: 208 (million) % 156.54/22.39 % (187789)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2425037996:i=232:rtra=on_2810 on theBenchmark for (2810ds/232Mi) % 156.54/22.39 % (187789)Instruction limit reached! % 156.54/22.39 % (187789)------------------------------ % 156.54/22.39 % (187789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.54/22.39 % (187789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.54/22.39 % (187789)CaDiCaL version: 2.1.3 % 156.54/22.39 % (187789)Termination reason: Instruction limit % 156.54/22.39 % (187789)Termination phase: Saturation % 156.54/22.39 % (187789)Time elapsed: 0.137 s % 156.54/22.39 % (187789)Peak memory usage: 13 MB % 156.54/22.39 % (187789)Instructions burned: 233 (million) % 156.54/22.39 % (187791)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=201262377:i=262:rtra=on_2808 on theBenchmark for (2808ds/262Mi) % 156.54/22.39 % (187791)Instruction limit reached! % 156.54/22.39 % (187791)------------------------------ % 156.54/22.39 % (187791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.54/22.39 % (187791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.54/22.39 % (187791)CaDiCaL version: 2.1.3 % 156.54/22.39 % (187791)Termination reason: Instruction limit % 156.54/22.39 % (187791)Termination phase: Saturation % 156.54/22.39 % (187791)Time elapsed: 0.152 s % 156.54/22.39 % (187791)Peak memory usage: 14 MB % 156.54/22.39 % (187791)Instructions burned: 262 (million) % 156.54/22.39 % (187793)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3617682300:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2806 on theBenchmark for (2806ds/318Mi) % 156.54/22.39 % (187793)Instruction limit reached! % 156.54/22.39 % (187793)------------------------------ % 156.54/22.39 % (187793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/29.61 % (187793)CaDiCaL version: 2.1.3 % 208.37/29.61 % (187793)Termination reason: Instruction limit % 208.37/29.61 % (187793)Termination phase: Saturation % 208.37/29.61 % (187793)Time elapsed: 0.187 s % 208.37/29.61 % (187793)Peak memory usage: 14 MB % 208.37/29.61 % (187793)Instructions burned: 319 (million) % 208.37/29.61 % (187795)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2483352750:i=1428:nm=2:rtra=on_2804 on theBenchmark for (2804ds/1428Mi) % 208.37/29.61 % (187484)Instruction limit reached! % 208.37/29.61 % (187484)------------------------------ % 208.37/29.61 % (187484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/29.61 % (187484)CaDiCaL version: 2.1.3 % 208.37/29.61 % (187484)Termination reason: Instruction limit % 208.37/29.61 % (187484)Termination phase: Saturation % 208.37/29.61 % (187484)Time elapsed: 5.194 s % 208.37/29.61 % (187484)Peak memory usage: 19 MB % 208.37/29.61 % (187484)Instructions burned: 28126 (million) % 208.37/29.61 % Exception at run slice level % 208.37/29.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.37/29.61 % (187797)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=914945454:i=262:bd=preordered:rtra=on:fsd=on_2804 on theBenchmark for (2804ds/262Mi) % 208.37/29.61 % (187798)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=3236415062:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/1368Mi) % 208.37/29.61 % (187797)Instruction limit reached! % 208.37/29.61 % (187797)------------------------------ % 208.37/29.61 % (187797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/29.61 % (187797)CaDiCaL version: 2.1.3 % 208.37/29.61 % (187797)Termination reason: Instruction limit % 208.37/29.61 % (187797)Termination phase: Saturation % 208.37/29.61 % (187797)Time elapsed: 0.087 s % 208.37/29.61 % (187797)Peak memory usage: 15 MB % 208.37/29.61 % (187797)Instructions burned: 263 (million) % 208.37/29.61 % (187801)ott-21_1_sil=16000:si=on:fs=off:random_seed=1204549554:i=360:av=off:fsr=off:rtra=on_2803 on theBenchmark for (2803ds/360Mi) % 208.37/29.61 % (187801)Instruction limit reached! % 208.37/29.61 % (187801)------------------------------ % 208.37/29.61 % (187801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/29.61 % (187801)CaDiCaL version: 2.1.3 % 208.37/29.61 % (187801)Termination reason: Instruction limit % 208.37/29.61 % (187801)Termination phase: Saturation % 208.37/29.61 % (187801)Time elapsed: 0.089 s % 208.37/29.61 % (187801)Peak memory usage: 13 MB % 208.37/29.61 % (187801)Instructions burned: 363 (million) % 208.37/29.61 % (187803)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=894930166:i=954:bd=all:rtra=on_2802 on theBenchmark for (2802ds/954Mi) % 208.37/29.61 % (187803)Instruction limit reached! % 208.37/29.61 % (187803)------------------------------ % 208.37/29.61 % (187803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/29.61 % (187803)CaDiCaL version: 2.1.3 % 208.37/29.61 % (187803)Termination reason: Instruction limit % 208.37/29.61 % (187803)Termination phase: Saturation % 208.37/29.61 % (187803)Time elapsed: 0.305 s % 208.37/29.61 % (187803)Peak memory usage: 16 MB % 208.37/29.61 % (187803)Instructions burned: 957 (million) % 208.37/29.61 % (187805)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2545367677:fmbsr=1.3:i=1730:ins=25:rtra=on_2799 on theBenchmark for (2799ds/1730Mi) % 208.37/29.61 % Exception at run slice level % 208.37/29.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.37/29.61 % (187807)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=322520929:i=2358:rtra=on_2799 on theBenchmark for (2799ds/2358Mi) % 208.37/29.61 % (187798)Instruction limit reached! % 208.37/29.61 % (187798)------------------------------ % 208.37/29.61 % (187798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.37/29.61 % (187798)Linked with Z3 4.14.0.0 3c47fd96cf5645Terminated %------------------------------------------------------------------------------