%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW565_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:27 PM UTC 2026 % Result : Timeout 300.59s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW565_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n015.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:22:47 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.35/1.34 % (2658742)Will run a generic schedule for satisfiability detection. % 7.35/1.34 % (2658765)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2245456594:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.35/1.34 % (2658761)% WARNING: option uhcvi not known. % 7.35/1.34 % (2658760)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2285273743_2999 on theBenchmark for (2999ds/0Mi) % 7.35/1.34 % (2658761)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2893617458:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.35/1.34 % (2658763)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=212147022:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.35/1.34 % (2658764)dis+10_1_sil=32000:sp=arity:random_seed=4111934806:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.35/1.34 % (2658766)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3344735956:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.35/1.34 % (2658767)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1299868602:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.35/1.34 % Exception at run slice level % 7.35/1.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.35/1.34 % (2658765)Instruction limit reached! % 7.35/1.34 % (2658765)------------------------------ % 7.35/1.34 % (2658765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2658765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2658765)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2658765)Termination reason: Instruction limit % 7.35/1.34 % (2658765)Termination phase: Saturation % 7.35/1.34 % (2658765)Time elapsed: 0.031 s % 7.35/1.34 % (2658765)Peak memory usage: 12 MB % 7.35/1.34 % (2658765)Instructions burned: 119 (million) % 7.35/1.34 % (2658783)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3895231924:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.35/1.34 % Exception at run slice level % 7.35/1.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.35/1.34 % (2658789)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3199389189:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.35/1.34 % (2658764)Instruction limit reached! % 7.35/1.34 % (2658764)------------------------------ % 7.35/1.34 % (2658764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2658764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2658764)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2658764)Termination reason: Instruction limit % 7.35/1.34 % (2658764)Termination phase: Saturation % 7.35/1.34 % (2658764)Time elapsed: 0.051 s % 7.35/1.34 % (2658764)Peak memory usage: 12 MB % 7.35/1.34 % (2658764)Instructions burned: 103 (million) % 7.35/1.34 % (2658794)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=436372245:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.35/1.34 % (2658766)Instruction limit reached! % 7.35/1.34 % (2658766)------------------------------ % 7.35/1.34 % (2658766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2658766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2658766)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2658766)Termination reason: Instruction limit % 7.35/1.34 % (2658766)Termination phase: Saturation % 7.35/1.34 % (2658766)Time elapsed: 0.069 s % 7.35/1.34 % (2658766)Peak memory usage: 12 MB % 7.35/1.34 % (2658766)Instructions burned: 132 (million) % 7.35/1.34 % (2658798)ott-21_1_sil=16000:fs=off:random_seed=1468935767:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.35/1.34 % (2658789)Instruction limit reached! % 7.35/1.34 % (2658789)------------------------------ % 7.35/1.34 % (2658789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2658789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2658789)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2658789)Termination reason: Instruction limit % 7.35/1.34 % (2658789)Termination phase: Saturation % 7.35/1.34 % (2658789)Time elapsed: 0.035 s % 7.35/1.34 % (2658789)Peak memory usage: 12 MB % 7.35/1.34 % (2658789)Instructions burned: 133 (million) % 7.35/1.34 % (2658804)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2503454766:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.74/3.12 % Exception at run slice level % 19.74/3.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.74/3.12 % (2658767)Instruction limit reached! % 19.74/3.12 % (2658767)------------------------------ % 19.74/3.12 % (2658767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.74/3.12 % (2658767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.74/3.12 % (2658767)CaDiCaL version: 2.1.3 % 19.74/3.12 % (2658767)Termination reason: Instruction limit % 19.74/3.12 % (2658767)Termination phase: Saturation % 19.74/3.12 % (2658767)Time elapsed: 0.085 s % 19.74/3.12 % (2658767)Peak memory usage: 12 MB % 19.74/3.12 % (2658767)Instructions burned: 159 (million) % 19.74/3.12 % (2658802)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3787221774:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.74/3.12 % (2658808)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=446922314:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.74/3.12 % (2658809)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=935901561:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.74/3.12 % Exception at run slice level % 19.74/3.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.74/3.12 % (2658813)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=3353947333: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) % 19.74/3.12 % (2658798)Instruction limit reached! % 19.74/3.12 % (2658798)------------------------------ % 19.74/3.12 % (2658798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.74/3.12 % (2658798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.74/3.12 % (2658798)CaDiCaL version: 2.1.3 % 19.74/3.12 % (2658798)Termination reason: Instruction limit % 19.74/3.12 % (2658798)Termination phase: Saturation % 19.74/3.12 % (2658798)Time elapsed: 0.084 s % 19.74/3.12 % (2658798)Peak memory usage: 12 MB % 19.74/3.12 % (2658798)Instructions burned: 182 (million) % 19.74/3.12 % (2658815)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1285736768:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.74/3.12 % (2658802)Instruction limit reached! % 19.74/3.12 % (2658802)------------------------------ % 19.74/3.12 % (2658802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.74/3.12 % (2658802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.74/3.12 % (2658802)CaDiCaL version: 2.1.3 % 19.74/3.12 % (2658802)Termination reason: Instruction limit % 19.74/3.12 % (2658802)Termination phase: Saturation % 19.74/3.12 % (2658802)Time elapsed: 0.226 s % 19.74/3.12 % (2658802)Peak memory usage: 13 MB % 19.74/3.12 % (2658802)Instructions burned: 479 (million) % 19.74/3.12 % (2658817)fmb+10_1_sil=64000:random_seed=1521334466:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.74/3.12 % (2658817)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.74/3.12 % Exception at run slice level % 19.74/3.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.74/3.12 % (2658819)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4045266440:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.74/3.12 % Exception at run slice level % 19.74/3.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.74/3.12 % (2658808)Instruction limit reached! % 19.74/3.12 % (2658808)------------------------------ % 19.74/3.12 % (2658808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.74/3.12 % (2658808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.74/3.12 % (2658808)CaDiCaL version: 2.1.3 % 19.74/3.12 % (2658808)Termination reason: Instruction limit % 19.74/3.12 % (2658808)Termination phase: Saturation % 19.74/3.12 % (2658808)Time elapsed: 0.280 s % 19.74/3.12 % (2658808)Peak memory usage: 15 MB % 19.74/3.12 % (2658808)Instructions burned: 1183 (million) % 19.74/3.12 % (2658822)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3048411742:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 19.74/3.12 % (2658821)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=277301022:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 63.04/9.16 % (2658794)Instruction limit reached! % 63.04/9.16 % (2658794)------------------------------ % 63.04/9.16 % (2658794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.04/9.16 % (2658794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.04/9.16 % (2658794)CaDiCaL version: 2.1.3 % 63.04/9.16 % (2658794)Termination reason: Instruction limit % 63.04/9.16 % (2658794)Termination phase: Saturation % 63.04/9.16 % (2658794)Time elapsed: 0.336 s % 63.04/9.16 % (2658794)Peak memory usage: 14 MB % 63.04/9.16 % (2658794)Instructions burned: 684 (million) % 63.04/9.16 % Exception at run slice level % 63.04/9.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.04/9.16 % (2658825)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3078963748:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 63.04/9.16 % (2658826)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1584740959:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 63.04/9.16 % (2658825)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 63.04/9.16 % Exception at run slice level % 63.04/9.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.04/9.16 % (2658829)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=991190872:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 63.04/9.16 % Exception at run slice level % 63.04/9.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.04/9.16 % (2658831)ott-2_1_sil=16000:newcnf=on:random_seed=3314945254:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 63.04/9.16 % (2658813)Instruction limit reached! % 63.04/9.16 % (2658813)------------------------------ % 63.04/9.16 % (2658813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.04/9.16 % (2658813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.04/9.16 % (2658813)CaDiCaL version: 2.1.3 % 63.04/9.16 % (2658813)Termination reason: Instruction limit % 63.04/9.16 % (2658813)Termination phase: Saturation % 63.04/9.16 % (2658813)Time elapsed: 0.374 s % 63.04/9.16 % (2658813)Peak memory usage: 20 MB % 63.04/9.16 % (2658813)Instructions burned: 693 (million) % 63.04/9.16 % (2658833)ott+10_1_sil=32000:tgt=ground:random_seed=1154230928:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 63.04/9.16 % (2658815)Instruction limit reached! % 63.04/9.16 % (2658815)------------------------------ % 63.04/9.16 % (2658815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.04/9.16 % (2658815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.04/9.16 % (2658815)CaDiCaL version: 2.1.3 % 63.04/9.16 % (2658815)Termination reason: Instruction limit % 63.04/9.16 % (2658815)Termination phase: Saturation % 63.04/9.16 % (2658815)Time elapsed: 0.479 s % 63.04/9.16 % (2658815)Peak memory usage: 17 MB % 63.04/9.16 % (2658815)Instructions burned: 880 (million) % 63.04/9.16 % (2658835)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2424983934:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 63.04/9.16 % Exception at run slice level % 63.04/9.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 63.04/9.16 % (2658837)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=709830805:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 63.04/9.16 % (2658831)Instruction limit reached! % 63.04/9.16 % (2658831)------------------------------ % 63.04/9.16 % (2658831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.04/9.16 % (2658831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.04/9.16 % (2658831)CaDiCaL version: 2.1.3 % 63.04/9.16 % (2658831)Termination reason: Instruction limit % 63.04/9.16 % (2658831)Termination phase: Saturation % 63.04/9.16 % (2658831)Time elapsed: 0.467 s % 63.04/9.16 % (2658831)Peak memory usage: 17 MB % 63.04/9.16 % (2658831)Instructions burned: 870 (million) % 63.04/9.16 % (2658839)dis+21_1_sil=32000:sas=cadical:random_seed=2703301287:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 63.04/9.16 % (2658825)Instruction limit reached! % 63.04/9.16 % (2658825)------------------------------ % 63.04/9.16 % (2658825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658825)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658825)Termination reason: Instruction limit % 108.98/15.69 % (2658825)Termination phase: Saturation % 108.98/15.69 % (2658825)Time elapsed: 0.644 s % 108.98/15.69 % (2658825)Peak memory usage: 14 MB % 108.98/15.69 % (2658825)Instructions burned: 1474 (million) % 108.98/15.69 % (2658841)ott+11_1_sil=16000:gs=on:random_seed=2468375459:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 108.98/15.69 % (2658822)Instruction limit reached! % 108.98/15.69 % (2658822)------------------------------ % 108.98/15.69 % (2658822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658822)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658822)Termination reason: Instruction limit % 108.98/15.69 % (2658822)Termination phase: Saturation % 108.98/15.69 % (2658822)Time elapsed: 1.326 s % 108.98/15.69 % (2658822)Peak memory usage: 27 MB % 108.98/15.69 % (2658822)Instructions burned: 5131 (million) % 108.98/15.69 % (2658843)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=193023472:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 108.98/15.69 % Exception at run slice level % 108.98/15.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 108.98/15.69 % (2658845)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2539408100:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 108.98/15.69 % (2658841)Instruction limit reached! % 108.98/15.69 % (2658841)------------------------------ % 108.98/15.69 % (2658841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658841)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658841)Termination reason: Instruction limit % 108.98/15.69 % (2658841)Termination phase: Saturation % 108.98/15.69 % (2658841)Time elapsed: 1.144 s % 108.98/15.69 % (2658841)Peak memory usage: 22 MB % 108.98/15.69 % (2658841)Instructions burned: 2254 (million) % 108.98/15.69 % (2658847)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=614888243:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 108.98/15.69 % (2658837)Instruction limit reached! % 108.98/15.69 % (2658837)------------------------------ % 108.98/15.69 % (2658837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658837)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658837)Termination reason: Instruction limit % 108.98/15.69 % (2658837)Termination phase: Saturation % 108.98/15.69 % (2658837)Time elapsed: 1.740 s % 108.98/15.69 % (2658837)Peak memory usage: 23 MB % 108.98/15.69 % (2658837)Instructions burned: 3513 (million) % 108.98/15.69 % (2658849)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=433778102:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 108.98/15.69 % (2658839)Instruction limit reached! % 108.98/15.69 % (2658839)------------------------------ % 108.98/15.69 % (2658839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658839)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658839)Termination reason: Instruction limit % 108.98/15.69 % (2658839)Termination phase: Saturation % 108.98/15.69 % (2658839)Time elapsed: 1.827 s % 108.98/15.69 % (2658839)Peak memory usage: 22 MB % 108.98/15.69 % (2658839)Instructions burned: 3774 (million) % 108.98/15.69 % (2658851)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3713928551:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 108.98/15.69 % Exception at run slice level % 108.98/15.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 108.98/15.69 % (2658833)Instruction limit reached! % 108.98/15.69 % (2658833)------------------------------ % 108.98/15.69 % (2658833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.98/15.69 % (2658833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.98/15.69 % (2658833)CaDiCaL version: 2.1.3 % 108.98/15.69 % (2658833)Termination reason: Instruction limit % 108.98/15.69 % (2658833)Termination phase: Saturation % 108.98/15.69 % (2658833)Time elapsed: 2.303 s % 133.30/19.05 % (2658833)Peak memory usage: 21 MB % 133.30/19.05 % (2658833)Instructions burned: 5116 (million) % 133.30/19.05 % (2658853)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4033861850:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 133.30/19.05 % Exception at run slice level % 133.30/19.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.30/19.05 % (2658855)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3507990167:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 133.30/19.05 % (2658856)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1730044043:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 133.30/19.05 % Exception at run slice level % 133.30/19.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.30/19.05 % (2658859)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4226580185:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi) % 133.30/19.05 % (2658845)Instruction limit reached! % 133.30/19.05 % (2658845)------------------------------ % 133.30/19.05 % (2658845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.05 % (2658845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.05 % (2658845)CaDiCaL version: 2.1.3 % 133.30/19.05 % (2658845)Termination reason: Instruction limit % 133.30/19.05 % (2658845)Termination phase: Saturation % 133.30/19.05 % (2658845)Time elapsed: 1.207 s % 133.30/19.05 % (2658845)Peak memory usage: 25 MB % 133.30/19.05 % (2658845)Instructions burned: 4593 (million) % 133.30/19.05 % (2658861)dis+10_16:1_sil=16000:random_seed=748562290:i=9155:fsr=off_2969 on theBenchmark for (2969ds/9155Mi) % 133.30/19.05 % (2658849)Instruction limit reached! % 133.30/19.05 % (2658849)------------------------------ % 133.30/19.05 % (2658849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.05 % (2658849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.05 % (2658849)CaDiCaL version: 2.1.3 % 133.30/19.05 % (2658849)Termination reason: Instruction limit % 133.30/19.05 % (2658849)Termination phase: Saturation % 133.30/19.05 % (2658849)Time elapsed: 2.516 s % 133.30/19.05 % (2658849)Peak memory usage: 37 MB % 133.30/19.05 % (2658849)Instructions burned: 5212 (million) % 133.30/19.05 % (2658863)ott-3_8_sil=64000:random_seed=3081612774:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 133.30/19.05 % (2658861)Instruction limit reached! % 133.30/19.05 % (2658861)------------------------------ % 133.30/19.05 % (2658861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.05 % (2658861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.05 % (2658861)CaDiCaL version: 2.1.3 % 133.30/19.05 % (2658861)Termination reason: Instruction limit % 133.30/19.05 % (2658861)Termination phase: Saturation % 133.30/19.05 % (2658861)Time elapsed: 2.395 s % 133.30/19.05 % (2658861)Peak memory usage: 36 MB % 133.30/19.05 % (2658861)Instructions burned: 9159 (million) % 133.30/19.05 % (2658865)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=881541727:fmbsr=2:i=32576_2945 on theBenchmark for (2945ds/32576Mi) % 133.30/19.05 % Exception at run slice level % 133.30/19.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.30/19.05 % (2658867)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2730200319:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 133.30/19.05 % (2658859)Instruction limit reached! % 133.30/19.05 % (2658859)------------------------------ % 133.30/19.05 % (2658859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.05 % (2658859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.05 % (2658859)CaDiCaL version: 2.1.3 % 133.30/19.05 % (2658859)Termination reason: Instruction limit % 133.30/19.05 % (2658859)Termination phase: Saturation % 133.30/19.05 % (2658859)Time elapsed: 3.862 s % 133.30/19.05 % (2658859)Peak memory usage: 28 MB % 133.30/19.05 % (2658859)Instructions burned: 8173 (million) % 133.30/19.05 % (2658869)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3279736006:i=14134_2932 on theBenchmark for (2932ds/14134Mi) % 133.30/19.05 % (2658867)Instruction limit reached! % 133.30/19.05 % (2658867)------------------------------ % 133.30/19.05 % (2658867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.05 % (2658867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.05 % (2658867)CaDiCaL version: 2.1.3 % 141.38/20.26 % (2658867)Termination reason: Instruction limit % 141.38/20.26 % (2658867)Termination phase: Saturation % 141.38/20.26 % (2658867)Time elapsed: 3.492 s % 141.38/20.26 % (2658867)Peak memory usage: 76 MB % 141.38/20.26 % (2658867)Instructions burned: 11404 (million) % 141.38/20.26 % (2658871)dis+33_16_sil=32000:sac=on:random_seed=4042048687:i=15851:nm=0_2910 on theBenchmark for (2910ds/15851Mi) % 141.38/20.26 % (2658863)Instruction limit reached! % 141.38/20.26 % (2658863)------------------------------ % 141.38/20.26 % (2658863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.38/20.26 % (2658863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.38/20.26 % (2658863)CaDiCaL version: 2.1.3 % 141.38/20.26 % (2658863)Termination reason: Instruction limit % 141.38/20.26 % (2658863)Termination phase: Saturation % 141.38/20.26 % (2658863)Time elapsed: 5.993 s % 141.38/20.26 % (2658863)Peak memory usage: 13 MB % 141.38/20.26 % (2658863)Instructions burned: 20139 (million) % 141.38/20.26 % (2658873)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1166746176:avsq=on:i=17627:add=on:amm=off_2889 on theBenchmark for (2889ds/17627Mi) % 141.38/20.26 % (2658869)Instruction limit reached! % 141.38/20.26 % (2658869)------------------------------ % 141.38/20.26 % (2658869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.38/20.26 % (2658869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.38/20.26 % (2658869)CaDiCaL version: 2.1.3 % 141.38/20.26 % (2658869)Termination reason: Instruction limit % 141.38/20.26 % (2658869)Termination phase: Saturation % 141.38/20.26 % (2658869)Time elapsed: 4.320 s % 141.38/20.26 % (2658869)Peak memory usage: 15 MB % 141.38/20.26 % (2658869)Instructions burned: 14136 (million) % 141.38/20.26 % (2658875)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2502886347:s2a=on:i=53295_2888 on theBenchmark for (2888ds/53295Mi) % 141.38/20.26 % (2658871)Instruction limit reached! % 141.38/20.26 % (2658871)------------------------------ % 141.38/20.26 % (2658871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.38/20.26 % (2658871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.38/20.26 % (2658871)CaDiCaL version: 2.1.3 % 141.38/20.26 % (2658871)Termination reason: Instruction limit % 141.38/20.26 % (2658871)Termination phase: Saturation % 141.38/20.26 % (2658871)Time elapsed: 3.664 s % 141.38/20.26 % (2658871)Peak memory usage: 24 MB % 141.38/20.26 % (2658871)Instructions burned: 15853 (million) % 141.38/20.26 % (2658877)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=940395037:i=26857:ins=20_2873 on theBenchmark for (2873ds/26857Mi) % 141.38/20.26 % Exception at run slice level % 141.38/20.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.38/20.26 % (2658879)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1435263789:i=28120:bs=on:fsr=off_2873 on theBenchmark for (2873ds/28120Mi) % 141.38/20.26 % (2658847)Instruction limit reached! % 141.38/20.26 % (2658847)------------------------------ % 141.38/20.26 % (2658847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.38/20.26 % (2658847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.38/20.26 % (2658847)CaDiCaL version: 2.1.3 % 141.38/20.26 % (2658847)Termination reason: Instruction limit % 141.38/20.26 % (2658847)Termination phase: Saturation % 141.38/20.26 % (2658847)Time elapsed: 13.058 s % 141.38/20.26 % (2658847)Peak memory usage: 55 MB % 141.38/20.26 % (2658847)Instructions burned: 29341 (million) % 141.38/20.26 % (2659143)fmb+10_1_sil=256000:fmbss=7:random_seed=1425424985:fmbsr=1.6:i=182295_2846 on theBenchmark for (2846ds/182295Mi) % 141.38/20.26 % Exception at run slice level % 141.38/20.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.38/20.26 % (2659145)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=725802006:i=44625:gsp=on_2846 on theBenchmark for (2846ds/44625Mi) % 141.38/20.26 % (2659145)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 141.38/20.26 % Exception at run slice level % 141.38/20.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.38/20.26 % (2659147)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1094520150:i=160505_2845 on theBenchmark for (2845ds/160505Mi) % 141.38/20.26 % Exception at run slice level % 141.38/20.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.38/20.26 % (2659149)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3032042827:fmbsr=1.3:i=225729_2845 on theBenchmark for (2845ds/225729Mi) % 157.20/22.40 % Exception at run slice level % 157.20/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 157.20/22.40 % (2659151)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1911993229:fmbsr=2:i=185024:ins=7_2845 on theBenchmark for (2845ds/185024Mi) % 157.20/22.40 % Exception at run slice level % 157.20/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 157.20/22.40 % (2659153)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1892032054:rtra=on_2845 on theBenchmark for (2845ds/0Mi) % 157.20/22.40 % Exception at run slice level % 157.20/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 157.20/22.40 % (2659155)% WARNING: option uhcvi not known. % 157.20/22.40 % (2659155)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3084227470:i=271062:add=off:rtra=on:rawr=on_2844 on theBenchmark for (2844ds/271062Mi) % 157.20/22.40 % (2658879)Instruction limit reached! % 157.20/22.40 % (2658879)------------------------------ % 157.20/22.40 % (2658879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.20/22.40 % (2658879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.20/22.40 % (2658879)CaDiCaL version: 2.1.3 % 157.20/22.40 % (2658879)Termination reason: Instruction limit % 157.20/22.40 % (2658879)Termination phase: Saturation % 157.20/22.40 % (2658879)Time elapsed: 5.454 s % 157.20/22.40 % (2658879)Peak memory usage: 21 MB % 157.20/22.40 % (2658879)Instructions burned: 28125 (million) % 157.20/22.40 % (2659329)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3353933626:i=176048:add=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/176048Mi) % 157.20/22.40 % (2658856)Instruction limit reached! % 157.20/22.40 % (2658856)------------------------------ % 157.20/22.40 % (2658856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.20/22.40 % (2658856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.20/22.40 % (2658856)CaDiCaL version: 2.1.3 % 157.20/22.40 % (2658856)Termination reason: Instruction limit % 157.20/22.40 % (2658856)Termination phase: Saturation % 157.20/22.40 % (2658856)Time elapsed: 15.456 s % 157.20/22.40 % (2658856)Peak memory usage: 197 MB % 157.20/22.40 % (2658856)Instructions burned: 22565 (million) % 157.20/22.40 % (2659331)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3605605119:i=206:fgj=on:rtra=on_2816 on theBenchmark for (2816ds/206Mi) % 157.20/22.40 % (2659331)Instruction limit reached! % 157.20/22.40 % (2659331)------------------------------ % 157.20/22.40 % (2659331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.20/22.40 % (2659331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.20/22.40 % (2659331)CaDiCaL version: 2.1.3 % 157.20/22.40 % (2659331)Termination reason: Instruction limit % 157.20/22.40 % (2659331)Termination phase: Saturation % 157.20/22.40 % (2659331)Time elapsed: 0.108 s % 157.20/22.40 % (2659331)Peak memory usage: 12 MB % 157.20/22.40 % (2659331)Instructions burned: 207 (million) % 157.20/22.40 % (2659333)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1679525822:i=232:rtra=on_2814 on theBenchmark for (2814ds/232Mi) % 157.20/22.40 % (2659333)Instruction limit reached! % 157.20/22.40 % (2659333)------------------------------ % 157.20/22.40 % (2659333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.20/22.40 % (2659333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.20/22.40 % (2659333)CaDiCaL version: 2.1.3 % 157.20/22.40 % (2659333)Termination reason: Instruction limit % 157.20/22.40 % (2659333)Termination phase: Saturation % 157.20/22.40 % (2659333)Time elapsed: 0.110 s % 157.20/22.40 % (2659333)Peak memory usage: 12 MB % 157.20/22.40 % (2659333)Instructions burned: 232 (million) % 157.20/22.40 % (2659335)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2449782380:i=262:rtra=on_2813 on theBenchmark for (2813ds/262Mi) % 157.20/22.40 % (2659335)Instruction limit reached! % 157.20/22.40 % (2659335)------------------------------ % 157.20/22.40 % (2659335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.20/22.40 % (2659335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.20/22.40 % (2659335)CaDiCaL version: 2.1.3 % 157.20/22.40 % (2659335)Termination reason: Instruction limit % 157.20/22.40 % (2659335)Termination phase: Saturation % 220.37/31.39 % (2659335)Time elapsed: 0.145 s % 220.37/31.39 % (2659335)Peak memory usage: 13 MB % 220.37/31.39 % (2659335)Instructions burned: 263 (million) % 220.37/31.39 % (2659337)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4200603414:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2811 on theBenchmark for (2811ds/318Mi) % 220.37/31.39 % (2659337)Instruction limit reached! % 220.37/31.39 % (2659337)------------------------------ % 220.37/31.39 % (2659337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.39 % (2659337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.39 % (2659337)CaDiCaL version: 2.1.3 % 220.37/31.39 % (2659337)Termination reason: Instruction limit % 220.37/31.39 % (2659337)Termination phase: Saturation % 220.37/31.39 % (2659337)Time elapsed: 0.157 s % 220.37/31.39 % (2659337)Peak memory usage: 13 MB % 220.37/31.39 % (2659337)Instructions burned: 319 (million) % 220.37/31.39 % (2659339)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1015522363:i=1428:nm=2:rtra=on_2810 on theBenchmark for (2810ds/1428Mi) % 220.37/31.39 % Exception at run slice level % 220.37/31.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 220.37/31.39 % (2659341)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1805290798:i=262:bd=preordered:rtra=on:fsd=on_2809 on theBenchmark for (2809ds/262Mi) % 220.37/31.39 % (2659341)Instruction limit reached! % 220.37/31.39 % (2659341)------------------------------ % 220.37/31.39 % (2659341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.39 % (2659341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.39 % (2659341)CaDiCaL version: 2.1.3 % 220.37/31.39 % (2659341)Termination reason: Instruction limit % 220.37/31.39 % (2659341)Termination phase: Saturation % 220.37/31.39 % (2659341)Time elapsed: 0.128 s % 220.37/31.39 % (2659341)Peak memory usage: 13 MB % 220.37/31.39 % (2659341)Instructions burned: 262 (million) % 220.37/31.39 % (2659343)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=749731058:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1368Mi) % 220.37/31.39 % (2658873)Instruction limit reached! % 220.37/31.39 % (2658873)------------------------------ % 220.37/31.39 % (2658873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.39 % (2658873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.39 % (2658873)CaDiCaL version: 2.1.3 % 220.37/31.39 % (2658873)Termination reason: Instruction limit % 220.37/31.39 % (2658873)Termination phase: Saturation % 220.37/31.39 % (2658873)Time elapsed: 8.728 s % 220.37/31.39 % (2658873)Peak memory usage: 39 MB % 220.37/31.39 % (2658873)Instructions burned: 17628 (million) % 220.37/31.39 % (2659345)ott-21_1_sil=16000:si=on:fs=off:random_seed=2309201862:i=360:av=off:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/360Mi) % 220.37/31.39 % (2659343)Instruction limit reached! % 220.37/31.39 % (2659343)------------------------------ % 220.37/31.39 % (2659343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.39 % (2659343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.39 % (2659343)CaDiCaL version: 2.1.3 % 220.37/31.39 % (2659343)Termination reason: Instruction limit % 220.37/31.39 % (2659343)Termination phase: Saturation % 220.37/31.39 % (2659343)Time elapsed: 0.710 s % 220.37/31.39 % (2659343)Peak memory usage: 16 MB % 220.37/31.39 % (2659343)Instructions burned: 1370 (million) % 220.37/31.39 % (2659347)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2966202671:i=954:bd=all:rtra=on_2800 on theBenchmark for (2800ds/954Mi) % 220.37/31.39 % (2659345)Instruction limit reached! % 220.37/31.39 % (2659345)------------------------------ % 220.37/31.39 % (2659345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.39 % (2659345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.39 % (2659345)CaDiCaL version: 2.1.3 % 220.37/31.39 % (2659345)Termination reason: Instruction limit % 220.37/31.39 % (2659345)Termination phase: Saturation % 220.37/31.39 % (2659345)Time elapsed: 0.175 s % 220.37/31.39 % (2659345)Peak memory usage: 13 MB % 220.37/31.39 % (2659345)Instructions burned: 361 (million) % 220.37/31.39 % (2659349)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4023333036:fmbsr=1.3:i=1730:ins=25:rtra=on_2800 on theBenchmark for (2800ds/1730Mi) % 220.37/31.39 % Exception at run slice level % 220.37/31.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 275.30/39.07 % (2659351)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=164760237:i=2358:rtra=on_2799 on theBenchmark for (2799ds/2358Mi) % 275.30/39.07 % (2659347)Instruction limit reached! % 275.30/39.07 % (2659347)------------------------------ % 275.30/39.07 % (2659347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.30/39.07 % (2659347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.30/39.07 % (2659347)CaDiCaL version: 2.1.3 % 275.30/39.07 % (2659347)Termination reason: Instruction limit % 275.30/39.07 % (2659347)Termination phase: Saturation % 275.30/39.07 % (2659347)Time elapsed: 0.473 s % 275.30/39.07 % (2659347)Peak memory usage: 14 MB % 275.30/39.07 % (2659347)Instructions burned: 956 (million) % 275.30/39.07 % (2659353)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2893750023:i=1778:ins=1:rtra=on_2795 on theBenchmark for (2795ds/1778Mi) % 275.30/39.07 % Exception at run slice level % 275.30/39.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 275.30/39.07 % (2659355)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=2136654892:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2795 on theBenchmark for (2795ds/1384Mi) % 275.30/39.07 % (2659355)Instruction limit reached! % 275.30/39.07 % (2659355)------------------------------ % 275.30/39.07 % (2659355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.30/39.07 % (2659355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.30/39.07 % (2659355)CaDiCaL version: 2.1.3 % 275.30/39.07 % (2659355)Termination reason: Instruction limit % 275.30/39.07 % (2659355)Termination phase: Saturation % 275.30/39.07 % (2659355)Time elapsed: 0.703 s % 275.30/39.07 % (2659355)Peak memory usage: 20 MB % 275.30/39.07 % (2659355)Instructions burned: 1385 (million) % 275.30/39.07 % (2659357)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2493840939:i=1758:kws=inv_precedence:fsr=off:rtra=on_2788 on theBenchmark for (2788ds/1758Mi) % 275.30/39.07 % (2659351)Instruction limit reached! % 275.30/39.07 % (2659351)------------------------------ % 275.30/39.07 % (2659351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.30/39.07 % (2659351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.30/39.07 % (2659351)CaDiCaL version: 2.1.3 % 275.30/39.07 % (2659351)Termination reason: Instruction limit % 275.30/39.07 % (2659351)Termination phase: Saturation % 275.30/39.07 % (2659351)Time elapsed: 1.178 s % 275.30/39.07 % (2659351)Peak memory usage: 17 MB % 275.30/39.07 % (2659351)Instructions burned: 2359 (million) % 275.30/39.07 % (2659359)fmb+10_1_sil=64000:si=on:random_seed=2445964806:i=44122:nm=2:rtra=on:gsp=on_2787 on theBenchmark for (2787ds/44122Mi) % 275.30/39.07 % (2659359)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 275.30/39.07 % Exception at run slice level % 275.30/39.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 275.30/39.07 % (2659361)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1833820512:i=19030:nm=5:rtra=on_2787 on theBenchmark for (2787ds/19030Mi) % 275.30/39.07 % Exception at run slice level % 275.30/39.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 275.30/39.07 % (2659363)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3808445712:fmbsr=1.7:i=1840:rtra=on_2787 on theBenchmark for (2787ds/1840Mi) % 275.30/39.07 % Exception at run slice level % 275.30/39.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 275.30/39.07 % (2659365)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=715647870:i=10262:rtra=on_2786 on theBenchmark for (2786ds/10262Mi) % 275.30/39.07 % (2659357)Instruction limit reached! % 275.30/39.07 % (2659357)------------------------------ % 275.30/39.07 % (2659357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.30/39.07 % (2659357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.30/39.07 % (2659357)CaDiCaL version: 2.1.3 % 275.30/39.07 % (2659357)Termination reason: Instruction limit % 275.30/39.07 % (2659357)Termination phase: Saturation % 275.30/39.07 % (2659357)Time elapsed: 1.002 s % 275.30/39.07 % (2659357)Peak memory usage: 23 MB % 275.30/39.07 % (2659357)Instructions burned: 1759 (million) % 300.59/42.63 % (2659367)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3003976955:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2778 on theBenchmark for (2778ds/2944Mi) % 300.59/42.63 % (2659367)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.59/42.63 % (2659367)Instruction limit reached! % 300.59/42.63 % (2659367)------------------------------ % 300.59/42.63 % (2659367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (2659367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (2659367)CaDiCaL version: 2.1.3 % 300.59/42.63 % (2659367)Termination reason: Instruction limit % 300.59/42.63 % (2659367)Termination phase: Saturation % 300.59/42.63 % (2659367)Time elapsed: 1.292 s % 300.59/42.63 % (2659367)Peak memory usage: 15 MB % 300.59/42.63 % (2659367)Instructions burned: 2946 (million) % 300.59/42.63 % (2659369)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4227190984:i=12648:rtra=on_2765 on theBenchmark for (2765ds/12648Mi) % 300.59/42.63 % Exception at run slice level % 300.59/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.59/42.63 % (2659371)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1977983892:fmbsr=2.30978:i=4348:rtra=on_2764 on theBenchmark for (2764ds/4348Mi) % 300.59/42.63 % Exception at run slice level % 300.59/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.59/42.63 % (2659373)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3733519017:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2764 on theBenchmark for (2764ds/1738Mi) % 300.59/42.63 % (2659373)Instruction limit reached! % 300.59/42.63 % (2659373)------------------------------ % 300.59/42.63 % (2659373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (2659373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (2659373)CaDiCaL version: 2.1.3 % 300.59/42.63 % (2659373)Termination reason: Instruction limit % 300.59/42.63 % (2659373)Termination phase: Saturation % 300.59/42.63 % (2659373)Time elapsed: 0.925 s % 300.59/42.63 % (2659373)Peak memory usage: 15 MB % 300.59/42.63 % (2659373)Instructions burned: 1739 (million) % 300.59/42.63 % (2659375)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3475832776:i=10228:av=off:rtra=on_2755 on theBenchmark for (2755ds/10228Mi) % 300.59/42.63 % (2659365)Instruction limit reached! % 300.59/42.63 % (2659365)------------------------------ % 300.59/42.63 % (2659365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (2659365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (2659365)CaDiCaL version: 2.1.3 % 300.59/42.63 % (2659365)Termination reason: Instruction limit % 300.59/42.63 % (2659365)Termination phase: Saturation % 300.59/42.63 % (2659365)Time elapsed: 5.893 s % 300.59/42.63 % (2659365)Peak memory usage: 32 MB % 300.59/42.63 % (2659365)Instructions burned: 10263 (million) % 300.59/42.63 % (2659377)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=745467709:i=108564:rtra=on_2727 on theBenchmark for (2727ds/108564Mi) % 300.59/42.63 % Exception at run slice level % 300.59/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.59/42.63 % (2659379)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=229104387:i=7024:aac=none:rtra=on_2727 on theBenchmark for (2727ds/7024Mi) % 300.59/42.63 % (2659375)Instruction limit reached! % 300.59/42.63 % (2659375)------------------------------ % 300.59/42.63 % (2659375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (2659375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (2659375)CaDiCaL version: 2.1.3 % 300.59/42.63 % (2659375)Termination reason: Instruction limit % 300.59/42.63 % (2659375)Termination phase: Saturation % 300.59/42.63 % (2659375)Time elapsed: 4.873 s % 300.59/42.63 % (2659375)Peak memory usage: 24 MB % 300.59/42.63 % (2659375)Instructions burned: 10230 (million) % 300.59/42.63 % (2659655)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3266919377:i=7546:rtra=on:amm=off_2706 on theBenchmark for (2706ds/7546Mi) % 300.59/42.63 % (2659379)Instruction limit reached! % 300.59/42.63 % (2659379)------------------------------ % 300.59/42.63 % (2659379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (2659379)Linked with Z3 4.14.0 % 300.59/42.64 Terminated % 300.59/42.64 % Vampire exiting % 300.59/42.64 Terminated %------------------------------------------------------------------------------