%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV593_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 : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:05 PM UTC 2026 % Result : Timeout 300.19s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV593_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.08/0.24 % Computer : n007.cluster.edu % 0.08/0.24 % Model : x86_64 x86_64 % 0.08/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.24 % Memory : 8046.5625MB % 0.08/0.24 % OS : Linux 6.8.0-71-generic % 0.08/0.24 % CPULimit : 300 % 0.08/0.24 % WCLimit : 300 % 0.08/0.24 % DateTime : Mon Sep 28 11:57:25 UTC 2026 % 0.08/0.24 % CPUTime : % 0.08/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.23/0.29 Running first-order model finding % 0.23/0.29 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 % 8.03/1.58 % (2344464)Will run a generic schedule for satisfiability detection. % 8.03/1.58 % (2344472)dis+10_1_sil=32000:sp=arity:random_seed=94655638:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.03/1.58 % (2344470)% WARNING: option uhcvi not known. % 8.03/1.58 % (2344470)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=528751214:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.03/1.58 % (2344469)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1143210741_2999 on theBenchmark for (2999ds/0Mi) % 8.03/1.58 % (2344473)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3780786938:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.03/1.58 % (2344471)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1711277453:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.03/1.58 % (2344474)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=112288366:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.03/1.58 % (2344475)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2291080164:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.03/1.58 % Exception at run slice level % 8.03/1.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.03/1.58 % (2344472)Instruction limit reached! % 8.03/1.58 % (2344472)------------------------------ % 8.03/1.58 % (2344472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.58 % (2344472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.58 % (2344472)CaDiCaL version: 2.1.3 % 8.03/1.58 % (2344472)Termination reason: Instruction limit % 8.03/1.58 % (2344472)Termination phase: Saturation % 8.03/1.58 % (2344472)Time elapsed: 0.058 s % 8.03/1.58 % (2344472)Peak memory usage: 12 MB % 8.03/1.58 % (2344472)Instructions burned: 105 (million) % 8.03/1.58 % (2344483)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3038705941:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.03/1.58 % Exception at run slice level % 8.03/1.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.03/1.58 % (2344484)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4260247815:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.03/1.58 % (2344486)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=1986588062:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.03/1.58 % (2344473)Instruction limit reached! % 8.03/1.58 % (2344473)------------------------------ % 8.03/1.58 % (2344473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.58 % (2344473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.58 % (2344473)CaDiCaL version: 2.1.3 % 8.03/1.58 % (2344473)Termination reason: Instruction limit % 8.03/1.58 % (2344473)Termination phase: Saturation % 8.03/1.58 % (2344473)Time elapsed: 0.118 s % 8.03/1.58 % (2344473)Peak memory usage: 12 MB % 8.03/1.58 % (2344473)Instructions burned: 116 (million) % 8.03/1.58 % (2344474)Instruction limit reached! % 8.03/1.58 % (2344474)------------------------------ % 8.03/1.58 % (2344474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.58 % (2344474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.58 % (2344474)CaDiCaL version: 2.1.3 % 8.03/1.58 % (2344474)Termination reason: Instruction limit % 8.03/1.58 % (2344474)Termination phase: Saturation % 8.03/1.58 % (2344474)Time elapsed: 0.132 s % 8.03/1.58 % (2344474)Peak memory usage: 13 MB % 8.03/1.58 % (2344474)Instructions burned: 132 (million) % 8.03/1.58 % (2344475)Instruction limit reached! % 8.03/1.58 % (2344475)------------------------------ % 8.03/1.58 % (2344475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.58 % (2344475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.58 % (2344475)CaDiCaL version: 2.1.3 % 8.03/1.58 % (2344475)Termination reason: Instruction limit % 8.03/1.58 % (2344475)Termination phase: Saturation % 8.03/1.58 % (2344475)Time elapsed: 0.140 s % 8.03/1.58 % (2344475)Peak memory usage: 12 MB % 8.03/1.58 % (2344475)Instructions burned: 161 (million) % 8.03/1.58 % (2344489)ott-21_1_sil=16000:fs=off:random_seed=425000125:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.03/1.58 % (2344484)Instruction limit reached! % 20.44/3.30 % (2344484)------------------------------ % 20.44/3.30 % (2344484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.44/3.30 % (2344484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.44/3.30 % (2344484)CaDiCaL version: 2.1.3 % 20.44/3.30 % (2344484)Termination reason: Instruction limit % 20.44/3.30 % (2344484)Termination phase: Saturation % 20.44/3.30 % (2344484)Time elapsed: 0.072 s % 20.44/3.30 % (2344484)Peak memory usage: 13 MB % 20.44/3.30 % (2344484)Instructions burned: 131 (million) % 20.44/3.30 % (2344490)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=665498514:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 20.44/3.30 % (2344491)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1390179114:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 20.44/3.30 % Exception at run slice level % 20.44/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.44/3.30 % (2344493)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=208030822:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 20.44/3.30 % (2344496)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=244282930:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 20.44/3.30 % Exception at run slice level % 20.44/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.44/3.30 % (2344489)Instruction limit reached! % 20.44/3.30 % (2344489)------------------------------ % 20.44/3.30 % (2344489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.44/3.30 % (2344489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.44/3.30 % (2344489)CaDiCaL version: 2.1.3 % 20.44/3.30 % (2344489)Termination reason: Instruction limit % 20.44/3.30 % (2344489)Termination phase: Saturation % 20.44/3.30 % (2344489)Time elapsed: 0.046 s % 20.44/3.30 % (2344489)Peak memory usage: 12 MB % 20.44/3.30 % (2344489)Instructions burned: 186 (million) % 20.44/3.30 % (2344500)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=127204585:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.44/3.30 % (2344499)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=3587259628:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 20.44/3.30 % (2344490)Instruction limit reached! % 20.44/3.30 % (2344490)------------------------------ % 20.44/3.30 % (2344490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.44/3.30 % (2344490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.44/3.30 % (2344490)CaDiCaL version: 2.1.3 % 20.44/3.30 % (2344490)Termination reason: Instruction limit % 20.44/3.30 % (2344490)Termination phase: Saturation % 20.44/3.30 % (2344490)Time elapsed: 0.308 s % 20.44/3.30 % (2344490)Peak memory usage: 14 MB % 20.44/3.30 % (2344490)Instructions burned: 479 (million) % 20.44/3.30 % (2344500)Instruction limit reached! % 20.44/3.30 % (2344500)------------------------------ % 20.44/3.30 % (2344500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.44/3.30 % (2344500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.44/3.30 % (2344500)CaDiCaL version: 2.1.3 % 20.44/3.30 % (2344500)Termination reason: Instruction limit % 20.44/3.30 % (2344500)Termination phase: Saturation % 20.44/3.30 % (2344500)Time elapsed: 0.268 s % 20.44/3.30 % (2344500)Peak memory usage: 19 MB % 20.44/3.30 % (2344500)Instructions burned: 880 (million) % 20.44/3.30 % (2344504)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1610306680:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 20.44/3.30 % (2344486)Instruction limit reached! % 20.44/3.30 % (2344486)------------------------------ % 20.44/3.30 % (2344486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.44/3.30 % (2344486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.44/3.30 % (2344486)CaDiCaL version: 2.1.3 % 20.44/3.30 % (2344486)Termination reason: Instruction limit % 20.44/3.30 % (2344486)Termination phase: Saturation % 20.44/3.30 % (2344486)Time elapsed: 0.396 s % 20.44/3.30 % (2344486)Peak memory usage: 16 MB % 20.44/3.30 % (2344486)Instructions burned: 684 (million) % 20.44/3.30 % Exception at run slice level % 20.44/3.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.44/3.30 % (2344503)fmb+10_1_sil=64000:random_seed=392307411:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 77.24/11.21 % (2344503)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 77.24/11.21 % Exception at run slice level % 77.24/11.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 77.24/11.21 % (2344507)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=661499701:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 77.24/11.21 % (2344506)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1525472427:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 77.24/11.21 % Exception at run slice level % 77.24/11.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 77.24/11.21 % (2344509)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1033910797:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 77.24/11.21 % (2344509)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 77.24/11.21 % (2344512)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3312279800:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 77.24/11.21 % Exception at run slice level % 77.24/11.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 77.24/11.21 % (2344499)Instruction limit reached! % 77.24/11.21 % (2344499)------------------------------ % 77.24/11.21 % (2344499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.24/11.21 % (2344499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.24/11.21 % (2344499)CaDiCaL version: 2.1.3 % 77.24/11.21 % (2344499)Termination reason: Instruction limit % 77.24/11.21 % (2344499)Termination phase: Saturation % 77.24/11.21 % (2344499)Time elapsed: 0.332 s % 77.24/11.21 % (2344499)Peak memory usage: 16 MB % 77.24/11.21 % (2344499)Instructions burned: 693 (million) % 77.24/11.21 % (2344515)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=10954344:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 77.24/11.21 % Exception at run slice level % 77.24/11.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 77.24/11.21 % (2344516)ott-2_1_sil=16000:newcnf=on:random_seed=1022530442:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 77.24/11.21 % (2344518)ott+10_1_sil=32000:tgt=ground:random_seed=4126092643:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 77.24/11.21 % (2344493)Instruction limit reached! % 77.24/11.21 % (2344493)------------------------------ % 77.24/11.21 % (2344493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.24/11.21 % (2344493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.24/11.21 % (2344493)CaDiCaL version: 2.1.3 % 77.24/11.21 % (2344493)Termination reason: Instruction limit % 77.24/11.21 % (2344493)Termination phase: Saturation % 77.24/11.21 % (2344493)Time elapsed: 0.639 s % 77.24/11.21 % (2344493)Peak memory usage: 17 MB % 77.24/11.21 % (2344493)Instructions burned: 1180 (million) % 77.24/11.21 % (2344521)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=733730080:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 77.24/11.21 % Exception at run slice level % 77.24/11.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 77.24/11.21 % (2344523)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2491615537:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 77.24/11.21 % (2344516)Instruction limit reached! % 77.24/11.21 % (2344516)------------------------------ % 77.24/11.21 % (2344516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.24/11.21 % (2344516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.24/11.21 % (2344516)CaDiCaL version: 2.1.3 % 77.24/11.21 % (2344516)Termination reason: Instruction limit % 77.24/11.21 % (2344516)Termination phase: Saturation % 77.24/11.21 % (2344516)Time elapsed: 0.507 s % 77.24/11.21 % (2344516)Peak memory usage: 15 MB % 77.24/11.21 % (2344516)Instructions burned: 869 (million) % 77.24/11.21 % (2344525)dis+21_1_sil=32000:sas=cadical:random_seed=548892308:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 77.24/11.21 % (2344509)Instruction limit reached! % 77.24/11.21 % (2344509)------------------------------ % 77.24/11.21 % (2344509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.74/16.92 % (2344509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.74/16.92 % (2344509)CaDiCaL version: 2.1.3 % 117.74/16.92 % (2344509)Termination reason: Instruction limit % 117.74/16.92 % (2344509)Termination phase: Saturation % 117.74/16.92 % (2344509)Time elapsed: 0.709 s % 117.74/16.92 % (2344509)Peak memory usage: 25 MB % 117.74/16.92 % (2344509)Instructions burned: 1473 (million) % 117.74/16.92 % (2344527)ott+11_1_sil=16000:gs=on:random_seed=1236233427:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 117.74/16.92 % (2344507)Instruction limit reached! % 117.74/16.92 % (2344507)------------------------------ % 117.74/16.92 % (2344507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.74/16.92 % (2344507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.74/16.92 % (2344507)CaDiCaL version: 2.1.3 % 117.74/16.92 % (2344507)Termination reason: Instruction limit % 117.74/16.92 % (2344507)Termination phase: Saturation % 117.74/16.92 % (2344507)Time elapsed: 1.395 s % 117.74/16.92 % (2344507)Peak memory usage: 27 MB % 117.74/16.92 % (2344507)Instructions burned: 5136 (million) % 117.74/16.92 % (2344529)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=97504857:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 117.74/16.92 % Exception at run slice level % 117.74/16.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.74/16.92 % (2344531)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=446202293:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 117.74/16.92 % (2344527)Instruction limit reached! % 117.74/16.92 % (2344527)------------------------------ % 117.74/16.92 % (2344527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.74/16.92 % (2344527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.74/16.92 % (2344527)CaDiCaL version: 2.1.3 % 117.74/16.92 % (2344527)Termination reason: Instruction limit % 117.74/16.92 % (2344527)Termination phase: Saturation % 117.74/16.92 % (2344527)Time elapsed: 0.911 s % 117.74/16.92 % (2344527)Peak memory usage: 16 MB % 117.74/16.92 % (2344527)Instructions burned: 2252 (million) % 117.74/16.92 % (2344533)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3403393174:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 117.74/16.92 % (2344531)Instruction limit reached! % 117.74/16.92 % (2344531)------------------------------ % 117.74/16.92 % (2344531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.74/16.92 % (2344531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.74/16.92 % (2344531)CaDiCaL version: 2.1.3 % 117.74/16.92 % (2344531)Termination reason: Instruction limit % 117.74/16.92 % (2344531)Termination phase: Saturation % 117.74/16.92 % (2344531)Time elapsed: 0.946 s % 117.74/16.92 % (2344531)Peak memory usage: 27 MB % 117.74/16.92 % (2344531)Instructions burned: 4594 (million) % 117.74/16.92 % (2344523)Instruction limit reached! % 117.74/16.92 % (2344523)------------------------------ % 117.74/16.92 % (2344523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.74/16.92 % (2344523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.74/16.92 % (2344523)CaDiCaL version: 2.1.3 % 117.74/16.92 % (2344523)Termination reason: Instruction limit % 117.74/16.92 % (2344523)Termination phase: Saturation % 117.74/16.92 % (2344523)Time elapsed: 2.012 s % 117.74/16.92 % (2344523)Peak memory usage: 26 MB % 117.74/16.92 % (2344523)Instructions burned: 3513 (million) % 117.74/16.92 % (2344535)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2714552105:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 117.74/16.92 % (2344536)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2685831960:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 117.74/16.92 % Exception at run slice level % 117.74/16.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.74/16.92 % (2344539)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1071824199:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 117.74/16.92 % Exception at run slice level % 117.74/16.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 117.74/16.92 % (2344541)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3101478024:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 117.74/16.92 % Exception at run slice level % 150.28/21.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 150.28/21.58 % (2344543)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2074001137:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 150.28/21.58 % (2344525)Instruction limit reached! % 150.28/21.58 % (2344525)------------------------------ % 150.28/21.58 % (2344525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344525)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344525)Termination reason: Instruction limit % 150.28/21.58 % (2344525)Termination phase: Saturation % 150.28/21.58 % (2344525)Time elapsed: 2.116 s % 150.28/21.58 % (2344525)Peak memory usage: 26 MB % 150.28/21.58 % (2344525)Instructions burned: 3774 (million) % 150.28/21.58 % (2344545)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=776440066:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 150.28/21.58 % (2344518)Instruction limit reached! % 150.28/21.58 % (2344518)------------------------------ % 150.28/21.58 % (2344518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344518)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344518)Termination reason: Instruction limit % 150.28/21.58 % (2344518)Termination phase: Saturation % 150.28/21.58 % (2344518)Time elapsed: 2.878 s % 150.28/21.58 % (2344518)Peak memory usage: 26 MB % 150.28/21.58 % (2344518)Instructions burned: 5115 (million) % 150.28/21.58 % (2344547)dis+10_16:1_sil=16000:random_seed=815837044:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 150.28/21.58 % (2344535)Instruction limit reached! % 150.28/21.58 % (2344535)------------------------------ % 150.28/21.58 % (2344535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344535)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344535)Termination reason: Instruction limit % 150.28/21.58 % (2344535)Termination phase: Saturation % 150.28/21.58 % (2344535)Time elapsed: 1.495 s % 150.28/21.58 % (2344535)Peak memory usage: 40 MB % 150.28/21.58 % (2344535)Instructions burned: 5212 (million) % 150.28/21.58 % (2344549)ott-3_8_sil=64000:random_seed=934085054:i=20139:bs=on_2955 on theBenchmark for (2955ds/20139Mi) % 150.28/21.58 % (2344545)Instruction limit reached! % 150.28/21.58 % (2344545)------------------------------ % 150.28/21.58 % (2344545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344545)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344545)Termination reason: Instruction limit % 150.28/21.58 % (2344545)Termination phase: Saturation % 150.28/21.58 % (2344545)Time elapsed: 3.939 s % 150.28/21.58 % (2344545)Peak memory usage: 31 MB % 150.28/21.58 % (2344545)Instructions burned: 8173 (million) % 150.28/21.58 % (2344551)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1170720381:fmbsr=2:i=32576_2927 on theBenchmark for (2927ds/32576Mi) % 150.28/21.58 % Exception at run slice level % 150.28/21.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 150.28/21.58 % (2344553)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2261660976:i=11404_2927 on theBenchmark for (2927ds/11404Mi) % 150.28/21.58 % (2344547)Instruction limit reached! % 150.28/21.58 % (2344547)------------------------------ % 150.28/21.58 % (2344547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344547)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344547)Termination reason: Instruction limit % 150.28/21.58 % (2344547)Termination phase: Saturation % 150.28/21.58 % (2344547)Time elapsed: 4.342 s % 150.28/21.58 % (2344547)Peak memory usage: 43 MB % 150.28/21.58 % (2344547)Instructions burned: 9156 (million) % 150.28/21.58 % (2344555)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3665444632:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 150.28/21.58 % (2344549)Instruction limit reached! % 150.28/21.58 % (2344549)------------------------------ % 150.28/21.58 % (2344549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.28/21.58 % (2344549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.28/21.58 % (2344549)CaDiCaL version: 2.1.3 % 150.28/21.58 % (2344549)Termination reason: Instruction limit % 165.28/23.64 % (2344549)Termination phase: Saturation % 165.28/23.64 % (2344549)Time elapsed: 6.452 s % 165.28/23.64 % (2344549)Peak memory usage: 66 MB % 165.28/23.64 % (2344549)Instructions burned: 20143 (million) % 165.28/23.64 % (2344557)dis+33_16_sil=32000:sac=on:random_seed=494636092:i=15851:nm=0_2890 on theBenchmark for (2890ds/15851Mi) % 165.28/23.64 % (2344553)Instruction limit reached! % 165.28/23.64 % (2344553)------------------------------ % 165.28/23.64 % (2344553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.28/23.64 % (2344553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.28/23.64 % (2344553)CaDiCaL version: 2.1.3 % 165.28/23.64 % (2344553)Termination reason: Instruction limit % 165.28/23.64 % (2344553)Termination phase: Saturation % 165.28/23.64 % (2344553)Time elapsed: 6.151 s % 165.28/23.64 % (2344553)Peak memory usage: 45 MB % 165.28/23.64 % (2344553)Instructions burned: 11404 (million) % 165.28/23.64 % (2344559)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1348553116:avsq=on:i=17627:add=on:amm=off_2865 on theBenchmark for (2865ds/17627Mi) % 165.28/23.64 % (2344557)Instruction limit reached! % 165.28/23.64 % (2344557)------------------------------ % 165.28/23.64 % (2344557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.28/23.64 % (2344557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.28/23.64 % (2344557)CaDiCaL version: 2.1.3 % 165.28/23.64 % (2344557)Termination reason: Instruction limit % 165.28/23.64 % (2344557)Termination phase: Saturation % 165.28/23.64 % (2344557)Time elapsed: 4.288 s % 165.28/23.64 % (2344557)Peak memory usage: 63 MB % 165.28/23.64 % (2344557)Instructions burned: 15854 (million) % 165.28/23.64 % (2344561)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2411209097:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 165.28/23.64 % (2344555)Instruction limit reached! % 165.28/23.64 % (2344555)------------------------------ % 165.28/23.64 % (2344555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.28/23.64 % (2344555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.28/23.64 % (2344555)CaDiCaL version: 2.1.3 % 165.28/23.64 % (2344555)Termination reason: Instruction limit % 165.28/23.64 % (2344555)Termination phase: Saturation % 165.28/23.64 % (2344555)Time elapsed: 7.616 s % 165.28/23.64 % (2344555)Peak memory usage: 45 MB % 165.28/23.64 % (2344555)Instructions burned: 14134 (million) % 165.28/23.64 % (2344563)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3577806049:i=26857:ins=20_2844 on theBenchmark for (2844ds/26857Mi) % 165.28/23.64 % Exception at run slice level % 165.28/23.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.28/23.64 % (2344565)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3396747212:i=28120:bs=on:fsr=off_2844 on theBenchmark for (2844ds/28120Mi) % 165.28/23.64 % (2344533)Instruction limit reached! % 165.28/23.64 % (2344533)------------------------------ % 165.28/23.64 % (2344533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.28/23.64 % (2344533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.28/23.64 % (2344533)CaDiCaL version: 2.1.3 % 165.28/23.64 % (2344533)Termination reason: Instruction limit % 165.28/23.64 % (2344533)Termination phase: Saturation % 165.28/23.64 % (2344533)Time elapsed: 14.268 s % 165.28/23.64 % (2344533)Peak memory usage: 213 MB % 165.28/23.64 % (2344533)Instructions burned: 29341 (million) % 165.28/23.64 % (2344567)fmb+10_1_sil=256000:fmbss=7:random_seed=1786820166:fmbsr=1.6:i=182295_2834 on theBenchmark for (2834ds/182295Mi) % 165.28/23.64 % Exception at run slice level % 165.28/23.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.28/23.64 % (2344569)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2465883084:i=44625:gsp=on_2834 on theBenchmark for (2834ds/44625Mi) % 165.28/23.64 % (2344569)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 165.28/23.64 % Exception at run slice level % 165.28/23.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.28/23.64 % (2344571)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1967234774:i=160505_2834 on theBenchmark for (2834ds/160505Mi) % 165.28/23.64 % Exception at run slice level % 165.28/23.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.28/23.64 % (2344573)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1857856695:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 195.03/27.91 % Exception at run slice level % 195.03/27.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.03/27.91 % (2344575)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1304767542:fmbsr=2:i=185024:ins=7_2833 on theBenchmark for (2833ds/185024Mi) % 195.03/27.91 % Exception at run slice level % 195.03/27.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.03/27.91 % (2344577)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3158583627:rtra=on_2833 on theBenchmark for (2833ds/0Mi) % 195.03/27.91 % Exception at run slice level % 195.03/27.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.03/27.91 % (2344579)% WARNING: option uhcvi not known. % 195.03/27.91 % (2344579)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2116535232:i=271062:add=off:rtra=on:rawr=on_2833 on theBenchmark for (2833ds/271062Mi) % 195.03/27.91 % (2344543)Instruction limit reached! % 195.03/27.91 % (2344543)------------------------------ % 195.03/27.91 % (2344543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.03/27.91 % (2344543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.03/27.91 % (2344543)CaDiCaL version: 2.1.3 % 195.03/27.91 % (2344543)Termination reason: Instruction limit % 195.03/27.91 % (2344543)Termination phase: Saturation % 195.03/27.91 % (2344543)Time elapsed: 14.706 s % 195.03/27.91 % (2344543)Peak memory usage: 109 MB % 195.03/27.91 % (2344543)Instructions burned: 22565 (million) % 195.03/27.91 % (2344581)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2884924979:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 195.03/27.91 % (2344559)Instruction limit reached! % 195.03/27.91 % (2344559)------------------------------ % 195.03/27.91 % (2344559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.03/27.91 % (2344559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.03/27.91 % (2344559)CaDiCaL version: 2.1.3 % 195.03/27.91 % (2344559)Termination reason: Instruction limit % 195.03/27.91 % (2344559)Termination phase: Saturation % 195.03/27.91 % (2344559)Time elapsed: 7.325 s % 195.03/27.91 % (2344559)Peak memory usage: 23 MB % 195.03/27.91 % (2344559)Instructions burned: 17627 (million) % 195.03/27.91 % (2344583)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2724100237:i=206:fgj=on:rtra=on_2792 on theBenchmark for (2792ds/206Mi) % 195.03/27.91 % (2344583)Instruction limit reached! % 195.03/27.91 % (2344583)------------------------------ % 195.03/27.91 % (2344583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.03/27.91 % (2344583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.03/27.91 % (2344583)CaDiCaL version: 2.1.3 % 195.03/27.91 % (2344583)Termination reason: Instruction limit % 195.03/27.91 % (2344583)Termination phase: Saturation % 195.03/27.91 % (2344583)Time elapsed: 0.128 s % 195.03/27.91 % (2344583)Peak memory usage: 13 MB % 195.03/27.91 % (2344583)Instructions burned: 208 (million) % 195.03/27.91 % (2344585)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2426370189:i=232:rtra=on_2790 on theBenchmark for (2790ds/232Mi) % 195.03/27.91 % (2344585)Instruction limit reached! % 195.03/27.91 % (2344585)------------------------------ % 195.03/27.91 % (2344585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.03/27.91 % (2344585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.03/27.91 % (2344585)CaDiCaL version: 2.1.3 % 195.03/27.91 % (2344585)Termination reason: Instruction limit % 195.03/27.91 % (2344585)Termination phase: Saturation % 195.03/27.91 % (2344585)Time elapsed: 0.147 s % 195.03/27.91 % (2344585)Peak memory usage: 13 MB % 195.03/27.91 % (2344585)Instructions burned: 233 (million) % 195.03/27.91 % (2344587)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1247332678:i=262:rtra=on_2789 on theBenchmark for (2789ds/262Mi) % 195.03/27.91 % (2344587)Instruction limit reached! % 195.03/27.91 % (2344587)------------------------------ % 195.03/27.91 % (2344587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.03/27.91 % (2344587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.03/27.91 % (2344587)CaDiCaL version: 2.1.3 % 195.03/27.91 % (2344587)Termination reason: Instruction limit % 195.03/27.91 % (2344587)Termination phase: Saturation % 230.19/33.00 % (2344587)Time elapsed: 0.155 s % 230.19/33.00 % (2344587)Peak memory usage: 14 MB % 230.19/33.00 % (2344587)Instructions burned: 263 (million) % 230.19/33.00 % (2344589)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2384868042:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2787 on theBenchmark for (2787ds/318Mi) % 230.19/33.00 % (2344589)Instruction limit reached! % 230.19/33.00 % (2344589)------------------------------ % 230.19/33.00 % (2344589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.19/33.00 % (2344589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.19/33.00 % (2344589)CaDiCaL version: 2.1.3 % 230.19/33.00 % (2344589)Termination reason: Instruction limit % 230.19/33.00 % (2344589)Termination phase: Saturation % 230.19/33.00 % (2344589)Time elapsed: 0.165 s % 230.19/33.00 % (2344589)Peak memory usage: 13 MB % 230.19/33.00 % (2344589)Instructions burned: 319 (million) % 230.19/33.00 % (2344591)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4214932887:i=1428:nm=2:rtra=on_2785 on theBenchmark for (2785ds/1428Mi) % 230.19/33.00 % Exception at run slice level % 230.19/33.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 230.19/33.00 % (2344593)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2682876742:i=262:bd=preordered:rtra=on:fsd=on_2785 on theBenchmark for (2785ds/262Mi) % 230.19/33.00 % (2344593)Instruction limit reached! % 230.19/33.00 % (2344593)------------------------------ % 230.19/33.00 % (2344593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.19/33.00 % (2344593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.19/33.00 % (2344593)CaDiCaL version: 2.1.3 % 230.19/33.00 % (2344593)Termination reason: Instruction limit % 230.19/33.00 % (2344593)Termination phase: Saturation % 230.19/33.00 % (2344593)Time elapsed: 0.169 s % 230.19/33.00 % (2344593)Peak memory usage: 15 MB % 230.19/33.00 % (2344593)Instructions burned: 262 (million) % 230.19/33.00 % (2344595)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=3376375063:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/1368Mi) % 230.19/33.00 % (2344595)Instruction limit reached! % 230.19/33.00 % (2344595)------------------------------ % 230.19/33.00 % (2344595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.19/33.00 % (2344595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.19/33.00 % (2344595)CaDiCaL version: 2.1.3 % 230.19/33.00 % (2344595)Termination reason: Instruction limit % 230.19/33.00 % (2344595)Termination phase: Saturation % 230.19/33.00 % (2344595)Time elapsed: 0.794 s % 230.19/33.00 % (2344595)Peak memory usage: 18 MB % 230.19/33.00 % (2344595)Instructions burned: 1368 (million) % 230.19/33.00 % (2344597)ott-21_1_sil=16000:si=on:fs=off:random_seed=388878043:i=360:av=off:fsr=off:rtra=on_2775 on theBenchmark for (2775ds/360Mi) % 230.19/33.00 % (2344597)Instruction limit reached! % 230.19/33.00 % (2344597)------------------------------ % 230.19/33.00 % (2344597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.19/33.00 % (2344597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.19/33.00 % (2344597)CaDiCaL version: 2.1.3 % 230.19/33.00 % (2344597)Termination reason: Instruction limit % 230.19/33.00 % (2344597)Termination phase: Saturation % 230.19/33.00 % (2344597)Time elapsed: 0.163 s % 230.19/33.00 % (2344597)Peak memory usage: 13 MB % 230.19/33.00 % (2344597)Instructions burned: 362 (million) % 230.19/33.00 % (2344599)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3191809439:i=954:bd=all:rtra=on_2773 on theBenchmark for (2773ds/954Mi) % 230.19/33.00 % (2344599)Instruction limit reached! % 230.19/33.00 % (2344599)------------------------------ % 230.19/33.00 % (2344599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.19/33.00 % (2344599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.19/33.00 % (2344599)CaDiCaL version: 2.1.3 % 230.19/33.00 % (2344599)Termination reason: Instruction limit % 230.19/33.00 % (2344599)Termination phase: Saturation % 230.19/33.00 % (2344599)Time elapsed: 0.614 s % 230.19/33.00 % (2344599)Peak memory usage: 16 MB % 230.19/33.00 % (2344599)Instructions burned: 955 (million) % 230.19/33.00 % (2344601)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=345210213:fmbsr=1.3:i=1730:ins=25:rtra=on_2766 on theBenchmark for (2766ds/1730Mi) % 230.19/33.00 % Exception at run slice level % 230.19/33.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.95/38.38 % (2344603)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1924153085:i=2358:rtra=on_2766 on theBenchmark for (2766ds/2358Mi) % 246.95/38.38 % (2344603)Instruction limit reached! % 246.95/38.38 % (2344603)------------------------------ % 246.95/38.38 % (2344603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.95/38.38 % (2344603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.95/38.38 % (2344603)CaDiCaL version: 2.1.3 % 246.95/38.38 % (2344603)Termination reason: Instruction limit % 246.95/38.38 % (2344603)Termination phase: Saturation % 246.95/38.38 % (2344603)Time elapsed: 1.474 s % 246.95/38.38 % (2344603)Peak memory usage: 22 MB % 246.95/38.38 % (2344603)Instructions burned: 2359 (million) % 246.95/38.38 % (2344605)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3130691491:i=1778:ins=1:rtra=on_2751 on theBenchmark for (2751ds/1778Mi) % 246.95/38.38 % Exception at run slice level % 246.95/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.95/38.38 % (2344607)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=3297923444:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/1384Mi) % 246.95/38.38 % (2344607)Instruction limit reached! % 246.95/38.38 % (2344607)------------------------------ % 246.95/38.38 % (2344607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.95/38.38 % (2344607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.95/38.38 % (2344607)CaDiCaL version: 2.1.3 % 246.95/38.38 % (2344607)Termination reason: Instruction limit % 246.95/38.38 % (2344607)Termination phase: Saturation % 246.95/38.38 % (2344607)Time elapsed: 0.795 s % 246.95/38.38 % (2344607)Peak memory usage: 19 MB % 246.95/38.38 % (2344607)Instructions burned: 1385 (million) % 246.95/38.38 % (2344609)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3472574540:i=1758:kws=inv_precedence:fsr=off:rtra=on_2743 on theBenchmark for (2743ds/1758Mi) % 246.95/38.38 % (2344609)Instruction limit reached! % 246.95/38.38 % (2344609)------------------------------ % 246.95/38.38 % (2344609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.95/38.38 % (2344609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.95/38.38 % (2344609)CaDiCaL version: 2.1.3 % 246.95/38.38 % (2344609)Termination reason: Instruction limit % 246.95/38.38 % (2344609)Termination phase: Saturation % 246.95/38.38 % (2344609)Time elapsed: 1.041 s % 246.95/38.38 % (2344609)Peak memory usage: 25 MB % 246.95/38.38 % (2344609)Instructions burned: 1759 (million) % 246.95/38.38 % (2344611)fmb+10_1_sil=64000:si=on:random_seed=2533704861:i=44122:nm=2:rtra=on:gsp=on_2732 on theBenchmark for (2732ds/44122Mi) % 246.95/38.38 % (2344611)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 246.95/38.38 % Exception at run slice level % 246.95/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.95/38.38 % (2344613)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=974486016:i=19030:nm=5:rtra=on_2732 on theBenchmark for (2732ds/19030Mi) % 246.95/38.38 % Exception at run slice level % 246.95/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.95/38.38 % (2344615)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1423384422:fmbsr=1.7:i=1840:rtra=on_2732 on theBenchmark for (2732ds/1840Mi) % 246.95/38.38 % Exception at run slice level % 246.95/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.95/38.38 % (2344617)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2370800421:i=10262:rtra=on_2731 on theBenchmark for (2731ds/10262Mi) % 246.95/38.38 % (2344561)Instruction limit reached! % 246.95/38.38 % (2344561)------------------------------ % 246.95/38.38 % (2344561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.95/38.38 % (2344561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.95/38.38 % (2344561)CaDiCaL version: 2.1.3 % 246.95/38.38 % (2344561)Termination reason: Instruction limit % 246.95/38.38 % (2344561)Termination phase: Saturation % 246.95/38.38 % (2344561)Time elapsed: 12.372 s % 246.95/38.38 % (2344561)Peak memory usage: 201 MB % 246.95/38.38 % (2344561)Instructions burned: 53297 (million) % 300.19/42.63 % (2344619)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2930863679:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2723 on theBenchmark for (2723ds/2944Mi) % 300.19/42.63 % (2344619)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.19/42.63 % (2344619)Instruction limit reached! % 300.19/42.63 % (2344619)------------------------------ % 300.19/42.63 % (2344619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (2344619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (2344619)CaDiCaL version: 2.1.3 % 300.19/42.63 % (2344619)Termination reason: Instruction limit % 300.19/42.63 % (2344619)Termination phase: Saturation % 300.19/42.63 % (2344619)Time elapsed: 0.793 s % 300.19/42.63 % (2344619)Peak memory usage: 35 MB % 300.19/42.63 % (2344619)Instructions burned: 2947 (million) % 300.19/42.63 % (2344621)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2750120352:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 300.19/42.63 % Exception at run slice level % 300.19/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.19/42.64 % (2344623)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3665091761:fmbsr=2.30978:i=4348:rtra=on_2715 on theBenchmark for (2715ds/4348Mi) % 300.19/42.64 % Exception at run slice level % 300.19/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.19/42.64 % (2344625)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2558339277:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2715 on theBenchmark for (2715ds/1738Mi) % 300.19/42.64 % (2344625)Instruction limit reached! % 300.19/42.64 % (2344625)------------------------------ % 300.19/42.64 % (2344625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.64 % (2344625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.64 % (2344625)CaDiCaL version: 2.1.3 % 300.19/42.64 % (2344625)Termination reason: Instruction limit % 300.19/42.64 % (2344625)Termination phase: Saturation % 300.19/42.64 % (2344625)Time elapsed: 0.561 s % 300.19/42.64 % (2344625)Peak memory usage: 18 MB % 300.19/42.64 % (2344625)Instructions burned: 1738 (million) % 300.19/42.64 % (2344627)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1086643533:i=10228:av=off:rtra=on_2709 on theBenchmark for (2709ds/10228Mi) % 300.19/42.64 % (2344471)Instruction limit reached! % 300.19/42.64 % (2344471)------------------------------ % 300.19/42.64 % (2344471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.64 % (2344471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.64 % (2344471)CaDiCaL version: 2.1.3 % 300.19/42.64 % (2344471)Termination reason: Instruction limit % 300.19/42.64 % (2344471)Termination phase: Saturation % 300.19/42.64 % (2344471)Time elapsed: 31.718 s % 300.19/42.64 % (2344471)Peak memory usage: 49 MB % 300.19/42.64 % (2344471)Instructions burned: 88024 (million) % 300.19/42.64 % (2344629)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=837382661:i=108564:rtra=on_2682 on theBenchmark for (2682ds/108564Mi) % 300.19/42.64 % Exception at run slice level % 300.19/42.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.19/42.64 % (2344631)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2645734617:i=7024:aac=none:rtra=on_2681 on theBenchmark for (2681ds/7024Mi) % 300.19/42.64 % (2344627)Instruction limit reached! % 300.19/42.64 % (2344627)------------------------------ % 300.19/42.64 % (2344627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.64 % (2344627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.64 % (2344627)CaDiCaL version: 2.1.3 % 300.19/42.64 % (2344627)Termination reason: Instruction limit % 300.19/42.64 % (2344627)Termination phase: Saturation % 300.19/42.64 % (2344627)Time elapsed: 3.197 s % 300.19/42.64 % (2344627)Peak memory usage: 31 MB % 300.19/42.64 % (2344627)Instructions burned: 10229 (million) % 300.19/42.64 % (2344633)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1933283535:i=7546:rtra=on:amm=off_2677 on theBenchmark for (2677ds/7546Mi) % 300.19/42.64 % (2344617)Instruction limit reached! % 300.19/42.64 % (2344617)------------------------------ % 300.19/42.64 % (2344617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.64 % (2344617)Linked with Z3 4.14.0.0 % 300.19/42.64 Terminated % 300.19/42.64 % Vampire exiting % 300.19/42.64 Terminated %------------------------------------------------------------------------------