%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW523_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:23 PM UTC 2026 % Result : Timeout 293.21s 41.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW523_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n007.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:15:25 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.25/1.40 % (2407614)Will run a generic schedule for satisfiability detection. % 7.25/1.40 % (2407620)% WARNING: option uhcvi not known. % 7.25/1.40 % (2407620)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=164630646:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.25/1.40 % (2407619)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=736228937_2999 on theBenchmark for (2999ds/0Mi) % 7.25/1.40 % (2407621)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2111440935:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.25/1.40 % (2407622)dis+10_1_sil=32000:sp=arity:random_seed=3819558266:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.25/1.40 % (2407623)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4005995932:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.25/1.40 % (2407624)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3043355113:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.25/1.40 % (2407625)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3907719946:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.25/1.40 % Exception at run slice level % 7.25/1.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.25/1.40 % (2407633)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=626040639:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.25/1.40 % Exception at run slice level % 7.25/1.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.25/1.40 % (2407622)Instruction limit reached! % 7.25/1.40 % (2407622)------------------------------ % 7.25/1.40 % (2407622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.40 % (2407622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.40 % (2407622)CaDiCaL version: 2.1.3 % 7.25/1.40 % (2407622)Termination reason: Instruction limit % 7.25/1.40 % (2407622)Termination phase: Saturation % 7.25/1.40 % (2407622)Time elapsed: 0.051 s % 7.25/1.40 % (2407622)Peak memory usage: 12 MB % 7.25/1.40 % (2407622)Instructions burned: 104 (million) % 7.25/1.40 % (2407635)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=360907813:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.25/1.40 % (2407623)Instruction limit reached! % 7.25/1.40 % (2407623)------------------------------ % 7.25/1.40 % (2407623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.40 % (2407623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.40 % (2407623)CaDiCaL version: 2.1.3 % 7.25/1.40 % (2407623)Termination reason: Instruction limit % 7.25/1.40 % (2407623)Termination phase: Saturation % 7.25/1.40 % (2407623)Time elapsed: 0.066 s % 7.25/1.40 % (2407623)Peak memory usage: 12 MB % 7.25/1.40 % (2407623)Instructions burned: 117 (million) % 7.25/1.40 % (2407636)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=814564020:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.25/1.40 % (2407624)Instruction limit reached! % 7.25/1.40 % (2407624)------------------------------ % 7.25/1.40 % (2407624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.40 % (2407624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.40 % (2407624)CaDiCaL version: 2.1.3 % 7.25/1.40 % (2407624)Termination reason: Instruction limit % 7.25/1.40 % (2407624)Termination phase: Saturation % 7.25/1.40 % (2407624)Time elapsed: 0.074 s % 7.25/1.40 % (2407624)Peak memory usage: 12 MB % 7.25/1.40 % (2407624)Instructions burned: 132 (million) % 7.25/1.40 % (2407625)Instruction limit reached! % 7.25/1.40 % (2407625)------------------------------ % 7.25/1.40 % (2407625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.25/1.40 % (2407625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.40 % (2407625)CaDiCaL version: 2.1.3 % 7.25/1.40 % (2407625)Termination reason: Instruction limit % 7.25/1.40 % (2407625)Termination phase: Saturation % 7.25/1.40 % (2407625)Time elapsed: 0.079 s % 7.25/1.40 % (2407625)Peak memory usage: 13 MB % 7.25/1.40 % (2407625)Instructions burned: 160 (million) % 7.25/1.40 % (2407638)ott-21_1_sil=16000:fs=off:random_seed=2152592607:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.25/1.40 % (2407640)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4294799135:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.31/3.44 % (2407641)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3444891689:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.31/3.44 % Exception at run slice level % 22.31/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.31/3.44 % (2407645)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=210227625:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.31/3.44 % (2407635)Instruction limit reached! % 22.31/3.44 % (2407635)------------------------------ % 22.31/3.44 % (2407635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.31/3.44 % (2407635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.31/3.44 % (2407635)CaDiCaL version: 2.1.3 % 22.31/3.44 % (2407635)Termination reason: Instruction limit % 22.31/3.44 % (2407635)Termination phase: Saturation % 22.31/3.44 % (2407635)Time elapsed: 0.077 s % 22.31/3.44 % (2407635)Peak memory usage: 13 MB % 22.31/3.44 % (2407635)Instructions burned: 131 (million) % 22.31/3.44 % (2407647)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1647896318:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.31/3.44 % Exception at run slice level % 22.31/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.31/3.44 % (2407638)Instruction limit reached! % 22.31/3.44 % (2407638)------------------------------ % 22.31/3.44 % (2407638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.31/3.44 % (2407638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.31/3.44 % (2407638)CaDiCaL version: 2.1.3 % 22.31/3.44 % (2407638)Termination reason: Instruction limit % 22.31/3.44 % (2407638)Termination phase: Saturation % 22.31/3.44 % (2407638)Time elapsed: 0.087 s % 22.31/3.44 % (2407638)Peak memory usage: 12 MB % 22.31/3.44 % (2407638)Instructions burned: 180 (million) % 22.31/3.44 % (2407649)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=3499304874:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 22.31/3.44 % (2407650)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2421570500:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.31/3.44 % (2407640)Instruction limit reached! % 22.31/3.44 % (2407640)------------------------------ % 22.31/3.44 % (2407640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.31/3.44 % (2407640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.31/3.44 % (2407640)CaDiCaL version: 2.1.3 % 22.31/3.44 % (2407640)Termination reason: Instruction limit % 22.31/3.44 % (2407640)Termination phase: Saturation % 22.31/3.44 % (2407640)Time elapsed: 0.248 s % 22.31/3.44 % (2407640)Peak memory usage: 13 MB % 22.31/3.44 % (2407640)Instructions burned: 478 (million) % 22.31/3.44 % (2407653)fmb+10_1_sil=64000:random_seed=961746202:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 22.31/3.44 % (2407653)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.31/3.44 % Exception at run slice level % 22.31/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.31/3.44 % (2407655)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3437160234:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.31/3.44 % Exception at run slice level % 22.31/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.31/3.44 % (2407636)Instruction limit reached! % 22.31/3.44 % (2407636)------------------------------ % 22.31/3.44 % (2407636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.31/3.44 % (2407636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.31/3.44 % (2407636)CaDiCaL version: 2.1.3 % 22.31/3.44 % (2407636)Termination reason: Instruction limit % 22.31/3.44 % (2407636)Termination phase: Saturation % 22.31/3.44 % (2407636)Time elapsed: 0.332 s % 22.31/3.44 % (2407636)Peak memory usage: 14 MB % 22.31/3.44 % (2407636)Instructions burned: 686 (million) % 22.31/3.44 % (2407657)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=234248686:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.31/3.44 % Exception at run slice level % 22.31/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.04/15.00 % (2407658)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=888487637:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 104.04/15.00 % (2407661)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1238065423:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 104.04/15.00 % (2407661)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 104.04/15.00 % (2407649)Instruction limit reached! % 104.04/15.00 % (2407649)------------------------------ % 104.04/15.00 % (2407649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.04/15.00 % (2407649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.04/15.00 % (2407649)CaDiCaL version: 2.1.3 % 104.04/15.00 % (2407649)Termination reason: Instruction limit % 104.04/15.00 % (2407649)Termination phase: Saturation % 104.04/15.00 % (2407649)Time elapsed: 0.348 s % 104.04/15.00 % (2407649)Peak memory usage: 15 MB % 104.04/15.00 % (2407649)Instructions burned: 693 (million) % 104.04/15.00 % (2407663)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1013655079:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 104.04/15.00 % Exception at run slice level % 104.04/15.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.04/15.00 % (2407665)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=263261607:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 104.04/15.00 % Exception at run slice level % 104.04/15.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.04/15.00 % (2407667)ott-2_1_sil=16000:newcnf=on:random_seed=3950296650:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 104.04/15.00 % (2407650)Instruction limit reached! % 104.04/15.00 % (2407650)------------------------------ % 104.04/15.00 % (2407650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.04/15.00 % (2407650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.04/15.00 % (2407650)CaDiCaL version: 2.1.3 % 104.04/15.00 % (2407650)Termination reason: Instruction limit % 104.04/15.00 % (2407650)Termination phase: Saturation % 104.04/15.00 % (2407650)Time elapsed: 0.492 s % 104.04/15.00 % (2407650)Peak memory usage: 18 MB % 104.04/15.00 % (2407650)Instructions burned: 880 (million) % 104.04/15.00 % (2407669)ott+10_1_sil=32000:tgt=ground:random_seed=3783030030:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 104.04/15.00 % (2407645)Instruction limit reached! % 104.04/15.00 % (2407645)------------------------------ % 104.04/15.00 % (2407645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.04/15.00 % (2407645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.04/15.00 % (2407645)CaDiCaL version: 2.1.3 % 104.04/15.00 % (2407645)Termination reason: Instruction limit % 104.04/15.00 % (2407645)Termination phase: Saturation % 104.04/15.00 % (2407645)Time elapsed: 0.619 s % 104.04/15.00 % (2407645)Peak memory usage: 16 MB % 104.04/15.00 % (2407645)Instructions burned: 1179 (million) % 104.04/15.00 % (2407671)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2766242637:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 104.04/15.00 % Exception at run slice level % 104.04/15.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.04/15.00 % (2407673)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2434587875:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 104.04/15.00 % (2407667)Instruction limit reached! % 104.04/15.00 % (2407667)------------------------------ % 104.04/15.00 % (2407667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.04/15.00 % (2407667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.04/15.00 % (2407667)CaDiCaL version: 2.1.3 % 104.04/15.00 % (2407667)Termination reason: Instruction limit % 104.04/15.00 % (2407667)Termination phase: Saturation % 104.04/15.00 % (2407667)Time elapsed: 0.392 s % 104.04/15.00 % (2407667)Peak memory usage: 14 MB % 104.04/15.00 % (2407667)Instructions burned: 871 (million) % 104.04/15.00 % (2407675)dis+21_1_sil=32000:sas=cadical:random_seed=483197877:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 104.04/15.00 % (2407661)Instruction limit reached! % 104.04/15.00 % (2407661)------------------------------ % 104.04/15.00 % (2407661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407661)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407661)Termination reason: Instruction limit % 123.97/17.70 % (2407661)Termination phase: Saturation % 123.97/17.70 % (2407661)Time elapsed: 0.680 s % 123.97/17.70 % (2407661)Peak memory usage: 18 MB % 123.97/17.70 % (2407661)Instructions burned: 1475 (million) % 123.97/17.70 % (2407677)ott+11_1_sil=16000:gs=on:random_seed=3296509867:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 123.97/17.70 % (2407677)Instruction limit reached! % 123.97/17.70 % (2407677)------------------------------ % 123.97/17.70 % (2407677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407677)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407677)Termination reason: Instruction limit % 123.97/17.70 % (2407677)Termination phase: Saturation % 123.97/17.70 % (2407677)Time elapsed: 1.166 s % 123.97/17.70 % (2407677)Peak memory usage: 19 MB % 123.97/17.70 % (2407677)Instructions burned: 2252 (million) % 123.97/17.70 % (2407679)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1347470612:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 123.97/17.70 % Exception at run slice level % 123.97/17.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 123.97/17.70 % (2407681)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=751114947:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi) % 123.97/17.70 % (2407673)Instruction limit reached! % 123.97/17.70 % (2407673)------------------------------ % 123.97/17.70 % (2407673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407673)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407673)Termination reason: Instruction limit % 123.97/17.70 % (2407673)Termination phase: Saturation % 123.97/17.70 % (2407673)Time elapsed: 1.817 s % 123.97/17.70 % (2407673)Peak memory usage: 26 MB % 123.97/17.70 % (2407673)Instructions burned: 3513 (million) % 123.97/17.70 % (2407683)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1863932190:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 123.97/17.70 % (2407658)Instruction limit reached! % 123.97/17.70 % (2407658)------------------------------ % 123.97/17.70 % (2407658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407658)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407658)Termination reason: Instruction limit % 123.97/17.70 % (2407658)Termination phase: Saturation % 123.97/17.70 % (2407658)Time elapsed: 2.576 s % 123.97/17.70 % (2407658)Peak memory usage: 28 MB % 123.97/17.70 % (2407658)Instructions burned: 5131 (million) % 123.97/17.70 % (2407685)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4103022781:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 123.97/17.70 % (2407669)Instruction limit reached! % 123.97/17.70 % (2407669)------------------------------ % 123.97/17.70 % (2407669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407669)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407669)Termination reason: Instruction limit % 123.97/17.70 % (2407669)Termination phase: Saturation % 123.97/17.70 % (2407669)Time elapsed: 2.425 s % 123.97/17.70 % (2407669)Peak memory usage: 18 MB % 123.97/17.70 % (2407669)Instructions burned: 5116 (million) % 123.97/17.70 % (2407687)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3270640857:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 123.97/17.70 % Exception at run slice level % 123.97/17.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 123.97/17.70 % (2407675)Instruction limit reached! % 123.97/17.70 % (2407675)------------------------------ % 123.97/17.70 % (2407675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.97/17.70 % (2407675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.97/17.70 % (2407675)CaDiCaL version: 2.1.3 % 123.97/17.70 % (2407675)Termination reason: Instruction limit % 123.97/17.70 % (2407675)Termination phase: Saturation % 123.97/17.70 % (2407675)Time elapsed: 2.145 s % 186.33/26.59 % (2407675)Peak memory usage: 34 MB % 186.33/26.59 % (2407675)Instructions burned: 3774 (million) % 186.33/26.59 % (2407689)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1740107902:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 186.33/26.59 % (2407690)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1125025677:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 186.33/26.59 % Exception at run slice level % 186.33/26.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.33/26.59 % Exception at run slice level % 186.33/26.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.33/26.59 % (2407693)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=448705913:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 186.33/26.59 % (2407694)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1658102047:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 186.33/26.59 % (2407681)Instruction limit reached! % 186.33/26.59 % (2407681)------------------------------ % 186.33/26.59 % (2407681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.33/26.59 % (2407681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.33/26.59 % (2407681)CaDiCaL version: 2.1.3 % 186.33/26.59 % (2407681)Termination reason: Instruction limit % 186.33/26.59 % (2407681)Termination phase: Saturation % 186.33/26.59 % (2407681)Time elapsed: 1.550 s % 186.33/26.59 % (2407681)Peak memory usage: 18 MB % 186.33/26.59 % (2407681)Instructions burned: 4592 (million) % 186.33/26.59 % (2407697)dis+10_16:1_sil=16000:random_seed=884542086:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 186.33/26.59 % (2407685)Instruction limit reached! % 186.33/26.59 % (2407685)------------------------------ % 186.33/26.59 % (2407685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.33/26.59 % (2407685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.33/26.59 % (2407685)CaDiCaL version: 2.1.3 % 186.33/26.59 % (2407685)Termination reason: Instruction limit % 186.33/26.59 % (2407685)Termination phase: Saturation % 186.33/26.59 % (2407685)Time elapsed: 2.906 s % 186.33/26.59 % (2407685)Peak memory usage: 49 MB % 186.33/26.59 % (2407685)Instructions burned: 5211 (million) % 186.33/26.59 % (2407699)ott-3_8_sil=64000:random_seed=1718617088:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 186.33/26.59 % (2407694)Instruction limit reached! % 186.33/26.59 % (2407694)------------------------------ % 186.33/26.59 % (2407694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.33/26.59 % (2407694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.33/26.59 % (2407694)CaDiCaL version: 2.1.3 % 186.33/26.59 % (2407694)Termination reason: Instruction limit % 186.33/26.59 % (2407694)Termination phase: Saturation % 186.33/26.59 % (2407694)Time elapsed: 4.012 s % 186.33/26.59 % (2407694)Peak memory usage: 23 MB % 186.33/26.59 % (2407694)Instructions burned: 8173 (million) % 186.33/26.59 % (2407701)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2619427480:fmbsr=2:i=32576_2927 on theBenchmark for (2927ds/32576Mi) % 186.33/26.59 % Exception at run slice level % 186.33/26.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.33/26.59 % (2407703)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=346315543:i=11404_2926 on theBenchmark for (2926ds/11404Mi) % 186.33/26.59 % (2407697)Instruction limit reached! % 186.33/26.59 % (2407697)------------------------------ % 186.33/26.59 % (2407697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.33/26.59 % (2407697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.33/26.59 % (2407697)CaDiCaL version: 2.1.3 % 186.33/26.59 % (2407697)Termination reason: Instruction limit % 186.33/26.59 % (2407697)Termination phase: Saturation % 186.33/26.59 % (2407697)Time elapsed: 5.027 s % 186.33/26.59 % (2407697)Peak memory usage: 54 MB % 186.33/26.59 % (2407697)Instructions burned: 9155 (million) % 186.33/26.59 % (2407705)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3341751546:i=14134_2909 on theBenchmark for (2909ds/14134Mi) % 186.33/26.59 % (2407703)Instruction limit reached! % 186.33/26.59 % (2407703)------------------------------ % 186.33/26.59 % (2407703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.33/26.59 % (2407703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.33/26.59 % (2407703)CaDiCaL version: 2.1.3 % 193.08/27.54 % (2407703)Termination reason: Instruction limit % 193.08/27.54 % (2407703)Termination phase: Saturation % 193.08/27.54 % (2407703)Time elapsed: 7.443 s % 193.08/27.54 % (2407703)Peak memory usage: 103 MB % 193.08/27.54 % (2407703)Instructions burned: 11406 (million) % 193.08/27.54 % (2407919)dis+33_16_sil=32000:sac=on:random_seed=3687473850:i=15851:nm=0_2852 on theBenchmark for (2852ds/15851Mi) % 193.08/27.54 % (2407699)Instruction limit reached! % 193.08/27.54 % (2407699)------------------------------ % 193.08/27.54 % (2407699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.08/27.54 % (2407699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.08/27.54 % (2407699)CaDiCaL version: 2.1.3 % 193.08/27.54 % (2407699)Termination reason: Instruction limit % 193.08/27.54 % (2407699)Termination phase: Saturation % 193.08/27.54 % (2407699)Time elapsed: 9.667 s % 193.08/27.54 % (2407699)Peak memory usage: 29 MB % 193.08/27.54 % (2407699)Instructions burned: 20139 (million) % 193.08/27.54 % (2407964)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3079993033:avsq=on:i=17627:add=on:amm=off_2843 on theBenchmark for (2843ds/17627Mi) % 193.08/27.54 % (2407683)Instruction limit reached! % 193.08/27.54 % (2407683)------------------------------ % 193.08/27.54 % (2407683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.08/27.54 % (2407683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.08/27.54 % (2407683)CaDiCaL version: 2.1.3 % 193.08/27.54 % (2407683)Termination reason: Instruction limit % 193.08/27.54 % (2407683)Termination phase: Saturation % 193.08/27.54 % (2407683)Time elapsed: 13.336 s % 193.08/27.54 % (2407683)Peak memory usage: 121 MB % 193.08/27.54 % (2407683)Instructions burned: 29341 (million) % 193.08/27.54 % (2407975)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=591631816:s2a=on:i=53295_2839 on theBenchmark for (2839ds/53295Mi) % 193.08/27.54 % (2407705)Instruction limit reached! % 193.08/27.54 % (2407705)------------------------------ % 193.08/27.54 % (2407705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.08/27.54 % (2407705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.08/27.54 % (2407705)CaDiCaL version: 2.1.3 % 193.08/27.54 % (2407705)Termination reason: Instruction limit % 193.08/27.54 % (2407705)Termination phase: Saturation % 193.08/27.54 % (2407705)Time elapsed: 7.577 s % 193.08/27.54 % (2407705)Peak memory usage: 41 MB % 193.08/27.54 % (2407705)Instructions burned: 14135 (million) % 193.08/27.54 % (2408019)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=560322506:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi) % 193.08/27.54 % Exception at run slice level % 193.08/27.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.08/27.54 % (2408021)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3534523462:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 193.08/27.54 % (2407693)Instruction limit reached! % 193.08/27.54 % (2407693)------------------------------ % 193.08/27.54 % (2407693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.08/27.54 % (2407693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.08/27.54 % (2407693)CaDiCaL version: 2.1.3 % 193.08/27.54 % (2407693)Termination reason: Instruction limit % 193.08/27.54 % (2407693)Termination phase: Saturation % 193.08/27.54 % (2407693)Time elapsed: 14.108 s % 193.08/27.54 % (2407693)Peak memory usage: 81 MB % 193.08/27.54 % (2407693)Instructions burned: 22565 (million) % 193.08/27.54 % (2408023)fmb+10_1_sil=256000:fmbss=7:random_seed=896981726:fmbsr=1.6:i=182295_2826 on theBenchmark for (2826ds/182295Mi) % 193.08/27.54 % Exception at run slice level % 193.08/27.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.08/27.54 % (2408025)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2824323709:i=44625:gsp=on_2825 on theBenchmark for (2825ds/44625Mi) % 193.08/27.54 % (2408025)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 193.08/27.54 % Exception at run slice level % 193.08/27.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.08/27.54 % (2408027)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2029501533:i=160505_2825 on theBenchmark for (2825ds/160505Mi) % 193.08/27.54 % Exception at run slice level % 193.08/27.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.08/27.54 % (2408029)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4047316185:fmbsr=1.3:i=225729_2825 on theBenchmark for (2825ds/225729Mi) % 206.75/29.45 % Exception at run slice level % 206.75/29.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 206.75/29.45 % (2408031)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=918770933:fmbsr=2:i=185024:ins=7_2825 on theBenchmark for (2825ds/185024Mi) % 206.75/29.45 % Exception at run slice level % 206.75/29.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 206.75/29.45 % (2408033)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=141462193:rtra=on_2824 on theBenchmark for (2824ds/0Mi) % 206.75/29.45 % Exception at run slice level % 206.75/29.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 206.75/29.45 % (2408035)% WARNING: option uhcvi not known. % 206.75/29.45 % (2408035)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4171348227:i=271062:add=off:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/271062Mi) % 206.75/29.45 % (2407919)Instruction limit reached! % 206.75/29.45 % (2407919)------------------------------ % 206.75/29.45 % (2407919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.75/29.45 % (2407919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.75/29.45 % (2407919)CaDiCaL version: 2.1.3 % 206.75/29.45 % (2407919)Termination reason: Instruction limit % 206.75/29.45 % (2407919)Termination phase: Saturation % 206.75/29.45 % (2407919)Time elapsed: 7.418 s % 206.75/29.45 % (2407919)Peak memory usage: 29 MB % 206.75/29.45 % (2407919)Instructions burned: 15852 (million) % 206.75/29.45 % (2408037)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3812770545:i=176048:add=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/176048Mi) % 206.75/29.45 % (2407964)Instruction limit reached! % 206.75/29.45 % (2407964)------------------------------ % 206.75/29.45 % (2407964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.75/29.45 % (2407964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.75/29.45 % (2407964)CaDiCaL version: 2.1.3 % 206.75/29.45 % (2407964)Termination reason: Instruction limit % 206.75/29.45 % (2407964)Termination phase: Saturation % 206.75/29.45 % (2407964)Time elapsed: 10.177 s % 206.75/29.45 % (2407964)Peak memory usage: 42 MB % 206.75/29.45 % (2407964)Instructions burned: 17628 (million) % 206.75/29.45 % (2408039)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3412450400:i=206:fgj=on:rtra=on_2741 on theBenchmark for (2741ds/206Mi) % 206.75/29.45 % (2408039)Instruction limit reached! % 206.75/29.45 % (2408039)------------------------------ % 206.75/29.45 % (2408039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.75/29.45 % (2408039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.75/29.45 % (2408039)CaDiCaL version: 2.1.3 % 206.75/29.45 % (2408039)Termination reason: Instruction limit % 206.75/29.45 % (2408039)Termination phase: Saturation % 206.75/29.45 % (2408039)Time elapsed: 0.111 s % 206.75/29.45 % (2408039)Peak memory usage: 12 MB % 206.75/29.45 % (2408039)Instructions burned: 206 (million) % 206.75/29.45 % (2408041)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2033253930:i=232:rtra=on_2739 on theBenchmark for (2739ds/232Mi) % 206.75/29.45 % (2408041)Instruction limit reached! % 206.75/29.45 % (2408041)------------------------------ % 206.75/29.45 % (2408041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.75/29.45 % (2408041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.75/29.45 % (2408041)CaDiCaL version: 2.1.3 % 206.75/29.45 % (2408041)Termination reason: Instruction limit % 206.75/29.45 % (2408041)Termination phase: Saturation % 206.75/29.45 % (2408041)Time elapsed: 0.142 s % 206.75/29.45 % (2408041)Peak memory usage: 13 MB % 206.75/29.45 % (2408041)Instructions burned: 232 (million) % 206.75/29.45 % (2408043)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=704489259:i=262:rtra=on_2738 on theBenchmark for (2738ds/262Mi) % 206.75/29.45 % (2408043)Instruction limit reached! % 206.75/29.45 % (2408043)------------------------------ % 206.75/29.45 % (2408043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.75/29.45 % (2408043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.75/29.45 % (2408043)CaDiCaL version: 2.1.3 % 206.75/29.45 % (2408043)Termination reason: Instruction limit % 206.75/29.45 % (2408043)Termination phase: Saturation % 276.62/39.30 % (2408043)Time elapsed: 0.158 s % 276.62/39.30 % (2408043)Peak memory usage: 13 MB % 276.62/39.30 % (2408043)Instructions burned: 263 (million) % 276.62/39.30 % (2408045)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2775514810:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2736 on theBenchmark for (2736ds/318Mi) % 276.62/39.30 % (2408021)Instruction limit reached! % 276.62/39.30 % (2408021)------------------------------ % 276.62/39.30 % (2408021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.62/39.30 % (2408021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.62/39.30 % (2408021)CaDiCaL version: 2.1.3 % 276.62/39.30 % (2408021)Termination reason: Instruction limit % 276.62/39.30 % (2408021)Termination phase: Saturation % 276.62/39.30 % (2408021)Time elapsed: 9.732 s % 276.62/39.30 % (2408021)Peak memory usage: 26 MB % 276.62/39.30 % (2408021)Instructions burned: 28120 (million) % 276.62/39.30 % (2408047)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3728852432:i=1428:nm=2:rtra=on_2735 on theBenchmark for (2735ds/1428Mi) % 276.62/39.30 % Exception at run slice level % 276.62/39.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.62/39.30 % (2408049)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3070146016:i=262:bd=preordered:rtra=on:fsd=on_2735 on theBenchmark for (2735ds/262Mi) % 276.62/39.30 % (2408045)Instruction limit reached! % 276.62/39.30 % (2408045)------------------------------ % 276.62/39.30 % (2408045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.62/39.30 % (2408045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.62/39.30 % (2408045)CaDiCaL version: 2.1.3 % 276.62/39.30 % (2408045)Termination reason: Instruction limit % 276.62/39.30 % (2408045)Termination phase: Saturation % 276.62/39.30 % (2408045)Time elapsed: 0.167 s % 276.62/39.30 % (2408045)Peak memory usage: 13 MB % 276.62/39.30 % (2408045)Instructions burned: 318 (million) % 276.62/39.30 % (2408051)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=2512742336:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2734 on theBenchmark for (2734ds/1368Mi) % 276.62/39.30 % (2408049)Instruction limit reached! % 276.62/39.30 % (2408049)------------------------------ % 276.62/39.30 % (2408049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.62/39.30 % (2408049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.62/39.30 % (2408049)CaDiCaL version: 2.1.3 % 276.62/39.30 % (2408049)Termination reason: Instruction limit % 276.62/39.30 % (2408049)Termination phase: Saturation % 276.62/39.30 % (2408049)Time elapsed: 0.155 s % 276.62/39.30 % (2408049)Peak memory usage: 13 MB % 276.62/39.30 % (2408049)Instructions burned: 263 (million) % 276.62/39.30 % (2408053)ott-21_1_sil=16000:si=on:fs=off:random_seed=2625302681:i=360:av=off:fsr=off:rtra=on_2733 on theBenchmark for (2733ds/360Mi) % 276.62/39.30 % (2408053)Instruction limit reached! % 276.62/39.30 % (2408053)------------------------------ % 276.62/39.30 % (2408053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.62/39.30 % (2408053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.62/39.30 % (2408053)CaDiCaL version: 2.1.3 % 276.62/39.30 % (2408053)Termination reason: Instruction limit % 276.62/39.30 % (2408053)Termination phase: Saturation % 276.62/39.30 % (2408053)Time elapsed: 0.177 s % 276.62/39.30 % (2408053)Peak memory usage: 13 MB % 276.62/39.30 % (2408053)Instructions burned: 360 (million) % 276.62/39.30 % (2408055)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3379807347:i=954:bd=all:rtra=on_2731 on theBenchmark for (2731ds/954Mi) % 276.62/39.30 % (2408051)Instruction limit reached! % 276.62/39.30 % (2408051)------------------------------ % 276.62/39.30 % (2408051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.62/39.30 % (2408051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.62/39.30 % (2408051)CaDiCaL version: 2.1.3 % 276.62/39.30 % (2408051)Termination reason: Instruction limit % 276.62/39.30 % (2408051)Termination phase: Saturation % 276.62/39.30 % (2408051)Time elapsed: 0.710 s % 276.62/39.30 % (2408051)Peak memory usage: 17 MB % 276.62/39.30 % (2408051)Instructions burned: 1369 (million) % 276.62/39.30 % (2408057)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2721919672:fmbsr=1.3:i=1730:ins=25:rtra=on_2727 on theBenchmark for (2727ds/1730Mi) % 276.62/39.30 % Exception at run slice level % 276.62/39.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 293.21/41.64 % (2408059)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1379593919:i=2358:rtra=on_2726 on theBenchmark for (2726ds/2358Mi) % 293.21/41.64 % (2408055)Instruction limit reached! % 293.21/41.64 % (2408055)------------------------------ % 293.21/41.64 % (2408055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.21/41.64 % (2408055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.21/41.64 % (2408055)CaDiCaL version: 2.1.3 % 293.21/41.64 % (2408055)Termination reason: Instruction limit % 293.21/41.64 % (2408055)Termination phase: Saturation % 293.21/41.64 % (2408055)Time elapsed: 0.553 s % 293.21/41.64 % (2408055)Peak memory usage: 15 MB % 293.21/41.64 % (2408055)Instructions burned: 954 (million) % 293.21/41.64 % (2408061)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2572155486:i=1778:ins=1:rtra=on_2726 on theBenchmark for (2726ds/1778Mi) % 293.21/41.64 % Exception at run slice level % 293.21/41.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 293.21/41.64 % (2408063)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=3959512819:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/1384Mi) % 293.21/41.65 % (2408063)Instruction limit reached! % 293.21/41.65 % (2408063)------------------------------ % 293.21/41.65 % (2408063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.21/41.65 % (2408063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.21/41.65 % (2408063)CaDiCaL version: 2.1.3 % 293.21/41.65 % (2408063)Termination reason: Instruction limit % 293.21/41.65 % (2408063)Termination phase: Saturation % 293.21/41.65 % (2408063)Time elapsed: 0.773 s % 293.21/41.65 % (2408063)Peak memory usage: 17 MB % 293.21/41.65 % (2408063)Instructions burned: 1385 (million) % 293.21/41.65 % (2408065)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3021961113:i=1758:kws=inv_precedence:fsr=off:rtra=on_2717 on theBenchmark for (2717ds/1758Mi) % 293.21/41.65 % (2408059)Instruction limit reached! % 293.21/41.65 % (2408059)------------------------------ % 293.21/41.65 % (2408059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.21/41.65 % (2408059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.21/41.65 % (2408059)CaDiCaL version: 2.1.3 % 293.21/41.65 % (2408059)Termination reason: Instruction limit % 293.21/41.65 % (2408059)Termination phase: Saturation % 293.21/41.65 % (2408059)Time elapsed: 1.444 s % 293.21/41.65 % (2408059)Peak memory usage: 23 MB % 293.21/41.65 % (2408059)Instructions burned: 2358 (million) % 293.21/41.65 % (2408069)fmb+10_1_sil=64000:si=on:random_seed=341815354:i=44122:nm=2:rtra=on:gsp=on_2712 on theBenchmark for (2712ds/44122Mi) % 293.21/41.65 % (2408069)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 293.21/41.65 % Exception at run slice level % 293.21/41.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 293.21/41.65 % (2408071)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1049739766:i=19030:nm=5:rtra=on_2711 on theBenchmark for (2711ds/19030Mi) % 293.21/41.65 % Exception at run slice level % 293.21/41.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 293.21/41.65 % (2408073)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=862370223:fmbsr=1.7:i=1840:rtra=on_2711 on theBenchmark for (2711ds/1840Mi) % 293.21/41.65 % Exception at run slice level % 293.21/41.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 293.21/41.65 % (2408075)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=173015177:i=10262:rtra=on_2711 on theBenchmark for (2711ds/10262Mi) % 293.21/41.65 % (2408065)Instruction limit reached! % 293.21/41.65 % (2408065)------------------------------ % 293.21/41.65 % (2408065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.21/41.65 % (2408065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.21/41.65 % (2408065)CaDiCaL version: 2.1.3 % 293.21/41.65 % (2408065)Termination reason: Instruction limit % 293.21/41.65 % (2408065)Termination phase: Saturation % 293.21/41.65 % (2408065)Time elapsed: 1.004 s % 293.21/41.65 % (2408065)Peak memory usage: 22 MB % 293.21/41.65 % (2408Terminated % 300.06/42.54 % Vampire exiting %------------------------------------------------------------------------------