%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV669_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 : n018.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:26:13 PM UTC 2026 % Result : Timeout 291.63s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV669_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.08/0.20 % Computer : n018.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 12:14:40 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/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.88/1.50 % (3335118)Will run a generic schedule for satisfiability detection. % 7.88/1.50 % (3335123)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=713668135_2999 on theBenchmark for (2999ds/0Mi) % 7.88/1.50 % (3335124)% WARNING: option uhcvi not known. % 7.88/1.50 % Exception at run slice level % 7.88/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.88/1.50 % (3335124)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1077050713:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.88/1.50 % (3335125)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2740877780:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.88/1.50 % (3335126)dis+10_1_sil=32000:sp=arity:random_seed=2615654562:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.88/1.50 % (3335127)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3720786476:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.88/1.50 % (3335128)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4148963342:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.88/1.50 % (3335129)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1598069766:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.88/1.50 % (3335131)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=662392341:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.88/1.50 % Exception at run slice level % 7.88/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.88/1.50 % (3335139)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3801868929:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.88/1.50 % (3335126)Instruction limit reached! % 7.88/1.50 % (3335126)------------------------------ % 7.88/1.50 % (3335126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.88/1.50 % (3335126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.50 % (3335126)CaDiCaL version: 2.1.3 % 7.88/1.50 % (3335126)Termination reason: Instruction limit % 7.88/1.50 % (3335126)Termination phase: Saturation % 7.88/1.50 % (3335126)Time elapsed: 0.064 s % 7.88/1.50 % (3335126)Peak memory usage: 12 MB % 7.88/1.50 % (3335126)Instructions burned: 104 (million) % 7.88/1.50 % (3335127)Instruction limit reached! % 7.88/1.50 % (3335127)------------------------------ % 7.88/1.50 % (3335127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.88/1.50 % (3335127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.50 % (3335127)CaDiCaL version: 2.1.3 % 7.88/1.50 % (3335127)Termination reason: Instruction limit % 7.88/1.50 % (3335127)Termination phase: Saturation % 7.88/1.50 % (3335127)Time elapsed: 0.068 s % 7.88/1.50 % (3335127)Peak memory usage: 13 MB % 7.88/1.50 % (3335127)Instructions burned: 117 (million) % 7.88/1.50 % (3335128)Instruction limit reached! % 7.88/1.50 % (3335128)------------------------------ % 7.88/1.50 % (3335128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.88/1.50 % (3335128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.50 % (3335128)CaDiCaL version: 2.1.3 % 7.88/1.50 % (3335128)Termination reason: Instruction limit % 7.88/1.50 % (3335128)Termination phase: Saturation % 7.88/1.50 % (3335128)Time elapsed: 0.078 s % 7.88/1.50 % (3335128)Peak memory usage: 13 MB % 7.88/1.50 % (3335128)Instructions burned: 132 (million) % 7.88/1.50 % (3335141)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=1916191138:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.88/1.50 % (3335142)ott-21_1_sil=16000:fs=off:random_seed=2034486580:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.88/1.50 % (3335143)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=907485519:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.88/1.50 % (3335129)Instruction limit reached! % 7.88/1.50 % (3335129)------------------------------ % 7.88/1.50 % (3335129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.88/1.50 % (3335129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.50 % (3335129)CaDiCaL version: 2.1.3 % 7.88/1.50 % (3335129)Termination reason: Instruction limit % 7.88/1.50 % (3335129)Termination phase: Saturation % 22.26/3.44 % (3335129)Time elapsed: 0.098 s % 22.26/3.44 % (3335129)Peak memory usage: 13 MB % 22.26/3.44 % (3335129)Instructions burned: 159 (million) % 22.26/3.44 % (3335139)Instruction limit reached! % 22.26/3.44 % (3335139)------------------------------ % 22.26/3.44 % (3335139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.26/3.44 % (3335139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/3.44 % (3335139)CaDiCaL version: 2.1.3 % 22.26/3.44 % (3335139)Termination reason: Instruction limit % 22.26/3.44 % (3335139)Termination phase: Saturation % 22.26/3.44 % (3335139)Time elapsed: 0.082 s % 22.26/3.44 % (3335139)Peak memory usage: 14 MB % 22.26/3.44 % (3335139)Instructions burned: 131 (million) % 22.26/3.44 % (3335147)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=516085115:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.26/3.44 % Exception at run slice level % 22.26/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.26/3.44 % (3335148)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2083527830:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.26/3.44 % (3335150)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=396086695:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.26/3.44 % Exception at run slice level % 22.26/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.26/3.44 % (3335153)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=1034962675: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.26/3.44 % (3335142)Instruction limit reached! % 22.26/3.44 % (3335142)------------------------------ % 22.26/3.44 % (3335142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.26/3.44 % (3335142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/3.44 % (3335142)CaDiCaL version: 2.1.3 % 22.26/3.44 % (3335142)Termination reason: Instruction limit % 22.26/3.44 % (3335142)Termination phase: Saturation % 22.26/3.44 % (3335142)Time elapsed: 0.097 s % 22.26/3.44 % (3335142)Peak memory usage: 13 MB % 22.26/3.44 % (3335142)Instructions burned: 181 (million) % 22.26/3.44 % (3335155)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2039365159:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.26/3.44 % (3335143)Instruction limit reached! % 22.26/3.44 % (3335143)------------------------------ % 22.26/3.44 % (3335143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.26/3.44 % (3335143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/3.44 % (3335143)CaDiCaL version: 2.1.3 % 22.26/3.44 % (3335143)Termination reason: Instruction limit % 22.26/3.44 % (3335143)Termination phase: Saturation % 22.26/3.44 % (3335143)Time elapsed: 0.303 s % 22.26/3.44 % (3335143)Peak memory usage: 14 MB % 22.26/3.44 % (3335143)Instructions burned: 478 (million) % 22.26/3.44 % (3335157)fmb+10_1_sil=64000:random_seed=3692247276:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.26/3.44 % (3335157)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.26/3.44 % Exception at run slice level % 22.26/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.26/3.44 % (3335159)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=911621400:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.26/3.44 % (3335141)Instruction limit reached! % 22.26/3.44 % (3335141)------------------------------ % 22.26/3.44 % (3335141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.26/3.44 % (3335141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/3.44 % (3335141)CaDiCaL version: 2.1.3 % 22.26/3.44 % (3335141)Termination reason: Instruction limit % 22.26/3.44 % (3335141)Termination phase: Saturation % 22.26/3.44 % (3335141)Time elapsed: 0.363 s % 22.26/3.44 % (3335141)Peak memory usage: 17 MB % 22.26/3.44 % (3335141)Instructions burned: 685 (million) % 22.26/3.44 % Exception at run slice level % 22.26/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.26/3.44 % (3335161)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=547072390:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.26/3.44 % (3335162)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=498244706:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 83.56/12.11 % Exception at run slice level % 83.56/12.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 83.56/12.11 % (3335165)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2545773558:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 83.56/12.11 % (3335165)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.56/12.11 % (3335153)Instruction limit reached! % 83.56/12.11 % (3335153)------------------------------ % 83.56/12.11 % (3335153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.56/12.11 % (3335153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.56/12.11 % (3335153)CaDiCaL version: 2.1.3 % 83.56/12.11 % (3335153)Termination reason: Instruction limit % 83.56/12.11 % (3335153)Termination phase: Saturation % 83.56/12.11 % (3335153)Time elapsed: 0.400 s % 83.56/12.11 % (3335153)Peak memory usage: 17 MB % 83.56/12.11 % (3335153)Instructions burned: 693 (million) % 83.56/12.11 % (3335167)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1498655850:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 83.56/12.11 % Exception at run slice level % 83.56/12.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 83.56/12.11 % (3335169)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2889570182:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 83.56/12.11 % Exception at run slice level % 83.56/12.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 83.56/12.11 % (3335171)ott-2_1_sil=16000:newcnf=on:random_seed=3926612404:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 83.56/12.11 % (3335155)Instruction limit reached! % 83.56/12.11 % (3335155)------------------------------ % 83.56/12.11 % (3335155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.56/12.11 % (3335155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.56/12.11 % (3335155)CaDiCaL version: 2.1.3 % 83.56/12.11 % (3335155)Termination reason: Instruction limit % 83.56/12.11 % (3335155)Termination phase: Saturation % 83.56/12.11 % (3335155)Time elapsed: 0.474 s % 83.56/12.11 % (3335155)Peak memory usage: 17 MB % 83.56/12.11 % (3335155)Instructions burned: 879 (million) % 83.56/12.11 % (3335173)ott+10_1_sil=32000:tgt=ground:random_seed=2174464244:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 83.56/12.11 % (3335148)Instruction limit reached! % 83.56/12.11 % (3335148)------------------------------ % 83.56/12.11 % (3335148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.56/12.11 % (3335148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.56/12.11 % (3335148)CaDiCaL version: 2.1.3 % 83.56/12.11 % (3335148)Termination reason: Instruction limit % 83.56/12.11 % (3335148)Termination phase: Saturation % 83.56/12.11 % (3335148)Time elapsed: 0.712 s % 83.56/12.11 % (3335148)Peak memory usage: 27 MB % 83.56/12.11 % (3335148)Instructions burned: 1180 (million) % 83.56/12.11 % (3335175)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=616857459:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 83.56/12.11 % Exception at run slice level % 83.56/12.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 83.56/12.11 % (3335177)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3438663668:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 83.56/12.11 % (3335171)Instruction limit reached! % 83.56/12.11 % (3335171)------------------------------ % 83.56/12.11 % (3335171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.56/12.11 % (3335171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.56/12.11 % (3335171)CaDiCaL version: 2.1.3 % 83.56/12.11 % (3335171)Termination reason: Instruction limit % 83.56/12.11 % (3335171)Termination phase: Saturation % 83.56/12.11 % (3335171)Time elapsed: 0.522 s % 83.56/12.11 % (3335171)Peak memory usage: 20 MB % 83.56/12.11 % (3335171)Instructions burned: 870 (million) % 83.56/12.11 % (3335179)dis+21_1_sil=32000:sas=cadical:random_seed=3880085934:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 83.56/12.11 % (3335165)Instruction limit reached! % 83.56/12.11 % (3335165)------------------------------ % 83.56/12.11 % (3335165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.00/18.67 % (3335165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/18.67 % (3335165)CaDiCaL version: 2.1.3 % 130.00/18.67 % (3335165)Termination reason: Instruction limit % 130.00/18.67 % (3335165)Termination phase: Saturation % 130.00/18.67 % (3335165)Time elapsed: 0.723 s % 130.00/18.67 % (3335165)Peak memory usage: 23 MB % 130.00/18.67 % (3335165)Instructions burned: 1474 (million) % 130.00/18.67 % (3335181)ott+11_1_sil=16000:gs=on:random_seed=2375962005:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 130.00/18.67 % (3335181)Instruction limit reached! % 130.00/18.67 % (3335181)------------------------------ % 130.00/18.67 % (3335181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.00/18.67 % (3335181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/18.67 % (3335181)CaDiCaL version: 2.1.3 % 130.00/18.67 % (3335181)Termination reason: Instruction limit % 130.00/18.67 % (3335181)Termination phase: Saturation % 130.00/18.67 % (3335181)Time elapsed: 1.356 s % 130.00/18.67 % (3335181)Peak memory usage: 38 MB % 130.00/18.67 % (3335181)Instructions burned: 2252 (million) % 130.00/18.67 % (3335183)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4163806170:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 130.00/18.67 % Exception at run slice level % 130.00/18.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.00/18.67 % (3335177)Instruction limit reached! % 130.00/18.67 % (3335177)------------------------------ % 130.00/18.67 % (3335177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.00/18.67 % (3335177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/18.67 % (3335177)CaDiCaL version: 2.1.3 % 130.00/18.67 % (3335177)Termination reason: Instruction limit % 130.00/18.67 % (3335177)Termination phase: Saturation % 130.00/18.67 % (3335177)Time elapsed: 1.746 s % 130.00/18.67 % (3335177)Peak memory usage: 30 MB % 130.00/18.67 % (3335177)Instructions burned: 3512 (million) % 130.00/18.67 % (3335185)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1930620935:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 130.00/18.67 % (3335186)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4070265370:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 130.00/18.67 % (3335179)Instruction limit reached! % 130.00/18.67 % (3335179)------------------------------ % 130.00/18.67 % (3335179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.00/18.67 % (3335179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/18.67 % (3335179)CaDiCaL version: 2.1.3 % 130.00/18.67 % (3335179)Termination reason: Instruction limit % 130.00/18.67 % (3335179)Termination phase: Saturation % 130.00/18.67 % (3335179)Time elapsed: 1.870 s % 130.00/18.67 % (3335179)Peak memory usage: 32 MB % 130.00/18.67 % (3335179)Instructions burned: 3773 (million) % 130.00/18.67 % (3335162)Instruction limit reached! % 130.00/18.67 % (3335162)------------------------------ % 130.00/18.67 % (3335162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.00/18.67 % (3335162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/18.67 % (3335162)CaDiCaL version: 2.1.3 % 130.00/18.67 % (3335162)Termination reason: Instruction limit % 130.00/18.67 % (3335162)Termination phase: Saturation % 130.00/18.67 % (3335162)Time elapsed: 2.599 s % 130.00/18.67 % (3335162)Peak memory usage: 41 MB % 130.00/18.67 % (3335162)Instructions burned: 5132 (million) % 130.00/18.67 % (3335189)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3324617547:i=5211_2968 on theBenchmark for (2968ds/5211Mi) % 130.00/18.67 % (3335190)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3466919547:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 130.00/18.67 % Exception at run slice level % 130.00/18.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.00/18.67 % (3335193)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1527147697:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 130.00/18.67 % Exception at run slice level % 130.00/18.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.00/18.67 % (3335195)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1135694448:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 130.00/18.67 % Exception at run slice level % 169.40/24.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.40/24.20 % (3335197)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4147577076:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 169.40/24.20 % (3335173)Instruction limit reached! % 169.40/24.20 % (3335173)------------------------------ % 169.40/24.20 % (3335173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335173)CaDiCaL version: 2.1.3 % 169.40/24.20 % (3335173)Termination reason: Instruction limit % 169.40/24.20 % (3335173)Termination phase: Saturation % 169.40/24.20 % (3335173)Time elapsed: 2.856 s % 169.40/24.20 % (3335173)Peak memory usage: 50 MB % 169.40/24.20 % (3335173)Instructions burned: 5115 (million) % 169.40/24.20 % (3335199)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2960011697:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 169.40/24.20 % (3335185)Instruction limit reached! % 169.40/24.20 % (3335185)------------------------------ % 169.40/24.20 % (3335185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335185)CaDiCaL version: 2.1.3 % 169.40/24.20 % (3335185)Termination reason: Instruction limit % 169.40/24.20 % (3335185)Termination phase: Saturation % 169.40/24.20 % (3335185)Time elapsed: 2.534 s % 169.40/24.20 % (3335185)Peak memory usage: 75 MB % 169.40/24.20 % (3335185)Instructions burned: 4592 (million) % 169.40/24.20 % (3335201)dis+10_16:1_sil=16000:random_seed=679311298:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi) % 169.40/24.20 % (3335189)Instruction limit reached! % 169.40/24.20 % (3335189)------------------------------ % 169.40/24.20 % (3335189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335189)CaDiCaL version: 2.1.3 % 169.40/24.20 % (3335189)Termination reason: Instruction limit % 169.40/24.20 % (3335189)Termination phase: Saturation % 169.40/24.20 % (3335189)Time elapsed: 2.845 s % 169.40/24.20 % (3335189)Peak memory usage: 42 MB % 169.40/24.20 % (3335189)Instructions burned: 5211 (million) % 169.40/24.20 % (3335203)ott-3_8_sil=64000:random_seed=254351917:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 169.40/24.20 % (3335199)Instruction limit reached! % 169.40/24.20 % (3335199)------------------------------ % 169.40/24.20 % (3335199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335199)CaDiCaL version: 2.1.3 % 169.40/24.20 % (3335199)Termination reason: Instruction limit % 169.40/24.20 % (3335199)Termination phase: Saturation % 169.40/24.20 % (3335199)Time elapsed: 4.469 s % 169.40/24.20 % (3335199)Peak memory usage: 58 MB % 169.40/24.20 % (3335199)Instructions burned: 8173 (million) % 169.40/24.20 % (3335205)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3578652733:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 169.40/24.20 % Exception at run slice level % 169.40/24.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 169.40/24.20 % (3335207)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3963394399:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 169.40/24.20 % (3335201)Instruction limit reached! % 169.40/24.20 % (3335201)------------------------------ % 169.40/24.20 % (3335201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335201)CaDiCaL version: 2.1.3 % 169.40/24.20 % (3335201)Termination reason: Instruction limit % 169.40/24.20 % (3335201)Termination phase: Saturation % 169.40/24.20 % (3335201)Time elapsed: 4.589 s % 169.40/24.20 % (3335201)Peak memory usage: 65 MB % 169.40/24.20 % (3335201)Instructions burned: 9156 (million) % 169.40/24.20 % (3335209)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=429960715:i=14134_2901 on theBenchmark for (2901ds/14134Mi) % 169.40/24.20 % (3335197)Instruction limit reached! % 169.40/24.20 % (3335197)------------------------------ % 169.40/24.20 % (3335197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.40/24.20 % (3335197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.40/24.20 % (3335197)CaDiCaL version: 2.1.3 % 184.17/26.22 % (3335197)Termination reason: Instruction limit % 184.17/26.22 % (3335197)Termination phase: Saturation % 184.17/26.22 % (3335197)Time elapsed: 8.653 s % 184.17/26.22 % (3335197)Peak memory usage: 23 MB % 184.17/26.22 % (3335197)Instructions burned: 22565 (million) % 184.17/26.22 % (3335211)dis+33_16_sil=32000:sac=on:random_seed=756327536:i=15851:nm=0_2881 on theBenchmark for (2881ds/15851Mi) % 184.17/26.22 % (3335207)Instruction limit reached! % 184.17/26.22 % (3335207)------------------------------ % 184.17/26.22 % (3335207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.17/26.22 % (3335207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.17/26.22 % (3335207)CaDiCaL version: 2.1.3 % 184.17/26.22 % (3335207)Termination reason: Instruction limit % 184.17/26.22 % (3335207)Termination phase: Saturation % 184.17/26.22 % (3335207)Time elapsed: 6.236 s % 184.17/26.22 % (3335207)Peak memory usage: 73 MB % 184.17/26.22 % (3335207)Instructions burned: 11405 (million) % 184.17/26.22 % (3335385)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1159488070:avsq=on:i=17627:add=on:amm=off_2856 on theBenchmark for (2856ds/17627Mi) % 184.17/26.22 % (3335186)Instruction limit reached! % 184.17/26.22 % (3335186)------------------------------ % 184.17/26.22 % (3335186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.17/26.22 % (3335186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.17/26.22 % (3335186)CaDiCaL version: 2.1.3 % 184.17/26.22 % (3335186)Termination reason: Instruction limit % 184.17/26.22 % (3335186)Termination phase: Saturation % 184.17/26.22 % (3335186)Time elapsed: 13.525 s % 184.17/26.22 % (3335186)Peak memory usage: 74 MB % 184.17/26.22 % (3335186)Instructions burned: 29341 (million) % 184.17/26.22 % (3335501)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2857254974:s2a=on:i=53295_2837 on theBenchmark for (2837ds/53295Mi) % 184.17/26.22 % (3335203)Instruction limit reached! % 184.17/26.22 % (3335203)------------------------------ % 184.17/26.22 % (3335203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.17/26.22 % (3335203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.17/26.22 % (3335203)CaDiCaL version: 2.1.3 % 184.17/26.22 % (3335203)Termination reason: Instruction limit % 184.17/26.22 % (3335203)Termination phase: Saturation % 184.17/26.22 % (3335203)Time elapsed: 12.101 s % 184.17/26.22 % (3335203)Peak memory usage: 114 MB % 184.17/26.22 % (3335203)Instructions burned: 20140 (million) % 184.17/26.22 % (3335669)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3978756782:i=26857:ins=20_2818 on theBenchmark for (2818ds/26857Mi) % 184.17/26.22 % Exception at run slice level % 184.17/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.17/26.22 % (3335671)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=933291398:i=28120:bs=on:fsr=off_2818 on theBenchmark for (2818ds/28120Mi) % 184.17/26.22 % (3335209)Instruction limit reached! % 184.17/26.22 % (3335209)------------------------------ % 184.17/26.22 % (3335209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.17/26.22 % (3335209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.17/26.22 % (3335209)CaDiCaL version: 2.1.3 % 184.17/26.22 % (3335209)Termination reason: Instruction limit % 184.17/26.22 % (3335209)Termination phase: Saturation % 184.17/26.22 % (3335209)Time elapsed: 8.459 s % 184.17/26.22 % (3335209)Peak memory usage: 93 MB % 184.17/26.22 % (3335209)Instructions burned: 14134 (million) % 184.17/26.22 % (3335673)fmb+10_1_sil=256000:fmbss=7:random_seed=3906144154:fmbsr=1.6:i=182295_2816 on theBenchmark for (2816ds/182295Mi) % 184.17/26.22 % Exception at run slice level % 184.17/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.17/26.22 % (3335675)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=950573520:i=44625:gsp=on_2816 on theBenchmark for (2816ds/44625Mi) % 184.17/26.22 % (3335675)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 184.17/26.22 % Exception at run slice level % 184.17/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.17/26.22 % (3335677)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2909725164:i=160505_2816 on theBenchmark for (2816ds/160505Mi) % 184.17/26.22 % Exception at run slice level % 184.17/26.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.17/26.22 % (3335679)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3522448291:fmbsr=1.3:i=225729_2815 on theBenchmark for (2815ds/225729Mi) % 249.48/35.45 % Exception at run slice level % 249.48/35.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 249.48/35.45 % (3335681)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2701344040:fmbsr=2:i=185024:ins=7_2815 on theBenchmark for (2815ds/185024Mi) % 249.48/35.45 % Exception at run slice level % 249.48/35.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 249.48/35.45 % (3335683)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2290434825:rtra=on_2815 on theBenchmark for (2815ds/0Mi) % 249.48/35.45 % Exception at run slice level % 249.48/35.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 249.48/35.45 % (3335685)% WARNING: option uhcvi not known. % 249.48/35.45 % (3335685)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2920577572:i=271062:add=off:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/271062Mi) % 249.48/35.45 % (3335211)Instruction limit reached! % 249.48/35.45 % (3335211)------------------------------ % 249.48/35.45 % (3335211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.48/35.45 % (3335211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/35.45 % (3335211)CaDiCaL version: 2.1.3 % 249.48/35.45 % (3335211)Termination reason: Instruction limit % 249.48/35.45 % (3335211)Termination phase: Saturation % 249.48/35.45 % (3335211)Time elapsed: 8.322 s % 249.48/35.45 % (3335211)Peak memory usage: 75 MB % 249.48/35.45 % (3335211)Instructions burned: 15852 (million) % 249.48/35.45 % (3335687)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2632925873:i=176048:add=on:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/176048Mi) % 249.48/35.45 % (3335385)Instruction limit reached! % 249.48/35.45 % (3335385)------------------------------ % 249.48/35.45 % (3335385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.48/35.45 % (3335385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/35.45 % (3335385)CaDiCaL version: 2.1.3 % 249.48/35.45 % (3335385)Termination reason: Instruction limit % 249.48/35.45 % (3335385)Termination phase: Saturation % 249.48/35.45 % (3335385)Time elapsed: 9.055 s % 249.48/35.45 % (3335385)Peak memory usage: 78 MB % 249.48/35.45 % (3335385)Instructions burned: 17629 (million) % 249.48/35.45 % (3335689)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3293504188:i=206:fgj=on:rtra=on_2765 on theBenchmark for (2765ds/206Mi) % 249.48/35.45 % (3335689)Instruction limit reached! % 249.48/35.45 % (3335689)------------------------------ % 249.48/35.45 % (3335689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.48/35.45 % (3335689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/35.45 % (3335689)CaDiCaL version: 2.1.3 % 249.48/35.45 % (3335689)Termination reason: Instruction limit % 249.48/35.45 % (3335689)Termination phase: Saturation % 249.48/35.45 % (3335689)Time elapsed: 0.120 s % 249.48/35.45 % (3335689)Peak memory usage: 13 MB % 249.48/35.45 % (3335689)Instructions burned: 206 (million) % 249.48/35.45 % (3335691)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1666184379:i=232:rtra=on_2763 on theBenchmark for (2763ds/232Mi) % 249.48/35.45 % (3335691)Instruction limit reached! % 249.48/35.45 % (3335691)------------------------------ % 249.48/35.45 % (3335691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.48/35.45 % (3335691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/35.45 % (3335691)CaDiCaL version: 2.1.3 % 249.48/35.45 % (3335691)Termination reason: Instruction limit % 249.48/35.45 % (3335691)Termination phase: Saturation % 249.48/35.45 % (3335691)Time elapsed: 0.133 s % 249.48/35.45 % (3335691)Peak memory usage: 14 MB % 249.48/35.45 % (3335691)Instructions burned: 233 (million) % 249.48/35.45 % (3335693)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=8174124:i=262:rtra=on_2762 on theBenchmark for (2762ds/262Mi) % 249.48/35.45 % (3335693)Instruction limit reached! % 249.48/35.45 % (3335693)------------------------------ % 249.48/35.45 % (3335693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.48/35.45 % (3335693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/35.45 % (3335693)CaDiCaL version: 2.1.3 % 249.48/35.45 % (3335693)Termination reason: Instruction limit % 249.48/35.45 % (3335693)Termination phase: Saturation % 277.86/39.40 % (3335693)Time elapsed: 0.161 s % 277.86/39.40 % (3335693)Peak memory usage: 14 MB % 277.86/39.40 % (3335693)Instructions burned: 262 (million) % 277.86/39.40 % (3335695)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1029060502:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2760 on theBenchmark for (2760ds/318Mi) % 277.86/39.40 % (3335695)Instruction limit reached! % 277.86/39.40 % (3335695)------------------------------ % 277.86/39.40 % (3335695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.86/39.40 % (3335695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.86/39.40 % (3335695)CaDiCaL version: 2.1.3 % 277.86/39.40 % (3335695)Termination reason: Instruction limit % 277.86/39.40 % (3335695)Termination phase: Saturation % 277.86/39.40 % (3335695)Time elapsed: 0.195 s % 277.86/39.40 % (3335695)Peak memory usage: 15 MB % 277.86/39.40 % (3335695)Instructions burned: 319 (million) % 277.86/39.40 % (3335697)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4279878765:i=1428:nm=2:rtra=on_2758 on theBenchmark for (2758ds/1428Mi) % 277.86/39.40 % Exception at run slice level % 277.86/39.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 277.86/39.40 % (3335699)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=512152758:i=262:bd=preordered:rtra=on:fsd=on_2758 on theBenchmark for (2758ds/262Mi) % 277.86/39.40 % (3335699)Instruction limit reached! % 277.86/39.40 % (3335699)------------------------------ % 277.86/39.40 % (3335699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.86/39.40 % (3335699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.86/39.40 % (3335699)CaDiCaL version: 2.1.3 % 277.86/39.40 % (3335699)Termination reason: Instruction limit % 277.86/39.40 % (3335699)Termination phase: Saturation % 277.86/39.40 % (3335699)Time elapsed: 0.163 s % 277.86/39.40 % (3335699)Peak memory usage: 14 MB % 277.86/39.40 % (3335699)Instructions burned: 263 (million) % 277.86/39.40 % (3335701)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=383421250:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/1368Mi) % 277.86/39.40 % (3335701)Instruction limit reached! % 277.86/39.40 % (3335701)------------------------------ % 277.86/39.40 % (3335701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.86/39.40 % (3335701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.86/39.40 % (3335701)CaDiCaL version: 2.1.3 % 277.86/39.40 % (3335701)Termination reason: Instruction limit % 277.86/39.40 % (3335701)Termination phase: Saturation % 277.86/39.40 % (3335701)Time elapsed: 0.748 s % 277.86/39.40 % (3335701)Peak memory usage: 20 MB % 277.86/39.40 % (3335701)Instructions burned: 1369 (million) % 277.86/39.40 % (3335703)ott-21_1_sil=16000:si=on:fs=off:random_seed=3493417016:i=360:av=off:fsr=off:rtra=on_2748 on theBenchmark for (2748ds/360Mi) % 277.86/39.40 % (3335703)Instruction limit reached! % 277.86/39.40 % (3335703)------------------------------ % 277.86/39.40 % (3335703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.86/39.40 % (3335703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.86/39.40 % (3335703)CaDiCaL version: 2.1.3 % 277.86/39.40 % (3335703)Termination reason: Instruction limit % 277.86/39.40 % (3335703)Termination phase: Saturation % 277.86/39.40 % (3335703)Time elapsed: 0.175 s % 277.86/39.40 % (3335703)Peak memory usage: 13 MB % 277.86/39.40 % (3335703)Instructions burned: 362 (million) % 277.86/39.40 % (3335705)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4026797824:i=954:bd=all:rtra=on_2746 on theBenchmark for (2746ds/954Mi) % 277.86/39.40 % (3335705)Instruction limit reached! % 277.86/39.40 % (3335705)------------------------------ % 277.86/39.40 % (3335705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.86/39.40 % (3335705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.86/39.40 % (3335705)CaDiCaL version: 2.1.3 % 277.86/39.40 % (3335705)Termination reason: Instruction limit % 277.86/39.40 % (3335705)Termination phase: Saturation % 277.86/39.40 % (3335705)Time elapsed: 0.579 s % 277.86/39.40 % (3335705)Peak memory usage: 16 MB % 277.86/39.40 % (3335705)Instructions burned: 954 (million) % 277.86/39.40 % (3335707)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3552851070:fmbsr=1.3:i=1730:ins=25:rtra=on_2740 on theBenchmark for (2740ds/1730Mi) % 277.86/39.40 % Exception at run slice level % 277.86/39.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.63/41.44 % (3335709)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2539792130:i=2358:rtra=on_2740 on theBenchmark for (2740ds/2358Mi) % 291.63/41.44 % (3335709)Instruction limit reached! % 291.63/41.44 % (3335709)------------------------------ % 291.63/41.44 % (3335709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.63/41.44 % (3335709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.63/41.44 % (3335709)CaDiCaL version: 2.1.3 % 291.63/41.44 % (3335709)Termination reason: Instruction limit % 291.63/41.44 % (3335709)Termination phase: Saturation % 291.63/41.44 % (3335709)Time elapsed: 1.552 s % 291.63/41.44 % (3335709)Peak memory usage: 48 MB % 291.63/41.44 % (3335709)Instructions burned: 2358 (million) % 291.63/41.44 % (3335711)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3716644220:i=1778:ins=1:rtra=on_2724 on theBenchmark for (2724ds/1778Mi) % 291.63/41.44 % Exception at run slice level % 291.63/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.63/41.44 % (3335713)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=692750194:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2724 on theBenchmark for (2724ds/1384Mi) % 291.63/41.44 % (3335713)Instruction limit reached! % 291.63/41.44 % (3335713)------------------------------ % 291.63/41.44 % (3335713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.63/41.44 % (3335713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.63/41.44 % (3335713)CaDiCaL version: 2.1.3 % 291.63/41.44 % (3335713)Termination reason: Instruction limit % 291.63/41.44 % (3335713)Termination phase: Saturation % 291.63/41.44 % (3335713)Time elapsed: 0.753 s % 291.63/41.44 % (3335713)Peak memory usage: 21 MB % 291.63/41.44 % (3335713)Instructions burned: 1384 (million) % 291.63/41.44 % (3335715)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3700211003:i=1758:kws=inv_precedence:fsr=off:rtra=on_2716 on theBenchmark for (2716ds/1758Mi) % 291.63/41.44 % (3335715)Instruction limit reached! % 291.63/41.44 % (3335715)------------------------------ % 291.63/41.44 % (3335715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.63/41.44 % (3335715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.63/41.44 % (3335715)CaDiCaL version: 2.1.3 % 291.63/41.44 % (3335715)Termination reason: Instruction limit % 291.63/41.44 % (3335715)Termination phase: Saturation % 291.63/41.44 % (3335715)Time elapsed: 0.976 s % 291.63/41.44 % (3335715)Peak memory usage: 22 MB % 291.63/41.44 % (3335715)Instructions burned: 1758 (million) % 291.63/41.44 % (3335932)fmb+10_1_sil=64000:si=on:random_seed=3185176651:i=44122:nm=2:rtra=on:gsp=on_2706 on theBenchmark for (2706ds/44122Mi) % 291.63/41.44 % (3335932)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.63/41.44 % Exception at run slice level % 291.63/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.63/41.44 % (3335945)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3349604979:i=19030:nm=5:rtra=on_2706 on theBenchmark for (2706ds/19030Mi) % 291.63/41.44 % Exception at run slice level % 291.63/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.63/41.44 % (3335951)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3096243524:fmbsr=1.7:i=1840:rtra=on_2705 on theBenchmark for (2705ds/1840Mi) % 291.63/41.44 % Exception at run slice level % 291.63/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.63/41.44 % (3335959)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2934573522:i=10262:rtra=on_2705 on theBenchmark for (2705ds/10262Mi) % 291.63/41.44 % (3335671)Instruction limit reached! % 291.63/41.44 % (3335671)------------------------------ % 291.63/41.44 % (3335671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.63/41.44 % (3335671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.63/41.44 % (3335671)CaDiCaL version: 2.1.3 % 291.63/41.44 % (3335671)Termination reason: Instruction limit % 291.63/41.44 % (3335671)Termination phase: Saturation % 291.63/41.44 % (3335671)Time elapsed: 17.054 s % 291.63/41.44 % (3335671)Peak memory usage: 187 MB % 291.63/41.44 % (3335671)Instructions burned: 28122 (million) % 300.33/42.63 % (3336000)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=702105762:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2647 on theBenchmark for (2647ds/2944Mi) % 300.33/42.63 % (3336000)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.33/42.63 % (3335959)Instruction limit reached! % 300.33/42.63 % (3335959)------------------------------ % 300.33/42.63 % (3335959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.63 % (3335959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.63 % (3335959)CaDiCaL version: 2.1.3 % 300.33/42.63 % (3335959)Termination reason: Instruction limit % 300.33/42.63 % (3335959)Termination phase: Saturation % 300.33/42.63 % (3335959)Time elapsed: 5.932 s % 300.33/42.63 % (3335959)Peak memory usage: 69 MB % 300.33/42.63 % (3335959)Instructions burned: 10262 (million) % 300.33/42.63 % (3336002)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=778625804:i=12648:rtra=on_2645 on theBenchmark for (2645ds/12648Mi) % 300.33/42.63 % Exception at run slice level % 300.33/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.33/42.63 % (3336004)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2820896226:fmbsr=2.30978:i=4348:rtra=on_2645 on theBenchmark for (2645ds/4348Mi) % 300.33/42.63 % Exception at run slice level % 300.33/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.33/42.63 % (3336006)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2462540037:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2645 on theBenchmark for (2645ds/1738Mi) % 300.33/42.63 % (3335125)Instruction limit reached! % 300.33/42.63 % (3335125)------------------------------ % 300.33/42.63 % (3335125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.63 % (3335125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.63 % (3335125)CaDiCaL version: 2.1.3 % 300.33/42.63 % (3335125)Termination reason: Instruction limit % 300.33/42.63 % (3335125)Termination phase: Saturation % 300.33/42.63 % (3335125)Time elapsed: 36.041 s % 300.33/42.63 % (3335125)Peak memory usage: 46 MB % 300.33/42.63 % (3335125)Instructions burned: 88024 (million) % 300.33/42.63 % (3336008)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=945432396:i=10228:av=off:rtra=on_2639 on theBenchmark for (2639ds/10228Mi) % 300.33/42.63 % (3336006)Instruction limit reached! % 300.33/42.63 % (3336006)------------------------------ % 300.33/42.63 % (3336006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.63 % (3336006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.63 % (3336006)CaDiCaL version: 2.1.3 % 300.33/42.63 % (3336006)Termination reason: Instruction limit % 300.33/42.63 % (3336006)Termination phase: Saturation % 300.33/42.63 % (3336006)Time elapsed: 0.963 s % 300.33/42.63 % (3336006)Peak memory usage: 27 MB % 300.33/42.63 % (3336006)Instructions burned: 1739 (million) % 300.33/42.63 % (3336010)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3175729571:i=108564:rtra=on_2635 on theBenchmark for (2635ds/108564Mi) % 300.33/42.63 % Exception at run slice level % 300.33/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.33/42.63 % (3336012)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=253547576:i=7024:aac=none:rtra=on_2635 on theBenchmark for (2635ds/7024Mi) % 300.33/42.63 % (3336000)Instruction limit reached! % 300.33/42.63 % (3336000)------------------------------ % 300.33/42.63 % (3336000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.63 % (3336000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.63 % (3336000)CaDiCaL version: 2.1.3 % 300.33/42.63 % (3336000)Termination reason: Instruction limit % 300.33/42.63 % (3336000)Termination phase: Saturation % 300.33/42.63 % (3336000)Time elapsed: 1.804 s % 300.33/42.63 % (3336000)Peak memory usage: 43 MB % 300.33/42.63 % (3336000)Instructions burned: 2944 (million) % 300.33/42.63 % (3336014)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3138084430:i=7546:rtra=on:amm=off_2629 on theBenchmark for (2629ds/7546Mi) % 300.33/42.63 % (3335124)Instruction limit reached! % 300.33/42.63 % (3335124)------------------------------ % 300.33/42.63 % (3335124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.63 % (3335124)Linked with Z3 4.14.0.0 % 300.33/42.63 Terminated % 300.33/42.63 % Vampire exiting %------------------------------------------------------------------------------