%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX183^1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.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 : Wed Sep 30 08:40:46 AM UTC 2026 % Result : Timeout 300.22s 42.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX183^1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n002.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Tue Sep 29 16:13:07 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 % 5.58/1.11 % (1479657)Will run a generic schedule for satisfiability detection. % 5.58/1.11 % (1479663)% WARNING: option uhcvi not known. % 5.58/1.11 % (1479663)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1005599126:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.58/1.11 % (1479663)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 5.58/1.11 % (1479662)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3296656520_2999 on theBenchmark for (2999ds/0Mi) % 5.58/1.11 % (1479666)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3556131216:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.58/1.11 % (1479664)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3226793505:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.58/1.11 % (1479665)dis+10_1_sil=32000:sp=arity:random_seed=2913125091:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.58/1.11 % (1479663)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 5.58/1.11 % (1479668)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1247722486:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.58/1.11 % (1479666)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 5.58/1.11 % (1479667)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=492997711:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.58/1.11 % Exception at run slice level % 5.58/1.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 5.58/1.11 % (1479676)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1498853718:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.58/1.11 % (1479665)Instruction limit reached! % 5.58/1.11 % (1479665)------------------------------ % 5.58/1.11 % (1479665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.58/1.11 % (1479665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.11 % (1479665)CaDiCaL version: 2.1.3 % 5.58/1.11 % (1479665)Termination reason: Instruction limit % 5.58/1.11 % (1479665)Termination phase: Saturation % 5.58/1.11 % (1479665)Time elapsed: 0.045 s % 5.58/1.11 % (1479665)Peak memory usage: 13 MB % 5.58/1.11 % (1479665)Instructions burned: 104 (million) % 5.58/1.11 % (1479666)Instruction limit reached! % 5.58/1.11 % (1479666)------------------------------ % 5.58/1.11 % (1479666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.58/1.11 % (1479666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.11 % (1479666)CaDiCaL version: 2.1.3 % 5.58/1.11 % (1479666)Termination reason: Instruction limit % 5.58/1.11 % (1479666)Termination phase: Saturation % 5.58/1.11 % (1479666)Time elapsed: 0.050 s % 5.58/1.11 % (1479666)Peak memory usage: 13 MB % 5.58/1.11 % (1479666)Instructions burned: 116 (million) % 5.58/1.11 % Exception at run slice level % 5.58/1.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 5.58/1.11 % (1479668)Instruction limit reached! % 5.58/1.11 % (1479668)------------------------------ % 5.58/1.11 % (1479668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.58/1.11 % (1479679)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=2730353720:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.58/1.11 % (1479668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.11 % (1479668)CaDiCaL version: 2.1.3 % 5.58/1.11 % (1479668)Termination reason: Instruction limit % 5.58/1.11 % (1479668)Termination phase: Saturation % 5.58/1.11 % (1479668)Time elapsed: 0.069 s % 5.58/1.11 % (1479668)Peak memory usage: 14 MB % 5.58/1.11 % (1479668)Instructions burned: 161 (million) % 5.58/1.11 % (1479680)ott-21_1_sil=16000:fs=off:random_seed=2443973631:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.58/1.11 % (1479678)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2983122708:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.58/1.11 % (1479679)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 5.58/1.11 % (1479679)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 5.58/1.11 % (1479683)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1338602940:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 16.85/2.71 % (1479667)Instruction limit reached! % 16.85/2.71 % (1479667)------------------------------ % 16.85/2.71 % (1479667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.71 % (1479667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.71 % (1479667)CaDiCaL version: 2.1.3 % 16.85/2.71 % (1479667)Termination reason: Instruction limit % 16.85/2.71 % (1479667)Termination phase: Saturation % 16.85/2.71 % (1479667)Time elapsed: 0.106 s % 16.85/2.71 % (1479667)Peak memory usage: 13 MB % 16.85/2.71 % (1479667)Instructions burned: 132 (million) % 16.85/2.71 % (1479686)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1189996168:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 16.85/2.71 % (1479680)Instruction limit reached! % 16.85/2.71 % (1479680)------------------------------ % 16.85/2.71 % (1479680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.71 % (1479680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.71 % (1479680)CaDiCaL version: 2.1.3 % 16.85/2.71 % (1479680)Termination reason: Instruction limit % 16.85/2.71 % (1479680)Termination phase: Saturation % 16.85/2.71 % (1479680)Time elapsed: 0.075 s % 16.85/2.71 % (1479680)Peak memory usage: 14 MB % 16.85/2.71 % (1479680)Instructions burned: 181 (million) % 16.85/2.71 % (1479678)Instruction limit reached! % 16.85/2.71 % (1479678)------------------------------ % 16.85/2.71 % (1479678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.71 % (1479678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.71 % (1479678)CaDiCaL version: 2.1.3 % 16.85/2.71 % (1479678)Termination reason: Instruction limit % 16.85/2.71 % (1479678)Termination phase: Saturation % 16.85/2.71 % (1479678)Time elapsed: 0.077 s % 16.85/2.71 % (1479678)Peak memory usage: 13 MB % 16.85/2.71 % (1479678)Instructions burned: 131 (million) % 16.85/2.71 % Exception at run slice level % 16.85/2.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.85/2.71 % (1479688)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2166675669:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 16.85/2.71 % (1479689)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3486892311:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 16.85/2.71 % (1479690)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=1141080484: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) % 16.85/2.71 % (1479690)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.85/2.71 % Exception at run slice level % 16.85/2.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.85/2.71 % (1479694)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3644314726:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.85/2.71 % (1479694)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.85/2.71 % (1479683)Instruction limit reached! % 16.85/2.71 % (1479683)------------------------------ % 16.85/2.71 % (1479683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.71 % (1479683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.71 % (1479683)CaDiCaL version: 2.1.3 % 16.85/2.71 % (1479683)Termination reason: Instruction limit % 16.85/2.71 % (1479683)Termination phase: Saturation % 16.85/2.71 % (1479683)Time elapsed: 0.194 s % 16.85/2.71 % (1479683)Peak memory usage: 17 MB % 16.85/2.71 % (1479683)Instructions burned: 480 (million) % 16.85/2.71 % (1479696)fmb+10_1_sil=64000:random_seed=3205212890:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.85/2.71 % (1479696)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.85/2.71 % Exception at run slice level % 16.85/2.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 16.85/2.71 % (1479698)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1358902892:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.85/2.71 % (1479679)Instruction limit reached! % 16.85/2.71 % (1479679)------------------------------ % 16.85/2.71 % (1479679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.19/6.27 % (1479679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.27 % (1479679)CaDiCaL version: 2.1.3 % 42.19/6.27 % (1479679)Termination reason: Instruction limit % 42.19/6.27 % (1479679)Termination phase: Saturation % 42.19/6.27 % (1479679)Time elapsed: 0.277 s % 42.19/6.27 % (1479679)Peak memory usage: 20 MB % 42.19/6.27 % (1479679)Instructions burned: 685 (million) % 42.19/6.27 % Exception at run slice level % 42.19/6.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 42.19/6.27 % (1479700)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1012548134:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 42.19/6.27 % (1479701)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=930632586:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 42.19/6.27 % Exception at run slice level % 42.19/6.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 42.19/6.27 % (1479701)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 42.19/6.27 % (1479704)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2893932965:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 42.19/6.27 % (1479704)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 42.19/6.27 % (1479704)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 42.19/6.27 % (1479690)Instruction limit reached! % 42.19/6.27 % (1479690)------------------------------ % 42.19/6.27 % (1479690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.19/6.27 % (1479690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.27 % (1479690)CaDiCaL version: 2.1.3 % 42.19/6.27 % (1479690)Termination reason: Instruction limit % 42.19/6.27 % (1479690)Termination phase: Saturation % 42.19/6.27 % (1479690)Time elapsed: 0.277 s % 42.19/6.27 % (1479690)Peak memory usage: 20 MB % 42.19/6.27 % (1479690)Instructions burned: 692 (million) % 42.19/6.27 % (1479706)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=825928032:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 42.19/6.27 % Exception at run slice level % 42.19/6.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 42.19/6.27 % (1479708)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1709888593:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 42.19/6.27 % Exception at run slice level % 42.19/6.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 42.19/6.27 % (1479710)ott-2_1_sil=16000:newcnf=on:random_seed=1347271904:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 42.19/6.27 % (1479710)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 42.19/6.27 % (1479688)Instruction limit reached! % 42.19/6.27 % (1479688)------------------------------ % 42.19/6.27 % (1479688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.19/6.27 % (1479688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.27 % (1479688)CaDiCaL version: 2.1.3 % 42.19/6.27 % (1479688)Termination reason: Instruction limit % 42.19/6.27 % (1479688)Termination phase: Saturation % 42.19/6.27 % (1479688)Time elapsed: 0.472 s % 42.19/6.27 % (1479688)Peak memory usage: 25 MB % 42.19/6.27 % (1479688)Instructions burned: 1181 (million) % 42.19/6.27 % (1479712)ott+10_1_sil=32000:tgt=ground:random_seed=3910903509:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 42.19/6.27 % (1479694)Instruction limit reached! % 42.19/6.27 % (1479694)------------------------------ % 42.19/6.27 % (1479694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.19/6.27 % (1479694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.27 % (1479694)CaDiCaL version: 2.1.3 % 42.19/6.27 % (1479694)Termination reason: Instruction limit % 42.19/6.27 % (1479694)Termination phase: Saturation % 42.19/6.27 % (1479694)Time elapsed: 0.566 s % 42.19/6.27 % (1479694)Peak memory usage: 22 MB % 42.19/6.27 % (1479694)Instructions burned: 880 (million) % 42.19/6.27 % (1479714)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2497474840:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 42.19/6.27 % Exception at run slice level % 100.18/14.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.18/14.42 % (1479716)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3383261441:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 100.18/14.42 % (1479716)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 100.18/14.42 % (1479710)Instruction limit reached! % 100.18/14.42 % (1479710)------------------------------ % 100.18/14.42 % (1479710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.18/14.42 % (1479710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.18/14.42 % (1479710)CaDiCaL version: 2.1.3 % 100.18/14.42 % (1479710)Termination reason: Instruction limit % 100.18/14.42 % (1479710)Termination phase: Saturation % 100.18/14.42 % (1479710)Time elapsed: 0.347 s % 100.18/14.42 % (1479710)Peak memory usage: 22 MB % 100.18/14.42 % (1479710)Instructions burned: 871 (million) % 100.18/14.42 % (1479718)dis+21_1_sil=32000:sas=cadical:random_seed=2739252790:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 100.18/14.42 % (1479704)Instruction limit reached! % 100.18/14.42 % (1479704)------------------------------ % 100.18/14.42 % (1479704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.18/14.42 % (1479704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.18/14.42 % (1479704)CaDiCaL version: 2.1.3 % 100.18/14.42 % (1479704)Termination reason: Instruction limit % 100.18/14.42 % (1479704)Termination phase: Saturation % 100.18/14.42 % (1479704)Time elapsed: 0.566 s % 100.18/14.42 % (1479704)Peak memory usage: 19 MB % 100.18/14.42 % (1479704)Instructions burned: 1473 (million) % 100.18/14.42 % (1479720)ott+11_1_sil=16000:gs=on:random_seed=2412069978:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 100.18/14.42 % (1479720)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 100.18/14.42 % (1479720)Instruction limit reached! % 100.18/14.42 % (1479720)------------------------------ % 100.18/14.42 % (1479720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.18/14.42 % (1479720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.18/14.42 % (1479720)CaDiCaL version: 2.1.3 % 100.18/14.42 % (1479720)Termination reason: Instruction limit % 100.18/14.42 % (1479720)Termination phase: Saturation % 100.18/14.42 % (1479720)Time elapsed: 0.891 s % 100.18/14.42 % (1479720)Peak memory usage: 36 MB % 100.18/14.42 % (1479720)Instructions burned: 2253 (million) % 100.18/14.42 % (1479722)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3975865758:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 100.18/14.42 % Exception at run slice level % 100.18/14.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.18/14.42 % (1479724)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2149077301:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 100.18/14.42 % (1479716)Instruction limit reached! % 100.18/14.42 % (1479716)------------------------------ % 100.18/14.42 % (1479716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.18/14.42 % (1479716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.18/14.42 % (1479716)CaDiCaL version: 2.1.3 % 100.18/14.42 % (1479716)Termination reason: Instruction limit % 100.18/14.42 % (1479716)Termination phase: Saturation % 100.18/14.42 % (1479716)Time elapsed: 1.509 s % 100.18/14.42 % (1479716)Peak memory usage: 51 MB % 100.18/14.42 % (1479716)Instructions burned: 3515 (million) % 100.18/14.42 % (1479726)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2205852612:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 100.18/14.42 % (1479718)Instruction limit reached! % 100.18/14.42 % (1479718)------------------------------ % 100.18/14.42 % (1479718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.18/14.42 % (1479718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.18/14.42 % (1479718)CaDiCaL version: 2.1.3 % 100.18/14.42 % (1479718)Termination reason: Instruction limit % 100.18/14.42 % (1479718)Termination phase: Saturation % 100.18/14.42 % (1479718)Time elapsed: 1.502 s % 100.18/14.42 % (1479718)Peak memory usage: 55 MB % 100.18/14.42 % (1479718)Instructions burned: 3775 (million) % 100.18/14.42 % (1479728)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3747584761:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 142.07/20.34 % (1479701)Instruction limit reached! % 142.07/20.34 % (1479701)------------------------------ % 142.07/20.34 % (1479701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.07/20.34 % (1479701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.07/20.34 % (1479701)CaDiCaL version: 2.1.3 % 142.07/20.34 % (1479701)Termination reason: Instruction limit % 142.07/20.34 % (1479701)Termination phase: Saturation % 142.07/20.34 % (1479701)Time elapsed: 2.089 s % 142.07/20.34 % (1479701)Peak memory usage: 68 MB % 142.07/20.34 % (1479701)Instructions burned: 5133 (million) % 142.07/20.34 % (1479730)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1196046528:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi) % 142.07/20.34 % Exception at run slice level % 142.07/20.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.07/20.34 % (1479732)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2587766306:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi) % 142.07/20.34 % Exception at run slice level % 142.07/20.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.07/20.34 % (1479734)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3105025544:i=14071_2974 on theBenchmark for (2974ds/14071Mi) % 142.07/20.34 % Exception at run slice level % 142.07/20.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 142.07/20.34 % (1479736)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3803756563:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi) % 142.07/20.34 % (1479712)Instruction limit reached! % 142.07/20.34 % (1479712)------------------------------ % 142.07/20.34 % (1479712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.07/20.34 % (1479712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.07/20.34 % (1479712)CaDiCaL version: 2.1.3 % 142.07/20.34 % (1479712)Termination reason: Instruction limit % 142.07/20.34 % (1479712)Termination phase: Saturation % 142.07/20.34 % (1479712)Time elapsed: 2.036 s % 142.07/20.34 % (1479712)Peak memory usage: 68 MB % 142.07/20.34 % (1479712)Instructions burned: 5116 (million) % 142.07/20.34 % (1479738)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=693016836:i=8173:av=off_2972 on theBenchmark for (2972ds/8173Mi) % 142.07/20.34 % (1479728)Instruction limit reached! % 142.07/20.34 % (1479728)------------------------------ % 142.07/20.34 % (1479728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.07/20.34 % (1479728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.07/20.34 % (1479728)CaDiCaL version: 2.1.3 % 142.07/20.34 % (1479728)Termination reason: Instruction limit % 142.07/20.34 % (1479728)Termination phase: Saturation % 142.07/20.34 % (1479728)Time elapsed: 2.083 s % 142.07/20.34 % (1479728)Peak memory usage: 69 MB % 142.07/20.34 % (1479728)Instructions burned: 5213 (million) % 142.07/20.34 % (1479724)Instruction limit reached! % 142.07/20.34 % (1479724)------------------------------ % 142.07/20.34 % (1479724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.07/20.34 % (1479724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.07/20.34 % (1479724)CaDiCaL version: 2.1.3 % 142.07/20.34 % (1479724)Termination reason: Instruction limit % 142.07/20.34 % (1479724)Termination phase: Saturation % 142.07/20.34 % (1479724)Time elapsed: 2.603 s % 142.07/20.34 % (1479724)Peak memory usage: 67 MB % 142.07/20.34 % (1479724)Instructions burned: 4593 (million) % 142.07/20.34 % (1479740)dis+10_16:1_sil=16000:random_seed=3907117450:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 142.07/20.34 % (1479742)ott-3_8_sil=64000:random_seed=2900510237:i=20139:bs=on_2954 on theBenchmark for (2954ds/20139Mi) % 142.07/20.34 % (1479738)Instruction limit reached! % 142.07/20.34 % (1479738)------------------------------ % 142.07/20.34 % (1479738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.07/20.34 % (1479738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.07/20.34 % (1479738)CaDiCaL version: 2.1.3 % 142.07/20.34 % (1479738)Termination reason: Instruction limit % 142.07/20.34 % (1479738)Termination phase: Saturation % 142.07/20.34 % (1479738)Time elapsed: 3.247 s % 142.07/20.34 % (1479738)Peak memory usage: 103 MB % 142.07/20.34 % (1479738)Instructions burned: 8175 (million) % 142.07/20.34 % (1479744)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1329496239:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi) % 150.77/21.67 % Exception at run slice level % 150.77/21.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 150.77/21.67 % (1479746)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=920838341:i=11404_2939 on theBenchmark for (2939ds/11404Mi) % 150.77/21.67 % (1479740)Instruction limit reached! % 150.77/21.67 % (1479740)------------------------------ % 150.77/21.67 % (1479740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.77/21.67 % (1479740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.77/21.67 % (1479740)CaDiCaL version: 2.1.3 % 150.77/21.67 % (1479740)Termination reason: Instruction limit % 150.77/21.67 % (1479740)Termination phase: Saturation % 150.77/21.67 % (1479740)Time elapsed: 3.671 s % 150.77/21.67 % (1479740)Peak memory usage: 114 MB % 150.77/21.67 % (1479740)Instructions burned: 9157 (million) % 150.77/21.67 % (1479748)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2867832534:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 150.77/21.67 % (1479748)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 150.77/21.67 % (1479746)Instruction limit reached! % 150.77/21.67 % (1479746)------------------------------ % 150.77/21.67 % (1479746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.77/21.67 % (1479746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.77/21.67 % (1479746)CaDiCaL version: 2.1.3 % 150.77/21.67 % (1479746)Termination reason: Instruction limit % 150.77/21.67 % (1479746)Termination phase: Saturation % 150.77/21.67 % (1479746)Time elapsed: 4.573 s % 150.77/21.67 % (1479746)Peak memory usage: 135 MB % 150.77/21.67 % (1479746)Instructions burned: 11407 (million) % 150.77/21.67 % (1479750)dis+33_16_sil=32000:sac=on:random_seed=709971462:i=15851:nm=0_2893 on theBenchmark for (2893ds/15851Mi) % 150.77/21.67 % (1479736)Instruction limit reached! % 150.77/21.67 % (1479736)------------------------------ % 150.77/21.67 % (1479736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.77/21.67 % (1479736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.77/21.67 % (1479736)CaDiCaL version: 2.1.3 % 150.77/21.67 % (1479736)Termination reason: Instruction limit % 150.77/21.67 % (1479736)Termination phase: Saturation % 150.77/21.67 % (1479736)Time elapsed: 10.248 s % 150.77/21.67 % (1479736)Peak memory usage: 256 MB % 150.77/21.67 % (1479736)Instructions burned: 22566 (million) % 150.77/21.67 % (1479742)Instruction limit reached! % 150.77/21.67 % (1479742)------------------------------ % 150.77/21.67 % (1479742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.77/21.67 % (1479742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.77/21.67 % (1479742)CaDiCaL version: 2.1.3 % 150.77/21.67 % (1479742)Termination reason: Instruction limit % 150.77/21.67 % (1479742)Termination phase: Saturation % 150.77/21.67 % (1479742)Time elapsed: 8.276 s % 150.77/21.67 % (1479742)Peak memory usage: 233 MB % 150.77/21.67 % (1479742)Instructions burned: 20140 (million) % 150.77/21.67 % (1479752)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1259467499:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 150.77/21.67 % (1479753)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4179861645:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi) % 150.77/21.67 % (1479748)Instruction limit reached! % 150.77/21.67 % (1479748)------------------------------ % 150.77/21.67 % (1479748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.77/21.67 % (1479748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.77/21.67 % (1479748)CaDiCaL version: 2.1.3 % 150.77/21.67 % (1479748)Termination reason: Instruction limit % 150.77/21.67 % (1479748)Termination phase: Saturation % 150.77/21.67 % (1479748)Time elapsed: 5.659 s % 150.77/21.67 % (1479748)Peak memory usage: 172 MB % 150.77/21.67 % (1479748)Instructions burned: 14135 (million) % 150.77/21.67 % (1479756)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3132539813:i=26857:ins=20_2860 on theBenchmark for (2860ds/26857Mi) % 150.77/21.67 % Exception at run slice level % 150.77/21.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 150.77/21.67 % (1479758)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3951094403:i=28120:bs=on:fsr=off_2859 on theBenchmark for (2859ds/28120Mi) % 150.77/21.67 % (1479726)Instruction limit reached! % 150.77/21.67 % (1479726)------------------------------ % 167.11/23.95 % (1479726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.11/23.95 % (1479726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/23.95 % (1479726)CaDiCaL version: 2.1.3 % 167.11/23.95 % (1479726)Termination reason: Instruction limit % 167.11/23.95 % (1479726)Termination phase: Saturation % 167.11/23.95 % (1479726)Time elapsed: 11.757 s % 167.11/23.95 % (1479726)Peak memory usage: 343 MB % 167.11/23.95 % (1479726)Instructions burned: 29341 (million) % 167.11/23.95 % (1479760)fmb+10_1_sil=256000:fmbss=7:random_seed=410367525:fmbsr=1.6:i=182295_2857 on theBenchmark for (2857ds/182295Mi) % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479762)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4287168874:i=44625:gsp=on_2857 on theBenchmark for (2857ds/44625Mi) % 167.11/23.95 % (1479762)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 167.11/23.95 % (1479762)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479764)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3976245774:i=160505_2857 on theBenchmark for (2857ds/160505Mi) % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479766)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1243098948:fmbsr=1.3:i=225729_2856 on theBenchmark for (2856ds/225729Mi) % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479768)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=757479373:fmbsr=2:i=185024:ins=7_2856 on theBenchmark for (2856ds/185024Mi) % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479770)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1321253000:rtra=on_2856 on theBenchmark for (2856ds/0Mi) % 167.11/23.95 % Exception at run slice level % 167.11/23.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 167.11/23.95 % (1479772)% WARNING: option uhcvi not known. % 167.11/23.95 % (1479772)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3577692489:i=271062:add=off:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/271062Mi) % 167.11/23.95 % (1479772)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 167.11/23.95 % (1479772)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 167.11/23.95 % (1479750)Instruction limit reached! % 167.11/23.95 % (1479750)------------------------------ % 167.11/23.95 % (1479750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.11/23.95 % (1479750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/23.95 % (1479750)CaDiCaL version: 2.1.3 % 167.11/23.95 % (1479750)Termination reason: Instruction limit % 167.11/23.95 % (1479750)Termination phase: Saturation % 167.11/23.95 % (1479750)Time elapsed: 7.068 s % 167.11/23.95 % (1479750)Peak memory usage: 188 MB % 167.11/23.95 % (1479750)Instructions burned: 15852 (million) % 167.11/23.95 % (1479774)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3880506612:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 167.11/23.95 % (1479752)Instruction limit reached! % 167.11/23.95 % (1479752)------------------------------ % 167.11/23.95 % (1479752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.11/23.95 % (1479752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/23.95 % (1479752)CaDiCaL version: 2.1.3 % 167.11/23.95 % (1479752)Termination reason: Instruction limit % 167.11/23.95 % (1479752)Termination phase: Saturation % 167.11/23.95 % (1479752)Time elapsed: 7.037 s % 167.11/23.95 % (1479752)Peak memory usage: 213 MB % 167.11/23.95 % (1479752)Instructions burned: 17629 (million) % 167.11/23.95 % (1479776)dis+10_1_sil=32000:si=on:sp=arity:random_seed=766472967:i=206:fgj=on:rtra=on_2800 on theBenchmark for (2800ds/206Mi) % 167.11/23.95 % (1479776)Instruction limit reached! % 188.20/26.88 % (1479776)------------------------------ % 188.20/26.88 % (1479776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.20/26.88 % (1479776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.20/26.88 % (1479776)CaDiCaL version: 2.1.3 % 188.20/26.88 % (1479776)Termination reason: Instruction limit % 188.20/26.88 % (1479776)Termination phase: Saturation % 188.20/26.88 % (1479776)Time elapsed: 0.088 s % 188.20/26.88 % (1479776)Peak memory usage: 14 MB % 188.20/26.88 % (1479776)Instructions burned: 208 (million) % 188.20/26.88 % (1479778)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3361204252:i=232:rtra=on_2798 on theBenchmark for (2798ds/232Mi) % 188.20/26.88 % (1479778)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 188.20/26.88 % (1479778)Instruction limit reached! % 188.20/26.88 % (1479778)------------------------------ % 188.20/26.88 % (1479778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.20/26.88 % (1479778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.20/26.88 % (1479778)CaDiCaL version: 2.1.3 % 188.20/26.88 % (1479778)Termination reason: Instruction limit % 188.20/26.88 % (1479778)Termination phase: Saturation % 188.20/26.88 % (1479778)Time elapsed: 0.131 s % 188.20/26.88 % (1479778)Peak memory usage: 14 MB % 188.20/26.88 % (1479778)Instructions burned: 232 (million) % 188.20/26.88 % (1479780)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2883452994:i=262:rtra=on_2797 on theBenchmark for (2797ds/262Mi) % 188.20/26.88 % (1479780)Instruction limit reached! % 188.20/26.88 % (1479780)------------------------------ % 188.20/26.88 % (1479780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.20/26.88 % (1479780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.20/26.88 % (1479780)CaDiCaL version: 2.1.3 % 188.20/26.88 % (1479780)Termination reason: Instruction limit % 188.20/26.88 % (1479780)Termination phase: Saturation % 188.20/26.88 % (1479780)Time elapsed: 0.134 s % 188.20/26.88 % (1479780)Peak memory usage: 15 MB % 188.20/26.88 % (1479780)Instructions burned: 262 (million) % 188.20/26.88 % (1479782)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2392250706:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2795 on theBenchmark for (2795ds/318Mi) % 188.20/26.88 % (1479782)Instruction limit reached! % 188.20/26.88 % (1479782)------------------------------ % 188.20/26.88 % (1479782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.20/26.88 % (1479782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.20/26.88 % (1479782)CaDiCaL version: 2.1.3 % 188.20/26.88 % (1479782)Termination reason: Instruction limit % 188.20/26.88 % (1479782)Termination phase: Saturation % 188.20/26.88 % (1479782)Time elapsed: 0.189 s % 188.20/26.88 % (1479782)Peak memory usage: 15 MB % 188.20/26.88 % (1479782)Instructions burned: 319 (million) % 188.20/26.88 % (1479784)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=782886683:i=1428:nm=2:rtra=on_2793 on theBenchmark for (2793ds/1428Mi) % 188.20/26.88 % Exception at run slice level % 188.20/26.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 188.20/26.88 % (1479786)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3896002547:i=262:bd=preordered:rtra=on:fsd=on_2793 on theBenchmark for (2793ds/262Mi) % 188.20/26.88 % (1479786)Instruction limit reached! % 188.20/26.88 % (1479786)------------------------------ % 188.20/26.88 % (1479786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.20/26.88 % (1479786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.20/26.88 % (1479786)CaDiCaL version: 2.1.3 % 188.20/26.88 % (1479786)Termination reason: Instruction limit % 188.20/26.88 % (1479786)Termination phase: Saturation % 188.20/26.88 % (1479786)Time elapsed: 0.135 s % 188.20/26.88 % (1479786)Peak memory usage: 15 MB % 188.20/26.88 % (1479786)Instructions burned: 263 (million) % 188.20/26.88 % (1479788)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=1367142235:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/1368Mi) % 188.20/26.88 % (1479788)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 188.20/26.88 % (1479788)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 188.20/26.88 % (1479788)Instruction limit reached! % 188.20/26.88 % (1479788)------------------------------ % 212.34/30.27 % (1479788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.34/30.27 % (1479788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.34/30.27 % (1479788)CaDiCaL version: 2.1.3 % 212.34/30.27 % (1479788)Termination reason: Instruction limit % 212.34/30.27 % (1479788)Termination phase: Saturation % 212.34/30.27 % (1479788)Time elapsed: 0.607 s % 212.34/30.27 % (1479788)Peak memory usage: 25 MB % 212.34/30.27 % (1479788)Instructions burned: 1368 (million) % 212.34/30.27 % (1479790)ott-21_1_sil=16000:si=on:fs=off:random_seed=1225893504:i=360:av=off:fsr=off:rtra=on_2785 on theBenchmark for (2785ds/360Mi) % 212.34/30.27 % (1479790)Instruction limit reached! % 212.34/30.27 % (1479790)------------------------------ % 212.34/30.27 % (1479790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.34/30.27 % (1479790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.34/30.27 % (1479790)CaDiCaL version: 2.1.3 % 212.34/30.27 % (1479790)Termination reason: Instruction limit % 212.34/30.27 % (1479790)Termination phase: Saturation % 212.34/30.27 % (1479790)Time elapsed: 0.174 s % 212.34/30.27 % (1479790)Peak memory usage: 16 MB % 212.34/30.27 % (1479790)Instructions burned: 361 (million) % 212.34/30.27 % (1479792)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=860932559:i=954:bd=all:rtra=on_2783 on theBenchmark for (2783ds/954Mi) % 212.34/30.27 % (1479792)Instruction limit reached! % 212.34/30.27 % (1479792)------------------------------ % 212.34/30.27 % (1479792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.34/30.27 % (1479792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.34/30.27 % (1479792)CaDiCaL version: 2.1.3 % 212.34/30.27 % (1479792)Termination reason: Instruction limit % 212.34/30.27 % (1479792)Termination phase: Saturation % 212.34/30.27 % (1479792)Time elapsed: 0.394 s % 212.34/30.27 % (1479792)Peak memory usage: 20 MB % 212.34/30.27 % (1479792)Instructions burned: 955 (million) % 212.34/30.27 % (1479794)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2372734363:fmbsr=1.3:i=1730:ins=25:rtra=on_2779 on theBenchmark for (2779ds/1730Mi) % 212.34/30.27 % Exception at run slice level % 212.34/30.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 212.34/30.27 % (1479796)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2187762960:i=2358:rtra=on_2779 on theBenchmark for (2779ds/2358Mi) % 212.34/30.27 % (1479796)Instruction limit reached! % 212.34/30.27 % (1479796)------------------------------ % 212.34/30.27 % (1479796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.34/30.27 % (1479796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.34/30.27 % (1479796)CaDiCaL version: 2.1.3 % 212.34/30.27 % (1479796)Termination reason: Instruction limit % 212.34/30.27 % (1479796)Termination phase: Saturation % 212.34/30.27 % (1479796)Time elapsed: 0.945 s % 212.34/30.27 % (1479796)Peak memory usage: 32 MB % 212.34/30.27 % (1479796)Instructions burned: 2359 (million) % 212.34/30.27 % (1479798)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1843781590:i=1778:ins=1:rtra=on_2769 on theBenchmark for (2769ds/1778Mi) % 212.34/30.27 % Exception at run slice level % 212.34/30.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 212.34/30.27 % (1479800)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=2989055830:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/1384Mi) % 212.34/30.27 % (1479800)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 212.34/30.27 % (1479800)Instruction limit reached! % 212.34/30.27 % (1479800)------------------------------ % 212.34/30.27 % (1479800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.34/30.27 % (1479800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.34/30.27 % (1479800)CaDiCaL version: 2.1.3 % 212.34/30.27 % (1479800)Termination reason: Instruction limit % 212.34/30.27 % (1479800)Termination phase: Saturation % 212.34/30.27 % (1479800)Time elapsed: 0.570 s % 212.34/30.27 % (1479800)Peak memory usage: 25 MB % 212.34/30.27 % (1479800)Instructions burned: 1385 (million) % 212.34/30.27 % (1479802)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1070401760:i=1758:kws=inv_precedence:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/1758Mi) % 212.34/30.27 % (1479802)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 256.24/36.42 % (1479802)Instruction limit reached! % 256.24/36.42 % (1479802)------------------------------ % 256.24/36.42 % (1479802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.24/36.42 % (1479802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.24/36.42 % (1479802)CaDiCaL version: 2.1.3 % 256.24/36.42 % (1479802)Termination reason: Instruction limit % 256.24/36.42 % (1479802)Termination phase: Saturation % 256.24/36.42 % (1479802)Time elapsed: 0.713 s % 256.24/36.42 % (1479802)Peak memory usage: 28 MB % 256.24/36.42 % (1479802)Instructions burned: 1760 (million) % 256.24/36.42 % (1479804)fmb+10_1_sil=64000:si=on:random_seed=865883270:i=44122:nm=2:rtra=on:gsp=on_2755 on theBenchmark for (2755ds/44122Mi) % 256.24/36.42 % (1479804)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 256.24/36.42 % Exception at run slice level % 256.24/36.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 256.24/36.42 % (1479806)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3616357384:i=19030:nm=5:rtra=on_2755 on theBenchmark for (2755ds/19030Mi) % 256.24/36.42 % Exception at run slice level % 256.24/36.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 256.24/36.42 % (1479808)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1949097130:fmbsr=1.7:i=1840:rtra=on_2755 on theBenchmark for (2755ds/1840Mi) % 256.24/36.42 % Exception at run slice level % 256.24/36.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 256.24/36.42 % (1479810)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3272557726:i=10262:rtra=on_2754 on theBenchmark for (2754ds/10262Mi) % 256.24/36.42 % (1479810)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 256.24/36.42 % (1479758)Instruction limit reached! % 256.24/36.42 % (1479758)------------------------------ % 256.24/36.42 % (1479758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.24/36.42 % (1479758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.24/36.42 % (1479758)CaDiCaL version: 2.1.3 % 256.24/36.42 % (1479758)Termination reason: Instruction limit % 256.24/36.42 % (1479758)Termination phase: Saturation % 256.24/36.42 % (1479758)Time elapsed: 11.262 s % 256.24/36.42 % (1479758)Peak memory usage: 331 MB % 256.24/36.42 % (1479758)Instructions burned: 28120 (million) % 256.24/36.42 % (1479812)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2026787122:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2746 on theBenchmark for (2746ds/2944Mi) % 256.24/36.42 % (1479812)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 256.24/36.42 % (1479812)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 256.24/36.42 % (1479812)Instruction limit reached! % 256.24/36.42 % (1479812)------------------------------ % 256.24/36.42 % (1479812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.24/36.42 % (1479812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.24/36.42 % (1479812)CaDiCaL version: 2.1.3 % 256.24/36.42 % (1479812)Termination reason: Instruction limit % 256.24/36.42 % (1479812)Termination phase: Saturation % 256.24/36.42 % (1479812)Time elapsed: 1.194 s % 256.24/36.42 % (1479812)Peak memory usage: 35 MB % 256.24/36.42 % (1479812)Instructions burned: 2945 (million) % 256.24/36.42 % (1479814)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3998548306:i=12648:rtra=on_2734 on theBenchmark for (2734ds/12648Mi) % 256.24/36.42 % Exception at run slice level % 256.24/36.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 256.24/36.42 % (1479816)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2644885533:fmbsr=2.30978:i=4348:rtra=on_2734 on theBenchmark for (2734ds/4348Mi) % 256.24/36.42 % Exception at run slice level % 256.24/36.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 256.24/36.42 % (1479818)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=532963476:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2733 on theBenchmark for (2733ds/1738Mi) % 256.24/36.42 % (1479818)WARNING: Not using 'newcnf' as currently not compatible with higherTerminated % 300.22/42.65 % Vampire exiting % 300.22/42.65 Terminated %------------------------------------------------------------------------------