%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV723_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:18 PM UTC 2026 % Result : Timeout 292.32s 41.45s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV723_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.12/0.26 % Computer : n018.cluster.edu % 0.12/0.26 % Model : x86_64 x86_64 % 0.12/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.26 % Memory : 8046.5625MB % 0.12/0.26 % OS : Linux 6.8.0-71-generic % 0.12/0.26 % CPULimit : 300 % 0.12/0.26 % WCLimit : 300 % 0.12/0.26 % DateTime : Mon Sep 28 12:23:54 UTC 2026 % 0.12/0.26 % CPUTime : % 0.12/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.25/0.31 Running first-order model finding % 0.25/0.31 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 % 13.92/2.34 % (3340758)Will run a generic schedule for satisfiability detection. % 13.92/2.34 % (3340766)dis+10_1_sil=32000:sp=arity:random_seed=817512138:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.92/2.34 % (3340764)% WARNING: option uhcvi not known. % 13.92/2.34 % (3340763)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2989021285_2999 on theBenchmark for (2999ds/0Mi) % 13.92/2.34 % (3340764)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1227797689:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.92/2.34 % (3340765)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3769080647:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.92/2.34 % (3340768)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=258464799:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.92/2.34 % (3340767)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2204869338:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.92/2.34 % Exception at run slice level % 13.92/2.34 % (3340769)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1204492939:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.92/2.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.92/2.34 % (3340777)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=721099493:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 13.92/2.34 % Exception at run slice level % 13.92/2.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.92/2.34 % (3340766)Instruction limit reached! % 13.92/2.34 % (3340766)------------------------------ % 13.92/2.34 % (3340766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.92/2.34 % (3340766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.34 % (3340766)CaDiCaL version: 2.1.3 % 13.92/2.34 % (3340766)Termination reason: Instruction limit % 13.92/2.34 % (3340766)Termination phase: Saturation % 13.92/2.34 % (3340766)Time elapsed: 0.061 s % 13.92/2.34 % (3340766)Peak memory usage: 12 MB % 13.92/2.34 % (3340766)Instructions burned: 103 (million) % 13.92/2.34 % (3340780)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3466072319:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 13.92/2.34 % (3340781)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=48287514:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 13.92/2.34 % (3340767)Instruction limit reached! % 13.92/2.34 % (3340767)------------------------------ % 13.92/2.34 % (3340767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.92/2.34 % (3340767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.34 % (3340767)CaDiCaL version: 2.1.3 % 13.92/2.34 % (3340767)Termination reason: Instruction limit % 13.92/2.34 % (3340767)Termination phase: Saturation % 13.92/2.34 % (3340767)Time elapsed: 0.121 s % 13.92/2.34 % (3340767)Peak memory usage: 13 MB % 13.92/2.34 % (3340767)Instructions burned: 116 (million) % 13.92/2.34 % (3340784)ott-21_1_sil=16000:fs=off:random_seed=777200149:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.92/2.34 % (3340768)Instruction limit reached! % 13.92/2.34 % (3340768)------------------------------ % 13.92/2.34 % (3340768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.92/2.34 % (3340768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.34 % (3340768)CaDiCaL version: 2.1.3 % 13.92/2.34 % (3340768)Termination reason: Instruction limit % 13.92/2.34 % (3340768)Termination phase: Saturation % 13.92/2.34 % (3340768)Time elapsed: 0.145 s % 13.92/2.34 % (3340768)Peak memory usage: 13 MB % 13.92/2.34 % (3340768)Instructions burned: 131 (million) % 13.92/2.34 % (3340769)Instruction limit reached! % 13.92/2.34 % (3340769)------------------------------ % 13.92/2.34 % (3340769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.92/2.34 % (3340769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.34 % (3340769)CaDiCaL version: 2.1.3 % 13.92/2.34 % (3340769)Termination reason: Instruction limit % 13.92/2.34 % (3340769)Termination phase: Saturation % 13.92/2.34 % (3340769)Time elapsed: 0.145 s % 13.92/2.34 % (3340769)Peak memory usage: 12 MB % 13.92/2.34 % (3340769)Instructions burned: 160 (million) % 13.92/2.34 % (3340786)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2742135690:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 34.71/5.23 % (3340787)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1654721433:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 34.71/5.23 % Exception at run slice level % 34.71/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.71/5.23 % (3340780)Instruction limit reached! % 34.71/5.23 % (3340780)------------------------------ % 34.71/5.23 % (3340780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.71/5.23 % (3340780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.71/5.23 % (3340780)CaDiCaL version: 2.1.3 % 34.71/5.23 % (3340780)Termination reason: Instruction limit % 34.71/5.23 % (3340780)Termination phase: Saturation % 34.71/5.23 % (3340780)Time elapsed: 0.150 s % 34.71/5.23 % (3340780)Peak memory usage: 13 MB % 34.71/5.23 % (3340780)Instructions burned: 131 (million) % 34.71/5.23 % (3340790)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2647109829:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 34.71/5.23 % (3340791)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3187164886:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 34.71/5.23 % Exception at run slice level % 34.71/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.71/5.23 % (3340795)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=1902966530:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 34.71/5.23 % (3340784)Instruction limit reached! % 34.71/5.23 % (3340784)------------------------------ % 34.71/5.23 % (3340784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.71/5.23 % (3340784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.71/5.23 % (3340784)CaDiCaL version: 2.1.3 % 34.71/5.23 % (3340784)Termination reason: Instruction limit % 34.71/5.23 % (3340784)Termination phase: Saturation % 34.71/5.23 % (3340784)Time elapsed: 0.184 s % 34.71/5.23 % (3340784)Peak memory usage: 13 MB % 34.71/5.23 % (3340784)Instructions burned: 181 (million) % 34.71/5.23 % (3340797)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3851770650:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 34.71/5.23 % (3340781)Instruction limit reached! % 34.71/5.23 % (3340781)------------------------------ % 34.71/5.23 % (3340781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.71/5.23 % (3340781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.71/5.23 % (3340781)CaDiCaL version: 2.1.3 % 34.71/5.23 % (3340781)Termination reason: Instruction limit % 34.71/5.23 % (3340781)Termination phase: Saturation % 34.71/5.23 % (3340781)Time elapsed: 0.349 s % 34.71/5.23 % (3340781)Peak memory usage: 16 MB % 34.71/5.23 % (3340781)Instructions burned: 684 (million) % 34.71/5.23 % (3340799)fmb+10_1_sil=64000:random_seed=1531164889:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 34.71/5.23 % (3340799)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 34.71/5.23 % Exception at run slice level % 34.71/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.71/5.23 % (3340801)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3779135225:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 34.71/5.23 % Exception at run slice level % 34.71/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.71/5.23 % (3340803)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1151704375:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 34.71/5.23 % Exception at run slice level % 34.71/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.71/5.23 % (3340805)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3389272635:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 34.71/5.23 % (3340786)Instruction limit reached! % 34.71/5.23 % (3340786)------------------------------ % 34.71/5.23 % (3340786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.71/5.23 % (3340786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.15/14.82 % (3340786)CaDiCaL version: 2.1.3 % 102.15/14.82 % (3340786)Termination reason: Instruction limit % 102.15/14.82 % (3340786)Termination phase: Saturation % 102.15/14.82 % (3340786)Time elapsed: 0.519 s % 102.15/14.82 % (3340786)Peak memory usage: 14 MB % 102.15/14.82 % (3340786)Instructions burned: 477 (million) % 102.15/14.82 % (3340807)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4023276687:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 102.15/14.82 % (3340807)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 102.15/14.82 % (3340795)Instruction limit reached! % 102.15/14.82 % (3340795)------------------------------ % 102.15/14.82 % (3340795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.15/14.82 % (3340795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.15/14.82 % (3340795)CaDiCaL version: 2.1.3 % 102.15/14.82 % (3340795)Termination reason: Instruction limit % 102.15/14.82 % (3340795)Termination phase: Saturation % 102.15/14.82 % (3340795)Time elapsed: 0.700 s % 102.15/14.82 % (3340795)Peak memory usage: 17 MB % 102.15/14.82 % (3340795)Instructions burned: 692 (million) % 102.15/14.82 % (3340809)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=32135149:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 102.15/14.82 % Exception at run slice level % 102.15/14.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.15/14.82 % (3340811)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3281299039:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 102.15/14.82 % Exception at run slice level % 102.15/14.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.15/14.82 % (3340813)ott-2_1_sil=16000:newcnf=on:random_seed=579699917:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 102.15/14.82 % (3340797)Instruction limit reached! % 102.15/14.82 % (3340797)------------------------------ % 102.15/14.82 % (3340797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.15/14.82 % (3340797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.15/14.82 % (3340797)CaDiCaL version: 2.1.3 % 102.15/14.82 % (3340797)Termination reason: Instruction limit % 102.15/14.82 % (3340797)Termination phase: Saturation % 102.15/14.82 % (3340797)Time elapsed: 0.854 s % 102.15/14.82 % (3340797)Peak memory usage: 20 MB % 102.15/14.82 % (3340797)Instructions burned: 880 (million) % 102.15/14.82 % (3340815)ott+10_1_sil=32000:tgt=ground:random_seed=3070804617:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 102.15/14.82 % (3340790)Instruction limit reached! % 102.15/14.82 % (3340790)------------------------------ % 102.15/14.82 % (3340790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.15/14.82 % (3340790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.15/14.82 % (3340790)CaDiCaL version: 2.1.3 % 102.15/14.82 % (3340790)Termination reason: Instruction limit % 102.15/14.82 % (3340790)Termination phase: Saturation % 102.15/14.82 % (3340790)Time elapsed: 1.204 s % 102.15/14.82 % (3340790)Peak memory usage: 32 MB % 102.15/14.82 % (3340790)Instructions burned: 1179 (million) % 102.15/14.82 % (3340817)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=879537248:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 102.15/14.82 % Exception at run slice level % 102.15/14.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.15/14.82 % (3340819)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1793276517:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi) % 102.15/14.82 % (3340813)Instruction limit reached! % 102.15/14.82 % (3340813)------------------------------ % 102.15/14.82 % (3340813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.15/14.82 % (3340813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.15/14.82 % (3340813)CaDiCaL version: 2.1.3 % 102.15/14.82 % (3340813)Termination reason: Instruction limit % 102.15/14.82 % (3340813)Termination phase: Saturation % 102.15/14.82 % (3340813)Time elapsed: 0.594 s % 102.15/14.82 % (3340813)Peak memory usage: 13 MB % 102.15/14.82 % (3340813)Instructions burned: 869 (million) % 102.15/14.82 % (3340822)dis+21_1_sil=32000:sas=cadical:random_seed=1533991460:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 102.15/14.82 % (3340807)Instruction limit reached! % 102.15/14.82 % (3340807)------------------------------ % 102.15/14.82 % (3340807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.58/28.99 % (3340807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.58/28.99 % (3340807)CaDiCaL version: 2.1.3 % 203.58/28.99 % (3340807)Termination reason: Instruction limit % 203.58/28.99 % (3340807)Termination phase: Saturation % 203.58/28.99 % (3340807)Time elapsed: 1.246 s % 203.58/28.99 % (3340807)Peak memory usage: 21 MB % 203.58/28.99 % (3340807)Instructions burned: 1472 (million) % 203.58/28.99 % (3340825)ott+11_1_sil=16000:gs=on:random_seed=779427969:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 203.58/28.99 % (3340805)Instruction limit reached! % 203.58/28.99 % (3340805)------------------------------ % 203.58/28.99 % (3340805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.58/28.99 % (3340805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.58/28.99 % (3340805)CaDiCaL version: 2.1.3 % 203.58/28.99 % (3340805)Termination reason: Instruction limit % 203.58/28.99 % (3340805)Termination phase: Saturation % 203.58/28.99 % (3340805)Time elapsed: 2.491 s % 203.58/28.99 % (3340805)Peak memory usage: 34 MB % 203.58/28.99 % (3340805)Instructions burned: 5132 (million) % 203.58/28.99 % (3340829)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2545530348:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 203.58/28.99 % Exception at run slice level % 203.58/28.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.58/28.99 % (3340831)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3545705939:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 203.58/28.99 % (3340825)Instruction limit reached! % 203.58/28.99 % (3340825)------------------------------ % 203.58/28.99 % (3340825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.58/28.99 % (3340825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.58/28.99 % (3340825)CaDiCaL version: 2.1.3 % 203.58/28.99 % (3340825)Termination reason: Instruction limit % 203.58/28.99 % (3340825)Termination phase: Saturation % 203.58/28.99 % (3340825)Time elapsed: 2.249 s % 203.58/28.99 % (3340825)Peak memory usage: 23 MB % 203.58/28.99 % (3340825)Instructions burned: 2251 (million) % 203.58/28.99 % (3340837)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3263535068:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 203.58/28.99 % (3340831)Instruction limit reached! % 203.58/28.99 % (3340831)------------------------------ % 203.58/28.99 % (3340831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.58/28.99 % (3340831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.58/28.99 % (3340831)CaDiCaL version: 2.1.3 % 203.58/28.99 % (3340831)Termination reason: Instruction limit % 203.58/28.99 % (3340831)Termination phase: Saturation % 203.58/28.99 % (3340831)Time elapsed: 1.660 s % 203.58/28.99 % (3340831)Peak memory usage: 27 MB % 203.58/28.99 % (3340831)Instructions burned: 4592 (million) % 203.58/28.99 % (3340819)Instruction limit reached! % 203.58/28.99 % (3340819)------------------------------ % 203.58/28.99 % (3340819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.58/28.99 % (3340819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.58/28.99 % (3340819)CaDiCaL version: 2.1.3 % 203.58/28.99 % (3340819)Termination reason: Instruction limit % 203.58/28.99 % (3340819)Termination phase: Saturation % 203.58/28.99 % (3340819)Time elapsed: 3.215 s % 203.58/28.99 % (3340819)Peak memory usage: 34 MB % 203.58/28.99 % (3340819)Instructions burned: 3512 (million) % 203.58/28.99 % (3340843)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3233913595:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 203.58/28.99 % (3340845)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2938197079:i=5497:nm=2_2952 on theBenchmark for (2952ds/5497Mi) % 203.58/28.99 % Exception at run slice level % 203.58/28.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.58/28.99 % (3340847)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=915433998:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi) % 203.58/28.99 % Exception at run slice level % 203.58/28.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 203.58/28.99 % (3340849)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3566648937:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 203.58/28.99 % Exception at run slice level % 232.96/33.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 232.96/33.10 % (3340851)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=988913288:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi) % 232.96/33.10 % (3340822)Instruction limit reached! % 232.96/33.10 % (3340822)------------------------------ % 232.96/33.10 % (3340822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340822)CaDiCaL version: 2.1.3 % 232.96/33.10 % (3340822)Termination reason: Instruction limit % 232.96/33.10 % (3340822)Termination phase: Saturation % 232.96/33.10 % (3340822)Time elapsed: 3.595 s % 232.96/33.10 % (3340822)Peak memory usage: 33 MB % 232.96/33.10 % (3340822)Instructions burned: 3773 (million) % 232.96/33.10 % (3340853)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=279151886:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 232.96/33.10 % (3340815)Instruction limit reached! % 232.96/33.10 % (3340815)------------------------------ % 232.96/33.10 % (3340815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340815)CaDiCaL version: 2.1.3 % 232.96/33.10 % (3340815)Termination reason: Instruction limit % 232.96/33.10 % (3340815)Termination phase: Saturation % 232.96/33.10 % (3340815)Time elapsed: 4.792 s % 232.96/33.10 % (3340815)Peak memory usage: 27 MB % 232.96/33.10 % (3340815)Instructions burned: 5115 (million) % 232.96/33.10 % (3340855)dis+10_16:1_sil=16000:random_seed=454605285:i=9155:fsr=off_2939 on theBenchmark for (2939ds/9155Mi) % 232.96/33.10 % (3340843)Instruction limit reached! % 232.96/33.10 % (3340843)------------------------------ % 232.96/33.10 % (3340843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340843)CaDiCaL version: 2.1.3 % 232.96/33.10 % (3340843)Termination reason: Instruction limit % 232.96/33.10 % (3340843)Termination phase: Saturation % 232.96/33.10 % (3340843)Time elapsed: 4.471 s % 232.96/33.10 % (3340843)Peak memory usage: 50 MB % 232.96/33.10 % (3340843)Instructions burned: 5212 (million) % 232.96/33.10 % (3340865)ott-3_8_sil=64000:random_seed=2657355798:i=20139:bs=on_2907 on theBenchmark for (2907ds/20139Mi) % 232.96/33.10 % (3340853)Instruction limit reached! % 232.96/33.10 % (3340853)------------------------------ % 232.96/33.10 % (3340853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340853)CaDiCaL version: 2.1.3 % 232.96/33.10 % (3340853)Termination reason: Instruction limit % 232.96/33.10 % (3340853)Termination phase: Saturation % 232.96/33.10 % (3340853)Time elapsed: 8.273 s % 232.96/33.10 % (3340853)Peak memory usage: 82 MB % 232.96/33.10 % (3340853)Instructions burned: 8174 (million) % 232.96/33.10 % (3340875)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2886338752:fmbsr=2:i=32576_2863 on theBenchmark for (2863ds/32576Mi) % 232.96/33.10 % Exception at run slice level % 232.96/33.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 232.96/33.10 % (3340877)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2815303540:i=11404_2862 on theBenchmark for (2862ds/11404Mi) % 232.96/33.10 % (3340851)Instruction limit reached! % 232.96/33.10 % (3340851)------------------------------ % 232.96/33.10 % (3340851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340851)CaDiCaL version: 2.1.3 % 232.96/33.10 % (3340851)Termination reason: Instruction limit % 232.96/33.10 % (3340851)Termination phase: Saturation % 232.96/33.10 % (3340851)Time elapsed: 9.316 s % 232.96/33.10 % (3340851)Peak memory usage: 130 MB % 232.96/33.10 % (3340851)Instructions burned: 22567 (million) % 232.96/33.10 % (3340882)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2266124303:i=14134_2857 on theBenchmark for (2857ds/14134Mi) % 232.96/33.10 % (3340855)Instruction limit reached! % 232.96/33.10 % (3340855)------------------------------ % 232.96/33.10 % (3340855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.96/33.10 % (3340855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.96/33.10 % (3340855)CaDiCaL version: 2.1.3 % 248.35/35.27 % (3340855)Termination reason: Instruction limit % 248.35/35.27 % (3340855)Termination phase: Saturation % 248.35/35.27 % (3340855)Time elapsed: 8.384 s % 248.35/35.27 % (3340855)Peak memory usage: 59 MB % 248.35/35.27 % (3340855)Instructions burned: 9156 (million) % 248.35/35.27 % (3340885)dis+33_16_sil=32000:sac=on:random_seed=3402366770:i=15851:nm=0_2854 on theBenchmark for (2854ds/15851Mi) % 248.35/35.27 % (3340865)Instruction limit reached! % 248.35/35.27 % (3340865)------------------------------ % 248.35/35.27 % (3340865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.35/35.27 % (3340865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.35/35.27 % (3340865)CaDiCaL version: 2.1.3 % 248.35/35.27 % (3340865)Termination reason: Instruction limit % 248.35/35.27 % (3340865)Termination phase: Saturation % 248.35/35.27 % (3340865)Time elapsed: 10.533 s % 248.35/35.27 % (3340865)Peak memory usage: 13 MB % 248.35/35.27 % (3340865)Instructions burned: 20139 (million) % 248.35/35.27 % (3340897)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2050323349:avsq=on:i=17627:add=on:amm=off_2802 on theBenchmark for (2802ds/17627Mi) % 248.35/35.27 % (3340882)Instruction limit reached! % 248.35/35.27 % (3340882)------------------------------ % 248.35/35.27 % (3340882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.35/35.27 % (3340882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.35/35.27 % (3340882)CaDiCaL version: 2.1.3 % 248.35/35.27 % (3340882)Termination reason: Instruction limit % 248.35/35.27 % (3340882)Termination phase: Saturation % 248.35/35.27 % (3340882)Time elapsed: 7.492 s % 248.35/35.27 % (3340882)Peak memory usage: 99 MB % 248.35/35.27 % (3340882)Instructions burned: 14136 (million) % 248.35/35.27 % (3340903)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=871358559:s2a=on:i=53295_2782 on theBenchmark for (2782ds/53295Mi) % 248.35/35.27 % (3340877)Instruction limit reached! % 248.35/35.27 % (3340877)------------------------------ % 248.35/35.27 % (3340877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.35/35.27 % (3340877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.35/35.27 % (3340877)CaDiCaL version: 2.1.3 % 248.35/35.27 % (3340877)Termination reason: Instruction limit % 248.35/35.27 % (3340877)Termination phase: Saturation % 248.35/35.27 % (3340877)Time elapsed: 12.164 s % 248.35/35.27 % (3340877)Peak memory usage: 107 MB % 248.35/35.27 % (3340877)Instructions burned: 11404 (million) % 248.35/35.27 % (3340913)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=810038497:i=26857:ins=20_2740 on theBenchmark for (2740ds/26857Mi) % 248.35/35.27 % Exception at run slice level % 248.35/35.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 248.35/35.27 % (3340915)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3657640008:i=28120:bs=on:fsr=off_2740 on theBenchmark for (2740ds/28120Mi) % 248.35/35.27 % (3340885)Instruction limit reached! % 248.35/35.27 % (3340885)------------------------------ % 248.35/35.27 % (3340885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.35/35.27 % (3340885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.35/35.27 % (3340885)CaDiCaL version: 2.1.3 % 248.35/35.27 % (3340885)Termination reason: Instruction limit % 248.35/35.27 % (3340885)Termination phase: Saturation % 248.35/35.27 % (3340885)Time elapsed: 14.021 s % 248.35/35.27 % (3340885)Peak memory usage: 82 MB % 248.35/35.27 % (3340885)Instructions burned: 15852 (million) % 248.35/35.27 % (3341010)fmb+10_1_sil=256000:fmbss=7:random_seed=2380814073:fmbsr=1.6:i=182295_2714 on theBenchmark for (2714ds/182295Mi) % 248.35/35.27 % Exception at run slice level % 248.35/35.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 248.35/35.27 % (3341017)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=863693385:i=44625:gsp=on_2714 on theBenchmark for (2714ds/44625Mi) % 248.35/35.27 % (3341017)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 248.35/35.27 % Exception at run slice level % 248.35/35.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 248.35/35.27 % (3341027)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=988258625:i=160505_2713 on theBenchmark for (2713ds/160505Mi) % 248.35/35.27 % Exception at run slice level % 248.35/35.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 248.35/35.27 % (3341029)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1738400770:fmbsr=1.3:i=225729_2713 on theBenchmark for (2713ds/225729Mi) % 292.32/41.45 % Exception at run slice level % 292.32/41.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 292.32/41.45 % (3341031)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=912277612:fmbsr=2:i=185024:ins=7_2713 on theBenchmark for (2713ds/185024Mi) % 292.32/41.45 % Exception at run slice level % 292.32/41.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 292.32/41.45 % (3341033)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3924460961:rtra=on_2713 on theBenchmark for (2713ds/0Mi) % 292.32/41.45 % Exception at run slice level % 292.32/41.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 292.32/41.45 % (3340837)Instruction limit reached! % 292.32/41.45 % (3340837)------------------------------ % 292.32/41.45 % (3340837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.32/41.45 % (3340837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/41.45 % (3340837)CaDiCaL version: 2.1.3 % 292.32/41.45 % (3340837)Termination reason: Instruction limit % 292.32/41.45 % (3340837)Termination phase: Saturation % 292.32/41.45 % (3340837)Time elapsed: 24.367 s % 292.32/41.45 % (3340837)Peak memory usage: 107 MB % 292.32/41.45 % (3340837)Instructions burned: 29342 (million) % 292.32/41.45 % (3341035)% WARNING: option uhcvi not known. % 292.32/41.45 % (3341035)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2719788165:i=271062:add=off:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/271062Mi) % 292.32/41.45 % (3341036)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4144694367:i=176048:add=on:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/176048Mi) % 292.32/41.45 % (3340897)Instruction limit reached! % 292.32/41.45 % (3340897)------------------------------ % 292.32/41.45 % (3340897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.32/41.45 % (3340897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/41.45 % (3340897)CaDiCaL version: 2.1.3 % 292.32/41.45 % (3340897)Termination reason: Instruction limit % 292.32/41.45 % (3340897)Termination phase: Saturation % 292.32/41.45 % (3340897)Time elapsed: 12.401 s % 292.32/41.45 % (3340897)Peak memory usage: 118 MB % 292.32/41.45 % (3340897)Instructions burned: 17627 (million) % 292.32/41.45 % (3341086)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1432973714:i=206:fgj=on:rtra=on_2677 on theBenchmark for (2677ds/206Mi) % 292.32/41.45 % (3341086)Instruction limit reached! % 292.32/41.45 % (3341086)------------------------------ % 292.32/41.45 % (3341086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.32/41.45 % (3341086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/41.45 % (3341086)CaDiCaL version: 2.1.3 % 292.32/41.45 % (3341086)Termination reason: Instruction limit % 292.32/41.45 % (3341086)Termination phase: Saturation % 292.32/41.45 % (3341086)Time elapsed: 0.132 s % 292.32/41.45 % (3341086)Peak memory usage: 13 MB % 292.32/41.45 % (3341086)Instructions burned: 207 (million) % 292.32/41.45 % (3341088)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3249560204:i=232:rtra=on_2675 on theBenchmark for (2675ds/232Mi) % 292.32/41.45 % (3341088)Instruction limit reached! % 292.32/41.45 % (3341088)------------------------------ % 292.32/41.45 % (3341088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.32/41.45 % (3341088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/41.45 % (3341088)CaDiCaL version: 2.1.3 % 292.32/41.45 % (3341088)Termination reason: Instruction limit % 292.32/41.45 % (3341088)Termination phase: Saturation % 292.32/41.45 % (3341088)Time elapsed: 0.150 s % 292.32/41.45 % (3341088)Peak memory usage: 13 MB % 292.32/41.45 % (3341088)Instructions burned: 234 (million) % 292.32/41.45 % (3341090)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1283809773:i=262:rtra=on_2674 on theBenchmark for (2674ds/262Mi) % 292.32/41.45 % (3341090)Instruction limit reached! % 292.32/41.45 % (3341090)------------------------------ % 292.32/41.45 % (3341090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.32/41.45 % (3341090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/41.45 % (3341090)CaDiCaL version: 2.1.3 % 292.32/41.45 % (3341090)Termination reason: Instruction limit % 292.32/41.45 % (3341090)Termination phase: SatTerminated % 300.84/42.64 % Vampire exiting %------------------------------------------------------------------------------