%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV759_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 : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:21 PM UTC 2026 % Result : Timeout 300.63s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV759_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.07/0.19 % Computer : n017.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 12:24:36 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/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 % 8.18/1.53 % (3508937)Will run a generic schedule for satisfiability detection. % 8.18/1.53 % (3508947)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1050126710_2999 on theBenchmark for (2999ds/0Mi) % 8.18/1.53 % (3508948)% WARNING: option uhcvi not known. % 8.18/1.53 % Exception at run slice level % 8.18/1.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.18/1.53 % (3508949)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3746289865:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.18/1.53 % (3508948)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3501957922:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.18/1.53 % (3508952)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3968164792:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.18/1.53 % (3508950)dis+10_1_sil=32000:sp=arity:random_seed=1561327149:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.18/1.53 % (3508951)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1875562840:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.18/1.53 % (3508953)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1686089016:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.18/1.53 % (3508959)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2087622631:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.18/1.53 % Exception at run slice level % 8.18/1.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.18/1.53 % (3508971)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1761841847:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.18/1.53 % (3508950)Instruction limit reached! % 8.18/1.53 % (3508950)------------------------------ % 8.18/1.53 % (3508950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.53 % (3508950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.53 % (3508950)CaDiCaL version: 2.1.3 % 8.18/1.53 % (3508950)Termination reason: Instruction limit % 8.18/1.53 % (3508950)Termination phase: Saturation % 8.18/1.53 % (3508950)Time elapsed: 0.064 s % 8.18/1.53 % (3508950)Peak memory usage: 12 MB % 8.18/1.53 % (3508950)Instructions burned: 104 (million) % 8.18/1.53 % (3508971)Instruction limit reached! % 8.18/1.53 % (3508971)------------------------------ % 8.18/1.53 % (3508971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.53 % (3508971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.53 % (3508971)CaDiCaL version: 2.1.3 % 8.18/1.53 % (3508971)Termination reason: Instruction limit % 8.18/1.53 % (3508971)Termination phase: Saturation % 8.18/1.53 % (3508971)Time elapsed: 0.046 s % 8.18/1.53 % (3508971)Peak memory usage: 13 MB % 8.18/1.53 % (3508971)Instructions burned: 131 (million) % 8.18/1.53 % (3508951)Instruction limit reached! % 8.18/1.53 % (3508951)------------------------------ % 8.18/1.53 % (3508951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.53 % (3508951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.53 % (3508951)CaDiCaL version: 2.1.3 % 8.18/1.53 % (3508951)Termination reason: Instruction limit % 8.18/1.53 % (3508951)Termination phase: Saturation % 8.18/1.53 % (3508951)Time elapsed: 0.069 s % 8.18/1.53 % (3508951)Peak memory usage: 13 MB % 8.18/1.53 % (3508951)Instructions burned: 116 (million) % 8.18/1.53 % (3508990)ott-21_1_sil=16000:fs=off:random_seed=490230305:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.18/1.53 % (3508952)Instruction limit reached! % 8.18/1.53 % (3508952)------------------------------ % 8.18/1.53 % (3508952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.53 % (3508952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.53 % (3508952)CaDiCaL version: 2.1.3 % 8.18/1.53 % (3508952)Termination reason: Instruction limit % 8.18/1.53 % (3508952)Termination phase: Saturation % 8.18/1.53 % (3508952)Time elapsed: 0.081 s % 8.18/1.53 % (3508952)Peak memory usage: 13 MB % 8.18/1.53 % (3508952)Instructions burned: 131 (million) % 8.18/1.53 % (3508988)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=1855271213:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.18/1.53 % (3508991)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1770587984:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 26.87/4.11 % (3508953)Instruction limit reached! % 26.87/4.11 % (3508953)------------------------------ % 26.87/4.11 % (3508953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.11 % (3508953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.11 % (3508953)CaDiCaL version: 2.1.3 % 26.87/4.11 % (3508953)Termination reason: Instruction limit % 26.87/4.11 % (3508953)Termination phase: Saturation % 26.87/4.11 % (3508953)Time elapsed: 0.088 s % 26.87/4.11 % (3508953)Peak memory usage: 13 MB % 26.87/4.11 % (3508953)Instructions burned: 159 (million) % 26.87/4.11 % (3508997)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=555523360:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 26.87/4.11 % Exception at run slice level % 26.87/4.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 26.87/4.11 % (3509002)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1545279426:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 26.87/4.11 % (3508990)Instruction limit reached! % 26.87/4.11 % (3508990)------------------------------ % 26.87/4.11 % (3508990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.11 % (3508990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.11 % (3508990)CaDiCaL version: 2.1.3 % 26.87/4.11 % (3508990)Termination reason: Instruction limit % 26.87/4.11 % (3508990)Termination phase: Saturation % 26.87/4.11 % (3508990)Time elapsed: 0.040 s % 26.87/4.11 % (3508990)Peak memory usage: 12 MB % 26.87/4.11 % (3508990)Instructions burned: 182 (million) % 26.87/4.11 % (3509009)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=309480676:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 26.87/4.11 % Exception at run slice level % 26.87/4.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 26.87/4.11 % (3509019)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=70419407: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) % 26.87/4.11 % (3509025)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2671294754:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 26.87/4.11 % (3509019)Instruction limit reached! % 26.87/4.11 % (3509019)------------------------------ % 26.87/4.11 % (3509019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.11 % (3509019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.11 % (3509019)CaDiCaL version: 2.1.3 % 26.87/4.11 % (3509019)Termination reason: Instruction limit % 26.87/4.11 % (3509019)Termination phase: Saturation % 26.87/4.11 % (3509019)Time elapsed: 0.248 s % 26.87/4.11 % (3509019)Peak memory usage: 18 MB % 26.87/4.11 % (3509019)Instructions burned: 695 (million) % 26.87/4.11 % (3509083)fmb+10_1_sil=64000:random_seed=3705558953:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 26.87/4.11 % (3508991)Instruction limit reached! % 26.87/4.11 % (3508991)------------------------------ % 26.87/4.11 % (3508991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.11 % (3508991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.11 % (3508991)CaDiCaL version: 2.1.3 % 26.87/4.11 % (3508991)Termination reason: Instruction limit % 26.87/4.11 % (3508991)Termination phase: Saturation % 26.87/4.11 % (3508991)Time elapsed: 0.310 s % 26.87/4.11 % (3508991)Peak memory usage: 14 MB % 26.87/4.11 % (3508991)Instructions burned: 477 (million) % 26.87/4.11 % (3509083)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 26.87/4.11 % Exception at run slice level % 26.87/4.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 26.87/4.11 % (3509092)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1205214460:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 26.87/4.11 % Exception at run slice level % 26.87/4.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 26.87/4.11 % (3509091)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2391925729:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 26.87/4.11 % Exception at run slice level % 26.87/4.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.08/9.73 % (3509100)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=620275768:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 67.08/9.73 % (3509100)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 67.08/9.73 % (3509095)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=142176512:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 67.08/9.73 % (3508988)Instruction limit reached! % 67.08/9.73 % (3508988)------------------------------ % 67.08/9.73 % (3508988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.08/9.73 % (3508988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.08/9.73 % (3508988)CaDiCaL version: 2.1.3 % 67.08/9.73 % (3508988)Termination reason: Instruction limit % 67.08/9.73 % (3508988)Termination phase: Saturation % 67.08/9.73 % (3508988)Time elapsed: 0.406 s % 67.08/9.73 % (3508988)Peak memory usage: 16 MB % 67.08/9.73 % (3508988)Instructions burned: 685 (million) % 67.08/9.73 % (3509108)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2236546246:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 67.08/9.73 % Exception at run slice level % 67.08/9.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.08/9.73 % (3509110)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3984742612:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 67.08/9.73 % Exception at run slice level % 67.08/9.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.08/9.73 % (3509112)ott-2_1_sil=16000:newcnf=on:random_seed=2317259370:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 67.08/9.73 % (3509025)Instruction limit reached! % 67.08/9.73 % (3509025)------------------------------ % 67.08/9.73 % (3509025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.08/9.73 % (3509025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.08/9.73 % (3509025)CaDiCaL version: 2.1.3 % 67.08/9.73 % (3509025)Termination reason: Instruction limit % 67.08/9.73 % (3509025)Termination phase: Saturation % 67.08/9.73 % (3509025)Time elapsed: 0.498 s % 67.08/9.73 % (3509025)Peak memory usage: 17 MB % 67.08/9.73 % (3509025)Instructions burned: 880 (million) % 67.08/9.73 % (3509114)ott+10_1_sil=32000:tgt=ground:random_seed=3222520048:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 67.08/9.73 % (3509002)Instruction limit reached! % 67.08/9.73 % (3509002)------------------------------ % 67.08/9.73 % (3509002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.08/9.73 % (3509002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.08/9.73 % (3509002)CaDiCaL version: 2.1.3 % 67.08/9.73 % (3509002)Termination reason: Instruction limit % 67.08/9.73 % (3509002)Termination phase: Saturation % 67.08/9.73 % (3509002)Time elapsed: 0.739 s % 67.08/9.73 % (3509002)Peak memory usage: 21 MB % 67.08/9.73 % (3509002)Instructions burned: 1179 (million) % 67.08/9.73 % (3509116)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=44525091:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 67.08/9.73 % Exception at run slice level % 67.08/9.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.08/9.73 % (3509100)Instruction limit reached! % 67.08/9.73 % (3509100)------------------------------ % 67.08/9.73 % (3509100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.08/9.73 % (3509100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.08/9.73 % (3509100)CaDiCaL version: 2.1.3 % 67.08/9.73 % (3509100)Termination reason: Instruction limit % 67.08/9.73 % (3509100)Termination phase: Saturation % 67.08/9.73 % (3509100)Time elapsed: 0.458 s % 67.08/9.73 % (3509100)Peak memory usage: 31 MB % 67.08/9.73 % (3509100)Instructions burned: 1475 (million) % 67.08/9.73 % (3509118)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3702618213:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 67.08/9.73 % (3509119)dis+21_1_sil=32000:sas=cadical:random_seed=4062156480:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 67.08/9.73 % (3509112)Instruction limit reached! % 67.08/9.73 % (3509112)------------------------------ % 67.08/9.73 % (3509112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.50/16.40 % (3509112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.50/16.40 % (3509112)CaDiCaL version: 2.1.3 % 114.50/16.40 % (3509112)Termination reason: Instruction limit % 114.50/16.40 % (3509112)Termination phase: Saturation % 114.50/16.40 % (3509112)Time elapsed: 0.680 s % 114.50/16.40 % (3509112)Peak memory usage: 15 MB % 114.50/16.40 % (3509112)Instructions burned: 870 (million) % 114.50/16.40 % (3509130)ott+11_1_sil=16000:gs=on:random_seed=38253547:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 114.50/16.40 % (3509119)Instruction limit reached! % 114.50/16.40 % (3509119)------------------------------ % 114.50/16.40 % (3509119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.50/16.40 % (3509119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.50/16.40 % (3509119)CaDiCaL version: 2.1.3 % 114.50/16.40 % (3509119)Termination reason: Instruction limit % 114.50/16.40 % (3509119)Termination phase: Saturation % 114.50/16.40 % (3509119)Time elapsed: 1.541 s % 114.50/16.40 % (3509119)Peak memory usage: 26 MB % 114.50/16.40 % (3509119)Instructions burned: 3773 (million) % 114.50/16.40 % (3509160)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2392532872:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 114.50/16.40 % Exception at run slice level % 114.50/16.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.50/16.40 % (3509163)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1356268947:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 114.50/16.40 % (3509130)Instruction limit reached! % 114.50/16.40 % (3509130)------------------------------ % 114.50/16.40 % (3509130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.50/16.40 % (3509130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.50/16.40 % (3509130)CaDiCaL version: 2.1.3 % 114.50/16.40 % (3509130)Termination reason: Instruction limit % 114.50/16.40 % (3509130)Termination phase: Saturation % 114.50/16.40 % (3509130)Time elapsed: 1.755 s % 114.50/16.40 % (3509130)Peak memory usage: 25 MB % 114.50/16.40 % (3509130)Instructions burned: 2251 (million) % 114.50/16.40 % (3509167)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2519481924:i=29340_2969 on theBenchmark for (2969ds/29340Mi) % 114.50/16.40 % (3509118)Instruction limit reached! % 114.50/16.40 % (3509118)------------------------------ % 114.50/16.40 % (3509118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.50/16.40 % (3509118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.50/16.40 % (3509118)CaDiCaL version: 2.1.3 % 114.50/16.40 % (3509118)Termination reason: Instruction limit % 114.50/16.40 % (3509118)Termination phase: Saturation % 114.50/16.40 % (3509118)Time elapsed: 2.324 s % 114.50/16.40 % (3509118)Peak memory usage: 26 MB % 114.50/16.40 % (3509118)Instructions burned: 3512 (million) % 114.50/16.40 % (3509202)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2301564731:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 114.50/16.40 % (3509095)Instruction limit reached! % 114.50/16.40 % (3509095)------------------------------ % 114.50/16.40 % (3509095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.50/16.40 % (3509095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.50/16.40 % (3509095)CaDiCaL version: 2.1.3 % 114.50/16.40 % (3509095)Termination reason: Instruction limit % 114.50/16.40 % (3509095)Termination phase: Saturation % 114.50/16.40 % (3509095)Time elapsed: 3.299 s % 114.50/16.40 % (3509095)Peak memory usage: 25 MB % 114.50/16.40 % (3509095)Instructions burned: 5132 (million) % 114.50/16.40 % (3509323)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2969604729:i=5497:nm=2_2962 on theBenchmark for (2962ds/5497Mi) % 114.50/16.40 % Exception at run slice level % 114.50/16.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.50/16.40 % (3509325)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2588665324:fmbsr=2:i=46332_2961 on theBenchmark for (2961ds/46332Mi) % 114.50/16.40 % Exception at run slice level % 114.50/16.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.50/16.40 % (3509327)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1048654111:i=14071_2961 on theBenchmark for (2961ds/14071Mi) % 114.50/16.40 % Exception at run slice level % 153.58/21.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.58/21.96 % (3509329)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=912817597:i=22565:add=on:rawr=on_2961 on theBenchmark for (2961ds/22565Mi) % 153.58/21.96 % (3509163)Instruction limit reached! % 153.58/21.96 % (3509163)------------------------------ % 153.58/21.96 % (3509163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509163)CaDiCaL version: 2.1.3 % 153.58/21.96 % (3509163)Termination reason: Instruction limit % 153.58/21.96 % (3509163)Termination phase: Saturation % 153.58/21.96 % (3509163)Time elapsed: 1.361 s % 153.58/21.96 % (3509163)Peak memory usage: 57 MB % 153.58/21.96 % (3509163)Instructions burned: 4591 (million) % 153.58/21.96 % (3509331)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=365846986:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 153.58/21.96 % (3509114)Instruction limit reached! % 153.58/21.96 % (3509114)------------------------------ % 153.58/21.96 % (3509114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509114)CaDiCaL version: 2.1.3 % 153.58/21.96 % (3509114)Termination reason: Instruction limit % 153.58/21.96 % (3509114)Termination phase: Saturation % 153.58/21.96 % (3509114)Time elapsed: 3.537 s % 153.58/21.96 % (3509114)Peak memory usage: 41 MB % 153.58/21.96 % (3509114)Instructions burned: 5114 (million) % 153.58/21.96 % (3509333)dis+10_16:1_sil=16000:random_seed=802631273:i=9155:fsr=off_2957 on theBenchmark for (2957ds/9155Mi) % 153.58/21.96 % (3509202)Instruction limit reached! % 153.58/21.96 % (3509202)------------------------------ % 153.58/21.96 % (3509202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509202)CaDiCaL version: 2.1.3 % 153.58/21.96 % (3509202)Termination reason: Instruction limit % 153.58/21.96 % (3509202)Termination phase: Saturation % 153.58/21.96 % (3509202)Time elapsed: 2.660 s % 153.58/21.96 % (3509202)Peak memory usage: 38 MB % 153.58/21.96 % (3509202)Instructions burned: 5211 (million) % 153.58/21.96 % (3509335)ott-3_8_sil=64000:random_seed=1674515408:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 153.58/21.96 % (3509331)Instruction limit reached! % 153.58/21.96 % (3509331)------------------------------ % 153.58/21.96 % (3509331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509331)CaDiCaL version: 2.1.3 % 153.58/21.96 % (3509331)Termination reason: Instruction limit % 153.58/21.96 % (3509331)Termination phase: Saturation % 153.58/21.96 % (3509331)Time elapsed: 2.542 s % 153.58/21.96 % (3509331)Peak memory usage: 62 MB % 153.58/21.96 % (3509331)Instructions burned: 8176 (million) % 153.58/21.96 % (3509337)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1366746618:fmbsr=2:i=32576_2935 on theBenchmark for (2935ds/32576Mi) % 153.58/21.96 % Exception at run slice level % 153.58/21.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.58/21.96 % (3509339)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2956311802:i=11404_2935 on theBenchmark for (2935ds/11404Mi) % 153.58/21.96 % (3509333)Instruction limit reached! % 153.58/21.96 % (3509333)------------------------------ % 153.58/21.96 % (3509333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509333)CaDiCaL version: 2.1.3 % 153.58/21.96 % (3509333)Termination reason: Instruction limit % 153.58/21.96 % (3509333)Termination phase: Saturation % 153.58/21.96 % (3509333)Time elapsed: 4.405 s % 153.58/21.96 % (3509333)Peak memory usage: 40 MB % 153.58/21.96 % (3509333)Instructions burned: 9156 (million) % 153.58/21.96 % (3509342)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1646194874:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 153.58/21.96 % (3509339)Instruction limit reached! % 153.58/21.96 % (3509339)------------------------------ % 153.58/21.96 % (3509339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.58/21.96 % (3509339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/21.96 % (3509339)CaDiCaL version: 2.1.3 % 167.34/23.99 % (3509339)Termination reason: Instruction limit % 167.34/23.99 % (3509339)Termination phase: Saturation % 167.34/23.99 % (3509339)Time elapsed: 2.991 s % 167.34/23.99 % (3509339)Peak memory usage: 66 MB % 167.34/23.99 % (3509339)Instructions burned: 11406 (million) % 167.34/23.99 % (3509344)dis+33_16_sil=32000:sac=on:random_seed=3074054422:i=15851:nm=0_2905 on theBenchmark for (2905ds/15851Mi) % 167.34/23.99 % (3509329)Instruction limit reached! % 167.34/23.99 % (3509329)------------------------------ % 167.34/23.99 % (3509329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.34/23.99 % (3509329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.34/23.99 % (3509329)CaDiCaL version: 2.1.3 % 167.34/23.99 % (3509329)Termination reason: Instruction limit % 167.34/23.99 % (3509329)Termination phase: Saturation % 167.34/23.99 % (3509329)Time elapsed: 8.395 s % 167.34/23.99 % (3509329)Peak memory usage: 40 MB % 167.34/23.99 % (3509329)Instructions burned: 22565 (million) % 167.34/23.99 % (3509346)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2018957487:avsq=on:i=17627:add=on:amm=off_2877 on theBenchmark for (2877ds/17627Mi) % 167.34/23.99 % (3509344)Instruction limit reached! % 167.34/23.99 % (3509344)------------------------------ % 167.34/23.99 % (3509344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.34/23.99 % (3509344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.34/23.99 % (3509344)CaDiCaL version: 2.1.3 % 167.34/23.99 % (3509344)Termination reason: Instruction limit % 167.34/23.99 % (3509344)Termination phase: Saturation % 167.34/23.99 % (3509344)Time elapsed: 4.706 s % 167.34/23.99 % (3509344)Peak memory usage: 110 MB % 167.34/23.99 % (3509344)Instructions burned: 15852 (million) % 167.34/23.99 % (3509385)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1551377747:s2a=on:i=53295_2857 on theBenchmark for (2857ds/53295Mi) % 167.34/23.99 % (3509335)Instruction limit reached! % 167.34/23.99 % (3509335)------------------------------ % 167.34/23.99 % (3509335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.34/23.99 % (3509335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.34/23.99 % (3509335)CaDiCaL version: 2.1.3 % 167.34/23.99 % (3509335)Termination reason: Instruction limit % 167.34/23.99 % (3509335)Termination phase: Saturation % 167.34/23.99 % (3509335)Time elapsed: 10.011 s % 167.34/23.99 % (3509335)Peak memory usage: 62 MB % 167.34/23.99 % (3509335)Instructions burned: 20139 (million) % 167.34/23.99 % (3509396)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3344318453:i=26857:ins=20_2840 on theBenchmark for (2840ds/26857Mi) % 167.34/23.99 % Exception at run slice level % 167.34/23.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.34/23.99 % (3509398)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2659501728:i=28120:bs=on:fsr=off_2839 on theBenchmark for (2839ds/28120Mi) % 167.34/23.99 % (3509342)Instruction limit reached! % 167.34/23.99 % (3509342)------------------------------ % 167.34/23.99 % (3509342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.34/23.99 % (3509342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.34/23.99 % (3509342)CaDiCaL version: 2.1.3 % 167.34/23.99 % (3509342)Termination reason: Instruction limit % 167.34/23.99 % (3509342)Termination phase: Saturation % 167.34/23.99 % (3509342)Time elapsed: 7.358 s % 167.34/23.99 % (3509342)Peak memory usage: 96 MB % 167.34/23.99 % (3509342)Instructions burned: 14135 (million) % 167.34/23.99 % (3509400)fmb+10_1_sil=256000:fmbss=7:random_seed=2227019807:fmbsr=1.6:i=182295_2839 on theBenchmark for (2839ds/182295Mi) % 167.34/23.99 % Exception at run slice level % 167.34/23.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.34/23.99 % (3509402)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=599623951:i=44625:gsp=on_2839 on theBenchmark for (2839ds/44625Mi) % 167.34/23.99 % (3509402)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 167.34/23.99 % Exception at run slice level % 167.34/23.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.34/23.99 % (3509404)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=417916548:i=160505_2838 on theBenchmark for (2838ds/160505Mi) % 167.34/23.99 % Exception at run slice level % 167.34/23.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.34/23.99 % (3509406)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2036290814:fmbsr=1.3:i=225729_2838 on theBenchmark for (2838ds/225729Mi) % 201.25/28.61 % Exception at run slice level % 201.25/28.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 201.25/28.61 % (3509408)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4160751125:fmbsr=2:i=185024:ins=7_2838 on theBenchmark for (2838ds/185024Mi) % 201.25/28.61 % Exception at run slice level % 201.25/28.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 201.25/28.61 % (3509410)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3643595823:rtra=on_2838 on theBenchmark for (2838ds/0Mi) % 201.25/28.61 % Exception at run slice level % 201.25/28.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 201.25/28.61 % (3509412)% WARNING: option uhcvi not known. % 201.25/28.61 % (3509412)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=822517114:i=271062:add=off:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/271062Mi) % 201.25/28.61 % (3509167)Instruction limit reached! % 201.25/28.61 % (3509167)------------------------------ % 201.25/28.61 % (3509167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.61 % (3509167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.61 % (3509167)CaDiCaL version: 2.1.3 % 201.25/28.61 % (3509167)Termination reason: Instruction limit % 201.25/28.61 % (3509167)Termination phase: Saturation % 201.25/28.61 % (3509167)Time elapsed: 16.208 s % 201.25/28.61 % (3509167)Peak memory usage: 160 MB % 201.25/28.61 % (3509167)Instructions burned: 29342 (million) % 201.25/28.61 % (3509414)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=622165262:i=176048:add=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/176048Mi) % 201.25/28.61 % (3509346)Instruction limit reached! % 201.25/28.61 % (3509346)------------------------------ % 201.25/28.61 % (3509346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.61 % (3509346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.61 % (3509346)CaDiCaL version: 2.1.3 % 201.25/28.61 % (3509346)Termination reason: Instruction limit % 201.25/28.61 % (3509346)Termination phase: Saturation % 201.25/28.61 % (3509346)Time elapsed: 8.910 s % 201.25/28.61 % (3509346)Peak memory usage: 112 MB % 201.25/28.61 % (3509346)Instructions burned: 17628 (million) % 201.25/28.61 % (3509416)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2709127522:i=206:fgj=on:rtra=on_2787 on theBenchmark for (2787ds/206Mi) % 201.25/28.61 % (3509416)Instruction limit reached! % 201.25/28.61 % (3509416)------------------------------ % 201.25/28.61 % (3509416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.61 % (3509416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.61 % (3509416)CaDiCaL version: 2.1.3 % 201.25/28.61 % (3509416)Termination reason: Instruction limit % 201.25/28.61 % (3509416)Termination phase: Saturation % 201.25/28.61 % (3509416)Time elapsed: 0.130 s % 201.25/28.61 % (3509416)Peak memory usage: 13 MB % 201.25/28.61 % (3509416)Instructions burned: 207 (million) % 201.25/28.61 % (3509418)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1301764075:i=232:rtra=on_2786 on theBenchmark for (2786ds/232Mi) % 201.25/28.61 % (3509418)Instruction limit reached! % 201.25/28.61 % (3509418)------------------------------ % 201.25/28.61 % (3509418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.61 % (3509418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.61 % (3509418)CaDiCaL version: 2.1.3 % 201.25/28.61 % (3509418)Termination reason: Instruction limit % 201.25/28.61 % (3509418)Termination phase: Saturation % 201.25/28.61 % (3509418)Time elapsed: 0.143 s % 201.25/28.61 % (3509418)Peak memory usage: 13 MB % 201.25/28.61 % (3509418)Instructions burned: 233 (million) % 201.25/28.61 % (3509420)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1526505957:i=262:rtra=on_2784 on theBenchmark for (2784ds/262Mi) % 201.25/28.61 % (3509420)Instruction limit reached! % 201.25/28.61 % (3509420)------------------------------ % 201.25/28.61 % (3509420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.61 % (3509420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.61 % (3509420)CaDiCaL version: 2.1.3 % 201.25/28.61 % (3509420)Termination reason: Instruction limit % 201.25/28.61 % (3509420)Termination phase: Saturation % 234.97/33.48 % (3509420)Time elapsed: 0.156 s % 234.97/33.48 % (3509420)Peak memory usage: 14 MB % 234.97/33.48 % (3509420)Instructions burned: 262 (million) % 234.97/33.48 % (3509422)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=267992154:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2782 on theBenchmark for (2782ds/318Mi) % 234.97/33.48 % (3509422)Instruction limit reached! % 234.97/33.48 % (3509422)------------------------------ % 234.97/33.48 % (3509422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.97/33.48 % (3509422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.97/33.48 % (3509422)CaDiCaL version: 2.1.3 % 234.97/33.48 % (3509422)Termination reason: Instruction limit % 234.97/33.48 % (3509422)Termination phase: Saturation % 234.97/33.48 % (3509422)Time elapsed: 0.145 s % 234.97/33.48 % (3509422)Peak memory usage: 12 MB % 234.97/33.48 % (3509422)Instructions burned: 319 (million) % 234.97/33.48 % (3509424)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2181112612:i=1428:nm=2:rtra=on_2781 on theBenchmark for (2781ds/1428Mi) % 234.97/33.48 % Exception at run slice level % 234.97/33.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 234.97/33.48 % (3509426)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=607781387:i=262:bd=preordered:rtra=on:fsd=on_2780 on theBenchmark for (2780ds/262Mi) % 234.97/33.48 % (3509426)Instruction limit reached! % 234.97/33.48 % (3509426)------------------------------ % 234.97/33.48 % (3509426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.97/33.48 % (3509426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.97/33.48 % (3509426)CaDiCaL version: 2.1.3 % 234.97/33.48 % (3509426)Termination reason: Instruction limit % 234.97/33.48 % (3509426)Termination phase: Saturation % 234.97/33.48 % (3509426)Time elapsed: 0.167 s % 234.97/33.48 % (3509426)Peak memory usage: 14 MB % 234.97/33.48 % (3509426)Instructions burned: 263 (million) % 234.97/33.48 % (3509428)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=1386807047:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/1368Mi) % 234.97/33.48 % (3509428)Instruction limit reached! % 234.97/33.48 % (3509428)------------------------------ % 234.97/33.48 % (3509428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.97/33.48 % (3509428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.97/33.48 % (3509428)CaDiCaL version: 2.1.3 % 234.97/33.48 % (3509428)Termination reason: Instruction limit % 234.97/33.48 % (3509428)Termination phase: Saturation % 234.97/33.48 % (3509428)Time elapsed: 0.798 s % 234.97/33.48 % (3509428)Peak memory usage: 19 MB % 234.97/33.48 % (3509428)Instructions burned: 1368 (million) % 234.97/33.48 % (3509430)ott-21_1_sil=16000:si=on:fs=off:random_seed=4036425463:i=360:av=off:fsr=off:rtra=on_2770 on theBenchmark for (2770ds/360Mi) % 234.97/33.48 % (3509430)Instruction limit reached! % 234.97/33.48 % (3509430)------------------------------ % 234.97/33.48 % (3509430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.97/33.48 % (3509430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.97/33.48 % (3509430)CaDiCaL version: 2.1.3 % 234.97/33.48 % (3509430)Termination reason: Instruction limit % 234.97/33.48 % (3509430)Termination phase: Saturation % 234.97/33.48 % (3509430)Time elapsed: 0.159 s % 234.97/33.48 % (3509430)Peak memory usage: 13 MB % 234.97/33.48 % (3509430)Instructions burned: 363 (million) % 234.97/33.48 % (3509432)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3158929966:i=954:bd=all:rtra=on_2768 on theBenchmark for (2768ds/954Mi) % 234.97/33.48 % (3509432)Instruction limit reached! % 234.97/33.48 % (3509432)------------------------------ % 234.97/33.48 % (3509432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.97/33.48 % (3509432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.97/33.48 % (3509432)CaDiCaL version: 2.1.3 % 234.97/33.48 % (3509432)Termination reason: Instruction limit % 234.97/33.48 % (3509432)Termination phase: Saturation % 234.97/33.48 % (3509432)Time elapsed: 0.587 s % 234.97/33.48 % (3509432)Peak memory usage: 15 MB % 234.97/33.48 % (3509432)Instructions burned: 955 (million) % 234.97/33.48 % (3509434)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2622370515:fmbsr=1.3:i=1730:ins=25:rtra=on_2762 on theBenchmark for (2762ds/1730Mi) % 234.97/33.48 % Exception at run slice level % 234.97/33.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.45/37.52 % (3509436)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=600355994:i=2358:rtra=on_2762 on theBenchmark for (2762ds/2358Mi) % 264.45/37.52 % (3509436)Instruction limit reached! % 264.45/37.52 % (3509436)------------------------------ % 264.45/37.52 % (3509436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.45/37.52 % (3509436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.45/37.52 % (3509436)CaDiCaL version: 2.1.3 % 264.45/37.52 % (3509436)Termination reason: Instruction limit % 264.45/37.52 % (3509436)Termination phase: Saturation % 264.45/37.52 % (3509436)Time elapsed: 1.431 s % 264.45/37.52 % (3509436)Peak memory usage: 27 MB % 264.45/37.52 % (3509436)Instructions burned: 2358 (million) % 264.45/37.52 % (3509438)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2372090321:i=1778:ins=1:rtra=on_2747 on theBenchmark for (2747ds/1778Mi) % 264.45/37.52 % Exception at run slice level % 264.45/37.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.45/37.52 % (3509440)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=2860550801:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2747 on theBenchmark for (2747ds/1384Mi) % 264.45/37.52 % (3509440)Instruction limit reached! % 264.45/37.52 % (3509440)------------------------------ % 264.45/37.52 % (3509440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.45/37.52 % (3509440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.45/37.52 % (3509440)CaDiCaL version: 2.1.3 % 264.45/37.52 % (3509440)Termination reason: Instruction limit % 264.45/37.52 % (3509440)Termination phase: Saturation % 264.45/37.52 % (3509440)Time elapsed: 0.865 s % 264.45/37.52 % (3509440)Peak memory usage: 24 MB % 264.45/37.52 % (3509440)Instructions burned: 1385 (million) % 264.45/37.52 % (3509442)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=833128434:i=1758:kws=inv_precedence:fsr=off:rtra=on_2738 on theBenchmark for (2738ds/1758Mi) % 264.45/37.52 % (3509442)Instruction limit reached! % 264.45/37.52 % (3509442)------------------------------ % 264.45/37.52 % (3509442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.45/37.52 % (3509442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.45/37.52 % (3509442)CaDiCaL version: 2.1.3 % 264.45/37.52 % (3509442)Termination reason: Instruction limit % 264.45/37.52 % (3509442)Termination phase: Saturation % 264.45/37.52 % (3509442)Time elapsed: 0.983 s % 264.45/37.52 % (3509442)Peak memory usage: 22 MB % 264.45/37.52 % (3509442)Instructions burned: 1759 (million) % 264.45/37.52 % (3509444)fmb+10_1_sil=64000:si=on:random_seed=3459068357:i=44122:nm=2:rtra=on:gsp=on_2728 on theBenchmark for (2728ds/44122Mi) % 264.45/37.52 % (3509444)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 264.45/37.52 % Exception at run slice level % 264.45/37.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.45/37.52 % (3509446)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3349348186:i=19030:nm=5:rtra=on_2728 on theBenchmark for (2728ds/19030Mi) % 264.45/37.52 % Exception at run slice level % 264.45/37.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.45/37.52 % (3509448)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2541766146:fmbsr=1.7:i=1840:rtra=on_2728 on theBenchmark for (2728ds/1840Mi) % 264.45/37.52 % Exception at run slice level % 264.45/37.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.45/37.52 % (3509450)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1991023997:i=10262:rtra=on_2728 on theBenchmark for (2728ds/10262Mi) % 264.45/37.52 % (3509385)Instruction limit reached! % 264.45/37.52 % (3509385)------------------------------ % 264.45/37.52 % (3509385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.45/37.52 % (3509385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.45/37.52 % (3509385)CaDiCaL version: 2.1.3 % 264.45/37.52 % (3509385)Termination reason: Instruction limit % 264.45/37.52 % (3509385)Termination phase: Saturation % 264.45/37.52 % (3509385)Time elapsed: 14.136 s % 264.45/37.52 % (3509385)Peak memory usage: 221 MB % 264.45/37.52 % (3509385)Instructions burned: 53297 (million) % 300.63/42.63 % (3509454)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2642516836:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2716 on theBenchmark for (2716ds/2944Mi) % 300.63/42.63 % (3509454)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.63/42.63 % (3509454)Instruction limit reached! % 300.63/42.63 % (3509454)------------------------------ % 300.63/42.63 % (3509454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3509454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3509454)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3509454)Termination reason: Instruction limit % 300.63/42.63 % (3509454)Termination phase: Saturation % 300.63/42.63 % (3509454)Time elapsed: 0.916 s % 300.63/42.63 % (3509454)Peak memory usage: 48 MB % 300.63/42.63 % (3509454)Instructions burned: 2946 (million) % 300.63/42.63 % (3509456)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=290754085:i=12648:rtra=on_2706 on theBenchmark for (2706ds/12648Mi) % 300.63/42.63 % Exception at run slice level % 300.63/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.63 % (3509458)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2959221148:fmbsr=2.30978:i=4348:rtra=on_2706 on theBenchmark for (2706ds/4348Mi) % 300.63/42.63 % Exception at run slice level % 300.63/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.63 % (3509460)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=315171160:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2706 on theBenchmark for (2706ds/1738Mi) % 300.63/42.63 % (3509460)Instruction limit reached! % 300.63/42.63 % (3509460)------------------------------ % 300.63/42.63 % (3509460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3509460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3509460)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3509460)Termination reason: Instruction limit % 300.63/42.63 % (3509460)Termination phase: Saturation % 300.63/42.63 % (3509460)Time elapsed: 0.555 s % 300.63/42.63 % (3509460)Peak memory usage: 19 MB % 300.63/42.63 % (3509460)Instructions burned: 1740 (million) % 300.63/42.63 % (3509462)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=870206747:i=10228:av=off:rtra=on_2700 on theBenchmark for (2700ds/10228Mi) % 300.63/42.63 % (3509398)Instruction limit reached! % 300.63/42.63 % (3509398)------------------------------ % 300.63/42.63 % (3509398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3509398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3509398)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3509398)Termination reason: Instruction limit % 300.63/42.63 % (3509398)Termination phase: Saturation % 300.63/42.63 % (3509398)Time elapsed: 14.123 s % 300.63/42.63 % (3509398)Peak memory usage: 123 MB % 300.63/42.63 % (3509398)Instructions burned: 28121 (million) % 300.63/42.63 % (3509464)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1893632281:i=108564:rtra=on_2698 on theBenchmark for (2698ds/108564Mi) % 300.63/42.63 % Exception at run slice level % 300.63/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.63 % (3509466)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=163613025:i=7024:aac=none:rtra=on_2698 on theBenchmark for (2698ds/7024Mi) % 300.63/42.63 % (3509450)Instruction limit reached! % 300.63/42.63 % (3509450)------------------------------ % 300.63/42.63 % (3509450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3509450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.63 % (3509450)CaDiCaL version: 2.1.3 % 300.63/42.63 % (3509450)Termination reason: Instruction limit % 300.63/42.63 % (3509450)Termination phase: Saturation % 300.63/42.63 % (3509450)Time elapsed: 5.560 s % 300.63/42.63 % (3509450)Peak memory usage: 38 MB % 300.63/42.63 % (3509450)Instructions burned: 10263 (million) % 300.63/42.63 % (3509468)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2378812436:i=7546:rtra=on:amm=off_2672 on theBenchmark for (2672ds/7546Mi) % 300.63/42.63 % (3509462)Instruction limit reached! % 300.63/42.63 % (3509462)------------------------------ % 300.63/42.63 % (3509462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.63 % (3509462)Linked with Z3 4.14.0. % 300.63/42.63 Terminated % 300.63/42.63 % Vampire exiting %------------------------------------------------------------------------------