%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW472^2 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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 : Wed Sep 30 08:40:22 AM UTC 2026 % Result : Timeout 300.09s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW472^2 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n011.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Tue Sep 29 16:05:16 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.22/0.28 Running first-order model finding % 0.22/0.28 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.34/1.52 % (269290)Will run a generic schedule for satisfiability detection. % 7.34/1.52 % (269296)% WARNING: option uhcvi not known. % 7.34/1.52 % (269299)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2039413868:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.34/1.52 % (269296)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1117972099:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.34/1.52 % (269298)dis+10_1_sil=32000:sp=arity:random_seed=1562952472:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.34/1.52 % (269295)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=81089213_2999 on theBenchmark for (2999ds/0Mi) % 7.34/1.52 % (269297)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3403588888:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.34/1.52 % (269300)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1566737945:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.34/1.52 % (269299)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 7.34/1.52 % (269301)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=43305464:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.34/1.52 % (269296)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 7.34/1.52 % (269299)Instruction limit reached! % 7.34/1.52 % (269299)------------------------------ % 7.34/1.52 % (269299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.52 % (269299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.52 % (269299)CaDiCaL version: 2.1.3 % 7.34/1.52 % (269299)Termination reason: Instruction limit % 7.34/1.52 % (269299)Termination phase: Saturation % 7.34/1.52 % (269299)Time elapsed: 0.051 s % 7.34/1.52 % (269299)Peak memory usage: 13 MB % 7.34/1.52 % (269299)Instructions burned: 122 (million) % 7.34/1.52 % (269309)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=50324340:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.34/1.52 % (269296)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 7.34/1.52 % Exception at run slice level % 7.34/1.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.34/1.52 % (269298)Instruction limit reached! % 7.34/1.52 % (269298)------------------------------ % 7.34/1.52 % (269298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.52 % (269298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.52 % (269298)CaDiCaL version: 2.1.3 % 7.34/1.52 % (269298)Termination reason: Instruction limit % 7.34/1.52 % (269298)Termination phase: Saturation % 7.34/1.52 % (269298)Time elapsed: 0.081 s % 7.34/1.52 % (269298)Peak memory usage: 12 MB % 7.34/1.52 % (269298)Instructions burned: 104 (million) % 7.34/1.52 % (269311)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3918111574:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.34/1.52 % (269300)Instruction limit reached! % 7.34/1.52 % (269300)------------------------------ % 7.34/1.52 % (269300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.52 % (269300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.52 % (269300)CaDiCaL version: 2.1.3 % 7.34/1.52 % (269300)Termination reason: Instruction limit % 7.34/1.52 % (269300)Termination phase: Saturation % 7.34/1.52 % (269300)Time elapsed: 0.106 s % 7.34/1.52 % (269300)Peak memory usage: 13 MB % 7.34/1.52 % (269300)Instructions burned: 133 (million) % 7.34/1.52 % Exception at run slice level % 7.34/1.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.34/1.52 % (269312)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=263683160:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.34/1.52 % (269301)Instruction limit reached! % 7.34/1.52 % (269301)------------------------------ % 7.34/1.52 % (269301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.52 % (269301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.52 % (269301)CaDiCaL version: 2.1.3 % 7.34/1.52 % (269301)Termination reason: Instruction limit % 7.34/1.52 % (269301)Termination phase: Saturation % 31.65/4.99 % (269301)Time elapsed: 0.132 s % 31.65/4.99 % (269301)Peak memory usage: 14 MB % 31.65/4.99 % (269301)Instructions burned: 160 (million) % 31.65/4.99 % (269314)ott-21_1_sil=16000:fs=off:random_seed=2788878332:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 31.65/4.99 % (269315)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=382851405:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 31.65/4.99 % (269312)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.65/4.99 % (269311)Instruction limit reached! % 31.65/4.99 % (269311)------------------------------ % 31.65/4.99 % (269311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.65/4.99 % (269311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.65/4.99 % (269311)CaDiCaL version: 2.1.3 % 31.65/4.99 % (269311)Termination reason: Instruction limit % 31.65/4.99 % (269311)Termination phase: Saturation % 31.65/4.99 % (269311)Time elapsed: 0.057 s % 31.65/4.99 % (269311)Peak memory usage: 13 MB % 31.65/4.99 % (269311)Instructions burned: 133 (million) % 31.65/4.99 % (269317)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1536114196:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 31.65/4.99 % (269320)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3015827556:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 31.65/4.99 % (269312)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 31.65/4.99 % Exception at run slice level % 31.65/4.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.65/4.99 % (269323)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3923989735:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 31.65/4.99 % (269314)Instruction limit reached! % 31.65/4.99 % (269314)------------------------------ % 31.65/4.99 % (269314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.65/4.99 % (269314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.65/4.99 % (269314)CaDiCaL version: 2.1.3 % 31.65/4.99 % (269314)Termination reason: Instruction limit % 31.65/4.99 % (269314)Termination phase: Saturation % 31.65/4.99 % (269314)Time elapsed: 0.149 s % 31.65/4.99 % (269314)Peak memory usage: 13 MB % 31.65/4.99 % (269314)Instructions burned: 181 (million) % 31.65/4.99 % Exception at run slice level % 31.65/4.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.65/4.99 % (269325)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=1205312937: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) % 31.65/4.99 % (269327)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1930683482:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.65/4.99 % (269325)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.65/4.99 % (269327)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.65/4.99 % (269315)Instruction limit reached! % 31.65/4.99 % (269315)------------------------------ % 31.65/4.99 % (269315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.65/4.99 % (269315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.65/4.99 % (269315)CaDiCaL version: 2.1.3 % 31.65/4.99 % (269315)Termination reason: Instruction limit % 31.65/4.99 % (269315)Termination phase: Saturation % 31.65/4.99 % (269315)Time elapsed: 0.417 s % 31.65/4.99 % (269315)Peak memory usage: 14 MB % 31.65/4.99 % (269315)Instructions burned: 477 (million) % 31.65/4.99 % (269329)fmb+10_1_sil=64000:random_seed=2863823426:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 31.65/4.99 % (269329)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 31.65/4.99 % Exception at run slice level % 31.65/4.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.65/4.99 % (269312)Instruction limit reached! % 31.65/4.99 % (269312)------------------------------ % 31.65/4.99 % (269312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.65/4.99 % (269312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.65/4.99 % (269312)CaDiCaL version: 2.1.3 % 31.65/4.99 % (269312)Termination reason: Instruction limit % 84.67/12.22 % (269312)Termination phase: Saturation % 84.67/12.22 % (269312)Time elapsed: 0.584 s % 84.67/12.22 % (269312)Peak memory usage: 16 MB % 84.67/12.22 % (269312)Instructions burned: 684 (million) % 84.67/12.22 % (269331)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2593634730:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 84.67/12.22 % (269320)Instruction limit reached! % 84.67/12.22 % (269320)------------------------------ % 84.67/12.22 % (269320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.67/12.22 % (269320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.67/12.22 % (269320)CaDiCaL version: 2.1.3 % 84.67/12.22 % (269320)Termination reason: Instruction limit % 84.67/12.22 % (269320)Termination phase: Saturation % 84.67/12.22 % (269320)Time elapsed: 0.540 s % 84.67/12.22 % (269320)Peak memory usage: 19 MB % 84.67/12.22 % (269320)Instructions burned: 1180 (million) % 84.67/12.22 % (269334)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1364013172:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 84.67/12.22 % (269332)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4177259393:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 84.67/12.22 % (269334)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 84.67/12.22 % Exception at run slice level % 84.67/12.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.67/12.22 % Exception at run slice level % 84.67/12.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.67/12.22 % (269337)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3348085951:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 84.67/12.22 % (269338)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3083103137:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 84.67/12.22 % (269337)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 84.67/12.22 % Exception at run slice level % 84.67/12.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.67/12.22 % (269337)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 84.67/12.22 % (269341)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=614049354:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 84.67/12.22 % (269325)Instruction limit reached! % 84.67/12.22 % (269325)------------------------------ % 84.67/12.22 % (269325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.67/12.22 % (269325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.67/12.22 % (269325)CaDiCaL version: 2.1.3 % 84.67/12.22 % (269325)Termination reason: Instruction limit % 84.67/12.22 % (269325)Termination phase: Saturation % 84.67/12.22 % (269325)Time elapsed: 0.592 s % 84.67/12.22 % (269325)Peak memory usage: 17 MB % 84.67/12.22 % (269325)Instructions burned: 692 (million) % 84.67/12.22 % (269343)ott-2_1_sil=16000:newcnf=on:random_seed=2847726541:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 84.67/12.22 % (269343)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 84.67/12.22 % Exception at run slice level % 84.67/12.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.67/12.22 % (269345)ott+10_1_sil=32000:tgt=ground:random_seed=1917280795:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 84.67/12.22 % (269327)Instruction limit reached! % 84.67/12.22 % (269327)------------------------------ % 84.67/12.22 % (269327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.67/12.22 % (269327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.67/12.22 % (269327)CaDiCaL version: 2.1.3 % 84.67/12.22 % (269327)Termination reason: Instruction limit % 84.67/12.22 % (269327)Termination phase: Saturation % 84.67/12.22 % (269327)Time elapsed: 0.736 s % 84.67/12.22 % (269327)Peak memory usage: 19 MB % 84.67/12.22 % (269327)Instructions burned: 879 (million) % 84.67/12.22 % (269347)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=138498383:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 84.67/12.22 % Exception at run slice level % 84.67/12.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 84.67/12.22 % (269351)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1493416256:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 172.71/24.70 % (269351)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 172.71/24.70 % (269343)Instruction limit reached! % 172.71/24.70 % (269343)------------------------------ % 172.71/24.70 % (269343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.71/24.70 % (269343)CaDiCaL version: 2.1.3 % 172.71/24.70 % (269343)Termination reason: Instruction limit % 172.71/24.70 % (269343)Termination phase: Saturation % 172.71/24.70 % (269343)Time elapsed: 0.667 s % 172.71/24.70 % (269343)Peak memory usage: 17 MB % 172.71/24.70 % (269343)Instructions burned: 869 (million) % 172.71/24.70 % (269353)dis+21_1_sil=32000:sas=cadical:random_seed=2991357944:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 172.71/24.70 % (269337)Instruction limit reached! % 172.71/24.70 % (269337)------------------------------ % 172.71/24.70 % (269337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.71/24.70 % (269337)CaDiCaL version: 2.1.3 % 172.71/24.70 % (269337)Termination reason: Instruction limit % 172.71/24.70 % (269337)Termination phase: Saturation % 172.71/24.70 % (269337)Time elapsed: 1.250 s % 172.71/24.70 % (269337)Peak memory usage: 20 MB % 172.71/24.70 % (269337)Instructions burned: 1472 (million) % 172.71/24.70 % (269355)ott+11_1_sil=16000:gs=on:random_seed=335734938:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 172.71/24.70 % (269355)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 172.71/24.70 % (269334)Instruction limit reached! % 172.71/24.70 % (269334)------------------------------ % 172.71/24.70 % (269334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.71/24.70 % (269334)CaDiCaL version: 2.1.3 % 172.71/24.70 % (269334)Termination reason: Instruction limit % 172.71/24.70 % (269334)Termination phase: Saturation % 172.71/24.70 % (269334)Time elapsed: 2.168 s % 172.71/24.70 % (269334)Peak memory usage: 27 MB % 172.71/24.70 % (269334)Instructions burned: 5132 (million) % 172.71/24.70 % (269363)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2460831902:fmbsr=1.6:i=67534_2970 on theBenchmark for (2970ds/67534Mi) % 172.71/24.70 % Exception at run slice level % 172.71/24.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 172.71/24.70 % (269365)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1077512309:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 172.71/24.70 % (269355)Instruction limit reached! % 172.71/24.70 % (269355)------------------------------ % 172.71/24.70 % (269355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.71/24.70 % (269355)CaDiCaL version: 2.1.3 % 172.71/24.70 % (269355)Termination reason: Instruction limit % 172.71/24.70 % (269355)Termination phase: Saturation % 172.71/24.70 % (269355)Time elapsed: 1.867 s % 172.71/24.70 % (269355)Peak memory usage: 23 MB % 172.71/24.70 % (269355)Instructions burned: 2251 (million) % 172.71/24.70 % (269375)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3561510291:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 172.71/24.70 % (269351)Instruction limit reached! % 172.71/24.70 % (269351)------------------------------ % 172.71/24.70 % (269351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.71/24.70 % (269351)CaDiCaL version: 2.1.3 % 172.71/24.70 % (269351)Termination reason: Instruction limit % 172.71/24.70 % (269351)Termination phase: Saturation % 172.71/24.70 % (269351)Time elapsed: 2.855 s % 172.71/24.70 % (269351)Peak memory usage: 26 MB % 172.71/24.70 % (269351)Instructions burned: 3512 (million) % 172.71/24.70 % (269377)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1352789331:i=5211_2959 on theBenchmark for (2959ds/5211Mi) % 172.71/24.70 % (269365)Instruction limit reached! % 172.71/24.70 % (269365)------------------------------ % 172.71/24.70 % (269365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.71/24.70 % (269365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.17 % (269365)CaDiCaL version: 2.1.3 % 233.28/33.17 % (269365)Termination reason: Instruction limit % 233.28/33.17 % (269365)Termination phase: Saturation % 233.28/33.17 % (269365)Time elapsed: 1.655 s % 233.28/33.17 % (269365)Peak memory usage: 31 MB % 233.28/33.17 % (269365)Instructions burned: 4593 (million) % 233.28/33.17 % (269383)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1471244755:i=5497:nm=2_2953 on theBenchmark for (2953ds/5497Mi) % 233.28/33.17 % Exception at run slice level % 233.28/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.28/33.17 % (269385)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1898279192:fmbsr=2:i=46332_2952 on theBenchmark for (2952ds/46332Mi) % 233.28/33.17 % Exception at run slice level % 233.28/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.28/33.17 % (269387)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2169751079:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 233.28/33.17 % (269353)Instruction limit reached! % 233.28/33.17 % (269353)------------------------------ % 233.28/33.17 % (269353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.28/33.17 % (269353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.17 % (269353)CaDiCaL version: 2.1.3 % 233.28/33.17 % (269353)Termination reason: Instruction limit % 233.28/33.17 % (269353)Termination phase: Saturation % 233.28/33.17 % (269353)Time elapsed: 3.143 s % 233.28/33.17 % (269353)Peak memory usage: 26 MB % 233.28/33.17 % (269353)Instructions burned: 3773 (million) % 233.28/33.17 % (269389)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=689507425:i=22565:add=on:rawr=on_2951 on theBenchmark for (2951ds/22565Mi) % 233.28/33.17 % Exception at run slice level % 233.28/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.28/33.17 % (269391)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3334661702:i=8173:av=off_2951 on theBenchmark for (2951ds/8173Mi) % 233.28/33.17 % (269345)Instruction limit reached! % 233.28/33.17 % (269345)------------------------------ % 233.28/33.17 % (269345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.28/33.17 % (269345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.17 % (269345)CaDiCaL version: 2.1.3 % 233.28/33.17 % (269345)Termination reason: Instruction limit % 233.28/33.17 % (269345)Termination phase: Saturation % 233.28/33.17 % (269345)Time elapsed: 4.232 s % 233.28/33.17 % (269345)Peak memory usage: 33 MB % 233.28/33.17 % (269345)Instructions burned: 5115 (million) % 233.28/33.17 % (269397)dis+10_16:1_sil=16000:random_seed=1390905955:i=9155:fsr=off_2946 on theBenchmark for (2946ds/9155Mi) % 233.28/33.17 % (269377)Instruction limit reached! % 233.28/33.17 % (269377)------------------------------ % 233.28/33.17 % (269377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.28/33.17 % (269377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.17 % (269377)CaDiCaL version: 2.1.3 % 233.28/33.17 % (269377)Termination reason: Instruction limit % 233.28/33.17 % (269377)Termination phase: Saturation % 233.28/33.17 % (269377)Time elapsed: 4.311 s % 233.28/33.17 % (269377)Peak memory usage: 43 MB % 233.28/33.17 % (269377)Instructions burned: 5212 (million) % 233.28/33.17 % (269413)ott-3_8_sil=64000:random_seed=419122505:i=20139:bs=on_2915 on theBenchmark for (2915ds/20139Mi) % 233.28/33.17 % (269391)Instruction limit reached! % 233.28/33.17 % (269391)------------------------------ % 233.28/33.17 % (269391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.28/33.17 % (269391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.17 % (269391)CaDiCaL version: 2.1.3 % 233.28/33.17 % (269391)Termination reason: Instruction limit % 233.28/33.17 % (269391)Termination phase: Saturation % 233.28/33.17 % (269391)Time elapsed: 6.874 s % 233.28/33.17 % (269391)Peak memory usage: 36 MB % 233.28/33.17 % (269391)Instructions burned: 8173 (million) % 233.28/33.17 % (269415)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1416537134:fmbsr=2:i=32576_2882 on theBenchmark for (2882ds/32576Mi) % 233.28/33.17 % Exception at run slice level % 233.28/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.28/33.17 % (269417)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2067217532:i=11404_2880 on theBenchmark for (2880ds/11404Mi) % 243.04/34.55 % (269397)Instruction limit reached! % 243.04/34.55 % (269397)------------------------------ % 243.04/34.55 % (269397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269397)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269397)Termination reason: Instruction limit % 243.04/34.55 % (269397)Termination phase: Saturation % 243.04/34.55 % (269397)Time elapsed: 7.467 s % 243.04/34.55 % (269397)Peak memory usage: 52 MB % 243.04/34.55 % (269397)Instructions burned: 9155 (million) % 243.04/34.55 % (269421)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1455717073:i=14134_2871 on theBenchmark for (2871ds/14134Mi) % 243.04/34.55 % (269421)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 243.04/34.55 % (269389)Instruction limit reached! % 243.04/34.55 % (269389)------------------------------ % 243.04/34.55 % (269389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269389)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269389)Termination reason: Instruction limit % 243.04/34.55 % (269389)Termination phase: Saturation % 243.04/34.55 % (269389)Time elapsed: 10.176 s % 243.04/34.55 % (269389)Peak memory usage: 78 MB % 243.04/34.55 % (269389)Instructions burned: 22566 (million) % 243.04/34.55 % (269431)dis+33_16_sil=32000:sac=on:random_seed=270798311:i=15851:nm=0_2849 on theBenchmark for (2849ds/15851Mi) % 243.04/34.55 % (269417)Instruction limit reached! % 243.04/34.55 % (269417)------------------------------ % 243.04/34.55 % (269417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269417)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269417)Termination reason: Instruction limit % 243.04/34.55 % (269417)Termination phase: Saturation % 243.04/34.55 % (269417)Time elapsed: 9.538 s % 243.04/34.55 % (269417)Peak memory usage: 86 MB % 243.04/34.55 % (269417)Instructions burned: 11404 (million) % 243.04/34.55 % (269439)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4240327907:avsq=on:i=17627:add=on:amm=off_2785 on theBenchmark for (2785ds/17627Mi) % 243.04/34.55 % (269431)Instruction limit reached! % 243.04/34.55 % (269431)------------------------------ % 243.04/34.55 % (269431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269431)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269431)Termination reason: Instruction limit % 243.04/34.55 % (269431)Termination phase: Saturation % 243.04/34.55 % (269431)Time elapsed: 6.760 s % 243.04/34.55 % (269431)Peak memory usage: 56 MB % 243.04/34.55 % (269431)Instructions burned: 15853 (million) % 243.04/34.55 % (269441)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=920010951:s2a=on:i=53295_2781 on theBenchmark for (2781ds/53295Mi) % 243.04/34.55 % (269413)Instruction limit reached! % 243.04/34.55 % (269413)------------------------------ % 243.04/34.55 % (269413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269413)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269413)Termination reason: Instruction limit % 243.04/34.55 % (269413)Termination phase: Saturation % 243.04/34.55 % (269413)Time elapsed: 15.662 s % 243.04/34.55 % (269413)Peak memory usage: 60 MB % 243.04/34.55 % (269413)Instructions burned: 20140 (million) % 243.04/34.55 % (269445)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3100525275:i=26857:ins=20_2758 on theBenchmark for (2758ds/26857Mi) % 243.04/34.55 % Exception at run slice level % 243.04/34.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 243.04/34.55 % (269447)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1167254867:i=28120:bs=on:fsr=off_2757 on theBenchmark for (2757ds/28120Mi) % 243.04/34.55 % (269421)Instruction limit reached! % 243.04/34.55 % (269421)------------------------------ % 243.04/34.55 % (269421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.04/34.55 % (269421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/34.55 % (269421)CaDiCaL version: 2.1.3 % 243.04/34.55 % (269421)Termination reason: Instruction limit % 243.04/34.55 % (269421)Termination phase: Saturation % 243.04/34.55 % (269421)Time elapsed: 11.565 s % 264.11/37.50 % (269421)Peak memory usage: 72 MB % 264.11/37.50 % (269421)Instructions burned: 14135 (million) % 264.11/37.50 % (269449)fmb+10_1_sil=256000:fmbss=7:random_seed=3404799173:fmbsr=1.6:i=182295_2755 on theBenchmark for (2755ds/182295Mi) % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269451)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1344310900:i=44625:gsp=on_2754 on theBenchmark for (2754ds/44625Mi) % 264.11/37.50 % (269451)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 264.11/37.50 % (269451)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269453)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2234990726:i=160505_2753 on theBenchmark for (2753ds/160505Mi) % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269457)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2323449885:fmbsr=1.3:i=225729_2752 on theBenchmark for (2752ds/225729Mi) % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269461)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1386446260:fmbsr=2:i=185024:ins=7_2751 on theBenchmark for (2751ds/185024Mi) % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269463)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1876008570:rtra=on_2750 on theBenchmark for (2750ds/0Mi) % 264.11/37.50 % Exception at run slice level % 264.11/37.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.11/37.50 % (269465)% WARNING: option uhcvi not known. % 264.11/37.50 % (269465)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2741206211:i=271062:add=off:rtra=on:rawr=on_2749 on theBenchmark for (2749ds/271062Mi) % 264.11/37.50 % (269465)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 264.11/37.50 % (269465)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 264.11/37.50 % (269375)Instruction limit reached! % 264.11/37.50 % (269375)------------------------------ % 264.11/37.50 % (269375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.11/37.50 % (269375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.11/37.50 % (269375)CaDiCaL version: 2.1.3 % 264.11/37.50 % (269375)Termination reason: Instruction limit % 264.11/37.50 % (269375)Termination phase: Saturation % 264.11/37.50 % (269375)Time elapsed: 23.473 s % 264.11/37.50 % (269375)Peak memory usage: 80 MB % 264.11/37.50 % (269375)Instructions burned: 29340 (million) % 264.11/37.50 % (269496)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=781789981:i=176048:add=on:rtra=on:rawr=on_2724 on theBenchmark for (2724ds/176048Mi) % 264.11/37.50 % (269439)Instruction limit reached! % 264.11/37.50 % (269439)------------------------------ % 264.11/37.50 % (269439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.11/37.50 % (269439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.11/37.50 % (269439)CaDiCaL version: 2.1.3 % 264.11/37.50 % (269439)Termination reason: Instruction limit % 264.11/37.50 % (269439)Termination phase: Saturation % 264.11/37.50 % (269439)Time elapsed: 11.242 s % 264.11/37.50 % (269439)Peak memory usage: 60 MB % 264.11/37.50 % (269439)Instructions burned: 17629 (million) % 264.11/37.50 % (269623)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1228891860:i=206:fgj=on:rtra=on_2672 on theBenchmark for (2672ds/206Mi) % 264.11/37.50 % (269623)Instruction limit reached! % 264.11/37.50 % (269623)------------------------------ % 264.11/37.50 % (269623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.11/37.50 % (269623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.11/37.50 % (269623)CaDiCaL version: 2.1.3 % 264.11/37.50 % (269623)Termination reason: Instruction limit % 264.11/37.50 % (269623)Termination phase: Saturation % 264.11/37.50 % (269623)Time elapsed: 0.098 s % 279.24/39.63 % (269623)Peak memory usage: 14 MB % 279.24/39.63 % (269623)Instructions burned: 207 (million) % 279.24/39.63 % (269625)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1791131258:i=232:rtra=on_2671 on theBenchmark for (2671ds/232Mi) % 279.24/39.63 % (269625)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 279.24/39.63 % (269625)Instruction limit reached! % 279.24/39.63 % (269625)------------------------------ % 279.24/39.63 % (269625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.24/39.63 % (269625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.24/39.63 % (269625)CaDiCaL version: 2.1.3 % 279.24/39.63 % (269625)Termination reason: Instruction limit % 279.24/39.63 % (269625)Termination phase: Saturation % 279.24/39.63 % (269625)Time elapsed: 0.114 s % 279.24/39.63 % (269625)Peak memory usage: 14 MB % 279.24/39.63 % (269625)Instructions burned: 233 (million) % 279.24/39.63 % (269627)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2327114539:i=262:rtra=on_2669 on theBenchmark for (2669ds/262Mi) % 279.24/39.63 % (269627)Instruction limit reached! % 279.24/39.63 % (269627)------------------------------ % 279.24/39.63 % (269627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.24/39.63 % (269627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.24/39.63 % (269627)CaDiCaL version: 2.1.3 % 279.24/39.63 % (269627)Termination reason: Instruction limit % 279.24/39.63 % (269627)Termination phase: Saturation % 279.24/39.63 % (269627)Time elapsed: 0.129 s % 279.24/39.63 % (269627)Peak memory usage: 14 MB % 279.24/39.63 % (269627)Instructions burned: 264 (million) % 279.24/39.63 % (269629)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2602815024:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2668 on theBenchmark for (2668ds/318Mi) % 279.24/39.63 % (269629)Instruction limit reached! % 279.24/39.63 % (269629)------------------------------ % 279.24/39.63 % (269629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.24/39.63 % (269629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.24/39.63 % (269629)CaDiCaL version: 2.1.3 % 279.24/39.63 % (269629)Termination reason: Instruction limit % 279.24/39.63 % (269629)Termination phase: Saturation % 279.24/39.63 % (269629)Time elapsed: 0.156 s % 279.24/39.63 % (269629)Peak memory usage: 15 MB % 279.24/39.63 % (269629)Instructions burned: 318 (million) % 279.24/39.63 % (269631)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=315142173:i=1428:nm=2:rtra=on_2666 on theBenchmark for (2666ds/1428Mi) % 279.24/39.63 % Exception at run slice level % 279.24/39.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.24/39.63 % (269633)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3014910022:i=262:bd=preordered:rtra=on:fsd=on_2665 on theBenchmark for (2665ds/262Mi) % 279.24/39.63 % (269633)Instruction limit reached! % 279.24/39.63 % (269633)------------------------------ % 279.24/39.63 % (269633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.24/39.63 % (269633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.24/39.63 % (269633)CaDiCaL version: 2.1.3 % 279.24/39.63 % (269633)Termination reason: Instruction limit % 279.24/39.63 % (269633)Termination phase: Saturation % 279.24/39.63 % (269633)Time elapsed: 0.134 s % 279.24/39.63 % (269633)Peak memory usage: 14 MB % 279.24/39.63 % (269633)Instructions burned: 263 (million) % 279.24/39.63 % (269635)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=4032138201:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2664 on theBenchmark for (2664ds/1368Mi) % 279.24/39.63 % (269635)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 279.24/39.63 % (269635)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 279.24/39.63 % (269635)Instruction limit reached! % 279.24/39.63 % (269635)------------------------------ % 279.24/39.63 % (269635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.24/39.63 % (269635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.24/39.63 % (269635)CaDiCaL version: 2.1.3 % 279.24/39.63 % (269635)Termination reason: Instruction limit % 279.24/39.63 % (269635)Termination phase: Saturation % 279.24/39.63 % (269635)Time elapsed: 0.664 s % 279.24/39.63 % (269635)Peak memory usage: 17 MB % 279.24/39.63 % (269635)Instructions burned: 1368 (million) % 279.24/39.63 % (269637)ott-21_1_sil=16000:si=on:fs=off:random_seed=3683684496:i=360:av=off:fsr=off:rtra=on_2657 on theBenchmark for (2657ds/360Mi) % 300.09/42.63 % (269637)Instruction limit reached! % 300.09/42.63 % (269637)------------------------------ % 300.09/42.63 % (269637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.63 % (269637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.63 % (269637)CaDiCaL version: 2.1.3 % 300.09/42.63 % (269637)Termination reason: Instruction limit % 300.09/42.63 % (269637)Termination phase: Saturation % 300.09/42.63 % (269637)Time elapsed: 0.161 s % 300.09/42.63 % (269637)Peak memory usage: 14 MB % 300.09/42.63 % (269637)Instructions burned: 361 (million) % 300.09/42.63 % (269639)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4202946790:i=954:bd=all:rtra=on_2655 on theBenchmark for (2655ds/954Mi) % 300.09/42.63 % (269639)Instruction limit reached! % 300.09/42.63 % (269639)------------------------------ % 300.09/42.63 % (269639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.63 % (269639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.63 % (269639)CaDiCaL version: 2.1.3 % 300.09/42.63 % (269639)Termination reason: Instruction limit % 300.09/42.63 % (269639)Termination phase: Saturation % 300.09/42.63 % (269639)Time elapsed: 0.471 s % 300.09/42.63 % (269639)Peak memory usage: 16 MB % 300.09/42.63 % (269639)Instructions burned: 955 (million) % 300.09/42.63 % (269641)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1241055775:fmbsr=1.3:i=1730:ins=25:rtra=on_2650 on theBenchmark for (2650ds/1730Mi) % 300.09/42.63 % Exception at run slice level % 300.09/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.09/42.63 % (269643)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1842157522:i=2358:rtra=on_2650 on theBenchmark for (2650ds/2358Mi) % 300.09/42.63 % (269643)Instruction limit reached! % 300.09/42.63 % (269643)------------------------------ % 300.09/42.63 % (269643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.63 % (269643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.63 % (269643)CaDiCaL version: 2.1.3 % 300.09/42.63 % (269643)Termination reason: Instruction limit % 300.09/42.63 % (269643)Termination phase: Saturation % 300.09/42.63 % (269643)Time elapsed: 1.168 s % 300.09/42.63 % (269643)Peak memory usage: 26 MB % 300.09/42.63 % (269643)Instructions burned: 2358 (million) % 300.09/42.63 % (269646)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3766545993:i=1778:ins=1:rtra=on_2638 on theBenchmark for (2638ds/1778Mi) % 300.09/42.63 % Exception at run slice level % 300.09/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.09/42.63 % (269648)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=2803669870:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2637 on theBenchmark for (2637ds/1384Mi) % 300.09/42.63 % (269648)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 300.09/42.63 % (269648)Instruction limit reached! % 300.09/42.63 % (269648)------------------------------ % 300.09/42.63 % (269648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.63 % (269648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.63 % (269648)CaDiCaL version: 2.1.3 % 300.09/42.63 % (269648)Termination reason: Instruction limit % 300.09/42.63 % (269648)Termination phase: Saturation % 300.09/42.63 % (269648)Time elapsed: 0.686 s % 300.09/42.63 % (269648)Peak memory usage: 21 MB % 300.09/42.63 % (269648)Instructions burned: 1384 (million) % 300.09/42.63 % (269650)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3978969983:i=1758:kws=inv_precedence:fsr=off:rtra=on_2630 on theBenchmark for (2630ds/1758Mi) % 300.09/42.63 % (269650)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 300.09/42.63 % (269441)Instruction limit reached! % 300.09/42.63 % (269441)------------------------------ % 300.09/42.63 % (269441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.63 % (269441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.63 % (269441)CaDiCaL version: 2.1.3 % 300.09/42.63 % (269441)Termination reason: Instruction limit % 300.09/42.63 % (269441)Termination phase: Saturation % 300.09/42.63 % (269441)Time elapse % 300.09/42.63 Terminated % 300.09/42.63 % Vampire exiting % 300.09/42.64 Terminated %------------------------------------------------------------------------------