%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM984_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n003.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 12:26:20 PM UTC 2026 % Result : Timeout 290.75s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM984_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.44 % Computer : n003.cluster.edu % 0.17/0.44 % Model : x86_64 x86_64 % 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.44 % Memory : 8046.5625MB % 0.17/0.44 % OS : Linux 6.8.0-71-generic % 0.17/0.44 % CPULimit : 300 % 0.17/0.44 % WCLimit : 300 % 0.17/0.44 % DateTime : Sun Sep 27 21:51:11 UTC 2026 % 0.17/0.45 % CPUTime : % 0.17/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.21/0.50 Running first-order model finding % 0.21/0.50 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.56/2.06 % (947972)Will run a generic schedule for satisfiability detection. % 7.56/2.06 % (947980)dis+10_1_sil=32000:sp=arity:random_seed=2913497238:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.56/2.06 % (947978)% WARNING: option uhcvi not known. % 7.56/2.06 % (947978)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2709843333:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.56/2.06 % (947977)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=734896399_2999 on theBenchmark for (2999ds/0Mi) % 7.56/2.06 % (947979)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1012088669:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.56/2.06 % (947981)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3796566772:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.56/2.06 % (947982)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=197695375:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.56/2.06 % (947983)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1390803349:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.56/2.06 % Exception at run slice level % 7.56/2.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.56/2.06 % (947980)Instruction limit reached! % 7.56/2.06 % (947980)------------------------------ % 7.56/2.06 % (947980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.56/2.06 % (947980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/2.06 % (947980)CaDiCaL version: 2.1.3 % 7.56/2.06 % (947980)Termination reason: Instruction limit % 7.56/2.06 % (947980)Termination phase: Saturation % 7.56/2.06 % (947980)Time elapsed: 0.052 s % 7.56/2.06 % (947980)Peak memory usage: 12 MB % 7.56/2.06 % (947980)Instructions burned: 103 (million) % 7.56/2.06 % (947991)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3357495310:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.56/2.06 % Exception at run slice level % 7.56/2.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.56/2.06 % (947992)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=957627775:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.56/2.06 % (947994)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=3298113268:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.56/2.06 % (947981)Instruction limit reached! % 7.56/2.06 % (947981)------------------------------ % 7.56/2.06 % (947981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.56/2.06 % (947981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/2.06 % (947981)CaDiCaL version: 2.1.3 % 7.56/2.06 % (947981)Termination reason: Instruction limit % 7.56/2.06 % (947981)Termination phase: Saturation % 7.56/2.06 % (947981)Time elapsed: 0.109 s % 7.56/2.06 % (947981)Peak memory usage: 13 MB % 7.56/2.06 % (947981)Instructions burned: 116 (million) % 7.56/2.06 % (947982)Instruction limit reached! % 7.56/2.06 % (947982)------------------------------ % 7.56/2.06 % (947982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.56/2.06 % (947982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/2.06 % (947982)CaDiCaL version: 2.1.3 % 7.56/2.06 % (947982)Termination reason: Instruction limit % 7.56/2.06 % (947982)Termination phase: Saturation % 7.56/2.06 % (947982)Time elapsed: 0.114 s % 7.56/2.06 % (947982)Peak memory usage: 12 MB % 7.56/2.06 % (947982)Instructions burned: 132 (million) % 7.56/2.06 % (947997)ott-21_1_sil=16000:fs=off:random_seed=4164506771:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.56/2.06 % (947992)Instruction limit reached! % 7.56/2.06 % (947992)------------------------------ % 7.56/2.06 % (947992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.56/2.06 % (947992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/2.06 % (947992)CaDiCaL version: 2.1.3 % 7.56/2.06 % (947992)Termination reason: Instruction limit % 7.56/2.06 % (947992)Termination phase: Saturation % 7.56/2.06 % (947992)Time elapsed: 0.079 s % 7.56/2.06 % (947992)Peak memory usage: 13 MB % 7.56/2.06 % (947992)Instructions burned: 132 (million) % 7.56/2.06 % (947998)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1000205508:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 35.96/5.68 % (947983)Instruction limit reached! % 35.96/5.68 % (947983)------------------------------ % 35.96/5.68 % (947983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.68 % (947983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.68 % (947983)CaDiCaL version: 2.1.3 % 35.96/5.68 % (947983)Termination reason: Instruction limit % 35.96/5.68 % (947983)Termination phase: Saturation % 35.96/5.68 % (947983)Time elapsed: 0.159 s % 35.96/5.68 % (947983)Peak memory usage: 13 MB % 35.96/5.68 % (947983)Instructions burned: 159 (million) % 35.96/5.68 % (948000)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2456920492:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 35.96/5.68 % Exception at run slice level % 35.96/5.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.96/5.68 % (948004)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2988722918:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 35.96/5.68 % (948002)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=59724733:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 35.96/5.68 % Exception at run slice level % 35.96/5.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.96/5.68 % (948007)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=1539520599:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 35.96/5.68 % (947997)Instruction limit reached! % 35.96/5.68 % (947997)------------------------------ % 35.96/5.68 % (947997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.68 % (947997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.68 % (947997)CaDiCaL version: 2.1.3 % 35.96/5.68 % (947997)Termination reason: Instruction limit % 35.96/5.68 % (947997)Termination phase: Saturation % 35.96/5.68 % (947997)Time elapsed: 0.085 s % 35.96/5.68 % (947997)Peak memory usage: 12 MB % 35.96/5.68 % (947997)Instructions burned: 182 (million) % 35.96/5.68 % (948009)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=43882388:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.96/5.68 % (948007)Instruction limit reached! % 35.96/5.68 % (948007)------------------------------ % 35.96/5.68 % (948007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.68 % (948007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.68 % (948007)CaDiCaL version: 2.1.3 % 35.96/5.68 % (948007)Termination reason: Instruction limit % 35.96/5.68 % (948007)Termination phase: Saturation % 35.96/5.68 % (948007)Time elapsed: 0.369 s % 35.96/5.68 % (948007)Peak memory usage: 18 MB % 35.96/5.68 % (948007)Instructions burned: 694 (million) % 35.96/5.68 % (948011)fmb+10_1_sil=64000:random_seed=3986303603:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 35.96/5.68 % (947998)Instruction limit reached! % 35.96/5.68 % (947998)------------------------------ % 35.96/5.68 % (947998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.68 % (947998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.68 % (947998)CaDiCaL version: 2.1.3 % 35.96/5.68 % (947998)Termination reason: Instruction limit % 35.96/5.68 % (947998)Termination phase: Saturation % 35.96/5.68 % (947998)Time elapsed: 0.464 s % 35.96/5.68 % (947998)Peak memory usage: 14 MB % 35.96/5.68 % (947998)Instructions burned: 477 (million) % 35.96/5.68 % (948011)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 35.96/5.68 % Exception at run slice level % 35.96/5.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.96/5.68 % (948014)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=57689084:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 35.96/5.68 % Exception at run slice level % 35.96/5.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.96/5.68 % (948013)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2229070004:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 35.96/5.68 % Exception at run slice level % 35.96/5.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.96/5.68 % (948016)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1902310522:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 99.94/14.61 % (948018)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=746505518:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 99.94/14.61 % (948018)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 99.94/14.61 % (947994)Instruction limit reached! % 99.94/14.61 % (947994)------------------------------ % 99.94/14.61 % (947994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.94/14.61 % (947994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.94/14.61 % (947994)CaDiCaL version: 2.1.3 % 99.94/14.61 % (947994)Termination reason: Instruction limit % 99.94/14.61 % (947994)Termination phase: Saturation % 99.94/14.61 % (947994)Time elapsed: 0.606 s % 99.94/14.61 % (947994)Peak memory usage: 17 MB % 99.94/14.61 % (947994)Instructions burned: 685 (million) % 99.94/14.61 % (948021)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3536228393:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 99.94/14.61 % Exception at run slice level % 99.94/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 99.94/14.61 % (948023)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3712531881:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 99.94/14.61 % Exception at run slice level % 99.94/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 99.94/14.61 % (948025)ott-2_1_sil=16000:newcnf=on:random_seed=3071527213:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 99.94/14.61 % (948009)Instruction limit reached! % 99.94/14.61 % (948009)------------------------------ % 99.94/14.61 % (948009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.94/14.61 % (948009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.94/14.61 % (948009)CaDiCaL version: 2.1.3 % 99.94/14.61 % (948009)Termination reason: Instruction limit % 99.94/14.61 % (948009)Termination phase: Saturation % 99.94/14.61 % (948009)Time elapsed: 0.802 s % 99.94/14.61 % (948009)Peak memory usage: 18 MB % 99.94/14.61 % (948009)Instructions burned: 880 (million) % 99.94/14.61 % (948027)ott+10_1_sil=32000:tgt=ground:random_seed=4201748881:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 99.94/14.61 % (948002)Instruction limit reached! % 99.94/14.61 % (948002)------------------------------ % 99.94/14.61 % (948002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.94/14.61 % (948002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.94/14.61 % (948002)CaDiCaL version: 2.1.3 % 99.94/14.61 % (948002)Termination reason: Instruction limit % 99.94/14.61 % (948002)Termination phase: Saturation % 99.94/14.61 % (948002)Time elapsed: 0.952 s % 99.94/14.61 % (948002)Peak memory usage: 18 MB % 99.94/14.61 % (948002)Instructions burned: 1179 (million) % 99.94/14.61 % (948029)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2426394917:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 99.94/14.61 % Exception at run slice level % 99.94/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 99.94/14.61 % (948031)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1806004533:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 99.94/14.61 % (948018)Instruction limit reached! % 99.94/14.61 % (948018)------------------------------ % 99.94/14.61 % (948018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.94/14.61 % (948018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.94/14.61 % (948018)CaDiCaL version: 2.1.3 % 99.94/14.61 % (948018)Termination reason: Instruction limit % 99.94/14.61 % (948018)Termination phase: Saturation % 99.94/14.61 % (948018)Time elapsed: 0.703 s % 99.94/14.61 % (948018)Peak memory usage: 27 MB % 99.94/14.61 % (948018)Instructions burned: 1472 (million) % 99.94/14.61 % (948033)dis+21_1_sil=32000:sas=cadical:random_seed=1864518190:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 99.94/14.61 % (948025)Instruction limit reached! % 99.94/14.61 % (948025)------------------------------ % 99.94/14.61 % (948025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.94/14.61 % (948025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.94/14.61 % (948025)CaDiCaL version: 2.1.3 % 202.96/29.07 % (948025)Termination reason: Instruction limit % 202.96/29.07 % (948025)Termination phase: Saturation % 202.96/29.07 % (948025)Time elapsed: 0.725 s % 202.96/29.07 % (948025)Peak memory usage: 20 MB % 202.96/29.07 % (948025)Instructions burned: 870 (million) % 202.96/29.07 % (948035)ott+11_1_sil=16000:gs=on:random_seed=1600556969:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 202.96/29.07 % (948031)Instruction limit reached! % 202.96/29.07 % (948031)------------------------------ % 202.96/29.07 % (948031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.96/29.07 % (948031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.96/29.07 % (948031)CaDiCaL version: 2.1.3 % 202.96/29.07 % (948031)Termination reason: Instruction limit % 202.96/29.07 % (948031)Termination phase: Saturation % 202.96/29.07 % (948031)Time elapsed: 1.780 s % 202.96/29.07 % (948031)Peak memory usage: 34 MB % 202.96/29.07 % (948031)Instructions burned: 3514 (million) % 202.96/29.07 % (948037)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1957296097:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 202.96/29.07 % Exception at run slice level % 202.96/29.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.96/29.07 % (948039)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=261489726:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 202.96/29.07 % (948035)Instruction limit reached! % 202.96/29.07 % (948035)------------------------------ % 202.96/29.07 % (948035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.96/29.07 % (948035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.96/29.07 % (948035)CaDiCaL version: 2.1.3 % 202.96/29.07 % (948035)Termination reason: Instruction limit % 202.96/29.07 % (948035)Termination phase: Saturation % 202.96/29.07 % (948035)Time elapsed: 2.172 s % 202.96/29.07 % (948035)Peak memory usage: 28 MB % 202.96/29.07 % (948035)Instructions burned: 2251 (million) % 202.96/29.07 % (948043)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=575450687:i=29340_2962 on theBenchmark for (2962ds/29340Mi) % 202.96/29.07 % (948033)Instruction limit reached! % 202.96/29.07 % (948033)------------------------------ % 202.96/29.07 % (948033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.96/29.07 % (948033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.96/29.07 % (948033)CaDiCaL version: 2.1.3 % 202.96/29.07 % (948033)Termination reason: Instruction limit % 202.96/29.07 % (948033)Termination phase: Saturation % 202.96/29.07 % (948033)Time elapsed: 3.324 s % 202.96/29.07 % (948033)Peak memory usage: 37 MB % 202.96/29.07 % (948033)Instructions burned: 3773 (million) % 202.96/29.07 % (948047)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3455689146:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 202.96/29.07 % (948039)Instruction limit reached! % 202.96/29.07 % (948039)------------------------------ % 202.96/29.07 % (948039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.96/29.07 % (948039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.96/29.07 % (948039)CaDiCaL version: 2.1.3 % 202.96/29.07 % (948039)Termination reason: Instruction limit % 202.96/29.07 % (948039)Termination phase: Saturation % 202.96/29.07 % (948039)Time elapsed: 1.990 s % 202.96/29.07 % (948039)Peak memory usage: 30 MB % 202.96/29.07 % (948039)Instructions burned: 4591 (million) % 202.96/29.07 % (948050)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3032031967:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi) % 202.96/29.07 % Exception at run slice level % 202.96/29.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.96/29.07 % (948052)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3668066006:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 202.96/29.07 % Exception at run slice level % 202.96/29.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.96/29.07 % (948054)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3059396849:i=14071_2948 on theBenchmark for (2948ds/14071Mi) % 202.96/29.07 % Exception at run slice level % 202.96/29.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.96/29.07 % (948016)Instruction limit reached! % 202.96/29.07 % (948016)------------------------------ % 210.02/30.04 % (948016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948016)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948016)Termination reason: Instruction limit % 210.02/30.04 % (948016)Termination phase: Saturation % 210.02/30.04 % (948016)Time elapsed: 4.478 s % 210.02/30.04 % (948016)Peak memory usage: 44 MB % 210.02/30.04 % (948016)Instructions burned: 5131 (million) % 210.02/30.04 % (948056)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3470713123:i=22565:add=on:rawr=on_2948 on theBenchmark for (2948ds/22565Mi) % 210.02/30.04 % (948058)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3550618582:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi) % 210.02/30.04 % (948027)Instruction limit reached! % 210.02/30.04 % (948027)------------------------------ % 210.02/30.04 % (948027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948027)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948027)Termination reason: Instruction limit % 210.02/30.04 % (948027)Termination phase: Saturation % 210.02/30.04 % (948027)Time elapsed: 4.645 s % 210.02/30.04 % (948027)Peak memory usage: 54 MB % 210.02/30.04 % (948027)Instructions burned: 5114 (million) % 210.02/30.04 % (948061)dis+10_16:1_sil=16000:random_seed=3582273261:i=9155:fsr=off_2942 on theBenchmark for (2942ds/9155Mi) % 210.02/30.04 % (948047)Instruction limit reached! % 210.02/30.04 % (948047)------------------------------ % 210.02/30.04 % (948047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948047)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948047)Termination reason: Instruction limit % 210.02/30.04 % (948047)Termination phase: Saturation % 210.02/30.04 % (948047)Time elapsed: 4.733 s % 210.02/30.04 % (948047)Peak memory usage: 45 MB % 210.02/30.04 % (948047)Instructions burned: 5211 (million) % 210.02/30.04 % (948089)ott-3_8_sil=64000:random_seed=1272364679:i=20139:bs=on_2904 on theBenchmark for (2904ds/20139Mi) % 210.02/30.04 % (948058)Instruction limit reached! % 210.02/30.04 % (948058)------------------------------ % 210.02/30.04 % (948058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948058)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948058)Termination reason: Instruction limit % 210.02/30.04 % (948058)Termination phase: Saturation % 210.02/30.04 % (948058)Time elapsed: 7.922 s % 210.02/30.04 % (948058)Peak memory usage: 64 MB % 210.02/30.04 % (948058)Instructions burned: 8173 (million) % 210.02/30.04 % (948095)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=921368377:fmbsr=2:i=32576_2868 on theBenchmark for (2868ds/32576Mi) % 210.02/30.04 % Exception at run slice level % 210.02/30.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 210.02/30.04 % (948097)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=230771313:i=11404_2868 on theBenchmark for (2868ds/11404Mi) % 210.02/30.04 % (948061)Instruction limit reached! % 210.02/30.04 % (948061)------------------------------ % 210.02/30.04 % (948061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948061)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948061)Termination reason: Instruction limit % 210.02/30.04 % (948061)Termination phase: Saturation % 210.02/30.04 % (948061)Time elapsed: 7.930 s % 210.02/30.04 % (948061)Peak memory usage: 59 MB % 210.02/30.04 % (948061)Instructions burned: 9156 (million) % 210.02/30.04 % (948101)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3564887621:i=14134_2862 on theBenchmark for (2862ds/14134Mi) % 210.02/30.04 % (948056)Instruction limit reached! % 210.02/30.04 % (948056)------------------------------ % 210.02/30.04 % (948056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.02/30.04 % (948056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.02/30.04 % (948056)CaDiCaL version: 2.1.3 % 210.02/30.04 % (948056)Termination reason: Instruction limit % 210.02/30.04 % (948056)Termination phase: Saturation % 210.02/30.04 % (948056)Time elapsed: 8.898 s % 210.02/30.04 % (948056)Peak memory usage: 30 MB % 210.02/30.04 % (948056)Instructions burned: 22568 (million) % 210.02/30.04 % (948104)dis+33_16_sil=32000:sac=on:random_seed=3470316092:i=15851:nm=0_2859 on theBenchmark for (2859ds/15851Mi) % 230.40/32.98 % (948104)Instruction limit reached! % 230.40/32.98 % (948104)------------------------------ % 230.40/32.98 % (948104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.40/32.98 % (948104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.40/32.98 % (948104)CaDiCaL version: 2.1.3 % 230.40/32.98 % (948104)Termination reason: Instruction limit % 230.40/32.98 % (948104)Termination phase: Saturation % 230.40/32.98 % (948104)Time elapsed: 7.266 s % 230.40/32.98 % (948104)Peak memory usage: 92 MB % 230.40/32.98 % (948104)Instructions burned: 15852 (million) % 230.40/32.98 % (948134)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1675536122:avsq=on:i=17627:add=on:amm=off_2786 on theBenchmark for (2786ds/17627Mi) % 230.40/32.98 % (948097)Instruction limit reached! % 230.40/32.98 % (948097)------------------------------ % 230.40/32.98 % (948097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.40/32.98 % (948097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.40/32.98 % (948097)CaDiCaL version: 2.1.3 % 230.40/32.98 % (948097)Termination reason: Instruction limit % 230.40/32.98 % (948097)Termination phase: Saturation % 230.40/32.98 % (948097)Time elapsed: 10.629 s % 230.40/32.98 % (948097)Peak memory usage: 81 MB % 230.40/32.98 % (948097)Instructions burned: 11405 (million) % 230.40/32.98 % (948154)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=916098160:s2a=on:i=53295_2761 on theBenchmark for (2761ds/53295Mi) % 230.40/32.98 % (948101)Instruction limit reached! % 230.40/32.98 % (948101)------------------------------ % 230.40/32.98 % (948101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.40/32.98 % (948101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.40/32.98 % (948101)CaDiCaL version: 2.1.3 % 230.40/32.98 % (948101)Termination reason: Instruction limit % 230.40/32.98 % (948101)Termination phase: Saturation % 230.40/32.98 % (948101)Time elapsed: 14.160 s % 230.40/32.98 % (948101)Peak memory usage: 92 MB % 230.40/32.98 % (948101)Instructions burned: 14134 (million) % 230.40/32.98 % (948180)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1742474444:i=26857:ins=20_2720 on theBenchmark for (2720ds/26857Mi) % 230.40/32.98 % Exception at run slice level % 230.40/32.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.40/32.98 % (948182)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1184911874:i=28120:bs=on:fsr=off_2720 on theBenchmark for (2720ds/28120Mi) % 230.40/32.98 % (948134)Instruction limit reached! % 230.40/32.98 % (948134)------------------------------ % 230.40/32.98 % (948134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.40/32.98 % (948134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.40/32.98 % (948134)CaDiCaL version: 2.1.3 % 230.40/32.98 % (948134)Termination reason: Instruction limit % 230.40/32.98 % (948134)Termination phase: Saturation % 230.40/32.98 % (948134)Time elapsed: 7.091 s % 230.40/32.98 % (948134)Peak memory usage: 116 MB % 230.40/32.98 % (948134)Instructions burned: 17628 (million) % 230.40/32.98 % (948268)fmb+10_1_sil=256000:fmbss=7:random_seed=3007429504:fmbsr=1.6:i=182295_2715 on theBenchmark for (2715ds/182295Mi) % 230.40/32.98 % Exception at run slice level % 230.40/32.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.40/32.98 % (948270)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4045669961:i=44625:gsp=on_2714 on theBenchmark for (2714ds/44625Mi) % 230.40/32.98 % (948270)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 230.40/32.98 % Exception at run slice level % 230.40/32.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.40/32.98 % (948272)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=735014376:i=160505_2714 on theBenchmark for (2714ds/160505Mi) % 230.40/32.98 % Exception at run slice level % 230.40/32.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.40/32.98 % (948274)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2735268634:fmbsr=1.3:i=225729_2714 on theBenchmark for (2714ds/225729Mi) % 230.40/32.98 % Exception at run slice level % 230.40/32.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.40/32.98 % (948276)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=835023571:fmbsr=2:i=185024:ins=7_2714 on theBenchmark for (2714ds/185024Mi) % 290.75/41.44 % Exception at run slice level % 290.75/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 290.75/41.44 % (948278)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3897723758:rtra=on_2714 on theBenchmark for (2714ds/0Mi) % 290.75/41.44 % Exception at run slice level % 290.75/41.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 290.75/41.44 % (948280)% WARNING: option uhcvi not known. % 290.75/41.44 % (948280)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1842977516:i=271062:add=off:rtra=on:rawr=on_2714 on theBenchmark for (2714ds/271062Mi) % 290.75/41.44 % (948089)Instruction limit reached! % 290.75/41.44 % (948089)------------------------------ % 290.75/41.44 % (948089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.75/41.44 % (948089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.75/41.44 % (948089)CaDiCaL version: 2.1.3 % 290.75/41.44 % (948089)Termination reason: Instruction limit % 290.75/41.44 % (948089)Termination phase: Saturation % 290.75/41.44 % (948089)Time elapsed: 19.298 s % 290.75/41.44 % (948089)Peak memory usage: 114 MB % 290.75/41.44 % (948089)Instructions burned: 20139 (million) % 290.75/41.44 % (948043)Instruction limit reached! % 290.75/41.44 % (948043)------------------------------ % 290.75/41.44 % (948043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.75/41.44 % (948043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.75/41.44 % (948043)CaDiCaL version: 2.1.3 % 290.75/41.44 % (948043)Termination reason: Instruction limit % 290.75/41.44 % (948043)Termination phase: Saturation % 290.75/41.44 % (948043)Time elapsed: 25.081 s % 290.75/41.44 % (948043)Peak memory usage: 155 MB % 290.75/41.44 % (948043)Instructions burned: 29342 (million) % 290.75/41.44 % (948312)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1377768806:i=176048:add=on:rtra=on:rawr=on_2711 on theBenchmark for (2711ds/176048Mi) % 290.75/41.44 % (948317)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2866593741:i=206:fgj=on:rtra=on_2710 on theBenchmark for (2710ds/206Mi) % 290.75/41.44 % (948317)Instruction limit reached! % 290.75/41.44 % (948317)------------------------------ % 290.75/41.44 % (948317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.75/41.44 % (948317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.75/41.44 % (948317)CaDiCaL version: 2.1.3 % 290.75/41.44 % (948317)Termination reason: Instruction limit % 290.75/41.44 % (948317)Termination phase: Saturation % 290.75/41.44 % (948317)Time elapsed: 0.108 s % 290.75/41.44 % (948317)Peak memory usage: 13 MB % 290.75/41.44 % (948317)Instructions burned: 206 (million) % 290.75/41.44 % (948355)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2984472903:i=232:rtra=on_2709 on theBenchmark for (2709ds/232Mi) % 290.75/41.44 % (948355)Instruction limit reached! % 290.75/41.44 % (948355)------------------------------ % 290.75/41.44 % (948355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.75/41.44 % (948355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.75/41.44 % (948355)CaDiCaL version: 2.1.3 % 290.75/41.44 % (948355)Termination reason: Instruction limit % 290.75/41.44 % (948355)Termination phase: Saturation % 290.75/41.44 % (948355)Time elapsed: 0.124 s % 290.75/41.44 % (948355)Peak memory usage: 14 MB % 290.75/41.44 % (948355)Instructions burned: 232 (million) % 290.75/41.44 % (948357)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=161005416:i=262:rtra=on_2708 on theBenchmark for (2708ds/262Mi) % 290.75/41.44 % (948357)Instruction limit reached! % 290.75/41.44 % (948357)------------------------------ % 290.75/41.44 % (948357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.75/41.44 % (948357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.75/41.44 % (948357)CaDiCaL version: 2.1.3 % 290.75/41.44 % (948357)Termination reason: Instruction limit % 290.75/41.44 % (948357)Termination phase: Saturation % 290.75/41.44 % (948357)Time elapsed: 0.135 s % 290.75/41.44 % (948357)Peak memory usage: 14 MB % 290.75/41.44 % (948357)Instructions burned: 263 (million) % 290.75/41.44 % (948359)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=887309521:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2706 on theBenchmark for (2706ds/318Mi) % 290.75/41.44 % (948359)Instruction limit reached! % 290.75/41.44 % (948359)------------------------------ % 290.75/41.44 % (948359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.83 % (948359)CaDiCaL version: 2.1.3 % 300.36/42.83 % (948359)Termination reason: Instruction limit % 300.36/42.83 % (948359)Termination phase: Saturation % 300.36/42.83 % (948359)Time elapsed: 0.183 s % 300.36/42.83 % (948359)Peak memory usage: 14 MB % 300.36/42.83 % (948359)Instructions burned: 318 (million) % 300.36/42.83 % (948361)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1706107600:i=1428:nm=2:rtra=on_2704 on theBenchmark for (2704ds/1428Mi) % 300.36/42.83 % Exception at run slice level % 300.36/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.36/42.83 % (948363)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=5822074:i=262:bd=preordered:rtra=on:fsd=on_2704 on theBenchmark for (2704ds/262Mi) % 300.36/42.83 % (948363)Instruction limit reached! % 300.36/42.83 % (948363)------------------------------ % 300.36/42.83 % (948363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.83 % (948363)CaDiCaL version: 2.1.3 % 300.36/42.83 % (948363)Termination reason: Instruction limit % 300.36/42.83 % (948363)Termination phase: Saturation % 300.36/42.83 % (948363)Time elapsed: 0.156 s % 300.36/42.83 % (948363)Peak memory usage: 14 MB % 300.36/42.83 % (948363)Instructions burned: 264 (million) % 300.36/42.83 % (948365)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=917766651:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2702 on theBenchmark for (2702ds/1368Mi) % 300.36/42.83 % (948365)Instruction limit reached! % 300.36/42.83 % (948365)------------------------------ % 300.36/42.83 % (948365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.83 % (948365)CaDiCaL version: 2.1.3 % 300.36/42.83 % (948365)Termination reason: Instruction limit % 300.36/42.83 % (948365)Termination phase: Saturation % 300.36/42.83 % (948365)Time elapsed: 0.674 s % 300.36/42.83 % (948365)Peak memory usage: 21 MB % 300.36/42.83 % (948365)Instructions burned: 1369 (million) % 300.36/42.83 % (948367)ott-21_1_sil=16000:si=on:fs=off:random_seed=700482156:i=360:av=off:fsr=off:rtra=on_2695 on theBenchmark for (2695ds/360Mi) % 300.36/42.83 % (948367)Instruction limit reached! % 300.36/42.83 % (948367)------------------------------ % 300.36/42.83 % (948367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.83 % (948367)CaDiCaL version: 2.1.3 % 300.36/42.83 % (948367)Termination reason: Instruction limit % 300.36/42.83 % (948367)Termination phase: Saturation % 300.36/42.83 % (948367)Time elapsed: 0.176 s % 300.36/42.83 % (948367)Peak memory usage: 13 MB % 300.36/42.83 % (948367)Instructions burned: 362 (million) % 300.36/42.83 % (948369)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=542818842:i=954:bd=all:rtra=on_2693 on theBenchmark for (2693ds/954Mi) % 300.36/42.83 % (948369)Instruction limit reached! % 300.36/42.83 % (948369)------------------------------ % 300.36/42.83 % (948369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.83 % (948369)CaDiCaL version: 2.1.3 % 300.36/42.83 % (948369)Termination reason: Instruction limit % 300.36/42.83 % (948369)Termination phase: Saturation % 300.36/42.83 % (948369)Time elapsed: 0.530 s % 300.36/42.83 % (948369)Peak memory usage: 17 MB % 300.36/42.83 % (948369)Instructions burned: 954 (million) % 300.36/42.83 % (948371)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=792452266:fmbsr=1.3:i=1730:ins=25:rtra=on_2688 on theBenchmark for (2688ds/1730Mi) % 300.36/42.83 % Exception at run slice level % 300.36/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.36/42.83 % (948373)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1658328544:i=2358:rtra=on_2688 on theBenchmark for (2688ds/2358Mi) % 300.36/42.83 % (948373)Instruction limit reached! % 300.36/42.83 % (948373)------------------------------ % 300.36/42.83 % (948373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.83 % (948373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c4 % 300.36/42.83 Terminated % 300.36/42.83 % Vampire exiting % 300.36/42.84 Terminated %------------------------------------------------------------------------------