%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV433^2 : TPTP v9.3.1. Released v3.6.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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 : Wed Sep 30 08:40:06 AM UTC 2026 % Result : Timeout 289.35s 41.20s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWV433^2 : TPTP v9.3.1. Released v3.6.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.27 % Computer : n006.cluster.edu % 0.25/0.27 % Model : x86_64 x86_64 % 0.25/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.25/0.27 % Memory : 8046.5625MB % 0.25/0.27 % OS : Linux 6.8.0-71-generic % 0.25/0.28 % CPULimit : 300 % 0.25/0.28 % WCLimit : 300 % 0.25/0.28 % DateTime : Tue Sep 29 16:02:55 UTC 2026 % 0.25/0.28 % CPUTime : % 0.25/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.31 Running first-order model finding % 0.25/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.24/1.60 % (911227)Will run a generic schedule for satisfiability detection. % 8.24/1.60 % (911236)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3762555943:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.24/1.60 % (911236)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.24/1.60 % (911233)% WARNING: option uhcvi not known. % 8.24/1.60 % (911232)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2400386930_2999 on theBenchmark for (2999ds/0Mi) % 8.24/1.60 % (911234)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=388785619:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.24/1.60 % (911233)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=368644520:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.24/1.60 % (911235)dis+10_1_sil=32000:sp=arity:random_seed=477426198:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.24/1.60 % (911237)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1430395066:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.24/1.60 % (911238)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=483521359:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.24/1.60 % (911233)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.24/1.60 % Exception at run slice level % 8.24/1.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.24/1.60 % (911233)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 8.24/1.60 % (911246)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2541043496:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.24/1.60 % (911236)Instruction limit reached! % 8.24/1.60 % (911236)------------------------------ % 8.24/1.60 % (911236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.24/1.60 % (911236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.60 % (911236)CaDiCaL version: 2.1.3 % 8.24/1.60 % (911236)Termination reason: Instruction limit % 8.24/1.60 % (911236)Termination phase: Saturation % 8.24/1.60 % (911236)Time elapsed: 0.053 s % 8.24/1.60 % (911236)Peak memory usage: 12 MB % 8.24/1.60 % (911236)Instructions burned: 118 (million) % 8.24/1.60 % Exception at run slice level % 8.24/1.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.24/1.60 % (911248)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2473262951:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.24/1.60 % (911249)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=135864209:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.24/1.60 % (911249)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.24/1.60 % (911249)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 8.24/1.60 % (911235)Instruction limit reached! % 8.24/1.60 % (911235)------------------------------ % 8.24/1.60 % (911235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.24/1.60 % (911235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.60 % (911235)CaDiCaL version: 2.1.3 % 8.24/1.60 % (911235)Termination reason: Instruction limit % 8.24/1.60 % (911235)Termination phase: Saturation % 8.24/1.60 % (911235)Time elapsed: 0.090 s % 8.24/1.60 % (911235)Peak memory usage: 12 MB % 8.24/1.60 % (911235)Instructions burned: 103 (million) % 8.24/1.60 % (911237)Instruction limit reached! % 8.24/1.60 % (911237)------------------------------ % 8.24/1.60 % (911237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.24/1.60 % (911237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.60 % (911237)CaDiCaL version: 2.1.3 % 8.24/1.60 % (911237)Termination reason: Instruction limit % 8.24/1.60 % (911237)Termination phase: Saturation % 8.24/1.60 % (911237)Time elapsed: 0.112 s % 8.24/1.60 % (911237)Peak memory usage: 12 MB % 8.24/1.60 % (911237)Instructions burned: 132 (million) % 8.24/1.60 % (911252)ott-21_1_sil=16000:fs=off:random_seed=3328970861:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.24/1.60 % (911238)Instruction limit reached! % 8.24/1.60 % (911238)------------------------------ % 31.13/5.01 % (911238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.13/5.01 % (911238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.13/5.01 % (911238)CaDiCaL version: 2.1.3 % 31.13/5.01 % (911238)Termination reason: Instruction limit % 31.13/5.01 % (911238)Termination phase: Saturation % 31.13/5.01 % (911238)Time elapsed: 0.143 s % 31.13/5.01 % (911238)Peak memory usage: 13 MB % 31.13/5.01 % (911238)Instructions burned: 159 (million) % 31.13/5.01 % (911253)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3289707677:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 31.13/5.01 % (911256)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=13738780:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 31.13/5.01 % (911248)Instruction limit reached! % 31.13/5.01 % (911248)------------------------------ % 31.13/5.01 % (911248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.13/5.01 % (911248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.13/5.01 % (911248)CaDiCaL version: 2.1.3 % 31.13/5.01 % (911248)Termination reason: Instruction limit % 31.13/5.01 % (911248)Termination phase: Saturation % 31.13/5.01 % (911248)Time elapsed: 0.121 s % 31.13/5.01 % (911248)Peak memory usage: 13 MB % 31.13/5.01 % (911248)Instructions burned: 132 (million) % 31.13/5.01 % Exception at run slice level % 31.13/5.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.13/5.01 % (911261)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3806165991:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 31.13/5.01 % (911262)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3994002484:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 31.13/5.01 % Exception at run slice level % 31.13/5.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.13/5.01 % (911266)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=1727942324: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) % 31.13/5.01 % (911252)Instruction limit reached! % 31.13/5.01 % (911252)------------------------------ % 31.13/5.01 % (911252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.13/5.01 % (911252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.13/5.01 % (911252)CaDiCaL version: 2.1.3 % 31.13/5.01 % (911252)Termination reason: Instruction limit % 31.13/5.01 % (911252)Termination phase: Saturation % 31.13/5.01 % (911252)Time elapsed: 0.150 s % 31.13/5.01 % (911252)Peak memory usage: 12 MB % 31.13/5.01 % (911252)Instructions burned: 180 (million) % 31.13/5.01 % (911266)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.13/5.01 % (911268)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=957743480:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.13/5.01 % (911268)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.13/5.01 % (911249)Instruction limit reached! % 31.13/5.01 % (911249)------------------------------ % 31.13/5.01 % (911249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.13/5.01 % (911249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.13/5.01 % (911249)CaDiCaL version: 2.1.3 % 31.13/5.01 % (911249)Termination reason: Instruction limit % 31.13/5.01 % (911249)Termination phase: Saturation % 31.13/5.01 % (911249)Time elapsed: 0.308 s % 31.13/5.01 % (911249)Peak memory usage: 16 MB % 31.13/5.01 % (911249)Instructions burned: 686 (million) % 31.13/5.01 % (911270)fmb+10_1_sil=64000:random_seed=3647379916:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 31.13/5.01 % (911270)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 31.13/5.01 % Exception at run slice level % 31.13/5.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.13/5.01 % (911272)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3787202367:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 31.13/5.01 % Exception at run slice level % 31.13/5.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.13/5.01 % (911274)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3748519876:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 59.95/8.90 % Exception at run slice level % 59.95/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.95/8.90 % (911276)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3445852977:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 59.95/8.90 % (911276)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 59.95/8.90 % (911253)Instruction limit reached! % 59.95/8.90 % (911253)------------------------------ % 59.95/8.90 % (911253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.95/8.90 % (911253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.95/8.90 % (911253)CaDiCaL version: 2.1.3 % 59.95/8.90 % (911253)Termination reason: Instruction limit % 59.95/8.90 % (911253)Termination phase: Saturation % 59.95/8.90 % (911253)Time elapsed: 0.424 s % 59.95/8.90 % (911253)Peak memory usage: 14 MB % 59.95/8.90 % (911253)Instructions burned: 477 (million) % 59.95/8.90 % (911278)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=70426049:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 59.95/8.90 % (911278)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 59.95/8.90 % (911278)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 59.95/8.90 % (911266)Instruction limit reached! % 59.95/8.90 % (911266)------------------------------ % 59.95/8.90 % (911266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.95/8.90 % (911266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.95/8.90 % (911266)CaDiCaL version: 2.1.3 % 59.95/8.90 % (911266)Termination reason: Instruction limit % 59.95/8.90 % (911266)Termination phase: Saturation % 59.95/8.90 % (911266)Time elapsed: 0.579 s % 59.95/8.90 % (911266)Peak memory usage: 18 MB % 59.95/8.90 % (911266)Instructions burned: 692 (million) % 59.95/8.90 % (911284)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4188987964:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 59.95/8.90 % Exception at run slice level % 59.95/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.95/8.90 % (911286)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=245506910:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 59.95/8.90 % Exception at run slice level % 59.95/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.95/8.90 % (911288)ott-2_1_sil=16000:newcnf=on:random_seed=1628973091:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 59.95/8.90 % (911288)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 59.95/8.90 % (911268)Instruction limit reached! % 59.95/8.90 % (911268)------------------------------ % 59.95/8.90 % (911268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.95/8.90 % (911268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.95/8.90 % (911268)CaDiCaL version: 2.1.3 % 59.95/8.90 % (911268)Termination reason: Instruction limit % 59.95/8.90 % (911268)Termination phase: Saturation % 59.95/8.90 % (911268)Time elapsed: 0.754 s % 59.95/8.90 % (911268)Peak memory usage: 16 MB % 59.95/8.90 % (911268)Instructions burned: 879 (million) % 59.95/8.90 % (911290)ott+10_1_sil=32000:tgt=ground:random_seed=61636516:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 59.95/8.90 % (911261)Instruction limit reached! % 59.95/8.90 % (911261)------------------------------ % 59.95/8.90 % (911261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.95/8.90 % (911261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.95/8.90 % (911261)CaDiCaL version: 2.1.3 % 59.95/8.90 % (911261)Termination reason: Instruction limit % 59.95/8.90 % (911261)Termination phase: Saturation % 59.95/8.90 % (911261)Time elapsed: 0.955 s % 59.95/8.90 % (911261)Peak memory usage: 15 MB % 59.95/8.90 % (911261)Instructions burned: 1179 (million) % 59.95/8.90 % (911292)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1869955354:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 59.95/8.90 % Exception at run slice level % 59.95/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.95/8.90 % (911294)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1346574423:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 182.86/26.07 % (911294)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 182.86/26.07 % (911288)Instruction limit reached! % 182.86/26.07 % (911288)------------------------------ % 182.86/26.07 % (911288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.86/26.07 % (911288)CaDiCaL version: 2.1.3 % 182.86/26.07 % (911288)Termination reason: Instruction limit % 182.86/26.07 % (911288)Termination phase: Saturation % 182.86/26.07 % (911288)Time elapsed: 0.716 s % 182.86/26.07 % (911288)Peak memory usage: 15 MB % 182.86/26.07 % (911288)Instructions burned: 869 (million) % 182.86/26.07 % (911296)dis+21_1_sil=32000:sas=cadical:random_seed=3349890494:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 182.86/26.07 % (911278)Instruction limit reached! % 182.86/26.07 % (911278)------------------------------ % 182.86/26.07 % (911278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.86/26.07 % (911278)CaDiCaL version: 2.1.3 % 182.86/26.07 % (911278)Termination reason: Instruction limit % 182.86/26.07 % (911278)Termination phase: Saturation % 182.86/26.07 % (911278)Time elapsed: 1.277 s % 182.86/26.07 % (911278)Peak memory usage: 18 MB % 182.86/26.07 % (911278)Instructions burned: 1472 (million) % 182.86/26.07 % (911300)ott+11_1_sil=16000:gs=on:random_seed=1815980906:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 182.86/26.07 % (911300)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 182.86/26.07 % (911276)Instruction limit reached! % 182.86/26.07 % (911276)------------------------------ % 182.86/26.07 % (911276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.86/26.07 % (911276)CaDiCaL version: 2.1.3 % 182.86/26.07 % (911276)Termination reason: Instruction limit % 182.86/26.07 % (911276)Termination phase: Saturation % 182.86/26.07 % (911276)Time elapsed: 2.113 s % 182.86/26.07 % (911276)Peak memory usage: 20 MB % 182.86/26.07 % (911276)Instructions burned: 5132 (million) % 182.86/26.07 % (911305)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=951149302:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 182.86/26.07 % Exception at run slice level % 182.86/26.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.86/26.07 % (911309)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=887119604:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 182.86/26.07 % (911300)Instruction limit reached! % 182.86/26.07 % (911300)------------------------------ % 182.86/26.07 % (911300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.86/26.07 % (911300)CaDiCaL version: 2.1.3 % 182.86/26.07 % (911300)Termination reason: Instruction limit % 182.86/26.07 % (911300)Termination phase: Saturation % 182.86/26.07 % (911300)Time elapsed: 1.765 s % 182.86/26.07 % (911300)Peak memory usage: 16 MB % 182.86/26.07 % (911300)Instructions burned: 2252 (million) % 182.86/26.07 % (911328)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2054042620:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 182.86/26.07 % (911294)Instruction limit reached! % 182.86/26.07 % (911294)------------------------------ % 182.86/26.07 % (911294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.86/26.07 % (911294)CaDiCaL version: 2.1.3 % 182.86/26.07 % (911294)Termination reason: Instruction limit % 182.86/26.07 % (911294)Termination phase: Saturation % 182.86/26.07 % (911294)Time elapsed: 2.687 s % 182.86/26.07 % (911294)Peak memory usage: 17 MB % 182.86/26.07 % (911294)Instructions burned: 3512 (million) % 182.86/26.07 % (911330)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4105962023:i=5211_2960 on theBenchmark for (2960ds/5211Mi) % 182.86/26.07 % (911296)Instruction limit reached! % 182.86/26.07 % (911296)------------------------------ % 182.86/26.07 % (911296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.86/26.07 % (911296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.49/31.97 % (911296)CaDiCaL version: 2.1.3 % 224.49/31.97 % (911296)Termination reason: Instruction limit % 224.49/31.97 % (911296)Termination phase: Saturation % 224.49/31.97 % (911296)Time elapsed: 2.946 s % 224.49/31.97 % (911296)Peak memory usage: 19 MB % 224.49/31.97 % (911296)Instructions burned: 3774 (million) % 224.49/31.97 % (911332)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1373899086:i=5497:nm=2_2953 on theBenchmark for (2953ds/5497Mi) % 224.49/31.97 % (911309)Instruction limit reached! % 224.49/31.97 % (911309)------------------------------ % 224.49/31.97 % (911309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.49/31.97 % (911309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.49/31.97 % (911309)CaDiCaL version: 2.1.3 % 224.49/31.97 % (911309)Termination reason: Instruction limit % 224.49/31.97 % (911309)Termination phase: Saturation % 224.49/31.97 % (911309)Time elapsed: 2.056 s % 224.49/31.97 % (911309)Peak memory usage: 28 MB % 224.49/31.97 % (911309)Instructions burned: 4592 (million) % 224.49/31.97 % Exception at run slice level % 224.49/31.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.49/31.97 % (911290)Instruction limit reached! % 224.49/31.97 % (911290)------------------------------ % 224.49/31.97 % (911290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.49/31.97 % (911290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.49/31.97 % (911290)CaDiCaL version: 2.1.3 % 224.49/31.97 % (911290)Termination reason: Instruction limit % 224.49/31.97 % (911290)Termination phase: Saturation % 224.49/31.97 % (911290)Time elapsed: 3.624 s % 224.49/31.97 % (911290)Peak memory usage: 22 MB % 224.49/31.97 % (911290)Instructions burned: 5114 (million) % 224.49/31.97 % (911335)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1471400905:i=14071_2952 on theBenchmark for (2952ds/14071Mi) % 224.49/31.97 % Exception at run slice level % 224.49/31.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.49/31.97 % (911334)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=32234219:fmbsr=2:i=46332_2952 on theBenchmark for (2952ds/46332Mi) % 224.49/31.97 % Exception at run slice level % 224.49/31.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.49/31.97 % (911336)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2055223556:i=22565:add=on:rawr=on_2952 on theBenchmark for (2952ds/22565Mi) % 224.49/31.97 % (911338)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1638047467:i=8173:av=off_2952 on theBenchmark for (2952ds/8173Mi) % 224.49/31.97 % (911340)dis+10_16:1_sil=16000:random_seed=591720966:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi) % 224.49/31.97 % (911330)Instruction limit reached! % 224.49/31.97 % (911330)------------------------------ % 224.49/31.97 % (911330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.49/31.97 % (911330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.49/31.97 % (911330)CaDiCaL version: 2.1.3 % 224.49/31.97 % (911330)Termination reason: Instruction limit % 224.49/31.97 % (911330)Termination phase: Saturation % 224.49/31.97 % (911330)Time elapsed: 4.161 s % 224.49/31.97 % (911330)Peak memory usage: 28 MB % 224.49/31.97 % (911330)Instructions burned: 5211 (million) % 224.49/31.97 % (911346)ott-3_8_sil=64000:random_seed=4023740213:i=20139:bs=on_2918 on theBenchmark for (2918ds/20139Mi) % 224.49/31.97 % (911340)Instruction limit reached! % 224.49/31.97 % (911340)------------------------------ % 224.49/31.97 % (911340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.49/31.97 % (911340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.49/31.97 % (911340)CaDiCaL version: 2.1.3 % 224.49/31.97 % (911340)Termination reason: Instruction limit % 224.49/31.97 % (911340)Termination phase: Saturation % 224.49/31.97 % (911340)Time elapsed: 3.730 s % 224.49/31.97 % (911340)Peak memory usage: 25 MB % 224.49/31.97 % (911340)Instructions burned: 9158 (million) % 224.49/31.97 % (911348)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=972296557:fmbsr=2:i=32576_2914 on theBenchmark for (2914ds/32576Mi) % 224.49/31.97 % Exception at run slice level % 224.49/31.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.49/31.97 % (911350)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3970526533:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 240.89/34.24 % (911338)Instruction limit reached! % 240.89/34.24 % (911338)------------------------------ % 240.89/34.24 % (911338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911338)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911338)Termination reason: Instruction limit % 240.89/34.24 % (911338)Termination phase: Saturation % 240.89/34.24 % (911338)Time elapsed: 6.425 s % 240.89/34.24 % (911338)Peak memory usage: 28 MB % 240.89/34.24 % (911338)Instructions burned: 8173 (million) % 240.89/34.24 % (911360)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3789722832:i=14134_2887 on theBenchmark for (2887ds/14134Mi) % 240.89/34.24 % (911360)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 240.89/34.24 % (911346)Instruction limit reached! % 240.89/34.24 % (911346)------------------------------ % 240.89/34.24 % (911346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911346)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911346)Termination reason: Instruction limit % 240.89/34.24 % (911346)Termination phase: Saturation % 240.89/34.24 % (911346)Time elapsed: 8.396 s % 240.89/34.24 % (911346)Peak memory usage: 32 MB % 240.89/34.24 % (911346)Instructions burned: 20141 (million) % 240.89/34.24 % (911400)dis+33_16_sil=32000:sac=on:random_seed=1934528763:i=15851:nm=0_2834 on theBenchmark for (2834ds/15851Mi) % 240.89/34.24 % (911350)Instruction limit reached! % 240.89/34.24 % (911350)------------------------------ % 240.89/34.24 % (911350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911350)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911350)Termination reason: Instruction limit % 240.89/34.24 % (911350)Termination phase: Saturation % 240.89/34.24 % (911350)Time elapsed: 8.837 s % 240.89/34.24 % (911350)Peak memory usage: 34 MB % 240.89/34.24 % (911350)Instructions burned: 11404 (million) % 240.89/34.24 % (911402)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1664312198:avsq=on:i=17627:add=on:amm=off_2825 on theBenchmark for (2825ds/17627Mi) % 240.89/34.24 % (911360)Instruction limit reached! % 240.89/34.24 % (911360)------------------------------ % 240.89/34.24 % (911360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911360)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911360)Termination reason: Instruction limit % 240.89/34.24 % (911360)Termination phase: Saturation % 240.89/34.24 % (911360)Time elapsed: 10.822 s % 240.89/34.24 % (911360)Peak memory usage: 35 MB % 240.89/34.24 % (911360)Instructions burned: 14135 (million) % 240.89/34.24 % (911426)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3504576762:s2a=on:i=53295_2779 on theBenchmark for (2779ds/53295Mi) % 240.89/34.24 % (911400)Instruction limit reached! % 240.89/34.24 % (911400)------------------------------ % 240.89/34.24 % (911400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911400)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911400)Termination reason: Instruction limit % 240.89/34.24 % (911400)Termination phase: Saturation % 240.89/34.24 % (911400)Time elapsed: 6.682 s % 240.89/34.24 % (911400)Peak memory usage: 35 MB % 240.89/34.24 % (911400)Instructions burned: 15853 (million) % 240.89/34.24 % (911434)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2724976940:i=26857:ins=20_2767 on theBenchmark for (2767ds/26857Mi) % 240.89/34.24 % Exception at run slice level % 240.89/34.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 240.89/34.24 % (911436)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3049340190:i=28120:bs=on:fsr=off_2766 on theBenchmark for (2766ds/28120Mi) % 240.89/34.24 % (911336)Instruction limit reached! % 240.89/34.24 % (911336)------------------------------ % 240.89/34.24 % (911336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.89/34.24 % (911336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.89/34.24 % (911336)CaDiCaL version: 2.1.3 % 240.89/34.24 % (911336)Termination reason: Instruction limit % 240.89/34.24 % (911336)Termination phase: Saturation % 240.89/34.24 % (911336)Time elapsed: 20.969 s % 257.09/36.65 % (911336)Peak memory usage: 77 MB % 257.09/36.65 % (911336)Instructions burned: 22566 (million) % 257.09/36.65 % (911442)fmb+10_1_sil=256000:fmbss=7:random_seed=2971084703:fmbsr=1.6:i=182295_2742 on theBenchmark for (2742ds/182295Mi) % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911444)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4287250072:i=44625:gsp=on_2742 on theBenchmark for (2742ds/44625Mi) % 257.09/36.65 % (911444)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 257.09/36.65 % (911444)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911446)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2769511929:i=160505_2741 on theBenchmark for (2741ds/160505Mi) % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911448)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3404351631:fmbsr=1.3:i=225729_2741 on theBenchmark for (2741ds/225729Mi) % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911450)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2226367565:fmbsr=2:i=185024:ins=7_2741 on theBenchmark for (2741ds/185024Mi) % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911452)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2547319103:rtra=on_2740 on theBenchmark for (2740ds/0Mi) % 257.09/36.65 % Exception at run slice level % 257.09/36.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.09/36.65 % (911454)% WARNING: option uhcvi not known. % 257.09/36.65 % (911454)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2408433304:i=271062:add=off:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/271062Mi) % 257.09/36.65 % (911454)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 257.09/36.65 % (911454)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 257.09/36.65 % (911328)Instruction limit reached! % 257.09/36.65 % (911328)------------------------------ % 257.09/36.65 % (911328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.09/36.65 % (911328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.09/36.65 % (911328)CaDiCaL version: 2.1.3 % 257.09/36.65 % (911328)Termination reason: Instruction limit % 257.09/36.65 % (911328)Termination phase: Saturation % 257.09/36.65 % (911328)Time elapsed: 23.718 s % 257.09/36.65 % (911328)Peak memory usage: 54 MB % 257.09/36.65 % (911328)Instructions burned: 29340 (million) % 257.09/36.65 % (911456)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=879415676:i=176048:add=on:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/176048Mi) % 257.09/36.65 % (911402)Instruction limit reached! % 257.09/36.65 % (911402)------------------------------ % 257.09/36.65 % (911402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.09/36.65 % (911402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.09/36.65 % (911402)CaDiCaL version: 2.1.3 % 257.09/36.65 % (911402)Termination reason: Instruction limit % 257.09/36.65 % (911402)Termination phase: Saturation % 257.09/36.65 % (911402)Time elapsed: 14.037 s % 257.09/36.65 % (911402)Peak memory usage: 45 MB % 257.09/36.65 % (911402)Instructions burned: 17629 (million) % 257.09/36.65 % (911480)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3362670493:i=206:fgj=on:rtra=on_2685 on theBenchmark for (2685ds/206Mi) % 257.09/36.65 % (911480)Instruction limit reached! % 257.09/36.65 % (911480)------------------------------ % 257.09/36.65 % (911480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.09/36.65 % (911480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.09/36.65 % (911480)CaDiCaL version: 2.1.3 % 257.09/36.65 % (911480)Termination reason: Instruction limit % 257.09/36.65 % (911480)Termination phase: Saturation % 257.09/36.65 % (911480)Time elapsed: 0.136 s % 289.35/41.20 % (911480)Peak memory usage: 12 MB % 289.35/41.20 % (911480)Instructions burned: 206 (million) % 289.35/41.20 % (911482)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=515388072:i=232:rtra=on_2683 on theBenchmark for (2683ds/232Mi) % 289.35/41.20 % (911482)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 289.35/41.20 % (911482)Instruction limit reached! % 289.35/41.20 % (911482)------------------------------ % 289.35/41.20 % (911482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.35/41.20 % (911482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.35/41.20 % (911482)CaDiCaL version: 2.1.3 % 289.35/41.20 % (911482)Termination reason: Instruction limit % 289.35/41.20 % (911482)Termination phase: Saturation % 289.35/41.20 % (911482)Time elapsed: 0.203 s % 289.35/41.20 % (911482)Peak memory usage: 13 MB % 289.35/41.20 % (911482)Instructions burned: 232 (million) % 289.35/41.20 % (911484)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1565691407:i=262:rtra=on_2681 on theBenchmark for (2681ds/262Mi) % 289.35/41.20 % (911484)Instruction limit reached! % 289.35/41.20 % (911484)------------------------------ % 289.35/41.20 % (911484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.35/41.20 % (911484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.35/41.20 % (911484)CaDiCaL version: 2.1.3 % 289.35/41.20 % (911484)Termination reason: Instruction limit % 289.35/41.20 % (911484)Termination phase: Saturation % 289.35/41.20 % (911484)Time elapsed: 0.169 s % 289.35/41.20 % (911484)Peak memory usage: 13 MB % 289.35/41.20 % (911484)Instructions burned: 264 (million) % 289.35/41.20 % (911486)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=536499378:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2679 on theBenchmark for (2679ds/318Mi) % 289.35/41.20 % (911486)Instruction limit reached! % 289.35/41.20 % (911486)------------------------------ % 289.35/41.20 % (911486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.35/41.20 % (911486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.35/41.20 % (911486)CaDiCaL version: 2.1.3 % 289.35/41.20 % (911486)Termination reason: Instruction limit % 289.35/41.20 % (911486)Termination phase: Saturation % 289.35/41.20 % (911486)Time elapsed: 0.298 s % 289.35/41.20 % (911486)Peak memory usage: 14 MB % 289.35/41.20 % (911486)Instructions burned: 319 (million) % 289.35/41.20 % (911488)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3192797336:i=1428:nm=2:rtra=on_2676 on theBenchmark for (2676ds/1428Mi) % 289.35/41.20 % Exception at run slice level % 289.35/41.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 289.35/41.20 % (911490)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1061960433:i=262:bd=preordered:rtra=on:fsd=on_2675 on theBenchmark for (2675ds/262Mi) % 289.35/41.20 % (911490)Instruction limit reached! % 289.35/41.20 % (911490)------------------------------ % 289.35/41.20 % (911490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.35/41.20 % (911490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.35/41.20 % (911490)CaDiCaL version: 2.1.3 % 289.35/41.20 % (911490)Termination reason: Instruction limit % 289.35/41.20 % (911490)Termination phase: Saturation % 289.35/41.20 % (911490)Time elapsed: 0.226 s % 289.35/41.20 % (911490)Peak memory usage: 13 MB % 289.35/41.20 % (911490)Instructions burned: 262 (million) % 289.35/41.20 % (911492)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=2211209460:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2673 on theBenchmark for (2673ds/1368Mi) % 289.35/41.20 % (911492)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 289.35/41.20 % (911492)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 289.35/41.20 % (911492)Instruction limit reached! % 289.35/41.20 % (911492)------------------------------ % 289.35/41.20 % (911492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.35/41.20 % (911492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.35/41.20 % (911492)CaDiCaL version: 2.1.3 % 289.35/41.20 % (911492)Termination reason: Instruction limit % 289.35/41.20 % (911492)Termination phase: Saturation % 289.35/41.20 % (911492)Time elapsed: 1.170 s % 289.35/41.20 % (911492)Peak memory usage: 17 MB % 289.35/41.20 % (911492)Instructions burned: 1369 (million) % 289.35/41.20 % (911436)Instruction limit reached! % 300.47/42.74 % (911436)------------------------------ % 300.47/42.74 % (911436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.74 % (911436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.74 % (911436)CaDiCaL version: 2.1.3 % 300.47/42.74 % (911436)Termination reason: Instruction limit % 300.47/42.74 % (911436)Termination phase: Saturation % 300.47/42.74 % (911436)Time elapsed: 10.579 s % 300.47/42.74 % (911436)Peak memory usage: 39 MB % 300.47/42.74 % (911436)Instructions burned: 28123 (million) % 300.47/42.74 % (911495)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2260158959:i=954:bd=all:rtra=on_2660 on theBenchmark for (2660ds/954Mi) % 300.47/42.74 % (911494)ott-21_1_sil=16000:si=on:fs=off:random_seed=3667929575:i=360:av=off:fsr=off:rtra=on_2660 on theBenchmark for (2660ds/360Mi) % 300.47/42.74 % (911494)Instruction limit reached! % 300.47/42.74 % (911494)------------------------------ % 300.47/42.74 % (911494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.74 % (911494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.74 % (911494)CaDiCaL version: 2.1.3 % 300.47/42.74 % (911494)Termination reason: Instruction limit % 300.47/42.74 % (911494)Termination phase: Saturation % 300.47/42.74 % (911494)Time elapsed: 0.304 s % 300.47/42.74 % (911494)Peak memory usage: 12 MB % 300.47/42.74 % (911494)Instructions burned: 360 (million) % 300.47/42.74 % (911499)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3742351364:fmbsr=1.3:i=1730:ins=25:rtra=on_2653 on theBenchmark for (2653ds/1730Mi) % 300.47/42.74 % Exception at run slice level % 300.47/42.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.47/42.74 % (911501)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=808100293:i=2358:rtra=on_2652 on theBenchmark for (2652ds/2358Mi) % 300.47/42.74 % (911495)Instruction limit reached! % 300.47/42.74 % (911495)------------------------------ % 300.47/42.74 % (911495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.74 % (911495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.74 % (911495)CaDiCaL version: 2.1.3 % 300.47/42.74 % (911495)Termination reason: Instruction limit % 300.47/42.74 % (911495)Termination phase: Saturation % 300.47/42.74 % (911495)Time elapsed: 0.461 s % 300.47/42.74 % (911495)Peak memory usage: 15 MB % 300.47/42.74 % (911495)Instructions burned: 955 (million) % 300.47/42.74 % (911503)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3772513924:i=1778:ins=1:rtra=on_2651 on theBenchmark for (2651ds/1778Mi) % 300.47/42.74 % Exception at run slice level % 300.47/42.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.47/42.74 % (911505)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=3772699094:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2651 on theBenchmark for (2651ds/1384Mi) % 300.47/42.74 % (911505)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 300.47/42.74 % (911505)Instruction limit reached! % 300.47/42.74 % (911505)------------------------------ % 300.47/42.74 % (911505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.74 % (911505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.74 % (911505)CaDiCaL version: 2.1.3 % 300.47/42.74 % (911505)Termination reason: Instruction limit % 300.47/42.74 % (911505)Termination phase: Saturation % 300.47/42.74 % (911505)Time elapsed: 0.615 s % 300.47/42.74 % (911505)Peak memory usage: 23 MB % 300.47/42.74 % (911505)Instructions burned: 1384 (million) % 300.47/42.74 % (911507)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2678432079:i=1758:kws=inv_precedence:fsr=off:rtra=on_2645 on theBenchmark for (2645ds/1758Mi) % 300.47/42.74 % (911507)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 300.47/42.74 % (911507)Instruction limit reached! % 300.47/42.74 % (911507)------------------------------ % 300.47/42.74 % (911507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.74 % (911507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.74 % (911507)CaDiCaL version: 2.1.3 % 300.47/42.74 % (911507)Termination reason: Instruction limit % 300.47/42.74 % (911507)Termination phase: Saturation % 300.47/42.74 % (911507)Time elapsed: 0. % 300.47/42.74 Terminated % 300.47/42.74 % Vampire exiting %------------------------------------------------------------------------------