%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM026_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 : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 09:40:11 AM UTC 2026 % Result : Timeout 300.09s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : COM026_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 21:48:49 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.12 Running first-order model finding % 0.08/0.12 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 % 4.11/0.82 % (3815440)Will run a generic schedule for satisfiability detection. % 4.11/0.82 % (3815446)% WARNING: option uhcvi not known. % 4.11/0.82 % (3815445)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3332818602_2999 on theBenchmark for (2999ds/0Mi) % 4.11/0.82 % (3815446)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=652876280:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.11/0.82 % (3815447)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=953885104:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.11/0.82 % (3815448)dis+10_1_sil=32000:sp=arity:random_seed=2618766323:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.11/0.82 % (3815449)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2519720423:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.11/0.82 % (3815450)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2273586149:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.11/0.82 % (3815451)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2304955755:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.11/0.82 % Exception at run slice level % 4.11/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 4.11/0.82 % (3815459)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3890645170:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.11/0.82 % Exception at run slice level % 4.11/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 4.11/0.82 % (3815461)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2819513587:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.11/0.82 % (3815448)Instruction limit reached! % 4.11/0.82 % (3815448)------------------------------ % 4.11/0.82 % (3815448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.11/0.82 % (3815448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.11/0.82 % (3815448)CaDiCaL version: 2.1.3 % 4.11/0.82 % (3815448)Termination reason: Instruction limit % 4.11/0.82 % (3815448)Termination phase: Saturation % 4.11/0.82 % (3815448)Time elapsed: 0.033 s % 4.11/0.82 % (3815448)Peak memory usage: 12 MB % 4.11/0.82 % (3815448)Instructions burned: 104 (million) % 4.11/0.82 % (3815449)Instruction limit reached! % 4.11/0.82 % (3815449)------------------------------ % 4.11/0.82 % (3815449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.11/0.82 % (3815449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.11/0.82 % (3815449)CaDiCaL version: 2.1.3 % 4.11/0.82 % (3815449)Termination reason: Instruction limit % 4.11/0.82 % (3815449)Termination phase: Saturation % 4.11/0.82 % (3815449)Time elapsed: 0.037 s % 4.11/0.82 % (3815449)Peak memory usage: 12 MB % 4.11/0.82 % (3815449)Instructions burned: 119 (million) % 4.11/0.82 % (3815450)Instruction limit reached! % 4.11/0.82 % (3815450)------------------------------ % 4.11/0.82 % (3815450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.11/0.82 % (3815450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.11/0.82 % (3815450)CaDiCaL version: 2.1.3 % 4.11/0.82 % (3815450)Termination reason: Instruction limit % 4.11/0.82 % (3815450)Termination phase: Saturation % 4.11/0.82 % (3815450)Time elapsed: 0.042 s % 4.11/0.82 % (3815450)Peak memory usage: 13 MB % 4.11/0.82 % (3815450)Instructions burned: 132 (million) % 4.11/0.82 % (3815463)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=2665042692:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.11/0.82 % (3815464)ott-21_1_sil=16000:fs=off:random_seed=234411105:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.11/0.82 % (3815465)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1613651777:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 4.11/0.82 % (3815451)Instruction limit reached! % 4.11/0.82 % (3815451)------------------------------ % 4.11/0.82 % (3815451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.11/0.82 % (3815451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.11/0.82 % (3815451)CaDiCaL version: 2.1.3 % 4.11/0.82 % (3815451)Termination reason: Instruction limit % 4.11/0.82 % (3815451)Termination phase: Saturation % 11.62/2.00 % (3815451)Time elapsed: 0.056 s % 11.62/2.00 % (3815451)Peak memory usage: 14 MB % 11.62/2.00 % (3815451)Instructions burned: 160 (million) % 11.62/2.00 % (3815469)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3926001324:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 11.62/2.00 % Exception at run slice level % 11.62/2.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.62/2.00 % (3815461)Instruction limit reached! % 11.62/2.00 % (3815461)------------------------------ % 11.62/2.00 % (3815461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.62/2.00 % (3815461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.62/2.00 % (3815461)CaDiCaL version: 2.1.3 % 11.62/2.00 % (3815461)Termination reason: Instruction limit % 11.62/2.00 % (3815461)Termination phase: Saturation % 11.62/2.00 % (3815461)Time elapsed: 0.045 s % 11.62/2.00 % (3815461)Peak memory usage: 13 MB % 11.62/2.00 % (3815461)Instructions burned: 133 (million) % 11.62/2.00 % (3815471)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2000286102:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 11.62/2.00 % (3815472)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2610946708:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 11.62/2.00 % Exception at run slice level % 11.62/2.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.62/2.00 % (3815475)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=855628270: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) % 11.62/2.00 % (3815464)Instruction limit reached! % 11.62/2.00 % (3815464)------------------------------ % 11.62/2.00 % (3815464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.62/2.00 % (3815464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.62/2.00 % (3815464)CaDiCaL version: 2.1.3 % 11.62/2.00 % (3815464)Termination reason: Instruction limit % 11.62/2.00 % (3815464)Termination phase: Saturation % 11.62/2.00 % (3815464)Time elapsed: 0.046 s % 11.62/2.00 % (3815464)Peak memory usage: 12 MB % 11.62/2.00 % (3815464)Instructions burned: 181 (million) % 11.62/2.00 % (3815477)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3972396503:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.62/2.00 % (3815465)Instruction limit reached! % 11.62/2.00 % (3815465)------------------------------ % 11.62/2.00 % (3815465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.62/2.00 % (3815465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.62/2.00 % (3815465)CaDiCaL version: 2.1.3 % 11.62/2.00 % (3815465)Termination reason: Instruction limit % 11.62/2.00 % (3815465)Termination phase: Saturation % 11.62/2.00 % (3815465)Time elapsed: 0.161 s % 11.62/2.00 % (3815465)Peak memory usage: 14 MB % 11.62/2.00 % (3815465)Instructions burned: 479 (million) % 11.62/2.00 % (3815479)fmb+10_1_sil=64000:random_seed=2472167701:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.62/2.00 % (3815479)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.62/2.00 % Exception at run slice level % 11.62/2.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.62/2.00 % (3815481)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1945077376:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.62/2.00 % Exception at run slice level % 11.62/2.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.62/2.00 % (3815463)Instruction limit reached! % 11.62/2.00 % (3815463)------------------------------ % 11.62/2.00 % (3815463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.62/2.00 % (3815463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.62/2.00 % (3815463)CaDiCaL version: 2.1.3 % 11.62/2.00 % (3815463)Termination reason: Instruction limit % 11.62/2.00 % (3815463)Termination phase: Saturation % 11.62/2.00 % (3815463)Time elapsed: 0.201 s % 11.62/2.00 % (3815463)Peak memory usage: 14 MB % 11.62/2.00 % (3815463)Instructions burned: 685 (million) % 11.62/2.00 % (3815483)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2668630658:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.62/2.00 % Exception at run slice level % 61.02/8.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 61.02/8.87 % (3815484)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2769020634:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 61.02/8.87 % (3815486)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3201733703:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 61.02/8.87 % (3815486)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.02/8.87 % (3815475)Instruction limit reached! % 61.02/8.87 % (3815475)------------------------------ % 61.02/8.87 % (3815475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.02/8.87 % (3815475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.02/8.87 % (3815475)CaDiCaL version: 2.1.3 % 61.02/8.87 % (3815475)Termination reason: Instruction limit % 61.02/8.87 % (3815475)Termination phase: Saturation % 61.02/8.87 % (3815475)Time elapsed: 0.197 s % 61.02/8.87 % (3815475)Peak memory usage: 16 MB % 61.02/8.87 % (3815475)Instructions burned: 696 (million) % 61.02/8.87 % (3815489)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3786061393:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 61.02/8.87 % Exception at run slice level % 61.02/8.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 61.02/8.87 % (3815491)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2662009410:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 61.02/8.87 % Exception at run slice level % 61.02/8.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 61.02/8.87 % (3815493)ott-2_1_sil=16000:newcnf=on:random_seed=3636652908:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 61.02/8.87 % (3815477)Instruction limit reached! % 61.02/8.87 % (3815477)------------------------------ % 61.02/8.87 % (3815477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.02/8.87 % (3815477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.02/8.87 % (3815477)CaDiCaL version: 2.1.3 % 61.02/8.87 % (3815477)Termination reason: Instruction limit % 61.02/8.87 % (3815477)Termination phase: Saturation % 61.02/8.87 % (3815477)Time elapsed: 0.278 s % 61.02/8.87 % (3815477)Peak memory usage: 19 MB % 61.02/8.87 % (3815477)Instructions burned: 882 (million) % 61.02/8.87 % (3815495)ott+10_1_sil=32000:tgt=ground:random_seed=4215344032:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 61.02/8.87 % (3815471)Instruction limit reached! % 61.02/8.87 % (3815471)------------------------------ % 61.02/8.87 % (3815471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.02/8.87 % (3815471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.02/8.87 % (3815471)CaDiCaL version: 2.1.3 % 61.02/8.87 % (3815471)Termination reason: Instruction limit % 61.02/8.87 % (3815471)Termination phase: Saturation % 61.02/8.87 % (3815471)Time elapsed: 0.356 s % 61.02/8.87 % (3815471)Peak memory usage: 18 MB % 61.02/8.87 % (3815471)Instructions burned: 1181 (million) % 61.02/8.87 % (3815497)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2780645662:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 61.02/8.87 % Exception at run slice level % 61.02/8.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 61.02/8.87 % (3815499)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1825845607:i=3512:aac=none_2995 on theBenchmark for (2995ds/3512Mi) % 61.02/8.87 % (3815493)Instruction limit reached! % 61.02/8.87 % (3815493)------------------------------ % 61.02/8.87 % (3815493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.02/8.87 % (3815493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.02/8.87 % (3815493)CaDiCaL version: 2.1.3 % 61.02/8.87 % (3815493)Termination reason: Instruction limit % 61.02/8.87 % (3815493)Termination phase: Saturation % 61.02/8.87 % (3815493)Time elapsed: 0.266 s % 61.02/8.87 % (3815493)Peak memory usage: 14 MB % 61.02/8.87 % (3815493)Instructions burned: 869 (million) % 61.02/8.87 % (3815501)dis+21_1_sil=32000:sas=cadical:random_seed=4056038428:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 61.02/8.87 % (3815486)Instruction limit reached! % 61.02/8.87 % (3815486)------------------------------ % 61.02/8.87 % (3815486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.33/10.34 % (3815486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.33/10.34 % (3815486)CaDiCaL version: 2.1.3 % 71.33/10.34 % (3815486)Termination reason: Instruction limit % 71.33/10.34 % (3815486)Termination phase: Saturation % 71.33/10.34 % (3815486)Time elapsed: 0.399 s % 71.33/10.34 % (3815486)Peak memory usage: 28 MB % 71.33/10.34 % (3815486)Instructions burned: 1475 (million) % 71.33/10.34 % (3815503)ott+11_1_sil=16000:gs=on:random_seed=3510232018:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi) % 71.33/10.34 % (3815503)Instruction limit reached! % 71.33/10.34 % (3815503)------------------------------ % 71.33/10.34 % (3815503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.33/10.34 % (3815503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.33/10.34 % (3815503)CaDiCaL version: 2.1.3 % 71.33/10.34 % (3815503)Termination reason: Instruction limit % 71.33/10.34 % (3815503)Termination phase: Saturation % 71.33/10.34 % (3815503)Time elapsed: 0.603 s % 71.33/10.34 % (3815503)Peak memory usage: 19 MB % 71.33/10.34 % (3815503)Instructions burned: 2255 (million) % 71.33/10.34 % (3815505)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=633733769:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 71.33/10.34 % Exception at run slice level % 71.33/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.33/10.34 % (3815507)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3529583872:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi) % 71.33/10.34 % (3815499)Instruction limit reached! % 71.33/10.34 % (3815499)------------------------------ % 71.33/10.34 % (3815499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.33/10.34 % (3815499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.33/10.34 % (3815499)CaDiCaL version: 2.1.3 % 71.33/10.34 % (3815499)Termination reason: Instruction limit % 71.33/10.34 % (3815499)Termination phase: Saturation % 71.33/10.34 % (3815499)Time elapsed: 0.996 s % 71.33/10.34 % (3815499)Peak memory usage: 21 MB % 71.33/10.34 % (3815499)Instructions burned: 3515 (million) % 71.33/10.34 % (3815509)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=754877114:i=29340_2985 on theBenchmark for (2985ds/29340Mi) % 71.33/10.34 % (3815484)Instruction limit reached! % 71.33/10.34 % (3815484)------------------------------ % 71.33/10.34 % (3815484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.33/10.34 % (3815484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.33/10.34 % (3815484)CaDiCaL version: 2.1.3 % 71.33/10.34 % (3815484)Termination reason: Instruction limit % 71.33/10.34 % (3815484)Termination phase: Saturation % 71.33/10.34 % (3815484)Time elapsed: 1.504 s % 71.33/10.34 % (3815484)Peak memory usage: 25 MB % 71.33/10.34 % (3815484)Instructions burned: 5133 (million) % 71.33/10.34 % (3815511)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=177868407:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 71.33/10.34 % (3815501)Instruction limit reached! % 71.33/10.34 % (3815501)------------------------------ % 71.33/10.34 % (3815501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.33/10.34 % (3815501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.33/10.34 % (3815501)CaDiCaL version: 2.1.3 % 71.33/10.34 % (3815501)Termination reason: Instruction limit % 71.33/10.34 % (3815501)Termination phase: Saturation % 71.33/10.34 % (3815501)Time elapsed: 1.189 s % 71.33/10.34 % (3815501)Peak memory usage: 25 MB % 71.33/10.34 % (3815501)Instructions burned: 3774 (million) % 71.33/10.34 % (3815513)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4235469317:i=5497:nm=2_2981 on theBenchmark for (2981ds/5497Mi) % 71.33/10.34 % Exception at run slice level % 71.33/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.33/10.34 % (3815515)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=31853521:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 71.33/10.34 % Exception at run slice level % 71.33/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.33/10.34 % (3815517)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=531015315:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 71.33/10.34 % Exception at run slice level % 105.50/15.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.50/15.13 % (3815519)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2065703027:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 105.50/15.13 % (3815495)Instruction limit reached! % 105.50/15.13 % (3815495)------------------------------ % 105.50/15.13 % (3815495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815495)CaDiCaL version: 2.1.3 % 105.50/15.13 % (3815495)Termination reason: Instruction limit % 105.50/15.13 % (3815495)Termination phase: Saturation % 105.50/15.13 % (3815495)Time elapsed: 1.671 s % 105.50/15.13 % (3815495)Peak memory usage: 25 MB % 105.50/15.13 % (3815495)Instructions burned: 5116 (million) % 105.50/15.13 % (3815521)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=976241687:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 105.50/15.13 % (3815507)Instruction limit reached! % 105.50/15.13 % (3815507)------------------------------ % 105.50/15.13 % (3815507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815507)CaDiCaL version: 2.1.3 % 105.50/15.13 % (3815507)Termination reason: Instruction limit % 105.50/15.13 % (3815507)Termination phase: Saturation % 105.50/15.13 % (3815507)Time elapsed: 1.014 s % 105.50/15.13 % (3815507)Peak memory usage: 32 MB % 105.50/15.13 % (3815507)Instructions burned: 4592 (million) % 105.50/15.13 % (3815523)dis+10_16:1_sil=16000:random_seed=4111904471:i=9155:fsr=off_2976 on theBenchmark for (2976ds/9155Mi) % 105.50/15.13 % (3815511)Instruction limit reached! % 105.50/15.13 % (3815511)------------------------------ % 105.50/15.13 % (3815511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815511)CaDiCaL version: 2.1.3 % 105.50/15.13 % (3815511)Termination reason: Instruction limit % 105.50/15.13 % (3815511)Termination phase: Saturation % 105.50/15.13 % (3815511)Time elapsed: 1.476 s % 105.50/15.13 % (3815511)Peak memory usage: 45 MB % 105.50/15.13 % (3815511)Instructions burned: 5215 (million) % 105.50/15.13 % (3815525)ott-3_8_sil=64000:random_seed=879448029:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 105.50/15.13 % (3815521)Instruction limit reached! % 105.50/15.13 % (3815521)------------------------------ % 105.50/15.13 % (3815521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815521)CaDiCaL version: 2.1.3 % 105.50/15.13 % (3815521)Termination reason: Instruction limit % 105.50/15.13 % (3815521)Termination phase: Saturation % 105.50/15.13 % (3815521)Time elapsed: 2.643 s % 105.50/15.13 % (3815521)Peak memory usage: 51 MB % 105.50/15.13 % (3815521)Instructions burned: 8174 (million) % 105.50/15.13 % (3815527)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1068813047:fmbsr=2:i=32576_2952 on theBenchmark for (2952ds/32576Mi) % 105.50/15.13 % Exception at run slice level % 105.50/15.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 105.50/15.13 % (3815529)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=655151209:i=11404_2952 on theBenchmark for (2952ds/11404Mi) % 105.50/15.13 % (3815523)Instruction limit reached! % 105.50/15.13 % (3815523)------------------------------ % 105.50/15.13 % (3815523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815523)CaDiCaL version: 2.1.3 % 105.50/15.13 % (3815523)Termination reason: Instruction limit % 105.50/15.13 % (3815523)Termination phase: Saturation % 105.50/15.13 % (3815523)Time elapsed: 2.579 s % 105.50/15.13 % (3815523)Peak memory usage: 84 MB % 105.50/15.13 % (3815523)Instructions burned: 9157 (million) % 105.50/15.13 % (3815531)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3866092406:i=14134_2950 on theBenchmark for (2950ds/14134Mi) % 105.50/15.13 % (3815529)Instruction limit reached! % 105.50/15.13 % (3815529)------------------------------ % 105.50/15.13 % (3815529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.50/15.13 % (3815529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.50/15.13 % (3815529)CaDiCaL version: 2.1.3 % 113.18/16.27 % (3815529)Termination reason: Instruction limit % 113.18/16.27 % (3815529)Termination phase: Saturation % 113.18/16.27 % (3815529)Time elapsed: 3.961 s % 113.18/16.27 % (3815529)Peak memory usage: 63 MB % 113.18/16.27 % (3815529)Instructions burned: 11404 (million) % 113.18/16.27 % (3815533)dis+33_16_sil=32000:sac=on:random_seed=3941326226:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi) % 113.18/16.27 % (3815519)Instruction limit reached! % 113.18/16.27 % (3815519)------------------------------ % 113.18/16.27 % (3815519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.18/16.27 % (3815519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.18/16.27 % (3815519)CaDiCaL version: 2.1.3 % 113.18/16.27 % (3815519)Termination reason: Instruction limit % 113.18/16.27 % (3815519)Termination phase: Saturation % 113.18/16.27 % (3815519)Time elapsed: 7.284 s % 113.18/16.27 % (3815519)Peak memory usage: 85 MB % 113.18/16.27 % (3815519)Instructions burned: 22566 (million) % 113.18/16.27 % (3815535)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3282229599:avsq=on:i=17627:add=on:amm=off_2908 on theBenchmark for (2908ds/17627Mi) % 113.18/16.27 % (3815531)Instruction limit reached! % 113.18/16.28 % (3815531)------------------------------ % 113.18/16.28 % (3815531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.18/16.28 % (3815531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.18/16.28 % (3815531)CaDiCaL version: 2.1.3 % 113.18/16.28 % (3815531)Termination reason: Instruction limit % 113.18/16.28 % (3815531)Termination phase: Saturation % 113.18/16.28 % (3815531)Time elapsed: 4.667 s % 113.18/16.28 % (3815531)Peak memory usage: 44 MB % 113.18/16.28 % (3815531)Instructions burned: 14137 (million) % 113.18/16.28 % (3815537)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3023874514:s2a=on:i=53295_2903 on theBenchmark for (2903ds/53295Mi) % 113.18/16.28 % (3815509)Instruction limit reached! % 113.18/16.28 % (3815509)------------------------------ % 113.18/16.28 % (3815509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.18/16.28 % (3815509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.18/16.28 % (3815509)CaDiCaL version: 2.1.3 % 113.18/16.28 % (3815509)Termination reason: Instruction limit % 113.18/16.28 % (3815509)Termination phase: Saturation % 113.18/16.28 % (3815509)Time elapsed: 8.399 s % 113.18/16.28 % (3815509)Peak memory usage: 69 MB % 113.18/16.28 % (3815509)Instructions burned: 29341 (million) % 113.18/16.28 % (3815539)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3180909146:i=26857:ins=20_2900 on theBenchmark for (2900ds/26857Mi) % 113.18/16.28 % Exception at run slice level % 113.18/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.18/16.28 % (3815541)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3904360756:i=28120:bs=on:fsr=off_2900 on theBenchmark for (2900ds/28120Mi) % 113.18/16.28 % (3815525)Instruction limit reached! % 113.18/16.28 % (3815525)------------------------------ % 113.18/16.28 % (3815525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.18/16.28 % (3815525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.18/16.28 % (3815525)CaDiCaL version: 2.1.3 % 113.18/16.28 % (3815525)Termination reason: Instruction limit % 113.18/16.28 % (3815525)Termination phase: Saturation % 113.18/16.28 % (3815525)Time elapsed: 6.860 s % 113.18/16.28 % (3815525)Peak memory usage: 50 MB % 113.18/16.28 % (3815525)Instructions burned: 20140 (million) % 113.18/16.28 % (3815543)fmb+10_1_sil=256000:fmbss=7:random_seed=890213995:fmbsr=1.6:i=182295_2898 on theBenchmark for (2898ds/182295Mi) % 113.18/16.28 % Exception at run slice level % 113.18/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.18/16.28 % (3815545)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1533136840:i=44625:gsp=on_2898 on theBenchmark for (2898ds/44625Mi) % 113.18/16.28 % (3815545)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 113.18/16.28 % Exception at run slice level % 113.18/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.18/16.28 % (3815547)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=134056625:i=160505_2898 on theBenchmark for (2898ds/160505Mi) % 113.18/16.28 % Exception at run slice level % 113.18/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.18/16.28 % (3815549)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1505283048:fmbsr=1.3:i=225729_2897 on theBenchmark for (2897ds/225729Mi) % 149.87/21.46 % Exception at run slice level % 149.87/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.87/21.46 % (3815551)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=170739879:fmbsr=2:i=185024:ins=7_2897 on theBenchmark for (2897ds/185024Mi) % 149.87/21.46 % Exception at run slice level % 149.87/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.87/21.46 % (3815553)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3761250995:rtra=on_2897 on theBenchmark for (2897ds/0Mi) % 149.87/21.46 % Exception at run slice level % 149.87/21.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.87/21.46 % (3815555)% WARNING: option uhcvi not known. % 149.87/21.46 % (3815555)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1205506620:i=271062:add=off:rtra=on:rawr=on_2897 on theBenchmark for (2897ds/271062Mi) % 149.87/21.46 % (3815533)Instruction limit reached! % 149.87/21.46 % (3815533)------------------------------ % 149.87/21.46 % (3815533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.87/21.46 % (3815533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.87/21.46 % (3815533)CaDiCaL version: 2.1.3 % 149.87/21.46 % (3815533)Termination reason: Instruction limit % 149.87/21.46 % (3815533)Termination phase: Saturation % 149.87/21.46 % (3815533)Time elapsed: 4.537 s % 149.87/21.46 % (3815533)Peak memory usage: 32 MB % 149.87/21.46 % (3815533)Instructions burned: 15854 (million) % 149.87/21.46 % (3815557)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3104320993:i=176048:add=on:rtra=on:rawr=on_2866 on theBenchmark for (2866ds/176048Mi) % 149.87/21.46 % (3815535)Instruction limit reached! % 149.87/21.46 % (3815535)------------------------------ % 149.87/21.46 % (3815535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.87/21.46 % (3815535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.87/21.46 % (3815535)CaDiCaL version: 2.1.3 % 149.87/21.46 % (3815535)Termination reason: Instruction limit % 149.87/21.46 % (3815535)Termination phase: Saturation % 149.87/21.46 % (3815535)Time elapsed: 5.521 s % 149.87/21.46 % (3815535)Peak memory usage: 226 MB % 149.87/21.46 % (3815535)Instructions burned: 17628 (million) % 149.87/21.46 % (3815559)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3841136830:i=206:fgj=on:rtra=on_2852 on theBenchmark for (2852ds/206Mi) % 149.87/21.46 % (3815559)Instruction limit reached! % 149.87/21.46 % (3815559)------------------------------ % 149.87/21.46 % (3815559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.87/21.46 % (3815559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.87/21.46 % (3815559)CaDiCaL version: 2.1.3 % 149.87/21.46 % (3815559)Termination reason: Instruction limit % 149.87/21.46 % (3815559)Termination phase: Saturation % 149.87/21.46 % (3815559)Time elapsed: 0.070 s % 149.87/21.46 % (3815559)Peak memory usage: 12 MB % 149.87/21.46 % (3815559)Instructions burned: 209 (million) % 149.87/21.46 % (3815561)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=987681552:i=232:rtra=on_2851 on theBenchmark for (2851ds/232Mi) % 149.87/21.46 % (3815561)Instruction limit reached! % 149.87/21.46 % (3815561)------------------------------ % 149.87/21.46 % (3815561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.87/21.46 % (3815561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.87/21.46 % (3815561)CaDiCaL version: 2.1.3 % 149.87/21.46 % (3815561)Termination reason: Instruction limit % 149.87/21.46 % (3815561)Termination phase: Saturation % 149.87/21.46 % (3815561)Time elapsed: 0.080 s % 149.87/21.46 % (3815561)Peak memory usage: 13 MB % 149.87/21.46 % (3815561)Instructions burned: 234 (million) % 149.87/21.46 % (3815563)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=515281132:i=262:rtra=on_2851 on theBenchmark for (2851ds/262Mi) % 149.87/21.46 % (3815563)Instruction limit reached! % 149.87/21.46 % (3815563)------------------------------ % 149.87/21.46 % (3815563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.87/21.46 % (3815563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.87/21.46 % (3815563)CaDiCaL version: 2.1.3 % 149.87/21.46 % (3815563)Termination reason: Instruction limit % 149.87/21.46 % (3815563)Termination phase: Saturation % 186.55/26.60 % (3815563)Time elapsed: 0.088 s % 186.55/26.60 % (3815563)Peak memory usage: 14 MB % 186.55/26.60 % (3815563)Instructions burned: 263 (million) % 186.55/26.60 % (3815565)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1954682015:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2850 on theBenchmark for (2850ds/318Mi) % 186.55/26.60 % (3815565)Instruction limit reached! % 186.55/26.60 % (3815565)------------------------------ % 186.55/26.60 % (3815565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.55/26.60 % (3815565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.55/26.60 % (3815565)CaDiCaL version: 2.1.3 % 186.55/26.60 % (3815565)Termination reason: Instruction limit % 186.55/26.60 % (3815565)Termination phase: Saturation % 186.55/26.60 % (3815565)Time elapsed: 0.088 s % 186.55/26.60 % (3815565)Peak memory usage: 13 MB % 186.55/26.60 % (3815565)Instructions burned: 318 (million) % 186.55/26.60 % (3815567)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1199921824:i=1428:nm=2:rtra=on_2848 on theBenchmark for (2848ds/1428Mi) % 186.55/26.60 % Exception at run slice level % 186.55/26.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.55/26.60 % (3815569)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3907759034:i=262:bd=preordered:rtra=on:fsd=on_2848 on theBenchmark for (2848ds/262Mi) % 186.55/26.60 % (3815569)Instruction limit reached! % 186.55/26.60 % (3815569)------------------------------ % 186.55/26.60 % (3815569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.55/26.60 % (3815569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.55/26.60 % (3815569)CaDiCaL version: 2.1.3 % 186.55/26.60 % (3815569)Termination reason: Instruction limit % 186.55/26.60 % (3815569)Termination phase: Saturation % 186.55/26.60 % (3815569)Time elapsed: 0.094 s % 186.55/26.60 % (3815569)Peak memory usage: 15 MB % 186.55/26.60 % (3815569)Instructions burned: 264 (million) % 186.55/26.60 % (3815571)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=2611827752:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/1368Mi) % 186.55/26.60 % (3815571)Instruction limit reached! % 186.55/26.60 % (3815571)------------------------------ % 186.55/26.60 % (3815571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.55/26.60 % (3815571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.55/26.60 % (3815571)CaDiCaL version: 2.1.3 % 186.55/26.60 % (3815571)Termination reason: Instruction limit % 186.55/26.60 % (3815571)Termination phase: Saturation % 186.55/26.60 % (3815571)Time elapsed: 0.445 s % 186.55/26.60 % (3815571)Peak memory usage: 16 MB % 186.55/26.60 % (3815571)Instructions burned: 1370 (million) % 186.55/26.60 % (3815573)ott-21_1_sil=16000:si=on:fs=off:random_seed=1610970345:i=360:av=off:fsr=off:rtra=on_2843 on theBenchmark for (2843ds/360Mi) % 186.55/26.60 % (3815573)Instruction limit reached! % 186.55/26.60 % (3815573)------------------------------ % 186.55/26.60 % (3815573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.55/26.60 % (3815573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.55/26.60 % (3815573)CaDiCaL version: 2.1.3 % 186.55/26.60 % (3815573)Termination reason: Instruction limit % 186.55/26.60 % (3815573)Termination phase: Saturation % 186.55/26.60 % (3815573)Time elapsed: 0.095 s % 186.55/26.60 % (3815573)Peak memory usage: 14 MB % 186.55/26.60 % (3815573)Instructions burned: 364 (million) % 186.55/26.60 % (3815575)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1663757644:i=954:bd=all:rtra=on_2842 on theBenchmark for (2842ds/954Mi) % 186.55/26.60 % (3815575)Instruction limit reached! % 186.55/26.60 % (3815575)------------------------------ % 186.55/26.60 % (3815575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.55/26.60 % (3815575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.55/26.60 % (3815575)CaDiCaL version: 2.1.3 % 186.55/26.60 % (3815575)Termination reason: Instruction limit % 186.55/26.60 % (3815575)Termination phase: Saturation % 186.55/26.60 % (3815575)Time elapsed: 0.335 s % 186.55/26.60 % (3815575)Peak memory usage: 17 MB % 186.55/26.60 % (3815575)Instructions burned: 956 (million) % 186.55/26.60 % (3815577)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2750552190:fmbsr=1.3:i=1730:ins=25:rtra=on_2838 on theBenchmark for (2838ds/1730Mi) % 186.55/26.60 % Exception at run slice level % 186.55/26.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 209.11/29.89 % (3815579)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2150479716:i=2358:rtra=on_2838 on theBenchmark for (2838ds/2358Mi) % 209.11/29.89 % (3815579)Instruction limit reached! % 209.11/29.89 % (3815579)------------------------------ % 209.11/29.89 % (3815579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.11/29.89 % (3815579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.11/29.89 % (3815579)CaDiCaL version: 2.1.3 % 209.11/29.89 % (3815579)Termination reason: Instruction limit % 209.11/29.89 % (3815579)Termination phase: Saturation % 209.11/29.89 % (3815579)Time elapsed: 0.806 s % 209.11/29.89 % (3815579)Peak memory usage: 21 MB % 209.11/29.89 % (3815579)Instructions burned: 2359 (million) % 209.11/29.89 % (3815581)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1518442269:i=1778:ins=1:rtra=on_2830 on theBenchmark for (2830ds/1778Mi) % 209.11/29.89 % Exception at run slice level % 209.11/29.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 209.11/29.89 % (3815583)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=3277981667:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/1384Mi) % 209.11/29.89 % (3815583)Instruction limit reached! % 209.11/29.89 % (3815583)------------------------------ % 209.11/29.89 % (3815583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.11/29.89 % (3815583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.11/29.89 % (3815583)CaDiCaL version: 2.1.3 % 209.11/29.89 % (3815583)Termination reason: Instruction limit % 209.11/29.89 % (3815583)Termination phase: Saturation % 209.11/29.89 % (3815583)Time elapsed: 0.353 s % 209.11/29.89 % (3815583)Peak memory usage: 18 MB % 209.11/29.89 % (3815583)Instructions burned: 1385 (million) % 209.11/29.89 % (3815585)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1419007404:i=1758:kws=inv_precedence:fsr=off:rtra=on_2826 on theBenchmark for (2826ds/1758Mi) % 209.11/29.89 % (3815585)Instruction limit reached! % 209.11/29.89 % (3815585)------------------------------ % 209.11/29.89 % (3815585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.11/29.89 % (3815585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.11/29.89 % (3815585)CaDiCaL version: 2.1.3 % 209.11/29.89 % (3815585)Termination reason: Instruction limit % 209.11/29.89 % (3815585)Termination phase: Saturation % 209.11/29.89 % (3815585)Time elapsed: 0.560 s % 209.11/29.89 % (3815585)Peak memory usage: 24 MB % 209.11/29.89 % (3815585)Instructions burned: 1761 (million) % 209.11/29.89 % (3815587)fmb+10_1_sil=64000:si=on:random_seed=3023255757:i=44122:nm=2:rtra=on:gsp=on_2820 on theBenchmark for (2820ds/44122Mi) % 209.11/29.89 % (3815587)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 209.11/29.89 % Exception at run slice level % 209.11/29.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 209.11/29.89 % (3815589)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3488545219:i=19030:nm=5:rtra=on_2820 on theBenchmark for (2820ds/19030Mi) % 209.11/29.89 % Exception at run slice level % 209.11/29.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 209.11/29.89 % (3815591)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4218234645:fmbsr=1.7:i=1840:rtra=on_2820 on theBenchmark for (2820ds/1840Mi) % 209.11/29.89 % Exception at run slice level % 209.11/29.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 209.11/29.89 % (3815593)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=371922073:i=10262:rtra=on_2820 on theBenchmark for (2820ds/10262Mi) % 209.11/29.89 % (3815593)Instruction limit reached! % 209.11/29.89 % (3815593)------------------------------ % 209.11/29.89 % (3815593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.11/29.89 % (3815593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.11/29.89 % (3815593)CaDiCaL version: 2.1.3 % 209.11/29.89 % (3815593)Termination reason: Instruction limit % 209.11/29.89 % (3815593)Termination phase: Saturation % 209.11/29.89 % (3815593)Time elapsed: 3.358 s % 209.11/29.89 % (3815593)Peak memory usage: 33 MB % 209.11/29.89 % (3815593)Instructions burned: 10263 (million) % 300.09/42.73 % (3815595)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2970669456:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2786 on theBenchmark for (2786ds/2944Mi) % 300.09/42.73 % (3815595)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.09/42.73 % (3815595)Instruction limit reached! % 300.09/42.73 % (3815595)------------------------------ % 300.09/42.73 % (3815595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.73 % (3815595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.73 % (3815595)CaDiCaL version: 2.1.3 % 300.09/42.73 % (3815595)Termination reason: Instruction limit % 300.09/42.73 % (3815595)Termination phase: Saturation % 300.09/42.73 % (3815595)Time elapsed: 0.758 s % 300.09/42.73 % (3815595)Peak memory usage: 30 MB % 300.09/42.73 % (3815595)Instructions burned: 2945 (million) % 300.09/42.73 % (3815597)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1992561600:i=12648:rtra=on_2778 on theBenchmark for (2778ds/12648Mi) % 300.09/42.73 % Exception at run slice level % 300.09/42.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.09/42.73 % (3815599)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3043728744:fmbsr=2.30978:i=4348:rtra=on_2778 on theBenchmark for (2778ds/4348Mi) % 300.09/42.73 % Exception at run slice level % 300.09/42.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.09/42.73 % (3815601)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2366526699:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2778 on theBenchmark for (2778ds/1738Mi) % 300.09/42.73 % (3815601)Instruction limit reached! % 300.09/42.73 % (3815601)------------------------------ % 300.09/42.73 % (3815601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.73 % (3815601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.73 % (3815601)CaDiCaL version: 2.1.3 % 300.09/42.73 % (3815601)Termination reason: Instruction limit % 300.09/42.73 % (3815601)Termination phase: Saturation % 300.09/42.73 % (3815601)Time elapsed: 0.567 s % 300.09/42.73 % (3815601)Peak memory usage: 17 MB % 300.09/42.73 % (3815601)Instructions burned: 1738 (million) % 300.09/42.73 % (3815603)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3567971435:i=10228:av=off:rtra=on_2772 on theBenchmark for (2772ds/10228Mi) % 300.09/42.73 % (3815541)Instruction limit reached! % 300.09/42.73 % (3815541)------------------------------ % 300.09/42.73 % (3815541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.73 % (3815541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.73 % (3815541)CaDiCaL version: 2.1.3 % 300.09/42.73 % (3815541)Termination reason: Instruction limit % 300.09/42.73 % (3815541)Termination phase: Saturation % 300.09/42.73 % (3815541)Time elapsed: 12.921 s % 300.09/42.73 % (3815541)Peak memory usage: 424 MB % 300.09/42.73 % (3815541)Instructions burned: 28120 (million) % 300.09/42.73 % (3815605)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3504102998:i=108564:rtra=on_2771 on theBenchmark for (2771ds/108564Mi) % 300.09/42.73 % Exception at run slice level % 300.09/42.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.09/42.73 % (3815607)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4199088525:i=7024:aac=none:rtra=on_2770 on theBenchmark for (2770ds/7024Mi) % 300.09/42.73 % (3815607)Instruction limit reached! % 300.09/42.73 % (3815607)------------------------------ % 300.09/42.73 % (3815607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.73 % (3815607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.73 % (3815607)CaDiCaL version: 2.1.3 % 300.09/42.73 % (3815607)Termination reason: Instruction limit % 300.09/42.73 % (3815607)Termination phase: Saturation % 300.09/42.73 % (3815607)Time elapsed: 2.320 s % 300.09/42.73 % (3815607)Peak memory usage: 28 MB % 300.09/42.73 % (3815607)Instructions burned: 7026 (million) % 300.09/42.73 % (3815609)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3726741843:i=7546:rtra=on:amm=off_2747 on theBenchmark for (2747ds/7546Mi) % 300.09/42.73 % (3815603)Instruction limit reached! % 300.09/42.73 % (3815603)------------------------------ % 300.09/42.73 % (3815603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.73 % (3815603)Linked with Z3 4.14.0.Terminated % 300.09/42.73 % Vampire exiting %------------------------------------------------------------------------------