%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM030_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 09:40:11 AM UTC 2026 % Result : Timeout 300.02s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : COM030_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.09/0.19 % Computer : n007.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 21:48:04 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.32/1.36 % (2885795)Will run a generic schedule for satisfiability detection. % 7.32/1.36 % (2885800)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=455487303_2999 on theBenchmark for (2999ds/0Mi) % 7.32/1.36 % Exception at run slice level % 7.32/1.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.32/1.36 % (2885801)% WARNING: option uhcvi not known. % 7.32/1.36 % (2885802)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=254345917:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.32/1.36 % (2885801)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3062026642:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.32/1.36 % (2885803)dis+10_1_sil=32000:sp=arity:random_seed=2254541107:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.32/1.36 % (2885804)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1015755413:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.32/1.36 % (2885805)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=747986199:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.32/1.36 % (2885806)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1698775350:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.32/1.36 % (2885808)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=50806843:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.32/1.36 % Exception at run slice level % 7.32/1.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.32/1.36 % (2885816)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2392277556:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.32/1.36 % (2885816)Instruction limit reached! % 7.32/1.36 % (2885816)------------------------------ % 7.32/1.36 % (2885816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.36 % (2885816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.36 % (2885816)CaDiCaL version: 2.1.3 % 7.32/1.36 % (2885816)Termination reason: Instruction limit % 7.32/1.36 % (2885816)Termination phase: Saturation % 7.32/1.36 % (2885816)Time elapsed: 0.044 s % 7.32/1.36 % (2885816)Peak memory usage: 13 MB % 7.32/1.36 % (2885816)Instructions burned: 134 (million) % 7.32/1.36 % (2885803)Instruction limit reached! % 7.32/1.36 % (2885803)------------------------------ % 7.32/1.36 % (2885803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.36 % (2885803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.36 % (2885803)CaDiCaL version: 2.1.3 % 7.32/1.36 % (2885803)Termination reason: Instruction limit % 7.32/1.36 % (2885803)Termination phase: Saturation % 7.32/1.36 % (2885803)Time elapsed: 0.062 s % 7.32/1.36 % (2885803)Peak memory usage: 12 MB % 7.32/1.36 % (2885803)Instructions burned: 103 (million) % 7.32/1.36 % (2885804)Instruction limit reached! % 7.32/1.36 % (2885804)------------------------------ % 7.32/1.36 % (2885804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.36 % (2885804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.36 % (2885804)CaDiCaL version: 2.1.3 % 7.32/1.36 % (2885804)Termination reason: Instruction limit % 7.32/1.36 % (2885804)Termination phase: Saturation % 7.32/1.36 % (2885804)Time elapsed: 0.071 s % 7.32/1.36 % (2885804)Peak memory usage: 13 MB % 7.32/1.36 % (2885804)Instructions burned: 116 (million) % 7.32/1.36 % (2885818)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=2370244715:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.32/1.36 % (2885805)Instruction limit reached! % 7.32/1.36 % (2885805)------------------------------ % 7.32/1.36 % (2885805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.36 % (2885805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.36 % (2885805)CaDiCaL version: 2.1.3 % 7.32/1.36 % (2885805)Termination reason: Instruction limit % 7.32/1.36 % (2885805)Termination phase: Saturation % 7.32/1.36 % (2885805)Time elapsed: 0.080 s % 7.32/1.36 % (2885805)Peak memory usage: 13 MB % 7.32/1.36 % (2885805)Instructions burned: 132 (million) % 7.32/1.36 % (2885819)ott-21_1_sil=16000:fs=off:random_seed=1377891321:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.32/1.36 % (2885820)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2498693580:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.81/3.13 % (2885806)Instruction limit reached! % 19.81/3.13 % (2885806)------------------------------ % 19.81/3.13 % (2885806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.13 % (2885806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.13 % (2885806)CaDiCaL version: 2.1.3 % 19.81/3.13 % (2885806)Termination reason: Instruction limit % 19.81/3.13 % (2885806)Termination phase: Saturation % 19.81/3.13 % (2885806)Time elapsed: 0.098 s % 19.81/3.13 % (2885806)Peak memory usage: 13 MB % 19.81/3.13 % (2885806)Instructions burned: 160 (million) % 19.81/3.13 % (2885822)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3923921210:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.81/3.13 % Exception at run slice level % 19.81/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.81/3.13 % (2885825)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2080138790:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.81/3.13 % (2885827)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=384824127:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.81/3.13 % Exception at run slice level % 19.81/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.81/3.13 % (2885830)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=553172644:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 19.81/3.13 % (2885819)Instruction limit reached! % 19.81/3.13 % (2885819)------------------------------ % 19.81/3.13 % (2885819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.13 % (2885819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.13 % (2885819)CaDiCaL version: 2.1.3 % 19.81/3.13 % (2885819)Termination reason: Instruction limit % 19.81/3.13 % (2885819)Termination phase: Saturation % 19.81/3.13 % (2885819)Time elapsed: 0.091 s % 19.81/3.13 % (2885819)Peak memory usage: 13 MB % 19.81/3.13 % (2885819)Instructions burned: 180 (million) % 19.81/3.13 % (2885832)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2555356335:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.81/3.13 % (2885818)Instruction limit reached! % 19.81/3.13 % (2885818)------------------------------ % 19.81/3.13 % (2885818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.13 % (2885818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.81/3.13 % (2885818)CaDiCaL version: 2.1.3 % 19.81/3.13 % (2885818)Termination reason: Instruction limit % 19.81/3.13 % (2885818)Termination phase: Saturation % 19.81/3.13 % (2885818)Time elapsed: 0.173 s % 19.81/3.13 % (2885818)Peak memory usage: 15 MB % 19.81/3.13 % (2885818)Instructions burned: 687 (million) % 19.81/3.13 % (2885834)fmb+10_1_sil=64000:random_seed=871041097:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 19.81/3.13 % (2885834)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.81/3.13 % Exception at run slice level % 19.81/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.81/3.13 % (2885836)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2306024293:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 19.81/3.13 % Exception at run slice level % 19.81/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.81/3.13 % (2885838)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1205606193:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 19.81/3.13 % Exception at run slice level % 19.81/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.81/3.13 % (2885840)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2376377955:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 19.81/3.13 % (2885820)Instruction limit reached! % 19.81/3.13 % (2885820)------------------------------ % 19.81/3.13 % (2885820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.81/3.13 % (2885820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.69/10.26 % (2885820)CaDiCaL version: 2.1.3 % 70.69/10.26 % (2885820)Termination reason: Instruction limit % 70.69/10.26 % (2885820)Termination phase: Saturation % 70.69/10.26 % (2885820)Time elapsed: 0.296 s % 70.69/10.26 % (2885820)Peak memory usage: 14 MB % 70.69/10.26 % (2885820)Instructions burned: 478 (million) % 70.69/10.26 % (2885842)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4086946000:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 70.69/10.26 % (2885842)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 70.69/10.26 % (2885830)Instruction limit reached! % 70.69/10.26 % (2885830)------------------------------ % 70.69/10.26 % (2885830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.69/10.26 % (2885830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.69/10.26 % (2885830)CaDiCaL version: 2.1.3 % 70.69/10.26 % (2885830)Termination reason: Instruction limit % 70.69/10.26 % (2885830)Termination phase: Saturation % 70.69/10.26 % (2885830)Time elapsed: 0.406 s % 70.69/10.26 % (2885830)Peak memory usage: 16 MB % 70.69/10.26 % (2885830)Instructions burned: 692 (million) % 70.69/10.26 % (2885844)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1052228408:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 70.69/10.26 % Exception at run slice level % 70.69/10.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 70.69/10.26 % (2885846)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=362625607:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 70.69/10.26 % Exception at run slice level % 70.69/10.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 70.69/10.26 % (2885848)ott-2_1_sil=16000:newcnf=on:random_seed=418000279:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 70.69/10.26 % (2885832)Instruction limit reached! % 70.69/10.26 % (2885832)------------------------------ % 70.69/10.26 % (2885832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.69/10.26 % (2885832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.69/10.26 % (2885832)CaDiCaL version: 2.1.3 % 70.69/10.26 % (2885832)Termination reason: Instruction limit % 70.69/10.26 % (2885832)Termination phase: Saturation % 70.69/10.26 % (2885832)Time elapsed: 0.502 s % 70.69/10.26 % (2885832)Peak memory usage: 18 MB % 70.69/10.26 % (2885832)Instructions burned: 880 (million) % 70.69/10.26 % (2885850)ott+10_1_sil=32000:tgt=ground:random_seed=3925064118:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 70.69/10.26 % (2885825)Instruction limit reached! % 70.69/10.26 % (2885825)------------------------------ % 70.69/10.26 % (2885825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.69/10.26 % (2885825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.69/10.26 % (2885825)CaDiCaL version: 2.1.3 % 70.69/10.26 % (2885825)Termination reason: Instruction limit % 70.69/10.26 % (2885825)Termination phase: Saturation % 70.69/10.26 % (2885825)Time elapsed: 0.710 s % 70.69/10.26 % (2885825)Peak memory usage: 23 MB % 70.69/10.26 % (2885825)Instructions burned: 1179 (million) % 70.69/10.26 % (2885852)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3390832529:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 70.69/10.26 % Exception at run slice level % 70.69/10.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 70.69/10.26 % (2885854)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=105450003:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 70.69/10.26 % (2885848)Instruction limit reached! % 70.69/10.26 % (2885848)------------------------------ % 70.69/10.26 % (2885848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.69/10.26 % (2885848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.69/10.26 % (2885848)CaDiCaL version: 2.1.3 % 70.69/10.26 % (2885848)Termination reason: Instruction limit % 70.69/10.26 % (2885848)Termination phase: Saturation % 70.69/10.26 % (2885848)Time elapsed: 0.406 s % 70.69/10.26 % (2885848)Peak memory usage: 13 MB % 70.69/10.26 % (2885848)Instructions burned: 870 (million) % 70.69/10.26 % (2885856)dis+21_1_sil=32000:sas=cadical:random_seed=4209275951:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 70.69/10.26 % (2885842)Instruction limit reached! % 70.69/10.26 % (2885842)------------------------------ % 70.69/10.26 % (2885842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.37/15.99 % (2885842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.37/15.99 % (2885842)CaDiCaL version: 2.1.3 % 97.37/15.99 % (2885842)Termination reason: Instruction limit % 97.37/15.99 % (2885842)Termination phase: Saturation % 97.37/15.99 % (2885842)Time elapsed: 0.677 s % 97.37/15.99 % (2885842)Peak memory usage: 18 MB % 97.37/15.99 % (2885842)Instructions burned: 1473 (million) % 97.37/15.99 % (2885858)ott+11_1_sil=16000:gs=on:random_seed=3729097493:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 97.37/15.99 % (2885840)Instruction limit reached! % 97.37/15.99 % (2885840)------------------------------ % 97.37/15.99 % (2885840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.37/15.99 % (2885840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.37/15.99 % (2885840)CaDiCaL version: 2.1.3 % 97.37/15.99 % (2885840)Termination reason: Instruction limit % 97.37/15.99 % (2885840)Termination phase: Saturation % 97.37/15.99 % (2885840)Time elapsed: 1.463 s % 97.37/15.99 % (2885840)Peak memory usage: 42 MB % 97.37/15.99 % (2885840)Instructions burned: 5131 (million) % 97.37/15.99 % (2885860)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=885685433:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 97.37/15.99 % Exception at run slice level % 97.37/15.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.37/15.99 % (2885862)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3626496841:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 97.37/15.99 % (2885858)Instruction limit reached! % 97.37/15.99 % (2885858)------------------------------ % 97.37/15.99 % (2885858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.37/15.99 % (2885858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.37/15.99 % (2885858)CaDiCaL version: 2.1.3 % 97.37/15.99 % (2885858)Termination reason: Instruction limit % 97.37/15.99 % (2885858)Termination phase: Saturation % 97.37/15.99 % (2885858)Time elapsed: 1.091 s % 97.37/15.99 % (2885858)Peak memory usage: 18 MB % 97.37/15.99 % (2885858)Instructions burned: 2252 (million) % 97.37/15.99 % (2885864)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=883363507:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 97.37/15.99 % (2885854)Instruction limit reached! % 97.37/15.99 % (2885854)------------------------------ % 97.37/15.99 % (2885854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.37/15.99 % (2885854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.37/15.99 % (2885854)CaDiCaL version: 2.1.3 % 97.37/15.99 % (2885854)Termination reason: Instruction limit % 97.37/15.99 % (2885854)Termination phase: Saturation % 97.37/15.99 % (2885854)Time elapsed: 1.900 s % 97.37/15.99 % (2885854)Peak memory usage: 32 MB % 97.37/15.99 % (2885854)Instructions burned: 3513 (million) % 97.37/15.99 % (2885862)Instruction limit reached! % 97.37/15.99 % (2885862)------------------------------ % 97.37/15.99 % (2885862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.37/15.99 % (2885862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.37/15.99 % (2885862)CaDiCaL version: 2.1.3 % 97.37/15.99 % (2885862)Termination reason: Instruction limit % 97.37/16.00 % (2885862)Termination phase: Saturation % 97.37/16.00 % (2885862)Time elapsed: 0.989 s % 97.37/16.00 % (2885862)Peak memory usage: 29 MB % 97.37/16.00 % (2885862)Instructions burned: 4592 (million) % 97.37/16.00 % (2885866)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2549001569:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 97.37/16.00 % (2885867)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2478158825:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 97.37/16.00 % Exception at run slice level % 97.37/16.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.37/16.00 % (2885870)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=440865355:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 97.37/16.00 % Exception at run slice level % 97.37/16.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 97.37/16.00 % (2885872)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1226314869:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 97.37/16.00 % Exception at run slice level % 164.25/23.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 164.25/23.41 % (2885874)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=854812753:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 164.25/23.41 % (2885856)Instruction limit reached! % 164.25/23.41 % (2885856)------------------------------ % 164.25/23.41 % (2885856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885856)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885856)Termination reason: Instruction limit % 164.25/23.41 % (2885856)Termination phase: Saturation % 164.25/23.41 % (2885856)Time elapsed: 2.061 s % 164.25/23.41 % (2885856)Peak memory usage: 34 MB % 164.25/23.41 % (2885856)Instructions burned: 3773 (million) % 164.25/23.41 % (2885876)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3072296329:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 164.25/23.41 % (2885850)Instruction limit reached! % 164.25/23.41 % (2885850)------------------------------ % 164.25/23.41 % (2885850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885850)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885850)Termination reason: Instruction limit % 164.25/23.41 % (2885850)Termination phase: Saturation % 164.25/23.41 % (2885850)Time elapsed: 3.085 s % 164.25/23.41 % (2885850)Peak memory usage: 59 MB % 164.25/23.41 % (2885850)Instructions burned: 5115 (million) % 164.25/23.41 % (2885878)dis+10_16:1_sil=16000:random_seed=3254248913:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 164.25/23.41 % (2885866)Instruction limit reached! % 164.25/23.41 % (2885866)------------------------------ % 164.25/23.41 % (2885866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885866)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885866)Termination reason: Instruction limit % 164.25/23.41 % (2885866)Termination phase: Saturation % 164.25/23.41 % (2885866)Time elapsed: 1.491 s % 164.25/23.41 % (2885866)Peak memory usage: 45 MB % 164.25/23.41 % (2885866)Instructions burned: 5213 (million) % 164.25/23.41 % (2885880)ott-3_8_sil=64000:random_seed=2071886565:i=20139:bs=on_2956 on theBenchmark for (2956ds/20139Mi) % 164.25/23.41 % (2885876)Instruction limit reached! % 164.25/23.41 % (2885876)------------------------------ % 164.25/23.41 % (2885876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885876)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885876)Termination reason: Instruction limit % 164.25/23.41 % (2885876)Termination phase: Saturation % 164.25/23.41 % (2885876)Time elapsed: 5.101 s % 164.25/23.41 % (2885876)Peak memory usage: 88 MB % 164.25/23.41 % (2885876)Instructions burned: 8174 (million) % 164.25/23.41 % (2886254)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=307046388:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 164.25/23.41 % Exception at run slice level % 164.25/23.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 164.25/23.41 % (2886256)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=32994727:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 164.25/23.41 % (2885878)Instruction limit reached! % 164.25/23.41 % (2885878)------------------------------ % 164.25/23.41 % (2885878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885878)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885878)Termination reason: Instruction limit % 164.25/23.41 % (2885878)Termination phase: Saturation % 164.25/23.41 % (2885878)Time elapsed: 4.892 s % 164.25/23.41 % (2885878)Peak memory usage: 58 MB % 164.25/23.41 % (2885878)Instructions burned: 9157 (million) % 164.25/23.41 % (2886258)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3702602409:i=14134_2912 on theBenchmark for (2912ds/14134Mi) % 164.25/23.41 % (2885880)Instruction limit reached! % 164.25/23.41 % (2885880)------------------------------ % 164.25/23.41 % (2885880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.25/23.41 % (2885880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.25/23.41 % (2885880)CaDiCaL version: 2.1.3 % 164.25/23.41 % (2885880)Termination reason: Instruction limit % 174.27/24.81 % (2885880)Termination phase: Saturation % 174.27/24.81 % (2885880)Time elapsed: 5.687 s % 174.27/24.81 % (2885880)Peak memory usage: 36 MB % 174.27/24.81 % (2885880)Instructions burned: 20143 (million) % 174.27/24.81 % (2886260)dis+33_16_sil=32000:sac=on:random_seed=2887285060:i=15851:nm=0_2899 on theBenchmark for (2899ds/15851Mi) % 174.27/24.81 % (2885874)Instruction limit reached! % 174.27/24.81 % (2885874)------------------------------ % 174.27/24.81 % (2885874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.27/24.81 % (2885874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.27/24.81 % (2885874)CaDiCaL version: 2.1.3 % 174.27/24.81 % (2885874)Termination reason: Instruction limit % 174.27/24.81 % (2885874)Termination phase: Saturation % 174.27/24.81 % (2885874)Time elapsed: 9.990 s % 174.27/24.81 % (2885874)Peak memory usage: 23 MB % 174.27/24.81 % (2885874)Instructions burned: 22565 (million) % 174.27/24.81 % (2886263)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1005436745:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 174.27/24.81 % (2886260)Instruction limit reached! % 174.27/24.81 % (2886260)------------------------------ % 174.27/24.81 % (2886260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.27/24.81 % (2886260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.27/24.81 % (2886260)CaDiCaL version: 2.1.3 % 174.27/24.81 % (2886260)Termination reason: Instruction limit % 174.27/24.81 % (2886260)Termination phase: Saturation % 174.27/24.81 % (2886260)Time elapsed: 3.826 s % 174.27/24.81 % (2886260)Peak memory usage: 31 MB % 174.27/24.81 % (2886260)Instructions burned: 15855 (million) % 174.27/24.81 % (2886265)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1497212923:s2a=on:i=53295_2861 on theBenchmark for (2861ds/53295Mi) % 174.27/24.81 % (2886256)Instruction limit reached! % 174.27/24.81 % (2886256)------------------------------ % 174.27/24.81 % (2886256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.27/24.81 % (2886256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.27/24.81 % (2886256)CaDiCaL version: 2.1.3 % 174.27/24.81 % (2886256)Termination reason: Instruction limit % 174.27/24.81 % (2886256)Termination phase: Saturation % 174.27/24.81 % (2886256)Time elapsed: 7.088 s % 174.27/24.81 % (2886256)Peak memory usage: 122 MB % 174.27/24.81 % (2886256)Instructions burned: 11405 (million) % 174.27/24.81 % (2886267)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=280763491:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 174.27/24.81 % Exception at run slice level % 174.27/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.27/24.81 % (2886269)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3364268270:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 174.27/24.81 % (2885864)Instruction limit reached! % 174.27/24.81 % (2885864)------------------------------ % 174.27/24.81 % (2885864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.27/24.81 % (2885864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.27/24.81 % (2885864)CaDiCaL version: 2.1.3 % 174.27/24.81 % (2885864)Termination reason: Instruction limit % 174.27/24.81 % (2885864)Termination phase: Saturation % 174.27/24.81 % (2885864)Time elapsed: 13.401 s % 174.27/24.81 % (2885864)Peak memory usage: 99 MB % 174.27/24.81 % (2885864)Instructions burned: 29341 (million) % 174.27/24.81 % (2886271)fmb+10_1_sil=256000:fmbss=7:random_seed=1385338443:fmbsr=1.6:i=182295_2843 on theBenchmark for (2843ds/182295Mi) % 174.27/24.81 % Exception at run slice level % 174.27/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.27/24.81 % (2886273)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4031319581:i=44625:gsp=on_2843 on theBenchmark for (2843ds/44625Mi) % 174.27/24.81 % (2886273)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 174.27/24.81 % Exception at run slice level % 174.27/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.27/24.81 % (2886275)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2467321575:i=160505_2842 on theBenchmark for (2842ds/160505Mi) % 174.27/24.81 % Exception at run slice level % 174.27/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.27/24.81 % (2886277)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3202501985:fmbsr=1.3:i=225729_2842 on theBenchmark for (2842ds/225729Mi) % 185.52/26.40 % Exception at run slice level % 185.52/26.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 185.52/26.40 % (2886279)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1307069653:fmbsr=2:i=185024:ins=7_2842 on theBenchmark for (2842ds/185024Mi) % 185.52/26.40 % Exception at run slice level % 185.52/26.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 185.52/26.40 % (2886281)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=477579695:rtra=on_2842 on theBenchmark for (2842ds/0Mi) % 185.52/26.40 % Exception at run slice level % 185.52/26.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 185.52/26.40 % (2886283)% WARNING: option uhcvi not known. % 185.52/26.40 % (2886283)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4111894560:i=271062:add=off:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/271062Mi) % 185.52/26.40 % (2886258)Instruction limit reached! % 185.52/26.40 % (2886258)------------------------------ % 185.52/26.40 % (2886258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.52/26.40 % (2886258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.52/26.40 % (2886258)CaDiCaL version: 2.1.3 % 185.52/26.40 % (2886258)Termination reason: Instruction limit % 185.52/26.40 % (2886258)Termination phase: Saturation % 185.52/26.40 % (2886258)Time elapsed: 8.173 s % 185.52/26.40 % (2886258)Peak memory usage: 93 MB % 185.52/26.40 % (2886258)Instructions burned: 14135 (million) % 185.52/26.40 % (2886285)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2307882023:i=176048:add=on:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/176048Mi) % 185.52/26.40 % (2886263)Instruction limit reached! % 185.52/26.40 % (2886263)------------------------------ % 185.52/26.40 % (2886263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.52/26.40 % (2886263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.52/26.40 % (2886263)CaDiCaL version: 2.1.3 % 185.52/26.40 % (2886263)Termination reason: Instruction limit % 185.52/26.40 % (2886263)Termination phase: Saturation % 185.52/26.40 % (2886263)Time elapsed: 9.741 s % 185.52/26.40 % (2886263)Peak memory usage: 71 MB % 185.52/26.40 % (2886263)Instructions burned: 17627 (million) % 185.52/26.40 % (2886348)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1909745246:i=206:fgj=on:rtra=on_2773 on theBenchmark for (2773ds/206Mi) % 185.52/26.40 % (2886348)Instruction limit reached! % 185.52/26.40 % (2886348)------------------------------ % 185.52/26.40 % (2886348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.52/26.40 % (2886348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.52/26.40 % (2886348)CaDiCaL version: 2.1.3 % 185.52/26.40 % (2886348)Termination reason: Instruction limit % 185.52/26.40 % (2886348)Termination phase: Saturation % 185.52/26.40 % (2886348)Time elapsed: 0.129 s % 185.52/26.40 % (2886348)Peak memory usage: 13 MB % 185.52/26.40 % (2886348)Instructions burned: 206 (million) % 185.52/26.40 % (2886350)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1085686156:i=232:rtra=on_2771 on theBenchmark for (2771ds/232Mi) % 185.52/26.40 % (2886350)Instruction limit reached! % 185.52/26.40 % (2886350)------------------------------ % 185.52/26.40 % (2886350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.52/26.40 % (2886350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.52/26.40 % (2886350)CaDiCaL version: 2.1.3 % 185.52/26.40 % (2886350)Termination reason: Instruction limit % 185.52/26.40 % (2886350)Termination phase: Saturation % 185.52/26.40 % (2886350)Time elapsed: 0.145 s % 185.52/26.40 % (2886350)Peak memory usage: 14 MB % 185.52/26.40 % (2886350)Instructions burned: 233 (million) % 185.52/26.40 % (2886352)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2600529775:i=262:rtra=on_2770 on theBenchmark for (2770ds/262Mi) % 185.52/26.40 % (2886352)Instruction limit reached! % 185.52/26.40 % (2886352)------------------------------ % 185.52/26.40 % (2886352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.52/26.40 % (2886352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.52/26.40 % (2886352)CaDiCaL version: 2.1.3 % 185.52/26.40 % (2886352)Termination reason: Instruction limit % 185.52/26.40 % (2886352)Termination phase: Saturation % 224.06/31.83 % (2886352)Time elapsed: 0.165 s % 224.06/31.83 % (2886352)Peak memory usage: 14 MB % 224.06/31.83 % (2886352)Instructions burned: 263 (million) % 224.06/31.83 % (2886354)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1258843426:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2768 on theBenchmark for (2768ds/318Mi) % 224.06/31.83 % (2886354)Instruction limit reached! % 224.06/31.83 % (2886354)------------------------------ % 224.06/31.83 % (2886354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.06/31.83 % (2886354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.06/31.83 % (2886354)CaDiCaL version: 2.1.3 % 224.06/31.83 % (2886354)Termination reason: Instruction limit % 224.06/31.83 % (2886354)Termination phase: Saturation % 224.06/31.83 % (2886354)Time elapsed: 0.189 s % 224.06/31.83 % (2886354)Peak memory usage: 14 MB % 224.06/31.83 % (2886354)Instructions burned: 320 (million) % 224.06/31.83 % (2886356)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1454929946:i=1428:nm=2:rtra=on_2766 on theBenchmark for (2766ds/1428Mi) % 224.06/31.83 % Exception at run slice level % 224.06/31.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.06/31.83 % (2886358)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=64582803:i=262:bd=preordered:rtra=on:fsd=on_2765 on theBenchmark for (2765ds/262Mi) % 224.06/31.83 % (2886358)Instruction limit reached! % 224.06/31.83 % (2886358)------------------------------ % 224.06/31.83 % (2886358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.06/31.83 % (2886358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.06/31.83 % (2886358)CaDiCaL version: 2.1.3 % 224.06/31.83 % (2886358)Termination reason: Instruction limit % 224.06/31.83 % (2886358)Termination phase: Saturation % 224.06/31.83 % (2886358)Time elapsed: 0.166 s % 224.06/31.83 % (2886358)Peak memory usage: 14 MB % 224.06/31.83 % (2886358)Instructions burned: 262 (million) % 224.06/31.83 % (2886360)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=1173661485:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2764 on theBenchmark for (2764ds/1368Mi) % 224.06/31.83 % (2886360)Instruction limit reached! % 224.06/31.83 % (2886360)------------------------------ % 224.06/31.83 % (2886360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.06/31.83 % (2886360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.06/31.83 % (2886360)CaDiCaL version: 2.1.3 % 224.06/31.83 % (2886360)Termination reason: Instruction limit % 224.06/31.83 % (2886360)Termination phase: Saturation % 224.06/31.83 % (2886360)Time elapsed: 0.733 s % 224.06/31.83 % (2886360)Peak memory usage: 16 MB % 224.06/31.83 % (2886360)Instructions burned: 1368 (million) % 224.06/31.83 % (2886362)ott-21_1_sil=16000:si=on:fs=off:random_seed=2697054996:i=360:av=off:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/360Mi) % 224.06/31.83 % (2886269)Instruction limit reached! % 224.06/31.83 % (2886269)------------------------------ % 224.06/31.83 % (2886269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.06/31.83 % (2886269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.06/31.83 % (2886269)CaDiCaL version: 2.1.3 % 224.06/31.83 % (2886269)Termination reason: Instruction limit % 224.06/31.83 % (2886269)Termination phase: Saturation % 224.06/31.83 % (2886269)Time elapsed: 9.021 s % 224.06/31.83 % (2886269)Peak memory usage: 18 MB % 224.06/31.83 % (2886269)Instructions burned: 28122 (million) % 224.06/31.83 % (2886364)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2909177860:i=954:bd=all:rtra=on_2755 on theBenchmark for (2755ds/954Mi) % 224.06/31.83 % (2886362)Instruction limit reached! % 224.06/31.83 % (2886362)------------------------------ % 224.06/31.83 % (2886362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.06/31.83 % (2886362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.06/31.83 % (2886362)CaDiCaL version: 2.1.3 % 224.06/31.83 % (2886362)Termination reason: Instruction limit % 224.06/31.83 % (2886362)Termination phase: Saturation % 224.06/31.83 % (2886362)Time elapsed: 0.187 s % 224.06/31.83 % (2886362)Peak memory usage: 14 MB % 224.06/31.83 % (2886362)Instructions burned: 361 (million) % 224.06/31.83 % (2886366)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2157157727:fmbsr=1.3:i=1730:ins=25:rtra=on_2754 on theBenchmark for (2754ds/1730Mi) % 224.06/31.83 % Exception at run slice level % 224.06/31.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.21/37.05 % (2886368)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=213417464:i=2358:rtra=on_2754 on theBenchmark for (2754ds/2358Mi) % 261.21/37.05 % (2886364)Instruction limit reached! % 261.21/37.05 % (2886364)------------------------------ % 261.21/37.05 % (2886364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.21/37.05 % (2886364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.21/37.05 % (2886364)CaDiCaL version: 2.1.3 % 261.21/37.05 % (2886364)Termination reason: Instruction limit % 261.21/37.05 % (2886364)Termination phase: Saturation % 261.21/37.05 % (2886364)Time elapsed: 0.600 s % 261.21/37.05 % (2886364)Peak memory usage: 16 MB % 261.21/37.05 % (2886364)Instructions burned: 954 (million) % 261.21/37.05 % (2886370)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3166998573:i=1778:ins=1:rtra=on_2748 on theBenchmark for (2748ds/1778Mi) % 261.21/37.05 % Exception at run slice level % 261.21/37.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.21/37.05 % (2886372)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=117574750:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1384Mi) % 261.21/37.05 % (2886372)Instruction limit reached! % 261.21/37.05 % (2886372)------------------------------ % 261.21/37.05 % (2886372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.21/37.05 % (2886372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.21/37.05 % (2886372)CaDiCaL version: 2.1.3 % 261.21/37.05 % (2886372)Termination reason: Instruction limit % 261.21/37.05 % (2886372)Termination phase: Saturation % 261.21/37.05 % (2886372)Time elapsed: 0.786 s % 261.21/37.05 % (2886372)Peak memory usage: 18 MB % 261.21/37.05 % (2886372)Instructions burned: 1384 (million) % 261.21/37.05 % (2886374)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1280140199:i=1758:kws=inv_precedence:fsr=off:rtra=on_2740 on theBenchmark for (2740ds/1758Mi) % 261.21/37.05 % (2886265)Instruction limit reached! % 261.21/37.05 % (2886265)------------------------------ % 261.21/37.05 % (2886265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.21/37.05 % (2886265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.21/37.05 % (2886265)CaDiCaL version: 2.1.3 % 261.21/37.05 % (2886265)Termination reason: Instruction limit % 261.21/37.05 % (2886265)Termination phase: Saturation % 261.21/37.05 % (2886265)Time elapsed: 12.227 s % 261.21/37.05 % (2886265)Peak memory usage: 166 MB % 261.21/37.05 % (2886265)Instructions burned: 53298 (million) % 261.21/37.05 % (2886376)fmb+10_1_sil=64000:si=on:random_seed=1353522815:i=44122:nm=2:rtra=on:gsp=on_2738 on theBenchmark for (2738ds/44122Mi) % 261.21/37.05 % (2886376)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 261.21/37.05 % Exception at run slice level % 261.21/37.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.21/37.05 % (2886368)Instruction limit reached! % 261.21/37.05 % (2886368)------------------------------ % 261.21/37.05 % (2886368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.21/37.05 % (2886368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.21/37.05 % (2886368)CaDiCaL version: 2.1.3 % 261.21/37.05 % (2886368)Termination reason: Instruction limit % 261.21/37.05 % (2886368)Termination phase: Saturation % 261.21/37.05 % (2886368)Time elapsed: 1.543 s % 261.21/37.05 % (2886368)Peak memory usage: 39 MB % 261.21/37.05 % (2886368)Instructions burned: 2358 (million) % 261.21/37.05 % (2886378)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3164550342:i=19030:nm=5:rtra=on_2738 on theBenchmark for (2738ds/19030Mi) % 261.21/37.05 % Exception at run slice level % 261.21/37.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.21/37.05 % (2886379)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1947856251:fmbsr=1.7:i=1840:rtra=on_2738 on theBenchmark for (2738ds/1840Mi) % 261.21/37.05 % Exception at run slice level % 261.21/37.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.21/37.05 % (2886381)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3127817652:i=10262:rtra=on_27Terminated % 300.02/42.54 % Vampire exiting %------------------------------------------------------------------------------