%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM950_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 : n008.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:16 PM UTC 2026 % Result : Timeout 300.68s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM950_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.12/0.39 % Computer : n008.cluster.edu % 0.12/0.39 % Model : x86_64 x86_64 % 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.39 % Memory : 8046.5625MB % 0.12/0.39 % OS : Linux 6.8.0-71-generic % 0.12/0.39 % CPULimit : 300 % 0.12/0.39 % WCLimit : 300 % 0.12/0.39 % DateTime : Sun Sep 27 21:48:10 UTC 2026 % 0.12/0.39 % CPUTime : % 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.43 Running first-order model finding % 0.12/0.43 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 % 6.86/1.67 % (1633591)Will run a generic schedule for satisfiability detection. % 6.86/1.67 % (1633597)% WARNING: option uhcvi not known. % 6.86/1.67 % (1633597)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=949306488:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.86/1.67 % (1633596)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2906342943_2999 on theBenchmark for (2999ds/0Mi) % 6.86/1.67 % (1633598)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=340039680:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.86/1.67 % (1633599)dis+10_1_sil=32000:sp=arity:random_seed=2642715736:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.86/1.67 % (1633600)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3979086189:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.86/1.67 % (1633601)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1002069954:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.86/1.67 % (1633602)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2385057336:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.86/1.67 % Exception at run slice level % 6.86/1.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.86/1.67 % (1633610)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4259592027:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.86/1.67 % Exception at run slice level % 6.86/1.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.86/1.67 % (1633612)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3712499019:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.86/1.67 % (1633599)Instruction limit reached! % 6.86/1.67 % (1633599)------------------------------ % 6.86/1.67 % (1633599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.67 % (1633599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.67 % (1633599)CaDiCaL version: 2.1.3 % 6.86/1.67 % (1633599)Termination reason: Instruction limit % 6.86/1.67 % (1633599)Termination phase: Saturation % 6.86/1.67 % (1633599)Time elapsed: 0.059 s % 6.86/1.67 % (1633599)Peak memory usage: 12 MB % 6.86/1.67 % (1633599)Instructions burned: 106 (million) % 6.86/1.67 % (1633600)Instruction limit reached! % 6.86/1.67 % (1633600)------------------------------ % 6.86/1.67 % (1633600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.67 % (1633600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.67 % (1633600)CaDiCaL version: 2.1.3 % 6.86/1.67 % (1633600)Termination reason: Instruction limit % 6.86/1.67 % (1633600)Termination phase: Saturation % 6.86/1.67 % (1633600)Time elapsed: 0.065 s % 6.86/1.67 % (1633600)Peak memory usage: 13 MB % 6.86/1.67 % (1633600)Instructions burned: 116 (million) % 6.86/1.67 % (1633601)Instruction limit reached! % 6.86/1.67 % (1633601)------------------------------ % 6.86/1.67 % (1633601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.67 % (1633601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.67 % (1633601)CaDiCaL version: 2.1.3 % 6.86/1.67 % (1633601)Termination reason: Instruction limit % 6.86/1.67 % (1633601)Termination phase: Saturation % 6.86/1.67 % (1633601)Time elapsed: 0.070 s % 6.86/1.67 % (1633601)Peak memory usage: 13 MB % 6.86/1.67 % (1633601)Instructions burned: 132 (million) % 6.86/1.67 % (1633614)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=2058073522:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.86/1.67 % (1633615)ott-21_1_sil=16000:fs=off:random_seed=1972450425:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.86/1.67 % (1633616)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1998793917:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.86/1.67 % (1633602)Instruction limit reached! % 6.86/1.67 % (1633602)------------------------------ % 6.86/1.67 % (1633602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.67 % (1633602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.67 % (1633602)CaDiCaL version: 2.1.3 % 6.86/1.67 % (1633602)Termination reason: Instruction limit % 6.86/1.67 % (1633602)Termination phase: Saturation % 22.34/3.61 % (1633602)Time elapsed: 0.090 s % 22.34/3.61 % (1633602)Peak memory usage: 13 MB % 22.34/3.61 % (1633602)Instructions burned: 160 (million) % 22.34/3.61 % (1633620)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4157574956:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.34/3.61 % Exception at run slice level % 22.34/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.34/3.61 % (1633612)Instruction limit reached! % 22.34/3.61 % (1633612)------------------------------ % 22.34/3.61 % (1633612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.34/3.61 % (1633612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.34/3.61 % (1633612)CaDiCaL version: 2.1.3 % 22.34/3.61 % (1633612)Termination reason: Instruction limit % 22.34/3.61 % (1633612)Termination phase: Saturation % 22.34/3.61 % (1633612)Time elapsed: 0.083 s % 22.34/3.61 % (1633612)Peak memory usage: 13 MB % 22.34/3.61 % (1633612)Instructions burned: 132 (million) % 22.34/3.61 % (1633622)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2031453410:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.34/3.61 % (1633623)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2614802640:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.34/3.61 % Exception at run slice level % 22.34/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.34/3.61 % (1633626)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=1420639494: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) % 22.34/3.61 % (1633615)Instruction limit reached! % 22.34/3.61 % (1633615)------------------------------ % 22.34/3.61 % (1633615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.34/3.61 % (1633615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.34/3.61 % (1633615)CaDiCaL version: 2.1.3 % 22.34/3.61 % (1633615)Termination reason: Instruction limit % 22.34/3.61 % (1633615)Termination phase: Saturation % 22.34/3.61 % (1633615)Time elapsed: 0.090 s % 22.34/3.61 % (1633615)Peak memory usage: 13 MB % 22.34/3.61 % (1633615)Instructions burned: 180 (million) % 22.34/3.61 % (1633628)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3171530235:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.34/3.61 % (1633616)Instruction limit reached! % 22.34/3.61 % (1633616)------------------------------ % 22.34/3.61 % (1633616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.34/3.61 % (1633616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.34/3.61 % (1633616)CaDiCaL version: 2.1.3 % 22.34/3.61 % (1633616)Termination reason: Instruction limit % 22.34/3.61 % (1633616)Termination phase: Saturation % 22.34/3.61 % (1633616)Time elapsed: 0.280 s % 22.34/3.61 % (1633616)Peak memory usage: 15 MB % 22.34/3.61 % (1633616)Instructions burned: 478 (million) % 22.34/3.61 % (1633630)fmb+10_1_sil=64000:random_seed=4005127530:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.34/3.61 % (1633630)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.34/3.61 % Exception at run slice level % 22.34/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.34/3.61 % (1633632)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2804347731:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.34/3.61 % (1633614)Instruction limit reached! % 22.34/3.61 % (1633614)------------------------------ % 22.34/3.61 % (1633614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.34/3.61 % (1633614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.34/3.61 % (1633614)CaDiCaL version: 2.1.3 % 22.34/3.61 % (1633614)Termination reason: Instruction limit % 22.34/3.61 % (1633614)Termination phase: Saturation % 22.34/3.61 % (1633614)Time elapsed: 0.333 s % 22.34/3.61 % (1633614)Peak memory usage: 16 MB % 22.34/3.61 % (1633614)Instructions burned: 686 (million) % 22.34/3.61 % Exception at run slice level % 22.34/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.34/3.61 % (1633634)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3645250033:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.34/3.61 % (1633635)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3236250706:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 90.12/13.18 % Exception at run slice level % 90.12/13.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 90.12/13.18 % (1633638)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3021241798:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 90.12/13.18 % (1633638)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 90.12/13.18 % (1633626)Instruction limit reached! % 90.12/13.18 % (1633626)------------------------------ % 90.12/13.18 % (1633626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.12/13.18 % (1633626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.12/13.18 % (1633626)CaDiCaL version: 2.1.3 % 90.12/13.18 % (1633626)Termination reason: Instruction limit % 90.12/13.18 % (1633626)Termination phase: Saturation % 90.12/13.18 % (1633626)Time elapsed: 0.412 s % 90.12/13.18 % (1633626)Peak memory usage: 18 MB % 90.12/13.18 % (1633626)Instructions burned: 693 (million) % 90.12/13.18 % (1633640)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=153856676:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 90.12/13.18 % Exception at run slice level % 90.12/13.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 90.12/13.18 % (1633642)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1175287453:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 90.12/13.18 % Exception at run slice level % 90.12/13.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 90.12/13.18 % (1633644)ott-2_1_sil=16000:newcnf=on:random_seed=520396910:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 90.12/13.18 % (1633622)Instruction limit reached! % 90.12/13.18 % (1633622)------------------------------ % 90.12/13.18 % (1633622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.12/13.18 % (1633622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.12/13.18 % (1633622)CaDiCaL version: 2.1.3 % 90.12/13.18 % (1633622)Termination reason: Instruction limit % 90.12/13.18 % (1633622)Termination phase: Saturation % 90.12/13.18 % (1633622)Time elapsed: 0.537 s % 90.12/13.18 % (1633622)Peak memory usage: 18 MB % 90.12/13.18 % (1633622)Instructions burned: 1181 (million) % 90.12/13.18 % (1633628)Instruction limit reached! % 90.12/13.18 % (1633628)------------------------------ % 90.12/13.18 % (1633628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.12/13.18 % (1633628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.12/13.18 % (1633628)CaDiCaL version: 2.1.3 % 90.12/13.18 % (1633628)Termination reason: Instruction limit % 90.12/13.18 % (1633628)Termination phase: Saturation % 90.12/13.18 % (1633628)Time elapsed: 0.493 s % 90.12/13.18 % (1633628)Peak memory usage: 17 MB % 90.12/13.18 % (1633628)Instructions burned: 879 (million) % 90.12/13.18 % (1633646)ott+10_1_sil=32000:tgt=ground:random_seed=475595076:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 90.12/13.18 % (1633647)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2739433707:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 90.12/13.18 % Exception at run slice level % 90.12/13.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 90.12/13.18 % (1633650)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1458024415:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 90.12/13.18 % (1633644)Instruction limit reached! % 90.12/13.18 % (1633644)------------------------------ % 90.12/13.18 % (1633644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.12/13.18 % (1633644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.12/13.18 % (1633644)CaDiCaL version: 2.1.3 % 90.12/13.18 % (1633644)Termination reason: Instruction limit % 90.12/13.18 % (1633644)Termination phase: Saturation % 90.12/13.18 % (1633644)Time elapsed: 0.480 s % 90.12/13.18 % (1633644)Peak memory usage: 20 MB % 90.12/13.18 % (1633644)Instructions burned: 869 (million) % 90.12/13.18 % (1633652)dis+21_1_sil=32000:sas=cadical:random_seed=262183671:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 90.12/13.18 % (1633638)Instruction limit reached! % 90.12/13.18 % (1633638)------------------------------ % 90.12/13.18 % (1633638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.93/19.02 % (1633638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.93/19.02 % (1633638)CaDiCaL version: 2.1.3 % 130.93/19.02 % (1633638)Termination reason: Instruction limit % 130.93/19.02 % (1633638)Termination phase: Saturation % 130.93/19.02 % (1633638)Time elapsed: 0.739 s % 130.93/19.02 % (1633638)Peak memory usage: 27 MB % 130.93/19.02 % (1633638)Instructions burned: 1473 (million) % 130.93/19.02 % (1633654)ott+11_1_sil=16000:gs=on:random_seed=3353981358:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 130.93/19.02 % (1633650)Instruction limit reached! % 130.93/19.02 % (1633650)------------------------------ % 130.93/19.02 % (1633650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.93/19.02 % (1633650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.93/19.02 % (1633650)CaDiCaL version: 2.1.3 % 130.93/19.02 % (1633650)Termination reason: Instruction limit % 130.93/19.02 % (1633650)Termination phase: Saturation % 130.93/19.02 % (1633650)Time elapsed: 1.713 s % 130.93/19.02 % (1633650)Peak memory usage: 31 MB % 130.93/19.02 % (1633650)Instructions burned: 3513 (million) % 130.93/19.02 % (1633656)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=597043150:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 130.93/19.02 % Exception at run slice level % 130.93/19.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.93/19.02 % (1633658)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1550302709:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 130.93/19.02 % (1633654)Instruction limit reached! % 130.93/19.02 % (1633654)------------------------------ % 130.93/19.02 % (1633654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.93/19.02 % (1633654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.93/19.02 % (1633654)CaDiCaL version: 2.1.3 % 130.93/19.02 % (1633654)Termination reason: Instruction limit % 130.93/19.02 % (1633654)Termination phase: Saturation % 130.93/19.02 % (1633654)Time elapsed: 1.299 s % 130.93/19.02 % (1633654)Peak memory usage: 27 MB % 130.93/19.02 % (1633654)Instructions burned: 2252 (million) % 130.93/19.02 % (1633660)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2150238254:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 130.93/19.02 % (1633652)Instruction limit reached! % 130.93/19.02 % (1633652)------------------------------ % 130.93/19.02 % (1633652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.93/19.02 % (1633652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.93/19.02 % (1633652)CaDiCaL version: 2.1.3 % 130.93/19.02 % (1633652)Termination reason: Instruction limit % 130.93/19.02 % (1633652)Termination phase: Saturation % 130.93/19.02 % (1633652)Time elapsed: 1.873 s % 130.93/19.02 % (1633652)Peak memory usage: 33 MB % 130.93/19.02 % (1633652)Instructions burned: 3776 (million) % 130.93/19.02 % (1633662)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3821474601:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 130.93/19.02 % (1633635)Instruction limit reached! % 130.93/19.02 % (1633635)------------------------------ % 130.93/19.02 % (1633635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.93/19.02 % (1633635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.93/19.02 % (1633635)CaDiCaL version: 2.1.3 % 130.93/19.02 % (1633635)Termination reason: Instruction limit % 130.93/19.02 % (1633635)Termination phase: Saturation % 130.93/19.02 % (1633635)Time elapsed: 2.623 s % 130.93/19.02 % (1633635)Peak memory usage: 45 MB % 130.93/19.02 % (1633635)Instructions burned: 5132 (million) % 130.93/19.02 % (1633664)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1500408331:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 130.93/19.02 % Exception at run slice level % 130.93/19.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.93/19.02 % (1633666)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=113572191:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 130.93/19.02 % Exception at run slice level % 130.93/19.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 130.93/19.02 % (1633668)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2549346579:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 130.93/19.02 % Exception at run slice level % 178.50/25.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 178.50/25.67 % (1633670)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2905000921:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 178.50/25.67 % (1633646)Instruction limit reached! % 178.50/25.67 % (1633646)------------------------------ % 178.50/25.67 % (1633646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633646)CaDiCaL version: 2.1.3 % 178.50/25.67 % (1633646)Termination reason: Instruction limit % 178.50/25.67 % (1633646)Termination phase: Saturation % 178.50/25.67 % (1633646)Time elapsed: 2.871 s % 178.50/25.67 % (1633646)Peak memory usage: 45 MB % 178.50/25.67 % (1633646)Instructions burned: 5115 (million) % 178.50/25.67 % (1633672)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=80871072:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 178.50/25.67 % (1633658)Instruction limit reached! % 178.50/25.67 % (1633658)------------------------------ % 178.50/25.67 % (1633658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633658)CaDiCaL version: 2.1.3 % 178.50/25.67 % (1633658)Termination reason: Instruction limit % 178.50/25.67 % (1633658)Termination phase: Saturation % 178.50/25.67 % (1633658)Time elapsed: 2.571 s % 178.50/25.67 % (1633658)Peak memory usage: 58 MB % 178.50/25.67 % (1633658)Instructions burned: 4591 (million) % 178.50/25.67 % (1633674)dis+10_16:1_sil=16000:random_seed=3372685106:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 178.50/25.67 % (1633662)Instruction limit reached! % 178.50/25.67 % (1633662)------------------------------ % 178.50/25.67 % (1633662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633662)CaDiCaL version: 2.1.3 % 178.50/25.67 % (1633662)Termination reason: Instruction limit % 178.50/25.67 % (1633662)Termination phase: Saturation % 178.50/25.67 % (1633662)Time elapsed: 2.841 s % 178.50/25.67 % (1633662)Peak memory usage: 47 MB % 178.50/25.67 % (1633662)Instructions burned: 5211 (million) % 178.50/25.67 % (1633676)ott-3_8_sil=64000:random_seed=1694051018:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 178.50/25.67 % (1633672)Instruction limit reached! % 178.50/25.67 % (1633672)------------------------------ % 178.50/25.67 % (1633672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633672)CaDiCaL version: 2.1.3 % 178.50/25.67 % (1633672)Termination reason: Instruction limit % 178.50/25.67 % (1633672)Termination phase: Saturation % 178.50/25.67 % (1633672)Time elapsed: 4.863 s % 178.50/25.67 % (1633672)Peak memory usage: 56 MB % 178.50/25.67 % (1633672)Instructions burned: 8174 (million) % 178.50/25.67 % (1633678)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4099042295:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 178.50/25.67 % Exception at run slice level % 178.50/25.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 178.50/25.67 % (1633680)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1356087930:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 178.50/25.67 % (1633674)Instruction limit reached! % 178.50/25.67 % (1633674)------------------------------ % 178.50/25.67 % (1633674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633674)CaDiCaL version: 2.1.3 % 178.50/25.67 % (1633674)Termination reason: Instruction limit % 178.50/25.67 % (1633674)Termination phase: Saturation % 178.50/25.67 % (1633674)Time elapsed: 4.657 s % 178.50/25.67 % (1633674)Peak memory usage: 53 MB % 178.50/25.67 % (1633674)Instructions burned: 9156 (million) % 178.50/25.67 % (1633682)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3294037933:i=14134_2902 on theBenchmark for (2902ds/14134Mi) % 178.50/25.67 % (1633670)Instruction limit reached! % 178.50/25.67 % (1633670)------------------------------ % 178.50/25.67 % (1633670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.50/25.67 % (1633670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.50/25.67 % (1633670)CaDiCaL version: 2.1.3 % 192.06/27.58 % (1633670)Termination reason: Instruction limit % 192.06/27.58 % (1633670)Termination phase: Saturation % 192.06/27.58 % (1633670)Time elapsed: 9.558 s % 192.06/27.58 % (1633670)Peak memory usage: 73 MB % 192.06/27.58 % (1633670)Instructions burned: 22568 (million) % 192.06/27.58 % (1633684)dis+33_16_sil=32000:sac=on:random_seed=1429342303:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi) % 192.06/27.58 % (1633680)Instruction limit reached! % 192.06/27.58 % (1633680)------------------------------ % 192.06/27.58 % (1633680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.06/27.58 % (1633680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.06/27.58 % (1633680)CaDiCaL version: 2.1.3 % 192.06/27.58 % (1633680)Termination reason: Instruction limit % 192.06/27.58 % (1633680)Termination phase: Saturation % 192.06/27.58 % (1633680)Time elapsed: 6.804 s % 192.06/27.58 % (1633680)Peak memory usage: 71 MB % 192.06/27.58 % (1633680)Instructions burned: 11404 (million) % 192.06/27.58 % (1633686)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1501840565:avsq=on:i=17627:add=on:amm=off_2846 on theBenchmark for (2846ds/17627Mi) % 192.06/27.58 % (1633660)Instruction limit reached! % 192.06/27.58 % (1633660)------------------------------ % 192.06/27.58 % (1633660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.06/27.58 % (1633660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.06/27.58 % (1633660)CaDiCaL version: 2.1.3 % 192.06/27.58 % (1633660)Termination reason: Instruction limit % 192.06/27.58 % (1633660)Termination phase: Saturation % 192.06/27.58 % (1633660)Time elapsed: 14.474 s % 192.06/27.58 % (1633660)Peak memory usage: 190 MB % 192.06/27.58 % (1633660)Instructions burned: 29340 (million) % 192.06/27.58 % (1633688)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3449474143:s2a=on:i=53295_2829 on theBenchmark for (2829ds/53295Mi) % 192.06/27.58 % (1633682)Instruction limit reached! % 192.06/27.58 % (1633682)------------------------------ % 192.06/27.58 % (1633682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.06/27.58 % (1633682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.06/27.58 % (1633682)CaDiCaL version: 2.1.3 % 192.06/27.58 % (1633682)Termination reason: Instruction limit % 192.06/27.58 % (1633682)Termination phase: Saturation % 192.06/27.58 % (1633682)Time elapsed: 8.507 s % 192.06/27.58 % (1633682)Peak memory usage: 79 MB % 192.06/27.58 % (1633682)Instructions burned: 14135 (million) % 192.06/27.58 % (1633690)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1430372991:i=26857:ins=20_2816 on theBenchmark for (2816ds/26857Mi) % 192.06/27.58 % Exception at run slice level % 192.06/27.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.06/27.58 % (1633692)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3675662016:i=28120:bs=on:fsr=off_2816 on theBenchmark for (2816ds/28120Mi) % 192.06/27.58 % (1633676)Instruction limit reached! % 192.06/27.58 % (1633676)------------------------------ % 192.06/27.58 % (1633676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.06/27.58 % (1633676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.06/27.58 % (1633676)CaDiCaL version: 2.1.3 % 192.06/27.58 % (1633676)Termination reason: Instruction limit % 192.06/27.58 % (1633676)Termination phase: Saturation % 192.06/27.58 % (1633676)Time elapsed: 12.523 s % 192.06/27.58 % (1633676)Peak memory usage: 121 MB % 192.06/27.58 % (1633676)Instructions burned: 20140 (million) % 192.06/27.58 % (1633694)fmb+10_1_sil=256000:fmbss=7:random_seed=3552356504:fmbsr=1.6:i=182295_2815 on theBenchmark for (2815ds/182295Mi) % 192.06/27.58 % Exception at run slice level % 192.06/27.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.06/27.58 % (1633696)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1489903389:i=44625:gsp=on_2814 on theBenchmark for (2814ds/44625Mi) % 192.06/27.58 % (1633696)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.06/27.58 % Exception at run slice level % 192.06/27.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.06/27.58 % (1633698)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1811109469:i=160505_2814 on theBenchmark for (2814ds/160505Mi) % 192.06/27.58 % Exception at run slice level % 192.06/27.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.06/27.58 % (1633700)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4146611221:fmbsr=1.3:i=225729_2814 on theBenchmark for (2814ds/225729Mi) % 254.52/36.33 % Exception at run slice level % 254.52/36.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 254.52/36.33 % (1633702)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2960028684:fmbsr=2:i=185024:ins=7_2814 on theBenchmark for (2814ds/185024Mi) % 254.52/36.33 % Exception at run slice level % 254.52/36.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 254.52/36.33 % (1633704)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3923670250:rtra=on_2813 on theBenchmark for (2813ds/0Mi) % 254.52/36.33 % Exception at run slice level % 254.52/36.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 254.52/36.33 % (1633706)% WARNING: option uhcvi not known. % 254.52/36.33 % (1633706)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2181492456:i=271062:add=off:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/271062Mi) % 254.52/36.33 % (1633684)Instruction limit reached! % 254.52/36.33 % (1633684)------------------------------ % 254.52/36.33 % (1633684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.52/36.33 % (1633684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.52/36.33 % (1633684)CaDiCaL version: 2.1.3 % 254.52/36.33 % (1633684)Termination reason: Instruction limit % 254.52/36.33 % (1633684)Termination phase: Saturation % 254.52/36.33 % (1633684)Time elapsed: 8.456 s % 254.52/36.33 % (1633684)Peak memory usage: 103 MB % 254.52/36.33 % (1633684)Instructions burned: 15852 (million) % 254.52/36.33 % (1633708)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=534072376:i=176048:add=on:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/176048Mi) % 254.52/36.33 % (1633686)Instruction limit reached! % 254.52/36.33 % (1633686)------------------------------ % 254.52/36.33 % (1633686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.52/36.33 % (1633686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.52/36.33 % (1633686)CaDiCaL version: 2.1.3 % 254.52/36.33 % (1633686)Termination reason: Instruction limit % 254.52/36.33 % (1633686)Termination phase: Saturation % 254.52/36.33 % (1633686)Time elapsed: 9.414 s % 254.52/36.33 % (1633686)Peak memory usage: 129 MB % 254.52/36.33 % (1633686)Instructions burned: 17628 (million) % 254.52/36.33 % (1633710)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1632119380:i=206:fgj=on:rtra=on_2751 on theBenchmark for (2751ds/206Mi) % 254.52/36.33 % (1633710)Instruction limit reached! % 254.52/36.33 % (1633710)------------------------------ % 254.52/36.33 % (1633710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.52/36.33 % (1633710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.52/36.33 % (1633710)CaDiCaL version: 2.1.3 % 254.52/36.33 % (1633710)Termination reason: Instruction limit % 254.52/36.33 % (1633710)Termination phase: Saturation % 254.52/36.33 % (1633710)Time elapsed: 0.114 s % 254.52/36.33 % (1633710)Peak memory usage: 13 MB % 254.52/36.33 % (1633710)Instructions burned: 207 (million) % 254.52/36.33 % (1633712)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2015511049:i=232:rtra=on_2750 on theBenchmark for (2750ds/232Mi) % 254.52/36.33 % (1633712)Instruction limit reached! % 254.52/36.33 % (1633712)------------------------------ % 254.52/36.33 % (1633712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.52/36.33 % (1633712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.52/36.33 % (1633712)CaDiCaL version: 2.1.3 % 254.52/36.33 % (1633712)Termination reason: Instruction limit % 254.52/36.33 % (1633712)Termination phase: Saturation % 254.52/36.33 % (1633712)Time elapsed: 0.124 s % 254.52/36.33 % (1633712)Peak memory usage: 14 MB % 254.52/36.33 % (1633712)Instructions burned: 233 (million) % 254.52/36.33 % (1633714)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1377104677:i=262:rtra=on_2749 on theBenchmark for (2749ds/262Mi) % 254.52/36.33 % (1633714)Instruction limit reached! % 254.52/36.33 % (1633714)------------------------------ % 254.52/36.33 % (1633714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.52/36.33 % (1633714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.52/36.33 % (1633714)CaDiCaL version: 2.1.3 % 254.52/36.33 % (1633714)Termination reason: Instruction limit % 254.52/36.33 % (1633714)Termination phase: Saturation % 279.97/39.97 % (1633714)Time elapsed: 0.139 s % 279.97/39.97 % (1633714)Peak memory usage: 14 MB % 279.97/39.97 % (1633714)Instructions burned: 263 (million) % 279.97/39.97 % (1633716)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2480179724:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2747 on theBenchmark for (2747ds/318Mi) % 279.97/39.97 % (1633716)Instruction limit reached! % 279.97/39.97 % (1633716)------------------------------ % 279.97/39.97 % (1633716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.97/39.97 % (1633716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.97/39.97 % (1633716)CaDiCaL version: 2.1.3 % 279.97/39.97 % (1633716)Termination reason: Instruction limit % 279.97/39.97 % (1633716)Termination phase: Saturation % 279.97/39.97 % (1633716)Time elapsed: 0.178 s % 279.97/39.97 % (1633716)Peak memory usage: 14 MB % 279.97/39.97 % (1633716)Instructions burned: 319 (million) % 279.97/39.97 % (1633718)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=43357224:i=1428:nm=2:rtra=on_2745 on theBenchmark for (2745ds/1428Mi) % 279.97/39.97 % Exception at run slice level % 279.97/39.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.97/39.97 % (1633720)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1706057598:i=262:bd=preordered:rtra=on:fsd=on_2745 on theBenchmark for (2745ds/262Mi) % 279.97/39.97 % (1633720)Instruction limit reached! % 279.97/39.97 % (1633720)------------------------------ % 279.97/39.97 % (1633720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.97/39.97 % (1633720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.97/39.97 % (1633720)CaDiCaL version: 2.1.3 % 279.97/39.97 % (1633720)Termination reason: Instruction limit % 279.97/39.97 % (1633720)Termination phase: Saturation % 279.97/39.97 % (1633720)Time elapsed: 0.170 s % 279.97/39.97 % (1633720)Peak memory usage: 14 MB % 279.97/39.97 % (1633720)Instructions burned: 263 (million) % 279.97/39.97 % (1633722)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=3686758738:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1368Mi) % 279.97/39.97 % (1633722)Instruction limit reached! % 279.97/39.97 % (1633722)------------------------------ % 279.97/39.97 % (1633722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.97/39.97 % (1633722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.97/39.97 % (1633722)CaDiCaL version: 2.1.3 % 279.97/39.97 % (1633722)Termination reason: Instruction limit % 279.97/39.97 % (1633722)Termination phase: Saturation % 279.97/39.97 % (1633722)Time elapsed: 0.677 s % 279.97/39.97 % (1633722)Peak memory usage: 19 MB % 279.97/39.97 % (1633722)Instructions burned: 1368 (million) % 279.97/39.97 % (1633724)ott-21_1_sil=16000:si=on:fs=off:random_seed=2110381693:i=360:av=off:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/360Mi) % 279.97/39.97 % (1633724)Instruction limit reached! % 279.97/39.97 % (1633724)------------------------------ % 279.97/39.97 % (1633724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.97/39.97 % (1633724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.97/39.97 % (1633724)CaDiCaL version: 2.1.3 % 279.97/39.97 % (1633724)Termination reason: Instruction limit % 279.97/39.97 % (1633724)Termination phase: Saturation % 279.97/39.97 % (1633724)Time elapsed: 0.170 s % 279.97/39.97 % (1633724)Peak memory usage: 14 MB % 279.97/39.97 % (1633724)Instructions burned: 361 (million) % 279.97/39.97 % (1633726)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1442286197:i=954:bd=all:rtra=on_2734 on theBenchmark for (2734ds/954Mi) % 279.97/39.97 % (1633726)Instruction limit reached! % 279.97/39.97 % (1633726)------------------------------ % 279.97/39.97 % (1633726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.97/39.97 % (1633726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.97/39.97 % (1633726)CaDiCaL version: 2.1.3 % 279.97/39.97 % (1633726)Termination reason: Instruction limit % 279.97/39.97 % (1633726)Termination phase: Saturation % 279.97/39.97 % (1633726)Time elapsed: 0.556 s % 279.97/39.97 % (1633726)Peak memory usage: 17 MB % 279.97/39.97 % (1633726)Instructions burned: 955 (million) % 279.97/39.97 % (1633728)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=959004199:fmbsr=1.3:i=1730:ins=25:rtra=on_2728 on theBenchmark for (2728ds/1730Mi) % 279.97/39.97 % Exception at run slice level % 279.97/39.97 User error: Finite model building is cuTerminated % 300.68/42.84 % Vampire exiting % 300.68/42.84 Terminated %------------------------------------------------------------------------------