%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW493_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 : n014.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:19 PM UTC 2026 % Result : Timeout 296.09s 41.96s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW493_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.16 % Computer : n014.cluster.edu % 0.10/0.16 % Model : x86_64 x86_64 % 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.16 % Memory : 8046.5625MB % 0.10/0.16 % OS : Linux 6.8.0-71-generic % 0.10/0.16 % CPULimit : 300 % 0.10/0.16 % WCLimit : 300 % 0.10/0.16 % DateTime : Mon Sep 28 14:14:45 UTC 2026 % 0.10/0.16 % CPUTime : % 0.10/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.19 Running first-order model finding % 0.10/0.19 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 % 8.14/1.42 % (1795831)Will run a generic schedule for satisfiability detection. % 8.14/1.42 % (1795842)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3348136095:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.14/1.42 % (1795837)% WARNING: option uhcvi not known. % 8.14/1.42 % (1795838)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=428906787:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.14/1.42 % (1795841)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2384004350:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.14/1.42 % (1795836)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4042345243_2999 on theBenchmark for (2999ds/0Mi) % 8.14/1.42 % (1795837)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3481783417:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.14/1.42 % (1795840)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2565036533:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.14/1.42 % (1795839)dis+10_1_sil=32000:sp=arity:random_seed=565955695:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.14/1.42 % Exception at run slice level % 8.14/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.14/1.42 % (1795850)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1988134826:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.14/1.42 % (1795842)Instruction limit reached! % 8.14/1.42 % (1795842)------------------------------ % 8.14/1.42 % (1795842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.14/1.42 % (1795842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.14/1.42 % (1795842)CaDiCaL version: 2.1.3 % 8.14/1.42 % (1795842)Termination reason: Instruction limit % 8.14/1.42 % (1795842)Termination phase: Saturation % 8.14/1.42 % (1795842)Time elapsed: 0.041 s % 8.14/1.42 % (1795842)Peak memory usage: 13 MB % 8.14/1.42 % (1795842)Instructions burned: 161 (million) % 8.14/1.42 % Exception at run slice level % 8.14/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.14/1.42 % (1795852)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3634693714:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.14/1.42 % (1795853)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=1031695989:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.14/1.42 % (1795840)Instruction limit reached! % 8.14/1.42 % (1795840)------------------------------ % 8.14/1.42 % (1795840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.14/1.42 % (1795840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.14/1.42 % (1795840)CaDiCaL version: 2.1.3 % 8.14/1.42 % (1795840)Termination reason: Instruction limit % 8.14/1.42 % (1795840)Termination phase: Saturation % 8.14/1.42 % (1795840)Time elapsed: 0.059 s % 8.14/1.42 % (1795840)Peak memory usage: 12 MB % 8.14/1.42 % (1795840)Instructions burned: 117 (million) % 8.14/1.42 % (1795841)Instruction limit reached! % 8.14/1.42 % (1795841)------------------------------ % 8.14/1.42 % (1795841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.14/1.42 % (1795841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.14/1.42 % (1795841)CaDiCaL version: 2.1.3 % 8.14/1.42 % (1795841)Termination reason: Instruction limit % 8.14/1.42 % (1795841)Termination phase: Saturation % 8.14/1.42 % (1795841)Time elapsed: 0.081 s % 8.14/1.42 % (1795841)Peak memory usage: 13 MB % 8.14/1.42 % (1795841)Instructions burned: 131 (million) % 8.14/1.42 % (1795856)ott-21_1_sil=16000:fs=off:random_seed=1927984311:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.14/1.42 % (1795852)Instruction limit reached! % 8.14/1.42 % (1795852)------------------------------ % 8.14/1.42 % (1795852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.14/1.42 % (1795852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.14/1.42 % (1795852)CaDiCaL version: 2.1.3 % 8.14/1.42 % (1795852)Termination reason: Instruction limit % 8.14/1.42 % (1795852)Termination phase: Saturation % 8.14/1.42 % (1795852)Time elapsed: 0.041 s % 8.14/1.42 % (1795852)Peak memory usage: 13 MB % 8.14/1.42 % (1795852)Instructions burned: 131 (million) % 8.14/1.42 % (1795839)Instruction limit reached! % 23.27/3.61 % (1795839)------------------------------ % 23.27/3.61 % (1795839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.27/3.61 % (1795839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.27/3.61 % (1795839)CaDiCaL version: 2.1.3 % 23.27/3.61 % (1795839)Termination reason: Instruction limit % 23.27/3.61 % (1795839)Termination phase: Saturation % 23.27/3.61 % (1795839)Time elapsed: 0.089 s % 23.27/3.61 % (1795839)Peak memory usage: 12 MB % 23.27/3.61 % (1795839)Instructions burned: 108 (million) % 23.27/3.61 % (1795859)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3495220574:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 23.27/3.61 % (1795858)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=516212551:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 23.27/3.61 % Exception at run slice level % 23.27/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 23.27/3.61 % (1795863)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2586176755:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 23.27/3.61 % Exception at run slice level % 23.27/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 23.27/3.61 % (1795860)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3468659516:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 23.27/3.61 % (1795865)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=545088578: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) % 23.27/3.61 % (1795856)Instruction limit reached! % 23.27/3.61 % (1795856)------------------------------ % 23.27/3.61 % (1795856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.27/3.61 % (1795856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.27/3.61 % (1795856)CaDiCaL version: 2.1.3 % 23.27/3.61 % (1795856)Termination reason: Instruction limit % 23.27/3.61 % (1795856)Termination phase: Saturation % 23.27/3.61 % (1795856)Time elapsed: 0.098 s % 23.27/3.61 % (1795856)Peak memory usage: 13 MB % 23.27/3.61 % (1795856)Instructions burned: 181 (million) % 23.27/3.61 % (1795881)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2291045426:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.27/3.61 % (1795865)Instruction limit reached! % 23.27/3.61 % (1795865)------------------------------ % 23.27/3.61 % (1795865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.27/3.61 % (1795865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.27/3.61 % (1795865)CaDiCaL version: 2.1.3 % 23.27/3.61 % (1795865)Termination reason: Instruction limit % 23.27/3.61 % (1795865)Termination phase: Saturation % 23.27/3.61 % (1795865)Time elapsed: 0.168 s % 23.27/3.61 % (1795865)Peak memory usage: 17 MB % 23.27/3.61 % (1795865)Instructions burned: 693 (million) % 23.27/3.61 % (1795930)fmb+10_1_sil=64000:random_seed=2592015075:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 23.27/3.61 % (1795930)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.27/3.61 % Exception at run slice level % 23.27/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 23.27/3.61 % (1795936)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2533620652:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 23.27/3.61 % Exception at run slice level % 23.27/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 23.27/3.61 % (1795940)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3758094617:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 23.27/3.61 % Exception at run slice level % 23.27/3.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 23.27/3.61 % (1795942)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=507802296:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 23.27/3.61 % (1795858)Instruction limit reached! % 23.27/3.61 % (1795858)------------------------------ % 23.27/3.61 % (1795858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.27/3.61 % (1795858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.71/10.11 % (1795858)CaDiCaL version: 2.1.3 % 69.71/10.11 % (1795858)Termination reason: Instruction limit % 69.71/10.11 % (1795858)Termination phase: Saturation % 69.71/10.11 % (1795858)Time elapsed: 0.303 s % 69.71/10.11 % (1795858)Peak memory usage: 15 MB % 69.71/10.11 % (1795858)Instructions burned: 478 (million) % 69.71/10.11 % (1795961)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3814906136:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 69.71/10.11 % (1795961)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 69.71/10.11 % (1795853)Instruction limit reached! % 69.71/10.11 % (1795853)------------------------------ % 69.71/10.11 % (1795853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.71/10.11 % (1795853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.71/10.11 % (1795853)CaDiCaL version: 2.1.3 % 69.71/10.11 % (1795853)Termination reason: Instruction limit % 69.71/10.11 % (1795853)Termination phase: Saturation % 69.71/10.11 % (1795853)Time elapsed: 0.404 s % 69.71/10.11 % (1795853)Peak memory usage: 18 MB % 69.71/10.11 % (1795853)Instructions burned: 684 (million) % 69.71/10.11 % (1795976)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1212333686:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 69.71/10.11 % Exception at run slice level % 69.71/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.71/10.11 % (1795984)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=714041250:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 69.71/10.11 % Exception at run slice level % 69.71/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.71/10.11 % (1795990)ott-2_1_sil=16000:newcnf=on:random_seed=3078139883:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 69.71/10.11 % (1795881)Instruction limit reached! % 69.71/10.11 % (1795881)------------------------------ % 69.71/10.11 % (1795881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.71/10.11 % (1795881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.71/10.11 % (1795881)CaDiCaL version: 2.1.3 % 69.71/10.11 % (1795881)Termination reason: Instruction limit % 69.71/10.11 % (1795881)Termination phase: Saturation % 69.71/10.11 % (1795881)Time elapsed: 0.516 s % 69.71/10.11 % (1795881)Peak memory usage: 21 MB % 69.71/10.11 % (1795881)Instructions burned: 879 (million) % 69.71/10.11 % (1796016)ott+10_1_sil=32000:tgt=ground:random_seed=1461623755:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 69.71/10.11 % (1795860)Instruction limit reached! % 69.71/10.11 % (1795860)------------------------------ % 69.71/10.11 % (1795860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.71/10.11 % (1795860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.71/10.11 % (1795860)CaDiCaL version: 2.1.3 % 69.71/10.11 % (1795860)Termination reason: Instruction limit % 69.71/10.11 % (1795860)Termination phase: Saturation % 69.71/10.11 % (1795860)Time elapsed: 0.725 s % 69.71/10.11 % (1795860)Peak memory usage: 24 MB % 69.71/10.11 % (1795860)Instructions burned: 1179 (million) % 69.71/10.11 % (1796018)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1470773982:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 69.71/10.11 % Exception at run slice level % 69.71/10.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 69.71/10.11 % (1796020)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3590221021:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 69.71/10.11 % (1795961)Instruction limit reached! % 69.71/10.11 % (1795961)------------------------------ % 69.71/10.11 % (1795961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.71/10.11 % (1795961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.71/10.11 % (1795961)CaDiCaL version: 2.1.3 % 69.71/10.11 % (1795961)Termination reason: Instruction limit % 69.71/10.11 % (1795961)Termination phase: Saturation % 69.71/10.11 % (1795961)Time elapsed: 0.714 s % 69.71/10.11 % (1795961)Peak memory usage: 35 MB % 69.71/10.11 % (1795961)Instructions burned: 1473 (million) % 69.71/10.11 % (1796022)dis+21_1_sil=32000:sas=cadical:random_seed=1838457590:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 69.71/10.11 % (1795990)Instruction limit reached! % 69.71/10.11 % (1795990)------------------------------ % 69.71/10.11 % (1795990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.69/18.25 % (1795990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.69/18.25 % (1795990)CaDiCaL version: 2.1.3 % 127.69/18.25 % (1795990)Termination reason: Instruction limit % 127.69/18.25 % (1795990)Termination phase: Saturation % 127.69/18.25 % (1795990)Time elapsed: 0.649 s % 127.69/18.25 % (1795990)Peak memory usage: 16 MB % 127.69/18.25 % (1795990)Instructions burned: 870 (million) % 127.69/18.25 % (1796024)ott+11_1_sil=16000:gs=on:random_seed=289159444:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 127.69/18.25 % (1795942)Instruction limit reached! % 127.69/18.25 % (1795942)------------------------------ % 127.69/18.25 % (1795942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.69/18.25 % (1795942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.69/18.25 % (1795942)CaDiCaL version: 2.1.3 % 127.69/18.25 % (1795942)Termination reason: Instruction limit % 127.69/18.25 % (1795942)Termination phase: Saturation % 127.69/18.25 % (1795942)Time elapsed: 1.694 s % 127.69/18.25 % (1795942)Peak memory usage: 31 MB % 127.69/18.25 % (1795942)Instructions burned: 5132 (million) % 127.69/18.25 % (1796043)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=214232876:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 127.69/18.25 % Exception at run slice level % 127.69/18.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 127.69/18.25 % (1796045)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1414669273:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 127.69/18.25 % (1796024)Instruction limit reached! % 127.69/18.25 % (1796024)------------------------------ % 127.69/18.25 % (1796024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.69/18.25 % (1796024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.69/18.25 % (1796024)CaDiCaL version: 2.1.3 % 127.69/18.25 % (1796024)Termination reason: Instruction limit % 127.69/18.25 % (1796024)Termination phase: Saturation % 127.69/18.25 % (1796024)Time elapsed: 1.699 s % 127.69/18.25 % (1796024)Peak memory usage: 42 MB % 127.69/18.25 % (1796024)Instructions burned: 2251 (million) % 127.69/18.25 % (1796199)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2009334227:i=29340_2970 on theBenchmark for (2970ds/29340Mi) % 127.69/18.25 % (1796020)Instruction limit reached! % 127.69/18.25 % (1796020)------------------------------ % 127.69/18.25 % (1796020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.69/18.25 % (1796020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.69/18.25 % (1796020)CaDiCaL version: 2.1.3 % 127.69/18.25 % (1796020)Termination reason: Instruction limit % 127.69/18.25 % (1796020)Termination phase: Saturation % 127.69/18.25 % (1796020)Time elapsed: 2.109 s % 127.69/18.25 % (1796020)Peak memory usage: 25 MB % 127.69/18.25 % (1796020)Instructions burned: 3513 (million) % 127.69/18.25 % (1796201)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3724495457:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 127.69/18.25 % (1796045)Instruction limit reached! % 127.69/18.25 % (1796045)------------------------------ % 127.69/18.25 % (1796045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.69/18.25 % (1796045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.69/18.25 % (1796045)CaDiCaL version: 2.1.3 % 127.69/18.25 % (1796045)Termination reason: Instruction limit % 127.69/18.25 % (1796045)Termination phase: Saturation % 127.69/18.25 % (1796045)Time elapsed: 1.261 s % 127.69/18.25 % (1796045)Peak memory usage: 24 MB % 127.69/18.25 % (1796045)Instructions burned: 4594 (million) % 127.69/18.25 % (1796203)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=190973962:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi) % 127.69/18.25 % Exception at run slice level % 127.69/18.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 127.69/18.25 % (1796205)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4253261275:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 127.69/18.25 % Exception at run slice level % 127.69/18.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 127.69/18.25 % (1796207)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3844318747:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 127.69/18.25 % Exception at run slice level % 137.63/19.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 137.63/19.67 % (1796209)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3776722770:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 137.63/19.67 % (1796022)Instruction limit reached! % 137.63/19.67 % (1796022)------------------------------ % 137.63/19.67 % (1796022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796022)CaDiCaL version: 2.1.3 % 137.63/19.67 % (1796022)Termination reason: Instruction limit % 137.63/19.67 % (1796022)Termination phase: Saturation % 137.63/19.67 % (1796022)Time elapsed: 2.359 s % 137.63/19.67 % (1796022)Peak memory usage: 28 MB % 137.63/19.67 % (1796022)Instructions burned: 3773 (million) % 137.63/19.67 % (1796211)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3872065541:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi) % 137.63/19.67 % (1796016)Instruction limit reached! % 137.63/19.67 % (1796016)------------------------------ % 137.63/19.67 % (1796016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796016)CaDiCaL version: 2.1.3 % 137.63/19.67 % (1796016)Termination reason: Instruction limit % 137.63/19.67 % (1796016)Termination phase: Saturation % 137.63/19.67 % (1796016)Time elapsed: 3.195 s % 137.63/19.67 % (1796016)Peak memory usage: 42 MB % 137.63/19.67 % (1796016)Instructions burned: 5114 (million) % 137.63/19.67 % (1796213)dis+10_16:1_sil=16000:random_seed=1859618952:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 137.63/19.67 % (1796201)Instruction limit reached! % 137.63/19.67 % (1796201)------------------------------ % 137.63/19.67 % (1796201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796201)CaDiCaL version: 2.1.3 % 137.63/19.67 % (1796201)Termination reason: Instruction limit % 137.63/19.67 % (1796201)Termination phase: Saturation % 137.63/19.67 % (1796201)Time elapsed: 2.499 s % 137.63/19.67 % (1796201)Peak memory usage: 50 MB % 137.63/19.67 % (1796201)Instructions burned: 5212 (million) % 137.63/19.67 % (1796215)ott-3_8_sil=64000:random_seed=3100076090:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 137.63/19.67 % (1796211)Instruction limit reached! % 137.63/19.67 % (1796211)------------------------------ % 137.63/19.67 % (1796211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796211)CaDiCaL version: 2.1.3 % 137.63/19.67 % (1796211)Termination reason: Instruction limit % 137.63/19.67 % (1796211)Termination phase: Saturation % 137.63/19.67 % (1796211)Time elapsed: 4.650 s % 137.63/19.67 % (1796211)Peak memory usage: 75 MB % 137.63/19.67 % (1796211)Instructions burned: 8175 (million) % 137.63/19.67 % (1796217)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=521718522:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 137.63/19.67 % Exception at run slice level % 137.63/19.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 137.63/19.67 % (1796219)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2379131049:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 137.63/19.67 % (1796213)Instruction limit reached! % 137.63/19.67 % (1796213)------------------------------ % 137.63/19.67 % (1796213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796213)CaDiCaL version: 2.1.3 % 137.63/19.67 % (1796213)Termination reason: Instruction limit % 137.63/19.67 % (1796213)Termination phase: Saturation % 137.63/19.67 % (1796213)Time elapsed: 4.719 s % 137.63/19.67 % (1796213)Peak memory usage: 95 MB % 137.63/19.67 % (1796213)Instructions burned: 9156 (million) % 137.63/19.67 % (1796221)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1893574115:i=14134_2912 on theBenchmark for (2912ds/14134Mi) % 137.63/19.67 % (1796209)Instruction limit reached! % 137.63/19.67 % (1796209)------------------------------ % 137.63/19.67 % (1796209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.63/19.67 % (1796209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.63/19.67 % (1796209)CaDiCaL version: 2.1.3 % 146.15/20.81 % (1796209)Termination reason: Instruction limit % 146.15/20.81 % (1796209)Termination phase: Saturation % 146.15/20.81 % (1796209)Time elapsed: 6.487 s % 146.15/20.81 % (1796209)Peak memory usage: 71 MB % 146.15/20.81 % (1796209)Instructions burned: 22565 (million) % 146.15/20.81 % (1796223)dis+33_16_sil=32000:sac=on:random_seed=4259180516:i=15851:nm=0_2900 on theBenchmark for (2900ds/15851Mi) % 146.15/20.81 % (1796223)Instruction limit reached! % 146.15/20.81 % (1796223)------------------------------ % 146.15/20.81 % (1796223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/20.81 % (1796223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/20.81 % (1796223)CaDiCaL version: 2.1.3 % 146.15/20.81 % (1796223)Termination reason: Instruction limit % 146.15/20.81 % (1796223)Termination phase: Saturation % 146.15/20.81 % (1796223)Time elapsed: 4.394 s % 146.15/20.81 % (1796223)Peak memory usage: 91 MB % 146.15/20.81 % (1796223)Instructions burned: 15851 (million) % 146.15/20.81 % (1796357)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3423473716:avsq=on:i=17627:add=on:amm=off_2856 on theBenchmark for (2856ds/17627Mi) % 146.15/20.81 % (1796219)Instruction limit reached! % 146.15/20.81 % (1796219)------------------------------ % 146.15/20.81 % (1796219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/20.81 % (1796219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/20.81 % (1796219)CaDiCaL version: 2.1.3 % 146.15/20.81 % (1796219)Termination reason: Instruction limit % 146.15/20.81 % (1796219)Termination phase: Saturation % 146.15/20.81 % (1796219)Time elapsed: 7.316 s % 146.15/20.81 % (1796219)Peak memory usage: 76 MB % 146.15/20.81 % (1796219)Instructions burned: 11404 (million) % 146.15/20.81 % (1796604)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=593856329:s2a=on:i=53295_2843 on theBenchmark for (2843ds/53295Mi) % 146.15/20.81 % (1796221)Instruction limit reached! % 146.15/20.81 % (1796221)------------------------------ % 146.15/20.81 % (1796221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/20.81 % (1796221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/20.81 % (1796221)CaDiCaL version: 2.1.3 % 146.15/20.81 % (1796221)Termination reason: Instruction limit % 146.15/20.81 % (1796221)Termination phase: Saturation % 146.15/20.81 % (1796221)Time elapsed: 8.933 s % 146.15/20.81 % (1796221)Peak memory usage: 72 MB % 146.15/20.81 % (1796221)Instructions burned: 14135 (million) % 146.15/20.81 % (1796653)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2583260779:i=26857:ins=20_2823 on theBenchmark for (2823ds/26857Mi) % 146.15/20.81 % Exception at run slice level % 146.15/20.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 146.15/20.81 % (1796655)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3482771470:i=28120:bs=on:fsr=off_2822 on theBenchmark for (2822ds/28120Mi) % 146.15/20.81 % (1796199)Instruction limit reached! % 146.15/20.81 % (1796199)------------------------------ % 146.15/20.81 % (1796199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/20.81 % (1796199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/20.81 % (1796199)CaDiCaL version: 2.1.3 % 146.15/20.81 % (1796199)Termination reason: Instruction limit % 146.15/20.81 % (1796199)Termination phase: Saturation % 146.15/20.81 % (1796199)Time elapsed: 14.988 s % 146.15/20.81 % (1796199)Peak memory usage: 203 MB % 146.15/20.81 % (1796199)Instructions burned: 29342 (million) % 146.15/20.81 % (1796657)fmb+10_1_sil=256000:fmbss=7:random_seed=3774106295:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 146.15/20.81 % Exception at run slice level % 146.15/20.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 146.15/20.81 % (1796659)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3191462861:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 146.15/20.81 % (1796659)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 146.15/20.81 % Exception at run slice level % 146.15/20.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 146.15/20.81 % (1796215)Instruction limit reached! % 146.15/20.81 % (1796215)------------------------------ % 146.15/20.81 % (1796215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/20.81 % (1796215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/20.81 % (1796215)CaDiCaL version: 2.1.3 % 181.62/25.87 % (1796215)Termination reason: Instruction limit % 181.62/25.87 % (1796215)Termination phase: Saturation % 181.62/25.87 % (1796215)Time elapsed: 12.469 s % 181.62/25.87 % (1796215)Peak memory usage: 107 MB % 181.62/25.87 % (1796215)Instructions burned: 20140 (million) % 181.62/25.87 % (1796661)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=428527088:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 181.62/25.87 % Exception at run slice level % 181.62/25.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.62/25.87 % (1796662)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4286798550:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 181.62/25.87 % Exception at run slice level % 181.62/25.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.62/25.87 % (1796664)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4253900667:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 181.62/25.87 % Exception at run slice level % 181.62/25.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.62/25.87 % (1796666)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4280481236:rtra=on_2819 on theBenchmark for (2819ds/0Mi) % 181.62/25.87 % (1796668)% WARNING: option uhcvi not known. % 181.62/25.87 % Exception at run slice level % 181.62/25.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.62/25.87 % (1796668)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3467642847:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 181.62/25.87 % (1796671)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=961211501:i=176048:add=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/176048Mi) % 181.62/25.87 % (1796357)Instruction limit reached! % 181.62/25.87 % (1796357)------------------------------ % 181.62/25.87 % (1796357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.62/25.87 % (1796357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.62/25.87 % (1796357)CaDiCaL version: 2.1.3 % 181.62/25.87 % (1796357)Termination reason: Instruction limit % 181.62/25.87 % (1796357)Termination phase: Saturation % 181.62/25.87 % (1796357)Time elapsed: 4.871 s % 181.62/25.87 % (1796357)Peak memory usage: 93 MB % 181.62/25.87 % (1796357)Instructions burned: 17631 (million) % 181.62/25.87 % (1796673)dis+10_1_sil=32000:si=on:sp=arity:random_seed=82267932:i=206:fgj=on:rtra=on_2807 on theBenchmark for (2807ds/206Mi) % 181.62/25.87 % (1796673)Instruction limit reached! % 181.62/25.87 % (1796673)------------------------------ % 181.62/25.87 % (1796673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.62/25.87 % (1796673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.62/25.87 % (1796673)CaDiCaL version: 2.1.3 % 181.62/25.87 % (1796673)Termination reason: Instruction limit % 181.62/25.87 % (1796673)Termination phase: Saturation % 181.62/25.87 % (1796673)Time elapsed: 0.069 s % 181.62/25.87 % (1796673)Peak memory usage: 13 MB % 181.62/25.87 % (1796673)Instructions burned: 209 (million) % 181.62/25.87 % (1796675)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=447421589:i=232:rtra=on_2807 on theBenchmark for (2807ds/232Mi) % 181.62/25.87 % (1796675)Instruction limit reached! % 181.62/25.87 % (1796675)------------------------------ % 181.62/25.87 % (1796675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.62/25.87 % (1796675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.62/25.87 % (1796675)CaDiCaL version: 2.1.3 % 181.62/25.87 % (1796675)Termination reason: Instruction limit % 181.62/25.87 % (1796675)Termination phase: Saturation % 181.62/25.87 % (1796675)Time elapsed: 0.062 s % 181.62/25.87 % (1796675)Peak memory usage: 12 MB % 181.62/25.87 % (1796675)Instructions burned: 235 (million) % 181.62/25.87 % (1796677)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2700648356:i=262:rtra=on_2806 on theBenchmark for (2806ds/262Mi) % 181.62/25.87 % (1796677)Instruction limit reached! % 181.62/25.87 % (1796677)------------------------------ % 181.62/25.87 % (1796677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.62/25.87 % (1796677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.62/25.87 % (1796677)CaDiCaL version: 2.1.3 % 181.62/25.87 % (1796677)Termination reason: Instruction limit % 181.62/25.87 % (1796677)Termination phase: Saturation % 296.09/41.96 % (1796677)Time elapsed: 0.083 s % 296.09/41.96 % (1796677)Peak memory usage: 15 MB % 296.09/41.96 % (1796677)Instructions burned: 264 (million) % 296.09/41.96 % (1796679)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2983083594:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2805 on theBenchmark for (2805ds/318Mi) % 296.09/41.96 % (1796679)Instruction limit reached! % 296.09/41.96 % (1796679)------------------------------ % 296.09/41.96 % (1796679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.09/41.96 % (1796679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.09/41.96 % (1796679)CaDiCaL version: 2.1.3 % 296.09/41.96 % (1796679)Termination reason: Instruction limit % 296.09/41.96 % (1796679)Termination phase: Saturation % 296.09/41.96 % (1796679)Time elapsed: 0.080 s % 296.09/41.96 % (1796679)Peak memory usage: 14 MB % 296.09/41.96 % (1796679)Instructions burned: 321 (million) % 296.09/41.96 % (1796681)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1927553129:i=1428:nm=2:rtra=on_2804 on theBenchmark for (2804ds/1428Mi) % 296.09/41.96 % Exception at run slice level % 296.09/41.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 296.09/41.96 % (1796683)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2638461388:i=262:bd=preordered:rtra=on:fsd=on_2804 on theBenchmark for (2804ds/262Mi) % 296.09/41.96 % (1796683)Instruction limit reached! % 296.09/41.96 % (1796683)------------------------------ % 296.09/41.96 % (1796683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.09/41.96 % (1796683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.09/41.96 % (1796683)CaDiCaL version: 2.1.3 % 296.09/41.96 % (1796683)Termination reason: Instruction limit % 296.09/41.96 % (1796683)Termination phase: Saturation % 296.09/41.96 % (1796683)Time elapsed: 0.078 s % 296.09/41.96 % (1796683)Peak memory usage: 15 MB % 296.09/41.96 % (1796683)Instructions burned: 266 (million) % 296.09/41.96 % (1796685)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=1321049236:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/1368Mi) % 296.09/41.96 % (1796685)Instruction limit reached! % 296.09/41.96 % (1796685)------------------------------ % 296.09/41.96 % (1796685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.09/41.96 % (1796685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.09/41.96 % (1796685)CaDiCaL version: 2.1.3 % 296.09/41.96 % (1796685)Termination reason: Instruction limit % 296.09/41.96 % (1796685)Termination phase: Saturation % 296.09/41.96 % (1796685)Time elapsed: 0.440 s % 296.09/41.96 % (1796685)Peak memory usage: 21 MB % 296.09/41.96 % (1796685)Instructions burned: 1368 (million) % 296.09/41.96 % (1796687)ott-21_1_sil=16000:si=on:fs=off:random_seed=1805464074:i=360:av=off:fsr=off:rtra=on_2798 on theBenchmark for (2798ds/360Mi) % 296.09/41.96 % (1796687)Instruction limit reached! % 296.09/41.96 % (1796687)------------------------------ % 296.09/41.96 % (1796687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.09/41.96 % (1796687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.09/41.96 % (1796687)CaDiCaL version: 2.1.3 % 296.09/41.96 % (1796687)Termination reason: Instruction limit % 296.09/41.96 % (1796687)Termination phase: Saturation % 296.09/41.96 % (1796687)Time elapsed: 0.100 s % 296.09/41.96 % (1796687)Peak memory usage: 15 MB % 296.09/41.96 % (1796687)Instructions burned: 363 (million) % 296.09/41.96 % (1796689)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=879255531:i=954:bd=all:rtra=on_2797 on theBenchmark for (2797ds/954Mi) % 296.09/41.96 % (1796689)Instruction limit reached! % 296.09/41.96 % (1796689)------------------------------ % 296.09/41.96 % (1796689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.09/41.96 % (1796689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.09/41.96 % (1796689)CaDiCaL version: 2.1.3 % 296.09/41.96 % (1796689)Termination reason: Instruction limit % 296.09/41.96 % (1796689)Termination phase: Saturation % 296.09/41.96 % (1796689)Time elapsed: 0.332 s % 296.09/41.96 % (1796689)Peak memory usage: 17 MB % 296.09/41.96 % (1796689)Instructions burned: 955 (million) % 296.09/41.96 % (1796691)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3050088860:fmbsr=1.3:i=1730:ins=25:rtra=on_2794 on theBenchmark for (2794ds/1730Mi) % 296.09/41.96 % Exception at run slice level % 296.09/41.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796693)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2807487045:i=2358:rtra=on_2793 on theBenchmark for (2793ds/2358Mi) % 300.35/42.54 % (1796693)Instruction limit reached! % 300.35/42.54 % (1796693)------------------------------ % 300.35/42.54 % (1796693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796693)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796693)Termination reason: Instruction limit % 300.35/42.54 % (1796693)Termination phase: Saturation % 300.35/42.54 % (1796693)Time elapsed: 0.818 s % 300.35/42.54 % (1796693)Peak memory usage: 31 MB % 300.35/42.54 % (1796693)Instructions burned: 2360 (million) % 300.35/42.54 % (1796695)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3445001717:i=1778:ins=1:rtra=on_2785 on theBenchmark for (2785ds/1778Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796697)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=208368748:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2785 on theBenchmark for (2785ds/1384Mi) % 300.35/42.54 % (1796697)Instruction limit reached! % 300.35/42.54 % (1796697)------------------------------ % 300.35/42.54 % (1796697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796697)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796697)Termination reason: Instruction limit % 300.35/42.54 % (1796697)Termination phase: Saturation % 300.35/42.54 % (1796697)Time elapsed: 0.333 s % 300.35/42.54 % (1796697)Peak memory usage: 18 MB % 300.35/42.54 % (1796697)Instructions burned: 1397 (million) % 300.35/42.54 % (1796699)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2656274807:i=1758:kws=inv_precedence:fsr=off:rtra=on_2781 on theBenchmark for (2781ds/1758Mi) % 300.35/42.54 % (1796699)Instruction limit reached! % 300.35/42.54 % (1796699)------------------------------ % 300.35/42.54 % (1796699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796699)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796699)Termination reason: Instruction limit % 300.35/42.54 % (1796699)Termination phase: Saturation % 300.35/42.54 % (1796699)Time elapsed: 0.536 s % 300.35/42.54 % (1796699)Peak memory usage: 27 MB % 300.35/42.54 % (1796699)Instructions burned: 1760 (million) % 300.35/42.54 % (1796701)fmb+10_1_sil=64000:si=on:random_seed=3443667536:i=44122:nm=2:rtra=on:gsp=on_2776 on theBenchmark for (2776ds/44122Mi) % 300.35/42.54 % (1796701)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796703)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4123886925:i=19030:nm=5:rtra=on_2776 on theBenchmark for (2776ds/19030Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796705)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1001628524:fmbsr=1.7:i=1840:rtra=on_2776 on theBenchmark for (2776ds/1840Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796707)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2234468905:i=10262:rtra=on_2775 on theBenchmark for (2775ds/10262Mi) % 300.35/42.54 % (1796707)Instruction limit reached! % 300.35/42.54 % (1796707)------------------------------ % 300.35/42.54 % (1796707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796707)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796707)Termination reason: Instruction limit % 300.35/42.54 % (1796707)Termination phase: Saturation % 300.35/42.54 % (1796707)Time elapsed: 3.266 s % 300.35/42.54 % (1796707)Peak memory usage: 45 MB % 300.35/42.54 % (1796707)Instructions burned: 10262 (million) % 300.35/42.54 % (1796709)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1131400963:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2743 on theBenchmark for (2743ds/2944Mi) % 300.35/42.54 % (1796709)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.35/42.54 % (1796709)Instruction limit reached! % 300.35/42.54 % (1796709)------------------------------ % 300.35/42.54 % (1796709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796709)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796709)Termination reason: Instruction limit % 300.35/42.54 % (1796709)Termination phase: Saturation % 300.35/42.54 % (1796709)Time elapsed: 0.941 s % 300.35/42.54 % (1796709)Peak memory usage: 32 MB % 300.35/42.54 % (1796709)Instructions burned: 2945 (million) % 300.35/42.54 % (1796711)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3989528808:i=12648:rtra=on_2733 on theBenchmark for (2733ds/12648Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796713)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2181567672:fmbsr=2.30978:i=4348:rtra=on_2733 on theBenchmark for (2733ds/4348Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796715)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2742787660:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2733 on theBenchmark for (2733ds/1738Mi) % 300.35/42.54 % (1796715)Instruction limit reached! % 300.35/42.54 % (1796715)------------------------------ % 300.35/42.54 % (1796715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796715)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796715)Termination reason: Instruction limit % 300.35/42.54 % (1796715)Termination phase: Saturation % 300.35/42.54 % (1796715)Time elapsed: 0.586 s % 300.35/42.54 % (1796715)Peak memory usage: 20 MB % 300.35/42.54 % (1796715)Instructions burned: 1738 (million) % 300.35/42.54 % (1796717)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3469199769:i=10228:av=off:rtra=on_2727 on theBenchmark for (2727ds/10228Mi) % 300.35/42.54 % (1796717)Instruction limit reached! % 300.35/42.54 % (1796717)------------------------------ % 300.35/42.54 % (1796717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796717)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796717)Termination reason: Instruction limit % 300.35/42.54 % (1796717)Termination phase: Saturation % 300.35/42.54 % (1796717)Time elapsed: 3.791 s % 300.35/42.54 % (1796717)Peak memory usage: 63 MB % 300.35/42.54 % (1796717)Instructions burned: 10228 (million) % 300.35/42.54 % (1796990)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3433077280:i=108564:rtra=on_2689 on theBenchmark for (2689ds/108564Mi) % 300.35/42.54 % Exception at run slice level % 300.35/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.35/42.54 % (1796995)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3045791789:i=7024:aac=none:rtra=on_2688 on theBenchmark for (2688ds/7024Mi) % 300.35/42.54 % (1796995)Instruction limit reached! % 300.35/42.54 % (1796995)------------------------------ % 300.35/42.54 % (1796995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1796995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.54 % (1796995)CaDiCaL version: 2.1.3 % 300.35/42.54 % (1796995)Termination reason: Instruction limit % 300.35/42.54 % (1796995)Termination phase: Saturation % 300.35/42.54 % (1796995)Time elapsed: 3.317 s % 300.35/42.54 % (1796995)Peak memory usage: 36 MB % 300.35/42.54 % (1796995)Instructions burned: 7025 (million) % 300.35/42.54 % (1797073)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3478890795:i=7546:rtra=on:amm=off_2655 on theBenchmark for (2655ds/7546Mi) % 300.35/42.54 % (1797073)Instruction limit reached! % 300.35/42.54 % (1797073)------------------------------ % 300.35/42.54 % (1797073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.54 % (1797073)Linked with Z3 4.14. % 300.35/42.54 Terminated % 300.35/42.54 % Vampire exiting % 300.35/42.54 Terminated %------------------------------------------------------------------------------