%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM990_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 : n009.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 12:26:20 PM UTC 2026 % Result : Timeout 300.32s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM990_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.37 % Computer : n009.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sun Sep 27 21:49:30 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.40 Running first-order model finding % 0.10/0.40 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.58/1.62 % (2431569)Will run a generic schedule for satisfiability detection. % 7.58/1.62 % (2431579)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3815011842:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.58/1.62 % (2431575)% WARNING: option uhcvi not known. % 7.58/1.62 % (2431574)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3992566114_2999 on theBenchmark for (2999ds/0Mi) % 7.58/1.62 % (2431576)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2226354626:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.58/1.62 % (2431577)dis+10_1_sil=32000:sp=arity:random_seed=2641333583:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.58/1.62 % (2431578)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1843665410:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.58/1.62 % (2431580)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3396451859:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.58/1.62 % (2431575)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3853540397:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.58/1.62 % Exception at run slice level % 7.58/1.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.58/1.62 % (2431588)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3458326680:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.58/1.62 % Exception at run slice level % 7.58/1.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.58/1.62 % (2431579)Instruction limit reached! % 7.58/1.62 % (2431579)------------------------------ % 7.58/1.62 % (2431579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.58/1.62 % (2431579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.62 % (2431579)CaDiCaL version: 2.1.3 % 7.58/1.62 % (2431579)Termination reason: Instruction limit % 7.58/1.62 % (2431579)Termination phase: Saturation % 7.58/1.62 % (2431579)Time elapsed: 0.039 s % 7.58/1.62 % (2431579)Peak memory usage: 13 MB % 7.58/1.62 % (2431579)Instructions burned: 132 (million) % 7.58/1.62 % (2431591)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=2314771622:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.58/1.62 % (2431590)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=707459224:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.58/1.62 % (2431577)Instruction limit reached! % 7.58/1.62 % (2431577)------------------------------ % 7.58/1.62 % (2431577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.58/1.62 % (2431577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.62 % (2431577)CaDiCaL version: 2.1.3 % 7.58/1.62 % (2431577)Termination reason: Instruction limit % 7.58/1.62 % (2431577)Termination phase: Saturation % 7.58/1.62 % (2431577)Time elapsed: 0.063 s % 7.58/1.62 % (2431577)Peak memory usage: 12 MB % 7.58/1.62 % (2431577)Instructions burned: 104 (million) % 7.58/1.62 % (2431578)Instruction limit reached! % 7.58/1.62 % (2431578)------------------------------ % 7.58/1.62 % (2431578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.58/1.62 % (2431578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.62 % (2431578)CaDiCaL version: 2.1.3 % 7.58/1.62 % (2431578)Termination reason: Instruction limit % 7.58/1.62 % (2431578)Termination phase: Saturation % 7.58/1.62 % (2431578)Time elapsed: 0.072 s % 7.58/1.62 % (2431578)Peak memory usage: 13 MB % 7.58/1.62 % (2431578)Instructions burned: 116 (million) % 7.58/1.62 % (2431594)ott-21_1_sil=16000:fs=off:random_seed=276774324:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.58/1.62 % (2431595)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2024894820:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.58/1.62 % (2431580)Instruction limit reached! % 7.58/1.62 % (2431580)------------------------------ % 7.58/1.62 % (2431580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.58/1.62 % (2431580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.62 % (2431580)CaDiCaL version: 2.1.3 % 7.58/1.62 % (2431580)Termination reason: Instruction limit % 7.58/1.62 % (2431580)Termination phase: Saturation % 20.39/3.32 % (2431580)Time elapsed: 0.097 s % 20.39/3.32 % (2431580)Peak memory usage: 14 MB % 20.39/3.32 % (2431580)Instructions burned: 159 (million) % 20.39/3.32 % (2431598)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4224681518:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.39/3.32 % Exception at run slice level % 20.39/3.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.39/3.32 % (2431590)Instruction limit reached! % 20.39/3.32 % (2431590)------------------------------ % 20.39/3.32 % (2431590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.39/3.32 % (2431590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.32 % (2431590)CaDiCaL version: 2.1.3 % 20.39/3.32 % (2431590)Termination reason: Instruction limit % 20.39/3.32 % (2431590)Termination phase: Saturation % 20.39/3.32 % (2431590)Time elapsed: 0.081 s % 20.39/3.32 % (2431590)Peak memory usage: 13 MB % 20.39/3.32 % (2431590)Instructions burned: 132 (million) % 20.39/3.32 % (2431600)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=430462087:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.39/3.32 % (2431601)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3026977245:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.39/3.32 % Exception at run slice level % 20.39/3.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.39/3.32 % (2431604)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=2892274482: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.39/3.32 % (2431594)Instruction limit reached! % 20.39/3.32 % (2431594)------------------------------ % 20.39/3.32 % (2431594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.39/3.32 % (2431594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.32 % (2431594)CaDiCaL version: 2.1.3 % 20.39/3.32 % (2431594)Termination reason: Instruction limit % 20.39/3.32 % (2431594)Termination phase: Saturation % 20.39/3.32 % (2431594)Time elapsed: 0.089 s % 20.39/3.32 % (2431594)Peak memory usage: 13 MB % 20.39/3.32 % (2431594)Instructions burned: 181 (million) % 20.39/3.32 % (2431606)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1498899019:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.39/3.32 % (2431591)Instruction limit reached! % 20.39/3.32 % (2431591)------------------------------ % 20.39/3.32 % (2431591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.39/3.32 % (2431591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.32 % (2431591)CaDiCaL version: 2.1.3 % 20.39/3.32 % (2431591)Termination reason: Instruction limit % 20.39/3.32 % (2431591)Termination phase: Saturation % 20.39/3.32 % (2431591)Time elapsed: 0.200 s % 20.39/3.32 % (2431591)Peak memory usage: 17 MB % 20.39/3.32 % (2431591)Instructions burned: 687 (million) % 20.39/3.32 % (2431608)fmb+10_1_sil=64000:random_seed=1932363708:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.39/3.32 % (2431608)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.39/3.32 % Exception at run slice level % 20.39/3.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.39/3.32 % (2431610)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=579200438:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.39/3.32 % Exception at run slice level % 20.39/3.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.39/3.32 % (2431612)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3836758292:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.39/3.32 % Exception at run slice level % 20.39/3.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.39/3.32 % (2431614)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1395577722:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.39/3.32 % (2431595)Instruction limit reached! % 20.39/3.32 % (2431595)------------------------------ % 20.39/3.32 % (2431595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.39/3.32 % (2431595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/10.90 % (2431595)CaDiCaL version: 2.1.3 % 73.70/10.90 % (2431595)Termination reason: Instruction limit % 73.70/10.90 % (2431595)Termination phase: Saturation % 73.70/10.90 % (2431595)Time elapsed: 0.318 s % 73.70/10.90 % (2431595)Peak memory usage: 14 MB % 73.70/10.90 % (2431595)Instructions burned: 478 (million) % 73.70/10.90 % (2431616)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1028957082:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 73.70/10.90 % (2431616)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 73.70/10.90 % (2431604)Instruction limit reached! % 73.70/10.90 % (2431604)------------------------------ % 73.70/10.90 % (2431604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/10.90 % (2431604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/10.90 % (2431604)CaDiCaL version: 2.1.3 % 73.70/10.90 % (2431604)Termination reason: Instruction limit % 73.70/10.90 % (2431604)Termination phase: Saturation % 73.70/10.90 % (2431604)Time elapsed: 0.339 s % 73.70/10.90 % (2431604)Peak memory usage: 17 MB % 73.70/10.90 % (2431604)Instructions burned: 694 (million) % 73.70/10.90 % (2431618)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2105871539:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 73.70/10.90 % Exception at run slice level % 73.70/10.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.70/10.90 % (2431620)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4072048339:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 73.70/10.90 % Exception at run slice level % 73.70/10.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.70/10.90 % (2431622)ott-2_1_sil=16000:newcnf=on:random_seed=3531126678:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 73.70/10.90 % (2431606)Instruction limit reached! % 73.70/10.90 % (2431606)------------------------------ % 73.70/10.90 % (2431606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/10.90 % (2431606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/10.90 % (2431606)CaDiCaL version: 2.1.3 % 73.70/10.90 % (2431606)Termination reason: Instruction limit % 73.70/10.90 % (2431606)Termination phase: Saturation % 73.70/10.90 % (2431606)Time elapsed: 0.490 s % 73.70/10.90 % (2431606)Peak memory usage: 19 MB % 73.70/10.90 % (2431606)Instructions burned: 879 (million) % 73.70/10.90 % (2431624)ott+10_1_sil=32000:tgt=ground:random_seed=3437602922:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 73.70/10.90 % (2431600)Instruction limit reached! % 73.70/10.90 % (2431600)------------------------------ % 73.70/10.90 % (2431600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/10.90 % (2431600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/10.90 % (2431600)CaDiCaL version: 2.1.3 % 73.70/10.90 % (2431600)Termination reason: Instruction limit % 73.70/10.90 % (2431600)Termination phase: Saturation % 73.70/10.90 % (2431600)Time elapsed: 0.667 s % 73.70/10.90 % (2431600)Peak memory usage: 23 MB % 73.70/10.90 % (2431600)Instructions burned: 1180 (million) % 73.70/10.90 % (2431626)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1885120677:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 73.70/10.90 % Exception at run slice level % 73.70/10.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 73.70/10.90 % (2431628)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=126414465:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 73.70/10.90 % (2431622)Instruction limit reached! % 73.70/10.90 % (2431622)------------------------------ % 73.70/10.90 % (2431622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/10.90 % (2431622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/10.90 % (2431622)CaDiCaL version: 2.1.3 % 73.70/10.90 % (2431622)Termination reason: Instruction limit % 73.70/10.90 % (2431622)Termination phase: Saturation % 73.70/10.90 % (2431622)Time elapsed: 0.523 s % 73.70/10.90 % (2431622)Peak memory usage: 18 MB % 73.70/10.90 % (2431622)Instructions burned: 869 (million) % 73.70/10.90 % (2431630)dis+21_1_sil=32000:sas=cadical:random_seed=1327548110:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 73.70/10.90 % (2431616)Instruction limit reached! % 73.70/10.90 % (2431616)------------------------------ % 73.70/10.90 % (2431616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.17/16.50 % (2431616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.17/16.50 % (2431616)CaDiCaL version: 2.1.3 % 114.17/16.50 % (2431616)Termination reason: Instruction limit % 114.17/16.50 % (2431616)Termination phase: Saturation % 114.17/16.50 % (2431616)Time elapsed: 0.747 s % 114.17/16.50 % (2431616)Peak memory usage: 27 MB % 114.17/16.50 % (2431616)Instructions burned: 1474 (million) % 114.17/16.50 % (2431632)ott+11_1_sil=16000:gs=on:random_seed=118603692:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 114.17/16.50 % (2431614)Instruction limit reached! % 114.17/16.50 % (2431614)------------------------------ % 114.17/16.50 % (2431614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.17/16.50 % (2431614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.17/16.50 % (2431614)CaDiCaL version: 2.1.3 % 114.17/16.50 % (2431614)Termination reason: Instruction limit % 114.17/16.50 % (2431614)Termination phase: Saturation % 114.17/16.50 % (2431614)Time elapsed: 1.417 s % 114.17/16.50 % (2431614)Peak memory usage: 44 MB % 114.17/16.50 % (2431614)Instructions burned: 5134 (million) % 114.17/16.50 % (2431634)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1070446199:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 114.17/16.50 % Exception at run slice level % 114.17/16.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.17/16.50 % (2431636)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2757337566:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 114.17/16.50 % (2431632)Instruction limit reached! % 114.17/16.50 % (2431632)------------------------------ % 114.17/16.50 % (2431632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.17/16.50 % (2431632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.17/16.50 % (2431632)CaDiCaL version: 2.1.3 % 114.17/16.50 % (2431632)Termination reason: Instruction limit % 114.17/16.50 % (2431632)Termination phase: Saturation % 114.17/16.50 % (2431632)Time elapsed: 1.191 s % 114.17/16.50 % (2431632)Peak memory usage: 29 MB % 114.17/16.50 % (2431632)Instructions burned: 2252 (million) % 114.17/16.50 % (2431638)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4192589328:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 114.17/16.50 % (2431636)Instruction limit reached! % 114.17/16.50 % (2431636)------------------------------ % 114.17/16.50 % (2431636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.17/16.50 % (2431636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.17/16.50 % (2431636)CaDiCaL version: 2.1.3 % 114.17/16.50 % (2431636)Termination reason: Instruction limit % 114.17/16.50 % (2431636)Termination phase: Saturation % 114.17/16.50 % (2431636)Time elapsed: 1.009 s % 114.17/16.50 % (2431636)Peak memory usage: 39 MB % 114.17/16.50 % (2431636)Instructions burned: 4591 (million) % 114.17/16.50 % (2431640)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3408930387:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 114.17/16.50 % (2431628)Instruction limit reached! % 114.17/16.50 % (2431628)------------------------------ % 114.17/16.50 % (2431628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.17/16.50 % (2431628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.17/16.50 % (2431628)CaDiCaL version: 2.1.3 % 114.17/16.50 % (2431628)Termination reason: Instruction limit % 114.17/16.50 % (2431628)Termination phase: Saturation % 114.17/16.50 % (2431628)Time elapsed: 1.958 s % 114.17/16.50 % (2431628)Peak memory usage: 33 MB % 114.17/16.50 % (2431628)Instructions burned: 3512 (million) % 114.17/16.50 % (2431642)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1020216866:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 114.17/16.50 % Exception at run slice level % 114.17/16.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.17/16.50 % (2431644)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=463774320:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 114.17/16.50 % Exception at run slice level % 114.17/16.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.17/16.50 % (2431646)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=485156969:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 114.17/16.50 % Exception at run slice level % 174.72/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.72/25.11 % (2431648)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4254769342:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 174.72/25.11 % (2431630)Instruction limit reached! % 174.72/25.11 % (2431630)------------------------------ % 174.72/25.11 % (2431630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431630)CaDiCaL version: 2.1.3 % 174.72/25.11 % (2431630)Termination reason: Instruction limit % 174.72/25.11 % (2431630)Termination phase: Saturation % 174.72/25.11 % (2431630)Time elapsed: 2.070 s % 174.72/25.11 % (2431630)Peak memory usage: 40 MB % 174.72/25.11 % (2431630)Instructions burned: 3773 (million) % 174.72/25.11 % (2431650)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1767665485:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 174.72/25.11 % (2431624)Instruction limit reached! % 174.72/25.11 % (2431624)------------------------------ % 174.72/25.11 % (2431624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431624)CaDiCaL version: 2.1.3 % 174.72/25.11 % (2431624)Termination reason: Instruction limit % 174.72/25.11 % (2431624)Termination phase: Saturation % 174.72/25.11 % (2431624)Time elapsed: 2.917 s % 174.72/25.11 % (2431624)Peak memory usage: 56 MB % 174.72/25.11 % (2431624)Instructions burned: 5116 (million) % 174.72/25.11 % (2431652)dis+10_16:1_sil=16000:random_seed=2440491171:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 174.72/25.11 % (2431640)Instruction limit reached! % 174.72/25.11 % (2431640)------------------------------ % 174.72/25.11 % (2431640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431640)CaDiCaL version: 2.1.3 % 174.72/25.11 % (2431640)Termination reason: Instruction limit % 174.72/25.11 % (2431640)Termination phase: Saturation % 174.72/25.11 % (2431640)Time elapsed: 1.420 s % 174.72/25.11 % (2431640)Peak memory usage: 44 MB % 174.72/25.11 % (2431640)Instructions burned: 5212 (million) % 174.72/25.11 % (2431654)ott-3_8_sil=64000:random_seed=984501801:i=20139:bs=on_2957 on theBenchmark for (2957ds/20139Mi) % 174.72/25.11 % (2431650)Instruction limit reached! % 174.72/25.11 % (2431650)------------------------------ % 174.72/25.11 % (2431650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431650)CaDiCaL version: 2.1.3 % 174.72/25.11 % (2431650)Termination reason: Instruction limit % 174.72/25.11 % (2431650)Termination phase: Saturation % 174.72/25.11 % (2431650)Time elapsed: 4.546 s % 174.72/25.11 % (2431650)Peak memory usage: 83 MB % 174.72/25.11 % (2431650)Instructions burned: 8174 (million) % 174.72/25.11 % (2431656)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1492353904:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi) % 174.72/25.11 % Exception at run slice level % 174.72/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.72/25.11 % (2431658)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=456828639:i=11404_2921 on theBenchmark for (2921ds/11404Mi) % 174.72/25.11 % (2431652)Instruction limit reached! % 174.72/25.11 % (2431652)------------------------------ % 174.72/25.11 % (2431652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431652)CaDiCaL version: 2.1.3 % 174.72/25.11 % (2431652)Termination reason: Instruction limit % 174.72/25.11 % (2431652)Termination phase: Saturation % 174.72/25.11 % (2431652)Time elapsed: 4.876 s % 174.72/25.11 % (2431652)Peak memory usage: 74 MB % 174.72/25.11 % (2431652)Instructions burned: 9156 (million) % 174.72/25.11 % (2431660)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1058019832:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 174.72/25.11 % (2431654)Instruction limit reached! % 174.72/25.11 % (2431654)------------------------------ % 174.72/25.11 % (2431654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.72/25.11 % (2431654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.72/25.11 % (2431654)CaDiCaL version: 2.1.3 % 183.44/26.31 % (2431654)Termination reason: Instruction limit % 183.44/26.31 % (2431654)Termination phase: Saturation % 183.44/26.31 % (2431654)Time elapsed: 6.264 s % 183.44/26.31 % (2431654)Peak memory usage: 147 MB % 183.44/26.31 % (2431654)Instructions burned: 20139 (million) % 183.44/26.31 % (2431662)dis+33_16_sil=32000:sac=on:random_seed=3408097028:i=15851:nm=0_2894 on theBenchmark for (2894ds/15851Mi) % 183.44/26.31 % (2431648)Instruction limit reached! % 183.44/26.31 % (2431648)------------------------------ % 183.44/26.31 % (2431648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.44/26.31 % (2431648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.44/26.31 % (2431648)CaDiCaL version: 2.1.3 % 183.44/26.31 % (2431648)Termination reason: Instruction limit % 183.44/26.31 % (2431648)Termination phase: Saturation % 183.44/26.31 % (2431648)Time elapsed: 9.894 s % 183.44/26.31 % (2431648)Peak memory usage: 100 MB % 183.44/26.31 % (2431648)Instructions burned: 22567 (million) % 183.44/26.31 % (2431664)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3322036326:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 183.44/26.31 % (2431658)Instruction limit reached! % 183.44/26.31 % (2431658)------------------------------ % 183.44/26.31 % (2431658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.44/26.31 % (2431658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.44/26.31 % (2431658)CaDiCaL version: 2.1.3 % 183.44/26.31 % (2431658)Termination reason: Instruction limit % 183.44/26.31 % (2431658)Termination phase: Saturation % 183.44/26.31 % (2431658)Time elapsed: 6.801 s % 183.44/26.31 % (2431658)Peak memory usage: 107 MB % 183.44/26.31 % (2431658)Instructions burned: 11404 (million) % 183.44/26.31 % (2431860)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2135354459:s2a=on:i=53295_2853 on theBenchmark for (2853ds/53295Mi) % 183.44/26.31 % (2431662)Instruction limit reached! % 183.44/26.31 % (2431662)------------------------------ % 183.44/26.31 % (2431662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.44/26.31 % (2431662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.44/26.31 % (2431662)CaDiCaL version: 2.1.3 % 183.44/26.31 % (2431662)Termination reason: Instruction limit % 183.44/26.31 % (2431662)Termination phase: Saturation % 183.44/26.31 % (2431662)Time elapsed: 4.574 s % 183.44/26.31 % (2431662)Peak memory usage: 118 MB % 183.44/26.31 % (2431662)Instructions burned: 15855 (million) % 183.44/26.31 % (2431905)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3992923889:i=26857:ins=20_2849 on theBenchmark for (2849ds/26857Mi) % 183.44/26.31 % Exception at run slice level % 183.44/26.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.44/26.31 % (2431909)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3413648320:i=28120:bs=on:fsr=off_2848 on theBenchmark for (2848ds/28120Mi) % 183.44/26.31 % (2431638)Instruction limit reached! % 183.44/26.31 % (2431638)------------------------------ % 183.44/26.31 % (2431638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.44/26.31 % (2431638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.44/26.31 % (2431638)CaDiCaL version: 2.1.3 % 183.44/26.31 % (2431638)Termination reason: Instruction limit % 183.44/26.31 % (2431638)Termination phase: Saturation % 183.44/26.31 % (2431638)Time elapsed: 13.535 s % 183.44/26.31 % (2431638)Peak memory usage: 160 MB % 183.44/26.31 % (2431638)Instructions burned: 29342 (million) % 183.44/26.31 % (2432070)fmb+10_1_sil=256000:fmbss=7:random_seed=3973836250:fmbsr=1.6:i=182295_2839 on theBenchmark for (2839ds/182295Mi) % 183.44/26.31 % Exception at run slice level % 183.44/26.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.44/26.31 % (2432072)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3716640976:i=44625:gsp=on_2839 on theBenchmark for (2839ds/44625Mi) % 183.44/26.31 % (2432072)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 183.44/26.31 % Exception at run slice level % 183.44/26.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.44/26.31 % (2432074)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2156834632:i=160505_2839 on theBenchmark for (2839ds/160505Mi) % 183.44/26.31 % Exception at run slice level % 183.44/26.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.44/26.31 % (2432076)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4254309301:fmbsr=1.3:i=225729_2839 on theBenchmark for (2839ds/225729Mi) % 193.29/27.76 % Exception at run slice level % 193.29/27.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.29/27.76 % (2432078)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=135612422:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 193.29/27.76 % Exception at run slice level % 193.29/27.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.29/27.76 % (2432080)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1563041755:rtra=on_2838 on theBenchmark for (2838ds/0Mi) % 193.29/27.76 % Exception at run slice level % 193.29/27.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.29/27.76 % (2432082)% WARNING: option uhcvi not known. % 193.29/27.76 % (2432082)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=937402946:i=271062:add=off:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/271062Mi) % 193.29/27.76 % (2431660)Instruction limit reached! % 193.29/27.76 % (2431660)------------------------------ % 193.29/27.76 % (2431660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.29/27.76 % (2431660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.29/27.76 % (2431660)CaDiCaL version: 2.1.3 % 193.29/27.76 % (2431660)Termination reason: Instruction limit % 193.29/27.76 % (2431660)Termination phase: Saturation % 193.29/27.76 % (2431660)Time elapsed: 8.629 s % 193.29/27.76 % (2431660)Peak memory usage: 114 MB % 193.29/27.76 % (2431660)Instructions burned: 14135 (million) % 193.29/27.76 % (2432084)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=381939705:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 193.29/27.76 % (2431664)Instruction limit reached! % 193.29/27.76 % (2431664)------------------------------ % 193.29/27.76 % (2431664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.29/27.76 % (2431664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.29/27.76 % (2431664)CaDiCaL version: 2.1.3 % 193.29/27.76 % (2431664)Termination reason: Instruction limit % 193.29/27.76 % (2431664)Termination phase: Saturation % 193.29/27.76 % (2431664)Time elapsed: 11.304 s % 193.29/27.76 % (2431664)Peak memory usage: 423 MB % 193.29/27.76 % (2431664)Instructions burned: 17628 (million) % 193.29/27.76 % (2432086)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2921648053:i=206:fgj=on:rtra=on_2757 on theBenchmark for (2757ds/206Mi) % 193.29/27.76 % (2432086)Instruction limit reached! % 193.29/27.76 % (2432086)------------------------------ % 193.29/27.76 % (2432086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.29/27.76 % (2432086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.29/27.76 % (2432086)CaDiCaL version: 2.1.3 % 193.29/27.76 % (2432086)Termination reason: Instruction limit % 193.29/27.76 % (2432086)Termination phase: Saturation % 193.29/27.76 % (2432086)Time elapsed: 0.125 s % 193.29/27.76 % (2432086)Peak memory usage: 13 MB % 193.29/27.76 % (2432086)Instructions burned: 207 (million) % 193.29/27.76 % (2432088)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=993792832:i=232:rtra=on_2756 on theBenchmark for (2756ds/232Mi) % 193.29/27.76 % (2432088)Instruction limit reached! % 193.29/27.76 % (2432088)------------------------------ % 193.29/27.76 % (2432088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.29/27.76 % (2432088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.29/27.76 % (2432088)CaDiCaL version: 2.1.3 % 193.29/27.76 % (2432088)Termination reason: Instruction limit % 193.29/27.76 % (2432088)Termination phase: Saturation % 193.29/27.76 % (2432088)Time elapsed: 0.146 s % 193.29/27.76 % (2432088)Peak memory usage: 14 MB % 193.29/27.76 % (2432088)Instructions burned: 233 (million) % 193.29/27.76 % (2432090)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3714967902:i=262:rtra=on_2754 on theBenchmark for (2754ds/262Mi) % 193.29/27.76 % (2432090)Instruction limit reached! % 193.29/27.76 % (2432090)------------------------------ % 193.29/27.76 % (2432090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.29/27.76 % (2432090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.29/27.76 % (2432090)CaDiCaL version: 2.1.3 % 193.29/27.76 % (2432090)Termination reason: Instruction limit % 193.29/27.76 % (2432090)Termination phase: Saturation % 244.74/35.02 % (2432090)Time elapsed: 0.149 s % 244.74/35.02 % (2432090)Peak memory usage: 14 MB % 244.74/35.02 % (2432090)Instructions burned: 262 (million) % 244.74/35.02 % (2432092)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=774283231:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2752 on theBenchmark for (2752ds/318Mi) % 244.74/35.02 % (2432092)Instruction limit reached! % 244.74/35.02 % (2432092)------------------------------ % 244.74/35.02 % (2432092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.74/35.02 % (2432092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.74/35.02 % (2432092)CaDiCaL version: 2.1.3 % 244.74/35.02 % (2432092)Termination reason: Instruction limit % 244.74/35.02 % (2432092)Termination phase: Saturation % 244.74/35.02 % (2432092)Time elapsed: 0.175 s % 244.74/35.02 % (2432092)Peak memory usage: 15 MB % 244.74/35.02 % (2432092)Instructions burned: 319 (million) % 244.74/35.02 % (2432094)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=136237093:i=1428:nm=2:rtra=on_2750 on theBenchmark for (2750ds/1428Mi) % 244.74/35.02 % Exception at run slice level % 244.74/35.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 244.74/35.02 % (2432096)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1866377812:i=262:bd=preordered:rtra=on:fsd=on_2750 on theBenchmark for (2750ds/262Mi) % 244.74/35.02 % (2432096)Instruction limit reached! % 244.74/35.02 % (2432096)------------------------------ % 244.74/35.02 % (2432096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.74/35.02 % (2432096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.74/35.02 % (2432096)CaDiCaL version: 2.1.3 % 244.74/35.02 % (2432096)Termination reason: Instruction limit % 244.74/35.02 % (2432096)Termination phase: Saturation % 244.74/35.02 % (2432096)Time elapsed: 0.174 s % 244.74/35.02 % (2432096)Peak memory usage: 15 MB % 244.74/35.02 % (2432096)Instructions burned: 263 (million) % 244.74/35.02 % (2432098)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=1342217831:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1368Mi) % 244.74/35.02 % (2431909)Instruction limit reached! % 244.74/35.02 % (2431909)------------------------------ % 244.74/35.02 % (2431909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.74/35.02 % (2431909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.74/35.02 % (2431909)CaDiCaL version: 2.1.3 % 244.74/35.02 % (2431909)Termination reason: Instruction limit % 244.74/35.02 % (2431909)Termination phase: Saturation % 244.74/35.02 % (2431909)Time elapsed: 10.318 s % 244.74/35.02 % (2431909)Peak memory usage: 338 MB % 244.74/35.02 % (2431909)Instructions burned: 28122 (million) % 244.74/35.02 % (2432100)ott-21_1_sil=16000:si=on:fs=off:random_seed=3524377093:i=360:av=off:fsr=off:rtra=on_2745 on theBenchmark for (2745ds/360Mi) % 244.74/35.02 % (2432100)Instruction limit reached! % 244.74/35.02 % (2432100)------------------------------ % 244.74/35.02 % (2432100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.74/35.02 % (2432100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.74/35.02 % (2432100)CaDiCaL version: 2.1.3 % 244.74/35.02 % (2432100)Termination reason: Instruction limit % 244.74/35.02 % (2432100)Termination phase: Saturation % 244.74/35.02 % (2432100)Time elapsed: 0.095 s % 244.74/35.02 % (2432100)Peak memory usage: 14 MB % 244.74/35.02 % (2432100)Instructions burned: 364 (million) % 244.74/35.02 % (2432102)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4283126304:i=954:bd=all:rtra=on_2744 on theBenchmark for (2744ds/954Mi) % 244.74/35.02 % (2432098)Instruction limit reached! % 244.74/35.02 % (2432098)------------------------------ % 244.74/35.02 % (2432098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.74/35.02 % (2432098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.74/35.02 % (2432098)CaDiCaL version: 2.1.3 % 244.74/35.02 % (2432098)Termination reason: Instruction limit % 244.74/35.02 % (2432098)Termination phase: Saturation % 244.74/35.02 % (2432098)Time elapsed: 0.737 s % 244.74/35.02 % (2432098)Peak memory usage: 19 MB % 244.74/35.02 % (2432098)Instructions burned: 1369 (million) % 244.74/35.02 % (2432104)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2675546195:fmbsr=1.3:i=1730:ins=25:rtra=on_2741 on theBenchmark for (2741ds/1730Mi) % 244.74/35.02 % Exception at run slice level % 244.74/35.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.88/37.09 % (2432102)Instruction limit reached! % 259.88/37.09 % (2432102)------------------------------ % 259.88/37.09 % (2432102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.88/37.09 % (2432102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.88/37.09 % (2432102)CaDiCaL version: 2.1.3 % 259.88/37.09 % (2432102)Termination reason: Instruction limit % 259.88/37.09 % (2432102)Termination phase: Saturation % 259.88/37.09 % (2432102)Time elapsed: 0.309 s % 259.88/37.09 % (2432102)Peak memory usage: 17 MB % 259.88/37.09 % (2432102)Instructions burned: 955 (million) % 259.88/37.09 % (2432106)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2267415281:i=2358:rtra=on_2740 on theBenchmark for (2740ds/2358Mi) % 259.88/37.09 % (2432107)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3528333970:i=1778:ins=1:rtra=on_2740 on theBenchmark for (2740ds/1778Mi) % 259.88/37.09 % Exception at run slice level % 259.88/37.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.88/37.09 % (2432110)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3700585265:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/1384Mi) % 259.88/37.09 % (2432110)Instruction limit reached! % 259.88/37.09 % (2432110)------------------------------ % 259.88/37.09 % (2432110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.88/37.09 % (2432110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.88/37.09 % (2432110)CaDiCaL version: 2.1.3 % 259.88/37.09 % (2432110)Termination reason: Instruction limit % 259.88/37.09 % (2432110)Termination phase: Saturation % 259.88/37.09 % (2432110)Time elapsed: 0.381 s % 259.88/37.09 % (2432110)Peak memory usage: 25 MB % 259.88/37.09 % (2432110)Instructions burned: 1386 (million) % 259.88/37.09 % (2432112)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=120785242:i=1758:kws=inv_precedence:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/1758Mi) % 259.88/37.09 % (2432112)Instruction limit reached! % 259.88/37.09 % (2432112)------------------------------ % 259.88/37.09 % (2432112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.88/37.09 % (2432112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.88/37.09 % (2432112)CaDiCaL version: 2.1.3 % 259.88/37.09 % (2432112)Termination reason: Instruction limit % 259.88/37.09 % (2432112)Termination phase: Saturation % 259.88/37.09 % (2432112)Time elapsed: 0.549 s % 259.88/37.09 % (2432112)Peak memory usage: 25 MB % 259.88/37.09 % (2432112)Instructions burned: 1760 (million) % 259.88/37.09 % (2432114)fmb+10_1_sil=64000:si=on:random_seed=1737841327:i=44122:nm=2:rtra=on:gsp=on_2731 on theBenchmark for (2731ds/44122Mi) % 259.88/37.09 % (2432114)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 259.88/37.09 % Exception at run slice level % 259.88/37.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.88/37.09 % (2432116)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1235557347:i=19030:nm=5:rtra=on_2730 on theBenchmark for (2730ds/19030Mi) % 259.88/37.09 % Exception at run slice level % 259.88/37.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.88/37.09 % (2432118)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1747473543:fmbsr=1.7:i=1840:rtra=on_2730 on theBenchmark for (2730ds/1840Mi) % 259.88/37.09 % Exception at run slice level % 259.88/37.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 259.88/37.09 % (2432120)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3746411573:i=10262:rtra=on_2730 on theBenchmark for (2730ds/10262Mi) % 259.88/37.09 % (2432106)Instruction limit reached! % 259.88/37.09 % (2432106)------------------------------ % 259.88/37.09 % (2432106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.88/37.09 % (2432106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.88/37.09 % (2432106)CaDiCaL version: 2.1.3 % 259.88/37.09 % (2432106)Termination reason: Instruction limit % 259.88/37.09 % (2432106)Termination phase: Saturation % 259.88/37.09 % (2432106)Time elapsed: 1.429 s % 259.88/37.09 % (2432106)Peak memory usage: 36 MB % 300.32/42.83 % (2432106)Instructions burned: 2359 (million) % 300.32/42.83 % (2432122)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=592614947:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2726 on theBenchmark for (2726ds/2944Mi) % 300.32/42.83 % (2432122)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.32/42.83 % (2432122)Instruction limit reached! % 300.32/42.83 % (2432122)------------------------------ % 300.32/42.83 % (2432122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.83 % (2432122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.83 % (2432122)CaDiCaL version: 2.1.3 % 300.32/42.83 % (2432122)Termination reason: Instruction limit % 300.32/42.83 % (2432122)Termination phase: Saturation % 300.32/42.83 % (2432122)Time elapsed: 1.450 s % 300.32/42.83 % (2432122)Peak memory usage: 40 MB % 300.32/42.83 % (2432122)Instructions burned: 2944 (million) % 300.32/42.83 % (2432237)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2330705461:i=12648:rtra=on_2711 on theBenchmark for (2711ds/12648Mi) % 300.32/42.83 % Exception at run slice level % 300.32/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.32/42.83 % (2432243)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3629880267:fmbsr=2.30978:i=4348:rtra=on_2711 on theBenchmark for (2711ds/4348Mi) % 300.32/42.83 % Exception at run slice level % 300.32/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.32/42.83 % (2432255)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3489377098:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2711 on theBenchmark for (2711ds/1738Mi) % 300.32/42.83 % (2432255)Instruction limit reached! % 300.32/42.83 % (2432255)------------------------------ % 300.32/42.83 % (2432255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.83 % (2432255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.83 % (2432255)CaDiCaL version: 2.1.3 % 300.32/42.83 % (2432255)Termination reason: Instruction limit % 300.32/42.83 % (2432255)Termination phase: Saturation % 300.32/42.83 % (2432255)Time elapsed: 1.060 s % 300.32/42.83 % (2432255)Peak memory usage: 25 MB % 300.32/42.83 % (2432255)Instructions burned: 1738 (million) % 300.32/42.83 % (2432120)Instruction limit reached! % 300.32/42.83 % (2432120)------------------------------ % 300.32/42.83 % (2432120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.83 % (2432120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.83 % (2432120)CaDiCaL version: 2.1.3 % 300.32/42.83 % (2432120)Termination reason: Instruction limit % 300.32/42.83 % (2432120)Termination phase: Saturation % 300.32/42.83 % (2432120)Time elapsed: 3.033 s % 300.32/42.83 % (2432120)Peak memory usage: 73 MB % 300.32/42.83 % (2432120)Instructions burned: 10265 (million) % 300.32/42.83 % (2432474)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3067834978:i=10228:av=off:rtra=on_2700 on theBenchmark for (2700ds/10228Mi) % 300.32/42.83 % (2432476)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2096323450:i=108564:rtra=on_2700 on theBenchmark for (2700ds/108564Mi) % 300.32/42.83 % Exception at run slice level % 300.32/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.32/42.83 % (2432478)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=993484528:i=7024:aac=none:rtra=on_2699 on theBenchmark for (2699ds/7024Mi) % 300.32/42.83 % (2432478)Instruction limit reached! % 300.32/42.83 % (2432478)------------------------------ % 300.32/42.83 % (2432478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.83 % (2432478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.83 % (2432478)CaDiCaL version: 2.1.3 % 300.32/42.83 % (2432478)Termination reason: Instruction limit % 300.32/42.83 % (2432478)Termination phase: Saturation % 300.32/42.83 % (2432478)Time elapsed: 2.228 s % 300.32/42.83 % (2432478)Peak memory usage: 55 MB % 300.32/42.83 % (2432478)Instructions burned: 7024 (million) % 300.32/42.83 % (2432480)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3578463104:i=7546:rtra=on:amm=off_2677 on theBenchmark for (2677ds/7546Mi) % 300.32/42.83 % (2432480)Instruction limit reached! % 300.32/42.83 % (2432480)------------------------------ % 300.32/42.83 % (2432480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.83 % (2432480)Linked with Z3 % 300.32/42.83 Terminated % 300.32/42.83 % Vampire exiting %------------------------------------------------------------------------------