%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM072_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 : n002.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:15 AM UTC 2026 % Result : Timeout 300.31s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : COM072_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n002.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 21:55:22 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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 % 8.61/1.66 % (812333)Will run a generic schedule for satisfiability detection. % 8.61/1.66 % (812338)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=918529256_2999 on theBenchmark for (2999ds/0Mi) % 8.61/1.66 % (812339)% WARNING: option uhcvi not known. % 8.61/1.66 % Exception at run slice level % 8.61/1.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.61/1.66 % (812342)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3332240640:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.61/1.66 % (812340)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3971871128:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.61/1.66 % (812339)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4261252683:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.61/1.66 % (812341)dis+10_1_sil=32000:sp=arity:random_seed=375324194:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.61/1.66 % (812343)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1501786203:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.61/1.66 % (812344)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=989895207:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.61/1.66 % (812350)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3582786491:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.61/1.66 % Exception at run slice level % 8.61/1.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.61/1.66 % (812343)Instruction limit reached! % 8.61/1.66 % (812343)------------------------------ % 8.61/1.66 % (812343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.66 % (812343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.66 % (812343)CaDiCaL version: 2.1.3 % 8.61/1.66 % (812343)Termination reason: Instruction limit % 8.61/1.66 % (812343)Termination phase: Saturation % 8.61/1.66 % (812343)Time elapsed: 0.043 s % 8.61/1.66 % (812343)Peak memory usage: 12 MB % 8.61/1.66 % (812343)Instructions burned: 139 (million) % 8.61/1.66 % (812354)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3524029120:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.61/1.66 % (812341)Instruction limit reached! % 8.61/1.66 % (812341)------------------------------ % 8.61/1.66 % (812341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.66 % (812341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.66 % (812341)CaDiCaL version: 2.1.3 % 8.61/1.66 % (812341)Termination reason: Instruction limit % 8.61/1.66 % (812341)Termination phase: Saturation % 8.61/1.66 % (812341)Time elapsed: 0.055 s % 8.61/1.66 % (812341)Peak memory usage: 12 MB % 8.61/1.66 % (812341)Instructions burned: 105 (million) % 8.61/1.66 % (812342)Instruction limit reached! % 8.61/1.66 % (812342)------------------------------ % 8.61/1.66 % (812342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.66 % (812342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.66 % (812342)CaDiCaL version: 2.1.3 % 8.61/1.66 % (812342)Termination reason: Instruction limit % 8.61/1.66 % (812342)Termination phase: Saturation % 8.61/1.66 % (812342)Time elapsed: 0.058 s % 8.61/1.66 % (812342)Peak memory usage: 12 MB % 8.61/1.66 % (812342)Instructions burned: 117 (million) % 8.61/1.66 % (812355)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=1137552108:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.61/1.66 % (812357)ott-21_1_sil=16000:fs=off:random_seed=956528252:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.61/1.66 % (812358)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=534213231:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.61/1.66 % (812344)Instruction limit reached! % 8.61/1.66 % (812344)------------------------------ % 8.61/1.66 % (812344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.66 % (812344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.66 % (812344)CaDiCaL version: 2.1.3 % 8.61/1.66 % (812344)Termination reason: Instruction limit % 8.61/1.66 % (812344)Termination phase: Saturation % 8.61/1.66 % (812344)Time elapsed: 0.098 s % 8.61/1.66 % (812344)Peak memory usage: 12 MB % 30.74/4.63 % (812344)Instructions burned: 159 (million) % 30.74/4.63 % (812362)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=145943566:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 30.74/4.63 % (812354)Instruction limit reached! % 30.74/4.63 % (812354)------------------------------ % 30.74/4.63 % (812354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.74/4.63 % (812354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/4.63 % (812354)CaDiCaL version: 2.1.3 % 30.74/4.63 % (812354)Termination reason: Instruction limit % 30.74/4.63 % (812354)Termination phase: Saturation % 30.74/4.63 % (812354)Time elapsed: 0.084 s % 30.74/4.63 % (812354)Peak memory usage: 13 MB % 30.74/4.63 % (812354)Instructions burned: 132 (million) % 30.74/4.63 % Exception at run slice level % 30.74/4.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.74/4.63 % (812364)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1762733999:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 30.74/4.63 % (812365)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1732435814:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 30.74/4.63 % (812357)Instruction limit reached! % 30.74/4.63 % (812357)------------------------------ % 30.74/4.63 % (812357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.74/4.63 % (812357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/4.63 % (812357)CaDiCaL version: 2.1.3 % 30.74/4.63 % (812357)Termination reason: Instruction limit % 30.74/4.63 % (812357)Termination phase: Saturation % 30.74/4.63 % (812357)Time elapsed: 0.088 s % 30.74/4.63 % (812357)Peak memory usage: 12 MB % 30.74/4.63 % (812357)Instructions burned: 182 (million) % 30.74/4.63 % Exception at run slice level % 30.74/4.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.74/4.63 % (812368)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=27922540: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) % 30.74/4.63 % (812369)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2574196160:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 30.74/4.63 % (812355)Instruction limit reached! % 30.74/4.63 % (812355)------------------------------ % 30.74/4.63 % (812355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.74/4.63 % (812355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/4.63 % (812355)CaDiCaL version: 2.1.3 % 30.74/4.63 % (812355)Termination reason: Instruction limit % 30.74/4.63 % (812355)Termination phase: Saturation % 30.74/4.63 % (812355)Time elapsed: 0.179 s % 30.74/4.63 % (812355)Peak memory usage: 14 MB % 30.74/4.63 % (812355)Instructions burned: 687 (million) % 30.74/4.63 % (812374)fmb+10_1_sil=64000:random_seed=3430104132:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 30.74/4.63 % (812374)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 30.74/4.63 % Exception at run slice level % 30.74/4.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.74/4.63 % (812386)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3959143682:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 30.74/4.63 % Exception at run slice level % 30.74/4.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.74/4.63 % (812393)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2395659478:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 30.74/4.63 % Exception at run slice level % 30.74/4.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.74/4.63 % (812403)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3077932:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 30.74/4.63 % (812358)Instruction limit reached! % 30.74/4.63 % (812358)------------------------------ % 30.74/4.63 % (812358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.74/4.63 % (812358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/4.63 % (812358)CaDiCaL version: 2.1.3 % 30.74/4.63 % (812358)Termination reason: Instruction limit % 30.74/4.63 % (812358)Termination phase: Saturation % 103.40/14.88 % (812358)Time elapsed: 0.291 s % 103.40/14.88 % (812358)Peak memory usage: 13 MB % 103.40/14.88 % (812358)Instructions burned: 478 (million) % 103.40/14.88 % (812429)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1674517829:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 103.40/14.88 % (812429)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 103.40/14.88 % (812369)Instruction limit reached! % 103.40/14.88 % (812369)------------------------------ % 103.40/14.88 % (812369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.40/14.88 % (812369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.40/14.88 % (812369)CaDiCaL version: 2.1.3 % 103.40/14.88 % (812369)Termination reason: Instruction limit % 103.40/14.88 % (812369)Termination phase: Saturation % 103.40/14.88 % (812369)Time elapsed: 0.321 s % 103.40/14.88 % (812369)Peak memory usage: 18 MB % 103.40/14.88 % (812369)Instructions burned: 879 (million) % 103.40/14.88 % (812466)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=464316174:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 103.40/14.89 % Exception at run slice level % 103.40/14.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.40/14.89 % (812473)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1921640500:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 103.40/14.89 % Exception at run slice level % 103.40/14.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.40/14.89 % (812482)ott-2_1_sil=16000:newcnf=on:random_seed=951092825:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 103.40/14.89 % (812368)Instruction limit reached! % 103.40/14.89 % (812368)------------------------------ % 103.40/14.89 % (812368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.40/14.89 % (812368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.40/14.89 % (812368)CaDiCaL version: 2.1.3 % 103.40/14.89 % (812368)Termination reason: Instruction limit % 103.40/14.89 % (812368)Termination phase: Saturation % 103.40/14.89 % (812368)Time elapsed: 0.391 s % 103.40/14.89 % (812368)Peak memory usage: 17 MB % 103.40/14.89 % (812368)Instructions burned: 692 (million) % 103.40/14.89 % (812491)ott+10_1_sil=32000:tgt=ground:random_seed=1486989871:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 103.40/14.89 % (812482)Instruction limit reached! % 103.40/14.89 % (812482)------------------------------ % 103.40/14.89 % (812482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.40/14.89 % (812482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.40/14.89 % (812482)CaDiCaL version: 2.1.3 % 103.40/14.89 % (812482)Termination reason: Instruction limit % 103.40/14.89 % (812482)Termination phase: Saturation % 103.40/14.89 % (812482)Time elapsed: 0.216 s % 103.40/14.89 % (812482)Peak memory usage: 13 MB % 103.40/14.89 % (812482)Instructions burned: 871 (million) % 103.40/14.89 % (812535)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2370545026:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 103.40/14.89 % Exception at run slice level % 103.40/14.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.40/14.89 % (812539)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=605973335:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 103.40/14.89 % (812364)Instruction limit reached! % 103.40/14.89 % (812364)------------------------------ % 103.40/14.89 % (812364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.40/14.89 % (812364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.40/14.89 % (812364)CaDiCaL version: 2.1.3 % 103.40/14.89 % (812364)Termination reason: Instruction limit % 103.40/14.89 % (812364)Termination phase: Saturation % 103.40/14.89 % (812364)Time elapsed: 0.697 s % 103.40/14.89 % (812364)Peak memory usage: 18 MB % 103.40/14.89 % (812364)Instructions burned: 1180 (million) % 103.40/14.89 % (812545)dis+21_1_sil=32000:sas=cadical:random_seed=2556920482:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 103.40/14.89 % (812429)Instruction limit reached! % 103.40/14.89 % (812429)------------------------------ % 103.40/14.89 % (812429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.40/14.89 % (812429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.40/14.89 % (812429)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812429)Termination reason: Instruction limit % 175.29/24.99 % (812429)Termination phase: Saturation % 175.29/24.99 % (812429)Time elapsed: 1.015 s % 175.29/24.99 % (812429)Peak memory usage: 17 MB % 175.29/24.99 % (812429)Instructions burned: 1472 (million) % 175.29/24.99 % (812567)ott+11_1_sil=16000:gs=on:random_seed=3153149318:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 175.29/24.99 % (812539)Instruction limit reached! % 175.29/24.99 % (812539)------------------------------ % 175.29/24.99 % (812539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.29/24.99 % (812539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.29/24.99 % (812539)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812539)Termination reason: Instruction limit % 175.29/24.99 % (812539)Termination phase: Saturation % 175.29/24.99 % (812539)Time elapsed: 1.524 s % 175.29/24.99 % (812539)Peak memory usage: 26 MB % 175.29/24.99 % (812539)Instructions burned: 3514 (million) % 175.29/24.99 % (812586)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1226645383:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 175.29/24.99 % Exception at run slice level % 175.29/24.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 175.29/24.99 % (812588)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1174377243:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 175.29/24.99 % (812567)Instruction limit reached! % 175.29/24.99 % (812567)------------------------------ % 175.29/24.99 % (812567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.29/24.99 % (812567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.29/24.99 % (812567)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812567)Termination reason: Instruction limit % 175.29/24.99 % (812567)Termination phase: Saturation % 175.29/24.99 % (812567)Time elapsed: 1.919 s % 175.29/24.99 % (812567)Peak memory usage: 18 MB % 175.29/24.99 % (812567)Instructions burned: 2251 (million) % 175.29/24.99 % (812592)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2747991124:i=29340_2965 on theBenchmark for (2965ds/29340Mi) % 175.29/24.99 % (812545)Instruction limit reached! % 175.29/24.99 % (812545)------------------------------ % 175.29/24.99 % (812545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.29/24.99 % (812545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.29/24.99 % (812545)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812545)Termination reason: Instruction limit % 175.29/24.99 % (812545)Termination phase: Saturation % 175.29/24.99 % (812545)Time elapsed: 3.287 s % 175.29/24.99 % (812545)Peak memory usage: 26 MB % 175.29/24.99 % (812545)Instructions burned: 3773 (million) % 175.29/24.99 % (812601)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=408528364:i=5211_2957 on theBenchmark for (2957ds/5211Mi) % 175.29/24.99 % (812403)Instruction limit reached! % 175.29/24.99 % (812403)------------------------------ % 175.29/24.99 % (812403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.29/24.99 % (812403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.29/24.99 % (812403)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812403)Termination reason: Instruction limit % 175.29/24.99 % (812403)Termination phase: Saturation % 175.29/24.99 % (812403)Time elapsed: 3.989 s % 175.29/24.99 % (812403)Peak memory usage: 23 MB % 175.29/24.99 % (812403)Instructions burned: 5132 (million) % 175.29/24.99 % (812588)Instruction limit reached! % 175.29/24.99 % (812588)------------------------------ % 175.29/24.99 % (812588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.29/24.99 % (812588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.29/24.99 % (812588)CaDiCaL version: 2.1.3 % 175.29/24.99 % (812588)Termination reason: Instruction limit % 175.29/24.99 % (812588)Termination phase: Saturation % 175.29/24.99 % (812588)Time elapsed: 1.954 s % 175.29/24.99 % (812588)Peak memory usage: 21 MB % 175.29/24.99 % (812588)Instructions burned: 4593 (million) % 175.29/24.99 % (812603)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3634854521:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi) % 175.29/24.99 % Exception at run slice level % 175.29/24.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 175.29/24.99 % (812604)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2118952457:fmbsr=2:i=46332_2956 on theBenchmark for (2956ds/46332Mi) % 236.17/33.55 % Exception at run slice level % 236.17/33.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.17/33.55 % (812607)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3737893862:i=14071_2955 on theBenchmark for (2955ds/14071Mi) % 236.17/33.55 % (812608)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=651580060:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 236.17/33.55 % Exception at run slice level % 236.17/33.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.17/33.55 % (812611)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=891510332:i=8173:av=off_2955 on theBenchmark for (2955ds/8173Mi) % 236.17/33.55 % (812491)Instruction limit reached! % 236.17/33.55 % (812491)------------------------------ % 236.17/33.55 % (812491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.17/33.55 % (812491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.17/33.55 % (812491)CaDiCaL version: 2.1.3 % 236.17/33.55 % (812491)Termination reason: Instruction limit % 236.17/33.55 % (812491)Termination phase: Saturation % 236.17/33.55 % (812491)Time elapsed: 4.190 s % 236.17/33.55 % (812491)Peak memory usage: 18 MB % 236.17/33.55 % (812491)Instructions burned: 5115 (million) % 236.17/33.55 % (812613)dis+10_16:1_sil=16000:random_seed=555693874:i=9155:fsr=off_2951 on theBenchmark for (2951ds/9155Mi) % 236.17/33.55 % (812601)Instruction limit reached! % 236.17/33.55 % (812601)------------------------------ % 236.17/33.55 % (812601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.17/33.55 % (812601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.17/33.55 % (812601)CaDiCaL version: 2.1.3 % 236.17/33.55 % (812601)Termination reason: Instruction limit % 236.17/33.55 % (812601)Termination phase: Saturation % 236.17/33.55 % (812601)Time elapsed: 2.446 s % 236.17/33.55 % (812601)Peak memory usage: 42 MB % 236.17/33.55 % (812601)Instructions burned: 5211 (million) % 236.17/33.55 % (812627)ott-3_8_sil=64000:random_seed=1376213358:i=20139:bs=on_2932 on theBenchmark for (2932ds/20139Mi) % 236.17/33.55 % (812611)Instruction limit reached! % 236.17/33.55 % (812611)------------------------------ % 236.17/33.55 % (812611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.17/33.55 % (812611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.17/33.55 % (812611)CaDiCaL version: 2.1.3 % 236.17/33.55 % (812611)Termination reason: Instruction limit % 236.17/33.55 % (812611)Termination phase: Saturation % 236.17/33.55 % (812611)Time elapsed: 6.305 s % 236.17/33.55 % (812611)Peak memory usage: 19 MB % 236.17/33.55 % (812611)Instructions burned: 8174 (million) % 236.17/33.55 % (812633)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2071133500:fmbsr=2:i=32576_2891 on theBenchmark for (2891ds/32576Mi) % 236.17/33.55 % Exception at run slice level % 236.17/33.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.17/33.55 % (812635)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2452667169:i=11404_2891 on theBenchmark for (2891ds/11404Mi) % 236.17/33.55 % (812613)Instruction limit reached! % 236.17/33.55 % (812613)------------------------------ % 236.17/33.55 % (812613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.17/33.55 % (812613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.17/33.55 % (812613)CaDiCaL version: 2.1.3 % 236.17/33.55 % (812613)Termination reason: Instruction limit % 236.17/33.55 % (812613)Termination phase: Saturation % 236.17/33.55 % (812613)Time elapsed: 8.397 s % 236.17/33.55 % (812613)Peak memory usage: 54 MB % 236.17/33.55 % (812613)Instructions burned: 9156 (million) % 236.17/33.55 % (812641)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=426361677:i=14134_2867 on theBenchmark for (2867ds/14134Mi) % 236.17/33.55 % (812627)Instruction limit reached! % 236.17/33.55 % (812627)------------------------------ % 236.17/33.55 % (812627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.17/33.55 % (812627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.17/33.55 % (812627)CaDiCaL version: 2.1.3 % 236.17/33.55 % (812627)Termination reason: Instruction limit % 236.17/33.55 % (812627)Termination phase: Saturation % 236.17/33.55 % (812627)Time elapsed: 7.907 s % 236.17/33.55 % (812627)Peak memory usage: 27 MB % 236.17/33.55 % (812627)Instructions burned: 20141 (million) % 236.17/33.55 % (812643)dis+33_16_sil=32000:sac=on:random_seed=2896412877:i=15851:nm=0_2853 on theBenchmark for (2853ds/15851Mi) % 268.63/38.05 % (812608)Instruction limit reached! % 268.63/38.05 % (812608)------------------------------ % 268.63/38.05 % (812608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.63/38.05 % (812608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.63/38.05 % (812608)CaDiCaL version: 2.1.3 % 268.63/38.05 % (812608)Termination reason: Instruction limit % 268.63/38.05 % (812608)Termination phase: Saturation % 268.63/38.05 % (812608)Time elapsed: 14.437 s % 268.63/38.05 % (812608)Peak memory usage: 24 MB % 268.63/38.05 % (812608)Instructions burned: 22565 (million) % 268.63/38.05 % (812649)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=519497787:avsq=on:i=17627:add=on:amm=off_2810 on theBenchmark for (2810ds/17627Mi) % 268.63/38.05 % (812643)Instruction limit reached! % 268.63/38.05 % (812643)------------------------------ % 268.63/38.05 % (812643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.63/38.05 % (812643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.63/38.05 % (812643)CaDiCaL version: 2.1.3 % 268.63/38.05 % (812643)Termination reason: Instruction limit % 268.63/38.05 % (812643)Termination phase: Saturation % 268.63/38.05 % (812643)Time elapsed: 6.126 s % 268.63/38.05 % (812643)Peak memory usage: 21 MB % 268.63/38.05 % (812643)Instructions burned: 15852 (million) % 268.63/38.05 % (812651)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1832549318:s2a=on:i=53295_2791 on theBenchmark for (2791ds/53295Mi) % 268.63/38.05 % (812635)Instruction limit reached! % 268.63/38.05 % (812635)------------------------------ % 268.63/38.05 % (812635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.63/38.05 % (812635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.63/38.05 % (812635)CaDiCaL version: 2.1.3 % 268.63/38.05 % (812635)Termination reason: Instruction limit % 268.63/38.05 % (812635)Termination phase: Saturation % 268.63/38.05 % (812635)Time elapsed: 11.533 s % 268.63/38.05 % (812635)Peak memory usage: 122 MB % 268.63/38.05 % (812635)Instructions burned: 11404 (million) % 268.63/38.05 % (812657)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2420082928:i=26857:ins=20_2775 on theBenchmark for (2775ds/26857Mi) % 268.63/38.05 % Exception at run slice level % 268.63/38.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.63/38.05 % (812659)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=688130994:i=28120:bs=on:fsr=off_2775 on theBenchmark for (2775ds/28120Mi) % 268.63/38.05 % (812641)Instruction limit reached! % 268.63/38.05 % (812641)------------------------------ % 268.63/38.05 % (812641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.63/38.05 % (812641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.63/38.05 % (812641)CaDiCaL version: 2.1.3 % 268.63/38.05 % (812641)Termination reason: Instruction limit % 268.63/38.05 % (812641)Termination phase: Saturation % 268.63/38.05 % (812641)Time elapsed: 11.335 s % 268.63/38.05 % (812641)Peak memory usage: 29 MB % 268.63/38.05 % (812641)Instructions burned: 14135 (million) % 268.63/38.05 % (812665)fmb+10_1_sil=256000:fmbss=7:random_seed=4284058410:fmbsr=1.6:i=182295_2753 on theBenchmark for (2753ds/182295Mi) % 268.63/38.05 % Exception at run slice level % 268.63/38.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.63/38.05 % (812667)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4087888148:i=44625:gsp=on_2753 on theBenchmark for (2753ds/44625Mi) % 268.63/38.05 % (812667)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 268.63/38.05 % Exception at run slice level % 268.63/38.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.63/38.05 % (812669)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1413026323:i=160505_2753 on theBenchmark for (2753ds/160505Mi) % 268.63/38.05 % Exception at run slice level % 268.63/38.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.63/38.05 % (812671)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=13685463:fmbsr=1.3:i=225729_2752 on theBenchmark for (2752ds/225729Mi) % 268.63/38.05 % Exception at run slice level % 268.63/38.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 268.63/38.05 % (812673)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=122415414:fmbsr=2:i=185024:ins=7_2752 on theBenchmark for (2752ds/185024Mi) % 283.46/40.16 % Exception at run slice level % 283.46/40.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 283.46/40.16 % (812675)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1960142402:rtra=on_2752 on theBenchmark for (2752ds/0Mi) % 283.46/40.16 % Exception at run slice level % 283.46/40.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 283.46/40.16 % (812677)% WARNING: option uhcvi not known. % 283.46/40.16 % (812677)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3065452832:i=271062:add=off:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/271062Mi) % 283.46/40.16 % (812592)Instruction limit reached! % 283.46/40.16 % (812592)------------------------------ % 283.46/40.16 % (812592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.46/40.16 % (812592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.46/40.16 % (812592)CaDiCaL version: 2.1.3 % 283.46/40.16 % (812592)Termination reason: Instruction limit % 283.46/40.16 % (812592)Termination phase: Saturation % 283.46/40.16 % (812592)Time elapsed: 22.376 s % 283.46/40.16 % (812592)Peak memory usage: 44 MB % 283.46/40.16 % (812592)Instructions burned: 29341 (million) % 283.46/40.16 % (812693)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2352694977:i=176048:add=on:rtra=on:rawr=on_2741 on theBenchmark for (2741ds/176048Mi) % 283.46/40.16 % (812649)Instruction limit reached! % 283.46/40.16 % (812649)------------------------------ % 283.46/40.16 % (812649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.46/40.16 % (812649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.46/40.16 % (812649)CaDiCaL version: 2.1.3 % 283.46/40.16 % (812649)Termination reason: Instruction limit % 283.46/40.16 % (812649)Termination phase: Saturation % 283.46/40.16 % (812649)Time elapsed: 13.429 s % 283.46/40.16 % (812649)Peak memory usage: 34 MB % 283.46/40.16 % (812649)Instructions burned: 17628 (million) % 283.46/40.16 % (812723)dis+10_1_sil=32000:si=on:sp=arity:random_seed=618901937:i=206:fgj=on:rtra=on_2676 on theBenchmark for (2676ds/206Mi) % 283.46/40.16 % (812723)Instruction limit reached! % 283.46/40.16 % (812723)------------------------------ % 283.46/40.16 % (812723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.46/40.16 % (812723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.46/40.16 % (812723)CaDiCaL version: 2.1.3 % 283.46/40.16 % (812723)Termination reason: Instruction limit % 283.46/40.16 % (812723)Termination phase: Saturation % 283.46/40.16 % (812723)Time elapsed: 0.185 s % 283.46/40.16 % (812723)Peak memory usage: 13 MB % 283.46/40.16 % (812723)Instructions burned: 206 (million) % 283.46/40.16 % (812727)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1475030171:i=232:rtra=on_2674 on theBenchmark for (2674ds/232Mi) % 283.46/40.16 % (812727)Instruction limit reached! % 283.46/40.16 % (812727)------------------------------ % 283.46/40.16 % (812727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.46/40.16 % (812727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.46/40.16 % (812727)CaDiCaL version: 2.1.3 % 283.46/40.16 % (812727)Termination reason: Instruction limit % 283.46/40.16 % (812727)Termination phase: Saturation % 283.46/40.16 % (812727)Time elapsed: 0.220 s % 283.46/40.16 % (812727)Peak memory usage: 13 MB % 283.46/40.16 % (812727)Instructions burned: 232 (million) % 283.46/40.16 % (812729)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1530723486:i=262:rtra=on_2671 on theBenchmark for (2671ds/262Mi) % 283.46/40.16 % (812729)Instruction limit reached! % 283.46/40.16 % (812729)------------------------------ % 283.46/40.16 % (812729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.46/40.16 % (812729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.46/40.16 % (812729)CaDiCaL version: 2.1.3 % 283.46/40.16 % (812729)Termination reason: Instruction limit % 283.46/40.16 % (812729)Termination phase: Saturation % 283.46/40.16 % (812729)Time elapsed: 0.197 s % 283.46/40.16 % (812729)Peak memory usage: 13 MB % 283.46/40.16 % (812729)Instructions burned: 263 (million) % 283.46/40.16 % (812731)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4194733405:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2669 on theBenchmark for (2669ds/318Mi) % 283.46/40.16 % (812731)Instruction limit reached! % 283.46/40.16 % (812731)------------------------------ % 283.46/40.16 % (812731)VersTerminated % 300.31/42.54 % Vampire exiting % 300.31/42.54 Terminated %------------------------------------------------------------------------------