%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM110_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:19 AM UTC 2026 % Result : Timeout 292.92s 41.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : COM110_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n008.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 21:55:10 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.26 Running first-order model finding % 0.10/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.74/1.42 % (2694083)Will run a generic schedule for satisfiability detection. % 7.74/1.42 % (2694098)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4267809031:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.74/1.42 % (2694093)% WARNING: option uhcvi not known. % 7.74/1.42 % (2694094)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1436034155:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.74/1.42 % (2694092)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3055471351_2999 on theBenchmark for (2999ds/0Mi) % 7.74/1.42 % (2694097)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3474673705:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.74/1.42 % (2694093)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2564898206:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.74/1.42 % (2694096)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=783241101:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.74/1.42 % (2694095)dis+10_1_sil=32000:sp=arity:random_seed=3538836244:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.74/1.42 % Exception at run slice level % 7.74/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.74/1.42 % (2694119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2643183545:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.74/1.42 % (2694098)Instruction limit reached! % 7.74/1.42 % (2694098)------------------------------ % 7.74/1.42 % (2694098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.74/1.42 % (2694098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.74/1.42 % (2694098)CaDiCaL version: 2.1.3 % 7.74/1.42 % (2694098)Termination reason: Instruction limit % 7.74/1.42 % (2694098)Termination phase: Saturation % 7.74/1.42 % (2694098)Time elapsed: 0.042 s % 7.74/1.42 % (2694098)Peak memory usage: 13 MB % 7.74/1.42 % (2694098)Instructions burned: 162 (million) % 7.74/1.42 % Exception at run slice level % 7.74/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.74/1.42 % (2694127)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3240314529:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.74/1.42 % (2694128)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=2365812886:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.74/1.42 % (2694095)Instruction limit reached! % 7.74/1.42 % (2694095)------------------------------ % 7.74/1.42 % (2694095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.74/1.42 % (2694095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.74/1.42 % (2694095)CaDiCaL version: 2.1.3 % 7.74/1.42 % (2694095)Termination reason: Instruction limit % 7.74/1.42 % (2694095)Termination phase: Saturation % 7.74/1.42 % (2694095)Time elapsed: 0.060 s % 7.74/1.42 % (2694095)Peak memory usage: 12 MB % 7.74/1.42 % (2694095)Instructions burned: 104 (million) % 7.74/1.42 % (2694096)Instruction limit reached! % 7.74/1.42 % (2694096)------------------------------ % 7.74/1.42 % (2694096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.74/1.42 % (2694096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.74/1.42 % (2694096)CaDiCaL version: 2.1.3 % 7.74/1.42 % (2694096)Termination reason: Instruction limit % 7.74/1.42 % (2694096)Termination phase: Saturation % 7.74/1.42 % (2694096)Time elapsed: 0.069 s % 7.74/1.42 % (2694096)Peak memory usage: 13 MB % 7.74/1.42 % (2694096)Instructions burned: 117 (million) % 7.74/1.42 % (2694097)Instruction limit reached! % 7.74/1.42 % (2694097)------------------------------ % 7.74/1.42 % (2694097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.74/1.42 % (2694097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.74/1.42 % (2694097)CaDiCaL version: 2.1.3 % 7.74/1.42 % (2694097)Termination reason: Instruction limit % 7.74/1.42 % (2694097)Termination phase: Saturation % 7.74/1.42 % (2694097)Time elapsed: 0.070 s % 7.74/1.42 % (2694097)Peak memory usage: 12 MB % 7.74/1.42 % (2694097)Instructions burned: 131 (million) % 7.74/1.42 % (2694137)ott-21_1_sil=16000:fs=off:random_seed=1224409298:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.74/1.42 % (2694127)Instruction limit reached! % 20.90/3.24 % (2694127)------------------------------ % 20.90/3.24 % (2694127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.90/3.24 % (2694127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.90/3.24 % (2694127)CaDiCaL version: 2.1.3 % 20.90/3.24 % (2694127)Termination reason: Instruction limit % 20.90/3.24 % (2694127)Termination phase: Saturation % 20.90/3.24 % (2694127)Time elapsed: 0.041 s % 20.90/3.24 % (2694127)Peak memory usage: 13 MB % 20.90/3.24 % (2694127)Instructions burned: 134 (million) % 20.90/3.24 % (2694140)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1543260121:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 20.90/3.24 % (2694142)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1307062674:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.90/3.24 % (2694150)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=854399181:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.90/3.24 % Exception at run slice level % 20.90/3.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.90/3.24 % (2694159)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1126379234:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.90/3.24 % Exception at run slice level % 20.90/3.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.90/3.24 % (2694169)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=3681487665:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 20.90/3.24 % (2694137)Instruction limit reached! % 20.90/3.24 % (2694137)------------------------------ % 20.90/3.24 % (2694137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.90/3.24 % (2694137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.90/3.24 % (2694137)CaDiCaL version: 2.1.3 % 20.90/3.24 % (2694137)Termination reason: Instruction limit % 20.90/3.24 % (2694137)Termination phase: Saturation % 20.90/3.24 % (2694137)Time elapsed: 0.090 s % 20.90/3.24 % (2694137)Peak memory usage: 12 MB % 20.90/3.24 % (2694137)Instructions burned: 182 (million) % 20.90/3.24 % (2694180)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1046826719:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.90/3.24 % (2694140)Instruction limit reached! % 20.90/3.24 % (2694140)------------------------------ % 20.90/3.24 % (2694140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.90/3.24 % (2694140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.90/3.24 % (2694140)CaDiCaL version: 2.1.3 % 20.90/3.24 % (2694140)Termination reason: Instruction limit % 20.90/3.24 % (2694140)Termination phase: Saturation % 20.90/3.24 % (2694140)Time elapsed: 0.248 s % 20.90/3.24 % (2694140)Peak memory usage: 13 MB % 20.90/3.24 % (2694140)Instructions burned: 478 (million) % 20.90/3.24 % (2694211)fmb+10_1_sil=64000:random_seed=1510225841:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.90/3.24 % (2694211)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.90/3.24 % Exception at run slice level % 20.90/3.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.90/3.24 % (2694128)Instruction limit reached! % 20.90/3.24 % (2694128)------------------------------ % 20.90/3.24 % (2694128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.90/3.24 % (2694128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.90/3.24 % (2694128)CaDiCaL version: 2.1.3 % 20.90/3.24 % (2694128)Termination reason: Instruction limit % 20.90/3.24 % (2694128)Termination phase: Saturation % 20.90/3.24 % (2694128)Time elapsed: 0.320 s % 20.90/3.24 % (2694128)Peak memory usage: 14 MB % 20.90/3.24 % (2694128)Instructions burned: 684 (million) % 20.90/3.24 % (2694213)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2704721595:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.90/3.24 % Exception at run slice level % 20.90/3.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.90/3.24 % (2694214)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3758540580:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 20.90/3.24 % Exception at run slice level % 69.40/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.40/10.11 % (2694216)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3688001064:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 69.40/10.11 % (2694150)Instruction limit reached! % 69.40/10.11 % (2694150)------------------------------ % 69.40/10.11 % (2694150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.40/10.11 % (2694150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.40/10.11 % (2694150)CaDiCaL version: 2.1.3 % 69.40/10.11 % (2694150)Termination reason: Instruction limit % 69.40/10.11 % (2694150)Termination phase: Saturation % 69.40/10.11 % (2694150)Time elapsed: 0.327 s % 69.40/10.11 % (2694150)Peak memory usage: 17 MB % 69.40/10.11 % (2694150)Instructions burned: 1182 (million) % 69.40/10.11 % (2694220)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3276964743:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 69.40/10.11 % (2694220)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 69.40/10.11 % (2694226)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=798883213:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 69.40/10.11 % Exception at run slice level % 69.40/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.40/10.11 % (2694231)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=479142771:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 69.40/10.11 % Exception at run slice level % 69.40/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.40/10.11 % (2694239)ott-2_1_sil=16000:newcnf=on:random_seed=3364311489:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 69.40/10.11 % (2694169)Instruction limit reached! % 69.40/10.11 % (2694169)------------------------------ % 69.40/10.11 % (2694169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.40/10.11 % (2694169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.40/10.11 % (2694169)CaDiCaL version: 2.1.3 % 69.40/10.11 % (2694169)Termination reason: Instruction limit % 69.40/10.11 % (2694169)Termination phase: Saturation % 69.40/10.11 % (2694169)Time elapsed: 0.383 s % 69.40/10.11 % (2694169)Peak memory usage: 15 MB % 69.40/10.11 % (2694169)Instructions burned: 693 (million) % 69.40/10.11 % (2694271)ott+10_1_sil=32000:tgt=ground:random_seed=547992581:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 69.40/10.11 % (2694180)Instruction limit reached! % 69.40/10.11 % (2694180)------------------------------ % 69.40/10.11 % (2694180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.40/10.11 % (2694180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.40/10.11 % (2694180)CaDiCaL version: 2.1.3 % 69.40/10.11 % (2694180)Termination reason: Instruction limit % 69.40/10.11 % (2694180)Termination phase: Saturation % 69.40/10.11 % (2694180)Time elapsed: 0.471 s % 69.40/10.11 % (2694180)Peak memory usage: 18 MB % 69.40/10.11 % (2694180)Instructions burned: 879 (million) % 69.40/10.11 % (2694276)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2159945545:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 69.40/10.11 % Exception at run slice level % 69.40/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.40/10.11 % (2694278)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1297753759:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 69.40/10.11 % (2694239)Instruction limit reached! % 69.40/10.11 % (2694239)------------------------------ % 69.40/10.11 % (2694239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.40/10.11 % (2694239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.40/10.11 % (2694239)CaDiCaL version: 2.1.3 % 69.40/10.11 % (2694239)Termination reason: Instruction limit % 69.40/10.11 % (2694239)Termination phase: Saturation % 69.40/10.11 % (2694239)Time elapsed: 0.248 s % 69.40/10.11 % (2694239)Peak memory usage: 14 MB % 69.40/10.11 % (2694239)Instructions burned: 873 (million) % 69.40/10.11 % (2694280)dis+21_1_sil=32000:sas=cadical:random_seed=2781352052:i=3773:amm=off_2992 on theBenchmark for (2992ds/3773Mi) % 69.40/10.11 % (2694220)Instruction limit reached! % 69.40/10.11 % (2694220)------------------------------ % 69.40/10.11 % (2694220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694220)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694220)Termination reason: Instruction limit % 109.85/15.87 % (2694220)Termination phase: Saturation % 109.85/15.87 % (2694220)Time elapsed: 0.702 s % 109.85/15.87 % (2694220)Peak memory usage: 19 MB % 109.85/15.87 % (2694220)Instructions burned: 1474 (million) % 109.85/15.87 % (2694282)ott+11_1_sil=16000:gs=on:random_seed=1726953836:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 109.85/15.87 % (2694280)Instruction limit reached! % 109.85/15.87 % (2694280)------------------------------ % 109.85/15.87 % (2694280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694280)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694280)Termination reason: Instruction limit % 109.85/15.87 % (2694280)Termination phase: Saturation % 109.85/15.87 % (2694280)Time elapsed: 1.035 s % 109.85/15.87 % (2694280)Peak memory usage: 27 MB % 109.85/15.87 % (2694280)Instructions burned: 3774 (million) % 109.85/15.87 % (2694284)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=158767021:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 109.85/15.87 % Exception at run slice level % 109.85/15.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 109.85/15.87 % (2694286)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4021429895:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 109.85/15.87 % (2694282)Instruction limit reached! % 109.85/15.87 % (2694282)------------------------------ % 109.85/15.87 % (2694282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694282)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694282)Termination reason: Instruction limit % 109.85/15.87 % (2694282)Termination phase: Saturation % 109.85/15.87 % (2694282)Time elapsed: 1.104 s % 109.85/15.87 % (2694282)Peak memory usage: 18 MB % 109.85/15.87 % (2694282)Instructions burned: 2253 (million) % 109.85/15.87 % (2694288)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=87222765:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 109.85/15.87 % (2694278)Instruction limit reached! % 109.85/15.87 % (2694278)------------------------------ % 109.85/15.87 % (2694278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694278)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694278)Termination reason: Instruction limit % 109.85/15.87 % (2694278)Termination phase: Saturation % 109.85/15.87 % (2694278)Time elapsed: 1.730 s % 109.85/15.87 % (2694278)Peak memory usage: 23 MB % 109.85/15.87 % (2694278)Instructions burned: 3513 (million) % 109.85/15.87 % (2694290)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1727477572:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 109.85/15.87 % (2694286)Instruction limit reached! % 109.85/15.87 % (2694286)------------------------------ % 109.85/15.87 % (2694286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694286)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694286)Termination reason: Instruction limit % 109.85/15.87 % (2694286)Termination phase: Saturation % 109.85/15.87 % (2694286)Time elapsed: 1.136 s % 109.85/15.87 % (2694286)Peak memory usage: 39 MB % 109.85/15.87 % (2694286)Instructions burned: 4591 (million) % 109.85/15.87 % (2694271)Instruction limit reached! % 109.85/15.87 % (2694271)------------------------------ % 109.85/15.87 % (2694271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.85/15.87 % (2694271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.85/15.87 % (2694271)CaDiCaL version: 2.1.3 % 109.85/15.87 % (2694271)Termination reason: Instruction limit % 109.85/15.87 % (2694271)Termination phase: Saturation % 109.85/15.87 % (2694271)Time elapsed: 2.390 s % 109.85/15.87 % (2694271)Peak memory usage: 19 MB % 109.85/15.87 % (2694271)Instructions burned: 5116 (million) % 109.85/15.87 % (2694292)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3647636901:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 109.85/15.87 % Exception at run slice level % 109.85/15.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.53/24.39 % (2694293)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=405842549:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 170.53/24.39 % (2694295)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3065574674:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 170.53/24.39 % Exception at run slice level % 170.53/24.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.53/24.39 % Exception at run slice level % 170.53/24.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.53/24.39 % (2694299)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=169456922:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi) % 170.53/24.39 % (2694216)Instruction limit reached! % 170.53/24.39 % (2694216)------------------------------ % 170.53/24.39 % (2694216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.53/24.39 % (2694216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.53/24.39 % (2694216)CaDiCaL version: 2.1.3 % 170.53/24.39 % (2694216)Termination reason: Instruction limit % 170.53/24.39 % (2694216)Termination phase: Saturation % 170.53/24.39 % (2694216)Time elapsed: 2.564 s % 170.53/24.39 % (2694216)Peak memory usage: 26 MB % 170.53/24.39 % (2694216)Instructions burned: 5131 (million) % 170.53/24.39 % (2694298)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4033266062:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 170.53/24.39 % (2694301)dis+10_16:1_sil=16000:random_seed=1274366498:i=9155:fsr=off_2969 on theBenchmark for (2969ds/9155Mi) % 170.53/24.39 % (2694299)Instruction limit reached! % 170.53/24.39 % (2694299)------------------------------ % 170.53/24.39 % (2694299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.53/24.39 % (2694299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.53/24.39 % (2694299)CaDiCaL version: 2.1.3 % 170.53/24.39 % (2694299)Termination reason: Instruction limit % 170.53/24.39 % (2694299)Termination phase: Saturation % 170.53/24.39 % (2694299)Time elapsed: 2.130 s % 170.53/24.39 % (2694299)Peak memory usage: 26 MB % 170.53/24.39 % (2694299)Instructions burned: 8173 (million) % 170.53/24.39 % (2694304)ott-3_8_sil=64000:random_seed=3010255949:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 170.53/24.39 % (2694290)Instruction limit reached! % 170.53/24.39 % (2694290)------------------------------ % 170.53/24.39 % (2694290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.53/24.39 % (2694290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.53/24.39 % (2694290)CaDiCaL version: 2.1.3 % 170.53/24.39 % (2694290)Termination reason: Instruction limit % 170.53/24.39 % (2694290)Termination phase: Saturation % 170.53/24.39 % (2694290)Time elapsed: 2.790 s % 170.53/24.39 % (2694290)Peak memory usage: 36 MB % 170.53/24.39 % (2694290)Instructions burned: 5212 (million) % 170.53/24.39 % (2694306)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2192184418:fmbsr=2:i=32576_2947 on theBenchmark for (2947ds/32576Mi) % 170.53/24.39 % Exception at run slice level % 170.53/24.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.53/24.39 % (2694308)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3335458818:i=11404_2946 on theBenchmark for (2946ds/11404Mi) % 170.53/24.39 % (2694301)Instruction limit reached! % 170.53/24.39 % (2694301)------------------------------ % 170.53/24.39 % (2694301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.53/24.39 % (2694301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.53/24.39 % (2694301)CaDiCaL version: 2.1.3 % 170.53/24.39 % (2694301)Termination reason: Instruction limit % 170.53/24.39 % (2694301)Termination phase: Saturation % 170.53/24.39 % (2694301)Time elapsed: 4.964 s % 170.53/24.39 % (2694301)Peak memory usage: 49 MB % 170.53/24.39 % (2694301)Instructions burned: 9156 (million) % 170.53/24.39 % (2694310)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1713001693:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 170.53/24.39 % (2694304)Instruction limit reached! % 170.53/24.39 % (2694304)------------------------------ % 170.53/24.39 % (2694304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.53/24.39 % (2694304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.53/24.39 % (2694304)CaDiCaL version: 2.1.3 % 192.68/27.44 % (2694304)Termination reason: Instruction limit % 192.68/27.44 % (2694304)Termination phase: Saturation % 192.68/27.44 % (2694304)Time elapsed: 4.698 s % 192.68/27.44 % (2694304)Peak memory usage: 24 MB % 192.68/27.44 % (2694304)Instructions burned: 20143 (million) % 192.68/27.44 % (2694312)dis+33_16_sil=32000:sac=on:random_seed=3706326806:i=15851:nm=0_2901 on theBenchmark for (2901ds/15851Mi) % 192.68/27.44 % (2694308)Instruction limit reached! % 192.68/27.44 % (2694308)------------------------------ % 192.68/27.44 % (2694308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.68/27.44 % (2694308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.68/27.44 % (2694308)CaDiCaL version: 2.1.3 % 192.68/27.44 % (2694308)Termination reason: Instruction limit % 192.68/27.44 % (2694308)Termination phase: Saturation % 192.68/27.44 % (2694308)Time elapsed: 7.274 s % 192.68/27.44 % (2694308)Peak memory usage: 144 MB % 192.68/27.44 % (2694308)Instructions burned: 11404 (million) % 192.68/27.44 % (2694314)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=960902245:avsq=on:i=17627:add=on:amm=off_2873 on theBenchmark for (2873ds/17627Mi) % 192.68/27.44 % (2694312)Instruction limit reached! % 192.68/27.44 % (2694312)------------------------------ % 192.68/27.44 % (2694312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.68/27.44 % (2694312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.68/27.44 % (2694312)CaDiCaL version: 2.1.3 % 192.68/27.44 % (2694312)Termination reason: Instruction limit % 192.68/27.44 % (2694312)Termination phase: Saturation % 192.68/27.44 % (2694312)Time elapsed: 4.675 s % 192.68/27.44 % (2694312)Peak memory usage: 405 MB % 192.68/27.44 % (2694312)Instructions burned: 15852 (million) % 192.68/27.44 % (2694578)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2633575894:s2a=on:i=53295_2854 on theBenchmark for (2854ds/53295Mi) % 192.68/27.44 % (2694310)Instruction limit reached! % 192.68/27.44 % (2694310)------------------------------ % 192.68/27.44 % (2694310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.68/27.44 % (2694310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.68/27.44 % (2694310)CaDiCaL version: 2.1.3 % 192.68/27.44 % (2694310)Termination reason: Instruction limit % 192.68/27.44 % (2694310)Termination phase: Saturation % 192.68/27.44 % (2694310)Time elapsed: 6.975 s % 192.68/27.44 % (2694310)Peak memory usage: 34 MB % 192.68/27.44 % (2694310)Instructions burned: 14135 (million) % 192.68/27.44 % (2694580)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=754712551:i=26857:ins=20_2850 on theBenchmark for (2850ds/26857Mi) % 192.68/27.44 % Exception at run slice level % 192.68/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.68/27.44 % (2694582)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=558312242:i=28120:bs=on:fsr=off_2849 on theBenchmark for (2849ds/28120Mi) % 192.68/27.44 % (2694298)Instruction limit reached! % 192.68/27.44 % (2694298)------------------------------ % 192.68/27.44 % (2694298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.68/27.44 % (2694298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.68/27.44 % (2694298)CaDiCaL version: 2.1.3 % 192.68/27.44 % (2694298)Termination reason: Instruction limit % 192.68/27.44 % (2694298)Termination phase: Saturation % 192.68/27.44 % (2694298)Time elapsed: 12.382 s % 192.68/27.44 % (2694298)Peak memory usage: 98 MB % 192.68/27.44 % (2694298)Instructions burned: 22565 (million) % 192.68/27.44 % (2694600)fmb+10_1_sil=256000:fmbss=7:random_seed=3928390862:fmbsr=1.6:i=182295_2845 on theBenchmark for (2845ds/182295Mi) % 192.68/27.44 % Exception at run slice level % 192.68/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.68/27.44 % (2694603)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2805513175:i=44625:gsp=on_2845 on theBenchmark for (2845ds/44625Mi) % 192.68/27.44 % (2694603)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.68/27.44 % Exception at run slice level % 192.68/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.68/27.44 % (2694605)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3964078562:i=160505_2844 on theBenchmark for (2844ds/160505Mi) % 192.68/27.44 % Exception at run slice level % 192.68/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.68/27.44 % (2694608)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3802961150:fmbsr=1.3:i=225729_2844 on theBenchmark for (2844ds/225729Mi) % 228.80/32.55 % Exception at run slice level % 228.80/32.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 228.80/32.55 % (2694611)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=225246997:fmbsr=2:i=185024:ins=7_2843 on theBenchmark for (2843ds/185024Mi) % 228.80/32.55 % Exception at run slice level % 228.80/32.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 228.80/32.55 % (2694614)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1426801613:rtra=on_2843 on theBenchmark for (2843ds/0Mi) % 228.80/32.55 % Exception at run slice level % 228.80/32.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 228.80/32.55 % (2694618)% WARNING: option uhcvi not known. % 228.80/32.55 % (2694618)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=972947759:i=271062:add=off:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/271062Mi) % 228.80/32.55 % (2694288)Instruction limit reached! % 228.80/32.55 % (2694288)------------------------------ % 228.80/32.55 % (2694288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.80/32.55 % (2694288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.80/32.55 % (2694288)CaDiCaL version: 2.1.3 % 228.80/32.55 % (2694288)Termination reason: Instruction limit % 228.80/32.55 % (2694288)Termination phase: Saturation % 228.80/32.55 % (2694288)Time elapsed: 16.365 s % 228.80/32.55 % (2694288)Peak memory usage: 631 MB % 228.80/32.55 % (2694288)Instructions burned: 29340 (million) % 228.80/32.55 % (2694685)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3216287830:i=176048:add=on:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/176048Mi) % 228.80/32.55 % (2694314)Instruction limit reached! % 228.80/32.55 % (2694314)------------------------------ % 228.80/32.55 % (2694314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.80/32.55 % (2694314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.80/32.55 % (2694314)CaDiCaL version: 2.1.3 % 228.80/32.55 % (2694314)Termination reason: Instruction limit % 228.80/32.55 % (2694314)Termination phase: Saturation % 228.80/32.55 % (2694314)Time elapsed: 10.744 s % 228.80/32.55 % (2694314)Peak memory usage: 71 MB % 228.80/32.55 % (2694314)Instructions burned: 17627 (million) % 228.80/32.55 % (2694740)dis+10_1_sil=32000:si=on:sp=arity:random_seed=731432032:i=206:fgj=on:rtra=on_2765 on theBenchmark for (2765ds/206Mi) % 228.80/32.55 % (2694740)Instruction limit reached! % 228.80/32.55 % (2694740)------------------------------ % 228.80/32.55 % (2694740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.80/32.55 % (2694740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.80/32.55 % (2694740)CaDiCaL version: 2.1.3 % 228.80/32.55 % (2694740)Termination reason: Instruction limit % 228.80/32.55 % (2694740)Termination phase: Saturation % 228.80/32.55 % (2694740)Time elapsed: 0.206 s % 228.80/32.55 % (2694740)Peak memory usage: 13 MB % 228.80/32.55 % (2694740)Instructions burned: 206 (million) % 228.80/32.55 % (2694746)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2068564566:i=232:rtra=on_2763 on theBenchmark for (2763ds/232Mi) % 228.80/32.55 % (2694746)Instruction limit reached! % 228.80/32.55 % (2694746)------------------------------ % 228.80/32.55 % (2694746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.80/32.55 % (2694746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.80/32.55 % (2694746)CaDiCaL version: 2.1.3 % 228.80/32.55 % (2694746)Termination reason: Instruction limit % 228.80/32.55 % (2694746)Termination phase: Saturation % 228.80/32.55 % (2694746)Time elapsed: 0.207 s % 228.80/32.55 % (2694746)Peak memory usage: 14 MB % 228.80/32.55 % (2694746)Instructions burned: 232 (million) % 228.80/32.55 % (2694749)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=954716577:i=262:rtra=on_2761 on theBenchmark for (2761ds/262Mi) % 228.80/32.55 % (2694749)Instruction limit reached! % 228.80/32.55 % (2694749)------------------------------ % 228.80/32.55 % (2694749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.80/32.55 % (2694749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.80/32.55 % (2694749)CaDiCaL version: 2.1.3 % 228.80/32.55 % (2694749)Termination reason: Instruction limit % 228.80/32.55 % (2694749)Termination phase: Saturation % 292.92/41.57 % (2694749)Time elapsed: 0.196 s % 292.92/41.57 % (2694749)Peak memory usage: 13 MB % 292.92/41.57 % (2694749)Instructions burned: 262 (million) % 292.92/41.57 % (2694752)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2552046780:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2758 on theBenchmark for (2758ds/318Mi) % 292.92/41.57 % (2694752)Instruction limit reached! % 292.92/41.57 % (2694752)------------------------------ % 292.92/41.57 % (2694752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.92/41.57 % (2694752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.92/41.57 % (2694752)CaDiCaL version: 2.1.3 % 292.92/41.57 % (2694752)Termination reason: Instruction limit % 292.92/41.57 % (2694752)Termination phase: Saturation % 292.92/41.57 % (2694752)Time elapsed: 0.260 s % 292.92/41.57 % (2694752)Peak memory usage: 13 MB % 292.92/41.57 % (2694752)Instructions burned: 318 (million) % 292.92/41.57 % (2694757)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3788773563:i=1428:nm=2:rtra=on_2755 on theBenchmark for (2755ds/1428Mi) % 292.92/41.57 % Exception at run slice level % 292.92/41.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 292.92/41.57 % (2694760)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2171354149:i=262:bd=preordered:rtra=on:fsd=on_2755 on theBenchmark for (2755ds/262Mi) % 292.92/41.57 % (2694760)Instruction limit reached! % 292.92/41.57 % (2694760)------------------------------ % 292.92/41.57 % (2694760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.92/41.57 % (2694760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.92/41.57 % (2694760)CaDiCaL version: 2.1.3 % 292.92/41.57 % (2694760)Termination reason: Instruction limit % 292.92/41.57 % (2694760)Termination phase: Saturation % 292.92/41.57 % (2694760)Time elapsed: 0.251 s % 292.92/41.57 % (2694760)Peak memory usage: 15 MB % 292.92/41.57 % (2694760)Instructions burned: 262 (million) % 292.92/41.57 % (2694764)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=262966390:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2752 on theBenchmark for (2752ds/1368Mi) % 292.92/41.57 % (2694764)Instruction limit reached! % 292.92/41.57 % (2694764)------------------------------ % 292.92/41.57 % (2694764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.92/41.57 % (2694764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.92/41.57 % (2694764)CaDiCaL version: 2.1.3 % 292.92/41.57 % (2694764)Termination reason: Instruction limit % 292.92/41.57 % (2694764)Termination phase: Saturation % 292.92/41.57 % (2694764)Time elapsed: 1.141 s % 292.92/41.57 % (2694764)Peak memory usage: 16 MB % 292.92/41.57 % (2694764)Instructions burned: 1368 (million) % 292.92/41.57 % (2694777)ott-21_1_sil=16000:si=on:fs=off:random_seed=2247184965:i=360:av=off:fsr=off:rtra=on_2740 on theBenchmark for (2740ds/360Mi) % 292.92/41.57 % (2694777)Instruction limit reached! % 292.92/41.57 % (2694777)------------------------------ % 292.92/41.57 % (2694777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.92/41.57 % (2694777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.92/41.57 % (2694777)CaDiCaL version: 2.1.3 % 292.92/41.57 % (2694777)Termination reason: Instruction limit % 292.92/41.57 % (2694777)Termination phase: Saturation % 292.92/41.57 % (2694777)Time elapsed: 0.281 s % 292.92/41.57 % (2694777)Peak memory usage: 13 MB % 292.92/41.57 % (2694777)Instructions burned: 360 (million) % 292.92/41.57 % (2694781)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3625003871:i=954:bd=all:rtra=on_2737 on theBenchmark for (2737ds/954Mi) % 292.92/41.57 % (2694781)Instruction limit reached! % 292.92/41.57 % (2694781)------------------------------ % 292.92/41.57 % (2694781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.92/41.57 % (2694781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.92/41.57 % (2694781)CaDiCaL version: 2.1.3 % 292.92/41.57 % (2694781)Termination reason: Instruction limit % 292.92/41.57 % (2694781)Termination phase: Saturation % 292.92/41.57 % (2694781)Time elapsed: 0.872 s % 292.92/41.57 % (2694781)Peak memory usage: 15 MB % 292.92/41.57 % (2694781)Instructions burned: 955 (million) % 292.92/41.57 % (2694791)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2496052503:fmbsr=1.3:i=1730:ins=25:rtra=on_2728 on theBenchmark for (2728ds/1730Mi) % 292.92/41.57 % Exception at run slice level % 292.92/41.57 User error: Finite model building is currenTerminated % 300.38/42.63 % Vampire exiting % 300.38/42.64 Terminated %------------------------------------------------------------------------------