%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM025_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 : 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 : Tue Sep 29 09:40:11 AM UTC 2026 % Result : Timeout 300.57s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM025_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n006.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 21:48:40 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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.98/1.56 % (239528)Will run a generic schedule for satisfiability detection. % 7.98/1.56 % (239540)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3897289255:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.98/1.56 % (239537)% WARNING: option uhcvi not known. % 7.98/1.56 % (239536)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2156760208_2999 on theBenchmark for (2999ds/0Mi) % 7.98/1.56 % (239538)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2259186664:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.98/1.56 % (239537)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2564765097:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.98/1.56 % (239539)dis+10_1_sil=32000:sp=arity:random_seed=1589732805:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.98/1.56 % (239541)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3720730914:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.98/1.56 % (239542)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3587766100:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.98/1.56 % Exception at run slice level % 7.98/1.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.98/1.56 % (239550)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1707113159:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.98/1.56 % (239540)Instruction limit reached! % 7.98/1.56 % (239540)------------------------------ % 7.98/1.56 % (239540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.56 % (239540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.56 % (239540)CaDiCaL version: 2.1.3 % 7.98/1.56 % (239540)Termination reason: Instruction limit % 7.98/1.56 % (239540)Termination phase: Saturation % 7.98/1.56 % (239540)Time elapsed: 0.038 s % 7.98/1.56 % (239540)Peak memory usage: 13 MB % 7.98/1.56 % (239540)Instructions burned: 117 (million) % 7.98/1.56 % Exception at run slice level % 7.98/1.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.98/1.56 % (239552)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1480555841:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.98/1.56 % (239553)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=3937414150:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.98/1.56 % (239539)Instruction limit reached! % 7.98/1.56 % (239539)------------------------------ % 7.98/1.56 % (239539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.56 % (239539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.56 % (239539)CaDiCaL version: 2.1.3 % 7.98/1.56 % (239539)Termination reason: Instruction limit % 7.98/1.56 % (239539)Termination phase: Saturation % 7.98/1.56 % (239539)Time elapsed: 0.063 s % 7.98/1.56 % (239539)Peak memory usage: 12 MB % 7.98/1.56 % (239539)Instructions burned: 103 (million) % 7.98/1.56 % (239541)Instruction limit reached! % 7.98/1.56 % (239541)------------------------------ % 7.98/1.56 % (239541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.56 % (239541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.56 % (239541)CaDiCaL version: 2.1.3 % 7.98/1.56 % (239541)Termination reason: Instruction limit % 7.98/1.56 % (239541)Termination phase: Saturation % 7.98/1.56 % (239541)Time elapsed: 0.077 s % 7.98/1.56 % (239541)Peak memory usage: 13 MB % 7.98/1.56 % (239541)Instructions burned: 132 (million) % 7.98/1.56 % (239552)Instruction limit reached! % 7.98/1.56 % (239552)------------------------------ % 7.98/1.56 % (239552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.56 % (239552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.56 % (239552)CaDiCaL version: 2.1.3 % 7.98/1.56 % (239552)Termination reason: Instruction limit % 7.98/1.56 % (239552)Termination phase: Saturation % 7.98/1.56 % (239552)Time elapsed: 0.040 s % 7.98/1.56 % (239552)Peak memory usage: 13 MB % 7.98/1.56 % (239552)Instructions burned: 132 (million) % 7.98/1.56 % (239556)ott-21_1_sil=16000:fs=off:random_seed=2968746864:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.98/1.56 % (239558)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3335955872:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.38/3.40 % Exception at run slice level % 22.38/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.38/3.40 % (239557)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=542994895:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.38/3.40 % (239542)Instruction limit reached! % 22.38/3.40 % (239542)------------------------------ % 22.38/3.40 % (239542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.38/3.40 % (239542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/3.40 % (239542)CaDiCaL version: 2.1.3 % 22.38/3.40 % (239542)Termination reason: Instruction limit % 22.38/3.40 % (239542)Termination phase: Saturation % 22.38/3.40 % (239542)Time elapsed: 0.096 s % 22.38/3.40 % (239542)Peak memory usage: 14 MB % 22.38/3.40 % (239542)Instructions burned: 159 (million) % 22.38/3.40 % (239561)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=423718114:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.38/3.40 % (239563)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3523008695:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.38/3.40 % Exception at run slice level % 22.38/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.38/3.40 % (239566)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=3720782025:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 22.38/3.40 % (239556)Instruction limit reached! % 22.38/3.40 % (239556)------------------------------ % 22.38/3.40 % (239556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.38/3.40 % (239556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/3.40 % (239556)CaDiCaL version: 2.1.3 % 22.38/3.40 % (239556)Termination reason: Instruction limit % 22.38/3.40 % (239556)Termination phase: Saturation % 22.38/3.40 % (239556)Time elapsed: 0.096 s % 22.38/3.40 % (239556)Peak memory usage: 13 MB % 22.38/3.40 % (239556)Instructions burned: 181 (million) % 22.38/3.40 % (239568)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=203970570:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.38/3.40 % (239557)Instruction limit reached! % 22.38/3.40 % (239557)------------------------------ % 22.38/3.40 % (239557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.38/3.40 % (239557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/3.40 % (239557)CaDiCaL version: 2.1.3 % 22.38/3.40 % (239557)Termination reason: Instruction limit % 22.38/3.40 % (239557)Termination phase: Saturation % 22.38/3.40 % (239557)Time elapsed: 0.287 s % 22.38/3.40 % (239557)Peak memory usage: 15 MB % 22.38/3.40 % (239557)Instructions burned: 477 (million) % 22.38/3.40 % (239553)Instruction limit reached! % 22.38/3.40 % (239553)------------------------------ % 22.38/3.40 % (239553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.38/3.40 % (239553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/3.40 % (239553)CaDiCaL version: 2.1.3 % 22.38/3.40 % (239553)Termination reason: Instruction limit % 22.38/3.40 % (239553)Termination phase: Saturation % 22.38/3.40 % (239553)Time elapsed: 0.352 s % 22.38/3.40 % (239553)Peak memory usage: 17 MB % 22.38/3.40 % (239553)Instructions burned: 684 (million) % 22.38/3.40 % (239570)fmb+10_1_sil=64000:random_seed=2461505719:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.38/3.40 % (239570)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.38/3.40 % Exception at run slice level % 22.38/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.38/3.40 % (239572)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3396356246:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.38/3.40 % (239573)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2373697123:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.38/3.40 % Exception at run slice level % 22.38/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.38/3.40 % Exception at run slice level % 22.38/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.56/8.69 % (239576)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2258398748:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 58.56/8.69 % (239577)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1111058423:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 58.56/8.69 % (239577)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.56/8.69 % (239561)Instruction limit reached! % 58.56/8.69 % (239561)------------------------------ % 58.56/8.69 % (239561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.56/8.69 % (239561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.56/8.69 % (239561)CaDiCaL version: 2.1.3 % 58.56/8.69 % (239561)Termination reason: Instruction limit % 58.56/8.69 % (239561)Termination phase: Saturation % 58.56/8.69 % (239561)Time elapsed: 0.372 s % 58.56/8.69 % (239561)Peak memory usage: 22 MB % 58.56/8.69 % (239561)Instructions burned: 1181 (million) % 58.56/8.69 % (239580)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3290188098:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 58.56/8.69 % Exception at run slice level % 58.56/8.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.56/8.69 % (239582)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2121185207:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 58.56/8.69 % Exception at run slice level % 58.56/8.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.56/8.69 % (239584)ott-2_1_sil=16000:newcnf=on:random_seed=449197774:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 58.56/8.69 % (239566)Instruction limit reached! % 58.56/8.69 % (239566)------------------------------ % 58.56/8.69 % (239566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.56/8.69 % (239566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.56/8.69 % (239566)CaDiCaL version: 2.1.3 % 58.56/8.69 % (239566)Termination reason: Instruction limit % 58.56/8.69 % (239566)Termination phase: Saturation % 58.56/8.69 % (239566)Time elapsed: 0.398 s % 58.56/8.69 % (239566)Peak memory usage: 21 MB % 58.56/8.69 % (239566)Instructions burned: 693 (million) % 58.56/8.69 % (239586)ott+10_1_sil=32000:tgt=ground:random_seed=2245394336:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 58.56/8.69 % (239568)Instruction limit reached! % 58.56/8.69 % (239568)------------------------------ % 58.56/8.69 % (239568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.56/8.69 % (239568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.56/8.69 % (239568)CaDiCaL version: 2.1.3 % 58.56/8.69 % (239568)Termination reason: Instruction limit % 58.56/8.69 % (239568)Termination phase: Saturation % 58.56/8.69 % (239568)Time elapsed: 0.497 s % 58.56/8.69 % (239568)Peak memory usage: 18 MB % 58.56/8.69 % (239568)Instructions burned: 880 (million) % 58.56/8.69 % (239588)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3898894832:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 58.56/8.69 % Exception at run slice level % 58.56/8.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 58.56/8.69 % (239590)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=401241564:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 58.56/8.69 % (239584)Instruction limit reached! % 58.56/8.69 % (239584)------------------------------ % 58.56/8.69 % (239584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.56/8.69 % (239584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.56/8.69 % (239584)CaDiCaL version: 2.1.3 % 58.56/8.69 % (239584)Termination reason: Instruction limit % 58.56/8.69 % (239584)Termination phase: Saturation % 58.56/8.69 % (239584)Time elapsed: 0.263 s % 58.56/8.69 % (239584)Peak memory usage: 19 MB % 58.56/8.69 % (239584)Instructions burned: 872 (million) % 58.56/8.69 % (239592)dis+21_1_sil=32000:sas=cadical:random_seed=2985126579:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 58.56/8.69 % (239577)Instruction limit reached! % 58.56/8.69 % (239577)------------------------------ % 58.56/8.69 % (239577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.56/8.69 % (239577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.56/8.69 % (239577)CaDiCaL version: 2.1.3 % 118.07/16.97 % (239577)Termination reason: Instruction limit % 118.07/16.97 % (239577)Termination phase: Saturation % 118.07/16.97 % (239577)Time elapsed: 0.821 s % 118.07/16.97 % (239577)Peak memory usage: 30 MB % 118.07/16.97 % (239577)Instructions burned: 1473 (million) % 118.07/16.97 % (239594)ott+11_1_sil=16000:gs=on:random_seed=899401765:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 118.07/16.97 % (239592)Instruction limit reached! % 118.07/16.97 % (239592)------------------------------ % 118.07/16.97 % (239592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.97 % (239592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.97 % (239592)CaDiCaL version: 2.1.3 % 118.07/16.97 % (239592)Termination reason: Instruction limit % 118.07/16.97 % (239592)Termination phase: Saturation % 118.07/16.97 % (239592)Time elapsed: 1.093 s % 118.07/16.97 % (239592)Peak memory usage: 33 MB % 118.07/16.97 % (239592)Instructions burned: 3773 (million) % 118.07/16.97 % (239596)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=16823429:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 118.07/16.97 % Exception at run slice level % 118.07/16.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.97 % (239598)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2797387392:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 118.07/16.97 % (239594)Instruction limit reached! % 118.07/16.97 % (239594)------------------------------ % 118.07/16.97 % (239594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.97 % (239594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.97 % (239594)CaDiCaL version: 2.1.3 % 118.07/16.97 % (239594)Termination reason: Instruction limit % 118.07/16.97 % (239594)Termination phase: Saturation % 118.07/16.97 % (239594)Time elapsed: 1.074 s % 118.07/16.97 % (239594)Peak memory usage: 17 MB % 118.07/16.97 % (239594)Instructions burned: 2252 (million) % 118.07/16.97 % (239600)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3513891429:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 118.07/16.97 % (239590)Instruction limit reached! % 118.07/16.97 % (239590)------------------------------ % 118.07/16.97 % (239590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.97 % (239590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.97 % (239590)CaDiCaL version: 2.1.3 % 118.07/16.97 % (239590)Termination reason: Instruction limit % 118.07/16.97 % (239590)Termination phase: Saturation % 118.07/16.97 % (239590)Time elapsed: 1.921 s % 118.07/16.97 % (239590)Peak memory usage: 33 MB % 118.07/16.97 % (239590)Instructions burned: 3512 (million) % 118.07/16.97 % (239602)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=988268233:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 118.07/16.97 % (239598)Instruction limit reached! % 118.07/16.97 % (239598)------------------------------ % 118.07/16.97 % (239598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.07/16.97 % (239598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.07/16.97 % (239598)CaDiCaL version: 2.1.3 % 118.07/16.97 % (239598)Termination reason: Instruction limit % 118.07/16.97 % (239598)Termination phase: Saturation % 118.07/16.97 % (239598)Time elapsed: 1.126 s % 118.07/16.97 % (239598)Peak memory usage: 30 MB % 118.07/16.97 % (239598)Instructions burned: 4592 (million) % 118.07/16.97 % (239604)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3576607496:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 118.07/16.97 % Exception at run slice level % 118.07/16.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.97 % (239606)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1106228404:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 118.07/16.97 % Exception at run slice level % 118.07/16.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.97 % (239608)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=683330752:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 118.07/16.97 % Exception at run slice level % 118.07/16.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 118.07/16.97 % (239610)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1254039243:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 129.38/18.56 % (239576)Instruction limit reached! % 129.38/18.56 % (239576)------------------------------ % 129.38/18.56 % (239576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239576)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239576)Termination reason: Instruction limit % 129.38/18.56 % (239576)Termination phase: Saturation % 129.38/18.56 % (239576)Time elapsed: 2.788 s % 129.38/18.56 % (239576)Peak memory usage: 41 MB % 129.38/18.56 % (239576)Instructions burned: 5132 (million) % 129.38/18.56 % (239612)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=454681666:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 129.38/18.56 % (239586)Instruction limit reached! % 129.38/18.56 % (239586)------------------------------ % 129.38/18.56 % (239586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239586)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239586)Termination reason: Instruction limit % 129.38/18.56 % (239586)Termination phase: Saturation % 129.38/18.56 % (239586)Time elapsed: 3.021 s % 129.38/18.56 % (239586)Peak memory usage: 52 MB % 129.38/18.56 % (239586)Instructions burned: 5114 (million) % 129.38/18.56 % (239614)dis+10_16:1_sil=16000:random_seed=3340408244:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 129.38/18.56 % (239602)Instruction limit reached! % 129.38/18.56 % (239602)------------------------------ % 129.38/18.56 % (239602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239602)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239602)Termination reason: Instruction limit % 129.38/18.56 % (239602)Termination phase: Saturation % 129.38/18.56 % (239602)Time elapsed: 2.711 s % 129.38/18.56 % (239602)Peak memory usage: 43 MB % 129.38/18.56 % (239602)Instructions burned: 5211 (million) % 129.38/18.56 % (239616)ott-3_8_sil=64000:random_seed=1038687820:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 129.38/18.56 % (239610)Instruction limit reached! % 129.38/18.56 % (239610)------------------------------ % 129.38/18.56 % (239610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239610)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239610)Termination reason: Instruction limit % 129.38/18.56 % (239610)Termination phase: Saturation % 129.38/18.56 % (239610)Time elapsed: 4.633 s % 129.38/18.56 % (239610)Peak memory usage: 73 MB % 129.38/18.56 % (239610)Instructions burned: 22568 (million) % 129.38/18.56 % (239618)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=722179719:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi) % 129.38/18.56 % Exception at run slice level % 129.38/18.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.38/18.56 % (239620)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1002139778:i=11404_2921 on theBenchmark for (2921ds/11404Mi) % 129.38/18.56 % (239612)Instruction limit reached! % 129.38/18.56 % (239612)------------------------------ % 129.38/18.56 % (239612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239612)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239612)Termination reason: Instruction limit % 129.38/18.56 % (239612)Termination phase: Saturation % 129.38/18.56 % (239612)Time elapsed: 4.888 s % 129.38/18.56 % (239612)Peak memory usage: 70 MB % 129.38/18.56 % (239612)Instructions burned: 8173 (million) % 129.38/18.56 % (239622)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2454841403:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 129.38/18.56 % (239614)Instruction limit reached! % 129.38/18.56 % (239614)------------------------------ % 129.38/18.56 % (239614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.38/18.56 % (239614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.38/18.56 % (239614)CaDiCaL version: 2.1.3 % 129.38/18.56 % (239614)Termination reason: Instruction limit % 129.38/18.56 % (239614)Termination phase: Saturation % 129.38/18.56 % (239614)Time elapsed: 4.775 s % 129.38/18.56 % (239614)Peak memory usage: 48 MB % 129.38/18.56 % (239614)Instructions burned: 9155 (million) % 129.38/18.56 % (239624)dis+33_16_sil=32000:sac=on:random_seed=3523978472:i=15851:nm=0_2915 on theBenchmark for (2915ds/15851Mi) % 152.95/21.82 % (239620)Instruction limit reached! % 152.95/21.82 % (239620)------------------------------ % 152.95/21.82 % (239620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.95/21.82 % (239620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/21.82 % (239620)CaDiCaL version: 2.1.3 % 152.95/21.82 % (239620)Termination reason: Instruction limit % 152.95/21.82 % (239620)Termination phase: Saturation % 152.95/21.82 % (239620)Time elapsed: 3.807 s % 152.95/21.82 % (239620)Peak memory usage: 100 MB % 152.95/21.82 % (239620)Instructions burned: 11407 (million) % 152.95/21.82 % (239626)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3799116434:avsq=on:i=17627:add=on:amm=off_2883 on theBenchmark for (2883ds/17627Mi) % 152.95/21.82 % (239600)Instruction limit reached! % 152.95/21.82 % (239600)------------------------------ % 152.95/21.82 % (239600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.95/21.82 % (239600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/21.82 % (239600)CaDiCaL version: 2.1.3 % 152.95/21.82 % (239600)Termination reason: Instruction limit % 152.95/21.82 % (239600)Termination phase: Saturation % 152.95/21.82 % (239600)Time elapsed: 12.759 s % 152.95/21.82 % (239600)Peak memory usage: 178 MB % 152.95/21.82 % (239600)Instructions burned: 29342 (million) % 152.95/21.82 % (239987)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=356435967:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 152.95/21.82 % (239626)Instruction limit reached! % 152.95/21.82 % (239626)------------------------------ % 152.95/21.82 % (239626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.95/21.82 % (239626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/21.82 % (239626)CaDiCaL version: 2.1.3 % 152.95/21.82 % (239626)Termination reason: Instruction limit % 152.95/21.82 % (239626)Termination phase: Saturation % 152.95/21.82 % (239626)Time elapsed: 4.886 s % 152.95/21.82 % (239626)Peak memory usage: 56 MB % 152.95/21.82 % (239626)Instructions burned: 17628 (million) % 152.95/21.82 % (239989)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1190296403:i=26857:ins=20_2834 on theBenchmark for (2834ds/26857Mi) % 152.95/21.82 % Exception at run slice level % 152.95/21.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 152.95/21.82 % (239991)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3253411085:i=28120:bs=on:fsr=off_2834 on theBenchmark for (2834ds/28120Mi) % 152.95/21.82 % (239624)Instruction limit reached! % 152.95/21.82 % (239624)------------------------------ % 152.95/21.82 % (239624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.95/21.82 % (239624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/21.82 % (239624)CaDiCaL version: 2.1.3 % 152.95/21.82 % (239624)Termination reason: Instruction limit % 152.95/21.82 % (239624)Termination phase: Saturation % 152.95/21.82 % (239624)Time elapsed: 8.142 s % 152.95/21.82 % (239624)Peak memory usage: 105 MB % 152.95/21.82 % (239624)Instructions burned: 15853 (million) % 152.95/21.82 % (239993)fmb+10_1_sil=256000:fmbss=7:random_seed=1285817205:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 152.95/21.82 % Exception at run slice level % 152.95/21.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 152.95/21.82 % (239995)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1248141251:i=44625:gsp=on_2833 on theBenchmark for (2833ds/44625Mi) % 152.95/21.82 % (239995)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 152.95/21.82 % Exception at run slice level % 152.95/21.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 152.95/21.82 % (239997)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3738844999:i=160505_2833 on theBenchmark for (2833ds/160505Mi) % 152.95/21.82 % Exception at run slice level % 152.95/21.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 152.95/21.82 % (239999)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3142971650:fmbsr=1.3:i=225729_2833 on theBenchmark for (2833ds/225729Mi) % 152.95/21.82 % Exception at run slice level % 152.95/21.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 152.95/21.82 % (240001)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2427591274:fmbsr=2:i=185024:ins=7_2832 on theBenchmark for (2832ds/185024Mi) % 184.19/26.22 % Exception at run slice level % 184.19/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.19/26.22 % (240003)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3255598654:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 184.19/26.22 % Exception at run slice level % 184.19/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.19/26.22 % (240005)% WARNING: option uhcvi not known. % 184.19/26.22 % (240005)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3570151550:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 184.19/26.22 % (239622)Instruction limit reached! % 184.19/26.22 % (239622)------------------------------ % 184.19/26.22 % (239622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.19/26.22 % (239622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.19/26.22 % (239622)CaDiCaL version: 2.1.3 % 184.19/26.22 % (239622)Termination reason: Instruction limit % 184.19/26.22 % (239622)Termination phase: Saturation % 184.19/26.22 % (239622)Time elapsed: 8.609 s % 184.19/26.22 % (239622)Peak memory usage: 110 MB % 184.19/26.22 % (239622)Instructions burned: 14135 (million) % 184.19/26.22 % (240007)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1645138772:i=176048:add=on:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/176048Mi) % 184.19/26.22 % (239616)Instruction limit reached! % 184.19/26.22 % (239616)------------------------------ % 184.19/26.22 % (239616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.19/26.22 % (239616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.19/26.22 % (239616)CaDiCaL version: 2.1.3 % 184.19/26.22 % (239616)Termination reason: Instruction limit % 184.19/26.22 % (239616)Termination phase: Saturation % 184.19/26.22 % (239616)Time elapsed: 12.141 s % 184.19/26.22 % (239616)Peak memory usage: 85 MB % 184.19/26.22 % (239616)Instructions burned: 20140 (million) % 184.19/26.22 % (240009)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2299609404:i=206:fgj=on:rtra=on_2823 on theBenchmark for (2823ds/206Mi) % 184.19/26.22 % (240009)Instruction limit reached! % 184.19/26.22 % (240009)------------------------------ % 184.19/26.22 % (240009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.19/26.22 % (240009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.19/26.22 % (240009)CaDiCaL version: 2.1.3 % 184.19/26.22 % (240009)Termination reason: Instruction limit % 184.19/26.22 % (240009)Termination phase: Saturation % 184.19/26.22 % (240009)Time elapsed: 0.125 s % 184.19/26.22 % (240009)Peak memory usage: 13 MB % 184.19/26.22 % (240009)Instructions burned: 206 (million) % 184.19/26.22 % (240011)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2410169397:i=232:rtra=on_2822 on theBenchmark for (2822ds/232Mi) % 184.19/26.22 % (240011)Instruction limit reached! % 184.19/26.22 % (240011)------------------------------ % 184.19/26.22 % (240011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.19/26.22 % (240011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.19/26.22 % (240011)CaDiCaL version: 2.1.3 % 184.19/26.22 % (240011)Termination reason: Instruction limit % 184.19/26.22 % (240011)Termination phase: Saturation % 184.19/26.22 % (240011)Time elapsed: 0.143 s % 184.19/26.22 % (240011)Peak memory usage: 14 MB % 184.19/26.22 % (240011)Instructions burned: 233 (million) % 184.19/26.22 % (240013)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=808945010:i=262:rtra=on_2820 on theBenchmark for (2820ds/262Mi) % 184.19/26.22 % (240013)Instruction limit reached! % 184.19/26.22 % (240013)------------------------------ % 184.19/26.22 % (240013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.19/26.22 % (240013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.19/26.22 % (240013)CaDiCaL version: 2.1.3 % 184.19/26.22 % (240013)Termination reason: Instruction limit % 184.19/26.22 % (240013)Termination phase: Saturation % 184.19/26.22 % (240013)Time elapsed: 0.159 s % 184.19/26.22 % (240013)Peak memory usage: 14 MB % 184.19/26.22 % (240013)Instructions burned: 264 (million) % 184.19/26.22 % (240015)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3364848628:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2818 on theBenchmark for (2818ds/318Mi) % 184.19/26.22 % (240015)Instruction limit reached! % 184.19/26.22 % (240015)------------------------------ % 184.19/26.22 % (240015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.61/32.70 % (240015)CaDiCaL version: 2.1.3 % 229.61/32.70 % (240015)Termination reason: Instruction limit % 229.61/32.70 % (240015)Termination phase: Saturation % 229.61/32.70 % (240015)Time elapsed: 0.195 s % 229.61/32.70 % (240015)Peak memory usage: 15 MB % 229.61/32.70 % (240015)Instructions burned: 318 (million) % 229.61/32.70 % (240017)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2845415568:i=1428:nm=2:rtra=on_2816 on theBenchmark for (2816ds/1428Mi) % 229.61/32.70 % Exception at run slice level % 229.61/32.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 229.61/32.70 % (240019)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3847881156:i=262:bd=preordered:rtra=on:fsd=on_2816 on theBenchmark for (2816ds/262Mi) % 229.61/32.70 % (240019)Instruction limit reached! % 229.61/32.70 % (240019)------------------------------ % 229.61/32.70 % (240019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.61/32.70 % (240019)CaDiCaL version: 2.1.3 % 229.61/32.70 % (240019)Termination reason: Instruction limit % 229.61/32.70 % (240019)Termination phase: Saturation % 229.61/32.70 % (240019)Time elapsed: 0.160 s % 229.61/32.70 % (240019)Peak memory usage: 14 MB % 229.61/32.70 % (240019)Instructions burned: 263 (million) % 229.61/32.70 % (240021)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=436635879:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/1368Mi) % 229.61/32.70 % (240021)Instruction limit reached! % 229.61/32.70 % (240021)------------------------------ % 229.61/32.70 % (240021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.61/32.70 % (240021)CaDiCaL version: 2.1.3 % 229.61/32.70 % (240021)Termination reason: Instruction limit % 229.61/32.70 % (240021)Termination phase: Saturation % 229.61/32.70 % (240021)Time elapsed: 0.692 s % 229.61/32.70 % (240021)Peak memory usage: 22 MB % 229.61/32.70 % (240021)Instructions burned: 1369 (million) % 229.61/32.70 % (240023)ott-21_1_sil=16000:si=on:fs=off:random_seed=4269433288:i=360:av=off:fsr=off:rtra=on_2807 on theBenchmark for (2807ds/360Mi) % 229.61/32.70 % (240023)Instruction limit reached! % 229.61/32.70 % (240023)------------------------------ % 229.61/32.70 % (240023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.61/32.70 % (240023)CaDiCaL version: 2.1.3 % 229.61/32.70 % (240023)Termination reason: Instruction limit % 229.61/32.70 % (240023)Termination phase: Saturation % 229.61/32.70 % (240023)Time elapsed: 0.179 s % 229.61/32.70 % (240023)Peak memory usage: 14 MB % 229.61/32.70 % (240023)Instructions burned: 361 (million) % 229.61/32.70 % (240025)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3192086173:i=954:bd=all:rtra=on_2805 on theBenchmark for (2805ds/954Mi) % 229.61/32.70 % (240025)Instruction limit reached! % 229.61/32.70 % (240025)------------------------------ % 229.61/32.70 % (240025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.61/32.70 % (240025)CaDiCaL version: 2.1.3 % 229.61/32.70 % (240025)Termination reason: Instruction limit % 229.61/32.70 % (240025)Termination phase: Saturation % 229.61/32.70 % (240025)Time elapsed: 0.538 s % 229.61/32.70 % (240025)Peak memory usage: 17 MB % 229.61/32.70 % (240025)Instructions burned: 954 (million) % 229.61/32.70 % (240027)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1513766588:fmbsr=1.3:i=1730:ins=25:rtra=on_2799 on theBenchmark for (2799ds/1730Mi) % 229.61/32.70 % Exception at run slice level % 229.61/32.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 229.61/32.70 % (240029)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2438510483:i=2358:rtra=on_2799 on theBenchmark for (2799ds/2358Mi) % 229.61/32.70 % (240029)Instruction limit reached! % 229.61/32.70 % (240029)------------------------------ % 229.61/32.70 % (240029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.61/32.70 % (240029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.23/37.29 % (240029)CaDiCaL version: 2.1.3 % 262.23/37.29 % (240029)Termination reason: Instruction limit % 262.23/37.29 % (240029)Termination phase: Saturation % 262.23/37.29 % (240029)Time elapsed: 1.524 s % 262.23/37.29 % (240029)Peak memory usage: 37 MB % 262.23/37.29 % (240029)Instructions burned: 2358 (million) % 262.23/37.29 % (240031)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2465879252:i=1778:ins=1:rtra=on_2784 on theBenchmark for (2784ds/1778Mi) % 262.23/37.29 % Exception at run slice level % 262.23/37.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 262.23/37.29 % (240033)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=3804468106:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/1384Mi) % 262.23/37.29 % (240033)Instruction limit reached! % 262.23/37.29 % (240033)------------------------------ % 262.23/37.29 % (240033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.23/37.29 % (240033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.23/37.29 % (240033)CaDiCaL version: 2.1.3 % 262.23/37.29 % (240033)Termination reason: Instruction limit % 262.23/37.29 % (240033)Termination phase: Saturation % 262.23/37.29 % (240033)Time elapsed: 0.813 s % 262.23/37.29 % (240033)Peak memory usage: 25 MB % 262.23/37.29 % (240033)Instructions burned: 1385 (million) % 262.23/37.29 % (240035)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2293967549:i=1758:kws=inv_precedence:fsr=off:rtra=on_2775 on theBenchmark for (2775ds/1758Mi) % 262.23/37.29 % (240035)Instruction limit reached! % 262.23/37.29 % (240035)------------------------------ % 262.23/37.29 % (240035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.23/37.29 % (240035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.23/37.29 % (240035)CaDiCaL version: 2.1.3 % 262.23/37.29 % (240035)Termination reason: Instruction limit % 262.23/37.29 % (240035)Termination phase: Saturation % 262.23/37.29 % (240035)Time elapsed: 0.983 s % 262.23/37.29 % (240035)Peak memory usage: 23 MB % 262.23/37.29 % (240035)Instructions burned: 1758 (million) % 262.23/37.29 % (240037)fmb+10_1_sil=64000:si=on:random_seed=965202799:i=44122:nm=2:rtra=on:gsp=on_2765 on theBenchmark for (2765ds/44122Mi) % 262.23/37.29 % (240037)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 262.23/37.29 % Exception at run slice level % 262.23/37.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 262.23/37.29 % (240039)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2262485384:i=19030:nm=5:rtra=on_2765 on theBenchmark for (2765ds/19030Mi) % 262.23/37.29 % Exception at run slice level % 262.23/37.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 262.23/37.29 % (240041)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2739005625:fmbsr=1.7:i=1840:rtra=on_2764 on theBenchmark for (2764ds/1840Mi) % 262.23/37.29 % Exception at run slice level % 262.23/37.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 262.23/37.29 % (240043)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3306729208:i=10262:rtra=on_2764 on theBenchmark for (2764ds/10262Mi) % 262.23/37.29 % (239991)Instruction limit reached! % 262.23/37.29 % (239991)------------------------------ % 262.23/37.29 % (239991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.23/37.29 % (239991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.23/37.29 % (239991)CaDiCaL version: 2.1.3 % 262.23/37.29 % (239991)Termination reason: Instruction limit % 262.23/37.29 % (239991)Termination phase: Saturation % 262.23/37.29 % (239991)Time elapsed: 8.522 s % 262.23/37.29 % (239991)Peak memory usage: 81 MB % 262.23/37.29 % (239991)Instructions burned: 28123 (million) % 262.23/37.29 % (240045)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=227707574:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2749 on theBenchmark for (2749ds/2944Mi) % 262.23/37.29 % (240045)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 262.23/37.29 % (240045)Instruction limit reached! % 262.23/37.29 % (240045)------------------------------ % 262.23/37.29 % (240045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.64 % (240045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.64 % (240045)CaDiCaL version: 2.1.3 % 300.57/42.64 % (240045)Termination reason: Instruction limit % 300.57/42.64 % (240045)Termination phase: Saturation % 300.57/42.64 % (240045)Time elapsed: 0.867 s % 300.57/42.64 % (240045)Peak memory usage: 45 MB % 300.57/42.64 % (240045)Instructions burned: 2946 (million) % 300.57/42.64 % (240047)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=62503178:i=12648:rtra=on_2740 on theBenchmark for (2740ds/12648Mi) % 300.57/42.64 % Exception at run slice level % 300.57/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.57/42.64 % (240049)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2987051400:fmbsr=2.30978:i=4348:rtra=on_2740 on theBenchmark for (2740ds/4348Mi) % 300.57/42.64 % Exception at run slice level % 300.57/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.57/42.64 % (240051)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=290605825:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2739 on theBenchmark for (2739ds/1738Mi) % 300.57/42.64 % (240051)Instruction limit reached! % 300.57/42.64 % (240051)------------------------------ % 300.57/42.64 % (240051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.64 % (240051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.64 % (240051)CaDiCaL version: 2.1.3 % 300.57/42.64 % (240051)Termination reason: Instruction limit % 300.57/42.64 % (240051)Termination phase: Saturation % 300.57/42.64 % (240051)Time elapsed: 0.545 s % 300.57/42.64 % (240051)Peak memory usage: 24 MB % 300.57/42.64 % (240051)Instructions burned: 1739 (million) % 300.57/42.64 % (240053)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=332102049:i=10228:av=off:rtra=on_2734 on theBenchmark for (2734ds/10228Mi) % 300.57/42.64 % (240043)Instruction limit reached! % 300.57/42.64 % (240043)------------------------------ % 300.57/42.64 % (240043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.64 % (240043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.64 % (240043)CaDiCaL version: 2.1.3 % 300.57/42.64 % (240043)Termination reason: Instruction limit % 300.57/42.64 % (240043)Termination phase: Saturation % 300.57/42.64 % (240043)Time elapsed: 5.998 s % 300.57/42.64 % (240043)Peak memory usage: 56 MB % 300.57/42.64 % (240043)Instructions burned: 10263 (million) % 300.57/42.64 % (240117)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2797376522:i=108564:rtra=on_2704 on theBenchmark for (2704ds/108564Mi) % 300.57/42.64 % Exception at run slice level % 300.57/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.57/42.64 % (240119)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2719220136:i=7024:aac=none:rtra=on_2703 on theBenchmark for (2703ds/7024Mi) % 300.57/42.64 % (239538)Instruction limit reached! % 300.57/42.64 % (239538)------------------------------ % 300.57/42.64 % (239538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.64 % (239538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.64 % (239538)CaDiCaL version: 2.1.3 % 300.57/42.64 % (239538)Termination reason: Instruction limit % 300.57/42.64 % (239538)Termination phase: Saturation % 300.57/42.64 % (239538)Time elapsed: 30.196 s % 300.57/42.64 % (239538)Peak memory usage: 109 MB % 300.57/42.64 % (239538)Instructions burned: 88027 (million) % 300.57/42.64 % (240053)Instruction limit reached! % 300.57/42.64 % (240053)------------------------------ % 300.57/42.64 % (240053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.64 % (240053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.64 % (240053)CaDiCaL version: 2.1.3 % 300.57/42.64 % (240053)Termination reason: Instruction limit % 300.57/42.64 % (240053)Termination phase: Saturation % 300.57/42.64 % (240053)Time elapsed: 3.640 s % 300.57/42.64 % (240053)Peak memory usage: 90 MB % 300.57/42.64 % (240053)Instructions burned: 10230 (million) % 300.57/42.64 % (240121)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=466837476:i=7546:rtra=on:amm=off_2697 on theBenchmark for (2697ds/7546Mi) % 300.57/42.64 % (240122)ott+11_1_sil=16000:si=on:gs=on:random_seed=3766336962:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2697 on theBenchmark for (2697ds/4502Mi) % 300.57/42.64 % (240122)Instruction limit reached! % 300.57/42.64 % (240122)--------------- % 300.57/42.64 Terminated % 300.57/42.64 % Vampire exiting % 300.57/42.64 Terminated %------------------------------------------------------------------------------