%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV625_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 : n004.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:26:09 PM UTC 2026 % Result : Timeout 300.01s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV625_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.09/0.19 % Computer : n004.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 12:04:52 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/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.93/1.46 % (309734)Will run a generic schedule for satisfiability detection. % 7.93/1.46 % (309741)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3957407335:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.93/1.46 % (309740)% WARNING: option uhcvi not known. % 7.93/1.46 % (309739)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1549143234_2999 on theBenchmark for (2999ds/0Mi) % 7.93/1.46 % (309743)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=937342726:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.93/1.46 % (309742)dis+10_1_sil=32000:sp=arity:random_seed=3233259300:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.93/1.46 % (309740)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2227299711:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.93/1.46 % (309744)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3797110818:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.93/1.46 % (309745)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3919684521:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.93/1.46 % Exception at run slice level % 7.93/1.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.93/1.46 % (309753)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2892105291:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.93/1.46 % Exception at run slice level % 7.93/1.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.93/1.46 % (309755)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4119838495:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.93/1.46 % (309742)Instruction limit reached! % 7.93/1.46 % (309742)------------------------------ % 7.93/1.46 % (309742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.46 % (309742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.46 % (309742)CaDiCaL version: 2.1.3 % 7.93/1.46 % (309742)Termination reason: Instruction limit % 7.93/1.46 % (309742)Termination phase: Saturation % 7.93/1.46 % (309742)Time elapsed: 0.066 s % 7.93/1.46 % (309742)Peak memory usage: 13 MB % 7.93/1.46 % (309742)Instructions burned: 103 (million) % 7.93/1.46 % (309743)Instruction limit reached! % 7.93/1.46 % (309743)------------------------------ % 7.93/1.46 % (309743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.46 % (309743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.46 % (309743)CaDiCaL version: 2.1.3 % 7.93/1.46 % (309743)Termination reason: Instruction limit % 7.93/1.46 % (309743)Termination phase: Saturation % 7.93/1.46 % (309743)Time elapsed: 0.072 s % 7.93/1.46 % (309743)Peak memory usage: 13 MB % 7.93/1.46 % (309743)Instructions burned: 117 (million) % 7.93/1.46 % (309744)Instruction limit reached! % 7.93/1.46 % (309744)------------------------------ % 7.93/1.46 % (309744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.46 % (309744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.46 % (309744)CaDiCaL version: 2.1.3 % 7.93/1.46 % (309744)Termination reason: Instruction limit % 7.93/1.46 % (309744)Termination phase: Saturation % 7.93/1.46 % (309744)Time elapsed: 0.082 s % 7.93/1.46 % (309744)Peak memory usage: 13 MB % 7.93/1.46 % (309744)Instructions burned: 131 (million) % 7.93/1.46 % (309757)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=4276535725:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.93/1.46 % (309758)ott-21_1_sil=16000:fs=off:random_seed=775751390:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.93/1.46 % (309745)Instruction limit reached! % 7.93/1.46 % (309745)------------------------------ % 7.93/1.46 % (309745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.46 % (309745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.46 % (309745)CaDiCaL version: 2.1.3 % 7.93/1.46 % (309745)Termination reason: Instruction limit % 7.93/1.46 % (309745)Termination phase: Saturation % 7.93/1.46 % (309745)Time elapsed: 0.100 s % 7.93/1.46 % (309745)Peak memory usage: 14 MB % 7.93/1.46 % (309745)Instructions burned: 161 (million) % 7.93/1.46 % (309759)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2893354436:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.79/3.57 % (309762)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=407867321:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.79/3.57 % Exception at run slice level % 22.79/3.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.79/3.57 % (309755)Instruction limit reached! % 22.79/3.57 % (309755)------------------------------ % 22.79/3.57 % (309755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.79/3.57 % (309755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.79/3.57 % (309755)CaDiCaL version: 2.1.3 % 22.79/3.57 % (309755)Termination reason: Instruction limit % 22.79/3.57 % (309755)Termination phase: Saturation % 22.79/3.57 % (309755)Time elapsed: 0.086 s % 22.79/3.57 % (309755)Peak memory usage: 13 MB % 22.79/3.57 % (309755)Instructions burned: 131 (million) % 22.79/3.57 % (309765)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=939536967:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.79/3.57 % (309766)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=156593721:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.79/3.57 % Exception at run slice level % 22.79/3.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.79/3.57 % (309769)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=3894471903: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) % 22.79/3.57 % (309758)Instruction limit reached! % 22.79/3.57 % (309758)------------------------------ % 22.79/3.57 % (309758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.79/3.57 % (309758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.79/3.57 % (309758)CaDiCaL version: 2.1.3 % 22.79/3.57 % (309758)Termination reason: Instruction limit % 22.79/3.57 % (309758)Termination phase: Saturation % 22.79/3.57 % (309758)Time elapsed: 0.088 s % 22.79/3.57 % (309758)Peak memory usage: 12 MB % 22.79/3.57 % (309758)Instructions burned: 181 (million) % 22.79/3.57 % (309771)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1490029960:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.79/3.57 % (309759)Instruction limit reached! % 22.79/3.57 % (309759)------------------------------ % 22.79/3.57 % (309759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.79/3.57 % (309759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.79/3.57 % (309759)CaDiCaL version: 2.1.3 % 22.79/3.57 % (309759)Termination reason: Instruction limit % 22.79/3.57 % (309759)Termination phase: Saturation % 22.79/3.57 % (309759)Time elapsed: 0.309 s % 22.79/3.57 % (309759)Peak memory usage: 14 MB % 22.79/3.57 % (309759)Instructions burned: 477 (million) % 22.79/3.57 % (309773)fmb+10_1_sil=64000:random_seed=2623623259:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.79/3.57 % (309773)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.79/3.57 % Exception at run slice level % 22.79/3.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.79/3.57 % (309757)Instruction limit reached! % 22.79/3.57 % (309757)------------------------------ % 22.79/3.57 % (309757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.79/3.57 % (309757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.79/3.57 % (309757)CaDiCaL version: 2.1.3 % 22.79/3.57 % (309757)Termination reason: Instruction limit % 22.79/3.57 % (309757)Termination phase: Saturation % 22.79/3.57 % (309757)Time elapsed: 0.368 s % 22.79/3.57 % (309757)Peak memory usage: 18 MB % 22.79/3.57 % (309757)Instructions burned: 686 (million) % 22.79/3.57 % (309775)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1717971407:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.79/3.57 % Exception at run slice level % 22.79/3.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.79/3.57 % (309777)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1547726549:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.79/3.57 % (309778)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3820424011:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 92.03/13.26 % Exception at run slice level % 92.03/13.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 92.03/13.26 % (309781)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1698864541:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 92.03/13.26 % (309781)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 92.03/13.26 % (309769)Instruction limit reached! % 92.03/13.26 % (309769)------------------------------ % 92.03/13.26 % (309769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.03/13.26 % (309769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.03/13.26 % (309769)CaDiCaL version: 2.1.3 % 92.03/13.26 % (309769)Termination reason: Instruction limit % 92.03/13.26 % (309769)Termination phase: Saturation % 92.03/13.26 % (309769)Time elapsed: 0.394 s % 92.03/13.26 % (309769)Peak memory usage: 20 MB % 92.03/13.26 % (309769)Instructions burned: 692 (million) % 92.03/13.26 % (309783)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1538180827:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 92.03/13.26 % Exception at run slice level % 92.03/13.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 92.03/13.26 % (309785)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=981154662:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 92.03/13.26 % Exception at run slice level % 92.03/13.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 92.03/13.26 % (309787)ott-2_1_sil=16000:newcnf=on:random_seed=1957907468:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 92.03/13.26 % (309771)Instruction limit reached! % 92.03/13.26 % (309771)------------------------------ % 92.03/13.26 % (309771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.03/13.26 % (309771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.03/13.26 % (309771)CaDiCaL version: 2.1.3 % 92.03/13.26 % (309771)Termination reason: Instruction limit % 92.03/13.26 % (309771)Termination phase: Saturation % 92.03/13.26 % (309771)Time elapsed: 0.485 s % 92.03/13.26 % (309771)Peak memory usage: 20 MB % 92.03/13.26 % (309771)Instructions burned: 879 (million) % 92.03/13.26 % (309789)ott+10_1_sil=32000:tgt=ground:random_seed=3771666926:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 92.03/13.26 % (309765)Instruction limit reached! % 92.03/13.26 % (309765)------------------------------ % 92.03/13.26 % (309765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.03/13.26 % (309765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.03/13.26 % (309765)CaDiCaL version: 2.1.3 % 92.03/13.26 % (309765)Termination reason: Instruction limit % 92.03/13.26 % (309765)Termination phase: Saturation % 92.03/13.26 % (309765)Time elapsed: 0.737 s % 92.03/13.26 % (309765)Peak memory usage: 21 MB % 92.03/13.26 % (309765)Instructions burned: 1180 (million) % 92.03/13.26 % (309791)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=789026043:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 92.03/13.26 % Exception at run slice level % 92.03/13.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 92.03/13.26 % (309793)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=894776604:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 92.03/13.26 % (309787)Instruction limit reached! % 92.03/13.26 % (309787)------------------------------ % 92.03/13.26 % (309787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.03/13.26 % (309787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.03/13.26 % (309787)CaDiCaL version: 2.1.3 % 92.03/13.26 % (309787)Termination reason: Instruction limit % 92.03/13.26 % (309787)Termination phase: Saturation % 92.03/13.26 % (309787)Time elapsed: 0.335 s % 92.03/13.26 % (309787)Peak memory usage: 14 MB % 92.03/13.26 % (309787)Instructions burned: 869 (million) % 92.03/13.26 % (309795)dis+21_1_sil=32000:sas=cadical:random_seed=59596942:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 92.03/13.26 % (309781)Instruction limit reached! % 92.03/13.26 % (309781)------------------------------ % 92.03/13.26 % (309781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.03/13.26 % (309781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.03/13.26 % (309781)CaDiCaL version: 2.1.3 % 135.34/19.32 % (309781)Termination reason: Instruction limit % 135.34/19.32 % (309781)Termination phase: Saturation % 135.34/19.32 % (309781)Time elapsed: 0.698 s % 135.34/19.32 % (309781)Peak memory usage: 24 MB % 135.34/19.32 % (309781)Instructions burned: 1472 (million) % 135.34/19.32 % (309797)ott+11_1_sil=16000:gs=on:random_seed=2412030745:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 135.34/19.32 % (309797)Instruction limit reached! % 135.34/19.32 % (309797)------------------------------ % 135.34/19.32 % (309797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.34/19.32 % (309797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.34/19.32 % (309797)CaDiCaL version: 2.1.3 % 135.34/19.32 % (309797)Termination reason: Instruction limit % 135.34/19.32 % (309797)Termination phase: Saturation % 135.34/19.32 % (309797)Time elapsed: 1.152 s % 135.34/19.32 % (309797)Peak memory usage: 24 MB % 135.34/19.32 % (309797)Instructions burned: 2252 (million) % 135.34/19.32 % (309799)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=61973722:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 135.34/19.32 % Exception at run slice level % 135.34/19.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 135.34/19.32 % (309801)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2654379325:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 135.34/19.32 % (309793)Instruction limit reached! % 135.34/19.32 % (309793)------------------------------ % 135.34/19.32 % (309793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.34/19.32 % (309793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.34/19.32 % (309793)CaDiCaL version: 2.1.3 % 135.34/19.32 % (309793)Termination reason: Instruction limit % 135.34/19.32 % (309793)Termination phase: Saturation % 135.34/19.32 % (309793)Time elapsed: 1.931 s % 135.34/19.32 % (309793)Peak memory usage: 33 MB % 135.34/19.32 % (309793)Instructions burned: 3514 (million) % 135.34/19.32 % (309803)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1691445945:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 135.34/19.32 % (309795)Instruction limit reached! % 135.34/19.32 % (309795)------------------------------ % 135.34/19.32 % (309795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.34/19.32 % (309795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.34/19.32 % (309795)CaDiCaL version: 2.1.3 % 135.34/19.32 % (309795)Termination reason: Instruction limit % 135.34/19.32 % (309795)Termination phase: Saturation % 135.34/19.32 % (309795)Time elapsed: 2.200 s % 135.34/19.32 % (309795)Peak memory usage: 33 MB % 135.34/19.32 % (309795)Instructions burned: 3773 (million) % 135.34/19.32 % (309778)Instruction limit reached! % 135.34/19.32 % (309778)------------------------------ % 135.34/19.32 % (309778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.34/19.32 % (309778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.34/19.32 % (309778)CaDiCaL version: 2.1.3 % 135.34/19.32 % (309778)Termination reason: Instruction limit % 135.34/19.32 % (309778)Termination phase: Saturation % 135.34/19.32 % (309778)Time elapsed: 2.727 s % 135.34/19.32 % (309778)Peak memory usage: 35 MB % 135.34/19.32 % (309778)Instructions burned: 5132 (million) % 135.34/19.32 % (309805)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=336132240:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 135.34/19.32 % (309806)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3727153094:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 135.34/19.32 % Exception at run slice level % 135.34/19.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 135.34/19.32 % (309809)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1075561369:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 135.34/19.32 % Exception at run slice level % 135.34/19.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 135.34/19.32 % (309811)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3353976191:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 135.34/19.32 % Exception at run slice level % 135.34/19.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 135.34/19.32 % (309813)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4109709086:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 157.13/22.40 % (309789)Instruction limit reached! % 157.13/22.40 % (309789)------------------------------ % 157.13/22.40 % (309789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309789)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309789)Termination reason: Instruction limit % 157.13/22.40 % (309789)Termination phase: Saturation % 157.13/22.40 % (309789)Time elapsed: 3.224 s % 157.13/22.40 % (309789)Peak memory usage: 37 MB % 157.13/22.40 % (309789)Instructions burned: 5115 (million) % 157.13/22.40 % (309815)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=412123801:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 157.13/22.40 % (309801)Instruction limit reached! % 157.13/22.40 % (309801)------------------------------ % 157.13/22.40 % (309801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309801)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309801)Termination reason: Instruction limit % 157.13/22.40 % (309801)Termination phase: Saturation % 157.13/22.40 % (309801)Time elapsed: 2.080 s % 157.13/22.40 % (309801)Peak memory usage: 54 MB % 157.13/22.40 % (309801)Instructions burned: 4592 (million) % 157.13/22.40 % (309817)dis+10_16:1_sil=16000:random_seed=2252540893:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 157.13/22.40 % (309805)Instruction limit reached! % 157.13/22.40 % (309805)------------------------------ % 157.13/22.40 % (309805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309805)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309805)Termination reason: Instruction limit % 157.13/22.40 % (309805)Termination phase: Saturation % 157.13/22.40 % (309805)Time elapsed: 2.527 s % 157.13/22.40 % (309805)Peak memory usage: 38 MB % 157.13/22.40 % (309805)Instructions burned: 5212 (million) % 157.13/22.40 % (309819)ott-3_8_sil=64000:random_seed=3295905515:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 157.13/22.40 % (309815)Instruction limit reached! % 157.13/22.40 % (309815)------------------------------ % 157.13/22.40 % (309815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309815)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309815)Termination reason: Instruction limit % 157.13/22.40 % (309815)Termination phase: Saturation % 157.13/22.40 % (309815)Time elapsed: 4.865 s % 157.13/22.40 % (309815)Peak memory usage: 60 MB % 157.13/22.40 % (309815)Instructions burned: 8174 (million) % 157.13/22.40 % (309821)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4190317216:fmbsr=2:i=32576_2911 on theBenchmark for (2911ds/32576Mi) % 157.13/22.40 % Exception at run slice level % 157.13/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 157.13/22.40 % (309823)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2883774722:i=11404_2911 on theBenchmark for (2911ds/11404Mi) % 157.13/22.40 % (309817)Instruction limit reached! % 157.13/22.40 % (309817)------------------------------ % 157.13/22.40 % (309817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309817)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309817)Termination reason: Instruction limit % 157.13/22.40 % (309817)Termination phase: Saturation % 157.13/22.40 % (309817)Time elapsed: 4.945 s % 157.13/22.40 % (309817)Peak memory usage: 68 MB % 157.13/22.40 % (309817)Instructions burned: 9156 (million) % 157.13/22.40 % (309825)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2989792334:i=14134_2904 on theBenchmark for (2904ds/14134Mi) % 157.13/22.40 % (309813)Instruction limit reached! % 157.13/22.40 % (309813)------------------------------ % 157.13/22.40 % (309813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.13/22.40 % (309813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.13/22.40 % (309813)CaDiCaL version: 2.1.3 % 157.13/22.40 % (309813)Termination reason: Instruction limit % 157.13/22.40 % (309813)Termination phase: Saturation % 157.13/22.40 % (309813)Time elapsed: 9.665 s % 157.13/22.40 % (309813)Peak memory usage: 27 MB % 157.13/22.40 % (309813)Instructions burned: 22566 (million) % 157.13/22.40 % (309827)dis+33_16_sil=32000:sac=on:random_seed=1807005710:i=15851:nm=0_2869 on theBenchmark for (2869ds/15851Mi) % 181.46/25.88 % (309823)Instruction limit reached! % 181.46/25.88 % (309823)------------------------------ % 181.46/25.88 % (309823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.46/25.88 % (309823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.46/25.88 % (309823)CaDiCaL version: 2.1.3 % 181.46/25.88 % (309823)Termination reason: Instruction limit % 181.46/25.88 % (309823)Termination phase: Saturation % 181.46/25.88 % (309823)Time elapsed: 7.393 s % 181.46/25.88 % (309823)Peak memory usage: 72 MB % 181.46/25.88 % (309823)Instructions burned: 11405 (million) % 181.46/25.88 % (309891)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1426800826:avsq=on:i=17627:add=on:amm=off_2836 on theBenchmark for (2836ds/17627Mi) % 181.46/25.88 % (309803)Instruction limit reached! % 181.46/25.88 % (309803)------------------------------ % 181.46/25.88 % (309803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.46/25.88 % (309803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.46/25.88 % (309803)CaDiCaL version: 2.1.3 % 181.46/25.88 % (309803)Termination reason: Instruction limit % 181.46/25.88 % (309803)Termination phase: Saturation % 181.46/25.88 % (309803)Time elapsed: 13.502 s % 181.46/25.88 % (309803)Peak memory usage: 149 MB % 181.46/25.88 % (309803)Instructions burned: 29341 (million) % 181.46/25.88 % (309893)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3923277302:s2a=on:i=53295_2835 on theBenchmark for (2835ds/53295Mi) % 181.46/25.88 % (309825)Instruction limit reached! % 181.46/25.88 % (309825)------------------------------ % 181.46/25.88 % (309825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.46/25.88 % (309825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.46/25.88 % (309825)CaDiCaL version: 2.1.3 % 181.46/25.88 % (309825)Termination reason: Instruction limit % 181.46/25.88 % (309825)Termination phase: Saturation % 181.46/25.88 % (309825)Time elapsed: 8.701 s % 181.46/25.88 % (309825)Peak memory usage: 80 MB % 181.46/25.88 % (309825)Instructions burned: 14134 (million) % 181.46/25.88 % (309895)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2969546823:i=26857:ins=20_2817 on theBenchmark for (2817ds/26857Mi) % 181.46/25.88 % Exception at run slice level % 181.46/25.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.46/25.88 % (309897)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=956106207:i=28120:bs=on:fsr=off_2817 on theBenchmark for (2817ds/28120Mi) % 181.46/25.88 % (309819)Instruction limit reached! % 181.46/25.88 % (309819)------------------------------ % 181.46/25.88 % (309819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.46/25.88 % (309819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.46/25.88 % (309819)CaDiCaL version: 2.1.3 % 181.46/25.88 % (309819)Termination reason: Instruction limit % 181.46/25.88 % (309819)Termination phase: Saturation % 181.46/25.88 % (309819)Time elapsed: 13.150 s % 181.46/25.88 % (309819)Peak memory usage: 126 MB % 181.46/25.88 % (309819)Instructions burned: 20140 (million) % 181.46/25.88 % (309899)fmb+10_1_sil=256000:fmbss=7:random_seed=99228493:fmbsr=1.6:i=182295_2810 on theBenchmark for (2810ds/182295Mi) % 181.46/25.88 % Exception at run slice level % 181.46/25.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.46/25.88 % (309901)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1497783165:i=44625:gsp=on_2810 on theBenchmark for (2810ds/44625Mi) % 181.46/25.88 % (309901)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 181.46/25.88 % Exception at run slice level % 181.46/25.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.46/25.88 % (309903)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=108787005:i=160505_2809 on theBenchmark for (2809ds/160505Mi) % 181.46/25.88 % Exception at run slice level % 181.46/25.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.46/25.88 % (309905)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1759485092:fmbsr=1.3:i=225729_2809 on theBenchmark for (2809ds/225729Mi) % 181.46/25.88 % Exception at run slice level % 181.46/25.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.46/25.88 % (309907)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1762389155:fmbsr=2:i=185024:ins=7_2809 on theBenchmark for (2809ds/185024Mi) % 205.14/29.20 % Exception at run slice level % 205.14/29.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.14/29.20 % (309909)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1442585184:rtra=on_2809 on theBenchmark for (2809ds/0Mi) % 205.14/29.20 % Exception at run slice level % 205.14/29.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 205.14/29.20 % (309911)% WARNING: option uhcvi not known. % 205.14/29.20 % (309911)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2736675026:i=271062:add=off:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/271062Mi) % 205.14/29.20 % (309741)Instruction limit reached! % 205.14/29.20 % (309741)------------------------------ % 205.14/29.20 % (309741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.14/29.20 % (309741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.14/29.20 % (309741)CaDiCaL version: 2.1.3 % 205.14/29.20 % (309741)Termination reason: Instruction limit % 205.14/29.20 % (309741)Termination phase: Saturation % 205.14/29.20 % (309741)Time elapsed: 21.290 s % 205.14/29.20 % (309741)Peak memory usage: 55 MB % 205.14/29.20 % (309741)Instructions burned: 88025 (million) % 205.14/29.20 % (309913)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2297693492:i=176048:add=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/176048Mi) % 205.14/29.20 % (309827)Instruction limit reached! % 205.14/29.20 % (309827)------------------------------ % 205.14/29.20 % (309827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.14/29.20 % (309827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.14/29.20 % (309827)CaDiCaL version: 2.1.3 % 205.14/29.20 % (309827)Termination reason: Instruction limit % 205.14/29.20 % (309827)Termination phase: Saturation % 205.14/29.20 % (309827)Time elapsed: 8.404 s % 205.14/29.20 % (309827)Peak memory usage: 130 MB % 205.14/29.20 % (309827)Instructions burned: 15852 (million) % 205.14/29.20 % (309915)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2442891918:i=206:fgj=on:rtra=on_2785 on theBenchmark for (2785ds/206Mi) % 205.14/29.20 % (309915)Instruction limit reached! % 205.14/29.20 % (309915)------------------------------ % 205.14/29.20 % (309915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.14/29.20 % (309915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.14/29.20 % (309915)CaDiCaL version: 2.1.3 % 205.14/29.20 % (309915)Termination reason: Instruction limit % 205.14/29.20 % (309915)Termination phase: Saturation % 205.14/29.20 % (309915)Time elapsed: 0.131 s % 205.14/29.20 % (309915)Peak memory usage: 13 MB % 205.14/29.20 % (309915)Instructions burned: 206 (million) % 205.14/29.20 % (309917)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4131833191:i=232:rtra=on_2784 on theBenchmark for (2784ds/232Mi) % 205.14/29.20 % (309917)Instruction limit reached! % 205.14/29.20 % (309917)------------------------------ % 205.14/29.20 % (309917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.14/29.20 % (309917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.14/29.20 % (309917)CaDiCaL version: 2.1.3 % 205.14/29.20 % (309917)Termination reason: Instruction limit % 205.14/29.20 % (309917)Termination phase: Saturation % 205.14/29.20 % (309917)Time elapsed: 0.146 s % 205.14/29.20 % (309917)Peak memory usage: 14 MB % 205.14/29.20 % (309917)Instructions burned: 233 (million) % 205.14/29.20 % (309919)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=536538297:i=262:rtra=on_2782 on theBenchmark for (2782ds/262Mi) % 205.14/29.20 % (309919)Instruction limit reached! % 205.14/29.20 % (309919)------------------------------ % 205.14/29.20 % (309919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.14/29.20 % (309919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.14/29.20 % (309919)CaDiCaL version: 2.1.3 % 205.14/29.20 % (309919)Termination reason: Instruction limit % 205.14/29.20 % (309919)Termination phase: Saturation % 205.14/29.20 % (309919)Time elapsed: 0.170 s % 205.14/29.20 % (309919)Peak memory usage: 14 MB % 205.14/29.20 % (309919)Instructions burned: 263 (million) % 205.14/29.20 % (309921)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3099076634:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2780 on theBenchmark for (2780ds/318Mi) % 205.14/29.20 % (309921)Instruction limit reached! % 205.14/29.20 % (309921)------------------------------ % 205.14/29.20 % (309921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.84/39.86 % (309921)CaDiCaL version: 2.1.3 % 280.84/39.86 % (309921)Termination reason: Instruction limit % 280.84/39.86 % (309921)Termination phase: Saturation % 280.84/39.86 % (309921)Time elapsed: 0.201 s % 280.84/39.86 % (309921)Peak memory usage: 15 MB % 280.84/39.86 % (309921)Instructions burned: 319 (million) % 280.84/39.86 % (309923)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=431991343:i=1428:nm=2:rtra=on_2778 on theBenchmark for (2778ds/1428Mi) % 280.84/39.86 % Exception at run slice level % 280.84/39.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 280.84/39.86 % (309925)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1106160766:i=262:bd=preordered:rtra=on:fsd=on_2777 on theBenchmark for (2777ds/262Mi) % 280.84/39.86 % (309925)Instruction limit reached! % 280.84/39.86 % (309925)------------------------------ % 280.84/39.86 % (309925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.84/39.86 % (309925)CaDiCaL version: 2.1.3 % 280.84/39.86 % (309925)Termination reason: Instruction limit % 280.84/39.86 % (309925)Termination phase: Saturation % 280.84/39.86 % (309925)Time elapsed: 0.177 s % 280.84/39.86 % (309925)Peak memory usage: 14 MB % 280.84/39.86 % (309925)Instructions burned: 263 (million) % 280.84/39.86 % (309927)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=2333049436:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/1368Mi) % 280.84/39.86 % (309927)Instruction limit reached! % 280.84/39.86 % (309927)------------------------------ % 280.84/39.86 % (309927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.84/39.86 % (309927)CaDiCaL version: 2.1.3 % 280.84/39.86 % (309927)Termination reason: Instruction limit % 280.84/39.86 % (309927)Termination phase: Saturation % 280.84/39.86 % (309927)Time elapsed: 0.801 s % 280.84/39.86 % (309927)Peak memory usage: 22 MB % 280.84/39.86 % (309927)Instructions burned: 1369 (million) % 280.84/39.86 % (309929)ott-21_1_sil=16000:si=on:fs=off:random_seed=3137130885:i=360:av=off:fsr=off:rtra=on_2767 on theBenchmark for (2767ds/360Mi) % 280.84/39.86 % (309929)Instruction limit reached! % 280.84/39.86 % (309929)------------------------------ % 280.84/39.86 % (309929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.84/39.86 % (309929)CaDiCaL version: 2.1.3 % 280.84/39.86 % (309929)Termination reason: Instruction limit % 280.84/39.86 % (309929)Termination phase: Saturation % 280.84/39.86 % (309929)Time elapsed: 0.179 s % 280.84/39.86 % (309929)Peak memory usage: 13 MB % 280.84/39.86 % (309929)Instructions burned: 360 (million) % 280.84/39.86 % (309931)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=840726947:i=954:bd=all:rtra=on_2765 on theBenchmark for (2765ds/954Mi) % 280.84/39.86 % (309931)Instruction limit reached! % 280.84/39.86 % (309931)------------------------------ % 280.84/39.86 % (309931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.84/39.86 % (309931)CaDiCaL version: 2.1.3 % 280.84/39.86 % (309931)Termination reason: Instruction limit % 280.84/39.86 % (309931)Termination phase: Saturation % 280.84/39.86 % (309931)Time elapsed: 0.638 s % 280.84/39.86 % (309931)Peak memory usage: 16 MB % 280.84/39.86 % (309931)Instructions burned: 954 (million) % 280.84/39.86 % (309933)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=490026033:fmbsr=1.3:i=1730:ins=25:rtra=on_2759 on theBenchmark for (2759ds/1730Mi) % 280.84/39.86 % Exception at run slice level % 280.84/39.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 280.84/39.86 % (309935)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1923446385:i=2358:rtra=on_2758 on theBenchmark for (2758ds/2358Mi) % 280.84/39.86 % (309935)Instruction limit reached! % 280.84/39.86 % (309935)------------------------------ % 280.84/39.86 % (309935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.84/39.86 % (309935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (309935)CaDiCaL version: 2.1.3 % 300.01/42.53 % (309935)Termination reason: Instruction limit % 300.01/42.53 % (309935)Termination phase: Saturation % 300.01/42.53 % (309935)Time elapsed: 1.521 s % 300.01/42.53 % (309935)Peak memory usage: 31 MB % 300.01/42.53 % (309935)Instructions burned: 2359 (million) % 300.01/42.53 % (309937)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2640181238:i=1778:ins=1:rtra=on_2743 on theBenchmark for (2743ds/1778Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (309939)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=3009153692:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1384Mi) % 300.01/42.53 % (309939)Instruction limit reached! % 300.01/42.53 % (309939)------------------------------ % 300.01/42.53 % (309939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (309939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (309939)CaDiCaL version: 2.1.3 % 300.01/42.53 % (309939)Termination reason: Instruction limit % 300.01/42.53 % (309939)Termination phase: Saturation % 300.01/42.53 % (309939)Time elapsed: 0.842 s % 300.01/42.53 % (309939)Peak memory usage: 25 MB % 300.01/42.53 % (309939)Instructions burned: 1385 (million) % 300.01/42.53 % (309941)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3991693425:i=1758:kws=inv_precedence:fsr=off:rtra=on_2734 on theBenchmark for (2734ds/1758Mi) % 300.01/42.53 % (309891)Instruction limit reached! % 300.01/42.53 % (309891)------------------------------ % 300.01/42.53 % (309891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (309891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (309891)CaDiCaL version: 2.1.3 % 300.01/42.53 % (309891)Termination reason: Instruction limit % 300.01/42.53 % (309891)Termination phase: Saturation % 300.01/42.53 % (309891)Time elapsed: 10.632 s % 300.01/42.53 % (309891)Peak memory usage: 149 MB % 300.01/42.53 % (309891)Instructions burned: 17628 (million) % 300.01/42.53 % (309943)fmb+10_1_sil=64000:si=on:random_seed=1936556733:i=44122:nm=2:rtra=on:gsp=on_2730 on theBenchmark for (2730ds/44122Mi) % 300.01/42.53 % (309943)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (309945)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4137828011:i=19030:nm=5:rtra=on_2729 on theBenchmark for (2729ds/19030Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (309947)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=880956435:fmbsr=1.7:i=1840:rtra=on_2729 on theBenchmark for (2729ds/1840Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (309949)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2181316632:i=10262:rtra=on_2729 on theBenchmark for (2729ds/10262Mi) % 300.01/42.53 % (309941)Instruction limit reached! % 300.01/42.53 % (309941)------------------------------ % 300.01/42.53 % (309941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (309941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (309941)CaDiCaL version: 2.1.3 % 300.01/42.53 % (309941)Termination reason: Instruction limit % 300.01/42.53 % (309941)Termination phase: Saturation % 300.01/42.53 % (309941)Time elapsed: 0.981 s % 300.01/42.53 % (309941)Peak memory usage: 25 MB % 300.01/42.53 % (309941)Instructions burned: 1759 (million) % 300.01/42.53 % (309951)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3375630570:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2724 on theBenchmark for (2724ds/2944Mi) % 300.01/42.53 % (309951)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.01/42.53 % (309951)Instruction limit reached! % 300.01/42.53 % (309951)------------------------------ % 300.01/42.53 % (309951)Version: Vampire 5.0.1 (Release build, commit 5ef7c267 % 300.01/42.53 Terminated % 300.01/42.53 % Vampire exiting %------------------------------------------------------------------------------