%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM997_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : 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 12:26:21 PM UTC 2026 % Result : Timeout 300.25s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM997_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.37 % Computer : n006.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 27 21:49:41 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.40 Running first-order model finding % 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.37/1.63 % (3353196)Will run a generic schedule for satisfiability detection. % 7.37/1.63 % (3353205)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=380338328:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.37/1.63 % (3353201)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2086417605_2999 on theBenchmark for (2999ds/0Mi) % 7.37/1.63 % (3353207)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4213710283:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.37/1.63 % (3353204)dis+10_1_sil=32000:sp=arity:random_seed=4006183031:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.37/1.63 % (3353203)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=849022191:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.37/1.63 % (3353206)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2117117166:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.37/1.63 % Exception at run slice level % 7.37/1.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.37/1.63 % (3353202)% WARNING: option uhcvi not known. % 7.37/1.63 % (3353202)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2245933012:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.37/1.63 % (3353214)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=952365264:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.37/1.63 % Exception at run slice level % 7.37/1.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.37/1.63 % (3353217)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=742910970:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.37/1.63 % (3353204)Instruction limit reached! % 7.37/1.63 % (3353204)------------------------------ % 7.37/1.63 % (3353204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.63 % (3353204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.63 % (3353204)CaDiCaL version: 2.1.3 % 7.37/1.63 % (3353204)Termination reason: Instruction limit % 7.37/1.63 % (3353204)Termination phase: Saturation % 7.37/1.63 % (3353204)Time elapsed: 0.059 s % 7.37/1.63 % (3353204)Peak memory usage: 12 MB % 7.37/1.63 % (3353204)Instructions burned: 104 (million) % 7.37/1.63 % (3353205)Instruction limit reached! % 7.37/1.63 % (3353205)------------------------------ % 7.37/1.63 % (3353205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.63 % (3353205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.63 % (3353205)CaDiCaL version: 2.1.3 % 7.37/1.63 % (3353205)Termination reason: Instruction limit % 7.37/1.63 % (3353205)Termination phase: Saturation % 7.37/1.63 % (3353205)Time elapsed: 0.066 s % 7.37/1.63 % (3353205)Peak memory usage: 13 MB % 7.37/1.63 % (3353205)Instructions burned: 117 (million) % 7.37/1.63 % (3353206)Instruction limit reached! % 7.37/1.63 % (3353206)------------------------------ % 7.37/1.63 % (3353206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.63 % (3353206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.63 % (3353206)CaDiCaL version: 2.1.3 % 7.37/1.63 % (3353206)Termination reason: Instruction limit % 7.37/1.63 % (3353206)Termination phase: Saturation % 7.37/1.63 % (3353206)Time elapsed: 0.067 s % 7.37/1.63 % (3353206)Peak memory usage: 13 MB % 7.37/1.63 % (3353206)Instructions burned: 132 (million) % 7.37/1.63 % (3353219)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=1570412709:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.37/1.63 % (3353220)ott-21_1_sil=16000:fs=off:random_seed=312849745:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.37/1.63 % (3353221)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=330046051:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 7.37/1.63 % (3353207)Instruction limit reached! % 7.37/1.63 % (3353207)------------------------------ % 7.37/1.63 % (3353207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.63 % (3353207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.63 % (3353207)CaDiCaL version: 2.1.3 % 7.37/1.63 % (3353207)Termination reason: Instruction limit % 7.37/1.63 % (3353207)Termination phase: Saturation % 21.85/3.62 % (3353207)Time elapsed: 0.100 s % 21.85/3.62 % (3353207)Peak memory usage: 14 MB % 21.85/3.62 % (3353207)Instructions burned: 159 (million) % 21.85/3.62 % (3353225)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3948617116:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.85/3.62 % Exception at run slice level % 21.85/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.62 % (3353217)Instruction limit reached! % 21.85/3.62 % (3353217)------------------------------ % 21.85/3.62 % (3353217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.62 % (3353217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.62 % (3353217)CaDiCaL version: 2.1.3 % 21.85/3.62 % (3353217)Termination reason: Instruction limit % 21.85/3.62 % (3353217)Termination phase: Saturation % 21.85/3.62 % (3353217)Time elapsed: 0.079 s % 21.85/3.62 % (3353217)Peak memory usage: 13 MB % 21.85/3.62 % (3353217)Instructions burned: 132 (million) % 21.85/3.62 % (3353227)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=37582025:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.85/3.62 % (3353228)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3283125059:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.85/3.62 % Exception at run slice level % 21.85/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.62 % (3353231)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=2522789836: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) % 21.85/3.62 % (3353220)Instruction limit reached! % 21.85/3.62 % (3353220)------------------------------ % 21.85/3.62 % (3353220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.62 % (3353220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.62 % (3353220)CaDiCaL version: 2.1.3 % 21.85/3.62 % (3353220)Termination reason: Instruction limit % 21.85/3.62 % (3353220)Termination phase: Saturation % 21.85/3.62 % (3353220)Time elapsed: 0.085 s % 21.85/3.62 % (3353220)Peak memory usage: 12 MB % 21.85/3.62 % (3353220)Instructions burned: 181 (million) % 21.85/3.62 % (3353233)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3888142048:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.85/3.62 % (3353221)Instruction limit reached! % 21.85/3.62 % (3353221)------------------------------ % 21.85/3.62 % (3353221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.62 % (3353221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.62 % (3353221)CaDiCaL version: 2.1.3 % 21.85/3.62 % (3353221)Termination reason: Instruction limit % 21.85/3.62 % (3353221)Termination phase: Saturation % 21.85/3.62 % (3353221)Time elapsed: 0.295 s % 21.85/3.62 % (3353221)Peak memory usage: 14 MB % 21.85/3.62 % (3353221)Instructions burned: 478 (million) % 21.85/3.62 % (3353235)fmb+10_1_sil=64000:random_seed=324446211:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.85/3.62 % (3353235)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.85/3.62 % Exception at run slice level % 21.85/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.62 % (3353237)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3452757547:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.85/3.62 % Exception at run slice level % 21.85/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.62 % (3353219)Instruction limit reached! % 21.85/3.62 % (3353219)------------------------------ % 21.85/3.62 % (3353219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.62 % (3353219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.62 % (3353219)CaDiCaL version: 2.1.3 % 21.85/3.62 % (3353219)Termination reason: Instruction limit % 21.85/3.62 % (3353219)Termination phase: Saturation % 21.85/3.62 % (3353219)Time elapsed: 0.357 s % 21.85/3.62 % (3353219)Peak memory usage: 18 MB % 21.85/3.62 % (3353219)Instructions burned: 685 (million) % 21.85/3.62 % (3353239)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4148074541:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 21.85/3.62 % Exception at run slice level % 21.85/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.81/14.93 % (3353240)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2611904032:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 102.81/14.93 % (3353242)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=698204583:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 102.81/14.93 % (3353242)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 102.81/14.93 % (3353231)Instruction limit reached! % 102.81/14.93 % (3353231)------------------------------ % 102.81/14.93 % (3353231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.81/14.93 % (3353231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.81/14.93 % (3353231)CaDiCaL version: 2.1.3 % 102.81/14.93 % (3353231)Termination reason: Instruction limit % 102.81/14.93 % (3353231)Termination phase: Saturation % 102.81/14.93 % (3353231)Time elapsed: 0.328 s % 102.81/14.93 % (3353231)Peak memory usage: 18 MB % 102.81/14.93 % (3353231)Instructions burned: 692 (million) % 102.81/14.93 % (3353245)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1762584075:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 102.81/14.93 % Exception at run slice level % 102.81/14.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.81/14.93 % (3353247)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2178233241:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 102.81/14.93 % Exception at run slice level % 102.81/14.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.81/14.93 % (3353249)ott-2_1_sil=16000:newcnf=on:random_seed=2361566076:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 102.81/14.93 % (3353233)Instruction limit reached! % 102.81/14.93 % (3353233)------------------------------ % 102.81/14.93 % (3353233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.81/14.93 % (3353233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.81/14.93 % (3353233)CaDiCaL version: 2.1.3 % 102.81/14.93 % (3353233)Termination reason: Instruction limit % 102.81/14.93 % (3353233)Termination phase: Saturation % 102.81/14.93 % (3353233)Time elapsed: 0.483 s % 102.81/14.93 % (3353233)Peak memory usage: 19 MB % 102.81/14.93 % (3353233)Instructions burned: 880 (million) % 102.81/14.93 % (3353251)ott+10_1_sil=32000:tgt=ground:random_seed=2149889902:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 102.81/14.93 % (3353227)Instruction limit reached! % 102.81/14.93 % (3353227)------------------------------ % 102.81/14.93 % (3353227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.81/14.93 % (3353227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.81/14.93 % (3353227)CaDiCaL version: 2.1.3 % 102.81/14.93 % (3353227)Termination reason: Instruction limit % 102.81/14.93 % (3353227)Termination phase: Saturation % 102.81/14.93 % (3353227)Time elapsed: 0.560 s % 102.81/14.93 % (3353227)Peak memory usage: 18 MB % 102.81/14.93 % (3353227)Instructions burned: 1181 (million) % 102.81/14.93 % (3353253)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1720267042:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 102.81/14.93 % Exception at run slice level % 102.81/14.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 102.81/14.93 % (3353255)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=431451136:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 102.81/14.93 % (3353249)Instruction limit reached! % 102.81/14.93 % (3353249)------------------------------ % 102.81/14.93 % (3353249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.81/14.93 % (3353249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.81/14.93 % (3353249)CaDiCaL version: 2.1.3 % 102.81/14.93 % (3353249)Termination reason: Instruction limit % 102.81/14.93 % (3353249)Termination phase: Saturation % 102.81/14.93 % (3353249)Time elapsed: 0.445 s % 102.81/14.93 % (3353249)Peak memory usage: 19 MB % 102.81/14.93 % (3353249)Instructions burned: 869 (million) % 102.81/14.93 % (3353257)dis+21_1_sil=32000:sas=cadical:random_seed=362325348:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 102.81/14.93 % (3353242)Instruction limit reached! % 102.81/14.93 % (3353242)------------------------------ % 102.81/14.93 % (3353242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.76 % (3353242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.76 % (3353242)CaDiCaL version: 2.1.3 % 129.62/18.76 % (3353242)Termination reason: Instruction limit % 129.62/18.76 % (3353242)Termination phase: Saturation % 129.62/18.76 % (3353242)Time elapsed: 0.715 s % 129.62/18.76 % (3353242)Peak memory usage: 28 MB % 129.62/18.76 % (3353242)Instructions burned: 1473 (million) % 129.62/18.76 % (3353259)ott+11_1_sil=16000:gs=on:random_seed=2255841545:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 129.62/18.76 % (3353259)Instruction limit reached! % 129.62/18.76 % (3353259)------------------------------ % 129.62/18.76 % (3353259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.76 % (3353259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.76 % (3353259)CaDiCaL version: 2.1.3 % 129.62/18.76 % (3353259)Termination reason: Instruction limit % 129.62/18.76 % (3353259)Termination phase: Saturation % 129.62/18.76 % (3353259)Time elapsed: 1.251 s % 129.62/18.76 % (3353259)Peak memory usage: 35 MB % 129.62/18.76 % (3353259)Instructions burned: 2251 (million) % 129.62/18.76 % (3353261)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3653806183:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 129.62/18.76 % Exception at run slice level % 129.62/18.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.62/18.76 % (3353263)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2370391617:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 129.62/18.76 % (3353255)Instruction limit reached! % 129.62/18.76 % (3353255)------------------------------ % 129.62/18.76 % (3353255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.76 % (3353255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.76 % (3353255)CaDiCaL version: 2.1.3 % 129.62/18.76 % (3353255)Termination reason: Instruction limit % 129.62/18.76 % (3353255)Termination phase: Saturation % 129.62/18.76 % (3353255)Time elapsed: 1.833 s % 129.62/18.76 % (3353255)Peak memory usage: 37 MB % 129.62/18.76 % (3353255)Instructions burned: 3513 (million) % 129.62/18.76 % (3353265)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3847139477:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 129.62/18.76 % (3353257)Instruction limit reached! % 129.62/18.76 % (3353257)------------------------------ % 129.62/18.76 % (3353257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.76 % (3353257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.76 % (3353257)CaDiCaL version: 2.1.3 % 129.62/18.76 % (3353257)Termination reason: Instruction limit % 129.62/18.76 % (3353257)Termination phase: Saturation % 129.62/18.76 % (3353257)Time elapsed: 1.938 s % 129.62/18.76 % (3353257)Peak memory usage: 39 MB % 129.62/18.76 % (3353257)Instructions burned: 3773 (million) % 129.62/18.76 % (3353267)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3206372538:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 129.62/18.76 % (3353240)Instruction limit reached! % 129.62/18.76 % (3353240)------------------------------ % 129.62/18.76 % (3353240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.62/18.76 % (3353240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.62/18.76 % (3353240)CaDiCaL version: 2.1.3 % 129.62/18.76 % (3353240)Termination reason: Instruction limit % 129.62/18.76 % (3353240)Termination phase: Saturation % 129.62/18.76 % (3353240)Time elapsed: 2.646 s % 129.62/18.76 % (3353240)Peak memory usage: 47 MB % 129.62/18.76 % (3353240)Instructions burned: 5133 (million) % 129.62/18.76 % (3353269)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2256895696:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 129.62/18.76 % Exception at run slice level % 129.62/18.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.62/18.76 % (3353271)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=720141188:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 129.62/18.76 % Exception at run slice level % 129.62/18.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.62/18.76 % (3353273)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3266739834:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 129.62/18.76 % Exception at run slice level % 198.56/28.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.56/28.47 % (3353275)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=170369502:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 198.56/28.47 % (3353251)Instruction limit reached! % 198.56/28.47 % (3353251)------------------------------ % 198.56/28.47 % (3353251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353251)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353251)Termination reason: Instruction limit % 198.56/28.47 % (3353251)Termination phase: Saturation % 198.56/28.47 % (3353251)Time elapsed: 2.798 s % 198.56/28.47 % (3353251)Peak memory usage: 54 MB % 198.56/28.47 % (3353251)Instructions burned: 5115 (million) % 198.56/28.47 % (3353279)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=898193825:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi) % 198.56/28.47 % (3353263)Instruction limit reached! % 198.56/28.47 % (3353263)------------------------------ % 198.56/28.47 % (3353263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353263)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353263)Termination reason: Instruction limit % 198.56/28.47 % (3353263)Termination phase: Saturation % 198.56/28.47 % (3353263)Time elapsed: 1.911 s % 198.56/28.47 % (3353263)Peak memory usage: 33 MB % 198.56/28.47 % (3353263)Instructions burned: 4593 (million) % 198.56/28.47 % (3353281)dis+10_16:1_sil=16000:random_seed=57611893:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 198.56/28.47 % (3353267)Instruction limit reached! % 198.56/28.47 % (3353267)------------------------------ % 198.56/28.47 % (3353267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353267)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353267)Termination reason: Instruction limit % 198.56/28.47 % (3353267)Termination phase: Saturation % 198.56/28.47 % (3353267)Time elapsed: 2.689 s % 198.56/28.47 % (3353267)Peak memory usage: 52 MB % 198.56/28.47 % (3353267)Instructions burned: 5214 (million) % 198.56/28.47 % (3353283)ott-3_8_sil=64000:random_seed=892205225:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 198.56/28.47 % (3353279)Instruction limit reached! % 198.56/28.47 % (3353279)------------------------------ % 198.56/28.47 % (3353279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353279)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353279)Termination reason: Instruction limit % 198.56/28.47 % (3353279)Termination phase: Saturation % 198.56/28.47 % (3353279)Time elapsed: 4.570 s % 198.56/28.47 % (3353279)Peak memory usage: 80 MB % 198.56/28.47 % (3353279)Instructions burned: 8173 (million) % 198.56/28.47 % (3353285)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=412645675:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 198.56/28.47 % Exception at run slice level % 198.56/28.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.56/28.47 % (3353287)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3384998792:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 198.56/28.47 % (3353281)Instruction limit reached! % 198.56/28.47 % (3353281)------------------------------ % 198.56/28.47 % (3353281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353281)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353281)Termination reason: Instruction limit % 198.56/28.47 % (3353281)Termination phase: Saturation % 198.56/28.47 % (3353281)Time elapsed: 4.661 s % 198.56/28.47 % (3353281)Peak memory usage: 71 MB % 198.56/28.47 % (3353281)Instructions burned: 9157 (million) % 198.56/28.47 % (3353289)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2383085662:i=14134_2908 on theBenchmark for (2908ds/14134Mi) % 198.56/28.47 % (3353275)Instruction limit reached! % 198.56/28.47 % (3353275)------------------------------ % 198.56/28.47 % (3353275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.56/28.47 % (3353275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.56/28.47 % (3353275)CaDiCaL version: 2.1.3 % 198.56/28.47 % (3353275)Termination reason: Instruction limit % 221.31/31.64 % (3353275)Termination phase: Saturation % 221.31/31.64 % (3353275)Time elapsed: 11.289 s % 221.31/31.64 % (3353275)Peak memory usage: 164 MB % 221.31/31.64 % (3353275)Instructions burned: 22566 (million) % 221.31/31.64 % (3353530)dis+33_16_sil=32000:sac=on:random_seed=1133232084:i=15851:nm=0_2854 on theBenchmark for (2854ds/15851Mi) % 221.31/31.64 % (3353287)Instruction limit reached! % 221.31/31.64 % (3353287)------------------------------ % 221.31/31.64 % (3353287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.31/31.64 % (3353287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.31/31.64 % (3353287)CaDiCaL version: 2.1.3 % 221.31/31.64 % (3353287)Termination reason: Instruction limit % 221.31/31.64 % (3353287)Termination phase: Saturation % 221.31/31.64 % (3353287)Time elapsed: 6.478 s % 221.31/31.64 % (3353287)Peak memory usage: 94 MB % 221.31/31.64 % (3353287)Instructions burned: 11404 (million) % 221.31/31.64 % (3353539)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3839107552:avsq=on:i=17627:add=on:amm=off_2853 on theBenchmark for (2853ds/17627Mi) % 221.31/31.64 % (3353265)Instruction limit reached! % 221.31/31.65 % (3353265)------------------------------ % 221.31/31.65 % (3353265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.31/31.65 % (3353265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.31/31.65 % (3353265)CaDiCaL version: 2.1.3 % 221.31/31.65 % (3353265)Termination reason: Instruction limit % 221.31/31.65 % (3353265)Termination phase: Saturation % 221.31/31.65 % (3353265)Time elapsed: 14.002 s % 221.31/31.65 % (3353265)Peak memory usage: 113 MB % 221.31/31.65 % (3353265)Instructions burned: 29340 (million) % 221.31/31.65 % (3353586)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1192025589:s2a=on:i=53295_2833 on theBenchmark for (2833ds/53295Mi) % 221.31/31.65 % (3353289)Instruction limit reached! % 221.31/31.65 % (3353289)------------------------------ % 221.31/31.65 % (3353289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.31/31.65 % (3353289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.31/31.65 % (3353289)CaDiCaL version: 2.1.3 % 221.31/31.65 % (3353289)Termination reason: Instruction limit % 221.31/31.65 % (3353289)Termination phase: Saturation % 221.31/31.65 % (3353289)Time elapsed: 8.835 s % 221.31/31.65 % (3353289)Peak memory usage: 109 MB % 221.31/31.65 % (3353289)Instructions burned: 14134 (million) % 221.31/31.65 % (3353619)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1483847826:i=26857:ins=20_2819 on theBenchmark for (2819ds/26857Mi) % 221.31/31.65 % Exception at run slice level % 221.31/31.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.31/31.65 % (3353623)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1349923809:i=28120:bs=on:fsr=off_2819 on theBenchmark for (2819ds/28120Mi) % 221.31/31.65 % (3353283)Instruction limit reached! % 221.31/31.65 % (3353283)------------------------------ % 221.31/31.65 % (3353283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.31/31.65 % (3353283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.31/31.65 % (3353283)CaDiCaL version: 2.1.3 % 221.31/31.65 % (3353283)Termination reason: Instruction limit % 221.31/31.65 % (3353283)Termination phase: Saturation % 221.31/31.65 % (3353283)Time elapsed: 12.450 s % 221.31/31.65 % (3353283)Peak memory usage: 137 MB % 221.31/31.65 % (3353283)Instructions burned: 20140 (million) % 221.31/31.65 % (3353629)fmb+10_1_sil=256000:fmbss=7:random_seed=2037953843:fmbsr=1.6:i=182295_2817 on theBenchmark for (2817ds/182295Mi) % 221.31/31.65 % Exception at run slice level % 221.31/31.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.31/31.65 % (3353631)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3912996549:i=44625:gsp=on_2817 on theBenchmark for (2817ds/44625Mi) % 221.31/31.65 % (3353631)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 221.31/31.65 % Exception at run slice level % 221.31/31.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.31/31.65 % (3353634)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1744186027:i=160505_2817 on theBenchmark for (2817ds/160505Mi) % 221.31/31.65 % Exception at run slice level % 221.31/31.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.31/31.65 % (3353636)fmb+10_1_sil=256000:tgt=full:Terminated % 300.25/42.74 % Vampire exiting % 300.25/42.74 Terminated %------------------------------------------------------------------------------