%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW475_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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:13 PM UTC 2026 % Result : Timeout 300.43s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW475_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.17 % Computer : n003.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 14:11:27 UTC 2026 % 0.06/0.17 % CPUTime : % 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.20 Running first-order model finding % 0.06/0.20 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.29/1.34 % (1606607)Will run a generic schedule for satisfiability detection. % 7.29/1.34 % (1606616)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2629016064:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.29/1.34 % (1606613)% WARNING: option uhcvi not known. % 7.29/1.34 % (1606612)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1778845710_2999 on theBenchmark for (2999ds/0Mi) % 7.29/1.34 % (1606613)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1978155901:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.29/1.34 % (1606614)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3215003284:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.29/1.34 % (1606615)dis+10_1_sil=32000:sp=arity:random_seed=2850126470:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.29/1.34 % (1606618)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3992549786:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.29/1.34 % (1606617)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1496950600:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.29/1.34 % Exception at run slice level % 7.29/1.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.29/1.34 % (1606616)Instruction limit reached! % 7.29/1.34 % (1606616)------------------------------ % 7.29/1.34 % (1606616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.29/1.34 % (1606616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.34 % (1606616)CaDiCaL version: 2.1.3 % 7.29/1.34 % (1606616)Termination reason: Instruction limit % 7.29/1.34 % (1606616)Termination phase: Saturation % 7.29/1.34 % (1606616)Time elapsed: 0.030 s % 7.29/1.34 % (1606616)Peak memory usage: 12 MB % 7.29/1.34 % (1606616)Instructions burned: 120 (million) % 7.29/1.34 % (1606626)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3661687971:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.29/1.34 % (1606627)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3289237846:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.29/1.34 % Exception at run slice level % 7.29/1.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.29/1.34 % (1606615)Instruction limit reached! % 7.29/1.34 % (1606615)------------------------------ % 7.29/1.34 % (1606615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.29/1.34 % (1606615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.34 % (1606615)CaDiCaL version: 2.1.3 % 7.29/1.34 % (1606615)Termination reason: Instruction limit % 7.29/1.34 % (1606615)Termination phase: Saturation % 7.29/1.34 % (1606615)Time elapsed: 0.050 s % 7.29/1.34 % (1606615)Peak memory usage: 12 MB % 7.29/1.34 % (1606615)Instructions burned: 104 (million) % 7.29/1.34 % (1606630)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=1122209469:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.29/1.34 % (1606617)Instruction limit reached! % 7.29/1.34 % (1606617)------------------------------ % 7.29/1.34 % (1606617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.29/1.34 % (1606617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.34 % (1606617)CaDiCaL version: 2.1.3 % 7.29/1.34 % (1606617)Termination reason: Instruction limit % 7.29/1.34 % (1606617)Termination phase: Saturation % 7.29/1.34 % (1606617)Time elapsed: 0.060 s % 7.29/1.34 % (1606617)Peak memory usage: 12 MB % 7.29/1.34 % (1606617)Instructions burned: 133 (million) % 7.29/1.34 % (1606631)ott-21_1_sil=16000:fs=off:random_seed=1924137344:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.29/1.34 % (1606627)Instruction limit reached! % 7.29/1.34 % (1606627)------------------------------ % 7.29/1.34 % (1606627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.29/1.34 % (1606627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.34 % (1606627)CaDiCaL version: 2.1.3 % 7.29/1.34 % (1606627)Termination reason: Instruction limit % 7.29/1.34 % (1606627)Termination phase: Saturation % 7.29/1.34 % (1606627)Time elapsed: 0.035 s % 7.29/1.34 % (1606627)Peak memory usage: 12 MB % 7.29/1.34 % (1606627)Instructions burned: 132 (million) % 7.29/1.34 % (1606618)Instruction limit reached! % 17.09/2.78 % (1606618)------------------------------ % 17.09/2.78 % (1606618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.09/2.78 % (1606618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/2.78 % (1606618)CaDiCaL version: 2.1.3 % 17.09/2.78 % (1606618)Termination reason: Instruction limit % 17.09/2.78 % (1606618)Termination phase: Saturation % 17.09/2.78 % (1606618)Time elapsed: 0.071 s % 17.09/2.78 % (1606618)Peak memory usage: 12 MB % 17.09/2.78 % (1606618)Instructions burned: 161 (million) % 17.09/2.78 % (1606633)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4209603641:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 17.09/2.78 % (1606635)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2400610176:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 17.09/2.78 % Exception at run slice level % 17.09/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 17.09/2.78 % (1606636)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=805617767:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 17.09/2.78 % (1606639)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3094065384:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 17.09/2.78 % Exception at run slice level % 17.09/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 17.09/2.78 % (1606642)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=1811004277: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) % 17.09/2.78 % (1606631)Instruction limit reached! % 17.09/2.78 % (1606631)------------------------------ % 17.09/2.78 % (1606631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.09/2.78 % (1606631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/2.78 % (1606631)CaDiCaL version: 2.1.3 % 17.09/2.78 % (1606631)Termination reason: Instruction limit % 17.09/2.78 % (1606631)Termination phase: Saturation % 17.09/2.78 % (1606631)Time elapsed: 0.083 s % 17.09/2.78 % (1606631)Peak memory usage: 12 MB % 17.09/2.78 % (1606631)Instructions burned: 180 (million) % 17.09/2.78 % (1606644)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4057542642:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.09/2.78 % (1606642)Instruction limit reached! % 17.09/2.78 % (1606642)------------------------------ % 17.09/2.78 % (1606642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.09/2.78 % (1606642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/2.78 % (1606642)CaDiCaL version: 2.1.3 % 17.09/2.78 % (1606642)Termination reason: Instruction limit % 17.09/2.78 % (1606642)Termination phase: Saturation % 17.09/2.78 % (1606642)Time elapsed: 0.202 s % 17.09/2.78 % (1606642)Peak memory usage: 16 MB % 17.09/2.78 % (1606642)Instructions burned: 695 (million) % 17.09/2.78 % (1606633)Instruction limit reached! % 17.09/2.78 % (1606633)------------------------------ % 17.09/2.78 % (1606633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.09/2.78 % (1606633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/2.78 % (1606633)CaDiCaL version: 2.1.3 % 17.09/2.78 % (1606633)Termination reason: Instruction limit % 17.09/2.78 % (1606633)Termination phase: Saturation % 17.09/2.78 % (1606633)Time elapsed: 0.238 s % 17.09/2.78 % (1606633)Peak memory usage: 14 MB % 17.09/2.78 % (1606633)Instructions burned: 478 (million) % 17.09/2.78 % (1606646)fmb+10_1_sil=64000:random_seed=3694418759:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 17.09/2.78 % (1606646)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.09/2.78 % Exception at run slice level % 17.09/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 17.09/2.78 % (1606649)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1900176317:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 17.09/2.78 % (1606647)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=841364918:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 17.09/2.78 % Exception at run slice level % 17.09/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 17.09/2.78 % Exception at run slice level % 60.08/8.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.08/8.71 % (1606652)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2175312395:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 60.08/8.71 % (1606630)Instruction limit reached! % 60.08/8.71 % (1606630)------------------------------ % 60.08/8.71 % (1606630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.08/8.71 % (1606630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.08/8.71 % (1606630)CaDiCaL version: 2.1.3 % 60.08/8.71 % (1606630)Termination reason: Instruction limit % 60.08/8.71 % (1606630)Termination phase: Saturation % 60.08/8.71 % (1606630)Time elapsed: 0.303 s % 60.08/8.71 % (1606630)Peak memory usage: 14 MB % 60.08/8.71 % (1606630)Instructions burned: 687 (million) % 60.08/8.71 % (1606653)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2238035811:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 60.08/8.71 % (1606653)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.08/8.71 % (1606655)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1458648747:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 60.08/8.71 % Exception at run slice level % 60.08/8.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.08/8.71 % (1606658)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=659948720:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 60.08/8.71 % Exception at run slice level % 60.08/8.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.08/8.71 % (1606660)ott-2_1_sil=16000:newcnf=on:random_seed=434267547:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 60.08/8.71 % (1606636)Instruction limit reached! % 60.08/8.71 % (1606636)------------------------------ % 60.08/8.71 % (1606636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.08/8.71 % (1606636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.08/8.71 % (1606636)CaDiCaL version: 2.1.3 % 60.08/8.71 % (1606636)Termination reason: Instruction limit % 60.08/8.71 % (1606636)Termination phase: Saturation % 60.08/8.71 % (1606636)Time elapsed: 0.518 s % 60.08/8.71 % (1606636)Peak memory usage: 14 MB % 60.08/8.71 % (1606636)Instructions burned: 1181 (million) % 60.08/8.71 % (1606662)ott+10_1_sil=32000:tgt=ground:random_seed=4026692882:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 60.08/8.71 % (1606644)Instruction limit reached! % 60.08/8.71 % (1606644)------------------------------ % 60.08/8.71 % (1606644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.08/8.71 % (1606644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.08/8.71 % (1606644)CaDiCaL version: 2.1.3 % 60.08/8.71 % (1606644)Termination reason: Instruction limit % 60.08/8.71 % (1606644)Termination phase: Saturation % 60.08/8.71 % (1606644)Time elapsed: 0.490 s % 60.08/8.71 % (1606644)Peak memory usage: 19 MB % 60.08/8.71 % (1606644)Instructions burned: 881 (million) % 60.08/8.71 % (1606664)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=526878626:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 60.08/8.71 % Exception at run slice level % 60.08/8.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.08/8.71 % (1606666)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1561411599:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 60.08/8.71 % (1606660)Instruction limit reached! % 60.08/8.71 % (1606660)------------------------------ % 60.08/8.71 % (1606660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.08/8.71 % (1606660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.08/8.71 % (1606660)CaDiCaL version: 2.1.3 % 60.08/8.71 % (1606660)Termination reason: Instruction limit % 60.08/8.71 % (1606660)Termination phase: Saturation % 60.08/8.71 % (1606660)Time elapsed: 0.328 s % 60.08/8.71 % (1606660)Peak memory usage: 13 MB % 60.08/8.71 % (1606660)Instructions burned: 869 (million) % 60.08/8.71 % (1606668)dis+21_1_sil=32000:sas=cadical:random_seed=3392262221:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 60.08/8.71 % (1606653)Instruction limit reached! % 60.08/8.71 % (1606653)------------------------------ % 60.08/8.71 % (1606653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.24/14.55 % (1606653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.24/14.55 % (1606653)CaDiCaL version: 2.1.3 % 101.24/14.55 % (1606653)Termination reason: Instruction limit % 101.24/14.55 % (1606653)Termination phase: Saturation % 101.24/14.55 % (1606653)Time elapsed: 0.709 s % 101.24/14.55 % (1606653)Peak memory usage: 17 MB % 101.24/14.55 % (1606653)Instructions burned: 1473 (million) % 101.24/14.55 % (1606670)ott+11_1_sil=16000:gs=on:random_seed=3421606034:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 101.24/14.55 % (1606652)Instruction limit reached! % 101.24/14.55 % (1606652)------------------------------ % 101.24/14.55 % (1606652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.24/14.55 % (1606652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.24/14.55 % (1606652)CaDiCaL version: 2.1.3 % 101.24/14.55 % (1606652)Termination reason: Instruction limit % 101.24/14.55 % (1606652)Termination phase: Saturation % 101.24/14.55 % (1606652)Time elapsed: 1.258 s % 101.24/14.55 % (1606652)Peak memory usage: 21 MB % 101.24/14.55 % (1606652)Instructions burned: 5134 (million) % 101.24/14.55 % (1606672)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1596988723:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 101.24/14.55 % Exception at run slice level % 101.24/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.24/14.55 % (1606674)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2614586837:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 101.24/14.55 % (1606670)Instruction limit reached! % 101.24/14.55 % (1606670)------------------------------ % 101.24/14.55 % (1606670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.24/14.55 % (1606670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.24/14.55 % (1606670)CaDiCaL version: 2.1.3 % 101.24/14.55 % (1606670)Termination reason: Instruction limit % 101.24/14.55 % (1606670)Termination phase: Saturation % 101.24/14.55 % (1606670)Time elapsed: 1.032 s % 101.24/14.55 % (1606670)Peak memory usage: 17 MB % 101.24/14.55 % (1606670)Instructions burned: 2253 (million) % 101.24/14.55 % (1606676)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3457462095:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 101.24/14.55 % (1606666)Instruction limit reached! % 101.24/14.55 % (1606666)------------------------------ % 101.24/14.55 % (1606666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.24/14.55 % (1606666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.24/14.55 % (1606666)CaDiCaL version: 2.1.3 % 101.24/14.55 % (1606666)Termination reason: Instruction limit % 101.24/14.55 % (1606666)Termination phase: Saturation % 101.24/14.55 % (1606666)Time elapsed: 1.589 s % 101.24/14.55 % (1606666)Peak memory usage: 19 MB % 101.24/14.55 % (1606666)Instructions burned: 3512 (million) % 101.24/14.55 % (1606678)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1737516968:i=5211_2976 on theBenchmark for (2976ds/5211Mi) % 101.24/14.55 % (1606668)Instruction limit reached! % 101.24/14.55 % (1606668)------------------------------ % 101.24/14.55 % (1606668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.24/14.55 % (1606668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.24/14.55 % (1606668)CaDiCaL version: 2.1.3 % 101.24/14.55 % (1606668)Termination reason: Instruction limit % 101.24/14.55 % (1606668)Termination phase: Saturation % 101.24/14.55 % (1606668)Time elapsed: 1.665 s % 101.24/14.55 % (1606668)Peak memory usage: 19 MB % 101.24/14.55 % (1606668)Instructions burned: 3775 (million) % 101.24/14.55 % (1606680)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=890510924:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi) % 101.24/14.55 % Exception at run slice level % 101.24/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.24/14.55 % (1606682)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=171573861:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi) % 101.24/14.55 % Exception at run slice level % 101.24/14.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.24/14.55 % (1606684)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2190611714:i=14071_2974 on theBenchmark for (2974ds/14071Mi) % 101.24/14.55 % Exception at run slice level % 163.00/23.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.00/23.26 % (1606686)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=391758089:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi) % 163.00/23.26 % (1606674)Instruction limit reached! % 163.00/23.26 % (1606674)------------------------------ % 163.00/23.26 % (1606674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606674)CaDiCaL version: 2.1.3 % 163.00/23.26 % (1606674)Termination reason: Instruction limit % 163.00/23.26 % (1606674)Termination phase: Saturation % 163.00/23.26 % (1606674)Time elapsed: 0.910 s % 163.00/23.26 % (1606674)Peak memory usage: 14 MB % 163.00/23.26 % (1606674)Instructions burned: 4591 (million) % 163.00/23.26 % (1606688)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2373128631:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 163.00/23.26 % (1606662)Instruction limit reached! % 163.00/23.26 % (1606662)------------------------------ % 163.00/23.26 % (1606662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606662)CaDiCaL version: 2.1.3 % 163.00/23.26 % (1606662)Termination reason: Instruction limit % 163.00/23.26 % (1606662)Termination phase: Saturation % 163.00/23.26 % (1606662)Time elapsed: 2.192 s % 163.00/23.26 % (1606662)Peak memory usage: 18 MB % 163.00/23.26 % (1606662)Instructions burned: 5117 (million) % 163.00/23.26 % (1606690)dis+10_16:1_sil=16000:random_seed=86769157:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 163.00/23.26 % (1606688)Instruction limit reached! % 163.00/23.26 % (1606688)------------------------------ % 163.00/23.26 % (1606688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606688)CaDiCaL version: 2.1.3 % 163.00/23.26 % (1606688)Termination reason: Instruction limit % 163.00/23.26 % (1606688)Termination phase: Saturation % 163.00/23.26 % (1606688)Time elapsed: 1.794 s % 163.00/23.26 % (1606688)Peak memory usage: 19 MB % 163.00/23.26 % (1606688)Instructions burned: 8179 (million) % 163.00/23.26 % (1606692)ott-3_8_sil=64000:random_seed=468146450:i=20139:bs=on_2955 on theBenchmark for (2955ds/20139Mi) % 163.00/23.26 % (1606678)Instruction limit reached! % 163.00/23.26 % (1606678)------------------------------ % 163.00/23.26 % (1606678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606678)CaDiCaL version: 2.1.3 % 163.00/23.26 % (1606678)Termination reason: Instruction limit % 163.00/23.26 % (1606678)Termination phase: Saturation % 163.00/23.26 % (1606678)Time elapsed: 2.627 s % 163.00/23.26 % (1606678)Peak memory usage: 43 MB % 163.00/23.26 % (1606678)Instructions burned: 5213 (million) % 163.00/23.26 % (1606694)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1153935670:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi) % 163.00/23.26 % Exception at run slice level % 163.00/23.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 163.00/23.26 % (1606696)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3789788165:i=11404_2949 on theBenchmark for (2949ds/11404Mi) % 163.00/23.26 % (1606690)Instruction limit reached! % 163.00/23.26 % (1606690)------------------------------ % 163.00/23.26 % (1606690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606690)CaDiCaL version: 2.1.3 % 163.00/23.26 % (1606690)Termination reason: Instruction limit % 163.00/23.26 % (1606690)Termination phase: Saturation % 163.00/23.26 % (1606690)Time elapsed: 4.562 s % 163.00/23.26 % (1606690)Peak memory usage: 36 MB % 163.00/23.26 % (1606690)Instructions burned: 9155 (million) % 163.00/23.26 % (1606698)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=546871149:i=14134_2925 on theBenchmark for (2925ds/14134Mi) % 163.00/23.26 % (1606692)Instruction limit reached! % 163.00/23.26 % (1606692)------------------------------ % 163.00/23.26 % (1606692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.00/23.26 % (1606692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.00/23.26 % (1606692)CaDiCaL version: 2.1.3 % 182.37/25.91 % (1606692)Termination reason: Instruction limit % 182.37/25.91 % (1606692)Termination phase: Saturation % 182.37/25.91 % (1606692)Time elapsed: 4.080 s % 182.37/25.91 % (1606692)Peak memory usage: 17 MB % 182.37/25.91 % (1606692)Instructions burned: 20142 (million) % 182.37/25.91 % (1606700)dis+33_16_sil=32000:sac=on:random_seed=1555726373:i=15851:nm=0_2915 on theBenchmark for (2915ds/15851Mi) % 182.37/25.91 % (1606696)Instruction limit reached! % 182.37/25.91 % (1606696)------------------------------ % 182.37/25.91 % (1606696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.37/25.91 % (1606696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.37/25.91 % (1606696)CaDiCaL version: 2.1.3 % 182.37/25.91 % (1606696)Termination reason: Instruction limit % 182.37/25.91 % (1606696)Termination phase: Saturation % 182.37/25.91 % (1606696)Time elapsed: 6.342 s % 182.37/25.91 % (1606696)Peak memory usage: 55 MB % 182.37/25.91 % (1606696)Instructions burned: 11405 (million) % 182.37/25.91 % (1606702)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3889081723:avsq=on:i=17627:add=on:amm=off_2886 on theBenchmark for (2886ds/17627Mi) % 182.37/25.91 % (1606700)Instruction limit reached! % 182.37/25.91 % (1606700)------------------------------ % 182.37/25.91 % (1606700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.37/25.91 % (1606700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.37/25.91 % (1606700)CaDiCaL version: 2.1.3 % 182.37/25.91 % (1606700)Termination reason: Instruction limit % 182.37/25.91 % (1606700)Termination phase: Saturation % 182.37/25.91 % (1606700)Time elapsed: 3.364 s % 182.37/25.91 % (1606700)Peak memory usage: 20 MB % 182.37/25.91 % (1606700)Instructions burned: 15854 (million) % 182.37/25.91 % (1606704)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=786780064:s2a=on:i=53295_2881 on theBenchmark for (2881ds/53295Mi) % 182.37/25.91 % (1606698)Instruction limit reached! % 182.37/25.91 % (1606698)------------------------------ % 182.37/25.91 % (1606698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.37/25.91 % (1606698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.37/25.91 % (1606698)CaDiCaL version: 2.1.3 % 182.37/25.91 % (1606698)Termination reason: Instruction limit % 182.37/25.91 % (1606698)Termination phase: Saturation % 182.37/25.91 % (1606698)Time elapsed: 5.620 s % 182.37/25.91 % (1606698)Peak memory usage: 18 MB % 182.37/25.91 % (1606698)Instructions burned: 14136 (million) % 182.37/25.91 % (1606706)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3318318068:i=26857:ins=20_2868 on theBenchmark for (2868ds/26857Mi) % 182.37/25.91 % Exception at run slice level % 182.37/25.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.37/25.91 % (1606708)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=299823251:i=28120:bs=on:fsr=off_2868 on theBenchmark for (2868ds/28120Mi) % 182.37/25.91 % (1606676)Instruction limit reached! % 182.37/25.91 % (1606676)------------------------------ % 182.37/25.91 % (1606676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.37/25.91 % (1606676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.37/25.91 % (1606676)CaDiCaL version: 2.1.3 % 182.37/25.91 % (1606676)Termination reason: Instruction limit % 182.37/25.91 % (1606676)Termination phase: Saturation % 182.37/25.91 % (1606676)Time elapsed: 12.037 s % 182.37/25.91 % (1606676)Peak memory usage: 28 MB % 182.37/25.91 % (1606676)Instructions burned: 29342 (million) % 182.37/25.91 % (1606915)fmb+10_1_sil=256000:fmbss=7:random_seed=2444194279:fmbsr=1.6:i=182295_2857 on theBenchmark for (2857ds/182295Mi) % 182.37/25.91 % Exception at run slice level % 182.37/25.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.37/25.91 % (1606926)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3158245398:i=44625:gsp=on_2857 on theBenchmark for (2857ds/44625Mi) % 182.37/25.91 % (1606926)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 182.37/25.91 % Exception at run slice level % 182.37/25.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.37/25.91 % (1606929)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2506139038:i=160505_2857 on theBenchmark for (2857ds/160505Mi) % 182.37/25.91 % Exception at run slice level % 182.37/25.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.37/25.91 % (1606933)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3447879074:fmbsr=1.3:i=225729_2856 on theBenchmark for (2856ds/225729Mi) % 212.96/30.23 % Exception at run slice level % 212.96/30.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 212.96/30.23 % (1606946)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3096758701:fmbsr=2:i=185024:ins=7_2856 on theBenchmark for (2856ds/185024Mi) % 212.96/30.23 % Exception at run slice level % 212.96/30.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 212.96/30.23 % (1606955)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1628690576:rtra=on_2856 on theBenchmark for (2856ds/0Mi) % 212.96/30.23 % Exception at run slice level % 212.96/30.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 212.96/30.23 % (1606962)% WARNING: option uhcvi not known. % 212.96/30.23 % (1606962)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2121698043:i=271062:add=off:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/271062Mi) % 212.96/30.23 % (1606686)Instruction limit reached! % 212.96/30.23 % (1606686)------------------------------ % 212.96/30.23 % (1606686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.96/30.23 % (1606686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.96/30.23 % (1606686)CaDiCaL version: 2.1.3 % 212.96/30.23 % (1606686)Termination reason: Instruction limit % 212.96/30.23 % (1606686)Termination phase: Saturation % 212.96/30.23 % (1606686)Time elapsed: 12.285 s % 212.96/30.23 % (1606686)Peak memory usage: 116 MB % 212.96/30.23 % (1606686)Instructions burned: 22565 (million) % 212.96/30.23 % (1607009)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3312014996:i=176048:add=on:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/176048Mi) % 212.96/30.23 % (1606702)Instruction limit reached! % 212.96/30.23 % (1606702)------------------------------ % 212.96/30.23 % (1606702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.96/30.23 % (1606702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.96/30.23 % (1606702)CaDiCaL version: 2.1.3 % 212.96/30.23 % (1606702)Termination reason: Instruction limit % 212.96/30.23 % (1606702)Termination phase: Saturation % 212.96/30.23 % (1606702)Time elapsed: 10.960 s % 212.96/30.23 % (1606702)Peak memory usage: 34 MB % 212.96/30.23 % (1606702)Instructions burned: 17628 (million) % 212.96/30.23 % (1607041)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1754781643:i=206:fgj=on:rtra=on_2776 on theBenchmark for (2776ds/206Mi) % 212.96/30.23 % (1607041)Instruction limit reached! % 212.96/30.23 % (1607041)------------------------------ % 212.96/30.23 % (1607041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.96/30.23 % (1607041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.96/30.23 % (1607041)CaDiCaL version: 2.1.3 % 212.96/30.23 % (1607041)Termination reason: Instruction limit % 212.96/30.23 % (1607041)Termination phase: Saturation % 212.96/30.23 % (1607041)Time elapsed: 0.185 s % 212.96/30.23 % (1607041)Peak memory usage: 13 MB % 212.96/30.23 % (1607041)Instructions burned: 206 (million) % 212.96/30.23 % (1607043)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=715093741:i=232:rtra=on_2773 on theBenchmark for (2773ds/232Mi) % 212.96/30.23 % (1607043)Instruction limit reached! % 212.96/30.23 % (1607043)------------------------------ % 212.96/30.23 % (1607043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.96/30.23 % (1607043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.96/30.23 % (1607043)CaDiCaL version: 2.1.3 % 212.96/30.23 % (1607043)Termination reason: Instruction limit % 212.96/30.23 % (1607043)Termination phase: Saturation % 212.96/30.23 % (1607043)Time elapsed: 0.170 s % 212.96/30.23 % (1607043)Peak memory usage: 13 MB % 212.96/30.23 % (1607043)Instructions burned: 232 (million) % 212.96/30.23 % (1607045)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2492176055:i=262:rtra=on_2771 on theBenchmark for (2771ds/262Mi) % 212.96/30.23 % (1607045)Instruction limit reached! % 212.96/30.23 % (1607045)------------------------------ % 212.96/30.23 % (1607045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.96/30.23 % (1607045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.96/30.23 % (1607045)CaDiCaL version: 2.1.3 % 212.96/30.23 % (1607045)Termination reason: Instruction limit % 212.96/30.23 % (1607045)Termination phase: Saturation % 266.27/37.75 % (1607045)Time elapsed: 0.211 s % 266.27/37.75 % (1607045)Peak memory usage: 12 MB % 266.27/37.75 % (1607045)Instructions burned: 264 (million) % 266.27/37.75 % (1607047)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3583452846:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2769 on theBenchmark for (2769ds/318Mi) % 266.27/37.75 % (1607047)Instruction limit reached! % 266.27/37.75 % (1607047)------------------------------ % 266.27/37.75 % (1607047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.27/37.75 % (1607047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.27/37.75 % (1607047)CaDiCaL version: 2.1.3 % 266.27/37.75 % (1607047)Termination reason: Instruction limit % 266.27/37.75 % (1607047)Termination phase: Saturation % 266.27/37.75 % (1607047)Time elapsed: 0.233 s % 266.27/37.75 % (1607047)Peak memory usage: 13 MB % 266.27/37.75 % (1607047)Instructions burned: 318 (million) % 266.27/37.75 % (1607049)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=958563970:i=1428:nm=2:rtra=on_2766 on theBenchmark for (2766ds/1428Mi) % 266.27/37.75 % Exception at run slice level % 266.27/37.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 266.27/37.75 % (1607051)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=652986683:i=262:bd=preordered:rtra=on:fsd=on_2766 on theBenchmark for (2766ds/262Mi) % 266.27/37.75 % (1607051)Instruction limit reached! % 266.27/37.75 % (1607051)------------------------------ % 266.27/37.75 % (1607051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.27/37.75 % (1607051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.27/37.75 % (1607051)CaDiCaL version: 2.1.3 % 266.27/37.75 % (1607051)Termination reason: Instruction limit % 266.27/37.75 % (1607051)Termination phase: Saturation % 266.27/37.75 % (1607051)Time elapsed: 0.216 s % 266.27/37.75 % (1607051)Peak memory usage: 13 MB % 266.27/37.75 % (1607051)Instructions burned: 263 (million) % 266.27/37.75 % (1607053)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=1446678758:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2764 on theBenchmark for (2764ds/1368Mi) % 266.27/37.75 % (1607053)Instruction limit reached! % 266.27/37.75 % (1607053)------------------------------ % 266.27/37.75 % (1607053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.27/37.75 % (1607053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.27/37.75 % (1607053)CaDiCaL version: 2.1.3 % 266.27/37.75 % (1607053)Termination reason: Instruction limit % 266.27/37.75 % (1607053)Termination phase: Saturation % 266.27/37.75 % (1607053)Time elapsed: 0.887 s % 266.27/37.75 % (1607053)Peak memory usage: 15 MB % 266.27/37.75 % (1607053)Instructions burned: 1375 (million) % 266.27/37.75 % (1607059)ott-21_1_sil=16000:si=on:fs=off:random_seed=183222329:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 266.27/37.75 % (1607059)Instruction limit reached! % 266.27/37.75 % (1607059)------------------------------ % 266.27/37.75 % (1607059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.27/37.75 % (1607059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.27/37.75 % (1607059)CaDiCaL version: 2.1.3 % 266.27/37.75 % (1607059)Termination reason: Instruction limit % 266.27/37.75 % (1607059)Termination phase: Saturation % 266.27/37.75 % (1607059)Time elapsed: 0.264 s % 266.27/37.75 % (1607059)Peak memory usage: 13 MB % 266.27/37.75 % (1607059)Instructions burned: 362 (million) % 266.27/37.75 % (1607061)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2703285026:i=954:bd=all:rtra=on_2752 on theBenchmark for (2752ds/954Mi) % 266.27/37.75 % (1607061)Instruction limit reached! % 266.27/37.75 % (1607061)------------------------------ % 266.27/37.75 % (1607061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.27/37.75 % (1607061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.27/37.75 % (1607061)CaDiCaL version: 2.1.3 % 266.27/37.75 % (1607061)Termination reason: Instruction limit % 266.27/37.75 % (1607061)Termination phase: Saturation % 266.27/37.75 % (1607061)Time elapsed: 0.838 s % 266.27/37.75 % (1607061)Peak memory usage: 15 MB % 266.27/37.75 % (1607061)Instructions burned: 954 (million) % 266.27/37.75 % (1607065)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4038107410:fmbsr=1.3:i=1730:ins=25:rtra=on_2743 on theBenchmark for (2743ds/1730Mi) % 266.27/37.75 % Exception at run slice level % 266.27/37.75 User error: Finite model building is currentlTerminated % 300.43/42.54 % Vampire exiting % 300.43/42.54 Terminated %------------------------------------------------------------------------------