%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM027_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 : n007.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 09:40:11 AM UTC 2026 % Result : Timeout 300.65s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : COM027_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n007.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 21:47:11 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 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.45/1.47 % (2885203)Will run a generic schedule for satisfiability detection. % 7.45/1.47 % (2885211)dis+10_1_sil=32000:sp=arity:random_seed=3195023604:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.45/1.47 % (2885209)% WARNING: option uhcvi not known. % 7.45/1.47 % (2885208)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1780423751_2999 on theBenchmark for (2999ds/0Mi) % 7.45/1.47 % (2885209)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2594217294:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.45/1.47 % (2885210)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3949860544:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.45/1.47 % (2885212)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=545559822:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.45/1.47 % (2885214)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=607662876:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.45/1.47 % (2885213)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1044046771:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.45/1.47 % Exception at run slice level % 7.45/1.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.45/1.47 % (2885222)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1421492311:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.45/1.47 % (2885211)Instruction limit reached! % 7.45/1.47 % (2885211)------------------------------ % 7.45/1.47 % (2885211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.45/1.47 % (2885211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.47 % (2885211)CaDiCaL version: 2.1.3 % 7.45/1.47 % (2885211)Termination reason: Instruction limit % 7.45/1.47 % (2885211)Termination phase: Saturation % 7.45/1.47 % (2885211)Time elapsed: 0.036 s % 7.45/1.47 % (2885211)Peak memory usage: 12 MB % 7.45/1.47 % (2885211)Instructions burned: 105 (million) % 7.45/1.47 % Exception at run slice level % 7.45/1.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.45/1.47 % (2885224)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3638419419:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.45/1.47 % (2885225)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=3966318883:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.45/1.47 % (2885212)Instruction limit reached! % 7.45/1.47 % (2885212)------------------------------ % 7.45/1.47 % (2885212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.45/1.47 % (2885212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.47 % (2885212)CaDiCaL version: 2.1.3 % 7.45/1.47 % (2885212)Termination reason: Instruction limit % 7.45/1.47 % (2885212)Termination phase: Saturation % 7.45/1.47 % (2885212)Time elapsed: 0.070 s % 7.45/1.47 % (2885212)Peak memory usage: 13 MB % 7.45/1.47 % (2885212)Instructions burned: 118 (million) % 7.45/1.47 % (2885213)Instruction limit reached! % 7.45/1.47 % (2885213)------------------------------ % 7.45/1.47 % (2885213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.45/1.47 % (2885213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.47 % (2885213)CaDiCaL version: 2.1.3 % 7.45/1.47 % (2885213)Termination reason: Instruction limit % 7.45/1.47 % (2885213)Termination phase: Saturation % 7.45/1.47 % (2885213)Time elapsed: 0.077 s % 7.45/1.47 % (2885213)Peak memory usage: 13 MB % 7.45/1.47 % (2885213)Instructions burned: 131 (million) % 7.45/1.47 % (2885224)Instruction limit reached! % 7.45/1.47 % (2885224)------------------------------ % 7.45/1.47 % (2885224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.45/1.47 % (2885224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.47 % (2885224)CaDiCaL version: 2.1.3 % 7.45/1.47 % (2885224)Termination reason: Instruction limit % 7.45/1.47 % (2885224)Termination phase: Saturation % 7.45/1.47 % (2885224)Time elapsed: 0.048 s % 7.45/1.47 % (2885224)Peak memory usage: 13 MB % 7.45/1.47 % (2885224)Instructions burned: 132 (million) % 7.45/1.47 % (2885228)ott-21_1_sil=16000:fs=off:random_seed=3318541059:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.45/1.47 % (2885229)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2627843788:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 20.95/3.22 % (2885230)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=106157620:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.95/3.22 % Exception at run slice level % 20.95/3.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.22 % (2885214)Instruction limit reached! % 20.95/3.22 % (2885214)------------------------------ % 20.95/3.22 % (2885214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.22 % (2885214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.22 % (2885214)CaDiCaL version: 2.1.3 % 20.95/3.22 % (2885214)Termination reason: Instruction limit % 20.95/3.22 % (2885214)Termination phase: Saturation % 20.95/3.22 % (2885214)Time elapsed: 0.103 s % 20.95/3.22 % (2885214)Peak memory usage: 14 MB % 20.95/3.22 % (2885214)Instructions burned: 159 (million) % 20.95/3.22 % (2885234)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2866628640:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.95/3.22 % (2885235)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3801481155:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.95/3.22 % Exception at run slice level % 20.95/3.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.22 % (2885238)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=3772271985:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 20.95/3.22 % (2885228)Instruction limit reached! % 20.95/3.22 % (2885228)------------------------------ % 20.95/3.22 % (2885228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.22 % (2885228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.22 % (2885228)CaDiCaL version: 2.1.3 % 20.95/3.22 % (2885228)Termination reason: Instruction limit % 20.95/3.22 % (2885228)Termination phase: Saturation % 20.95/3.22 % (2885228)Time elapsed: 0.093 s % 20.95/3.22 % (2885228)Peak memory usage: 13 MB % 20.95/3.22 % (2885228)Instructions burned: 180 (million) % 20.95/3.22 % (2885240)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4105966078:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.95/3.22 % (2885229)Instruction limit reached! % 20.95/3.22 % (2885229)------------------------------ % 20.95/3.22 % (2885229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.22 % (2885229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.22 % (2885229)CaDiCaL version: 2.1.3 % 20.95/3.22 % (2885229)Termination reason: Instruction limit % 20.95/3.22 % (2885229)Termination phase: Saturation % 20.95/3.22 % (2885229)Time elapsed: 0.290 s % 20.95/3.22 % (2885229)Peak memory usage: 15 MB % 20.95/3.22 % (2885229)Instructions burned: 478 (million) % 20.95/3.22 % (2885242)fmb+10_1_sil=64000:random_seed=132679919:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 20.95/3.22 % (2885242)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.95/3.22 % Exception at run slice level % 20.95/3.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.22 % (2885244)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3407482794:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 20.95/3.22 % Exception at run slice level % 20.95/3.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.95/3.22 % (2885225)Instruction limit reached! % 20.95/3.22 % (2885225)------------------------------ % 20.95/3.22 % (2885225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.22 % (2885225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.22 % (2885225)CaDiCaL version: 2.1.3 % 20.95/3.22 % (2885225)Termination reason: Instruction limit % 20.95/3.22 % (2885225)Termination phase: Saturation % 20.95/3.22 % (2885225)Time elapsed: 0.393 s % 20.95/3.22 % (2885225)Peak memory usage: 16 MB % 20.95/3.22 % (2885225)Instructions burned: 685 (million) % 20.95/3.22 % (2885246)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3067600014:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 20.95/3.22 % (2885247)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1887081840:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 62.35/9.06 % Exception at run slice level % 62.35/9.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 62.35/9.06 % (2885250)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3749500636:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 62.35/9.06 % (2885234)Instruction limit reached! % 62.35/9.06 % (2885234)------------------------------ % 62.35/9.06 % (2885234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.35/9.06 % (2885234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.35/9.06 % (2885234)CaDiCaL version: 2.1.3 % 62.35/9.06 % (2885234)Termination reason: Instruction limit % 62.35/9.06 % (2885234)Termination phase: Saturation % 62.35/9.06 % (2885234)Time elapsed: 0.378 s % 62.35/9.06 % (2885234)Peak memory usage: 20 MB % 62.35/9.06 % (2885234)Instructions burned: 1180 (million) % 62.35/9.06 % (2885250)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.35/9.06 % (2885238)Instruction limit reached! % 62.35/9.06 % (2885238)------------------------------ % 62.35/9.06 % (2885238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.35/9.06 % (2885238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.35/9.06 % (2885238)CaDiCaL version: 2.1.3 % 62.35/9.06 % (2885238)Termination reason: Instruction limit % 62.35/9.06 % (2885238)Termination phase: Saturation % 62.35/9.06 % (2885238)Time elapsed: 0.349 s % 62.35/9.06 % (2885238)Peak memory usage: 15 MB % 62.35/9.06 % (2885238)Instructions burned: 693 (million) % 62.35/9.06 % (2885252)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1769778285:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 62.35/9.06 % Exception at run slice level % 62.35/9.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 62.35/9.06 % (2885255)ott-2_1_sil=16000:newcnf=on:random_seed=3723717681:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 62.35/9.06 % (2885253)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=652856132:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 62.35/9.06 % Exception at run slice level % 62.35/9.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 62.35/9.06 % (2885258)ott+10_1_sil=32000:tgt=ground:random_seed=2014302201:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 62.35/9.06 % (2885240)Instruction limit reached! % 62.35/9.06 % (2885240)------------------------------ % 62.35/9.06 % (2885240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.35/9.06 % (2885240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.35/9.06 % (2885240)CaDiCaL version: 2.1.3 % 62.35/9.06 % (2885240)Termination reason: Instruction limit % 62.35/9.06 % (2885240)Termination phase: Saturation % 62.35/9.06 % (2885240)Time elapsed: 0.491 s % 62.35/9.06 % (2885240)Peak memory usage: 19 MB % 62.35/9.06 % (2885240)Instructions burned: 879 (million) % 62.35/9.06 % (2885260)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1418593926:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 62.35/9.06 % Exception at run slice level % 62.35/9.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 62.35/9.06 % (2885262)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3180123774:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 62.35/9.06 % (2885255)Instruction limit reached! % 62.35/9.06 % (2885255)------------------------------ % 62.35/9.06 % (2885255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.35/9.06 % (2885255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.35/9.06 % (2885255)CaDiCaL version: 2.1.3 % 62.35/9.06 % (2885255)Termination reason: Instruction limit % 62.35/9.06 % (2885255)Termination phase: Saturation % 62.35/9.06 % (2885255)Time elapsed: 0.260 s % 62.35/9.06 % (2885255)Peak memory usage: 16 MB % 62.35/9.06 % (2885255)Instructions burned: 870 (million) % 62.35/9.06 % (2885264)dis+21_1_sil=32000:sas=cadical:random_seed=1087326974:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 62.35/9.06 % (2885250)Instruction limit reached! % 62.35/9.06 % (2885250)------------------------------ % 62.35/9.06 % (2885250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.35/16.54 % (2885250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.35/16.54 % (2885250)CaDiCaL version: 2.1.3 % 115.35/16.54 % (2885250)Termination reason: Instruction limit % 115.35/16.54 % (2885250)Termination phase: Saturation % 115.35/16.54 % (2885250)Time elapsed: 0.704 s % 115.35/16.54 % (2885250)Peak memory usage: 24 MB % 115.35/16.54 % (2885250)Instructions burned: 1473 (million) % 115.35/16.54 % (2885266)ott+11_1_sil=16000:gs=on:random_seed=988128854:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 115.35/16.54 % (2885264)Instruction limit reached! % 115.35/16.54 % (2885264)------------------------------ % 115.35/16.54 % (2885264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.35/16.54 % (2885264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.35/16.54 % (2885264)CaDiCaL version: 2.1.3 % 115.35/16.54 % (2885264)Termination reason: Instruction limit % 115.35/16.54 % (2885264)Termination phase: Saturation % 115.35/16.54 % (2885264)Time elapsed: 1.082 s % 115.35/16.54 % (2885264)Peak memory usage: 33 MB % 115.35/16.54 % (2885264)Instructions burned: 3774 (million) % 115.35/16.54 % (2885268)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=614994766:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 115.35/16.54 % Exception at run slice level % 115.35/16.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.35/16.54 % (2885270)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=719644718:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 115.35/16.54 % (2885266)Instruction limit reached! % 115.35/16.54 % (2885266)------------------------------ % 115.35/16.54 % (2885266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.35/16.54 % (2885266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.35/16.54 % (2885266)CaDiCaL version: 2.1.3 % 115.35/16.54 % (2885266)Termination reason: Instruction limit % 115.35/16.54 % (2885266)Termination phase: Saturation % 115.35/16.54 % (2885266)Time elapsed: 1.089 s % 115.35/16.54 % (2885266)Peak memory usage: 21 MB % 115.35/16.54 % (2885266)Instructions burned: 2252 (million) % 115.35/16.54 % (2885272)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3918524651:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 115.35/16.54 % (2885262)Instruction limit reached! % 115.35/16.54 % (2885262)------------------------------ % 115.35/16.54 % (2885262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.35/16.54 % (2885262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.35/16.54 % (2885262)CaDiCaL version: 2.1.3 % 115.35/16.54 % (2885262)Termination reason: Instruction limit % 115.35/16.54 % (2885262)Termination phase: Saturation % 115.35/16.54 % (2885262)Time elapsed: 1.954 s % 115.35/16.54 % (2885262)Peak memory usage: 26 MB % 115.35/16.54 % (2885262)Instructions burned: 3512 (million) % 115.35/16.54 % (2885274)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=975928666:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 115.35/16.54 % (2885270)Instruction limit reached! % 115.35/16.54 % (2885270)------------------------------ % 115.35/16.54 % (2885270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.35/16.54 % (2885270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.35/16.54 % (2885270)CaDiCaL version: 2.1.3 % 115.35/16.54 % (2885270)Termination reason: Instruction limit % 115.35/16.54 % (2885270)Termination phase: Saturation % 115.35/16.54 % (2885270)Time elapsed: 0.992 s % 115.35/16.54 % (2885270)Peak memory usage: 28 MB % 115.35/16.54 % (2885270)Instructions burned: 4596 (million) % 115.35/16.54 % (2885276)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3598856123:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 115.35/16.54 % Exception at run slice level % 115.35/16.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.35/16.54 % (2885278)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=131780036:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 115.35/16.54 % Exception at run slice level % 115.35/16.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.35/16.54 % (2885280)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2409339861:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 115.35/16.54 % Exception at run slice level % 122.24/17.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 122.24/17.59 % (2885282)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4294497622:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 122.24/17.59 % (2885247)Instruction limit reached! % 122.24/17.59 % (2885247)------------------------------ % 122.24/17.59 % (2885247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885247)CaDiCaL version: 2.1.3 % 122.24/17.59 % (2885247)Termination reason: Instruction limit % 122.24/17.59 % (2885247)Termination phase: Saturation % 122.24/17.59 % (2885247)Time elapsed: 2.539 s % 122.24/17.59 % (2885247)Peak memory usage: 26 MB % 122.24/17.59 % (2885247)Instructions burned: 5133 (million) % 122.24/17.59 % (2885284)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=786707320:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 122.24/17.59 % (2885258)Instruction limit reached! % 122.24/17.59 % (2885258)------------------------------ % 122.24/17.59 % (2885258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885258)CaDiCaL version: 2.1.3 % 122.24/17.59 % (2885258)Termination reason: Instruction limit % 122.24/17.59 % (2885258)Termination phase: Saturation % 122.24/17.59 % (2885258)Time elapsed: 2.823 s % 122.24/17.59 % (2885258)Peak memory usage: 35 MB % 122.24/17.59 % (2885258)Instructions burned: 5116 (million) % 122.24/17.59 % (2885286)dis+10_16:1_sil=16000:random_seed=3000449930:i=9155:fsr=off_2965 on theBenchmark for (2965ds/9155Mi) % 122.24/17.59 % (2885274)Instruction limit reached! % 122.24/17.59 % (2885274)------------------------------ % 122.24/17.59 % (2885274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885274)CaDiCaL version: 2.1.3 % 122.24/17.59 % (2885274)Termination reason: Instruction limit % 122.24/17.59 % (2885274)Termination phase: Saturation % 122.24/17.59 % (2885274)Time elapsed: 2.688 s % 122.24/17.59 % (2885274)Peak memory usage: 41 MB % 122.24/17.59 % (2885274)Instructions burned: 5211 (million) % 122.24/17.59 % (2885288)ott-3_8_sil=64000:random_seed=1723156367:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 122.24/17.59 % (2885284)Instruction limit reached! % 122.24/17.59 % (2885284)------------------------------ % 122.24/17.59 % (2885284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885284)CaDiCaL version: 2.1.3 % 122.24/17.59 % (2885284)Termination reason: Instruction limit % 122.24/17.59 % (2885284)Termination phase: Saturation % 122.24/17.59 % (2885284)Time elapsed: 3.974 s % 122.24/17.59 % (2885284)Peak memory usage: 55 MB % 122.24/17.59 % (2885284)Instructions burned: 8175 (million) % 122.24/17.59 % (2885290)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3912692901:fmbsr=2:i=32576_2929 on theBenchmark for (2929ds/32576Mi) % 122.24/17.59 % Exception at run slice level % 122.24/17.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 122.24/17.59 % (2885292)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=74006746:i=11404_2929 on theBenchmark for (2929ds/11404Mi) % 122.24/17.59 % (2885286)Instruction limit reached! % 122.24/17.59 % (2885286)------------------------------ % 122.24/17.59 % (2885286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885286)CaDiCaL version: 2.1.3 % 122.24/17.59 % (2885286)Termination reason: Instruction limit % 122.24/17.59 % (2885286)Termination phase: Saturation % 122.24/17.59 % (2885286)Time elapsed: 4.498 s % 122.24/17.59 % (2885286)Peak memory usage: 66 MB % 122.24/17.59 % (2885286)Instructions burned: 9157 (million) % 122.24/17.59 % (2885294)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1814206415:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 122.24/17.59 % (2885282)Instruction limit reached! % 122.24/17.59 % (2885282)------------------------------ % 122.24/17.59 % (2885282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.24/17.59 % (2885282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.24/17.59 % (2885282)CaDiCaL version: 2.1.3 % 131.38/18.83 % (2885282)Termination reason: Instruction limit % 131.38/18.83 % (2885282)Termination phase: Saturation % 131.38/18.83 % (2885282)Time elapsed: 5.830 s % 131.38/18.83 % (2885282)Peak memory usage: 94 MB % 131.38/18.83 % (2885282)Instructions burned: 22566 (million) % 131.38/18.83 % (2885296)dis+33_16_sil=32000:sac=on:random_seed=567232935:i=15851:nm=0_2911 on theBenchmark for (2911ds/15851Mi) % 131.38/18.83 % (2885296)Instruction limit reached! % 131.38/18.83 % (2885296)------------------------------ % 131.38/18.83 % (2885296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.38/18.83 % (2885296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.38/18.83 % (2885296)CaDiCaL version: 2.1.3 % 131.38/18.83 % (2885296)Termination reason: Instruction limit % 131.38/18.83 % (2885296)Termination phase: Saturation % 131.38/18.83 % (2885296)Time elapsed: 4.302 s % 131.38/18.83 % (2885296)Peak memory usage: 119 MB % 131.38/18.83 % (2885296)Instructions burned: 15852 (million) % 131.38/18.83 % (2885298)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=423600610:avsq=on:i=17627:add=on:amm=off_2868 on theBenchmark for (2868ds/17627Mi) % 131.38/18.83 % (2885292)Instruction limit reached! % 131.38/18.83 % (2885292)------------------------------ % 131.38/18.83 % (2885292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.38/18.83 % (2885292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.38/18.83 % (2885292)CaDiCaL version: 2.1.3 % 131.38/18.83 % (2885292)Termination reason: Instruction limit % 131.38/18.83 % (2885292)Termination phase: Saturation % 131.38/18.83 % (2885292)Time elapsed: 6.422 s % 131.38/18.83 % (2885292)Peak memory usage: 50 MB % 131.38/18.83 % (2885292)Instructions burned: 11405 (million) % 131.38/18.83 % (2885302)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1399651832:s2a=on:i=53295_2864 on theBenchmark for (2864ds/53295Mi) % 131.38/18.83 % (2885272)Instruction limit reached! % 131.38/18.83 % (2885272)------------------------------ % 131.38/18.83 % (2885272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.38/18.83 % (2885272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.38/18.83 % (2885272)CaDiCaL version: 2.1.3 % 131.38/18.83 % (2885272)Termination reason: Instruction limit % 131.38/18.83 % (2885272)Termination phase: Saturation % 131.38/18.83 % (2885272)Time elapsed: 12.334 s % 131.38/18.83 % (2885272)Peak memory usage: 156 MB % 131.38/18.83 % (2885272)Instructions burned: 29341 (million) % 131.38/18.83 % (2885348)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=337369702:i=26857:ins=20_2852 on theBenchmark for (2852ds/26857Mi) % 131.38/18.83 % Exception at run slice level % 131.38/18.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.38/18.83 % (2885350)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=496636990:i=28120:bs=on:fsr=off_2852 on theBenchmark for (2852ds/28120Mi) % 131.38/18.83 % (2885294)Instruction limit reached! % 131.38/18.83 % (2885294)------------------------------ % 131.38/18.83 % (2885294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.38/18.83 % (2885294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.38/18.83 % (2885294)CaDiCaL version: 2.1.3 % 131.38/18.83 % (2885294)Termination reason: Instruction limit % 131.38/18.83 % (2885294)Termination phase: Saturation % 131.38/18.83 % (2885294)Time elapsed: 8.234 s % 131.38/18.83 % (2885294)Peak memory usage: 57 MB % 131.38/18.83 % (2885294)Instructions burned: 14135 (million) % 131.38/18.83 % (2885352)fmb+10_1_sil=256000:fmbss=7:random_seed=386194304:fmbsr=1.6:i=182295_2838 on theBenchmark for (2838ds/182295Mi) % 131.38/18.83 % Exception at run slice level % 131.38/18.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.38/18.83 % (2885354)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=462114353:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 131.38/18.83 % (2885354)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 131.38/18.83 % Exception at run slice level % 131.38/18.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.38/18.83 % (2885356)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4109111155:i=160505_2837 on theBenchmark for (2837ds/160505Mi) % 131.38/18.83 % Exception at run slice level % 131.38/18.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.38/18.83 % (2885358)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=254435975:fmbsr=1.3:i=225729_2837 on theBenchmark for (2837ds/225729Mi) % 166.47/23.71 % Exception at run slice level % 166.47/23.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 166.47/23.71 % (2885360)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3507785996:fmbsr=2:i=185024:ins=7_2836 on theBenchmark for (2836ds/185024Mi) % 166.47/23.71 % Exception at run slice level % 166.47/23.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 166.47/23.71 % (2885362)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=141533753:rtra=on_2836 on theBenchmark for (2836ds/0Mi) % 166.47/23.71 % Exception at run slice level % 166.47/23.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 166.47/23.71 % (2885364)% WARNING: option uhcvi not known. % 166.47/23.71 % (2885364)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4290390195:i=271062:add=off:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/271062Mi) % 166.47/23.71 % (2885288)Instruction limit reached! % 166.47/23.71 % (2885288)------------------------------ % 166.47/23.71 % (2885288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.47/23.71 % (2885288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/23.71 % (2885288)CaDiCaL version: 2.1.3 % 166.47/23.71 % (2885288)Termination reason: Instruction limit % 166.47/23.71 % (2885288)Termination phase: Saturation % 166.47/23.71 % (2885288)Time elapsed: 11.530 s % 166.47/23.71 % (2885288)Peak memory usage: 49 MB % 166.47/23.71 % (2885288)Instructions burned: 20139 (million) % 166.47/23.71 % (2885366)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2342064457:i=176048:add=on:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/176048Mi) % 166.47/23.71 % (2885298)Instruction limit reached! % 166.47/23.71 % (2885298)------------------------------ % 166.47/23.71 % (2885298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.47/23.71 % (2885298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/23.71 % (2885298)CaDiCaL version: 2.1.3 % 166.47/23.71 % (2885298)Termination reason: Instruction limit % 166.47/23.71 % (2885298)Termination phase: Saturation % 166.47/23.71 % (2885298)Time elapsed: 3.922 s % 166.47/23.71 % (2885298)Peak memory usage: 54 MB % 166.47/23.71 % (2885298)Instructions burned: 17628 (million) % 166.47/23.71 % (2885368)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3224876797:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 166.47/23.71 % (2885368)Instruction limit reached! % 166.47/23.71 % (2885368)------------------------------ % 166.47/23.71 % (2885368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.47/23.71 % (2885368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/23.71 % (2885368)CaDiCaL version: 2.1.3 % 166.47/23.71 % (2885368)Termination reason: Instruction limit % 166.47/23.71 % (2885368)Termination phase: Saturation % 166.47/23.71 % (2885368)Time elapsed: 0.068 s % 166.47/23.71 % (2885368)Peak memory usage: 13 MB % 166.47/23.71 % (2885368)Instructions burned: 207 (million) % 166.47/23.71 % (2885370)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=706108136:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 166.47/23.71 % (2885370)Instruction limit reached! % 166.47/23.71 % (2885370)------------------------------ % 166.47/23.71 % (2885370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.47/23.71 % (2885370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/23.71 % (2885370)CaDiCaL version: 2.1.3 % 166.47/23.71 % (2885370)Termination reason: Instruction limit % 166.47/23.71 % (2885370)Termination phase: Saturation % 166.47/23.71 % (2885370)Time elapsed: 0.076 s % 166.47/23.71 % (2885370)Peak memory usage: 13 MB % 166.47/23.71 % (2885370)Instructions burned: 234 (million) % 166.47/23.71 % (2885372)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2482178283:i=262:rtra=on_2827 on theBenchmark for (2827ds/262Mi) % 166.47/23.71 % (2885372)Instruction limit reached! % 166.47/23.71 % (2885372)------------------------------ % 166.47/23.71 % (2885372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.47/23.71 % (2885372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/23.71 % (2885372)CaDiCaL version: 2.1.3 % 166.47/23.71 % (2885372)Termination reason: Instruction limit % 166.47/23.71 % (2885372)Termination phase: Saturation % 236.75/33.61 % (2885372)Time elapsed: 0.086 s % 236.75/33.61 % (2885372)Peak memory usage: 14 MB % 236.75/33.61 % (2885372)Instructions burned: 265 (million) % 236.75/33.61 % (2885374)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=939511338:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2826 on theBenchmark for (2826ds/318Mi) % 236.75/33.61 % (2885374)Instruction limit reached! % 236.75/33.61 % (2885374)------------------------------ % 236.75/33.61 % (2885374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.75/33.61 % (2885374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.75/33.61 % (2885374)CaDiCaL version: 2.1.3 % 236.75/33.61 % (2885374)Termination reason: Instruction limit % 236.75/33.61 % (2885374)Termination phase: Saturation % 236.75/33.61 % (2885374)Time elapsed: 0.188 s % 236.75/33.61 % (2885374)Peak memory usage: 14 MB % 236.75/33.61 % (2885374)Instructions burned: 320 (million) % 236.75/33.61 % (2885376)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1853789489:i=1428:nm=2:rtra=on_2824 on theBenchmark for (2824ds/1428Mi) % 236.75/33.61 % Exception at run slice level % 236.75/33.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.75/33.61 % (2885378)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1814693162:i=262:bd=preordered:rtra=on:fsd=on_2824 on theBenchmark for (2824ds/262Mi) % 236.75/33.61 % (2885378)Instruction limit reached! % 236.75/33.61 % (2885378)------------------------------ % 236.75/33.61 % (2885378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.75/33.61 % (2885378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.75/33.61 % (2885378)CaDiCaL version: 2.1.3 % 236.75/33.61 % (2885378)Termination reason: Instruction limit % 236.75/33.61 % (2885378)Termination phase: Saturation % 236.75/33.61 % (2885378)Time elapsed: 0.094 s % 236.75/33.61 % (2885378)Peak memory usage: 14 MB % 236.75/33.61 % (2885378)Instructions burned: 263 (million) % 236.75/33.61 % (2885380)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=3178240626:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/1368Mi) % 236.75/33.61 % (2885380)Instruction limit reached! % 236.75/33.61 % (2885380)------------------------------ % 236.75/33.61 % (2885380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.75/33.61 % (2885380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.75/33.61 % (2885380)CaDiCaL version: 2.1.3 % 236.75/33.61 % (2885380)Termination reason: Instruction limit % 236.75/33.61 % (2885380)Termination phase: Saturation % 236.75/33.61 % (2885380)Time elapsed: 0.421 s % 236.75/33.61 % (2885380)Peak memory usage: 19 MB % 236.75/33.61 % (2885380)Instructions burned: 1371 (million) % 236.75/33.61 % (2885382)ott-21_1_sil=16000:si=on:fs=off:random_seed=986749753:i=360:av=off:fsr=off:rtra=on_2818 on theBenchmark for (2818ds/360Mi) % 236.75/33.61 % (2885382)Instruction limit reached! % 236.75/33.61 % (2885382)------------------------------ % 236.75/33.61 % (2885382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.75/33.61 % (2885382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.75/33.61 % (2885382)CaDiCaL version: 2.1.3 % 236.75/33.61 % (2885382)Termination reason: Instruction limit % 236.75/33.61 % (2885382)Termination phase: Saturation % 236.75/33.61 % (2885382)Time elapsed: 0.098 s % 236.75/33.61 % (2885382)Peak memory usage: 14 MB % 236.75/33.61 % (2885382)Instructions burned: 363 (million) % 236.75/33.61 % (2885384)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2539259993:i=954:bd=all:rtra=on_2817 on theBenchmark for (2817ds/954Mi) % 236.75/33.61 % (2885384)Instruction limit reached! % 236.75/33.61 % (2885384)------------------------------ % 236.75/33.61 % (2885384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.75/33.61 % (2885384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.75/33.61 % (2885384)CaDiCaL version: 2.1.3 % 236.75/33.61 % (2885384)Termination reason: Instruction limit % 236.75/33.61 % (2885384)Termination phase: Saturation % 236.75/33.61 % (2885384)Time elapsed: 0.330 s % 236.75/33.61 % (2885384)Peak memory usage: 16 MB % 236.75/33.61 % (2885384)Instructions burned: 954 (million) % 236.75/33.61 % (2885386)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1391391131:fmbsr=1.3:i=1730:ins=25:rtra=on_2814 on theBenchmark for (2814ds/1730Mi) % 236.75/33.61 % Exception at run slice level % 236.75/33.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.01/39.29 % (2885388)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=772552925:i=2358:rtra=on_2814 on theBenchmark for (2814ds/2358Mi) % 252.01/39.29 % (2885388)Instruction limit reached! % 252.01/39.29 % (2885388)------------------------------ % 252.01/39.29 % (2885388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/39.29 % (2885388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/39.29 % (2885388)CaDiCaL version: 2.1.3 % 252.01/39.29 % (2885388)Termination reason: Instruction limit % 252.01/39.29 % (2885388)Termination phase: Saturation % 252.01/39.29 % (2885388)Time elapsed: 0.833 s % 252.01/39.29 % (2885388)Peak memory usage: 29 MB % 252.01/39.29 % (2885388)Instructions burned: 2361 (million) % 252.01/39.29 % (2885390)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=892131218:i=1778:ins=1:rtra=on_2805 on theBenchmark for (2805ds/1778Mi) % 252.01/39.29 % Exception at run slice level % 252.01/39.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.01/39.29 % (2885392)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=1678496684:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/1384Mi) % 252.01/39.29 % (2885392)Instruction limit reached! % 252.01/39.29 % (2885392)------------------------------ % 252.01/39.29 % (2885392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/39.29 % (2885392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/39.29 % (2885392)CaDiCaL version: 2.1.3 % 252.01/39.29 % (2885392)Termination reason: Instruction limit % 252.01/39.29 % (2885392)Termination phase: Saturation % 252.01/39.29 % (2885392)Time elapsed: 0.439 s % 252.01/39.29 % (2885392)Peak memory usage: 21 MB % 252.01/39.29 % (2885392)Instructions burned: 1386 (million) % 252.01/39.29 % (2885394)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=296157232:i=1758:kws=inv_precedence:fsr=off:rtra=on_2800 on theBenchmark for (2800ds/1758Mi) % 252.01/39.29 % (2885394)Instruction limit reached! % 252.01/39.29 % (2885394)------------------------------ % 252.01/39.29 % (2885394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/39.29 % (2885394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/39.29 % (2885394)CaDiCaL version: 2.1.3 % 252.01/39.29 % (2885394)Termination reason: Instruction limit % 252.01/39.29 % (2885394)Termination phase: Saturation % 252.01/39.29 % (2885394)Time elapsed: 0.528 s % 252.01/39.29 % (2885394)Peak memory usage: 25 MB % 252.01/39.29 % (2885394)Instructions burned: 1758 (million) % 252.01/39.29 % (2885396)fmb+10_1_sil=64000:si=on:random_seed=1161997364:i=44122:nm=2:rtra=on:gsp=on_2795 on theBenchmark for (2795ds/44122Mi) % 252.01/39.29 % (2885396)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 252.01/39.29 % Exception at run slice level % 252.01/39.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.01/39.29 % (2885398)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1495476560:i=19030:nm=5:rtra=on_2795 on theBenchmark for (2795ds/19030Mi) % 252.01/39.29 % Exception at run slice level % 252.01/39.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.01/39.29 % (2885400)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1052721593:fmbsr=1.7:i=1840:rtra=on_2795 on theBenchmark for (2795ds/1840Mi) % 252.01/39.29 % Exception at run slice level % 252.01/39.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 252.01/39.29 % (2885402)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=601878033:i=10262:rtra=on_2794 on theBenchmark for (2794ds/10262Mi) % 252.01/39.29 % (2885402)Instruction limit reached! % 252.01/39.29 % (2885402)------------------------------ % 252.01/39.29 % (2885402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/39.29 % (2885402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/39.29 % (2885402)CaDiCaL version: 2.1.3 % 252.01/39.29 % (2885402)Termination reason: Instruction limit % 252.01/39.29 % (2885402)Termination phase: Saturation % 252.01/39.29 % (2885402)Time elapsed: 2.936 s % 252.01/39.29 % (2885402)Peak memory usage: 36 MB % 252.01/39.29 % (2885402)Instructions burned: 10263 (million) % 300.65/42.63 % (2885404)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=398848978:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2765 on theBenchmark for (2765ds/2944Mi) % 300.65/42.63 % (2885404)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.65/42.63 % (2885404)Instruction limit reached! % 300.65/42.63 % (2885404)------------------------------ % 300.65/42.63 % (2885404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.63 % (2885404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.63 % (2885404)CaDiCaL version: 2.1.3 % 300.65/42.63 % (2885404)Termination reason: Instruction limit % 300.65/42.63 % (2885404)Termination phase: Saturation % 300.65/42.63 % (2885404)Time elapsed: 1.043 s % 300.65/42.63 % (2885404)Peak memory usage: 64 MB % 300.65/42.63 % (2885404)Instructions burned: 2945 (million) % 300.65/42.63 % (2885406)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3351360795:i=12648:rtra=on_2754 on theBenchmark for (2754ds/12648Mi) % 300.65/42.63 % Exception at run slice level % 300.65/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.65/42.64 % (2885408)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3410925658:fmbsr=2.30978:i=4348:rtra=on_2754 on theBenchmark for (2754ds/4348Mi) % 300.65/42.64 % Exception at run slice level % 300.65/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.65/42.64 % (2885410)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1846733159:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2754 on theBenchmark for (2754ds/1738Mi) % 300.65/42.64 % (2885410)Instruction limit reached! % 300.65/42.64 % (2885410)------------------------------ % 300.65/42.64 % (2885410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.64 % (2885410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.64 % (2885410)CaDiCaL version: 2.1.3 % 300.65/42.64 % (2885410)Termination reason: Instruction limit % 300.65/42.64 % (2885410)Termination phase: Saturation % 300.65/42.64 % (2885410)Time elapsed: 0.565 s % 300.65/42.64 % (2885410)Peak memory usage: 20 MB % 300.65/42.64 % (2885410)Instructions burned: 1741 (million) % 300.65/42.64 % (2885412)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=654082119:i=10228:av=off:rtra=on_2748 on theBenchmark for (2748ds/10228Mi) % 300.65/42.64 % (2885412)Instruction limit reached! % 300.65/42.64 % (2885412)------------------------------ % 300.65/42.64 % (2885412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.64 % (2885412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.64 % (2885412)CaDiCaL version: 2.1.3 % 300.65/42.64 % (2885412)Termination reason: Instruction limit % 300.65/42.64 % (2885412)Termination phase: Saturation % 300.65/42.64 % (2885412)Time elapsed: 3.416 s % 300.65/42.64 % (2885412)Peak memory usage: 49 MB % 300.65/42.64 % (2885412)Instructions burned: 10230 (million) % 300.65/42.64 % (2885416)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=397937320:i=108564:rtra=on_2714 on theBenchmark for (2714ds/108564Mi) % 300.65/42.64 % Exception at run slice level % 300.65/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.65/42.64 % (2885418)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3658640969:i=7024:aac=none:rtra=on_2713 on theBenchmark for (2713ds/7024Mi) % 300.65/42.64 % (2885418)Instruction limit reached! % 300.65/42.64 % (2885418)------------------------------ % 300.65/42.64 % (2885418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.64 % (2885418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.64 % (2885418)CaDiCaL version: 2.1.3 % 300.65/42.64 % (2885418)Termination reason: Instruction limit % 300.65/42.64 % (2885418)Termination phase: Saturation % 300.65/42.64 % (2885418)Time elapsed: 2.326 s % 300.65/42.64 % (2885418)Peak memory usage: 37 MB % 300.65/42.64 % (2885418)Instructions burned: 7026 (million) % 300.65/42.64 % (2885420)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=767146750:i=7546:rtra=on:amm=off_2690 on theBenchmark for (2690ds/7546Mi) % 300.65/42.64 % (2885420)Instruction limit reached! % 300.65/42.64 % (2885420)------------------------------ % 300.65/42.64 % (2885420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.64 % (2885420)Linked with Z3 4.14.0.0 3c47fd96cf % 300.65/42.64 Terminated % 300.65/42.64 % Vampire exiting % 300.65/42.64 Terminated %------------------------------------------------------------------------------