%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW519_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 : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:22 PM UTC 2026 % Result : Timeout 300.13s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW519_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.08/0.17 % Computer : n010.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:17:32 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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.39/1.33 % (1946464)Will run a generic schedule for satisfiability detection. % 7.39/1.33 % (1946472)dis+10_1_sil=32000:sp=arity:random_seed=581109308:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.39/1.33 % (1946470)% WARNING: option uhcvi not known. % 7.39/1.33 % (1946469)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2465979042_2999 on theBenchmark for (2999ds/0Mi) % 7.39/1.33 % (1946470)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3263736679:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.39/1.33 % (1946471)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4245743099:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.39/1.33 % (1946473)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=313112921:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.39/1.33 % (1946475)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=787042970:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.39/1.33 % (1946474)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3582453147:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.39/1.33 % Exception at run slice level % 7.39/1.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.39/1.33 % (1946472)Instruction limit reached! % 7.39/1.33 % (1946472)------------------------------ % 7.39/1.33 % (1946472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.33 % (1946472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.33 % (1946472)CaDiCaL version: 2.1.3 % 7.39/1.33 % (1946472)Termination reason: Instruction limit % 7.39/1.33 % (1946472)Termination phase: Saturation % 7.39/1.33 % (1946472)Time elapsed: 0.033 s % 7.39/1.33 % (1946472)Peak memory usage: 12 MB % 7.39/1.33 % (1946472)Instructions burned: 105 (million) % 7.39/1.33 % (1946483)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=857269647:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.39/1.33 % (1946484)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1634339545:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.39/1.33 % Exception at run slice level % 7.39/1.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.39/1.33 % (1946487)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=3255232340:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.39/1.33 % (1946473)Instruction limit reached! % 7.39/1.33 % (1946473)------------------------------ % 7.39/1.33 % (1946473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.33 % (1946473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.33 % (1946473)CaDiCaL version: 2.1.3 % 7.39/1.33 % (1946473)Termination reason: Instruction limit % 7.39/1.33 % (1946473)Termination phase: Saturation % 7.39/1.33 % (1946473)Time elapsed: 0.067 s % 7.39/1.33 % (1946473)Peak memory usage: 12 MB % 7.39/1.33 % (1946473)Instructions burned: 116 (million) % 7.39/1.33 % (1946484)Instruction limit reached! % 7.39/1.33 % (1946484)------------------------------ % 7.39/1.33 % (1946484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.33 % (1946484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.33 % (1946484)CaDiCaL version: 2.1.3 % 7.39/1.33 % (1946484)Termination reason: Instruction limit % 7.39/1.33 % (1946484)Termination phase: Saturation % 7.39/1.33 % (1946484)Time elapsed: 0.043 s % 7.39/1.33 % (1946484)Peak memory usage: 13 MB % 7.39/1.33 % (1946484)Instructions burned: 138 (million) % 7.39/1.33 % (1946474)Instruction limit reached! % 7.39/1.33 % (1946474)------------------------------ % 7.39/1.33 % (1946474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.33 % (1946474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.33 % (1946474)CaDiCaL version: 2.1.3 % 7.39/1.33 % (1946474)Termination reason: Instruction limit % 7.39/1.33 % (1946474)Termination phase: Saturation % 7.39/1.33 % (1946474)Time elapsed: 0.078 s % 7.39/1.33 % (1946474)Peak memory usage: 13 MB % 7.39/1.33 % (1946474)Instructions burned: 133 (million) % 7.39/1.33 % (1946489)ott-21_1_sil=16000:fs=off:random_seed=962947843:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.39/1.33 % (1946490)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=639301823:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.10/3.27 % (1946475)Instruction limit reached! % 21.10/3.27 % (1946475)------------------------------ % 21.10/3.27 % (1946475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.27 % (1946475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.27 % (1946475)CaDiCaL version: 2.1.3 % 21.10/3.27 % (1946475)Termination reason: Instruction limit % 21.10/3.27 % (1946475)Termination phase: Saturation % 21.10/3.27 % (1946475)Time elapsed: 0.090 s % 21.10/3.27 % (1946475)Peak memory usage: 13 MB % 21.10/3.27 % (1946475)Instructions burned: 160 (million) % 21.10/3.27 % (1946491)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=855073386:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.10/3.27 % Exception at run slice level % 21.10/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.27 % (1946494)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=902792232:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.10/3.27 % (1946496)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=64553456:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.10/3.27 % Exception at run slice level % 21.10/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.27 % (1946499)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=1171624879: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.10/3.27 % (1946489)Instruction limit reached! % 21.10/3.27 % (1946489)------------------------------ % 21.10/3.27 % (1946489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.27 % (1946489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.27 % (1946489)CaDiCaL version: 2.1.3 % 21.10/3.27 % (1946489)Termination reason: Instruction limit % 21.10/3.27 % (1946489)Termination phase: Saturation % 21.10/3.27 % (1946489)Time elapsed: 0.086 s % 21.10/3.27 % (1946489)Peak memory usage: 12 MB % 21.10/3.27 % (1946489)Instructions burned: 181 (million) % 21.10/3.27 % (1946501)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3433573554:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.10/3.27 % (1946490)Instruction limit reached! % 21.10/3.27 % (1946490)------------------------------ % 21.10/3.27 % (1946490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.27 % (1946490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.27 % (1946490)CaDiCaL version: 2.1.3 % 21.10/3.27 % (1946490)Termination reason: Instruction limit % 21.10/3.27 % (1946490)Termination phase: Saturation % 21.10/3.27 % (1946490)Time elapsed: 0.142 s % 21.10/3.27 % (1946490)Peak memory usage: 13 MB % 21.10/3.27 % (1946490)Instructions burned: 480 (million) % 21.10/3.27 % (1946503)fmb+10_1_sil=64000:random_seed=4095355501:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.10/3.27 % (1946503)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.10/3.27 % Exception at run slice level % 21.10/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.27 % (1946505)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3812621110:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.10/3.27 % Exception at run slice level % 21.10/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.27 % (1946507)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3511731819:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.10/3.27 % Exception at run slice level % 21.10/3.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.27 % (1946509)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4090778832:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.10/3.27 % (1946487)Instruction limit reached! % 21.10/3.27 % (1946487)------------------------------ % 21.10/3.27 % (1946487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.27 % (1946487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/10.36 % (1946487)CaDiCaL version: 2.1.3 % 71.46/10.36 % (1946487)Termination reason: Instruction limit % 71.46/10.36 % (1946487)Termination phase: Saturation % 71.46/10.36 % (1946487)Time elapsed: 0.357 s % 71.46/10.36 % (1946487)Peak memory usage: 15 MB % 71.46/10.36 % (1946487)Instructions burned: 684 (million) % 71.46/10.36 % (1946511)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3170497274:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 71.46/10.36 % (1946511)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.46/10.36 % (1946499)Instruction limit reached! % 71.46/10.36 % (1946499)------------------------------ % 71.46/10.36 % (1946499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.46/10.36 % (1946499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/10.36 % (1946499)CaDiCaL version: 2.1.3 % 71.46/10.36 % (1946499)Termination reason: Instruction limit % 71.46/10.36 % (1946499)Termination phase: Saturation % 71.46/10.36 % (1946499)Time elapsed: 0.399 s % 71.46/10.36 % (1946499)Peak memory usage: 16 MB % 71.46/10.36 % (1946499)Instructions burned: 692 (million) % 71.46/10.36 % (1946513)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4193446400:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 71.46/10.36 % Exception at run slice level % 71.46/10.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.46/10.36 % (1946515)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2794588568:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 71.46/10.36 % Exception at run slice level % 71.46/10.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.46/10.36 % (1946517)ott-2_1_sil=16000:newcnf=on:random_seed=937559092:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 71.46/10.36 % (1946501)Instruction limit reached! % 71.46/10.36 % (1946501)------------------------------ % 71.46/10.36 % (1946501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.46/10.36 % (1946501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/10.36 % (1946501)CaDiCaL version: 2.1.3 % 71.46/10.36 % (1946501)Termination reason: Instruction limit % 71.46/10.36 % (1946501)Termination phase: Saturation % 71.46/10.36 % (1946501)Time elapsed: 0.505 s % 71.46/10.36 % (1946501)Peak memory usage: 19 MB % 71.46/10.36 % (1946501)Instructions burned: 879 (million) % 71.46/10.36 % (1946519)ott+10_1_sil=32000:tgt=ground:random_seed=1344461266:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 71.46/10.36 % (1946494)Instruction limit reached! % 71.46/10.36 % (1946494)------------------------------ % 71.46/10.36 % (1946494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.46/10.36 % (1946494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/10.36 % (1946494)CaDiCaL version: 2.1.3 % 71.46/10.36 % (1946494)Termination reason: Instruction limit % 71.46/10.36 % (1946494)Termination phase: Saturation % 71.46/10.36 % (1946494)Time elapsed: 0.651 s % 71.46/10.36 % (1946494)Peak memory usage: 18 MB % 71.46/10.36 % (1946494)Instructions burned: 1179 (million) % 71.46/10.36 % (1946521)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2603006299:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 71.46/10.36 % Exception at run slice level % 71.46/10.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.46/10.36 % (1946523)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3932521705:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 71.46/10.36 % (1946517)Instruction limit reached! % 71.46/10.36 % (1946517)------------------------------ % 71.46/10.36 % (1946517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.46/10.36 % (1946517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/10.36 % (1946517)CaDiCaL version: 2.1.3 % 71.46/10.36 % (1946517)Termination reason: Instruction limit % 71.46/10.36 % (1946517)Termination phase: Saturation % 71.46/10.36 % (1946517)Time elapsed: 0.397 s % 71.46/10.36 % (1946517)Peak memory usage: 13 MB % 71.46/10.36 % (1946517)Instructions burned: 870 (million) % 71.46/10.36 % (1946525)dis+21_1_sil=32000:sas=cadical:random_seed=3223917903:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 71.46/10.36 % (1946511)Instruction limit reached! % 71.46/10.36 % (1946511)------------------------------ % 71.46/10.36 % (1946511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.20/16.11 % (1946511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.11 % (1946511)CaDiCaL version: 2.1.3 % 112.20/16.11 % (1946511)Termination reason: Instruction limit % 112.20/16.11 % (1946511)Termination phase: Saturation % 112.20/16.11 % (1946511)Time elapsed: 0.647 s % 112.20/16.11 % (1946511)Peak memory usage: 16 MB % 112.20/16.11 % (1946511)Instructions burned: 1473 (million) % 112.20/16.11 % (1946527)ott+11_1_sil=16000:gs=on:random_seed=3451599470:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 112.20/16.11 % (1946509)Instruction limit reached! % 112.20/16.11 % (1946509)------------------------------ % 112.20/16.11 % (1946509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.20/16.11 % (1946509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.11 % (1946509)CaDiCaL version: 2.1.3 % 112.20/16.11 % (1946509)Termination reason: Instruction limit % 112.20/16.11 % (1946509)Termination phase: Saturation % 112.20/16.11 % (1946509)Time elapsed: 1.426 s % 112.20/16.11 % (1946509)Peak memory usage: 36 MB % 112.20/16.11 % (1946509)Instructions burned: 5132 (million) % 112.20/16.11 % (1946529)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3064053327:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 112.20/16.11 % Exception at run slice level % 112.20/16.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.20/16.11 % (1946531)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2870859280:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 112.20/16.11 % (1946527)Instruction limit reached! % 112.20/16.11 % (1946527)------------------------------ % 112.20/16.11 % (1946527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.20/16.11 % (1946527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.11 % (1946527)CaDiCaL version: 2.1.3 % 112.20/16.11 % (1946527)Termination reason: Instruction limit % 112.20/16.11 % (1946527)Termination phase: Saturation % 112.20/16.11 % (1946527)Time elapsed: 1.213 s % 112.20/16.11 % (1946527)Peak memory usage: 21 MB % 112.20/16.11 % (1946527)Instructions burned: 2253 (million) % 112.20/16.11 % (1946533)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1615559682:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 112.20/16.11 % (1946523)Instruction limit reached! % 112.20/16.11 % (1946523)------------------------------ % 112.20/16.11 % (1946523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.20/16.11 % (1946523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.11 % (1946523)CaDiCaL version: 2.1.3 % 112.20/16.11 % (1946523)Termination reason: Instruction limit % 112.20/16.11 % (1946523)Termination phase: Saturation % 112.20/16.11 % (1946523)Time elapsed: 1.842 s % 112.20/16.11 % (1946523)Peak memory usage: 28 MB % 112.20/16.11 % (1946523)Instructions burned: 3513 (million) % 112.20/16.11 % (1946535)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4079021571:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 112.20/16.11 % (1946531)Instruction limit reached! % 112.20/16.11 % (1946531)------------------------------ % 112.20/16.11 % (1946531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.20/16.11 % (1946531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.11 % (1946531)CaDiCaL version: 2.1.3 % 112.20/16.11 % (1946531)Termination reason: Instruction limit % 112.20/16.11 % (1946531)Termination phase: Saturation % 112.20/16.11 % (1946531)Time elapsed: 1.216 s % 112.20/16.11 % (1946531)Peak memory usage: 50 MB % 112.20/16.11 % (1946531)Instructions burned: 4592 (million) % 112.20/16.11 % (1946537)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2072889365:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 112.20/16.11 % Exception at run slice level % 112.20/16.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.20/16.11 % (1946539)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3517907353:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 112.20/16.11 % Exception at run slice level % 112.20/16.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 112.20/16.11 % (1946541)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3230635659:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 112.20/16.11 % Exception at run slice level % 133.47/19.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.47/19.09 % (1946543)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3187369149:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 133.47/19.09 % (1946525)Instruction limit reached! % 133.47/19.09 % (1946525)------------------------------ % 133.47/19.09 % (1946525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946525)CaDiCaL version: 2.1.3 % 133.47/19.09 % (1946525)Termination reason: Instruction limit % 133.47/19.09 % (1946525)Termination phase: Saturation % 133.47/19.09 % (1946525)Time elapsed: 2.028 s % 133.47/19.09 % (1946525)Peak memory usage: 32 MB % 133.47/19.09 % (1946525)Instructions burned: 3774 (million) % 133.47/19.09 % (1946545)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2766889655:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 133.47/19.09 % (1946519)Instruction limit reached! % 133.47/19.09 % (1946519)------------------------------ % 133.47/19.09 % (1946519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946519)CaDiCaL version: 2.1.3 % 133.47/19.09 % (1946519)Termination reason: Instruction limit % 133.47/19.09 % (1946519)Termination phase: Saturation % 133.47/19.09 % (1946519)Time elapsed: 2.610 s % 133.47/19.09 % (1946519)Peak memory usage: 22 MB % 133.47/19.09 % (1946519)Instructions burned: 5115 (million) % 133.47/19.09 % (1946547)dis+10_16:1_sil=16000:random_seed=1461683202:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 133.47/19.09 % (1946535)Instruction limit reached! % 133.47/19.09 % (1946535)------------------------------ % 133.47/19.09 % (1946535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946535)CaDiCaL version: 2.1.3 % 133.47/19.09 % (1946535)Termination reason: Instruction limit % 133.47/19.09 % (1946535)Termination phase: Saturation % 133.47/19.09 % (1946535)Time elapsed: 2.804 s % 133.47/19.09 % (1946535)Peak memory usage: 46 MB % 133.47/19.09 % (1946535)Instructions burned: 5212 (million) % 133.47/19.09 % (1946549)ott-3_8_sil=64000:random_seed=3577799291:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 133.47/19.09 % (1946545)Instruction limit reached! % 133.47/19.09 % (1946545)------------------------------ % 133.47/19.09 % (1946545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946545)CaDiCaL version: 2.1.3 % 133.47/19.09 % (1946545)Termination reason: Instruction limit % 133.47/19.09 % (1946545)Termination phase: Saturation % 133.47/19.09 % (1946545)Time elapsed: 4.584 s % 133.47/19.09 % (1946545)Peak memory usage: 53 MB % 133.47/19.09 % (1946545)Instructions burned: 8174 (million) % 133.47/19.09 % (1946551)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2315298542:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 133.47/19.09 % Exception at run slice level % 133.47/19.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 133.47/19.09 % (1946553)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3281516554:i=11404_2922 on theBenchmark for (2922ds/11404Mi) % 133.47/19.09 % (1946547)Instruction limit reached! % 133.47/19.09 % (1946547)------------------------------ % 133.47/19.09 % (1946547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946547)CaDiCaL version: 2.1.3 % 133.47/19.09 % (1946547)Termination reason: Instruction limit % 133.47/19.09 % (1946547)Termination phase: Saturation % 133.47/19.09 % (1946547)Time elapsed: 4.859 s % 133.47/19.09 % (1946547)Peak memory usage: 53 MB % 133.47/19.09 % (1946547)Instructions burned: 9155 (million) % 133.47/19.09 % (1946555)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1093509426:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 133.47/19.09 % (1946543)Instruction limit reached! % 133.47/19.09 % (1946543)------------------------------ % 133.47/19.09 % (1946543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.47/19.09 % (1946543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.47/19.09 % (1946543)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946543)Termination reason: Instruction limit % 141.27/20.16 % (1946543)Termination phase: Saturation % 141.27/20.16 % (1946543)Time elapsed: 7.075 s % 141.27/20.16 % (1946543)Peak memory usage: 124 MB % 141.27/20.16 % (1946543)Instructions burned: 22566 (million) % 141.27/20.16 % (1946557)dis+33_16_sil=32000:sac=on:random_seed=1114861095:i=15851:nm=0_2898 on theBenchmark for (2898ds/15851Mi) % 141.27/20.16 % (1946557)Instruction limit reached! % 141.27/20.16 % (1946557)------------------------------ % 141.27/20.16 % (1946557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.27/20.16 % (1946557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.27/20.16 % (1946557)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946557)Termination reason: Instruction limit % 141.27/20.16 % (1946557)Termination phase: Saturation % 141.27/20.16 % (1946557)Time elapsed: 3.681 s % 141.27/20.16 % (1946557)Peak memory usage: 35 MB % 141.27/20.16 % (1946557)Instructions burned: 15854 (million) % 141.27/20.16 % (1946561)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3277075264:avsq=on:i=17627:add=on:amm=off_2861 on theBenchmark for (2861ds/17627Mi) % 141.27/20.16 % (1946553)Instruction limit reached! % 141.27/20.16 % (1946553)------------------------------ % 141.27/20.16 % (1946553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.27/20.16 % (1946553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.27/20.16 % (1946553)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946553)Termination reason: Instruction limit % 141.27/20.16 % (1946553)Termination phase: Saturation % 141.27/20.16 % (1946553)Time elapsed: 7.142 s % 141.27/20.16 % (1946553)Peak memory usage: 82 MB % 141.27/20.16 % (1946553)Instructions burned: 11405 (million) % 141.27/20.16 % (1946920)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1481041796:s2a=on:i=53295_2850 on theBenchmark for (2850ds/53295Mi) % 141.27/20.16 % (1946533)Instruction limit reached! % 141.27/20.16 % (1946533)------------------------------ % 141.27/20.16 % (1946533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.27/20.16 % (1946533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.27/20.16 % (1946533)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946533)Termination reason: Instruction limit % 141.27/20.16 % (1946533)Termination phase: Saturation % 141.27/20.16 % (1946533)Time elapsed: 13.289 s % 141.27/20.16 % (1946533)Peak memory usage: 75 MB % 141.27/20.16 % (1946533)Instructions burned: 29341 (million) % 141.27/20.16 % (1946922)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2783772272:i=26857:ins=20_2843 on theBenchmark for (2843ds/26857Mi) % 141.27/20.16 % Exception at run slice level % 141.27/20.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.27/20.16 % (1946924)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2109741784:i=28120:bs=on:fsr=off_2842 on theBenchmark for (2842ds/28120Mi) % 141.27/20.16 % (1946555)Instruction limit reached! % 141.27/20.16 % (1946555)------------------------------ % 141.27/20.16 % (1946555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.27/20.16 % (1946555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.27/20.16 % (1946555)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946555)Termination reason: Instruction limit % 141.27/20.16 % (1946555)Termination phase: Saturation % 141.27/20.16 % (1946555)Time elapsed: 7.568 s % 141.27/20.16 % (1946555)Peak memory usage: 46 MB % 141.27/20.16 % (1946555)Instructions burned: 14134 (million) % 141.27/20.16 % (1946926)fmb+10_1_sil=256000:fmbss=7:random_seed=983236922:fmbsr=1.6:i=182295_2841 on theBenchmark for (2841ds/182295Mi) % 141.27/20.16 % (1946549)Instruction limit reached! % 141.27/20.16 % (1946549)------------------------------ % 141.27/20.16 % (1946549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.27/20.16 % (1946549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.27/20.16 % (1946549)CaDiCaL version: 2.1.3 % 141.27/20.16 % (1946549)Termination reason: Instruction limit % 141.27/20.16 % (1946549)Termination phase: Saturation % 141.27/20.16 % (1946549)Time elapsed: 10.326 s % 141.27/20.16 % (1946549)Peak memory usage: 34 MB % 141.27/20.16 % (1946549)Instructions burned: 20140 (million) % 141.27/20.16 % Exception at run slice level % 141.27/20.16 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 141.27/20.16 % (1946928)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=136099915:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi) % 141.27/20.16 % (1946929)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2488190289:i=160505_2841 on theBenchmark for (2841ds/160505Mi) % 176.05/25.11 % (1946928)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 176.05/25.11 % Exception at run slice level % 176.05/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.05/25.11 % Exception at run slice level % 176.05/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.05/25.11 % (1946932)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=583598509:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 176.05/25.11 % (1946933)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3712897067:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi) % 176.05/25.11 % Exception at run slice level % 176.05/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.05/25.11 % Exception at run slice level % 176.05/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.05/25.11 % (1946937)% WARNING: option uhcvi not known. % 176.05/25.11 % (1946936)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3965156089:rtra=on_2840 on theBenchmark for (2840ds/0Mi) % 176.05/25.11 % (1946937)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4253303442:i=271062:add=off:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/271062Mi) % 176.05/25.11 % Exception at run slice level % 176.05/25.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.05/25.11 % (1946940)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2967527650:i=176048:add=on:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/176048Mi) % 176.05/25.11 % (1946561)Instruction limit reached! % 176.05/25.11 % (1946561)------------------------------ % 176.05/25.11 % (1946561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.05/25.11 % (1946561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.05/25.11 % (1946561)CaDiCaL version: 2.1.3 % 176.05/25.11 % (1946561)Termination reason: Instruction limit % 176.05/25.11 % (1946561)Termination phase: Saturation % 176.05/25.11 % (1946561)Time elapsed: 4.718 s % 176.05/25.11 % (1946561)Peak memory usage: 49 MB % 176.05/25.11 % (1946561)Instructions burned: 17627 (million) % 176.05/25.11 % (1946942)dis+10_1_sil=32000:si=on:sp=arity:random_seed=502942889:i=206:fgj=on:rtra=on_2814 on theBenchmark for (2814ds/206Mi) % 176.05/25.11 % (1946942)Instruction limit reached! % 176.05/25.11 % (1946942)------------------------------ % 176.05/25.11 % (1946942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.05/25.11 % (1946942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.05/25.11 % (1946942)CaDiCaL version: 2.1.3 % 176.05/25.11 % (1946942)Termination reason: Instruction limit % 176.05/25.11 % (1946942)Termination phase: Saturation % 176.05/25.11 % (1946942)Time elapsed: 0.064 s % 176.05/25.11 % (1946942)Peak memory usage: 13 MB % 176.05/25.11 % (1946942)Instructions burned: 208 (million) % 176.05/25.11 % (1946944)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2921314305:i=232:rtra=on_2813 on theBenchmark for (2813ds/232Mi) % 176.05/25.11 % (1946944)Instruction limit reached! % 176.05/25.11 % (1946944)------------------------------ % 176.05/25.11 % (1946944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.05/25.11 % (1946944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.05/25.11 % (1946944)CaDiCaL version: 2.1.3 % 176.05/25.11 % (1946944)Termination reason: Instruction limit % 176.05/25.11 % (1946944)Termination phase: Saturation % 176.05/25.11 % (1946944)Time elapsed: 0.075 s % 176.05/25.11 % (1946944)Peak memory usage: 13 MB % 176.05/25.11 % (1946944)Instructions burned: 233 (million) % 176.05/25.11 % (1946946)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3199864540:i=262:rtra=on_2812 on theBenchmark for (2812ds/262Mi) % 176.05/25.11 % (1946946)Instruction limit reached! % 176.05/25.11 % (1946946)------------------------------ % 176.05/25.11 % (1946946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.05/25.11 % (1946946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.05/25.11 % (1946946)CaDiCaL version: 2.1.3 % 176.05/25.11 % (1946946)Termination reason: Instruction limit % 176.05/25.11 % (1946946)Termination phase: Saturation % 219.47/31.15 % (1946946)Time elapsed: 0.090 s % 219.47/31.15 % (1946946)Peak memory usage: 14 MB % 219.47/31.15 % (1946946)Instructions burned: 263 (million) % 219.47/31.15 % (1946948)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1419752146:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2811 on theBenchmark for (2811ds/318Mi) % 219.47/31.15 % (1946948)Instruction limit reached! % 219.47/31.15 % (1946948)------------------------------ % 219.47/31.15 % (1946948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.15 % (1946948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.15 % (1946948)CaDiCaL version: 2.1.3 % 219.47/31.15 % (1946948)Termination reason: Instruction limit % 219.47/31.15 % (1946948)Termination phase: Saturation % 219.47/31.15 % (1946948)Time elapsed: 0.097 s % 219.47/31.15 % (1946948)Peak memory usage: 13 MB % 219.47/31.15 % (1946948)Instructions burned: 324 (million) % 219.47/31.15 % (1946950)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=168802854:i=1428:nm=2:rtra=on_2810 on theBenchmark for (2810ds/1428Mi) % 219.47/31.15 % Exception at run slice level % 219.47/31.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.47/31.15 % (1946952)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=792271716:i=262:bd=preordered:rtra=on:fsd=on_2809 on theBenchmark for (2809ds/262Mi) % 219.47/31.15 % (1946952)Instruction limit reached! % 219.47/31.15 % (1946952)------------------------------ % 219.47/31.15 % (1946952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.15 % (1946952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.15 % (1946952)CaDiCaL version: 2.1.3 % 219.47/31.15 % (1946952)Termination reason: Instruction limit % 219.47/31.15 % (1946952)Termination phase: Saturation % 219.47/31.15 % (1946952)Time elapsed: 0.087 s % 219.47/31.15 % (1946952)Peak memory usage: 13 MB % 219.47/31.15 % (1946952)Instructions burned: 262 (million) % 219.47/31.15 % (1946954)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=1055238397:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1368Mi) % 219.47/31.15 % (1946954)Instruction limit reached! % 219.47/31.15 % (1946954)------------------------------ % 219.47/31.15 % (1946954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.15 % (1946954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.15 % (1946954)CaDiCaL version: 2.1.3 % 219.47/31.15 % (1946954)Termination reason: Instruction limit % 219.47/31.15 % (1946954)Termination phase: Saturation % 219.47/31.15 % (1946954)Time elapsed: 0.398 s % 219.47/31.15 % (1946954)Peak memory usage: 16 MB % 219.47/31.15 % (1946954)Instructions burned: 1368 (million) % 219.47/31.15 % (1946956)ott-21_1_sil=16000:si=on:fs=off:random_seed=520263616:i=360:av=off:fsr=off:rtra=on_2804 on theBenchmark for (2804ds/360Mi) % 219.47/31.15 % (1946956)Instruction limit reached! % 219.47/31.15 % (1946956)------------------------------ % 219.47/31.15 % (1946956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.15 % (1946956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.15 % (1946956)CaDiCaL version: 2.1.3 % 219.47/31.15 % (1946956)Termination reason: Instruction limit % 219.47/31.15 % (1946956)Termination phase: Saturation % 219.47/31.15 % (1946956)Time elapsed: 0.091 s % 219.47/31.15 % (1946956)Peak memory usage: 13 MB % 219.47/31.15 % (1946956)Instructions burned: 361 (million) % 219.47/31.15 % (1946958)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4243258855:i=954:bd=all:rtra=on_2803 on theBenchmark for (2803ds/954Mi) % 219.47/31.15 % (1946958)Instruction limit reached! % 219.47/31.15 % (1946958)------------------------------ % 219.47/31.15 % (1946958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.15 % (1946958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.15 % (1946958)CaDiCaL version: 2.1.3 % 219.47/31.15 % (1946958)Termination reason: Instruction limit % 219.47/31.15 % (1946958)Termination phase: Saturation % 219.47/31.15 % (1946958)Time elapsed: 0.283 s % 219.47/31.15 % (1946958)Peak memory usage: 15 MB % 219.47/31.15 % (1946958)Instructions burned: 956 (million) % 219.47/31.15 % (1946960)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2593278272:fmbsr=1.3:i=1730:ins=25:rtra=on_2800 on theBenchmark for (2800ds/1730Mi) % 219.47/31.15 % Exception at run slice level % 219.47/31.15 User error: Finite model building is currentlyTerminated % 300.13/42.54 % Vampire exiting % 300.13/42.54 Terminated %------------------------------------------------------------------------------