%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM097_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 : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 09:40:18 AM UTC 2026 % Result : Timeout 287.56s 40.88s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : COM097_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.24 % Computer : n010.cluster.edu % 0.11/0.24 % Model : x86_64 x86_64 % 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.24 % Memory : 8046.5625MB % 0.11/0.24 % OS : Linux 6.8.0-71-generic % 0.11/0.24 % CPULimit : 300 % 0.11/0.25 % WCLimit : 300 % 0.11/0.25 % DateTime : Mon Sep 28 21:54:02 UTC 2026 % 0.11/0.25 % CPUTime : % 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.28 Running first-order model finding % 0.11/0.28 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 % 12.65/2.14 % (2398427)Will run a generic schedule for satisfiability detection. % 12.65/2.14 % (2398433)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3591059913_2999 on theBenchmark for (2999ds/0Mi) % 12.65/2.14 % (2398434)% WARNING: option uhcvi not known. % 12.65/2.14 % (2398436)dis+10_1_sil=32000:sp=arity:random_seed=820093114:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 12.65/2.14 % (2398434)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1141088176:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 12.65/2.14 % (2398435)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2522494308:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 12.65/2.14 % (2398437)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2694331732:i=116_2999 on theBenchmark for (2999ds/116Mi) % 12.65/2.14 % Exception at run slice level % 12.65/2.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 12.65/2.14 % (2398438)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2885621323:i=131_2999 on theBenchmark for (2999ds/131Mi) % 12.65/2.14 % (2398439)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=414774311:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 12.65/2.14 % (2398446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4067922615:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 12.65/2.14 % Exception at run slice level % 12.65/2.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 12.65/2.14 % (2398449)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1817110155:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 12.65/2.14 % (2398436)Instruction limit reached! % 12.65/2.14 % (2398436)------------------------------ % 12.65/2.14 % (2398436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.65/2.14 % (2398436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.14 % (2398436)CaDiCaL version: 2.1.3 % 12.65/2.14 % (2398436)Termination reason: Instruction limit % 12.65/2.14 % (2398436)Termination phase: Saturation % 12.65/2.14 % (2398436)Time elapsed: 0.065 s % 12.65/2.14 % (2398436)Peak memory usage: 12 MB % 12.65/2.14 % (2398436)Instructions burned: 104 (million) % 12.65/2.14 % (2398451)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=4286518031:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 12.65/2.14 % (2398437)Instruction limit reached! % 12.65/2.14 % (2398437)------------------------------ % 12.65/2.14 % (2398437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.65/2.14 % (2398437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.14 % (2398437)CaDiCaL version: 2.1.3 % 12.65/2.14 % (2398437)Termination reason: Instruction limit % 12.65/2.14 % (2398437)Termination phase: Saturation % 12.65/2.14 % (2398437)Time elapsed: 0.109 s % 12.65/2.14 % (2398437)Peak memory usage: 12 MB % 12.65/2.14 % (2398437)Instructions burned: 117 (million) % 12.65/2.14 % (2398453)ott-21_1_sil=16000:fs=off:random_seed=1885090103:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 12.65/2.14 % (2398438)Instruction limit reached! % 12.65/2.14 % (2398438)------------------------------ % 12.65/2.14 % (2398438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.65/2.14 % (2398438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.14 % (2398438)CaDiCaL version: 2.1.3 % 12.65/2.14 % (2398438)Termination reason: Instruction limit % 12.65/2.14 % (2398438)Termination phase: Saturation % 12.65/2.14 % (2398438)Time elapsed: 0.135 s % 12.65/2.14 % (2398438)Peak memory usage: 13 MB % 12.65/2.14 % (2398438)Instructions burned: 131 (million) % 12.65/2.14 % (2398449)Instruction limit reached! % 12.65/2.14 % (2398449)------------------------------ % 12.65/2.14 % (2398449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.65/2.14 % (2398449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.14 % (2398449)CaDiCaL version: 2.1.3 % 12.65/2.14 % (2398449)Termination reason: Instruction limit % 12.65/2.14 % (2398449)Termination phase: Saturation % 12.65/2.14 % (2398449)Time elapsed: 0.115 s % 12.65/2.14 % (2398449)Peak memory usage: 13 MB % 12.65/2.14 % (2398449)Instructions burned: 131 (million) % 12.65/2.14 % (2398455)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3362392878:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 34.74/5.21 % (2398439)Instruction limit reached! % 34.74/5.21 % (2398439)------------------------------ % 34.74/5.21 % (2398439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.74/5.21 % (2398439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.21 % (2398439)CaDiCaL version: 2.1.3 % 34.74/5.21 % (2398439)Termination reason: Instruction limit % 34.74/5.21 % (2398439)Termination phase: Saturation % 34.74/5.21 % (2398439)Time elapsed: 0.169 s % 34.74/5.21 % (2398439)Peak memory usage: 13 MB % 34.74/5.21 % (2398439)Instructions burned: 159 (million) % 34.74/5.21 % (2398457)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2440215566:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 34.74/5.21 % (2398459)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4173010763:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 34.74/5.21 % Exception at run slice level % 34.74/5.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.74/5.21 % (2398453)Instruction limit reached! % 34.74/5.21 % (2398453)------------------------------ % 34.74/5.21 % (2398453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.74/5.21 % (2398453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.21 % (2398453)CaDiCaL version: 2.1.3 % 34.74/5.21 % (2398453)Termination reason: Instruction limit % 34.74/5.21 % (2398453)Termination phase: Saturation % 34.74/5.21 % (2398453)Time elapsed: 0.103 s % 34.74/5.21 % (2398453)Peak memory usage: 13 MB % 34.74/5.21 % (2398453)Instructions burned: 181 (million) % 34.74/5.21 % (2398462)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1421424952:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 34.74/5.21 % Exception at run slice level % 34.74/5.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.74/5.21 % (2398465)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2083451859:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 34.74/5.21 % (2398463)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=3043041026:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 34.74/5.21 % (2398451)Instruction limit reached! % 34.74/5.21 % (2398451)------------------------------ % 34.74/5.21 % (2398451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.74/5.21 % (2398451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.21 % (2398451)CaDiCaL version: 2.1.3 % 34.74/5.21 % (2398451)Termination reason: Instruction limit % 34.74/5.21 % (2398451)Termination phase: Saturation % 34.74/5.21 % (2398451)Time elapsed: 0.295 s % 34.74/5.21 % (2398451)Peak memory usage: 15 MB % 34.74/5.21 % (2398451)Instructions burned: 686 (million) % 34.74/5.21 % (2398468)fmb+10_1_sil=64000:random_seed=1489482739:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 34.74/5.21 % (2398468)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 34.74/5.21 % Exception at run slice level % 34.74/5.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.74/5.21 % (2398470)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2945470959:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 34.74/5.21 % Exception at run slice level % 34.74/5.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.74/5.21 % (2398473)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3142402164:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 34.74/5.21 % Exception at run slice level % 34.74/5.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.74/5.21 % (2398475)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1579847793:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 34.74/5.21 % (2398455)Instruction limit reached! % 34.74/5.21 % (2398455)------------------------------ % 34.74/5.21 % (2398455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.74/5.21 % (2398455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.65/14.66 % (2398455)CaDiCaL version: 2.1.3 % 101.65/14.66 % (2398455)Termination reason: Instruction limit % 101.65/14.66 % (2398455)Termination phase: Saturation % 101.65/14.66 % (2398455)Time elapsed: 0.406 s % 101.65/14.66 % (2398455)Peak memory usage: 13 MB % 101.65/14.66 % (2398455)Instructions burned: 477 (million) % 101.65/14.66 % (2398478)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=445329071:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 101.65/14.66 % (2398478)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 101.65/14.66 % (2398463)Instruction limit reached! % 101.65/14.66 % (2398463)------------------------------ % 101.65/14.66 % (2398463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.65/14.66 % (2398463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.65/14.66 % (2398463)CaDiCaL version: 2.1.3 % 101.65/14.66 % (2398463)Termination reason: Instruction limit % 101.65/14.66 % (2398463)Termination phase: Saturation % 101.65/14.66 % (2398463)Time elapsed: 0.529 s % 101.65/14.66 % (2398463)Peak memory usage: 16 MB % 101.65/14.66 % (2398463)Instructions burned: 692 (million) % 101.65/14.66 % (2398482)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2216900358:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 101.65/14.66 % Exception at run slice level % 101.65/14.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.65/14.66 % (2398484)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1714380623:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 101.65/14.66 % Exception at run slice level % 101.65/14.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.65/14.66 % (2398487)ott-2_1_sil=16000:newcnf=on:random_seed=3262050924:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 101.65/14.66 % (2398465)Instruction limit reached! % 101.65/14.66 % (2398465)------------------------------ % 101.65/14.66 % (2398465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.65/14.66 % (2398465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.65/14.66 % (2398465)CaDiCaL version: 2.1.3 % 101.65/14.66 % (2398465)Termination reason: Instruction limit % 101.65/14.66 % (2398465)Termination phase: Saturation % 101.65/14.66 % (2398465)Time elapsed: 0.816 s % 101.65/14.66 % (2398465)Peak memory usage: 18 MB % 101.65/14.66 % (2398465)Instructions burned: 879 (million) % 101.65/14.66 % (2398489)ott+10_1_sil=32000:tgt=ground:random_seed=322609752:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 101.65/14.66 % (2398459)Instruction limit reached! % 101.65/14.66 % (2398459)------------------------------ % 101.65/14.66 % (2398459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.65/14.66 % (2398459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.65/14.66 % (2398459)CaDiCaL version: 2.1.3 % 101.65/14.66 % (2398459)Termination reason: Instruction limit % 101.65/14.66 % (2398459)Termination phase: Saturation % 101.65/14.66 % (2398459)Time elapsed: 0.995 s % 101.65/14.66 % (2398459)Peak memory usage: 15 MB % 101.65/14.66 % (2398459)Instructions burned: 1179 (million) % 101.65/14.66 % (2398491)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3787779807:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 101.65/14.66 % Exception at run slice level % 101.65/14.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.65/14.66 % (2398493)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3828616506:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 101.65/14.66 % (2398487)Instruction limit reached! % 101.65/14.66 % (2398487)------------------------------ % 101.65/14.66 % (2398487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.65/14.66 % (2398487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.65/14.66 % (2398487)CaDiCaL version: 2.1.3 % 101.65/14.66 % (2398487)Termination reason: Instruction limit % 101.65/14.66 % (2398487)Termination phase: Saturation % 101.65/14.66 % (2398487)Time elapsed: 0.681 s % 101.65/14.66 % (2398487)Peak memory usage: 13 MB % 101.65/14.66 % (2398487)Instructions burned: 870 (million) % 101.65/14.66 % (2398496)dis+21_1_sil=32000:sas=cadical:random_seed=3637304083:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 101.65/14.66 % (2398478)Instruction limit reached! % 101.65/14.66 % (2398478)------------------------------ % 101.65/14.66 % (2398478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398478)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398478)Termination reason: Instruction limit % 148.49/21.22 % (2398478)Termination phase: Saturation % 148.49/21.22 % (2398478)Time elapsed: 1.201 s % 148.49/21.22 % (2398478)Peak memory usage: 17 MB % 148.49/21.22 % (2398478)Instructions burned: 1473 (million) % 148.49/21.22 % (2398500)ott+11_1_sil=16000:gs=on:random_seed=3844479560:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 148.49/21.22 % (2398475)Instruction limit reached! % 148.49/21.22 % (2398475)------------------------------ % 148.49/21.22 % (2398475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398475)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398475)Termination reason: Instruction limit % 148.49/21.22 % (2398475)Termination phase: Saturation % 148.49/21.22 % (2398475)Time elapsed: 2.351 s % 148.49/21.22 % (2398475)Peak memory usage: 34 MB % 148.49/21.22 % (2398475)Instructions burned: 5133 (million) % 148.49/21.22 % (2398509)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2196483306:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 148.49/21.22 % Exception at run slice level % 148.49/21.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.49/21.22 % (2398511)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2567660780:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2970 on theBenchmark for (2970ds/4591Mi) % 148.49/21.22 % (2398500)Instruction limit reached! % 148.49/21.22 % (2398500)------------------------------ % 148.49/21.22 % (2398500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398500)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398500)Termination reason: Instruction limit % 148.49/21.22 % (2398500)Termination phase: Saturation % 148.49/21.22 % (2398500)Time elapsed: 1.744 s % 148.49/21.22 % (2398500)Peak memory usage: 18 MB % 148.49/21.22 % (2398500)Instructions burned: 2252 (million) % 148.49/21.22 % (2398516)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2642951187:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 148.49/21.22 % (2398493)Instruction limit reached! % 148.49/21.22 % (2398493)------------------------------ % 148.49/21.22 % (2398493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398493)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398493)Termination reason: Instruction limit % 148.49/21.22 % (2398493)Termination phase: Saturation % 148.49/21.22 % (2398493)Time elapsed: 3.250 s % 148.49/21.22 % (2398493)Peak memory usage: 33 MB % 148.49/21.22 % (2398493)Instructions burned: 3512 (million) % 148.49/21.22 % (2398523)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=43795099:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 148.49/21.22 % (2398496)Instruction limit reached! % 148.49/21.22 % (2398496)------------------------------ % 148.49/21.22 % (2398496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398496)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398496)Termination reason: Instruction limit % 148.49/21.22 % (2398496)Termination phase: Saturation % 148.49/21.22 % (2398496)Time elapsed: 3.200 s % 148.49/21.22 % (2398496)Peak memory usage: 35 MB % 148.49/21.22 % (2398496)Instructions burned: 3774 (million) % 148.49/21.22 % (2398511)Instruction limit reached! % 148.49/21.22 % (2398511)------------------------------ % 148.49/21.22 % (2398511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.49/21.22 % (2398511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.49/21.22 % (2398511)CaDiCaL version: 2.1.3 % 148.49/21.22 % (2398511)Termination reason: Instruction limit % 148.49/21.22 % (2398511)Termination phase: Saturation % 148.49/21.22 % (2398511)Time elapsed: 1.948 s % 148.49/21.22 % (2398511)Peak memory usage: 30 MB % 148.49/21.22 % (2398511)Instructions burned: 4592 (million) % 148.49/21.22 % (2398525)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=339989400:i=5497:nm=2_2951 on theBenchmark for (2951ds/5497Mi) % 148.49/21.22 % Exception at run slice level % 148.49/21.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.35/23.33 % (2398526)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3349734918:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi) % 163.35/23.33 % Exception at run slice level % 163.35/23.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.35/23.33 % (2398529)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1374200321:i=14071_2950 on theBenchmark for (2950ds/14071Mi) % 163.35/23.33 % Exception at run slice level % 163.35/23.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.35/23.33 % (2398531)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2607025806:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi) % 163.35/23.33 % (2398533)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2835227636:i=8173:av=off_2950 on theBenchmark for (2950ds/8173Mi) % 163.35/23.33 % (2398489)Instruction limit reached! % 163.35/23.33 % (2398489)------------------------------ % 163.35/23.34 % (2398489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.35/23.34 % (2398489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.34 % (2398489)CaDiCaL version: 2.1.3 % 163.35/23.34 % (2398489)Termination reason: Instruction limit % 163.35/23.34 % (2398489)Termination phase: Saturation % 163.35/23.34 % (2398489)Time elapsed: 4.531 s % 163.35/23.34 % (2398489)Peak memory usage: 25 MB % 163.35/23.34 % (2398489)Instructions burned: 5114 (million) % 163.35/23.34 % (2398542)dis+10_16:1_sil=16000:random_seed=3277102741:i=9155:fsr=off_2942 on theBenchmark for (2942ds/9155Mi) % 163.35/23.34 % (2398523)Instruction limit reached! % 163.35/23.34 % (2398523)------------------------------ % 163.35/23.34 % (2398523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.35/23.34 % (2398523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.34 % (2398523)CaDiCaL version: 2.1.3 % 163.35/23.34 % (2398523)Termination reason: Instruction limit % 163.35/23.34 % (2398523)Termination phase: Saturation % 163.35/23.34 % (2398523)Time elapsed: 4.802 s % 163.35/23.34 % (2398523)Peak memory usage: 48 MB % 163.35/23.34 % (2398523)Instructions burned: 5212 (million) % 163.35/23.34 % (2398559)ott-3_8_sil=64000:random_seed=1613933028:i=20139:bs=on_2906 on theBenchmark for (2906ds/20139Mi) % 163.35/23.34 % (2398533)Instruction limit reached! % 163.35/23.34 % (2398533)------------------------------ % 163.35/23.34 % (2398533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.35/23.34 % (2398533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.34 % (2398533)CaDiCaL version: 2.1.3 % 163.35/23.34 % (2398533)Termination reason: Instruction limit % 163.35/23.34 % (2398533)Termination phase: Saturation % 163.35/23.34 % (2398533)Time elapsed: 7.239 s % 163.35/23.34 % (2398533)Peak memory usage: 35 MB % 163.35/23.34 % (2398533)Instructions burned: 8173 (million) % 163.35/23.34 % (2398573)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3037631647:fmbsr=2:i=32576_2877 on theBenchmark for (2877ds/32576Mi) % 163.35/23.34 % Exception at run slice level % 163.35/23.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.35/23.34 % (2398575)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3614953601:i=11404_2877 on theBenchmark for (2877ds/11404Mi) % 163.35/23.34 % (2398542)Instruction limit reached! % 163.35/23.34 % (2398542)------------------------------ % 163.35/23.34 % (2398542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.35/23.34 % (2398542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.34 % (2398542)CaDiCaL version: 2.1.3 % 163.35/23.34 % (2398542)Termination reason: Instruction limit % 163.35/23.34 % (2398542)Termination phase: Saturation % 163.35/23.34 % (2398542)Time elapsed: 7.773 s % 163.35/23.34 % (2398542)Peak memory usage: 56 MB % 163.35/23.34 % (2398542)Instructions burned: 9156 (million) % 163.35/23.34 % (2398691)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=948344453:i=14134_2864 on theBenchmark for (2864ds/14134Mi) % 163.35/23.34 % (2398531)Instruction limit reached! % 163.35/23.34 % (2398531)------------------------------ % 163.35/23.34 % (2398531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.35/23.34 % (2398531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.34 % (2398531)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398531)Termination reason: Instruction limit % 170.24/24.37 % (2398531)Termination phase: Saturation % 170.24/24.37 % (2398531)Time elapsed: 9.415 s % 170.24/24.37 % (2398531)Peak memory usage: 78 MB % 170.24/24.37 % (2398531)Instructions burned: 22567 (million) % 170.24/24.37 % (2398735)dis+33_16_sil=32000:sac=on:random_seed=3805681288:i=15851:nm=0_2856 on theBenchmark for (2856ds/15851Mi) % 170.24/24.37 % (2398735)Instruction limit reached! % 170.24/24.37 % (2398735)------------------------------ % 170.24/24.37 % (2398735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.24/24.37 % (2398735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.24/24.37 % (2398735)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398735)Termination reason: Instruction limit % 170.24/24.37 % (2398735)Termination phase: Saturation % 170.24/24.37 % (2398735)Time elapsed: 3.763 s % 170.24/24.37 % (2398735)Peak memory usage: 31 MB % 170.24/24.37 % (2398735)Instructions burned: 15853 (million) % 170.24/24.37 % (2398738)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3264041901:avsq=on:i=17627:add=on:amm=off_2818 on theBenchmark for (2818ds/17627Mi) % 170.24/24.37 % (2398575)Instruction limit reached! % 170.24/24.37 % (2398575)------------------------------ % 170.24/24.37 % (2398575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.24/24.37 % (2398575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.24/24.37 % (2398575)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398575)Termination reason: Instruction limit % 170.24/24.37 % (2398575)Termination phase: Saturation % 170.24/24.37 % (2398575)Time elapsed: 7.259 s % 170.24/24.37 % (2398575)Peak memory usage: 119 MB % 170.24/24.37 % (2398575)Instructions burned: 11405 (million) % 170.24/24.37 % (2398741)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=192248794:s2a=on:i=53295_2804 on theBenchmark for (2804ds/53295Mi) % 170.24/24.37 % (2398559)Instruction limit reached! % 170.24/24.37 % (2398559)------------------------------ % 170.24/24.37 % (2398559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.24/24.37 % (2398559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.24/24.37 % (2398559)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398559)Termination reason: Instruction limit % 170.24/24.37 % (2398559)Termination phase: Saturation % 170.24/24.37 % (2398559)Time elapsed: 11.123 s % 170.24/24.37 % (2398559)Peak memory usage: 31 MB % 170.24/24.37 % (2398559)Instructions burned: 20141 (million) % 170.24/24.37 % (2398743)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1222890361:i=26857:ins=20_2794 on theBenchmark for (2794ds/26857Mi) % 170.24/24.37 % Exception at run slice level % 170.24/24.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.24/24.37 % (2398745)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2213165501:i=28120:bs=on:fsr=off_2794 on theBenchmark for (2794ds/28120Mi) % 170.24/24.37 % (2398516)Instruction limit reached! % 170.24/24.37 % (2398516)------------------------------ % 170.24/24.37 % (2398516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.24/24.37 % (2398516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.24/24.37 % (2398516)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398516)Termination reason: Instruction limit % 170.24/24.37 % (2398516)Termination phase: Saturation % 170.24/24.37 % (2398516)Time elapsed: 17.218 s % 170.24/24.37 % (2398516)Peak memory usage: 107 MB % 170.24/24.37 % (2398516)Instructions burned: 29341 (million) % 170.24/24.37 % (2398691)Instruction limit reached! % 170.24/24.37 % (2398691)------------------------------ % 170.24/24.37 % (2398691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.24/24.37 % (2398691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.24/24.37 % (2398691)CaDiCaL version: 2.1.3 % 170.24/24.37 % (2398691)Termination reason: Instruction limit % 170.24/24.37 % (2398691)Termination phase: Saturation % 170.24/24.37 % (2398691)Time elapsed: 7.357 s % 170.24/24.37 % (2398691)Peak memory usage: 51 MB % 170.24/24.37 % (2398691)Instructions burned: 14134 (million) % 170.24/24.37 % (2398747)fmb+10_1_sil=256000:fmbss=7:random_seed=768208102:fmbsr=1.6:i=182295_2791 on theBenchmark for (2791ds/182295Mi) % 170.24/24.37 % Exception at run slice level % 170.24/24.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.24/24.37 % (2398749)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2186136107:i=44625:gsp=on_2790 on theBenchmark for (2790ds/44625Mi) % 170.24/24.37 % (2398750)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1625040968:i=160505_2790 on theBenchmark for (2790ds/160505Mi) % 205.95/29.38 % (2398749)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 205.95/29.38 % Exception at run slice level % 205.95/29.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.95/29.38 % Exception at run slice level % 205.95/29.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.95/29.38 % (2398753)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1304876369:fmbsr=1.3:i=225729_2790 on theBenchmark for (2790ds/225729Mi) % 205.95/29.38 % (2398754)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1309607439:fmbsr=2:i=185024:ins=7_2790 on theBenchmark for (2790ds/185024Mi) % 205.95/29.38 % Exception at run slice level % 205.95/29.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.95/29.38 % Exception at run slice level % 205.95/29.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.95/29.38 % (2398757)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1342978773:rtra=on_2790 on theBenchmark for (2790ds/0Mi) % 205.95/29.38 % (2398758)% WARNING: option uhcvi not known. % 205.95/29.38 % (2398758)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1851641019:i=271062:add=off:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/271062Mi) % 205.95/29.38 % Exception at run slice level % 205.95/29.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.95/29.38 % (2398761)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=736536954:i=176048:add=on:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/176048Mi) % 205.95/29.38 % (2398738)Instruction limit reached! % 205.95/29.38 % (2398738)------------------------------ % 205.95/29.38 % (2398738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.95/29.38 % (2398738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.95/29.38 % (2398738)CaDiCaL version: 2.1.3 % 205.95/29.38 % (2398738)Termination reason: Instruction limit % 205.95/29.38 % (2398738)Termination phase: Saturation % 205.95/29.38 % (2398738)Time elapsed: 4.619 s % 205.95/29.38 % (2398738)Peak memory usage: 36 MB % 205.95/29.38 % (2398738)Instructions burned: 17628 (million) % 205.95/29.38 % (2398763)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2973125315:i=206:fgj=on:rtra=on_2772 on theBenchmark for (2772ds/206Mi) % 205.95/29.38 % (2398763)Instruction limit reached! % 205.95/29.38 % (2398763)------------------------------ % 205.95/29.38 % (2398763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.95/29.38 % (2398763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.95/29.38 % (2398763)CaDiCaL version: 2.1.3 % 205.95/29.38 % (2398763)Termination reason: Instruction limit % 205.95/29.38 % (2398763)Termination phase: Saturation % 205.95/29.38 % (2398763)Time elapsed: 0.058 s % 205.95/29.38 % (2398763)Peak memory usage: 12 MB % 205.95/29.38 % (2398763)Instructions burned: 207 (million) % 205.95/29.38 % (2398765)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=724518645:i=232:rtra=on_2771 on theBenchmark for (2771ds/232Mi) % 205.95/29.38 % (2398765)Instruction limit reached! % 205.95/29.38 % (2398765)------------------------------ % 205.95/29.38 % (2398765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.95/29.38 % (2398765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.95/29.38 % (2398765)CaDiCaL version: 2.1.3 % 205.95/29.38 % (2398765)Termination reason: Instruction limit % 205.95/29.38 % (2398765)Termination phase: Saturation % 205.95/29.38 % (2398765)Time elapsed: 0.075 s % 205.95/29.38 % (2398765)Peak memory usage: 13 MB % 205.95/29.38 % (2398765)Instructions burned: 234 (million) % 205.95/29.38 % (2398767)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=510649359:i=262:rtra=on_2770 on theBenchmark for (2770ds/262Mi) % 205.95/29.38 % (2398767)Instruction limit reached! % 205.95/29.38 % (2398767)------------------------------ % 205.95/29.38 % (2398767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.95/29.38 % (2398767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.95/29.38 % (2398767)CaDiCaL version: 2.1.3 % 205.95/29.38 % (2398767)Termination reason: Instruction limit % 205.95/29.38 % (2398767)Termination phase: Saturation % 246.62/35.05 % (2398767)Time elapsed: 0.087 s % 246.62/35.05 % (2398767)Peak memory usage: 14 MB % 246.62/35.05 % (2398767)Instructions burned: 263 (million) % 246.62/35.05 % (2398769)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1912466377:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2769 on theBenchmark for (2769ds/318Mi) % 246.62/35.05 % (2398769)Instruction limit reached! % 246.62/35.05 % (2398769)------------------------------ % 246.62/35.05 % (2398769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.62/35.05 % (2398769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.62/35.05 % (2398769)CaDiCaL version: 2.1.3 % 246.62/35.05 % (2398769)Termination reason: Instruction limit % 246.62/35.05 % (2398769)Termination phase: Saturation % 246.62/35.05 % (2398769)Time elapsed: 0.114 s % 246.62/35.05 % (2398769)Peak memory usage: 15 MB % 246.62/35.05 % (2398769)Instructions burned: 321 (million) % 246.62/35.05 % (2398771)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2193971772:i=1428:nm=2:rtra=on_2768 on theBenchmark for (2768ds/1428Mi) % 246.62/35.05 % Exception at run slice level % 246.62/35.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.62/35.05 % (2398773)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=335254626:i=262:bd=preordered:rtra=on:fsd=on_2768 on theBenchmark for (2768ds/262Mi) % 246.62/35.05 % (2398773)Instruction limit reached! % 246.62/35.05 % (2398773)------------------------------ % 246.62/35.05 % (2398773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.62/35.05 % (2398773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.62/35.05 % (2398773)CaDiCaL version: 2.1.3 % 246.62/35.05 % (2398773)Termination reason: Instruction limit % 246.62/35.05 % (2398773)Termination phase: Saturation % 246.62/35.05 % (2398773)Time elapsed: 0.086 s % 246.62/35.05 % (2398773)Peak memory usage: 13 MB % 246.62/35.05 % (2398773)Instructions burned: 264 (million) % 246.62/35.05 % (2398775)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=2228225521:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/1368Mi) % 246.62/35.05 % (2398775)Instruction limit reached! % 246.62/35.05 % (2398775)------------------------------ % 246.62/35.05 % (2398775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.62/35.05 % (2398775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.62/35.05 % (2398775)CaDiCaL version: 2.1.3 % 246.62/35.05 % (2398775)Termination reason: Instruction limit % 246.62/35.05 % (2398775)Termination phase: Saturation % 246.62/35.05 % (2398775)Time elapsed: 0.361 s % 246.62/35.05 % (2398775)Peak memory usage: 17 MB % 246.62/35.05 % (2398775)Instructions burned: 1370 (million) % 246.62/35.05 % (2398777)ott-21_1_sil=16000:si=on:fs=off:random_seed=3060499077:i=360:av=off:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/360Mi) % 246.62/35.05 % (2398777)Instruction limit reached! % 246.62/35.05 % (2398777)------------------------------ % 246.62/35.05 % (2398777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.62/35.05 % (2398777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.62/35.05 % (2398777)CaDiCaL version: 2.1.3 % 246.62/35.05 % (2398777)Termination reason: Instruction limit % 246.62/35.05 % (2398777)Termination phase: Saturation % 246.62/35.05 % (2398777)Time elapsed: 0.092 s % 246.62/35.05 % (2398777)Peak memory usage: 13 MB % 246.62/35.05 % (2398777)Instructions burned: 363 (million) % 246.62/35.05 % (2398779)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3425399281:i=954:bd=all:rtra=on_2762 on theBenchmark for (2762ds/954Mi) % 246.62/35.05 % (2398779)Instruction limit reached! % 246.62/35.05 % (2398779)------------------------------ % 246.62/35.05 % (2398779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.62/35.05 % (2398779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.62/35.05 % (2398779)CaDiCaL version: 2.1.3 % 246.62/35.05 % (2398779)Termination reason: Instruction limit % 246.62/35.05 % (2398779)Termination phase: Saturation % 246.62/35.05 % (2398779)Time elapsed: 0.286 s % 246.62/35.05 % (2398779)Peak memory usage: 16 MB % 246.62/35.05 % (2398779)Instructions burned: 957 (million) % 246.62/35.05 % (2398781)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2802620841:fmbsr=1.3:i=1730:ins=25:rtra=on_2759 on theBenchmark for (2759ds/1730Mi) % 246.62/35.05 % Exception at run slice level % 246.62/35.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 287.56/40.88 % (2398783)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3795515335:i=2358:rtra=on_2759 on theBenchmark for (2759ds/2358Mi) % 287.56/40.88 % (2398783)Instruction limit reached! % 287.56/40.88 % (2398783)------------------------------ % 287.56/40.88 % (2398783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.56/40.88 % (2398783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.56/40.88 % (2398783)CaDiCaL version: 2.1.3 % 287.56/40.88 % (2398783)Termination reason: Instruction limit % 287.56/40.88 % (2398783)Termination phase: Saturation % 287.56/40.88 % (2398783)Time elapsed: 0.829 s % 287.56/40.88 % (2398783)Peak memory usage: 32 MB % 287.56/40.88 % (2398783)Instructions burned: 2360 (million) % 287.56/40.88 % (2398785)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1114595843:i=1778:ins=1:rtra=on_2750 on theBenchmark for (2750ds/1778Mi) % 287.56/40.88 % Exception at run slice level % 287.56/40.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 287.56/40.88 % (2398787)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=3706975633:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/1384Mi) % 287.56/40.88 % (2398787)Instruction limit reached! % 287.56/40.88 % (2398787)------------------------------ % 287.56/40.88 % (2398787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.56/40.88 % (2398787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.56/40.88 % (2398787)CaDiCaL version: 2.1.3 % 287.56/40.88 % (2398787)Termination reason: Instruction limit % 287.56/40.88 % (2398787)Termination phase: Saturation % 287.56/40.88 % (2398787)Time elapsed: 0.461 s % 287.56/40.88 % (2398787)Peak memory usage: 19 MB % 287.56/40.88 % (2398787)Instructions burned: 1385 (million) % 287.56/40.88 % (2398789)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=181310439:i=1758:kws=inv_precedence:fsr=off:rtra=on_2745 on theBenchmark for (2745ds/1758Mi) % 287.56/40.88 % (2398789)Instruction limit reached! % 287.56/40.88 % (2398789)------------------------------ % 287.56/40.88 % (2398789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.56/40.88 % (2398789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.56/40.88 % (2398789)CaDiCaL version: 2.1.3 % 287.56/40.88 % (2398789)Termination reason: Instruction limit % 287.56/40.88 % (2398789)Termination phase: Saturation % 287.56/40.88 % (2398789)Time elapsed: 0.540 s % 287.56/40.88 % (2398789)Peak memory usage: 23 MB % 287.56/40.88 % (2398789)Instructions burned: 1759 (million) % 287.56/40.88 % (2398791)fmb+10_1_sil=64000:si=on:random_seed=3692880577:i=44122:nm=2:rtra=on:gsp=on_2740 on theBenchmark for (2740ds/44122Mi) % 287.56/40.88 % (2398791)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 287.56/40.88 % Exception at run slice level % 287.56/40.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 287.56/40.88 % (2398793)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2233127047:i=19030:nm=5:rtra=on_2740 on theBenchmark for (2740ds/19030Mi) % 287.56/40.88 % Exception at run slice level % 287.56/40.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 287.56/40.88 % (2398795)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3634457399:fmbsr=1.7:i=1840:rtra=on_2739 on theBenchmark for (2739ds/1840Mi) % 287.56/40.88 % Exception at run slice level % 287.56/40.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 287.56/40.88 % (2398797)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2038273390:i=10262:rtra=on_2739 on theBenchmark for (2739ds/10262Mi) % 287.56/40.88 % (2398797)Instruction limit reached! % 287.56/40.88 % (2398797)------------------------------ % 287.56/40.88 % (2398797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.56/40.88 % (2398797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.56/40.88 % (2398797)CaDiCaL version: 2.1.3 % 287.56/40.88 % (2398797)Termination reason: Instruction limit % 287.56/40.88 % (2398797)Termination phase: Saturation % 287.56/40.88 % (2398797)Time elapsed: 3.048 s % 287.56/40.88 % (2398797)Peak memory usage: 52 MB % 300.33/42.64 Terminated % 300.33/42.64 % Vampire exiting %------------------------------------------------------------------------------