%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV605_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 : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:06 PM UTC 2026 % Result : Timeout 300.48s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV605_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n006.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 12:00:10 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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.18/1.37 % (3916591)Will run a generic schedule for satisfiability detection. % 7.18/1.37 % (3916600)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3205317277:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.18/1.37 % (3916597)% WARNING: option uhcvi not known. % 7.18/1.37 % (3916599)dis+10_1_sil=32000:sp=arity:random_seed=2229825791:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.18/1.37 % (3916596)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1173055114_2999 on theBenchmark for (2999ds/0Mi) % 7.18/1.37 % (3916598)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3351347719:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.18/1.37 % (3916597)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3673324080:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.18/1.37 % (3916601)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3325387930:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.18/1.37 % (3916602)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3977683207:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.18/1.37 % Exception at run slice level % 7.18/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.18/1.37 % (3916610)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4162082069:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.18/1.37 % Exception at run slice level % 7.18/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.18/1.37 % (3916600)Instruction limit reached! % 7.18/1.37 % (3916600)------------------------------ % 7.18/1.37 % (3916600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.18/1.37 % (3916600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.37 % (3916600)CaDiCaL version: 2.1.3 % 7.18/1.37 % (3916600)Termination reason: Instruction limit % 7.18/1.37 % (3916600)Termination phase: Saturation % 7.18/1.37 % (3916600)Time elapsed: 0.037 s % 7.18/1.37 % (3916600)Peak memory usage: 13 MB % 7.18/1.37 % (3916600)Instructions burned: 117 (million) % 7.18/1.37 % (3916613)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=2051275648:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.18/1.37 % (3916612)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3048210982:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.18/1.37 % (3916599)Instruction limit reached! % 7.18/1.37 % (3916599)------------------------------ % 7.18/1.37 % (3916599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.18/1.37 % (3916599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.37 % (3916599)CaDiCaL version: 2.1.3 % 7.18/1.37 % (3916599)Termination reason: Instruction limit % 7.18/1.37 % (3916599)Termination phase: Saturation % 7.18/1.37 % (3916599)Time elapsed: 0.059 s % 7.18/1.37 % (3916599)Peak memory usage: 12 MB % 7.18/1.37 % (3916599)Instructions burned: 104 (million) % 7.18/1.37 % (3916601)Instruction limit reached! % 7.18/1.37 % (3916601)------------------------------ % 7.18/1.37 % (3916601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.18/1.37 % (3916601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.37 % (3916601)CaDiCaL version: 2.1.3 % 7.18/1.37 % (3916601)Termination reason: Instruction limit % 7.18/1.37 % (3916601)Termination phase: Saturation % 7.18/1.37 % (3916601)Time elapsed: 0.070 s % 7.18/1.37 % (3916601)Peak memory usage: 12 MB % 7.18/1.37 % (3916601)Instructions burned: 131 (million) % 7.18/1.37 % (3916616)ott-21_1_sil=16000:fs=off:random_seed=848111374:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.18/1.37 % (3916602)Instruction limit reached! % 7.18/1.37 % (3916602)------------------------------ % 7.18/1.37 % (3916602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.18/1.37 % (3916602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.37 % (3916602)CaDiCaL version: 2.1.3 % 7.18/1.37 % (3916602)Termination reason: Instruction limit % 7.18/1.37 % (3916602)Termination phase: Saturation % 7.18/1.37 % (3916602)Time elapsed: 0.085 s % 7.18/1.37 % (3916602)Peak memory usage: 12 MB % 7.18/1.37 % (3916602)Instructions burned: 160 (million) % 7.18/1.37 % (3916617)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=97655796:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.73/3.10 % (3916619)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2317842184:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.73/3.10 % Exception at run slice level % 19.73/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.73/3.10 % (3916622)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=584420043:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.73/3.10 % (3916612)Instruction limit reached! % 19.73/3.10 % (3916612)------------------------------ % 19.73/3.10 % (3916612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.73/3.10 % (3916612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.10 % (3916612)CaDiCaL version: 2.1.3 % 19.73/3.10 % (3916612)Termination reason: Instruction limit % 19.73/3.10 % (3916612)Termination phase: Saturation % 19.73/3.10 % (3916612)Time elapsed: 0.083 s % 19.73/3.10 % (3916612)Peak memory usage: 13 MB % 19.73/3.10 % (3916612)Instructions burned: 131 (million) % 19.73/3.10 % (3916624)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3779121603:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.73/3.10 % Exception at run slice level % 19.73/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.73/3.10 % (3916616)Instruction limit reached! % 19.73/3.10 % (3916616)------------------------------ % 19.73/3.10 % (3916616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.73/3.10 % (3916616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.10 % (3916616)CaDiCaL version: 2.1.3 % 19.73/3.10 % (3916616)Termination reason: Instruction limit % 19.73/3.10 % (3916616)Termination phase: Saturation % 19.73/3.10 % (3916616)Time elapsed: 0.076 s % 19.73/3.10 % (3916616)Peak memory usage: 12 MB % 19.73/3.10 % (3916616)Instructions burned: 180 (million) % 19.73/3.10 % (3916626)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=144836249:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 19.73/3.10 % (3916627)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4136210942:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 19.73/3.10 % (3916613)Instruction limit reached! % 19.73/3.10 % (3916613)------------------------------ % 19.73/3.10 % (3916613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.73/3.10 % (3916613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.10 % (3916613)CaDiCaL version: 2.1.3 % 19.73/3.10 % (3916613)Termination reason: Instruction limit % 19.73/3.10 % (3916613)Termination phase: Saturation % 19.73/3.10 % (3916613)Time elapsed: 0.180 s % 19.73/3.10 % (3916613)Peak memory usage: 16 MB % 19.73/3.10 % (3916613)Instructions burned: 686 (million) % 19.73/3.10 % (3916630)fmb+10_1_sil=64000:random_seed=210010178:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 19.73/3.10 % (3916630)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.73/3.10 % Exception at run slice level % 19.73/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.73/3.10 % (3916632)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1183723651:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 19.73/3.10 % Exception at run slice level % 19.73/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.73/3.10 % (3916634)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=328731091:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 19.73/3.10 % Exception at run slice level % 19.73/3.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.73/3.10 % (3916636)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2966735975:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 19.73/3.10 % (3916617)Instruction limit reached! % 19.73/3.10 % (3916617)------------------------------ % 19.73/3.10 % (3916617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.73/3.10 % (3916617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3916617)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3916617)Termination reason: Instruction limit % 64.19/9.31 % (3916617)Termination phase: Saturation % 64.19/9.31 % (3916617)Time elapsed: 0.284 s % 64.19/9.31 % (3916617)Peak memory usage: 14 MB % 64.19/9.31 % (3916617)Instructions burned: 478 (million) % 64.19/9.31 % (3916638)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1327577687:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 64.19/9.31 % (3916638)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.19/9.31 % (3916626)Instruction limit reached! % 64.19/9.31 % (3916626)------------------------------ % 64.19/9.31 % (3916626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3916626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3916626)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3916626)Termination reason: Instruction limit % 64.19/9.31 % (3916626)Termination phase: Saturation % 64.19/9.31 % (3916626)Time elapsed: 0.367 s % 64.19/9.31 % (3916626)Peak memory usage: 17 MB % 64.19/9.31 % (3916626)Instructions burned: 693 (million) % 64.19/9.31 % (3916640)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3182076628:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 64.19/9.31 % Exception at run slice level % 64.19/9.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.19/9.31 % (3916642)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=489227955:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 64.19/9.31 % Exception at run slice level % 64.19/9.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.19/9.31 % (3916644)ott-2_1_sil=16000:newcnf=on:random_seed=2555433157:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 64.19/9.31 % (3916627)Instruction limit reached! % 64.19/9.31 % (3916627)------------------------------ % 64.19/9.31 % (3916627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3916627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3916627)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3916627)Termination reason: Instruction limit % 64.19/9.31 % (3916627)Termination phase: Saturation % 64.19/9.31 % (3916627)Time elapsed: 0.490 s % 64.19/9.31 % (3916627)Peak memory usage: 18 MB % 64.19/9.31 % (3916627)Instructions burned: 880 (million) % 64.19/9.31 % (3916646)ott+10_1_sil=32000:tgt=ground:random_seed=253484637:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.19/9.31 % (3916622)Instruction limit reached! % 64.19/9.31 % (3916622)------------------------------ % 64.19/9.31 % (3916622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3916622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3916622)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3916622)Termination reason: Instruction limit % 64.19/9.31 % (3916622)Termination phase: Saturation % 64.19/9.31 % (3916622)Time elapsed: 0.624 s % 64.19/9.31 % (3916622)Peak memory usage: 19 MB % 64.19/9.31 % (3916622)Instructions burned: 1181 (million) % 64.19/9.31 % (3916648)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3158966467:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 64.19/9.31 % Exception at run slice level % 64.19/9.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.19/9.31 % (3916650)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=386556441:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 64.19/9.31 % (3916644)Instruction limit reached! % 64.19/9.31 % (3916644)------------------------------ % 64.19/9.31 % (3916644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3916644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3916644)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3916644)Termination reason: Instruction limit % 64.19/9.31 % (3916644)Termination phase: Saturation % 64.19/9.31 % (3916644)Time elapsed: 0.405 s % 64.19/9.31 % (3916644)Peak memory usage: 16 MB % 64.19/9.31 % (3916644)Instructions burned: 871 (million) % 64.19/9.31 % (3916652)dis+21_1_sil=32000:sas=cadical:random_seed=2000064909:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 64.19/9.31 % (3916638)Instruction limit reached! % 64.19/9.31 % (3916638)------------------------------ % 64.19/9.31 % (3916638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.24/16.29 % (3916638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.24/16.29 % (3916638)CaDiCaL version: 2.1.3 % 102.24/16.29 % (3916638)Termination reason: Instruction limit % 102.24/16.29 % (3916638)Termination phase: Saturation % 102.24/16.29 % (3916638)Time elapsed: 0.686 s % 102.24/16.29 % (3916638)Peak memory usage: 23 MB % 102.24/16.29 % (3916638)Instructions burned: 1472 (million) % 102.24/16.29 % (3916654)ott+11_1_sil=16000:gs=on:random_seed=1311555876:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 102.24/16.29 % (3916636)Instruction limit reached! % 102.24/16.29 % (3916636)------------------------------ % 102.24/16.29 % (3916636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.24/16.29 % (3916636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.24/16.29 % (3916636)CaDiCaL version: 2.1.3 % 102.24/16.29 % (3916636)Termination reason: Instruction limit % 102.24/16.29 % (3916636)Termination phase: Saturation % 102.24/16.29 % (3916636)Time elapsed: 1.334 s % 102.24/16.29 % (3916636)Peak memory usage: 34 MB % 102.24/16.29 % (3916636)Instructions burned: 5134 (million) % 102.24/16.29 % (3916656)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1447781631:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 102.24/16.29 % Exception at run slice level % 102.24/16.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.24/16.29 % (3916658)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3902388224:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 102.24/16.29 % (3916654)Instruction limit reached! % 102.24/16.29 % (3916654)------------------------------ % 102.24/16.29 % (3916654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.24/16.29 % (3916654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.24/16.29 % (3916654)CaDiCaL version: 2.1.3 % 102.24/16.29 % (3916654)Termination reason: Instruction limit % 102.24/16.29 % (3916654)Termination phase: Saturation % 102.24/16.29 % (3916654)Time elapsed: 1.173 s % 102.24/16.29 % (3916654)Peak memory usage: 20 MB % 102.24/16.29 % (3916654)Instructions burned: 2252 (million) % 102.24/16.29 % (3916660)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3473237536:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 102.24/16.29 % (3916650)Instruction limit reached! % 102.24/16.29 % (3916650)------------------------------ % 102.24/16.29 % (3916650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.24/16.29 % (3916650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.24/16.29 % (3916650)CaDiCaL version: 2.1.3 % 102.24/16.29 % (3916650)Termination reason: Instruction limit % 102.24/16.29 % (3916650)Termination phase: Saturation % 102.24/16.29 % (3916650)Time elapsed: 1.699 s % 102.24/16.29 % (3916650)Peak memory usage: 28 MB % 102.24/16.29 % (3916650)Instructions burned: 3513 (million) % 102.24/16.29 % (3916662)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=418443357:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 102.24/16.29 % (3916658)Instruction limit reached! % 102.24/16.29 % (3916658)------------------------------ % 102.24/16.29 % (3916658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.24/16.29 % (3916658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.24/16.29 % (3916658)CaDiCaL version: 2.1.3 % 102.24/16.29 % (3916658)Termination reason: Instruction limit % 102.24/16.29 % (3916658)Termination phase: Saturation % 102.24/16.29 % (3916658)Time elapsed: 1.123 s % 102.24/16.29 % (3916658)Peak memory usage: 43 MB % 102.24/16.29 % (3916658)Instructions burned: 4593 (million) % 102.24/16.29 % (3916664)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=205638739:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 102.24/16.29 % Exception at run slice level % 102.24/16.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.24/16.29 % (3916666)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1980644524:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 102.24/16.29 % Exception at run slice level % 102.24/16.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.24/16.29 % (3916668)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3333270193:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 102.24/16.29 % Exception at run slice level % 127.24/18.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 127.24/18.29 % (3916670)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4092544291:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 127.24/18.29 % (3916652)Instruction limit reached! % 127.24/18.29 % (3916652)------------------------------ % 127.24/18.29 % (3916652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916652)CaDiCaL version: 2.1.3 % 127.24/18.29 % (3916652)Termination reason: Instruction limit % 127.24/18.29 % (3916652)Termination phase: Saturation % 127.24/18.29 % (3916652)Time elapsed: 1.845 s % 127.24/18.29 % (3916652)Peak memory usage: 30 MB % 127.24/18.29 % (3916652)Instructions burned: 3774 (million) % 127.24/18.29 % (3916672)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2632795417:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi) % 127.24/18.29 % (3916646)Instruction limit reached! % 127.24/18.29 % (3916646)------------------------------ % 127.24/18.29 % (3916646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916646)CaDiCaL version: 2.1.3 % 127.24/18.29 % (3916646)Termination reason: Instruction limit % 127.24/18.29 % (3916646)Termination phase: Saturation % 127.24/18.29 % (3916646)Time elapsed: 2.759 s % 127.24/18.29 % (3916646)Peak memory usage: 38 MB % 127.24/18.29 % (3916646)Instructions burned: 5116 (million) % 127.24/18.29 % (3916674)dis+10_16:1_sil=16000:random_seed=3688594972:i=9155:fsr=off_2965 on theBenchmark for (2965ds/9155Mi) % 127.24/18.29 % (3916662)Instruction limit reached! % 127.24/18.29 % (3916662)------------------------------ % 127.24/18.29 % (3916662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916662)CaDiCaL version: 2.1.3 % 127.24/18.29 % (3916662)Termination reason: Instruction limit % 127.24/18.29 % (3916662)Termination phase: Saturation % 127.24/18.29 % (3916662)Time elapsed: 2.604 s % 127.24/18.29 % (3916662)Peak memory usage: 43 MB % 127.24/18.29 % (3916662)Instructions burned: 5212 (million) % 127.24/18.29 % (3916676)ott-3_8_sil=64000:random_seed=2594131804:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 127.24/18.29 % (3916672)Instruction limit reached! % 127.24/18.29 % (3916672)------------------------------ % 127.24/18.29 % (3916672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916672)CaDiCaL version: 2.1.3 % 127.24/18.29 % (3916672)Termination reason: Instruction limit % 127.24/18.29 % (3916672)Termination phase: Saturation % 127.24/18.29 % (3916672)Time elapsed: 4.480 s % 127.24/18.29 % (3916672)Peak memory usage: 44 MB % 127.24/18.29 % (3916672)Instructions burned: 8174 (million) % 127.24/18.29 % (3916678)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2984299600:fmbsr=2:i=32576_2925 on theBenchmark for (2925ds/32576Mi) % 127.24/18.29 % Exception at run slice level % 127.24/18.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 127.24/18.29 % (3916680)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2080405426:i=11404_2925 on theBenchmark for (2925ds/11404Mi) % 127.24/18.29 % (3916674)Instruction limit reached! % 127.24/18.29 % (3916674)------------------------------ % 127.24/18.29 % (3916674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916674)CaDiCaL version: 2.1.3 % 127.24/18.29 % (3916674)Termination reason: Instruction limit % 127.24/18.29 % (3916674)Termination phase: Saturation % 127.24/18.29 % (3916674)Time elapsed: 4.354 s % 127.24/18.29 % (3916674)Peak memory usage: 50 MB % 127.24/18.29 % (3916674)Instructions burned: 9157 (million) % 127.24/18.29 % (3916682)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=583752726:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 127.24/18.29 % (3916670)Instruction limit reached! % 127.24/18.29 % (3916670)------------------------------ % 127.24/18.29 % (3916670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.24/18.29 % (3916670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.24/18.29 % (3916670)CaDiCaL version: 2.1.3 % 134.43/19.28 % (3916670)Termination reason: Instruction limit % 134.43/19.28 % (3916670)Termination phase: Saturation % 134.43/19.28 % (3916670)Time elapsed: 6.194 s % 134.43/19.28 % (3916670)Peak memory usage: 34 MB % 134.43/19.28 % (3916670)Instructions burned: 22568 (million) % 134.43/19.28 % (3916684)dis+33_16_sil=32000:sac=on:random_seed=3860102930:i=15851:nm=0_2909 on theBenchmark for (2909ds/15851Mi) % 134.43/19.28 % (3916684)Instruction limit reached! % 134.43/19.28 % (3916684)------------------------------ % 134.43/19.28 % (3916684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.43/19.28 % (3916684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.43/19.28 % (3916684)CaDiCaL version: 2.1.3 % 134.43/19.28 % (3916684)Termination reason: Instruction limit % 134.43/19.28 % (3916684)Termination phase: Saturation % 134.43/19.28 % (3916684)Time elapsed: 4.189 s % 134.43/19.28 % (3916684)Peak memory usage: 62 MB % 134.43/19.28 % (3916684)Instructions burned: 15855 (million) % 134.43/19.28 % (3916686)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=286006187:avsq=on:i=17627:add=on:amm=off_2867 on theBenchmark for (2867ds/17627Mi) % 134.43/19.28 % (3916680)Instruction limit reached! % 134.43/19.28 % (3916680)------------------------------ % 134.43/19.28 % (3916680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.43/19.28 % (3916680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.43/19.28 % (3916680)CaDiCaL version: 2.1.3 % 134.43/19.28 % (3916680)Termination reason: Instruction limit % 134.43/19.28 % (3916680)Termination phase: Saturation % 134.43/19.28 % (3916680)Time elapsed: 5.972 s % 134.43/19.28 % (3916680)Peak memory usage: 65 MB % 134.43/19.28 % (3916680)Instructions burned: 11405 (million) % 134.43/19.28 % (3916688)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=846464523:s2a=on:i=53295_2865 on theBenchmark for (2865ds/53295Mi) % 134.43/19.28 % (3916682)Instruction limit reached! % 134.43/19.28 % (3916682)------------------------------ % 134.43/19.28 % (3916682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.43/19.28 % (3916682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.43/19.28 % (3916682)CaDiCaL version: 2.1.3 % 134.43/19.28 % (3916682)Termination reason: Instruction limit % 134.43/19.28 % (3916682)Termination phase: Saturation % 134.43/19.28 % (3916682)Time elapsed: 7.440 s % 134.43/19.28 % (3916682)Peak memory usage: 72 MB % 134.43/19.28 % (3916682)Instructions burned: 14134 (million) % 134.43/19.28 % (3916690)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1227209001:i=26857:ins=20_2846 on theBenchmark for (2846ds/26857Mi) % 134.43/19.28 % Exception at run slice level % 134.43/19.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.43/19.28 % (3916692)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=46691116:i=28120:bs=on:fsr=off_2846 on theBenchmark for (2846ds/28120Mi) % 134.43/19.28 % (3916676)Instruction limit reached! % 134.43/19.28 % (3916676)------------------------------ % 134.43/19.28 % (3916676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.43/19.28 % (3916676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.43/19.28 % (3916676)CaDiCaL version: 2.1.3 % 134.43/19.28 % (3916676)Termination reason: Instruction limit % 134.43/19.28 % (3916676)Termination phase: Saturation % 134.43/19.28 % (3916676)Time elapsed: 10.759 s % 134.43/19.28 % (3916676)Peak memory usage: 69 MB % 134.43/19.28 % (3916676)Instructions burned: 20140 (million) % 134.43/19.28 % (3916694)fmb+10_1_sil=256000:fmbss=7:random_seed=1473649427:fmbsr=1.6:i=182295_2840 on theBenchmark for (2840ds/182295Mi) % 134.43/19.28 % Exception at run slice level % 134.43/19.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.43/19.28 % (3916696)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1629026594:i=44625:gsp=on_2840 on theBenchmark for (2840ds/44625Mi) % 134.43/19.28 % (3916696)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 134.43/19.28 % Exception at run slice level % 134.43/19.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.43/19.28 % (3916698)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4266279402:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 134.43/19.28 % Exception at run slice level % 134.43/19.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.43/19.28 % (3916700)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4038090949:fmbsr=1.3:i=225729_2839 on theBenchmark for (2839ds/225729Mi) % 184.09/26.24 % Exception at run slice level % 184.09/26.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.09/26.24 % (3916702)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2381225896:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 184.09/26.24 % Exception at run slice level % 184.09/26.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.09/26.24 % (3916704)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=314201012:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 184.09/26.24 % Exception at run slice level % 184.09/26.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.09/26.24 % (3916706)% WARNING: option uhcvi not known. % 184.09/26.24 % (3916706)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3087867156:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi) % 184.09/26.24 % (3916660)Instruction limit reached! % 184.09/26.24 % (3916660)------------------------------ % 184.09/26.24 % (3916660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.09/26.24 % (3916660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.09/26.24 % (3916660)CaDiCaL version: 2.1.3 % 184.09/26.24 % (3916660)Termination reason: Instruction limit % 184.09/26.24 % (3916660)Termination phase: Saturation % 184.09/26.24 % (3916660)Time elapsed: 14.111 s % 184.09/26.24 % (3916660)Peak memory usage: 91 MB % 184.09/26.24 % (3916660)Instructions burned: 29342 (million) % 184.09/26.24 % (3916708)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=308611823:i=176048:add=on:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/176048Mi) % 184.09/26.24 % (3916686)Instruction limit reached! % 184.09/26.24 % (3916686)------------------------------ % 184.09/26.24 % (3916686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.09/26.24 % (3916686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.09/26.24 % (3916686)CaDiCaL version: 2.1.3 % 184.09/26.24 % (3916686)Termination reason: Instruction limit % 184.09/26.24 % (3916686)Termination phase: Saturation % 184.09/26.24 % (3916686)Time elapsed: 4.503 s % 184.09/26.24 % (3916686)Peak memory usage: 154 MB % 184.09/26.24 % (3916686)Instructions burned: 17629 (million) % 184.09/26.24 % (3916710)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3956123498:i=206:fgj=on:rtra=on_2821 on theBenchmark for (2821ds/206Mi) % 184.09/26.24 % (3916710)Instruction limit reached! % 184.09/26.24 % (3916710)------------------------------ % 184.09/26.24 % (3916710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.09/26.24 % (3916710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.09/26.24 % (3916710)CaDiCaL version: 2.1.3 % 184.09/26.24 % (3916710)Termination reason: Instruction limit % 184.09/26.24 % (3916710)Termination phase: Saturation % 184.09/26.24 % (3916710)Time elapsed: 0.061 s % 184.09/26.24 % (3916710)Peak memory usage: 14 MB % 184.09/26.24 % (3916710)Instructions burned: 207 (million) % 184.09/26.24 % (3916712)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1316932639:i=232:rtra=on_2821 on theBenchmark for (2821ds/232Mi) % 184.09/26.24 % (3916712)Instruction limit reached! % 184.09/26.24 % (3916712)------------------------------ % 184.09/26.24 % (3916712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.09/26.24 % (3916712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.09/26.24 % (3916712)CaDiCaL version: 2.1.3 % 184.09/26.24 % (3916712)Termination reason: Instruction limit % 184.09/26.24 % (3916712)Termination phase: Saturation % 184.09/26.24 % (3916712)Time elapsed: 0.070 s % 184.09/26.24 % (3916712)Peak memory usage: 14 MB % 184.09/26.24 % (3916712)Instructions burned: 235 (million) % 184.09/26.24 % (3916714)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=833383344:i=262:rtra=on_2820 on theBenchmark for (2820ds/262Mi) % 184.09/26.24 % (3916714)Instruction limit reached! % 184.09/26.24 % (3916714)------------------------------ % 184.09/26.24 % (3916714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.09/26.24 % (3916714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.09/26.24 % (3916714)CaDiCaL version: 2.1.3 % 184.09/26.24 % (3916714)Termination reason: Instruction limit % 184.09/26.24 % (3916714)Termination phase: Saturation % 224.43/31.90 % (3916714)Time elapsed: 0.074 s % 224.43/31.90 % (3916714)Peak memory usage: 13 MB % 224.43/31.90 % (3916714)Instructions burned: 263 (million) % 224.43/31.90 % (3916716)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3481030054:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2819 on theBenchmark for (2819ds/318Mi) % 224.43/31.90 % (3916716)Instruction limit reached! % 224.43/31.90 % (3916716)------------------------------ % 224.43/31.90 % (3916716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.43/31.90 % (3916716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.43/31.90 % (3916716)CaDiCaL version: 2.1.3 % 224.43/31.90 % (3916716)Termination reason: Instruction limit % 224.43/31.90 % (3916716)Termination phase: Saturation % 224.43/31.90 % (3916716)Time elapsed: 0.094 s % 224.43/31.90 % (3916716)Peak memory usage: 14 MB % 224.43/31.90 % (3916716)Instructions burned: 319 (million) % 224.43/31.90 % (3916718)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4184842020:i=1428:nm=2:rtra=on_2818 on theBenchmark for (2818ds/1428Mi) % 224.43/31.90 % Exception at run slice level % 224.43/31.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 224.43/31.90 % (3916720)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2359447502:i=262:bd=preordered:rtra=on:fsd=on_2818 on theBenchmark for (2818ds/262Mi) % 224.43/31.90 % (3916720)Instruction limit reached! % 224.43/31.90 % (3916720)------------------------------ % 224.43/31.90 % (3916720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.43/31.90 % (3916720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.43/31.90 % (3916720)CaDiCaL version: 2.1.3 % 224.43/31.90 % (3916720)Termination reason: Instruction limit % 224.43/31.90 % (3916720)Termination phase: Saturation % 224.43/31.90 % (3916720)Time elapsed: 0.088 s % 224.43/31.90 % (3916720)Peak memory usage: 14 MB % 224.43/31.90 % (3916720)Instructions burned: 265 (million) % 224.43/31.90 % (3916722)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=3866729112:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/1368Mi) % 224.43/31.90 % (3916722)Instruction limit reached! % 224.43/31.90 % (3916722)------------------------------ % 224.43/31.90 % (3916722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.43/31.90 % (3916722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.43/31.90 % (3916722)CaDiCaL version: 2.1.3 % 224.43/31.90 % (3916722)Termination reason: Instruction limit % 224.43/31.90 % (3916722)Termination phase: Saturation % 224.43/31.90 % (3916722)Time elapsed: 0.360 s % 224.43/31.90 % (3916722)Peak memory usage: 19 MB % 224.43/31.90 % (3916722)Instructions burned: 1371 (million) % 224.43/31.90 % (3916724)ott-21_1_sil=16000:si=on:fs=off:random_seed=2221073073:i=360:av=off:fsr=off:rtra=on_2813 on theBenchmark for (2813ds/360Mi) % 224.43/31.90 % (3916724)Instruction limit reached! % 224.43/31.90 % (3916724)------------------------------ % 224.43/31.90 % (3916724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.43/31.90 % (3916724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.43/31.90 % (3916724)CaDiCaL version: 2.1.3 % 224.43/31.90 % (3916724)Termination reason: Instruction limit % 224.43/31.90 % (3916724)Termination phase: Saturation % 224.43/31.90 % (3916724)Time elapsed: 0.074 s % 224.43/31.90 % (3916724)Peak memory usage: 12 MB % 224.43/31.90 % (3916724)Instructions burned: 362 (million) % 224.43/31.90 % (3916726)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3519697007:i=954:bd=all:rtra=on_2812 on theBenchmark for (2812ds/954Mi) % 224.43/31.90 % (3916726)Instruction limit reached! % 224.43/31.90 % (3916726)------------------------------ % 224.43/31.90 % (3916726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.43/31.90 % (3916726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.43/31.90 % (3916726)CaDiCaL version: 2.1.3 % 224.43/31.90 % (3916726)Termination reason: Instruction limit % 224.43/31.90 % (3916726)Termination phase: Saturation % 224.43/31.90 % (3916726)Time elapsed: 0.292 s % 224.43/31.90 % (3916726)Peak memory usage: 16 MB % 224.43/31.90 % (3916726)Instructions burned: 956 (million) % 224.43/31.90 % (3916728)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=877140833:fmbsr=1.3:i=1730:ins=25:rtra=on_2809 on theBenchmark for (2809ds/1730Mi) % 224.43/31.90 % Exception at run slice level % 224.43/31.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.79/35.06 % (3916730)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1889687559:i=2358:rtra=on_2809 on theBenchmark for (2809ds/2358Mi) % 246.79/35.06 % (3916730)Instruction limit reached! % 246.79/35.06 % (3916730)------------------------------ % 246.79/35.06 % (3916730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.79/35.06 % (3916730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.79/35.06 % (3916730)CaDiCaL version: 2.1.3 % 246.79/35.06 % (3916730)Termination reason: Instruction limit % 246.79/35.06 % (3916730)Termination phase: Saturation % 246.79/35.06 % (3916730)Time elapsed: 0.679 s % 246.79/35.06 % (3916730)Peak memory usage: 22 MB % 246.79/35.06 % (3916730)Instructions burned: 2361 (million) % 246.79/35.06 % (3916732)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3686827207:i=1778:ins=1:rtra=on_2802 on theBenchmark for (2802ds/1778Mi) % 246.79/35.06 % Exception at run slice level % 246.79/35.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.79/35.06 % (3916734)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=2411484244:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/1384Mi) % 246.79/35.06 % (3916734)Instruction limit reached! % 246.79/35.06 % (3916734)------------------------------ % 246.79/35.06 % (3916734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.79/35.06 % (3916734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.79/35.06 % (3916734)CaDiCaL version: 2.1.3 % 246.79/35.06 % (3916734)Termination reason: Instruction limit % 246.79/35.06 % (3916734)Termination phase: Saturation % 246.79/35.06 % (3916734)Time elapsed: 0.426 s % 246.79/35.06 % (3916734)Peak memory usage: 21 MB % 246.79/35.06 % (3916734)Instructions burned: 1386 (million) % 246.79/35.06 % (3916736)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=629277017:i=1758:kws=inv_precedence:fsr=off:rtra=on_2798 on theBenchmark for (2798ds/1758Mi) % 246.79/35.06 % (3916736)Instruction limit reached! % 246.79/35.06 % (3916736)------------------------------ % 246.79/35.06 % (3916736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.79/35.06 % (3916736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.79/35.06 % (3916736)CaDiCaL version: 2.1.3 % 246.79/35.06 % (3916736)Termination reason: Instruction limit % 246.79/35.06 % (3916736)Termination phase: Saturation % 246.79/35.06 % (3916736)Time elapsed: 0.523 s % 246.79/35.06 % (3916736)Peak memory usage: 22 MB % 246.79/35.06 % (3916736)Instructions burned: 1759 (million) % 246.79/35.06 % (3916738)fmb+10_1_sil=64000:si=on:random_seed=475900802:i=44122:nm=2:rtra=on:gsp=on_2792 on theBenchmark for (2792ds/44122Mi) % 246.79/35.06 % (3916738)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 246.79/35.06 % Exception at run slice level % 246.79/35.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.79/35.06 % (3916740)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=126917613:i=19030:nm=5:rtra=on_2792 on theBenchmark for (2792ds/19030Mi) % 246.79/35.06 % Exception at run slice level % 246.79/35.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.79/35.06 % (3916742)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1233014781:fmbsr=1.7:i=1840:rtra=on_2792 on theBenchmark for (2792ds/1840Mi) % 246.79/35.06 % Exception at run slice level % 246.79/35.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.79/35.06 % (3916744)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1990179219:i=10262:rtra=on_2792 on theBenchmark for (2792ds/10262Mi) % 246.79/35.06 % (3916744)Instruction limit reached! % 246.79/35.06 % (3916744)------------------------------ % 246.79/35.06 % (3916744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.79/35.06 % (3916744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.79/35.06 % (3916744)CaDiCaL version: 2.1.3 % 246.79/35.06 % (3916744)Termination reason: Instruction limit % 246.79/35.06 % (3916744)Termination phase: Saturation % 246.79/35.06 % (3916744)Time elapsed: 5.187 s % 246.79/35.06 % (3916744)Peak memory usage: 53 MB % 246.79/35.06 % (3916744)Instructions burned: 10263 (million) % 300.48/42.63 % (3916746)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2734231496:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2740 on theBenchmark for (2740ds/2944Mi) % 300.48/42.63 % (3916746)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.48/42.63 % (3916746)Instruction limit reached! % 300.48/42.63 % (3916746)------------------------------ % 300.48/42.63 % (3916746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (3916746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (3916746)CaDiCaL version: 2.1.3 % 300.48/42.63 % (3916746)Termination reason: Instruction limit % 300.48/42.63 % (3916746)Termination phase: Saturation % 300.48/42.63 % (3916746)Time elapsed: 1.424 s % 300.48/42.63 % (3916746)Peak memory usage: 32 MB % 300.48/42.63 % (3916746)Instructions burned: 2945 (million) % 300.48/42.63 % (3916748)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1819344858:i=12648:rtra=on_2725 on theBenchmark for (2725ds/12648Mi) % 300.48/42.63 % Exception at run slice level % 300.48/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.48/42.63 % (3916750)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1231832511:fmbsr=2.30978:i=4348:rtra=on_2725 on theBenchmark for (2725ds/4348Mi) % 300.48/42.63 % Exception at run slice level % 300.48/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.48/42.63 % (3916752)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3121899585:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2725 on theBenchmark for (2725ds/1738Mi) % 300.48/42.63 % (3916752)Instruction limit reached! % 300.48/42.63 % (3916752)------------------------------ % 300.48/42.63 % (3916752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (3916752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (3916752)CaDiCaL version: 2.1.3 % 300.48/42.63 % (3916752)Termination reason: Instruction limit % 300.48/42.63 % (3916752)Termination phase: Saturation % 300.48/42.63 % (3916752)Time elapsed: 0.881 s % 300.48/42.63 % (3916752)Peak memory usage: 20 MB % 300.48/42.63 % (3916752)Instructions burned: 1739 (million) % 300.48/42.63 % (3916754)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=718465699:i=10228:av=off:rtra=on_2716 on theBenchmark for (2716ds/10228Mi) % 300.48/42.63 % (3916688)Instruction limit reached! % 300.48/42.63 % (3916688)------------------------------ % 300.48/42.63 % (3916688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (3916688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (3916688)CaDiCaL version: 2.1.3 % 300.48/42.63 % (3916688)Termination reason: Instruction limit % 300.48/42.63 % (3916688)Termination phase: Saturation % 300.48/42.63 % (3916688)Time elapsed: 16.968 s % 300.48/42.63 % (3916688)Peak memory usage: 278 MB % 300.48/42.63 % (3916688)Instructions burned: 53296 (million) % 300.48/42.63 % (3916756)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1152961667:i=108564:rtra=on_2695 on theBenchmark for (2695ds/108564Mi) % 300.48/42.63 % Exception at run slice level % 300.48/42.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.48/42.63 % (3916758)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3209151430:i=7024:aac=none:rtra=on_2695 on theBenchmark for (2695ds/7024Mi) % 300.48/42.63 % (3916598)Instruction limit reached! % 300.48/42.63 % (3916598)------------------------------ % 300.48/42.63 % (3916598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (3916598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (3916598)CaDiCaL version: 2.1.3 % 300.48/42.63 % (3916598)Termination reason: Instruction limit % 300.48/42.63 % (3916598)Termination phase: Saturation % 300.48/42.63 % (3916598)Time elapsed: 31.484 s % 300.48/42.63 % (3916598)Peak memory usage: 44 MB % 300.48/42.63 % (3916598)Instructions burned: 88027 (million) % 300.48/42.63 % (3916760)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=426625835:i=7546:rtra=on:amm=off_2684 on theBenchmark for (2684ds/7546Mi) % 300.48/42.63 % (3916692)Instruction limit reached! % 300.48/42.63 % (3916692)------------------------------ % 300.48/42.63 % (3916692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (3916692)Linked with Z3 4.14.0.0 3 % 300.48/42.64 Terminated % 300.48/42.64 % Vampire exiting % 300.48/42.64 Terminated %------------------------------------------------------------------------------