%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW477_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 : n010.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:16 PM UTC 2026 % Result : Timeout 300.66s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW477_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.19 % Computer : n010.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:13:17 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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 % 6.67/1.22 % (1943114)Will run a generic schedule for satisfiability detection. % 6.67/1.22 % (1943122)dis+10_1_sil=32000:sp=arity:random_seed=2341586944:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.67/1.22 % (1943120)% WARNING: option uhcvi not known. % 6.67/1.22 % (1943119)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2958802051_2999 on theBenchmark for (2999ds/0Mi) % 6.67/1.22 % (1943120)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3348674295:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.67/1.22 % (1943121)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4274546872:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.67/1.22 % (1943124)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3685231919:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.67/1.22 % (1943123)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4142739000:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.67/1.22 % (1943125)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=208014684:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.67/1.22 % Exception at run slice level % 6.67/1.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.67/1.22 % (1943122)Instruction limit reached! % 6.67/1.22 % (1943122)------------------------------ % 6.67/1.22 % (1943122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.67/1.22 % (1943122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.67/1.22 % (1943122)CaDiCaL version: 2.1.3 % 6.67/1.22 % (1943122)Termination reason: Instruction limit % 6.67/1.22 % (1943122)Termination phase: Saturation % 6.67/1.22 % (1943122)Time elapsed: 0.032 s % 6.67/1.22 % (1943122)Peak memory usage: 12 MB % 6.67/1.22 % (1943122)Instructions burned: 105 (million) % 6.67/1.22 % (1943133)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3737154960:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.67/1.22 % Exception at run slice level % 6.67/1.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.67/1.22 % (1943134)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1120819979:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.67/1.22 % (1943136)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=3877963683:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.67/1.22 % (1943125)Instruction limit reached! % 6.67/1.22 % (1943125)------------------------------ % 6.67/1.22 % (1943125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.67/1.22 % (1943125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.67/1.22 % (1943125)CaDiCaL version: 2.1.3 % 6.67/1.22 % (1943125)Termination reason: Instruction limit % 6.67/1.22 % (1943125)Termination phase: Saturation % 6.67/1.22 % (1943125)Time elapsed: 0.057 s % 6.67/1.22 % (1943125)Peak memory usage: 12 MB % 6.67/1.22 % (1943125)Instructions burned: 161 (million) % 6.67/1.22 % (1943123)Instruction limit reached! % 6.67/1.22 % (1943123)------------------------------ % 6.67/1.22 % (1943123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.67/1.22 % (1943123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.67/1.22 % (1943123)CaDiCaL version: 2.1.3 % 6.67/1.22 % (1943123)Termination reason: Instruction limit % 6.67/1.22 % (1943123)Termination phase: Saturation % 6.67/1.22 % (1943123)Time elapsed: 0.066 s % 6.67/1.22 % (1943123)Peak memory usage: 12 MB % 6.67/1.22 % (1943123)Instructions burned: 121 (million) % 6.67/1.22 % (1943124)Instruction limit reached! % 6.67/1.22 % (1943124)------------------------------ % 6.67/1.22 % (1943124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.67/1.22 % (1943124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.67/1.22 % (1943124)CaDiCaL version: 2.1.3 % 6.67/1.22 % (1943124)Termination reason: Instruction limit % 6.67/1.22 % (1943124)Termination phase: Saturation % 6.67/1.22 % (1943124)Time elapsed: 0.076 s % 6.67/1.22 % (1943124)Peak memory usage: 13 MB % 6.67/1.22 % (1943124)Instructions burned: 131 (million) % 6.67/1.22 % (1943139)ott-21_1_sil=16000:fs=off:random_seed=578156316:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.67/1.22 % (1943134)Instruction limit reached! % 16.48/2.68 % (1943134)------------------------------ % 16.48/2.68 % (1943134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.48/2.68 % (1943134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.68 % (1943134)CaDiCaL version: 2.1.3 % 16.48/2.68 % (1943134)Termination reason: Instruction limit % 16.48/2.68 % (1943134)Termination phase: Saturation % 16.48/2.68 % (1943134)Time elapsed: 0.042 s % 16.48/2.68 % (1943134)Peak memory usage: 13 MB % 16.48/2.68 % (1943134)Instructions burned: 132 (million) % 16.48/2.68 % (1943140)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3851022511:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 16.48/2.68 % (1943143)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1255694049:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 16.48/2.68 % (1943141)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1026751869:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 16.48/2.68 % Exception at run slice level % 16.48/2.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.48/2.68 % (1943147)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2253716355:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 16.48/2.68 % Exception at run slice level % 16.48/2.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.48/2.68 % (1943149)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=278686696: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) % 16.48/2.68 % (1943139)Instruction limit reached! % 16.48/2.68 % (1943139)------------------------------ % 16.48/2.68 % (1943139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.48/2.68 % (1943139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.68 % (1943139)CaDiCaL version: 2.1.3 % 16.48/2.68 % (1943139)Termination reason: Instruction limit % 16.48/2.68 % (1943139)Termination phase: Saturation % 16.48/2.68 % (1943139)Time elapsed: 0.104 s % 16.48/2.68 % (1943139)Peak memory usage: 12 MB % 16.48/2.68 % (1943139)Instructions burned: 181 (million) % 16.48/2.68 % (1943151)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2046144670:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.48/2.68 % (1943140)Instruction limit reached! % 16.48/2.68 % (1943140)------------------------------ % 16.48/2.68 % (1943140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.48/2.68 % (1943140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.68 % (1943140)CaDiCaL version: 2.1.3 % 16.48/2.68 % (1943140)Termination reason: Instruction limit % 16.48/2.68 % (1943140)Termination phase: Saturation % 16.48/2.68 % (1943140)Time elapsed: 0.248 s % 16.48/2.68 % (1943140)Peak memory usage: 16 MB % 16.48/2.68 % (1943140)Instructions burned: 478 (million) % 16.48/2.68 % (1943153)fmb+10_1_sil=64000:random_seed=568193969:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.48/2.68 % (1943153)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.48/2.68 % Exception at run slice level % 16.48/2.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.48/2.68 % (1943155)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=327923904:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 16.48/2.68 % Exception at run slice level % 16.48/2.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.48/2.68 % (1943157)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=142041672:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.48/2.68 % Exception at run slice level % 16.48/2.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.48/2.68 % (1943159)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=189846596:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.48/2.68 % (1943143)Instruction limit reached! % 16.48/2.68 % (1943143)------------------------------ % 16.48/2.68 % (1943143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.48/2.68 % (1943143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.02/8.73 % (1943143)CaDiCaL version: 2.1.3 % 60.02/8.73 % (1943143)Termination reason: Instruction limit % 60.02/8.73 % (1943143)Termination phase: Saturation % 60.02/8.73 % (1943143)Time elapsed: 0.345 s % 60.02/8.73 % (1943143)Peak memory usage: 19 MB % 60.02/8.73 % (1943143)Instructions burned: 1180 (million) % 60.02/8.73 % (1943136)Instruction limit reached! % 60.02/8.73 % (1943136)------------------------------ % 60.02/8.73 % (1943136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.02/8.73 % (1943136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.02/8.73 % (1943136)CaDiCaL version: 2.1.3 % 60.02/8.73 % (1943136)Termination reason: Instruction limit % 60.02/8.73 % (1943136)Termination phase: Saturation % 60.02/8.73 % (1943136)Time elapsed: 0.387 s % 60.02/8.73 % (1943136)Peak memory usage: 17 MB % 60.02/8.73 % (1943136)Instructions burned: 684 (million) % 60.02/8.73 % (1943161)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1404512178:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 60.02/8.73 % (1943161)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.02/8.73 % (1943162)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=377221769:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 60.02/8.73 % Exception at run slice level % 60.02/8.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.02/8.73 % (1943165)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3387200889:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 60.02/8.73 % Exception at run slice level % 60.02/8.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.02/8.73 % (1943167)ott-2_1_sil=16000:newcnf=on:random_seed=1358375052:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 60.02/8.73 % (1943149)Instruction limit reached! % 60.02/8.73 % (1943149)------------------------------ % 60.02/8.73 % (1943149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.02/8.73 % (1943149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.02/8.73 % (1943149)CaDiCaL version: 2.1.3 % 60.02/8.73 % (1943149)Termination reason: Instruction limit % 60.02/8.73 % (1943149)Termination phase: Saturation % 60.02/8.73 % (1943149)Time elapsed: 0.379 s % 60.02/8.73 % (1943149)Peak memory usage: 17 MB % 60.02/8.73 % (1943149)Instructions burned: 693 (million) % 60.02/8.73 % (1943169)ott+10_1_sil=32000:tgt=ground:random_seed=3562566243:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 60.02/8.73 % (1943151)Instruction limit reached! % 60.02/8.73 % (1943151)------------------------------ % 60.02/8.73 % (1943151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.02/8.73 % (1943151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.02/8.73 % (1943151)CaDiCaL version: 2.1.3 % 60.02/8.73 % (1943151)Termination reason: Instruction limit % 60.02/8.73 % (1943151)Termination phase: Saturation % 60.02/8.73 % (1943151)Time elapsed: 0.483 s % 60.02/8.73 % (1943151)Peak memory usage: 18 MB % 60.02/8.73 % (1943151)Instructions burned: 879 (million) % 60.02/8.73 % (1943171)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2053292863:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 60.02/8.73 % Exception at run slice level % 60.02/8.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.02/8.73 % (1943173)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1274228890:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 60.02/8.73 % (1943167)Instruction limit reached! % 60.02/8.73 % (1943167)------------------------------ % 60.02/8.73 % (1943167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.02/8.73 % (1943167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.02/8.73 % (1943167)CaDiCaL version: 2.1.3 % 60.02/8.73 % (1943167)Termination reason: Instruction limit % 60.02/8.73 % (1943167)Termination phase: Saturation % 60.02/8.73 % (1943167)Time elapsed: 0.277 s % 60.02/8.73 % (1943167)Peak memory usage: 12 MB % 60.02/8.73 % (1943167)Instructions burned: 869 (million) % 60.02/8.73 % (1943175)dis+21_1_sil=32000:sas=cadical:random_seed=930588869:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 60.02/8.73 % (1943161)Instruction limit reached! % 60.02/8.73 % (1943161)------------------------------ % 60.02/8.73 % (1943161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.71/15.16 % (1943161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.71/15.16 % (1943161)CaDiCaL version: 2.1.3 % 105.71/15.16 % (1943161)Termination reason: Instruction limit % 105.71/15.16 % (1943161)Termination phase: Saturation % 105.71/15.16 % (1943161)Time elapsed: 0.493 s % 105.71/15.16 % (1943161)Peak memory usage: 37 MB % 105.71/15.16 % (1943161)Instructions burned: 1472 (million) % 105.71/15.16 % (1943177)ott+11_1_sil=16000:gs=on:random_seed=757887569:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi) % 105.71/15.16 % (1943177)Instruction limit reached! % 105.71/15.16 % (1943177)------------------------------ % 105.71/15.16 % (1943177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.71/15.16 % (1943177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.71/15.16 % (1943177)CaDiCaL version: 2.1.3 % 105.71/15.16 % (1943177)Termination reason: Instruction limit % 105.71/15.16 % (1943177)Termination phase: Saturation % 105.71/15.16 % (1943177)Time elapsed: 0.666 s % 105.71/15.16 % (1943177)Peak memory usage: 26 MB % 105.71/15.16 % (1943177)Instructions burned: 2252 (million) % 105.71/15.16 % (1943179)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2622792084:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 105.71/15.16 % Exception at run slice level % 105.71/15.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.71/15.16 % (1943181)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2347749686:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 105.71/15.16 % (1943159)Instruction limit reached! % 105.71/15.16 % (1943159)------------------------------ % 105.71/15.16 % (1943159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.71/15.16 % (1943159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.71/15.16 % (1943159)CaDiCaL version: 2.1.3 % 105.71/15.16 % (1943159)Termination reason: Instruction limit % 105.71/15.16 % (1943159)Termination phase: Saturation % 105.71/15.16 % (1943159)Time elapsed: 1.645 s % 105.71/15.16 % (1943159)Peak memory usage: 14 MB % 105.71/15.16 % (1943159)Instructions burned: 5135 (million) % 105.71/15.16 % (1943183)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4248023029:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 105.71/15.16 % (1943173)Instruction limit reached! % 105.71/15.16 % (1943173)------------------------------ % 105.71/15.16 % (1943173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.71/15.16 % (1943173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.71/15.16 % (1943173)CaDiCaL version: 2.1.3 % 105.71/15.16 % (1943173)Termination reason: Instruction limit % 105.71/15.16 % (1943173)Termination phase: Saturation % 105.71/15.16 % (1943173)Time elapsed: 1.569 s % 105.71/15.16 % (1943173)Peak memory usage: 22 MB % 105.71/15.16 % (1943173)Instructions burned: 3512 (million) % 105.71/15.16 % (1943185)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3051469452:i=5211_2976 on theBenchmark for (2976ds/5211Mi) % 105.71/15.16 % (1943181)Instruction limit reached! % 105.71/15.16 % (1943181)------------------------------ % 105.71/15.16 % (1943181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.71/15.16 % (1943181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.71/15.16 % (1943181)CaDiCaL version: 2.1.3 % 105.71/15.16 % (1943181)Termination reason: Instruction limit % 105.71/15.16 % (1943181)Termination phase: Saturation % 105.71/15.16 % (1943181)Time elapsed: 0.715 s % 105.71/15.16 % (1943181)Peak memory usage: 12 MB % 105.71/15.16 % (1943181)Instructions burned: 4595 (million) % 105.71/15.16 % (1943187)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1723644118:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi) % 105.71/15.16 % Exception at run slice level % 105.71/15.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.71/15.16 % (1943189)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3203925556:fmbsr=2:i=46332_2975 on theBenchmark for (2975ds/46332Mi) % 105.71/15.16 % Exception at run slice level % 105.71/15.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.71/15.16 % (1943191)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=404164070:i=14071_2975 on theBenchmark for (2975ds/14071Mi) % 105.71/15.16 % Exception at run slice level % 124.36/17.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.36/17.95 % (1943193)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=707931997:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi) % 124.36/17.95 % (1943175)Instruction limit reached! % 124.36/17.95 % (1943175)------------------------------ % 124.36/17.95 % (1943175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943175)CaDiCaL version: 2.1.3 % 124.36/17.95 % (1943175)Termination reason: Instruction limit % 124.36/17.95 % (1943175)Termination phase: Saturation % 124.36/17.95 % (1943175)Time elapsed: 2.119 s % 124.36/17.95 % (1943175)Peak memory usage: 25 MB % 124.36/17.95 % (1943175)Instructions burned: 3773 (million) % 124.36/17.95 % (1943195)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=345516714:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi) % 124.36/17.95 % (1943169)Instruction limit reached! % 124.36/17.95 % (1943169)------------------------------ % 124.36/17.95 % (1943169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943169)CaDiCaL version: 2.1.3 % 124.36/17.95 % (1943169)Termination reason: Instruction limit % 124.36/17.95 % (1943169)Termination phase: Saturation % 124.36/17.95 % (1943169)Time elapsed: 3.034 s % 124.36/17.95 % (1943169)Peak memory usage: 37 MB % 124.36/17.95 % (1943169)Instructions burned: 5115 (million) % 124.36/17.95 % (1943197)dis+10_16:1_sil=16000:random_seed=217964210:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 124.36/17.95 % (1943185)Instruction limit reached! % 124.36/17.95 % (1943185)------------------------------ % 124.36/17.95 % (1943185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943185)CaDiCaL version: 2.1.3 % 124.36/17.95 % (1943185)Termination reason: Instruction limit % 124.36/17.95 % (1943185)Termination phase: Saturation % 124.36/17.95 % (1943185)Time elapsed: 2.678 s % 124.36/17.95 % (1943185)Peak memory usage: 54 MB % 124.36/17.95 % (1943185)Instructions burned: 5211 (million) % 124.36/17.95 % (1943199)ott-3_8_sil=64000:random_seed=2322177729:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 124.36/17.95 % (1943193)Instruction limit reached! % 124.36/17.95 % (1943193)------------------------------ % 124.36/17.95 % (1943193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943193)CaDiCaL version: 2.1.3 % 124.36/17.95 % (1943193)Termination reason: Instruction limit % 124.36/17.95 % (1943193)Termination phase: Saturation % 124.36/17.95 % (1943193)Time elapsed: 3.598 s % 124.36/17.95 % (1943193)Peak memory usage: 55 MB % 124.36/17.95 % (1943193)Instructions burned: 22569 (million) % 124.36/17.95 % (1943201)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=58348984:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi) % 124.36/17.95 % Exception at run slice level % 124.36/17.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.36/17.95 % (1943203)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2659555593:i=11404_2939 on theBenchmark for (2939ds/11404Mi) % 124.36/17.95 % (1943195)Instruction limit reached! % 124.36/17.95 % (1943195)------------------------------ % 124.36/17.95 % (1943195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943195)CaDiCaL version: 2.1.3 % 124.36/17.95 % (1943195)Termination reason: Instruction limit % 124.36/17.95 % (1943195)Termination phase: Saturation % 124.36/17.95 % (1943195)Time elapsed: 4.755 s % 124.36/17.95 % (1943195)Peak memory usage: 71 MB % 124.36/17.95 % (1943195)Instructions burned: 8173 (million) % 124.36/17.95 % (1943205)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3856149067:i=14134_2922 on theBenchmark for (2922ds/14134Mi) % 124.36/17.95 % (1943197)Instruction limit reached! % 124.36/17.95 % (1943197)------------------------------ % 124.36/17.95 % (1943197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.95 % (1943197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.95 % (1943197)CaDiCaL version: 2.1.3 % 139.02/19.93 % (1943197)Termination reason: Instruction limit % 139.02/19.93 % (1943197)Termination phase: Saturation % 139.02/19.93 % (1943197)Time elapsed: 4.850 s % 139.02/19.93 % (1943197)Peak memory usage: 34 MB % 139.02/19.93 % (1943197)Instructions burned: 9157 (million) % 139.02/19.93 % (1943207)dis+33_16_sil=32000:sac=on:random_seed=266314155:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 139.02/19.93 % (1943203)Instruction limit reached! % 139.02/19.93 % (1943203)------------------------------ % 139.02/19.93 % (1943203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.02/19.93 % (1943203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.02/19.93 % (1943203)CaDiCaL version: 2.1.3 % 139.02/19.93 % (1943203)Termination reason: Instruction limit % 139.02/19.93 % (1943203)Termination phase: Saturation % 139.02/19.93 % (1943203)Time elapsed: 3.486 s % 139.02/19.93 % (1943203)Peak memory usage: 68 MB % 139.02/19.93 % (1943203)Instructions burned: 11407 (million) % 139.02/19.93 % (1943209)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=945404555:avsq=on:i=17627:add=on:amm=off_2904 on theBenchmark for (2904ds/17627Mi) % 139.02/19.93 % (1943199)Instruction limit reached! % 139.02/19.93 % (1943199)------------------------------ % 139.02/19.93 % (1943199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.02/19.93 % (1943199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.02/19.93 % (1943199)CaDiCaL version: 2.1.3 % 139.02/19.93 % (1943199)Termination reason: Instruction limit % 139.02/19.93 % (1943199)Termination phase: Saturation % 139.02/19.93 % (1943199)Time elapsed: 5.756 s % 139.02/19.93 % (1943199)Peak memory usage: 12 MB % 139.02/19.93 % (1943199)Instructions burned: 20140 (million) % 139.02/19.93 % (1943211)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=578503610:s2a=on:i=53295_2891 on theBenchmark for (2891ds/53295Mi) % 139.02/19.93 % (1943205)Instruction limit reached! % 139.02/19.93 % (1943205)------------------------------ % 139.02/19.93 % (1943205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.02/19.93 % (1943205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.02/19.93 % (1943205)CaDiCaL version: 2.1.3 % 139.02/19.93 % (1943205)Termination reason: Instruction limit % 139.02/19.93 % (1943205)Termination phase: Saturation % 139.02/19.93 % (1943205)Time elapsed: 4.054 s % 139.02/19.93 % (1943205)Peak memory usage: 12 MB % 139.02/19.93 % (1943205)Instructions burned: 14137 (million) % 139.02/19.93 % (1943213)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1479572859:i=26857:ins=20_2881 on theBenchmark for (2881ds/26857Mi) % 139.02/19.93 % Exception at run slice level % 139.02/19.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 139.02/19.93 % (1943215)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1008667445:i=28120:bs=on:fsr=off_2881 on theBenchmark for (2881ds/28120Mi) % 139.02/19.93 % (1943209)Instruction limit reached! % 139.02/19.93 % (1943209)------------------------------ % 139.02/19.93 % (1943209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.02/19.93 % (1943209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.02/19.93 % (1943209)CaDiCaL version: 2.1.3 % 139.02/19.93 % (1943209)Termination reason: Instruction limit % 139.02/19.93 % (1943209)Termination phase: Saturation % 139.02/19.93 % (1943209)Time elapsed: 5.238 s % 139.02/19.93 % (1943209)Peak memory usage: 179 MB % 139.02/19.93 % (1943209)Instructions burned: 17630 (million) % 139.02/19.93 % (1943217)fmb+10_1_sil=256000:fmbss=7:random_seed=1408966940:fmbsr=1.6:i=182295_2851 on theBenchmark for (2851ds/182295Mi) % 139.02/19.93 % Exception at run slice level % 139.02/19.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 139.02/19.93 % (1943219)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3754461853:i=44625:gsp=on_2851 on theBenchmark for (2851ds/44625Mi) % 139.02/19.93 % (1943219)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 139.02/19.93 % Exception at run slice level % 139.02/19.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 139.02/19.93 % (1943221)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=708132974:i=160505_2850 on theBenchmark for (2850ds/160505Mi) % 139.02/19.93 % Exception at run slice level % 139.02/19.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 139.02/19.93 % (1943223)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3363500834:fmbsr=1.3:i=225729_2850 on theBenchmark for (2850ds/225729Mi) % 187.78/26.76 % Exception at run slice level % 187.78/26.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 187.78/26.76 % (1943225)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3724370997:fmbsr=2:i=185024:ins=7_2850 on theBenchmark for (2850ds/185024Mi) % 187.78/26.76 % Exception at run slice level % 187.78/26.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 187.78/26.76 % (1943227)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3214874678:rtra=on_2850 on theBenchmark for (2850ds/0Mi) % 187.78/26.76 % Exception at run slice level % 187.78/26.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 187.78/26.76 % (1943229)% WARNING: option uhcvi not known. % 187.78/26.76 % (1943229)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2641136457:i=271062:add=off:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/271062Mi) % 187.78/26.76 % (1943207)Instruction limit reached! % 187.78/26.76 % (1943207)------------------------------ % 187.78/26.76 % (1943207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.78/26.76 % (1943207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.78/26.76 % (1943207)CaDiCaL version: 2.1.3 % 187.78/26.76 % (1943207)Termination reason: Instruction limit % 187.78/26.76 % (1943207)Termination phase: Saturation % 187.78/26.76 % (1943207)Time elapsed: 8.311 s % 187.78/26.76 % (1943207)Peak memory usage: 77 MB % 187.78/26.76 % (1943207)Instructions burned: 15853 (million) % 187.78/26.76 % (1943231)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2687315640:i=176048:add=on:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/176048Mi) % 187.78/26.76 % (1943183)Instruction limit reached! % 187.78/26.76 % (1943183)------------------------------ % 187.78/26.76 % (1943183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.78/26.76 % (1943183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.78/26.76 % (1943183)CaDiCaL version: 2.1.3 % 187.78/26.76 % (1943183)Termination reason: Instruction limit % 187.78/26.76 % (1943183)Termination phase: Saturation % 187.78/26.76 % (1943183)Time elapsed: 15.081 s % 187.78/26.76 % (1943183)Peak memory usage: 123 MB % 187.78/26.76 % (1943183)Instructions burned: 29341 (million) % 187.78/26.76 % (1943233)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2198646132:i=206:fgj=on:rtra=on_2827 on theBenchmark for (2827ds/206Mi) % 187.78/26.76 % (1943233)Instruction limit reached! % 187.78/26.76 % (1943233)------------------------------ % 187.78/26.76 % (1943233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.78/26.76 % (1943233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.78/26.76 % (1943233)CaDiCaL version: 2.1.3 % 187.78/26.76 % (1943233)Termination reason: Instruction limit % 187.78/26.76 % (1943233)Termination phase: Saturation % 187.78/26.76 % (1943233)Time elapsed: 0.121 s % 187.78/26.76 % (1943233)Peak memory usage: 13 MB % 187.78/26.76 % (1943233)Instructions burned: 208 (million) % 187.78/26.76 % (1943235)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1131993923:i=232:rtra=on_2826 on theBenchmark for (2826ds/232Mi) % 187.78/26.76 % (1943235)Instruction limit reached! % 187.78/26.76 % (1943235)------------------------------ % 187.78/26.76 % (1943235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.78/26.76 % (1943235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.78/26.76 % (1943235)CaDiCaL version: 2.1.3 % 187.78/26.76 % (1943235)Termination reason: Instruction limit % 187.78/26.76 % (1943235)Termination phase: Saturation % 187.78/26.76 % (1943235)Time elapsed: 0.135 s % 187.78/26.76 % (1943235)Peak memory usage: 13 MB % 187.78/26.76 % (1943235)Instructions burned: 233 (million) % 187.78/26.76 % (1943237)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=979815556:i=262:rtra=on_2824 on theBenchmark for (2824ds/262Mi) % 187.78/26.76 % (1943237)Instruction limit reached! % 187.78/26.76 % (1943237)------------------------------ % 187.78/26.76 % (1943237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.78/26.76 % (1943237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.78/26.76 % (1943237)CaDiCaL version: 2.1.3 % 187.78/26.76 % (1943237)Termination reason: Instruction limit % 187.78/26.76 % (1943237)Termination phase: Saturation % 228.23/32.49 % (1943237)Time elapsed: 0.157 s % 228.23/32.49 % (1943237)Peak memory usage: 14 MB % 228.23/32.49 % (1943237)Instructions burned: 263 (million) % 228.23/32.49 % (1943239)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=898240214:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2822 on theBenchmark for (2822ds/318Mi) % 228.23/32.49 % (1943239)Instruction limit reached! % 228.23/32.49 % (1943239)------------------------------ % 228.23/32.49 % (1943239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.23/32.49 % (1943239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.23/32.49 % (1943239)CaDiCaL version: 2.1.3 % 228.23/32.49 % (1943239)Termination reason: Instruction limit % 228.23/32.49 % (1943239)Termination phase: Saturation % 228.23/32.49 % (1943239)Time elapsed: 0.194 s % 228.23/32.49 % (1943239)Peak memory usage: 14 MB % 228.23/32.49 % (1943239)Instructions burned: 318 (million) % 228.23/32.49 % (1943241)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3197022537:i=1428:nm=2:rtra=on_2820 on theBenchmark for (2820ds/1428Mi) % 228.23/32.49 % Exception at run slice level % 228.23/32.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 228.23/32.49 % (1943243)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1473611196:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi) % 228.23/32.49 % (1943243)Instruction limit reached! % 228.23/32.49 % (1943243)------------------------------ % 228.23/32.49 % (1943243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.23/32.49 % (1943243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.23/32.49 % (1943243)CaDiCaL version: 2.1.3 % 228.23/32.49 % (1943243)Termination reason: Instruction limit % 228.23/32.49 % (1943243)Termination phase: Saturation % 228.23/32.49 % (1943243)Time elapsed: 0.155 s % 228.23/32.49 % (1943243)Peak memory usage: 15 MB % 228.23/32.49 % (1943243)Instructions burned: 262 (million) % 228.23/32.49 % (1943245)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=2902650318:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/1368Mi) % 228.23/32.49 % (1943245)Instruction limit reached! % 228.23/32.49 % (1943245)------------------------------ % 228.23/32.49 % (1943245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.23/32.49 % (1943245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.23/32.49 % (1943245)CaDiCaL version: 2.1.3 % 228.23/32.49 % (1943245)Termination reason: Instruction limit % 228.23/32.49 % (1943245)Termination phase: Saturation % 228.23/32.49 % (1943245)Time elapsed: 0.779 s % 228.23/32.49 % (1943245)Peak memory usage: 21 MB % 228.23/32.49 % (1943245)Instructions burned: 1370 (million) % 228.23/32.49 % (1943247)ott-21_1_sil=16000:si=on:fs=off:random_seed=1085001003:i=360:av=off:fsr=off:rtra=on_2810 on theBenchmark for (2810ds/360Mi) % 228.23/32.49 % (1943247)Instruction limit reached! % 228.23/32.49 % (1943247)------------------------------ % 228.23/32.49 % (1943247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.23/32.49 % (1943247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.23/32.49 % (1943247)CaDiCaL version: 2.1.3 % 228.23/32.49 % (1943247)Termination reason: Instruction limit % 228.23/32.49 % (1943247)Termination phase: Saturation % 228.23/32.49 % (1943247)Time elapsed: 0.202 s % 228.23/32.49 % (1943247)Peak memory usage: 13 MB % 228.23/32.49 % (1943247)Instructions burned: 361 (million) % 228.23/32.49 % (1943249)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2514521061:i=954:bd=all:rtra=on_2808 on theBenchmark for (2808ds/954Mi) % 228.23/32.49 % (1943249)Instruction limit reached! % 228.23/32.49 % (1943249)------------------------------ % 228.23/32.49 % (1943249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.23/32.49 % (1943249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.23/32.49 % (1943249)CaDiCaL version: 2.1.3 % 228.23/32.49 % (1943249)Termination reason: Instruction limit % 228.23/32.49 % (1943249)Termination phase: Saturation % 228.23/32.49 % (1943249)Time elapsed: 0.485 s % 228.23/32.49 % (1943249)Peak memory usage: 18 MB % 228.23/32.49 % (1943249)Instructions burned: 955 (million) % 228.23/32.49 % (1943251)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4031083752:fmbsr=1.3:i=1730:ins=25:rtra=on_2803 on theBenchmark for (2803ds/1730Mi) % 228.23/32.49 % Exception at run slice level % 228.23/32.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.91/36.36 % (1943253)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=52799374:i=2358:rtra=on_2802 on theBenchmark for (2802ds/2358Mi) % 255.91/36.36 % (1943253)Instruction limit reached! % 255.91/36.36 % (1943253)------------------------------ % 255.91/36.36 % (1943253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.91/36.36 % (1943253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.91/36.36 % (1943253)CaDiCaL version: 2.1.3 % 255.91/36.36 % (1943253)Termination reason: Instruction limit % 255.91/36.36 % (1943253)Termination phase: Saturation % 255.91/36.36 % (1943253)Time elapsed: 1.416 s % 255.91/36.36 % (1943253)Peak memory usage: 24 MB % 255.91/36.36 % (1943253)Instructions burned: 2359 (million) % 255.91/36.36 % (1943255)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4099982616:i=1778:ins=1:rtra=on_2788 on theBenchmark for (2788ds/1778Mi) % 255.91/36.36 % Exception at run slice level % 255.91/36.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.91/36.36 % (1943257)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=166152753:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/1384Mi) % 255.91/36.36 % (1943257)Instruction limit reached! % 255.91/36.36 % (1943257)------------------------------ % 255.91/36.36 % (1943257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.91/36.36 % (1943257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.91/36.36 % (1943257)CaDiCaL version: 2.1.3 % 255.91/36.36 % (1943257)Termination reason: Instruction limit % 255.91/36.36 % (1943257)Termination phase: Saturation % 255.91/36.36 % (1943257)Time elapsed: 0.816 s % 255.91/36.36 % (1943257)Peak memory usage: 22 MB % 255.91/36.36 % (1943257)Instructions burned: 1385 (million) % 255.91/36.36 % (1943259)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=102462912:i=1758:kws=inv_precedence:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/1758Mi) % 255.91/36.36 % (1943259)Instruction limit reached! % 255.91/36.36 % (1943259)------------------------------ % 255.91/36.36 % (1943259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.91/36.36 % (1943259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.91/36.36 % (1943259)CaDiCaL version: 2.1.3 % 255.91/36.36 % (1943259)Termination reason: Instruction limit % 255.91/36.36 % (1943259)Termination phase: Saturation % 255.91/36.36 % (1943259)Time elapsed: 1.012 s % 255.91/36.36 % (1943259)Peak memory usage: 24 MB % 255.91/36.36 % (1943259)Instructions burned: 1758 (million) % 255.91/36.36 % (1943261)fmb+10_1_sil=64000:si=on:random_seed=2485794441:i=44122:nm=2:rtra=on:gsp=on_2769 on theBenchmark for (2769ds/44122Mi) % 255.91/36.36 % (1943261)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 255.91/36.36 % Exception at run slice level % 255.91/36.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.91/36.36 % (1943263)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1427321410:i=19030:nm=5:rtra=on_2769 on theBenchmark for (2769ds/19030Mi) % 255.91/36.36 % Exception at run slice level % 255.91/36.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.91/36.36 % (1943265)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3447985116:fmbsr=1.7:i=1840:rtra=on_2769 on theBenchmark for (2769ds/1840Mi) % 255.91/36.36 % Exception at run slice level % 255.91/36.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.91/36.36 % (1943267)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3142289714:i=10262:rtra=on_2768 on theBenchmark for (2768ds/10262Mi) % 255.91/36.36 % (1943267)Instruction limit reached! % 255.91/36.36 % (1943267)------------------------------ % 255.91/36.36 % (1943267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.91/36.36 % (1943267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.91/36.36 % (1943267)CaDiCaL version: 2.1.3 % 255.91/36.36 % (1943267)Termination reason: Instruction limit % 255.91/36.36 % (1943267)Termination phase: Saturation % 255.91/36.36 % (1943267)Time elapsed: 3.380 s % 255.91/36.36 % (1943267)Peak memory usage: 14 MB % 255.91/36.36 % (1943267)Instructions burned: 10262 (million) % 300.66/42.63 % (1943269)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1277417032:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2734 on theBenchmark for (2734ds/2944Mi) % 300.66/42.63 % (1943269)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.66/42.63 % (1943215)Instruction limit reached! % 300.66/42.63 % (1943215)------------------------------ % 300.66/42.63 % (1943215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (1943215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (1943215)CaDiCaL version: 2.1.3 % 300.66/42.63 % (1943215)Termination reason: Instruction limit % 300.66/42.63 % (1943215)Termination phase: Saturation % 300.66/42.63 % (1943215)Time elapsed: 15.508 s % 300.66/42.63 % (1943215)Peak memory usage: 106 MB % 300.66/42.63 % (1943215)Instructions burned: 28120 (million) % 300.66/42.63 % (1943271)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2844774538:i=12648:rtra=on_2725 on theBenchmark for (2725ds/12648Mi) % 300.66/42.63 % Exception at run slice level % 300.66/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.66/42.63 % (1943273)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1764425806:fmbsr=2.30978:i=4348:rtra=on_2725 on theBenchmark for (2725ds/4348Mi) % 300.66/42.63 % Exception at run slice level % 300.66/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.66/42.63 % (1943275)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1080382730:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2725 on theBenchmark for (2725ds/1738Mi) % 300.66/42.63 % (1943275)Instruction limit reached! % 300.66/42.63 % (1943275)------------------------------ % 300.66/42.63 % (1943275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (1943275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (1943275)CaDiCaL version: 2.1.3 % 300.66/42.63 % (1943275)Termination reason: Instruction limit % 300.66/42.63 % (1943275)Termination phase: Saturation % 300.66/42.63 % (1943275)Time elapsed: 0.593 s % 300.66/42.63 % (1943275)Peak memory usage: 12 MB % 300.66/42.63 % (1943275)Instructions burned: 1739 (million) % 300.66/42.63 % (1943277)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3647160060:i=10228:av=off:rtra=on_2719 on theBenchmark for (2719ds/10228Mi) % 300.66/42.63 % (1943269)Instruction limit reached! % 300.66/42.63 % (1943269)------------------------------ % 300.66/42.63 % (1943269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (1943269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (1943269)CaDiCaL version: 2.1.3 % 300.66/42.63 % (1943269)Termination reason: Instruction limit % 300.66/42.63 % (1943269)Termination phase: Saturation % 300.66/42.63 % (1943269)Time elapsed: 1.620 s % 300.66/42.63 % (1943269)Peak memory usage: 41 MB % 300.66/42.63 % (1943269)Instructions burned: 2944 (million) % 300.66/42.63 % (1943279)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2267137829:i=108564:rtra=on_2718 on theBenchmark for (2718ds/108564Mi) % 300.66/42.63 % Exception at run slice level % 300.66/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.66/42.63 % (1943281)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2648587616:i=7024:aac=none:rtra=on_2717 on theBenchmark for (2717ds/7024Mi) % 300.66/42.63 % (1943121)Instruction limit reached! % 300.66/42.63 % (1943121)------------------------------ % 300.66/42.63 % (1943121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (1943121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (1943121)CaDiCaL version: 2.1.3 % 300.66/42.63 % (1943121)Termination reason: Instruction limit % 300.66/42.63 % (1943121)Termination phase: Saturation % 300.66/42.63 % (1943121)Time elapsed: 31.531 s % 300.66/42.63 % (1943121)Peak memory usage: 167 MB % 300.66/42.63 % (1943121)Instructions burned: 88025 (million) % 300.66/42.63 % (1943283)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1606897012:i=7546:rtra=on:amm=off_2683 on theBenchmark for (2683ds/7546Mi) % 300.66/42.63 % (1943281)Instruction limit reached! % 300.66/42.63 % (1943281)------------------------------ % 300.66/42.63 % (1943281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (1943281)Linked with Z3 4.14.0.0 % 300.66/42.64 Terminated % 300.66/42.64 % Vampire exiting %------------------------------------------------------------------------------