%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW534_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 : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:24 PM UTC 2026 % Result : Timeout 300.27s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW534_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.07/0.18 % Computer : n004.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 14:18:07 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 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.61/1.37 % (376350)Will run a generic schedule for satisfiability detection. % 7.61/1.37 % (376358)dis+10_1_sil=32000:sp=arity:random_seed=486653525:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.61/1.37 % (376356)% WARNING: option uhcvi not known. % 7.61/1.37 % (376355)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1484987890_2999 on theBenchmark for (2999ds/0Mi) % 7.61/1.37 % (376356)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=29538798:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.61/1.37 % (376357)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3685229655:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.61/1.37 % (376359)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4167212976:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.61/1.37 % (376360)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=552202336:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.61/1.37 % Exception at run slice level % 7.61/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.61/1.37 % (376361)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3667566140:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.61/1.37 % (376358)Instruction limit reached! % 7.61/1.37 % (376358)------------------------------ % 7.61/1.37 % (376358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.61/1.37 % (376358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.37 % (376358)CaDiCaL version: 2.1.3 % 7.61/1.37 % (376358)Termination reason: Instruction limit % 7.61/1.37 % (376358)Termination phase: Saturation % 7.61/1.37 % (376358)Time elapsed: 0.028 s % 7.61/1.37 % (376358)Peak memory usage: 12 MB % 7.61/1.37 % (376358)Instructions burned: 106 (million) % 7.61/1.37 % (376368)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=846862205:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.61/1.37 % (376370)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3704538521:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.61/1.37 % Exception at run slice level % 7.61/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.61/1.37 % (376373)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=1291229010:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.61/1.37 % (376359)Instruction limit reached! % 7.61/1.37 % (376359)------------------------------ % 7.61/1.37 % (376359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.61/1.37 % (376359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.37 % (376359)CaDiCaL version: 2.1.3 % 7.61/1.37 % (376359)Termination reason: Instruction limit % 7.61/1.37 % (376359)Termination phase: Saturation % 7.61/1.37 % (376359)Time elapsed: 0.063 s % 7.61/1.37 % (376359)Peak memory usage: 12 MB % 7.61/1.37 % (376359)Instructions burned: 116 (million) % 7.61/1.37 % (376370)Instruction limit reached! % 7.61/1.37 % (376370)------------------------------ % 7.61/1.37 % (376370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.61/1.37 % (376370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.37 % (376370)CaDiCaL version: 2.1.3 % 7.61/1.37 % (376370)Termination reason: Instruction limit % 7.61/1.37 % (376370)Termination phase: Saturation % 7.61/1.37 % (376370)Time elapsed: 0.041 s % 7.61/1.37 % (376370)Peak memory usage: 13 MB % 7.61/1.37 % (376370)Instructions burned: 131 (million) % 7.61/1.37 % (376360)Instruction limit reached! % 7.61/1.37 % (376360)------------------------------ % 7.61/1.37 % (376360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.61/1.37 % (376360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.37 % (376360)CaDiCaL version: 2.1.3 % 7.61/1.37 % (376360)Termination reason: Instruction limit % 7.61/1.37 % (376360)Termination phase: Saturation % 7.61/1.37 % (376360)Time elapsed: 0.080 s % 7.61/1.37 % (376360)Peak memory usage: 13 MB % 7.61/1.37 % (376360)Instructions burned: 132 (million) % 7.61/1.37 % (376375)ott-21_1_sil=16000:fs=off:random_seed=3465438437:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.61/1.37 % (376376)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4239195370:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 14.96/2.99 % (376361)Instruction limit reached! % 14.96/2.99 % (376361)------------------------------ % 14.96/2.99 % (376361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.96/2.99 % (376361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.96/2.99 % (376361)CaDiCaL version: 2.1.3 % 14.96/2.99 % (376361)Termination reason: Instruction limit % 14.96/2.99 % (376361)Termination phase: Saturation % 14.96/2.99 % (376361)Time elapsed: 0.079 s % 14.96/2.99 % (376361)Peak memory usage: 12 MB % 14.96/2.99 % (376361)Instructions burned: 160 (million) % 14.96/2.99 % (376377)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2724012969:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 14.96/2.99 % Exception at run slice level % 14.96/2.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.96/2.99 % (376380)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=828248210:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 14.96/2.99 % (376382)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4189807879:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 14.96/2.99 % Exception at run slice level % 14.96/2.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.96/2.99 % (376385)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=2470009458: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) % 14.96/2.99 % (376375)Instruction limit reached! % 14.96/2.99 % (376375)------------------------------ % 14.96/2.99 % (376375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.96/2.99 % (376375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.96/2.99 % (376375)CaDiCaL version: 2.1.3 % 14.96/2.99 % (376375)Termination reason: Instruction limit % 14.96/2.99 % (376375)Termination phase: Saturation % 14.96/2.99 % (376375)Time elapsed: 0.092 s % 14.96/2.99 % (376375)Peak memory usage: 12 MB % 14.96/2.99 % (376375)Instructions burned: 182 (million) % 14.96/2.99 % (376387)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1510330878:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 14.96/2.99 % (376376)Instruction limit reached! % 14.96/2.99 % (376376)------------------------------ % 14.96/2.99 % (376376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.96/2.99 % (376376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.96/2.99 % (376376)CaDiCaL version: 2.1.3 % 14.96/2.99 % (376376)Termination reason: Instruction limit % 14.96/2.99 % (376376)Termination phase: Saturation % 14.96/2.99 % (376376)Time elapsed: 0.131 s % 14.96/2.99 % (376376)Peak memory usage: 13 MB % 14.96/2.99 % (376376)Instructions burned: 479 (million) % 14.96/2.99 % (376389)fmb+10_1_sil=64000:random_seed=50145697:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 14.96/2.99 % (376389)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 14.96/2.99 % Exception at run slice level % 14.96/2.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.96/2.99 % (376391)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1650843044:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 14.96/2.99 % Exception at run slice level % 14.96/2.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.96/2.99 % (376393)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2760758364:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 14.96/2.99 % Exception at run slice level % 14.96/2.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.96/2.99 % (376395)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1641744311:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 14.96/2.99 % (376373)Instruction limit reached! % 14.96/2.99 % (376373)------------------------------ % 14.96/2.99 % (376373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.96/2.99 % (376373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.96/2.99 % (376373)CaDiCaL version: 2.1.3 % 14.96/2.99 % (376373)Termination reason: Instruction limit % 14.96/2.99 % (376373)Termination phase: Saturation % 67.93/9.85 % (376373)Time elapsed: 0.325 s % 67.93/9.85 % (376373)Peak memory usage: 15 MB % 67.93/9.85 % (376373)Instructions burned: 687 (million) % 67.93/9.85 % (376397)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1819209181:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 67.93/9.85 % (376397)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 67.93/9.85 % (376387)Instruction limit reached! % 67.93/9.85 % (376387)------------------------------ % 67.93/9.85 % (376387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.93/9.85 % (376387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.93/9.85 % (376387)CaDiCaL version: 2.1.3 % 67.93/9.85 % (376387)Termination reason: Instruction limit % 67.93/9.85 % (376387)Termination phase: Saturation % 67.93/9.85 % (376387)Time elapsed: 0.302 s % 67.93/9.85 % (376387)Peak memory usage: 18 MB % 67.93/9.85 % (376387)Instructions burned: 881 (million) % 67.93/9.85 % (376399)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4003865852:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 67.93/9.85 % (376385)Instruction limit reached! % 67.93/9.85 % (376385)------------------------------ % 67.93/9.85 % (376385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.93/9.85 % (376385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.93/9.85 % (376385)CaDiCaL version: 2.1.3 % 67.93/9.85 % (376385)Termination reason: Instruction limit % 67.93/9.85 % (376385)Termination phase: Saturation % 67.93/9.85 % (376385)Time elapsed: 0.360 s % 67.93/9.85 % (376385)Peak memory usage: 22 MB % 67.93/9.85 % (376385)Instructions burned: 693 (million) % 67.93/9.85 % Exception at run slice level % 67.93/9.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.93/9.85 % (376402)ott-2_1_sil=16000:newcnf=on:random_seed=28910736:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 67.93/9.85 % (376401)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2051079051:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 67.93/9.85 % Exception at run slice level % 67.93/9.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.93/9.85 % (376405)ott+10_1_sil=32000:tgt=ground:random_seed=320021925:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 67.93/9.85 % (376380)Instruction limit reached! % 67.93/9.85 % (376380)------------------------------ % 67.93/9.85 % (376380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.93/9.85 % (376380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.93/9.85 % (376380)CaDiCaL version: 2.1.3 % 67.93/9.85 % (376380)Termination reason: Instruction limit % 67.93/9.85 % (376380)Termination phase: Saturation % 67.93/9.85 % (376380)Time elapsed: 0.541 s % 67.93/9.85 % (376380)Peak memory usage: 15 MB % 67.93/9.85 % (376380)Instructions burned: 1182 (million) % 67.93/9.85 % (376407)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3623551357:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 67.93/9.85 % Exception at run slice level % 67.93/9.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 67.93/9.85 % (376409)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1317431411:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 67.93/9.85 % (376402)Instruction limit reached! % 67.93/9.85 % (376402)------------------------------ % 67.93/9.85 % (376402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.93/9.85 % (376402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.93/9.85 % (376402)CaDiCaL version: 2.1.3 % 67.93/9.85 % (376402)Termination reason: Instruction limit % 67.93/9.85 % (376402)Termination phase: Saturation % 67.93/9.85 % (376402)Time elapsed: 0.197 s % 67.93/9.85 % (376402)Peak memory usage: 13 MB % 67.93/9.85 % (376402)Instructions burned: 871 (million) % 67.93/9.85 % (376411)dis+21_1_sil=32000:sas=cadical:random_seed=2348892565:i=3773:amm=off_2992 on theBenchmark for (2992ds/3773Mi) % 67.93/9.85 % (376397)Instruction limit reached! % 67.93/9.85 % (376397)------------------------------ % 67.93/9.85 % (376397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.93/9.85 % (376397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.93/9.85 % (376397)CaDiCaL version: 2.1.3 % 97.92/14.08 % (376397)Termination reason: Instruction limit % 97.92/14.08 % (376397)Termination phase: Saturation % 97.92/14.08 % (376397)Time elapsed: 0.709 s % 97.92/14.08 % (376397)Peak memory usage: 18 MB % 97.92/14.08 % (376397)Instructions burned: 1472 (million) % 97.92/14.08 % (376413)ott+11_1_sil=16000:gs=on:random_seed=2717327312:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 97.92/14.08 % (376411)Instruction limit reached! % 97.92/14.08 % (376411)------------------------------ % 97.92/14.08 % (376411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.08 % (376411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.08 % (376411)CaDiCaL version: 2.1.3 % 97.92/14.08 % (376411)Termination reason: Instruction limit % 97.92/14.08 % (376411)Termination phase: Saturation % 97.92/14.08 % (376411)Time elapsed: 1.017 s % 97.92/14.08 % (376411)Peak memory usage: 28 MB % 97.92/14.08 % (376411)Instructions burned: 3775 (million) % 97.92/14.08 % (376415)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=695702645:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 97.92/14.08 % Exception at run slice level % 97.92/14.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.92/14.08 % (376417)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3538338663:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 97.92/14.08 % (376413)Instruction limit reached! % 97.92/14.08 % (376413)------------------------------ % 97.92/14.08 % (376413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.08 % (376413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.08 % (376413)CaDiCaL version: 2.1.3 % 97.92/14.08 % (376413)Termination reason: Instruction limit % 97.92/14.08 % (376413)Termination phase: Saturation % 97.92/14.08 % (376413)Time elapsed: 1.036 s % 97.92/14.08 % (376413)Peak memory usage: 17 MB % 97.92/14.08 % (376413)Instructions burned: 2253 (million) % 97.92/14.08 % (376419)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=336099150:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 97.92/14.08 % (376409)Instruction limit reached! % 97.92/14.08 % (376409)------------------------------ % 97.92/14.08 % (376409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.08 % (376409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.08 % (376409)CaDiCaL version: 2.1.3 % 97.92/14.08 % (376409)Termination reason: Instruction limit % 97.92/14.08 % (376409)Termination phase: Saturation % 97.92/14.08 % (376409)Time elapsed: 1.688 s % 97.92/14.08 % (376409)Peak memory usage: 24 MB % 97.92/14.08 % (376409)Instructions burned: 3512 (million) % 97.92/14.08 % (376421)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3311929384:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 97.92/14.08 % (376395)Instruction limit reached! % 97.92/14.08 % (376395)------------------------------ % 97.92/14.08 % (376395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.08 % (376395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.08 % (376395)CaDiCaL version: 2.1.3 % 97.92/14.08 % (376395)Termination reason: Instruction limit % 97.92/14.08 % (376395)Termination phase: Saturation % 97.92/14.08 % (376395)Time elapsed: 2.359 s % 97.92/14.08 % (376395)Peak memory usage: 23 MB % 97.92/14.08 % (376395)Instructions burned: 5131 (million) % 97.92/14.08 % (376423)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2108418544:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi) % 97.92/14.08 % Exception at run slice level % 97.92/14.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.92/14.08 % (376425)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1440783253:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 97.92/14.08 % Exception at run slice level % 97.92/14.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.92/14.08 % (376427)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3678619650:i=14071_2972 on theBenchmark for (2972ds/14071Mi) % 97.92/14.08 % Exception at run slice level % 97.92/14.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.92/14.08 % (376429)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3208169915:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi) % 153.66/21.93 % (376405)Instruction limit reached! % 153.66/21.93 % (376405)------------------------------ % 153.66/21.93 % (376405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376405)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376405)Termination reason: Instruction limit % 153.66/21.93 % (376405)Termination phase: Saturation % 153.66/21.93 % (376405)Time elapsed: 2.295 s % 153.66/21.93 % (376405)Peak memory usage: 17 MB % 153.66/21.93 % (376405)Instructions burned: 5116 (million) % 153.66/21.93 % (376431)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3338683035:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi) % 153.66/21.93 % (376417)Instruction limit reached! % 153.66/21.93 % (376417)------------------------------ % 153.66/21.93 % (376417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376417)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376417)Termination reason: Instruction limit % 153.66/21.93 % (376417)Termination phase: Saturation % 153.66/21.93 % (376417)Time elapsed: 1.127 s % 153.66/21.93 % (376417)Peak memory usage: 23 MB % 153.66/21.93 % (376417)Instructions burned: 4592 (million) % 153.66/21.93 % (376433)dis+10_16:1_sil=16000:random_seed=3632176094:i=9155:fsr=off_2970 on theBenchmark for (2970ds/9155Mi) % 153.66/21.93 % (376421)Instruction limit reached! % 153.66/21.93 % (376421)------------------------------ % 153.66/21.93 % (376421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376421)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376421)Termination reason: Instruction limit % 153.66/21.93 % (376421)Termination phase: Saturation % 153.66/21.93 % (376421)Time elapsed: 2.787 s % 153.66/21.93 % (376421)Peak memory usage: 41 MB % 153.66/21.93 % (376421)Instructions burned: 5211 (million) % 153.66/21.93 % (376435)ott-3_8_sil=64000:random_seed=2379380437:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 153.66/21.93 % (376433)Instruction limit reached! % 153.66/21.93 % (376433)------------------------------ % 153.66/21.93 % (376433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376433)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376433)Termination reason: Instruction limit % 153.66/21.93 % (376433)Termination phase: Saturation % 153.66/21.93 % (376433)Time elapsed: 2.609 s % 153.66/21.93 % (376433)Peak memory usage: 63 MB % 153.66/21.93 % (376433)Instructions burned: 9158 (million) % 153.66/21.93 % (376437)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2205009187:fmbsr=2:i=32576_2944 on theBenchmark for (2944ds/32576Mi) % 153.66/21.93 % Exception at run slice level % 153.66/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.66/21.93 % (376439)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1073865471:i=11404_2944 on theBenchmark for (2944ds/11404Mi) % 153.66/21.93 % (376431)Instruction limit reached! % 153.66/21.93 % (376431)------------------------------ % 153.66/21.93 % (376431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376431)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376431)Termination reason: Instruction limit % 153.66/21.93 % (376431)Termination phase: Saturation % 153.66/21.93 % (376431)Time elapsed: 3.933 s % 153.66/21.93 % (376431)Peak memory usage: 24 MB % 153.66/21.93 % (376431)Instructions burned: 8173 (million) % 153.66/21.93 % (376441)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3747517883:i=14134_2931 on theBenchmark for (2931ds/14134Mi) % 153.66/21.93 % (376439)Instruction limit reached! % 153.66/21.93 % (376439)------------------------------ % 153.66/21.93 % (376439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.66/21.93 % (376439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.66/21.93 % (376439)CaDiCaL version: 2.1.3 % 153.66/21.93 % (376439)Termination reason: Instruction limit % 153.66/21.93 % (376439)Termination phase: Saturation % 153.66/21.93 % (376439)Time elapsed: 4.014 s % 153.66/21.93 % (376439)Peak memory usage: 101 MB % 153.66/21.93 % (376439)Instructions burned: 11404 (million) % 153.66/21.93 % (376443)dis+33_16_sil=32000:sac=on:random_seed=36513962:i=15851:nm=0_2903 on theBenchmark for (2903ds/15851Mi) % 163.01/23.20 % (376441)Instruction limit reached! % 163.01/23.20 % (376441)------------------------------ % 163.01/23.20 % (376441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.01/23.20 % (376441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.01/23.20 % (376441)CaDiCaL version: 2.1.3 % 163.01/23.20 % (376441)Termination reason: Instruction limit % 163.01/23.20 % (376441)Termination phase: Saturation % 163.01/23.20 % (376441)Time elapsed: 6.512 s % 163.01/23.20 % (376441)Peak memory usage: 27 MB % 163.01/23.20 % (376441)Instructions burned: 14135 (million) % 163.01/23.20 % (376445)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=181106749:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi) % 163.01/23.20 % (376443)Instruction limit reached! % 163.01/23.20 % (376443)------------------------------ % 163.01/23.20 % (376443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.01/23.20 % (376443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.01/23.20 % (376443)CaDiCaL version: 2.1.3 % 163.01/23.20 % (376443)Termination reason: Instruction limit % 163.01/23.20 % (376443)Termination phase: Saturation % 163.01/23.20 % (376443)Time elapsed: 3.871 s % 163.01/23.20 % (376443)Peak memory usage: 142 MB % 163.01/23.20 % (376443)Instructions burned: 15870 (million) % 163.01/23.20 % (376447)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=244709837:s2a=on:i=53295_2864 on theBenchmark for (2864ds/53295Mi) % 163.01/23.20 % (376429)Instruction limit reached! % 163.01/23.20 % (376429)------------------------------ % 163.01/23.20 % (376429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.01/23.20 % (376429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.01/23.20 % (376429)CaDiCaL version: 2.1.3 % 163.01/23.20 % (376429)Termination reason: Instruction limit % 163.01/23.20 % (376429)Termination phase: Saturation % 163.01/23.20 % (376429)Time elapsed: 10.927 s % 163.01/23.20 % (376429)Peak memory usage: 76 MB % 163.01/23.20 % (376429)Instructions burned: 22567 (million) % 163.01/23.20 % (376435)Instruction limit reached! % 163.01/23.20 % (376435)------------------------------ % 163.01/23.20 % (376435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.01/23.20 % (376435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.01/23.20 % (376435)CaDiCaL version: 2.1.3 % 163.01/23.20 % (376435)Termination reason: Instruction limit % 163.01/23.20 % (376435)Termination phase: Saturation % 163.01/23.20 % (376435)Time elapsed: 8.451 s % 163.01/23.20 % (376435)Peak memory usage: 23 MB % 163.01/23.20 % (376435)Instructions burned: 20140 (million) % 163.01/23.20 % (376449)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1846522982:i=26857:ins=20_2862 on theBenchmark for (2862ds/26857Mi) % 163.01/23.20 % (376450)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=939641504:i=28120:bs=on:fsr=off_2862 on theBenchmark for (2862ds/28120Mi) % 163.01/23.20 % Exception at run slice level % 163.01/23.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.01/23.20 % (376453)fmb+10_1_sil=256000:fmbss=7:random_seed=2596187557:fmbsr=1.6:i=182295_2862 on theBenchmark for (2862ds/182295Mi) % 163.01/23.20 % Exception at run slice level % 163.01/23.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.01/23.20 % (376455)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3230352029:i=44625:gsp=on_2862 on theBenchmark for (2862ds/44625Mi) % 163.01/23.20 % (376455)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 163.01/23.20 % Exception at run slice level % 163.01/23.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.01/23.20 % (376457)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2252978021:i=160505_2862 on theBenchmark for (2862ds/160505Mi) % 163.01/23.20 % Exception at run slice level % 163.01/23.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.01/23.20 % (376459)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1054522871:fmbsr=1.3:i=225729_2861 on theBenchmark for (2861ds/225729Mi) % 163.01/23.20 % Exception at run slice level % 163.01/23.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.01/23.20 % (376461)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1271679395:fmbsr=2:i=185024:ins=7_2861 on theBenchmark for (2861ds/185024Mi) % 183.09/26.13 % Exception at run slice level % 183.09/26.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.09/26.13 % (376463)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=193801514:rtra=on_2861 on theBenchmark for (2861ds/0Mi) % 183.09/26.13 % Exception at run slice level % 183.09/26.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 183.09/26.13 % (376465)% WARNING: option uhcvi not known. % 183.09/26.13 % (376465)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1771814123:i=271062:add=off:rtra=on:rawr=on_2861 on theBenchmark for (2861ds/271062Mi) % 183.09/26.13 % (376419)Instruction limit reached! % 183.09/26.13 % (376419)------------------------------ % 183.09/26.13 % (376419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.09/26.13 % (376419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.13 % (376419)CaDiCaL version: 2.1.3 % 183.09/26.13 % (376419)Termination reason: Instruction limit % 183.09/26.13 % (376419)Termination phase: Saturation % 183.09/26.13 % (376419)Time elapsed: 14.589 s % 183.09/26.13 % (376419)Peak memory usage: 631 MB % 183.09/26.13 % (376419)Instructions burned: 29340 (million) % 183.09/26.13 % (376619)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1882363645:i=176048:add=on:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/176048Mi) % 183.09/26.13 % (376445)Instruction limit reached! % 183.09/26.13 % (376445)------------------------------ % 183.09/26.13 % (376445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.09/26.13 % (376445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.13 % (376445)CaDiCaL version: 2.1.3 % 183.09/26.13 % (376445)Termination reason: Instruction limit % 183.09/26.13 % (376445)Termination phase: Saturation % 183.09/26.13 % (376445)Time elapsed: 7.663 s % 183.09/26.13 % (376445)Peak memory usage: 33 MB % 183.09/26.13 % (376445)Instructions burned: 17630 (million) % 183.09/26.13 % (376622)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3053789286:i=206:fgj=on:rtra=on_2789 on theBenchmark for (2789ds/206Mi) % 183.09/26.13 % (376622)Instruction limit reached! % 183.09/26.13 % (376622)------------------------------ % 183.09/26.13 % (376622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.09/26.13 % (376622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.13 % (376622)CaDiCaL version: 2.1.3 % 183.09/26.13 % (376622)Termination reason: Instruction limit % 183.09/26.13 % (376622)Termination phase: Saturation % 183.09/26.13 % (376622)Time elapsed: 0.109 s % 183.09/26.13 % (376622)Peak memory usage: 12 MB % 183.09/26.13 % (376622)Instructions burned: 206 (million) % 183.09/26.13 % (376624)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2029458844:i=232:rtra=on_2788 on theBenchmark for (2788ds/232Mi) % 183.09/26.13 % (376624)Instruction limit reached! % 183.09/26.13 % (376624)------------------------------ % 183.09/26.13 % (376624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.09/26.13 % (376624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.13 % (376624)CaDiCaL version: 2.1.3 % 183.09/26.13 % (376624)Termination reason: Instruction limit % 183.09/26.13 % (376624)Termination phase: Saturation % 183.09/26.13 % (376624)Time elapsed: 0.125 s % 183.09/26.13 % (376624)Peak memory usage: 13 MB % 183.09/26.13 % (376624)Instructions burned: 233 (million) % 183.09/26.13 % (376626)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1159074045:i=262:rtra=on_2786 on theBenchmark for (2786ds/262Mi) % 183.09/26.13 % (376626)Instruction limit reached! % 183.09/26.13 % (376626)------------------------------ % 183.09/26.13 % (376626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.09/26.13 % (376626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.13 % (376626)CaDiCaL version: 2.1.3 % 183.09/26.13 % (376626)Termination reason: Instruction limit % 183.09/26.13 % (376626)Termination phase: Saturation % 183.09/26.13 % (376626)Time elapsed: 0.168 s % 183.09/26.13 % (376626)Peak memory usage: 15 MB % 183.09/26.13 % (376626)Instructions burned: 263 (million) % 183.09/26.13 % (376628)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3340075515:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2784 on theBenchmark for (2784ds/318Mi) % 183.09/26.13 % (376628)Instruction limit reached! % 183.09/26.13 % (376628)------------------------------ % 183.09/26.13 % (376628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.96/31.55 % (376628)CaDiCaL version: 2.1.3 % 221.96/31.55 % (376628)Termination reason: Instruction limit % 221.96/31.55 % (376628)Termination phase: Saturation % 221.96/31.55 % (376628)Time elapsed: 0.159 s % 221.96/31.55 % (376628)Peak memory usage: 13 MB % 221.96/31.55 % (376628)Instructions burned: 319 (million) % 221.96/31.55 % (376630)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1842848901:i=1428:nm=2:rtra=on_2782 on theBenchmark for (2782ds/1428Mi) % 221.96/31.55 % Exception at run slice level % 221.96/31.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.96/31.55 % (376632)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3840556859:i=262:bd=preordered:rtra=on:fsd=on_2782 on theBenchmark for (2782ds/262Mi) % 221.96/31.55 % (376632)Instruction limit reached! % 221.96/31.55 % (376632)------------------------------ % 221.96/31.55 % (376632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.96/31.55 % (376632)CaDiCaL version: 2.1.3 % 221.96/31.55 % (376632)Termination reason: Instruction limit % 221.96/31.55 % (376632)Termination phase: Saturation % 221.96/31.55 % (376632)Time elapsed: 0.156 s % 221.96/31.55 % (376632)Peak memory usage: 14 MB % 221.96/31.55 % (376632)Instructions burned: 262 (million) % 221.96/31.55 % (376634)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=3109527447:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1368Mi) % 221.96/31.55 % (376450)Instruction limit reached! % 221.96/31.55 % (376450)------------------------------ % 221.96/31.55 % (376450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.96/31.55 % (376450)CaDiCaL version: 2.1.3 % 221.96/31.55 % (376450)Termination reason: Instruction limit % 221.96/31.55 % (376450)Termination phase: Saturation % 221.96/31.55 % (376450)Time elapsed: 8.567 s % 221.96/31.55 % (376450)Peak memory usage: 14 MB % 221.96/31.55 % (376450)Instructions burned: 28122 (million) % 221.96/31.55 % (376636)ott-21_1_sil=16000:si=on:fs=off:random_seed=601314238:i=360:av=off:fsr=off:rtra=on_2777 on theBenchmark for (2777ds/360Mi) % 221.96/31.55 % (376636)Instruction limit reached! % 221.96/31.55 % (376636)------------------------------ % 221.96/31.55 % (376636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.96/31.55 % (376636)CaDiCaL version: 2.1.3 % 221.96/31.55 % (376636)Termination reason: Instruction limit % 221.96/31.55 % (376636)Termination phase: Saturation % 221.96/31.55 % (376636)Time elapsed: 0.175 s % 221.96/31.55 % (376636)Peak memory usage: 13 MB % 221.96/31.55 % (376636)Instructions burned: 361 (million) % 221.96/31.55 % (376638)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1114444032:i=954:bd=all:rtra=on_2775 on theBenchmark for (2775ds/954Mi) % 221.96/31.55 % (376634)Instruction limit reached! % 221.96/31.55 % (376634)------------------------------ % 221.96/31.55 % (376634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.96/31.55 % (376634)CaDiCaL version: 2.1.3 % 221.96/31.55 % (376634)Termination reason: Instruction limit % 221.96/31.55 % (376634)Termination phase: Saturation % 221.96/31.55 % (376634)Time elapsed: 0.689 s % 221.96/31.55 % (376634)Peak memory usage: 17 MB % 221.96/31.55 % (376634)Instructions burned: 1369 (million) % 221.96/31.55 % (376640)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1676422943:fmbsr=1.3:i=1730:ins=25:rtra=on_2773 on theBenchmark for (2773ds/1730Mi) % 221.96/31.55 % Exception at run slice level % 221.96/31.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.96/31.55 % (376642)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3582381622:i=2358:rtra=on_2773 on theBenchmark for (2773ds/2358Mi) % 221.96/31.55 % (376638)Instruction limit reached! % 221.96/31.55 % (376638)------------------------------ % 221.96/31.55 % (376638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.96/31.55 % (376638)Linked with Z3 4.14.0.0 3c47fd96cf56Terminated % 300.27/42.54 % Vampire exiting % 300.27/42.54 Terminated %------------------------------------------------------------------------------