%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW560_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:26 PM UTC 2026 % Result : Timeout 300.59s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW560_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 % Computer : n006.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:18:40 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.70/1.43 % (3994412)Will run a generic schedule for satisfiability detection. % 7.70/1.43 % (3994417)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1803997729_2999 on theBenchmark for (2999ds/0Mi) % 7.70/1.43 % (3994418)% WARNING: option uhcvi not known. % 7.70/1.43 % Exception at run slice level % 7.70/1.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.70/1.43 % (3994418)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2853673488:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.70/1.43 % (3994419)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1471565046:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.70/1.43 % (3994420)dis+10_1_sil=32000:sp=arity:random_seed=1032384867:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.70/1.43 % (3994421)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2511044921:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.70/1.43 % (3994422)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2671606717:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.70/1.43 % (3994423)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3119511877:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.70/1.43 % (3994425)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=960250990:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.70/1.43 % Exception at run slice level % 7.70/1.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.70/1.43 % (3994433)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=769877223:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.70/1.43 % (3994420)Instruction limit reached! % 7.70/1.43 % (3994420)------------------------------ % 7.70/1.43 % (3994420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.70/1.43 % (3994420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.43 % (3994420)CaDiCaL version: 2.1.3 % 7.70/1.43 % (3994420)Termination reason: Instruction limit % 7.70/1.43 % (3994420)Termination phase: Saturation % 7.70/1.43 % (3994420)Time elapsed: 0.061 s % 7.70/1.43 % (3994420)Peak memory usage: 12 MB % 7.70/1.43 % (3994420)Instructions burned: 103 (million) % 7.70/1.43 % (3994421)Instruction limit reached! % 7.70/1.43 % (3994421)------------------------------ % 7.70/1.43 % (3994421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.70/1.43 % (3994421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.43 % (3994421)CaDiCaL version: 2.1.3 % 7.70/1.43 % (3994421)Termination reason: Instruction limit % 7.70/1.43 % (3994421)Termination phase: Saturation % 7.70/1.43 % (3994421)Time elapsed: 0.062 s % 7.70/1.43 % (3994421)Peak memory usage: 13 MB % 7.70/1.43 % (3994421)Instructions burned: 116 (million) % 7.70/1.43 % (3994433)Instruction limit reached! % 7.70/1.43 % (3994433)------------------------------ % 7.70/1.43 % (3994433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.70/1.43 % (3994433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.43 % (3994433)CaDiCaL version: 2.1.3 % 7.70/1.43 % (3994433)Termination reason: Instruction limit % 7.70/1.43 % (3994433)Termination phase: Saturation % 7.70/1.43 % (3994433)Time elapsed: 0.041 s % 7.70/1.43 % (3994433)Peak memory usage: 13 MB % 7.70/1.43 % (3994433)Instructions burned: 133 (million) % 7.70/1.43 % (3994437)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2943666729:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.70/1.43 % (3994422)Instruction limit reached! % 7.70/1.43 % (3994422)------------------------------ % 7.70/1.43 % (3994422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.70/1.43 % (3994422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.43 % (3994422)CaDiCaL version: 2.1.3 % 7.70/1.43 % (3994422)Termination reason: Instruction limit % 7.70/1.43 % (3994422)Termination phase: Saturation % 7.70/1.43 % (3994422)Time elapsed: 0.077 s % 7.70/1.43 % (3994422)Peak memory usage: 13 MB % 7.70/1.43 % (3994422)Instructions burned: 132 (million) % 7.70/1.43 % (3994435)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=1533796443:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 20.37/3.18 % (3994436)ott-21_1_sil=16000:fs=off:random_seed=5993757:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 20.37/3.18 % (3994423)Instruction limit reached! % 20.37/3.18 % (3994423)------------------------------ % 20.37/3.18 % (3994423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.37/3.18 % (3994423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.37/3.18 % (3994423)CaDiCaL version: 2.1.3 % 20.37/3.18 % (3994423)Termination reason: Instruction limit % 20.37/3.18 % (3994423)Termination phase: Saturation % 20.37/3.18 % (3994423)Time elapsed: 0.091 s % 20.37/3.18 % (3994423)Peak memory usage: 13 MB % 20.37/3.18 % (3994423)Instructions burned: 161 (million) % 20.37/3.18 % (3994439)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=467183373:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.37/3.18 % Exception at run slice level % 20.37/3.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.37/3.18 % (3994442)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3412461544:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.37/3.18 % (3994444)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3185798612:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.37/3.18 % Exception at run slice level % 20.37/3.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.37/3.18 % (3994447)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=3713832628: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.37/3.18 % (3994436)Instruction limit reached! % 20.37/3.18 % (3994436)------------------------------ % 20.37/3.18 % (3994436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.37/3.18 % (3994436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.37/3.18 % (3994436)CaDiCaL version: 2.1.3 % 20.37/3.18 % (3994436)Termination reason: Instruction limit % 20.37/3.18 % (3994436)Termination phase: Saturation % 20.37/3.18 % (3994436)Time elapsed: 0.092 s % 20.37/3.18 % (3994436)Peak memory usage: 12 MB % 20.37/3.18 % (3994436)Instructions burned: 181 (million) % 20.37/3.18 % (3994449)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1320219552:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.37/3.18 % (3994437)Instruction limit reached! % 20.37/3.18 % (3994437)------------------------------ % 20.37/3.18 % (3994437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.37/3.18 % (3994437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.37/3.18 % (3994437)CaDiCaL version: 2.1.3 % 20.37/3.18 % (3994437)Termination reason: Instruction limit % 20.37/3.18 % (3994437)Termination phase: Saturation % 20.37/3.18 % (3994437)Time elapsed: 0.159 s % 20.37/3.18 % (3994437)Peak memory usage: 14 MB % 20.37/3.18 % (3994437)Instructions burned: 482 (million) % 20.37/3.18 % (3994451)fmb+10_1_sil=64000:random_seed=3357640997:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.37/3.18 % (3994451)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.37/3.18 % Exception at run slice level % 20.37/3.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.37/3.18 % (3994453)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2328051545:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.37/3.18 % Exception at run slice level % 20.37/3.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.37/3.18 % (3994455)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=73011638:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.37/3.18 % Exception at run slice level % 20.37/3.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.37/3.18 % (3994457)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3210778338:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.37/3.18 % (3994435)Instruction limit reached! % 20.37/3.18 % (3994435)------------------------------ % 20.37/3.18 % (3994435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.37/3.18 % (3994435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/9.44 % (3994435)CaDiCaL version: 2.1.3 % 64.87/9.44 % (3994435)Termination reason: Instruction limit % 64.87/9.44 % (3994435)Termination phase: Saturation % 64.87/9.44 % (3994435)Time elapsed: 0.350 s % 64.87/9.44 % (3994435)Peak memory usage: 15 MB % 64.87/9.44 % (3994435)Instructions burned: 684 (million) % 64.87/9.44 % (3994459)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1607029309:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 64.87/9.44 % (3994459)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.87/9.44 % (3994447)Instruction limit reached! % 64.87/9.44 % (3994447)------------------------------ % 64.87/9.44 % (3994447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.87/9.44 % (3994447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/9.44 % (3994447)CaDiCaL version: 2.1.3 % 64.87/9.44 % (3994447)Termination reason: Instruction limit % 64.87/9.44 % (3994447)Termination phase: Saturation % 64.87/9.44 % (3994447)Time elapsed: 0.392 s % 64.87/9.44 % (3994447)Peak memory usage: 15 MB % 64.87/9.44 % (3994447)Instructions burned: 692 (million) % 64.87/9.44 % (3994461)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=220102391:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 64.87/9.44 % Exception at run slice level % 64.87/9.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.87/9.44 % (3994463)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4159995908:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 64.87/9.44 % Exception at run slice level % 64.87/9.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.87/9.44 % (3994465)ott-2_1_sil=16000:newcnf=on:random_seed=631811094:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 64.87/9.44 % (3994449)Instruction limit reached! % 64.87/9.44 % (3994449)------------------------------ % 64.87/9.44 % (3994449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.87/9.44 % (3994449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/9.44 % (3994449)CaDiCaL version: 2.1.3 % 64.87/9.44 % (3994449)Termination reason: Instruction limit % 64.87/9.44 % (3994449)Termination phase: Saturation % 64.87/9.44 % (3994449)Time elapsed: 0.467 s % 64.87/9.44 % (3994449)Peak memory usage: 18 MB % 64.87/9.44 % (3994449)Instructions burned: 881 (million) % 64.87/9.44 % (3994467)ott+10_1_sil=32000:tgt=ground:random_seed=3770700631:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.87/9.44 % (3994442)Instruction limit reached! % 64.87/9.44 % (3994442)------------------------------ % 64.87/9.44 % (3994442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.87/9.44 % (3994442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/9.44 % (3994442)CaDiCaL version: 2.1.3 % 64.87/9.44 % (3994442)Termination reason: Instruction limit % 64.87/9.44 % (3994442)Termination phase: Saturation % 64.87/9.44 % (3994442)Time elapsed: 0.623 s % 64.87/9.44 % (3994442)Peak memory usage: 16 MB % 64.87/9.44 % (3994442)Instructions burned: 1180 (million) % 64.87/9.44 % (3994469)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2393088428:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 64.87/9.44 % Exception at run slice level % 64.87/9.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.87/9.44 % (3994471)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1072166791:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 64.87/9.44 % (3994465)Instruction limit reached! % 64.87/9.44 % (3994465)------------------------------ % 64.87/9.44 % (3994465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.87/9.44 % (3994465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/9.44 % (3994465)CaDiCaL version: 2.1.3 % 64.87/9.44 % (3994465)Termination reason: Instruction limit % 64.87/9.44 % (3994465)Termination phase: Saturation % 64.87/9.44 % (3994465)Time elapsed: 0.419 s % 64.87/9.44 % (3994465)Peak memory usage: 14 MB % 64.87/9.44 % (3994465)Instructions burned: 870 (million) % 64.87/9.44 % (3994473)dis+21_1_sil=32000:sas=cadical:random_seed=2517978092:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 64.87/9.44 % (3994459)Instruction limit reached! % 64.87/9.44 % (3994459)------------------------------ % 64.87/9.44 % (3994459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.93 % (3994459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.93 % (3994459)CaDiCaL version: 2.1.3 % 118.07/16.93 % (3994459)Termination reason: Instruction limit % 118.07/16.93 % (3994459)Termination phase: Saturation % 118.07/16.93 % (3994459)Time elapsed: 0.677 s % 118.07/16.93 % (3994459)Peak memory usage: 18 MB % 118.07/16.93 % (3994459)Instructions burned: 1472 (million) % 118.07/16.93 % (3994475)ott+11_1_sil=16000:gs=on:random_seed=352527335:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 118.07/16.93 % (3994457)Instruction limit reached! % 118.07/16.93 % (3994457)------------------------------ % 118.07/16.93 % (3994457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.93 % (3994457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.93 % (3994457)CaDiCaL version: 2.1.3 % 118.07/16.93 % (3994457)Termination reason: Instruction limit % 118.07/16.93 % (3994457)Termination phase: Saturation % 118.07/16.93 % (3994457)Time elapsed: 1.479 s % 118.07/16.93 % (3994457)Peak memory usage: 34 MB % 118.07/16.93 % (3994457)Instructions burned: 5135 (million) % 118.07/16.93 % (3994477)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4037938597:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 118.07/16.93 % Exception at run slice level % 118.07/16.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.93 % (3994479)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2558351511:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 118.07/16.93 % (3994475)Instruction limit reached! % 118.07/16.93 % (3994475)------------------------------ % 118.07/16.93 % (3994475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.93 % (3994475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.93 % (3994475)CaDiCaL version: 2.1.3 % 118.07/16.93 % (3994475)Termination reason: Instruction limit % 118.07/16.93 % (3994475)Termination phase: Saturation % 118.07/16.93 % (3994475)Time elapsed: 1.172 s % 118.07/16.93 % (3994475)Peak memory usage: 25 MB % 118.07/16.93 % (3994475)Instructions burned: 2251 (million) % 118.07/16.93 % (3994481)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=197760079:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 118.07/16.93 % (3994471)Instruction limit reached! % 118.07/16.93 % (3994471)------------------------------ % 118.07/16.93 % (3994471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.93 % (3994471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.93 % (3994471)CaDiCaL version: 2.1.3 % 118.07/16.93 % (3994471)Termination reason: Instruction limit % 118.07/16.93 % (3994471)Termination phase: Saturation % 118.07/16.93 % (3994471)Time elapsed: 1.850 s % 118.07/16.93 % (3994471)Peak memory usage: 26 MB % 118.07/16.93 % (3994471)Instructions burned: 3512 (million) % 118.07/16.93 % (3994483)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3342006257:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 118.07/16.93 % (3994479)Instruction limit reached! % 118.07/16.93 % (3994479)------------------------------ % 118.07/16.93 % (3994479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.93 % (3994479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.93 % (3994479)CaDiCaL version: 2.1.3 % 118.07/16.93 % (3994479)Termination reason: Instruction limit % 118.07/16.93 % (3994479)Termination phase: Saturation % 118.07/16.93 % (3994479)Time elapsed: 1.017 s % 118.07/16.93 % (3994479)Peak memory usage: 29 MB % 118.07/16.93 % (3994479)Instructions burned: 4593 (million) % 118.07/16.93 % (3994485)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=844368096:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 118.07/16.93 % Exception at run slice level % 118.07/16.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.93 % (3994487)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2656685049:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 118.07/16.93 % Exception at run slice level % 118.07/16.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.93 % (3994489)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2823406500:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 118.07/16.93 % Exception at run slice level % 133.35/19.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.35/19.11 % (3994491)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3812417495:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 133.35/19.11 % (3994473)Instruction limit reached! % 133.35/19.11 % (3994473)------------------------------ % 133.35/19.11 % (3994473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994473)CaDiCaL version: 2.1.3 % 133.35/19.11 % (3994473)Termination reason: Instruction limit % 133.35/19.11 % (3994473)Termination phase: Saturation % 133.35/19.11 % (3994473)Time elapsed: 2.112 s % 133.35/19.11 % (3994473)Peak memory usage: 28 MB % 133.35/19.11 % (3994473)Instructions burned: 3773 (million) % 133.35/19.11 % (3994493)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3318410293:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 133.35/19.11 % (3994467)Instruction limit reached! % 133.35/19.11 % (3994467)------------------------------ % 133.35/19.11 % (3994467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994467)CaDiCaL version: 2.1.3 % 133.35/19.11 % (3994467)Termination reason: Instruction limit % 133.35/19.11 % (3994467)Termination phase: Saturation % 133.35/19.11 % (3994467)Time elapsed: 2.717 s % 133.35/19.11 % (3994467)Peak memory usage: 26 MB % 133.35/19.11 % (3994467)Instructions burned: 5114 (million) % 133.35/19.11 % (3994495)dis+10_16:1_sil=16000:random_seed=1440366360:i=9155:fsr=off_2965 on theBenchmark for (2965ds/9155Mi) % 133.35/19.11 % (3994483)Instruction limit reached! % 133.35/19.11 % (3994483)------------------------------ % 133.35/19.11 % (3994483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994483)CaDiCaL version: 2.1.3 % 133.35/19.11 % (3994483)Termination reason: Instruction limit % 133.35/19.11 % (3994483)Termination phase: Saturation % 133.35/19.11 % (3994483)Time elapsed: 2.689 s % 133.35/19.11 % (3994483)Peak memory usage: 41 MB % 133.35/19.11 % (3994483)Instructions burned: 5212 (million) % 133.35/19.11 % (3994497)ott-3_8_sil=64000:random_seed=1800214822:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 133.35/19.11 % (3994493)Instruction limit reached! % 133.35/19.11 % (3994493)------------------------------ % 133.35/19.11 % (3994493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994493)CaDiCaL version: 2.1.3 % 133.35/19.11 % (3994493)Termination reason: Instruction limit % 133.35/19.11 % (3994493)Termination phase: Saturation % 133.35/19.11 % (3994493)Time elapsed: 4.699 s % 133.35/19.11 % (3994493)Peak memory usage: 54 MB % 133.35/19.11 % (3994493)Instructions burned: 8173 (million) % 133.35/19.11 % (3994499)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3763713398:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 133.35/19.11 % Exception at run slice level % 133.35/19.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.35/19.11 % (3994501)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=429703836:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 133.35/19.11 % (3994495)Instruction limit reached! % 133.35/19.11 % (3994495)------------------------------ % 133.35/19.11 % (3994495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994495)CaDiCaL version: 2.1.3 % 133.35/19.11 % (3994495)Termination reason: Instruction limit % 133.35/19.11 % (3994495)Termination phase: Saturation % 133.35/19.11 % (3994495)Time elapsed: 4.832 s % 133.35/19.11 % (3994495)Peak memory usage: 48 MB % 133.35/19.11 % (3994495)Instructions burned: 9155 (million) % 133.35/19.11 % (3994503)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3564450225:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 133.35/19.11 % (3994491)Instruction limit reached! % 133.35/19.11 % (3994491)------------------------------ % 133.35/19.11 % (3994491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.35/19.11 % (3994491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.35/19.11 % (3994491)CaDiCaL version: 2.1.3 % 145.97/21.03 % (3994491)Termination reason: Instruction limit % 145.97/21.03 % (3994491)Termination phase: Saturation % 145.97/21.03 % (3994491)Time elapsed: 6.243 s % 145.97/21.03 % (3994491)Peak memory usage: 44 MB % 145.97/21.03 % (3994491)Instructions burned: 22566 (million) % 145.97/21.03 % (3994505)dis+33_16_sil=32000:sac=on:random_seed=30575083:i=15851:nm=0_2907 on theBenchmark for (2907ds/15851Mi) % 145.97/21.03 % (3994505)Instruction limit reached! % 145.97/21.03 % (3994505)------------------------------ % 145.97/21.03 % (3994505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.97/21.03 % (3994505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.97/21.03 % (3994505)CaDiCaL version: 2.1.3 % 145.97/21.03 % (3994505)Termination reason: Instruction limit % 145.97/21.03 % (3994505)Termination phase: Saturation % 145.97/21.03 % (3994505)Time elapsed: 3.718 s % 145.97/21.03 % (3994505)Peak memory usage: 25 MB % 145.97/21.03 % (3994505)Instructions burned: 15854 (million) % 145.97/21.03 % (3994507)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1851195852:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 145.97/21.03 % (3994501)Instruction limit reached! % 145.97/21.03 % (3994501)------------------------------ % 145.97/21.03 % (3994501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.97/21.03 % (3994501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.97/21.03 % (3994501)CaDiCaL version: 2.1.3 % 145.97/21.03 % (3994501)Termination reason: Instruction limit % 145.97/21.03 % (3994501)Termination phase: Saturation % 145.97/21.03 % (3994501)Time elapsed: 6.990 s % 145.97/21.03 % (3994501)Peak memory usage: 118 MB % 145.97/21.03 % (3994501)Instructions burned: 11404 (million) % 145.97/21.03 % (3994755)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1568540999:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 145.97/21.03 % (3994497)Instruction limit reached! % 145.97/21.03 % (3994497)------------------------------ % 145.97/21.03 % (3994497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.97/21.03 % (3994497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.97/21.03 % (3994497)CaDiCaL version: 2.1.3 % 145.97/21.03 % (3994497)Termination reason: Instruction limit % 145.97/21.03 % (3994497)Termination phase: Saturation % 145.97/21.03 % (3994497)Time elapsed: 9.920 s % 145.97/21.03 % (3994497)Peak memory usage: 29 MB % 145.97/21.03 % (3994497)Instructions burned: 20140 (million) % 145.97/21.03 % (3994765)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2571362774:i=26857:ins=20_2846 on theBenchmark for (2846ds/26857Mi) % 145.97/21.03 % Exception at run slice level % 145.97/21.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 145.97/21.03 % (3994767)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3330683752:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 145.97/21.03 % (3994481)Instruction limit reached! % 145.97/21.03 % (3994481)------------------------------ % 145.97/21.03 % (3994481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.97/21.03 % (3994481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.97/21.03 % (3994481)CaDiCaL version: 2.1.3 % 145.97/21.03 % (3994481)Termination reason: Instruction limit % 145.97/21.03 % (3994481)Termination phase: Saturation % 145.97/21.03 % (3994481)Time elapsed: 14.096 s % 145.97/21.03 % (3994481)Peak memory usage: 79 MB % 145.97/21.03 % (3994481)Instructions burned: 29341 (million) % 145.97/21.03 % (3994800)fmb+10_1_sil=256000:fmbss=7:random_seed=2618411683:fmbsr=1.6:i=182295_2834 on theBenchmark for (2834ds/182295Mi) % 145.97/21.03 % Exception at run slice level % 145.97/21.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 145.97/21.03 % (3994803)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=594675650:i=44625:gsp=on_2834 on theBenchmark for (2834ds/44625Mi) % 145.97/21.03 % (3994803)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 145.97/21.03 % Exception at run slice level % 145.97/21.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 145.97/21.03 % (3994806)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3846693032:i=160505_2833 on theBenchmark for (2833ds/160505Mi) % 145.97/21.03 % Exception at run slice level % 145.97/21.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 145.97/21.03 % (3994503)Instruction limit reached! % 145.97/21.03 % (3994503)------------------------------ % 205.02/29.20 % (3994503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.02/29.20 % (3994503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.02/29.20 % (3994503)CaDiCaL version: 2.1.3 % 205.02/29.20 % (3994503)Termination reason: Instruction limit % 205.02/29.20 % (3994503)Termination phase: Saturation % 205.02/29.20 % (3994503)Time elapsed: 8.355 s % 205.02/29.20 % (3994503)Peak memory usage: 57 MB % 205.02/29.20 % (3994503)Instructions burned: 14135 (million) % 205.02/29.20 % (3994811)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4277327016:fmbsr=2:i=185024:ins=7_2832 on theBenchmark for (2832ds/185024Mi) % 205.02/29.20 % (3994809)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2521677948:fmbsr=1.3:i=225729_2833 on theBenchmark for (2833ds/225729Mi) % 205.02/29.20 % Exception at run slice level % 205.02/29.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.02/29.20 % Exception at run slice level % 205.02/29.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.02/29.20 % (3994814)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3409148115:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 205.02/29.20 % Exception at run slice level % 205.02/29.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.02/29.20 % (3994815)% WARNING: option uhcvi not known. % 205.02/29.20 % (3994815)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=999240938:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 205.02/29.20 % (3994818)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4089347656:i=176048:add=on:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/176048Mi) % 205.02/29.20 % (3994507)Instruction limit reached! % 205.02/29.20 % (3994507)------------------------------ % 205.02/29.20 % (3994507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.02/29.20 % (3994507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.02/29.20 % (3994507)CaDiCaL version: 2.1.3 % 205.02/29.20 % (3994507)Termination reason: Instruction limit % 205.02/29.20 % (3994507)Termination phase: Saturation % 205.02/29.20 % (3994507)Time elapsed: 5.280 s % 205.02/29.20 % (3994507)Peak memory usage: 33 MB % 205.02/29.20 % (3994507)Instructions burned: 17629 (million) % 205.02/29.20 % (3994856)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4072732005:i=206:fgj=on:rtra=on_2817 on theBenchmark for (2817ds/206Mi) % 205.02/29.20 % (3994856)Instruction limit reached! % 205.02/29.20 % (3994856)------------------------------ % 205.02/29.20 % (3994856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.02/29.20 % (3994856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.02/29.20 % (3994856)CaDiCaL version: 2.1.3 % 205.02/29.20 % (3994856)Termination reason: Instruction limit % 205.02/29.20 % (3994856)Termination phase: Saturation % 205.02/29.20 % (3994856)Time elapsed: 0.185 s % 205.02/29.20 % (3994856)Peak memory usage: 13 MB % 205.02/29.20 % (3994856)Instructions burned: 206 (million) % 205.02/29.20 % (3994863)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1342814624:i=232:rtra=on_2815 on theBenchmark for (2815ds/232Mi) % 205.02/29.20 % (3994863)Instruction limit reached! % 205.02/29.20 % (3994863)------------------------------ % 205.02/29.20 % (3994863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.02/29.20 % (3994863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.02/29.20 % (3994863)CaDiCaL version: 2.1.3 % 205.02/29.20 % (3994863)Termination reason: Instruction limit % 205.02/29.20 % (3994863)Termination phase: Saturation % 205.02/29.20 % (3994863)Time elapsed: 0.181 s % 205.02/29.20 % (3994863)Peak memory usage: 13 MB % 205.02/29.20 % (3994863)Instructions burned: 233 (million) % 205.02/29.20 % (3994870)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2241019541:i=262:rtra=on_2813 on theBenchmark for (2813ds/262Mi) % 205.02/29.20 % (3994870)Instruction limit reached! % 205.02/29.20 % (3994870)------------------------------ % 205.02/29.20 % (3994870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.02/29.20 % (3994870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.02/29.20 % (3994870)CaDiCaL version: 2.1.3 % 205.02/29.20 % (3994870)Termination reason: Instruction limit % 205.02/29.20 % (3994870)Termination phase: Saturation % 273.65/38.83 % (3994870)Time elapsed: 0.159 s % 273.65/38.83 % (3994870)Peak memory usage: 15 MB % 273.65/38.83 % (3994870)Instructions burned: 263 (million) % 273.65/38.83 % (3994874)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=949970497:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2811 on theBenchmark for (2811ds/318Mi) % 273.65/38.83 % (3994874)Instruction limit reached! % 273.65/38.83 % (3994874)------------------------------ % 273.65/38.83 % (3994874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.65/38.83 % (3994874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.65/38.83 % (3994874)CaDiCaL version: 2.1.3 % 273.65/38.83 % (3994874)Termination reason: Instruction limit % 273.65/38.83 % (3994874)Termination phase: Saturation % 273.65/38.83 % (3994874)Time elapsed: 0.217 s % 273.65/38.83 % (3994874)Peak memory usage: 13 MB % 273.65/38.83 % (3994874)Instructions burned: 319 (million) % 273.65/38.83 % (3994882)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4091512889:i=1428:nm=2:rtra=on_2808 on theBenchmark for (2808ds/1428Mi) % 273.65/38.83 % Exception at run slice level % 273.65/38.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 273.65/38.83 % (3994884)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1275988354:i=262:bd=preordered:rtra=on:fsd=on_2808 on theBenchmark for (2808ds/262Mi) % 273.65/38.83 % (3994884)Instruction limit reached! % 273.65/38.83 % (3994884)------------------------------ % 273.65/38.83 % (3994884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.65/38.83 % (3994884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.65/38.83 % (3994884)CaDiCaL version: 2.1.3 % 273.65/38.83 % (3994884)Termination reason: Instruction limit % 273.65/38.83 % (3994884)Termination phase: Saturation % 273.65/38.83 % (3994884)Time elapsed: 0.155 s % 273.65/38.83 % (3994884)Peak memory usage: 14 MB % 273.65/38.83 % (3994884)Instructions burned: 263 (million) % 273.65/38.83 % (3994887)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=1082990170:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1368Mi) % 273.65/38.83 % (3994887)Instruction limit reached! % 273.65/38.83 % (3994887)------------------------------ % 273.65/38.83 % (3994887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.65/38.83 % (3994887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.65/38.83 % (3994887)CaDiCaL version: 2.1.3 % 273.65/38.83 % (3994887)Termination reason: Instruction limit % 273.65/38.83 % (3994887)Termination phase: Saturation % 273.65/38.83 % (3994887)Time elapsed: 0.663 s % 273.65/38.83 % (3994887)Peak memory usage: 16 MB % 273.65/38.83 % (3994887)Instructions burned: 1369 (million) % 273.65/38.83 % (3994900)ott-21_1_sil=16000:si=on:fs=off:random_seed=180141296:i=360:av=off:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/360Mi) % 273.65/38.83 % (3994900)Instruction limit reached! % 273.65/38.83 % (3994900)------------------------------ % 273.65/38.83 % (3994900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.65/38.83 % (3994900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.65/38.83 % (3994900)CaDiCaL version: 2.1.3 % 273.65/38.83 % (3994900)Termination reason: Instruction limit % 273.65/38.83 % (3994900)Termination phase: Saturation % 273.65/38.83 % (3994900)Time elapsed: 0.129 s % 273.65/38.83 % (3994900)Peak memory usage: 13 MB % 273.65/38.83 % (3994900)Instructions burned: 360 (million) % 273.65/38.83 % (3994905)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2546741868:i=954:bd=all:rtra=on_2798 on theBenchmark for (2798ds/954Mi) % 273.65/38.83 % (3994905)Instruction limit reached! % 273.65/38.83 % (3994905)------------------------------ % 273.65/38.83 % (3994905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.65/38.83 % (3994905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.65/38.83 % (3994905)CaDiCaL version: 2.1.3 % 273.65/38.83 % (3994905)Termination reason: Instruction limit % 273.65/38.83 % (3994905)Termination phase: Saturation % 273.65/38.83 % (3994905)Time elapsed: 0.559 s % 273.65/38.83 % (3994905)Peak memory usage: 16 MB % 273.65/38.83 % (3994905)Instructions burned: 959 (million) % 273.65/38.83 % (3994914)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1979044088:fmbsr=1.3:i=1730:ins=25:rtra=on_2792 on theBenchmark for (2792ds/1730Mi) % 273.65/38.83 % Exception at run slice level % 273.65/38.83 User error: Finite model building is currently noTerminated % 300.59/42.64 % Vampire exiting % 300.59/42.64 Terminated %------------------------------------------------------------------------------