%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV597_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 : n015.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:06 PM UTC 2026 % Result : Timeout 300.09s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV597_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.08/0.18 % Computer : n015.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 12:03:02 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.44/1.39 % (2579824)Will run a generic schedule for satisfiability detection. % 7.44/1.39 % (2579833)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=820643245:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.44/1.39 % (2579830)% WARNING: option uhcvi not known. % 7.44/1.39 % (2579829)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=351240412_2999 on theBenchmark for (2999ds/0Mi) % 7.44/1.39 % (2579830)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4034348162:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.44/1.39 % (2579831)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=112535345:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.44/1.39 % (2579832)dis+10_1_sil=32000:sp=arity:random_seed=3370208771:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.44/1.39 % (2579835)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=336044177:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.44/1.39 % (2579834)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2879583372:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.44/1.39 % Exception at run slice level % 7.44/1.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.44/1.39 % (2579843)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2013067337:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.44/1.39 % Exception at run slice level % 7.44/1.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.44/1.39 % (2579833)Instruction limit reached! % 7.44/1.39 % (2579833)------------------------------ % 7.44/1.39 % (2579833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.39 % (2579833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.39 % (2579833)CaDiCaL version: 2.1.3 % 7.44/1.39 % (2579833)Termination reason: Instruction limit % 7.44/1.39 % (2579833)Termination phase: Saturation % 7.44/1.39 % (2579833)Time elapsed: 0.038 s % 7.44/1.39 % (2579833)Peak memory usage: 13 MB % 7.44/1.39 % (2579833)Instructions burned: 117 (million) % 7.44/1.39 % (2579846)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=1394486542:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.44/1.39 % (2579845)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=537510814:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.44/1.39 % (2579832)Instruction limit reached! % 7.44/1.39 % (2579832)------------------------------ % 7.44/1.39 % (2579832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.39 % (2579832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.39 % (2579832)CaDiCaL version: 2.1.3 % 7.44/1.39 % (2579832)Termination reason: Instruction limit % 7.44/1.39 % (2579832)Termination phase: Saturation % 7.44/1.39 % (2579832)Time elapsed: 0.063 s % 7.44/1.39 % (2579832)Peak memory usage: 12 MB % 7.44/1.39 % (2579832)Instructions burned: 105 (million) % 7.44/1.39 % (2579834)Instruction limit reached! % 7.44/1.39 % (2579834)------------------------------ % 7.44/1.39 % (2579834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.39 % (2579834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.39 % (2579834)CaDiCaL version: 2.1.3 % 7.44/1.39 % (2579834)Termination reason: Instruction limit % 7.44/1.39 % (2579834)Termination phase: Saturation % 7.44/1.39 % (2579834)Time elapsed: 0.080 s % 7.44/1.39 % (2579834)Peak memory usage: 13 MB % 7.44/1.39 % (2579834)Instructions burned: 134 (million) % 7.44/1.39 % (2579849)ott-21_1_sil=16000:fs=off:random_seed=492856530:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.44/1.39 % (2579835)Instruction limit reached! % 7.44/1.39 % (2579835)------------------------------ % 7.44/1.39 % (2579835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.39 % (2579835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.39 % (2579835)CaDiCaL version: 2.1.3 % 7.44/1.39 % (2579835)Termination reason: Instruction limit % 7.44/1.39 % (2579835)Termination phase: Saturation % 7.44/1.39 % (2579835)Time elapsed: 0.094 s % 7.44/1.39 % (2579835)Peak memory usage: 13 MB % 7.44/1.39 % (2579835)Instructions burned: 161 (million) % 7.44/1.39 % (2579850)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2762771991:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.22/3.46 % (2579852)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3241660374:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.22/3.46 % Exception at run slice level % 22.22/3.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.22/3.46 % (2579845)Instruction limit reached! % 22.22/3.46 % (2579845)------------------------------ % 22.22/3.46 % (2579845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.46 % (2579845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.46 % (2579845)CaDiCaL version: 2.1.3 % 22.22/3.46 % (2579845)Termination reason: Instruction limit % 22.22/3.46 % (2579845)Termination phase: Saturation % 22.22/3.46 % (2579845)Time elapsed: 0.085 s % 22.22/3.46 % (2579845)Peak memory usage: 13 MB % 22.22/3.46 % (2579845)Instructions burned: 132 (million) % 22.22/3.46 % (2579855)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1733476197:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.22/3.46 % (2579856)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2935104390:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.22/3.46 % Exception at run slice level % 22.22/3.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.22/3.46 % (2579849)Instruction limit reached! % 22.22/3.46 % (2579849)------------------------------ % 22.22/3.46 % (2579849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.46 % (2579849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.46 % (2579849)CaDiCaL version: 2.1.3 % 22.22/3.46 % (2579849)Termination reason: Instruction limit % 22.22/3.46 % (2579849)Termination phase: Saturation % 22.22/3.46 % (2579849)Time elapsed: 0.084 s % 22.22/3.46 % (2579849)Peak memory usage: 12 MB % 22.22/3.46 % (2579849)Instructions burned: 182 (million) % 22.22/3.46 % (2579859)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=2965154063: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) % 22.22/3.46 % (2579860)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1082721423:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 22.22/3.46 % (2579846)Instruction limit reached! % 22.22/3.46 % (2579846)------------------------------ % 22.22/3.46 % (2579846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.46 % (2579846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.46 % (2579846)CaDiCaL version: 2.1.3 % 22.22/3.46 % (2579846)Termination reason: Instruction limit % 22.22/3.46 % (2579846)Termination phase: Saturation % 22.22/3.46 % (2579846)Time elapsed: 0.187 s % 22.22/3.46 % (2579846)Peak memory usage: 16 MB % 22.22/3.46 % (2579846)Instructions burned: 688 (million) % 22.22/3.46 % (2579863)fmb+10_1_sil=64000:random_seed=1014275732:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 22.22/3.46 % (2579863)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.22/3.46 % Exception at run slice level % 22.22/3.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.22/3.46 % (2579865)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3330118702:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 22.22/3.46 % Exception at run slice level % 22.22/3.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.22/3.46 % (2579867)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1929582936:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 22.22/3.46 % Exception at run slice level % 22.22/3.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.22/3.46 % (2579869)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2172128669:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 22.22/3.46 % (2579850)Instruction limit reached! % 22.22/3.46 % (2579850)------------------------------ % 22.22/3.46 % (2579850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.46 % (2579850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.55/12.17 % (2579850)CaDiCaL version: 2.1.3 % 84.55/12.17 % (2579850)Termination reason: Instruction limit % 84.55/12.17 % (2579850)Termination phase: Saturation % 84.55/12.17 % (2579850)Time elapsed: 0.302 s % 84.55/12.17 % (2579850)Peak memory usage: 14 MB % 84.55/12.17 % (2579850)Instructions burned: 477 (million) % 84.55/12.17 % (2579871)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3771470401:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 84.55/12.17 % (2579871)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 84.55/12.17 % (2579859)Instruction limit reached! % 84.55/12.17 % (2579859)------------------------------ % 84.55/12.17 % (2579859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.55/12.17 % (2579859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.55/12.17 % (2579859)CaDiCaL version: 2.1.3 % 84.55/12.17 % (2579859)Termination reason: Instruction limit % 84.55/12.17 % (2579859)Termination phase: Saturation % 84.55/12.17 % (2579859)Time elapsed: 0.381 s % 84.55/12.17 % (2579859)Peak memory usage: 19 MB % 84.55/12.17 % (2579859)Instructions burned: 693 (million) % 84.55/12.17 % (2579873)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=6651021:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 84.55/12.17 % Exception at run slice level % 84.55/12.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.55/12.17 % (2579875)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3218407932:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 84.55/12.17 % Exception at run slice level % 84.55/12.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.55/12.17 % (2579877)ott-2_1_sil=16000:newcnf=on:random_seed=3364869576:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 84.55/12.17 % (2579860)Instruction limit reached! % 84.55/12.17 % (2579860)------------------------------ % 84.55/12.17 % (2579860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.55/12.17 % (2579860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.55/12.17 % (2579860)CaDiCaL version: 2.1.3 % 84.55/12.17 % (2579860)Termination reason: Instruction limit % 84.55/12.17 % (2579860)Termination phase: Saturation % 84.55/12.17 % (2579860)Time elapsed: 0.496 s % 84.55/12.17 % (2579860)Peak memory usage: 20 MB % 84.55/12.17 % (2579860)Instructions burned: 879 (million) % 84.55/12.17 % (2579879)ott+10_1_sil=32000:tgt=ground:random_seed=4294368232:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 84.55/12.17 % (2579855)Instruction limit reached! % 84.55/12.17 % (2579855)------------------------------ % 84.55/12.17 % (2579855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.55/12.17 % (2579855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.55/12.17 % (2579855)CaDiCaL version: 2.1.3 % 84.55/12.17 % (2579855)Termination reason: Instruction limit % 84.55/12.17 % (2579855)Termination phase: Saturation % 84.55/12.17 % (2579855)Time elapsed: 0.678 s % 84.55/12.17 % (2579855)Peak memory usage: 19 MB % 84.55/12.17 % (2579855)Instructions burned: 1180 (million) % 84.55/12.17 % (2579881)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2254476178:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 84.55/12.17 % Exception at run slice level % 84.55/12.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.55/12.17 % (2579883)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3831910537:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 84.55/12.17 % (2579871)Instruction limit reached! % 84.55/12.17 % (2579871)------------------------------ % 84.55/12.17 % (2579871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.55/12.17 % (2579871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.55/12.17 % (2579871)CaDiCaL version: 2.1.3 % 84.55/12.17 % (2579871)Termination reason: Instruction limit % 84.55/12.17 % (2579871)Termination phase: Saturation % 84.55/12.17 % (2579871)Time elapsed: 0.708 s % 84.55/12.17 % (2579871)Peak memory usage: 25 MB % 84.55/12.17 % (2579871)Instructions burned: 1472 (million) % 84.55/12.17 % (2579877)Instruction limit reached! % 84.55/12.17 % (2579877)------------------------------ % 84.55/12.17 % (2579877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.55/12.17 % (2579877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.81 % (2579877)CaDiCaL version: 2.1.3 % 124.78/17.81 % (2579877)Termination reason: Instruction limit % 124.78/17.81 % (2579877)Termination phase: Saturation % 124.78/17.81 % (2579877)Time elapsed: 0.516 s % 124.78/17.81 % (2579877)Peak memory usage: 17 MB % 124.78/17.81 % (2579877)Instructions burned: 869 (million) % 124.78/17.81 % (2579885)dis+21_1_sil=32000:sas=cadical:random_seed=2024831025:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 124.78/17.81 % (2579886)ott+11_1_sil=16000:gs=on:random_seed=1242582927:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 124.78/17.81 % (2579869)Instruction limit reached! % 124.78/17.81 % (2579869)------------------------------ % 124.78/17.81 % (2579869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.81 % (2579869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.81 % (2579869)CaDiCaL version: 2.1.3 % 124.78/17.81 % (2579869)Termination reason: Instruction limit % 124.78/17.81 % (2579869)Termination phase: Saturation % 124.78/17.81 % (2579869)Time elapsed: 1.587 s % 124.78/17.81 % (2579869)Peak memory usage: 31 MB % 124.78/17.81 % (2579869)Instructions burned: 5134 (million) % 124.78/17.81 % (2579889)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3130557662:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 124.78/17.81 % Exception at run slice level % 124.78/17.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.78/17.81 % (2579891)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=898915334:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 124.78/17.81 % (2579886)Instruction limit reached! % 124.78/17.81 % (2579886)------------------------------ % 124.78/17.81 % (2579886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.81 % (2579886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.81 % (2579886)CaDiCaL version: 2.1.3 % 124.78/17.81 % (2579886)Termination reason: Instruction limit % 124.78/17.81 % (2579886)Termination phase: Saturation % 124.78/17.81 % (2579886)Time elapsed: 1.239 s % 124.78/17.81 % (2579886)Peak memory usage: 27 MB % 124.78/17.81 % (2579886)Instructions burned: 2251 (million) % 124.78/17.81 % (2579894)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1152769838:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 124.78/17.81 % (2579883)Instruction limit reached! % 124.78/17.81 % (2579883)------------------------------ % 124.78/17.81 % (2579883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.81 % (2579883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.81 % (2579883)CaDiCaL version: 2.1.3 % 124.78/17.81 % (2579883)Termination reason: Instruction limit % 124.78/17.81 % (2579883)Termination phase: Saturation % 124.78/17.81 % (2579883)Time elapsed: 1.943 s % 124.78/17.81 % (2579883)Peak memory usage: 29 MB % 124.78/17.81 % (2579883)Instructions burned: 3513 (million) % 124.78/17.81 % (2579896)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2243363978:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 124.78/17.81 % (2579891)Instruction limit reached! % 124.78/17.81 % (2579891)------------------------------ % 124.78/17.81 % (2579891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.81 % (2579891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.81 % (2579891)CaDiCaL version: 2.1.3 % 124.78/17.81 % (2579891)Termination reason: Instruction limit % 124.78/17.81 % (2579891)Termination phase: Saturation % 124.78/17.81 % (2579891)Time elapsed: 1.250 s % 124.78/17.81 % (2579891)Peak memory usage: 51 MB % 124.78/17.81 % (2579891)Instructions burned: 4592 (million) % 124.78/17.81 % (2579898)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4009744730:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 124.78/17.81 % Exception at run slice level % 124.78/17.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.78/17.81 % (2579900)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2592969102:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 124.78/17.81 % Exception at run slice level % 124.78/17.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.78/17.81 % (2579902)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1894725024:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 124.78/17.81 % Exception at run slice level % 180.74/25.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.74/25.76 % (2579885)Instruction limit reached! % 180.74/25.76 % (2579885)------------------------------ % 180.74/25.76 % (2579885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579885)CaDiCaL version: 2.1.3 % 180.74/25.76 % (2579885)Termination reason: Instruction limit % 180.74/25.76 % (2579885)Termination phase: Saturation % 180.74/25.76 % (2579885)Time elapsed: 2.069 s % 180.74/25.76 % (2579885)Peak memory usage: 26 MB % 180.74/25.76 % (2579885)Instructions burned: 3774 (million) % 180.74/25.76 % (2579904)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2620471238:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 180.74/25.76 % (2579905)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3953616334:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 180.74/25.76 % (2579879)Instruction limit reached! % 180.74/25.76 % (2579879)------------------------------ % 180.74/25.76 % (2579879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579879)CaDiCaL version: 2.1.3 % 180.74/25.76 % (2579879)Termination reason: Instruction limit % 180.74/25.76 % (2579879)Termination phase: Saturation % 180.74/25.76 % (2579879)Time elapsed: 2.991 s % 180.74/25.76 % (2579879)Peak memory usage: 28 MB % 180.74/25.76 % (2579879)Instructions burned: 5115 (million) % 180.74/25.76 % (2579908)dis+10_16:1_sil=16000:random_seed=557170389:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 180.74/25.76 % (2579896)Instruction limit reached! % 180.74/25.76 % (2579896)------------------------------ % 180.74/25.76 % (2579896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579896)CaDiCaL version: 2.1.3 % 180.74/25.76 % (2579896)Termination reason: Instruction limit % 180.74/25.76 % (2579896)Termination phase: Saturation % 180.74/25.76 % (2579896)Time elapsed: 2.770 s % 180.74/25.76 % (2579896)Peak memory usage: 41 MB % 180.74/25.76 % (2579896)Instructions burned: 5211 (million) % 180.74/25.76 % (2579910)ott-3_8_sil=64000:random_seed=2398660300:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 180.74/25.76 % (2579905)Instruction limit reached! % 180.74/25.76 % (2579905)------------------------------ % 180.74/25.76 % (2579905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579905)CaDiCaL version: 2.1.3 % 180.74/25.76 % (2579905)Termination reason: Instruction limit % 180.74/25.76 % (2579905)Termination phase: Saturation % 180.74/25.76 % (2579905)Time elapsed: 4.872 s % 180.74/25.76 % (2579905)Peak memory usage: 61 MB % 180.74/25.76 % (2579905)Instructions burned: 8173 (million) % 180.74/25.76 % (2579912)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1222819853:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 180.74/25.76 % Exception at run slice level % 180.74/25.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 180.74/25.76 % (2579914)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=676561658:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 180.74/25.76 % (2579908)Instruction limit reached! % 180.74/25.76 % (2579908)------------------------------ % 180.74/25.76 % (2579908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579908)CaDiCaL version: 2.1.3 % 180.74/25.76 % (2579908)Termination reason: Instruction limit % 180.74/25.76 % (2579908)Termination phase: Saturation % 180.74/25.76 % (2579908)Time elapsed: 4.783 s % 180.74/25.76 % (2579908)Peak memory usage: 58 MB % 180.74/25.76 % (2579908)Instructions burned: 9155 (million) % 180.74/25.76 % (2579916)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2286433209:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 180.74/25.76 % (2579904)Instruction limit reached! % 180.74/25.76 % (2579904)------------------------------ % 180.74/25.76 % (2579904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.74/25.76 % (2579904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.74/25.76 % (2579904)CaDiCaL version: 2.1.3 % 195.05/27.72 % (2579904)Termination reason: Instruction limit % 195.05/27.72 % (2579904)Termination phase: Saturation % 195.05/27.72 % (2579904)Time elapsed: 8.691 s % 195.05/27.72 % (2579904)Peak memory usage: 31 MB % 195.05/27.72 % (2579904)Instructions burned: 22566 (million) % 195.05/27.72 % (2579918)dis+33_16_sil=32000:sac=on:random_seed=3618794163:i=15851:nm=0_2880 on theBenchmark for (2880ds/15851Mi) % 195.05/27.72 % (2579894)Instruction limit reached! % 195.05/27.72 % (2579894)------------------------------ % 195.05/27.72 % (2579894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.05/27.72 % (2579894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.05/27.72 % (2579894)CaDiCaL version: 2.1.3 % 195.05/27.72 % (2579894)Termination reason: Instruction limit % 195.05/27.72 % (2579894)Termination phase: Saturation % 195.05/27.72 % (2579894)Time elapsed: 12.298 s % 195.05/27.72 % (2579894)Peak memory usage: 168 MB % 195.05/27.72 % (2579894)Instructions burned: 29340 (million) % 195.05/27.72 % (2579920)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=982343769:avsq=on:i=17627:add=on:amm=off_2852 on theBenchmark for (2852ds/17627Mi) % 195.05/27.72 % (2579914)Instruction limit reached! % 195.05/27.72 % (2579914)------------------------------ % 195.05/27.72 % (2579914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.05/27.72 % (2579914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.05/27.72 % (2579914)CaDiCaL version: 2.1.3 % 195.05/27.72 % (2579914)Termination reason: Instruction limit % 195.05/27.72 % (2579914)Termination phase: Saturation % 195.05/27.72 % (2579914)Time elapsed: 6.872 s % 195.05/27.72 % (2579914)Peak memory usage: 56 MB % 195.05/27.72 % (2579914)Instructions burned: 11404 (million) % 195.05/27.72 % (2579922)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2844708945:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 195.05/27.72 % (2579910)Instruction limit reached! % 195.05/27.72 % (2579910)------------------------------ % 195.05/27.72 % (2579910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.05/27.72 % (2579910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.05/27.72 % (2579910)CaDiCaL version: 2.1.3 % 195.05/27.72 % (2579910)Termination reason: Instruction limit % 195.05/27.72 % (2579910)Termination phase: Saturation % 195.05/27.72 % (2579910)Time elapsed: 10.938 s % 195.05/27.72 % (2579910)Peak memory usage: 63 MB % 195.05/27.72 % (2579910)Instructions burned: 20140 (million) % 195.05/27.72 % (2579924)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3792330101:i=26857:ins=20_2834 on theBenchmark for (2834ds/26857Mi) % 195.05/27.72 % Exception at run slice level % 195.05/27.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.05/27.72 % (2579926)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3521122261:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 195.05/27.72 % (2579916)Instruction limit reached! % 195.05/27.72 % (2579916)------------------------------ % 195.05/27.72 % (2579916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.05/27.72 % (2579916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.05/27.72 % (2579916)CaDiCaL version: 2.1.3 % 195.05/27.72 % (2579916)Termination reason: Instruction limit % 195.05/27.72 % (2579916)Termination phase: Saturation % 195.05/27.72 % (2579916)Time elapsed: 8.936 s % 195.05/27.72 % (2579916)Peak memory usage: 69 MB % 195.05/27.72 % (2579916)Instructions burned: 14135 (million) % 195.05/27.72 % (2579928)fmb+10_1_sil=256000:fmbss=7:random_seed=2613669574:fmbsr=1.6:i=182295_2824 on theBenchmark for (2824ds/182295Mi) % 195.05/27.72 % Exception at run slice level % 195.05/27.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.05/27.72 % (2579930)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1103524451:i=44625:gsp=on_2824 on theBenchmark for (2824ds/44625Mi) % 195.05/27.72 % (2579930)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 195.05/27.72 % Exception at run slice level % 195.05/27.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.05/27.72 % (2579932)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=489030662:i=160505_2824 on theBenchmark for (2824ds/160505Mi) % 195.05/27.72 % Exception at run slice level % 195.05/27.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.05/27.72 % (2579934)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3002590645:fmbsr=1.3:i=225729_2824 on theBenchmark for (2824ds/225729Mi) % 245.44/34.82 % Exception at run slice level % 245.44/34.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 245.44/34.82 % (2579936)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1399060039:fmbsr=2:i=185024:ins=7_2824 on theBenchmark for (2824ds/185024Mi) % 245.44/34.82 % Exception at run slice level % 245.44/34.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 245.44/34.82 % (2579938)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3526946324:rtra=on_2823 on theBenchmark for (2823ds/0Mi) % 245.44/34.82 % Exception at run slice level % 245.44/34.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 245.44/34.82 % (2579940)% WARNING: option uhcvi not known. % 245.44/34.82 % (2579940)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2129756918:i=271062:add=off:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/271062Mi) % 245.44/34.82 % (2579918)Instruction limit reached! % 245.44/34.82 % (2579918)------------------------------ % 245.44/34.82 % (2579918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.44/34.82 % (2579918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.44/34.82 % (2579918)CaDiCaL version: 2.1.3 % 245.44/34.82 % (2579918)Termination reason: Instruction limit % 245.44/34.82 % (2579918)Termination phase: Saturation % 245.44/34.82 % (2579918)Time elapsed: 8.257 s % 245.44/34.82 % (2579918)Peak memory usage: 84 MB % 245.44/34.82 % (2579918)Instructions burned: 15851 (million) % 245.44/34.82 % (2579942)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=547030669:i=176048:add=on:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/176048Mi) % 245.44/34.82 % (2579920)Instruction limit reached! % 245.44/34.82 % (2579920)------------------------------ % 245.44/34.82 % (2579920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.44/34.82 % (2579920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.44/34.82 % (2579920)CaDiCaL version: 2.1.3 % 245.44/34.82 % (2579920)Termination reason: Instruction limit % 245.44/34.82 % (2579920)Termination phase: Saturation % 245.44/34.82 % (2579920)Time elapsed: 10.220 s % 245.44/34.82 % (2579920)Peak memory usage: 344 MB % 245.44/34.82 % (2579920)Instructions burned: 17628 (million) % 245.44/34.82 % (2579944)dis+10_1_sil=32000:si=on:sp=arity:random_seed=398934186:i=206:fgj=on:rtra=on_2749 on theBenchmark for (2749ds/206Mi) % 245.44/34.82 % (2579944)Instruction limit reached! % 245.44/34.82 % (2579944)------------------------------ % 245.44/34.82 % (2579944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.44/34.82 % (2579944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.44/34.82 % (2579944)CaDiCaL version: 2.1.3 % 245.44/34.82 % (2579944)Termination reason: Instruction limit % 245.44/34.82 % (2579944)Termination phase: Saturation % 245.44/34.82 % (2579944)Time elapsed: 0.126 s % 245.44/34.82 % (2579944)Peak memory usage: 13 MB % 245.44/34.82 % (2579944)Instructions burned: 207 (million) % 245.44/34.82 % (2579946)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2189689110:i=232:rtra=on_2747 on theBenchmark for (2747ds/232Mi) % 245.44/34.82 % (2579946)Instruction limit reached! % 245.44/34.82 % (2579946)------------------------------ % 245.44/34.82 % (2579946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.44/34.82 % (2579946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.44/34.82 % (2579946)CaDiCaL version: 2.1.3 % 245.44/34.82 % (2579946)Termination reason: Instruction limit % 245.44/34.82 % (2579946)Termination phase: Saturation % 245.44/34.82 % (2579946)Time elapsed: 0.147 s % 245.44/34.82 % (2579946)Peak memory usage: 14 MB % 245.44/34.82 % (2579946)Instructions burned: 232 (million) % 245.44/34.82 % (2579948)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2731681006:i=262:rtra=on_2746 on theBenchmark for (2746ds/262Mi) % 245.44/34.82 % (2579948)Instruction limit reached! % 245.44/34.82 % (2579948)------------------------------ % 245.44/34.82 % (2579948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.44/34.82 % (2579948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.44/34.82 % (2579948)CaDiCaL version: 2.1.3 % 245.44/34.82 % (2579948)Termination reason: Instruction limit % 245.44/34.82 % (2579948)Termination phase: Saturation % 266.60/38.03 % (2579948)Time elapsed: 0.148 s % 266.60/38.03 % (2579948)Peak memory usage: 14 MB % 266.60/38.03 % (2579948)Instructions burned: 263 (million) % 266.60/38.03 % (2579950)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=698943202:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2744 on theBenchmark for (2744ds/318Mi) % 266.60/38.03 % (2579950)Instruction limit reached! % 266.60/38.03 % (2579950)------------------------------ % 266.60/38.03 % (2579950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.60/38.03 % (2579950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.03 % (2579950)CaDiCaL version: 2.1.3 % 266.60/38.03 % (2579950)Termination reason: Instruction limit % 266.60/38.03 % (2579950)Termination phase: Saturation % 266.60/38.03 % (2579950)Time elapsed: 0.194 s % 266.60/38.03 % (2579950)Peak memory usage: 16 MB % 266.60/38.03 % (2579950)Instructions burned: 319 (million) % 266.60/38.03 % (2579952)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1589049517:i=1428:nm=2:rtra=on_2742 on theBenchmark for (2742ds/1428Mi) % 266.60/38.03 % Exception at run slice level % 266.60/38.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 266.60/38.03 % (2579954)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=788345274:i=262:bd=preordered:rtra=on:fsd=on_2742 on theBenchmark for (2742ds/262Mi) % 266.60/38.03 % (2579954)Instruction limit reached! % 266.60/38.03 % (2579954)------------------------------ % 266.60/38.03 % (2579954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.60/38.03 % (2579954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.03 % (2579954)CaDiCaL version: 2.1.3 % 266.60/38.03 % (2579954)Termination reason: Instruction limit % 266.60/38.03 % (2579954)Termination phase: Saturation % 266.60/38.03 % (2579954)Time elapsed: 0.173 s % 266.60/38.03 % (2579954)Peak memory usage: 15 MB % 266.60/38.03 % (2579954)Instructions burned: 262 (million) % 266.60/38.03 % (2579956)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=1910139721:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/1368Mi) % 266.60/38.03 % (2579956)Instruction limit reached! % 266.60/38.03 % (2579956)------------------------------ % 266.60/38.03 % (2579956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.60/38.03 % (2579956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.03 % (2579956)CaDiCaL version: 2.1.3 % 266.60/38.03 % (2579956)Termination reason: Instruction limit % 266.60/38.03 % (2579956)Termination phase: Saturation % 266.60/38.03 % (2579956)Time elapsed: 0.662 s % 266.60/38.03 % (2579956)Peak memory usage: 18 MB % 266.60/38.03 % (2579956)Instructions burned: 1370 (million) % 266.60/38.03 % (2579958)ott-21_1_sil=16000:si=on:fs=off:random_seed=3360011081:i=360:av=off:fsr=off:rtra=on_2733 on theBenchmark for (2733ds/360Mi) % 266.60/38.03 % (2579958)Instruction limit reached! % 266.60/38.03 % (2579958)------------------------------ % 266.60/38.03 % (2579958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.60/38.03 % (2579958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.03 % (2579958)CaDiCaL version: 2.1.3 % 266.60/38.03 % (2579958)Termination reason: Instruction limit % 266.60/38.03 % (2579958)Termination phase: Saturation % 266.60/38.03 % (2579958)Time elapsed: 0.159 s % 266.60/38.03 % (2579958)Peak memory usage: 13 MB % 266.60/38.03 % (2579958)Instructions burned: 360 (million) % 266.60/38.03 % (2579960)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=573409959:i=954:bd=all:rtra=on_2731 on theBenchmark for (2731ds/954Mi) % 266.60/38.03 % (2579960)Instruction limit reached! % 266.60/38.03 % (2579960)------------------------------ % 266.60/38.03 % (2579960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.60/38.03 % (2579960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.03 % (2579960)CaDiCaL version: 2.1.3 % 266.60/38.03 % (2579960)Termination reason: Instruction limit % 266.60/38.03 % (2579960)Termination phase: Saturation % 266.60/38.03 % (2579960)Time elapsed: 0.614 s % 266.60/38.03 % (2579960)Peak memory usage: 15 MB % 266.60/38.03 % (2579960)Instructions burned: 954 (million) % 266.60/38.03 % (2579962)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1381507148:fmbsr=1.3:i=1730:ins=25:rtra=on_2725 on theBenchmark for (2725ds/1730Mi) % 266.60/38.03 % Exception at run slice level % 266.60/38.03 User error: Finite model building is currentlTerminated % 300.09/42.54 % Vampire exiting %------------------------------------------------------------------------------