%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW546_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 : n005.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:25 PM UTC 2026 % Result : Timeout 291.59s 41.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW546_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n005.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:18:17 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 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 % 8.03/1.40 % (809807)Will run a generic schedule for satisfiability detection. % 8.03/1.40 % (809813)% WARNING: option uhcvi not known. % 8.03/1.40 % (809813)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=338098033:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.03/1.40 % (809812)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1379261862_2999 on theBenchmark for (2999ds/0Mi) % 8.03/1.40 % (809814)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1730239924:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.03/1.40 % (809815)dis+10_1_sil=32000:sp=arity:random_seed=2531094740:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.03/1.40 % (809816)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3100464149:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.03/1.40 % (809817)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=739682162:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.03/1.40 % (809818)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=855659053:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.03/1.40 % Exception at run slice level % 8.03/1.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.03/1.40 % (809826)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2337101405:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.03/1.40 % Exception at run slice level % 8.03/1.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.03/1.40 % (809828)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1284337129:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.03/1.40 % (809815)Instruction limit reached! % 8.03/1.40 % (809815)------------------------------ % 8.03/1.40 % (809815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.40 % (809815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.40 % (809815)CaDiCaL version: 2.1.3 % 8.03/1.40 % (809815)Termination reason: Instruction limit % 8.03/1.40 % (809815)Termination phase: Saturation % 8.03/1.40 % (809815)Time elapsed: 0.061 s % 8.03/1.40 % (809815)Peak memory usage: 12 MB % 8.03/1.40 % (809815)Instructions burned: 104 (million) % 8.03/1.40 % (809816)Instruction limit reached! % 8.03/1.40 % (809816)------------------------------ % 8.03/1.40 % (809816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.40 % (809816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.40 % (809816)CaDiCaL version: 2.1.3 % 8.03/1.40 % (809816)Termination reason: Instruction limit % 8.03/1.40 % (809816)Termination phase: Saturation % 8.03/1.40 % (809816)Time elapsed: 0.071 s % 8.03/1.40 % (809816)Peak memory usage: 13 MB % 8.03/1.40 % (809816)Instructions burned: 117 (million) % 8.03/1.40 % (809830)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=269111824:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.03/1.40 % (809817)Instruction limit reached! % 8.03/1.40 % (809817)------------------------------ % 8.03/1.40 % (809817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.40 % (809817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.40 % (809817)CaDiCaL version: 2.1.3 % 8.03/1.40 % (809817)Termination reason: Instruction limit % 8.03/1.40 % (809817)Termination phase: Saturation % 8.03/1.40 % (809817)Time elapsed: 0.080 s % 8.03/1.40 % (809817)Peak memory usage: 13 MB % 8.03/1.40 % (809817)Instructions burned: 131 (million) % 8.03/1.40 % (809831)ott-21_1_sil=16000:fs=off:random_seed=1272576546:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.03/1.40 % (809818)Instruction limit reached! % 8.03/1.40 % (809818)------------------------------ % 8.03/1.40 % (809818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.40 % (809818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.40 % (809818)CaDiCaL version: 2.1.3 % 8.03/1.40 % (809818)Termination reason: Instruction limit % 8.03/1.40 % (809818)Termination phase: Saturation % 8.03/1.40 % (809818)Time elapsed: 0.095 s % 8.03/1.40 % (809818)Peak memory usage: 13 MB % 8.03/1.40 % (809818)Instructions burned: 160 (million) % 8.03/1.40 % (809833)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3218228058:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.85/3.40 % (809835)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3562068359:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.85/3.40 % Exception at run slice level % 21.85/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.40 % (809828)Instruction limit reached! % 21.85/3.40 % (809828)------------------------------ % 21.85/3.40 % (809828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.40 % (809828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.40 % (809828)CaDiCaL version: 2.1.3 % 21.85/3.40 % (809828)Termination reason: Instruction limit % 21.85/3.40 % (809828)Termination phase: Saturation % 21.85/3.40 % (809828)Time elapsed: 0.086 s % 21.85/3.40 % (809828)Peak memory usage: 14 MB % 21.85/3.40 % (809828)Instructions burned: 132 (million) % 21.85/3.40 % (809838)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3367294641:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.85/3.40 % (809839)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=714541781:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.85/3.40 % Exception at run slice level % 21.85/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.40 % (809842)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=2719562425:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 21.85/3.40 % (809831)Instruction limit reached! % 21.85/3.40 % (809831)------------------------------ % 21.85/3.40 % (809831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.40 % (809831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.40 % (809831)CaDiCaL version: 2.1.3 % 21.85/3.40 % (809831)Termination reason: Instruction limit % 21.85/3.40 % (809831)Termination phase: Saturation % 21.85/3.40 % (809831)Time elapsed: 0.094 s % 21.85/3.40 % (809831)Peak memory usage: 12 MB % 21.85/3.40 % (809831)Instructions burned: 186 (million) % 21.85/3.40 % (809844)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3083447689:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.85/3.40 % (809833)Instruction limit reached! % 21.85/3.40 % (809833)------------------------------ % 21.85/3.40 % (809833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.40 % (809833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.40 % (809833)CaDiCaL version: 2.1.3 % 21.85/3.40 % (809833)Termination reason: Instruction limit % 21.85/3.40 % (809833)Termination phase: Saturation % 21.85/3.40 % (809833)Time elapsed: 0.293 s % 21.85/3.40 % (809833)Peak memory usage: 14 MB % 21.85/3.40 % (809833)Instructions burned: 478 (million) % 21.85/3.40 % (809846)fmb+10_1_sil=64000:random_seed=2492340037:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.85/3.40 % (809830)Instruction limit reached! % 21.85/3.40 % (809830)------------------------------ % 21.85/3.40 % (809830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.40 % (809830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.40 % (809830)CaDiCaL version: 2.1.3 % 21.85/3.40 % (809830)Termination reason: Instruction limit % 21.85/3.40 % (809830)Termination phase: Saturation % 21.85/3.40 % (809830)Time elapsed: 0.334 s % 21.85/3.40 % (809830)Peak memory usage: 14 MB % 21.85/3.40 % (809830)Instructions burned: 685 (million) % 21.85/3.40 % (809846)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.85/3.40 % Exception at run slice level % 21.85/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.40 % (809848)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=117774287:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.85/3.40 % (809849)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3963209520:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 21.85/3.40 % Exception at run slice level % 21.85/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.40 % Exception at run slice level % 21.85/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.23/15.01 % (809852)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1785277429:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 104.23/15.01 % (809853)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2235922268:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 104.23/15.01 % (809853)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 104.23/15.01 % (809842)Instruction limit reached! % 104.23/15.01 % (809842)------------------------------ % 104.23/15.01 % (809842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.23/15.01 % (809842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.23/15.01 % (809842)CaDiCaL version: 2.1.3 % 104.23/15.01 % (809842)Termination reason: Instruction limit % 104.23/15.01 % (809842)Termination phase: Saturation % 104.23/15.01 % (809842)Time elapsed: 0.354 s % 104.23/15.01 % (809842)Peak memory usage: 17 MB % 104.23/15.01 % (809842)Instructions burned: 692 (million) % 104.23/15.01 % (809856)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2638712542:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 104.23/15.01 % Exception at run slice level % 104.23/15.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.23/15.01 % (809858)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3042547964:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 104.23/15.01 % Exception at run slice level % 104.23/15.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.23/15.01 % (809860)ott-2_1_sil=16000:newcnf=on:random_seed=4110539313:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 104.23/15.01 % (809844)Instruction limit reached! % 104.23/15.01 % (809844)------------------------------ % 104.23/15.01 % (809844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.23/15.01 % (809844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.23/15.01 % (809844)CaDiCaL version: 2.1.3 % 104.23/15.01 % (809844)Termination reason: Instruction limit % 104.23/15.01 % (809844)Termination phase: Saturation % 104.23/15.01 % (809844)Time elapsed: 0.513 s % 104.23/15.01 % (809844)Peak memory usage: 19 MB % 104.23/15.01 % (809844)Instructions burned: 879 (million) % 104.23/15.01 % (809862)ott+10_1_sil=32000:tgt=ground:random_seed=3731783071:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 104.23/15.01 % (809838)Instruction limit reached! % 104.23/15.01 % (809838)------------------------------ % 104.23/15.01 % (809838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.23/15.01 % (809838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.23/15.01 % (809838)CaDiCaL version: 2.1.3 % 104.23/15.01 % (809838)Termination reason: Instruction limit % 104.23/15.01 % (809838)Termination phase: Saturation % 104.23/15.01 % (809838)Time elapsed: 0.682 s % 104.23/15.01 % (809838)Peak memory usage: 19 MB % 104.23/15.01 % (809838)Instructions burned: 1181 (million) % 104.23/15.01 % (809864)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4083589288:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 104.23/15.01 % Exception at run slice level % 104.23/15.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 104.23/15.01 % (809866)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=345654148:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 104.23/15.01 % (809860)Instruction limit reached! % 104.23/15.01 % (809860)------------------------------ % 104.23/15.01 % (809860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.23/15.01 % (809860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.23/15.01 % (809860)CaDiCaL version: 2.1.3 % 104.23/15.01 % (809860)Termination reason: Instruction limit % 104.23/15.01 % (809860)Termination phase: Saturation % 104.23/15.01 % (809860)Time elapsed: 0.473 s % 104.23/15.01 % (809860)Peak memory usage: 17 MB % 104.23/15.01 % (809860)Instructions burned: 869 (million) % 104.23/15.01 % (809868)dis+21_1_sil=32000:sas=cadical:random_seed=1734777237:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 104.23/15.01 % (809853)Instruction limit reached! % 104.23/15.01 % (809853)------------------------------ % 104.23/15.01 % (809853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.23/15.01 % (809853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.23/15.01 % (809853)CaDiCaL version: 2.1.3 % 126.46/18.06 % (809853)Termination reason: Instruction limit % 126.46/18.06 % (809853)Termination phase: Saturation % 126.46/18.06 % (809853)Time elapsed: 0.695 s % 126.46/18.06 % (809853)Peak memory usage: 18 MB % 126.46/18.06 % (809853)Instructions burned: 1472 (million) % 126.46/18.06 % (809870)ott+11_1_sil=16000:gs=on:random_seed=606073787:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 126.46/18.06 % (809870)Instruction limit reached! % 126.46/18.06 % (809870)------------------------------ % 126.46/18.06 % (809870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.46/18.06 % (809870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.46/18.06 % (809870)CaDiCaL version: 2.1.3 % 126.46/18.06 % (809870)Termination reason: Instruction limit % 126.46/18.06 % (809870)Termination phase: Saturation % 126.46/18.06 % (809870)Time elapsed: 1.210 s % 126.46/18.06 % (809870)Peak memory usage: 26 MB % 126.46/18.06 % (809870)Instructions burned: 2251 (million) % 126.46/18.06 % (809872)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3504015772:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 126.46/18.06 % Exception at run slice level % 126.46/18.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.46/18.06 % (809874)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3395422117:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 126.46/18.06 % (809866)Instruction limit reached! % 126.46/18.06 % (809866)------------------------------ % 126.46/18.06 % (809866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.46/18.06 % (809866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.46/18.06 % (809866)CaDiCaL version: 2.1.3 % 126.46/18.06 % (809866)Termination reason: Instruction limit % 126.46/18.06 % (809866)Termination phase: Saturation % 126.46/18.06 % (809866)Time elapsed: 1.826 s % 126.46/18.06 % (809866)Peak memory usage: 21 MB % 126.46/18.06 % (809866)Instructions burned: 3512 (million) % 126.46/18.06 % (809876)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3988418597:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 126.46/18.06 % (809868)Instruction limit reached! % 126.46/18.06 % (809868)------------------------------ % 126.46/18.06 % (809868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.46/18.06 % (809868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.46/18.06 % (809868)CaDiCaL version: 2.1.3 % 126.46/18.06 % (809868)Termination reason: Instruction limit % 126.46/18.06 % (809868)Termination phase: Saturation % 126.46/18.06 % (809868)Time elapsed: 1.960 s % 126.46/18.06 % (809868)Peak memory usage: 24 MB % 126.46/18.06 % (809868)Instructions burned: 3774 (million) % 126.46/18.06 % (809852)Instruction limit reached! % 126.46/18.06 % (809852)------------------------------ % 126.46/18.06 % (809852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.46/18.06 % (809852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.46/18.06 % (809852)CaDiCaL version: 2.1.3 % 126.46/18.06 % (809852)Termination reason: Instruction limit % 126.46/18.06 % (809852)Termination phase: Saturation % 126.46/18.06 % (809852)Time elapsed: 2.601 s % 126.46/18.06 % (809852)Peak memory usage: 25 MB % 126.46/18.06 % (809852)Instructions burned: 5132 (million) % 126.46/18.06 % (809878)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=681924337:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 126.46/18.06 % (809879)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=570226111:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 126.46/18.06 % Exception at run slice level % 126.46/18.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.46/18.06 % (809882)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1944214386:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 126.46/18.06 % Exception at run slice level % 126.46/18.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.46/18.06 % (809884)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3321692038:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 126.46/18.06 % Exception at run slice level % 126.46/18.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 126.46/18.06 % (809886)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=473143652:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 184.98/26.35 % (809862)Instruction limit reached! % 184.98/26.35 % (809862)------------------------------ % 184.98/26.35 % (809862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809862)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809862)Termination reason: Instruction limit % 184.98/26.35 % (809862)Termination phase: Saturation % 184.98/26.35 % (809862)Time elapsed: 2.849 s % 184.98/26.35 % (809862)Peak memory usage: 30 MB % 184.98/26.35 % (809862)Instructions burned: 5116 (million) % 184.98/26.35 % (809888)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=544331703:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 184.98/26.35 % (809874)Instruction limit reached! % 184.98/26.35 % (809874)------------------------------ % 184.98/26.35 % (809874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809874)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809874)Termination reason: Instruction limit % 184.98/26.35 % (809874)Termination phase: Saturation % 184.98/26.35 % (809874)Time elapsed: 2.237 s % 184.98/26.35 % (809874)Peak memory usage: 31 MB % 184.98/26.35 % (809874)Instructions burned: 4593 (million) % 184.98/26.35 % (809890)dis+10_16:1_sil=16000:random_seed=1903404617:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi) % 184.98/26.35 % (809878)Instruction limit reached! % 184.98/26.35 % (809878)------------------------------ % 184.98/26.35 % (809878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809878)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809878)Termination reason: Instruction limit % 184.98/26.35 % (809878)Termination phase: Saturation % 184.98/26.35 % (809878)Time elapsed: 2.748 s % 184.98/26.35 % (809878)Peak memory usage: 39 MB % 184.98/26.35 % (809878)Instructions burned: 5211 (million) % 184.98/26.35 % (809892)ott-3_8_sil=64000:random_seed=2340079509:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi) % 184.98/26.35 % (809888)Instruction limit reached! % 184.98/26.35 % (809888)------------------------------ % 184.98/26.35 % (809888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809888)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809888)Termination reason: Instruction limit % 184.98/26.35 % (809888)Termination phase: Saturation % 184.98/26.35 % (809888)Time elapsed: 4.431 s % 184.98/26.35 % (809888)Peak memory usage: 26 MB % 184.98/26.35 % (809888)Instructions burned: 8174 (million) % 184.98/26.35 % (809894)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1107560128:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi) % 184.98/26.35 % Exception at run slice level % 184.98/26.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 184.98/26.35 % (809896)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3719004753:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 184.98/26.35 % (809890)Instruction limit reached! % 184.98/26.35 % (809890)------------------------------ % 184.98/26.35 % (809890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809890)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809890)Termination reason: Instruction limit % 184.98/26.35 % (809890)Termination phase: Saturation % 184.98/26.35 % (809890)Time elapsed: 4.772 s % 184.98/26.35 % (809890)Peak memory usage: 65 MB % 184.98/26.35 % (809890)Instructions burned: 9156 (million) % 184.98/26.35 % (809898)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1005064273:i=14134_2904 on theBenchmark for (2904ds/14134Mi) % 184.98/26.35 % (809896)Instruction limit reached! % 184.98/26.35 % (809896)------------------------------ % 184.98/26.35 % (809896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.98/26.35 % (809896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.98/26.35 % (809896)CaDiCaL version: 2.1.3 % 184.98/26.35 % (809896)Termination reason: Instruction limit % 184.98/26.35 % (809896)Termination phase: Saturation % 184.98/26.35 % (809896)Time elapsed: 6.644 s % 184.98/26.35 % (809896)Peak memory usage: 50 MB % 184.98/26.35 % (809896)Instructions burned: 11405 (million) % 184.98/26.35 % (809900)dis+33_16_sil=32000:sac=on:random_seed=843775850:i=15851:nm=0_2852 on theBenchmark for (2852ds/15851Mi) % 198.17/28.14 % (809892)Instruction limit reached! % 198.17/28.14 % (809892)------------------------------ % 198.17/28.14 % (809892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.17/28.14 % (809892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.17/28.14 % (809892)CaDiCaL version: 2.1.3 % 198.17/28.14 % (809892)Termination reason: Instruction limit % 198.17/28.14 % (809892)Termination phase: Saturation % 198.17/28.14 % (809892)Time elapsed: 10.489 s % 198.17/28.14 % (809892)Peak memory usage: 37 MB % 198.17/28.14 % (809892)Instructions burned: 20141 (million) % 198.17/28.14 % (809902)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1465853286:avsq=on:i=17627:add=on:amm=off_2836 on theBenchmark for (2836ds/17627Mi) % 198.17/28.14 % (809876)Instruction limit reached! % 198.17/28.14 % (809876)------------------------------ % 198.17/28.14 % (809876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.17/28.14 % (809876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.17/28.14 % (809876)CaDiCaL version: 2.1.3 % 198.17/28.14 % (809876)Termination reason: Instruction limit % 198.17/28.14 % (809876)Termination phase: Saturation % 198.17/28.14 % (809876)Time elapsed: 14.090 s % 198.17/28.14 % (809876)Peak memory usage: 361 MB % 198.17/28.14 % (809876)Instructions burned: 29342 (million) % 198.17/28.14 % (809904)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3677139261:s2a=on:i=53295_2831 on theBenchmark for (2831ds/53295Mi) % 198.17/28.14 % (809898)Instruction limit reached! % 198.17/28.14 % (809898)------------------------------ % 198.17/28.14 % (809898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.17/28.14 % (809898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.17/28.14 % (809898)CaDiCaL version: 2.1.3 % 198.17/28.14 % (809898)Termination reason: Instruction limit % 198.17/28.14 % (809898)Termination phase: Saturation % 198.17/28.14 % (809898)Time elapsed: 7.631 s % 198.17/28.14 % (809898)Peak memory usage: 39 MB % 198.17/28.14 % (809898)Instructions burned: 14135 (million) % 198.17/28.14 % (809906)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=511070823:i=26857:ins=20_2828 on theBenchmark for (2828ds/26857Mi) % 198.17/28.14 % Exception at run slice level % 198.17/28.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.17/28.14 % (809908)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2300931646:i=28120:bs=on:fsr=off_2828 on theBenchmark for (2828ds/28120Mi) % 198.17/28.14 % (809886)Instruction limit reached! % 198.17/28.14 % (809886)------------------------------ % 198.17/28.14 % (809886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.17/28.14 % (809886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.17/28.14 % (809886)CaDiCaL version: 2.1.3 % 198.17/28.14 % (809886)Termination reason: Instruction limit % 198.17/28.14 % (809886)Termination phase: Saturation % 198.17/28.14 % (809886)Time elapsed: 14.545 s % 198.17/28.14 % (809886)Peak memory usage: 73 MB % 198.17/28.14 % (809886)Instructions burned: 22566 (million) % 198.17/28.14 % (809910)fmb+10_1_sil=256000:fmbss=7:random_seed=1170018352:fmbsr=1.6:i=182295_2822 on theBenchmark for (2822ds/182295Mi) % 198.17/28.14 % Exception at run slice level % 198.17/28.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.17/28.14 % (809912)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3043588958:i=44625:gsp=on_2822 on theBenchmark for (2822ds/44625Mi) % 198.17/28.14 % (809912)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 198.17/28.14 % Exception at run slice level % 198.17/28.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.17/28.14 % (809914)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1465844007:i=160505_2822 on theBenchmark for (2822ds/160505Mi) % 198.17/28.14 % Exception at run slice level % 198.17/28.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.17/28.14 % (809916)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1931084065:fmbsr=1.3:i=225729_2821 on theBenchmark for (2821ds/225729Mi) % 198.17/28.14 % Exception at run slice level % 198.17/28.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.17/28.14 % (809918)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4207029355:fmbsr=2:i=185024:ins=7_2821 on theBenchmark for (2821ds/185024Mi) % 222.75/31.61 % Exception at run slice level % 222.75/31.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 222.75/31.61 % (809920)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3438045747:rtra=on_2821 on theBenchmark for (2821ds/0Mi) % 222.75/31.61 % Exception at run slice level % 222.75/31.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 222.75/31.61 % (809922)% WARNING: option uhcvi not known. % 222.75/31.61 % (809922)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=127333710:i=271062:add=off:rtra=on:rawr=on_2821 on theBenchmark for (2821ds/271062Mi) % 222.75/31.61 % (809900)Instruction limit reached! % 222.75/31.61 % (809900)------------------------------ % 222.75/31.61 % (809900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.75/31.61 % (809900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.75/31.61 % (809900)CaDiCaL version: 2.1.3 % 222.75/31.61 % (809900)Termination reason: Instruction limit % 222.75/31.61 % (809900)Termination phase: Saturation % 222.75/31.61 % (809900)Time elapsed: 8.072 s % 222.75/31.61 % (809900)Peak memory usage: 312 MB % 222.75/31.61 % (809900)Instructions burned: 15851 (million) % 222.75/31.61 % (809924)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1703945624:i=176048:add=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/176048Mi) % 222.75/31.61 % (809902)Instruction limit reached! % 222.75/31.61 % (809902)------------------------------ % 222.75/31.61 % (809902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.75/31.61 % (809902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.75/31.61 % (809902)CaDiCaL version: 2.1.3 % 222.75/31.61 % (809902)Termination reason: Instruction limit % 222.75/31.61 % (809902)Termination phase: Saturation % 222.75/31.61 % (809902)Time elapsed: 9.027 s % 222.75/31.61 % (809902)Peak memory usage: 132 MB % 222.75/31.61 % (809902)Instructions burned: 17627 (million) % 222.75/31.61 % (809926)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3236966284:i=206:fgj=on:rtra=on_2745 on theBenchmark for (2745ds/206Mi) % 222.75/31.61 % (809926)Instruction limit reached! % 222.75/31.61 % (809926)------------------------------ % 222.75/31.61 % (809926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.75/31.61 % (809926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.75/31.61 % (809926)CaDiCaL version: 2.1.3 % 222.75/31.61 % (809926)Termination reason: Instruction limit % 222.75/31.61 % (809926)Termination phase: Saturation % 222.75/31.61 % (809926)Time elapsed: 0.130 s % 222.75/31.61 % (809926)Peak memory usage: 13 MB % 222.75/31.61 % (809926)Instructions burned: 206 (million) % 222.75/31.61 % (809928)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2819222454:i=232:rtra=on_2744 on theBenchmark for (2744ds/232Mi) % 222.75/31.61 % (809928)Instruction limit reached! % 222.75/31.61 % (809928)------------------------------ % 222.75/31.61 % (809928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.75/31.61 % (809928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.75/31.61 % (809928)CaDiCaL version: 2.1.3 % 222.75/31.61 % (809928)Termination reason: Instruction limit % 222.75/31.61 % (809928)Termination phase: Saturation % 222.75/31.61 % (809928)Time elapsed: 0.143 s % 222.75/31.61 % (809928)Peak memory usage: 14 MB % 222.75/31.61 % (809928)Instructions burned: 233 (million) % 222.75/31.61 % (809930)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1884290613:i=262:rtra=on_2742 on theBenchmark for (2742ds/262Mi) % 222.75/31.61 % (809930)Instruction limit reached! % 222.75/31.61 % (809930)------------------------------ % 222.75/31.61 % (809930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.75/31.61 % (809930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.75/31.61 % (809930)CaDiCaL version: 2.1.3 % 222.75/31.61 % (809930)Termination reason: Instruction limit % 222.75/31.61 % (809930)Termination phase: Saturation % 222.75/31.61 % (809930)Time elapsed: 0.156 s % 222.75/31.61 % (809930)Peak memory usage: 14 MB % 222.75/31.61 % (809930)Instructions burned: 262 (million) % 222.75/31.61 % (809932)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1889375622:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2740 on theBenchmark for (2740ds/318Mi) % 222.75/31.61 % (809932)Instruction limit reached! % 222.75/31.61 % (809932)------------------------------ % 222.75/31.61 % (809932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.63/37.54 % (809932)CaDiCaL version: 2.1.3 % 264.63/37.54 % (809932)Termination reason: Instruction limit % 264.63/37.54 % (809932)Termination phase: Saturation % 264.63/37.54 % (809932)Time elapsed: 0.192 s % 264.63/37.54 % (809932)Peak memory usage: 13 MB % 264.63/37.54 % (809932)Instructions burned: 318 (million) % 264.63/37.54 % (809934)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1977981493:i=1428:nm=2:rtra=on_2738 on theBenchmark for (2738ds/1428Mi) % 264.63/37.54 % Exception at run slice level % 264.63/37.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.63/37.54 % (809936)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1537033387:i=262:bd=preordered:rtra=on:fsd=on_2738 on theBenchmark for (2738ds/262Mi) % 264.63/37.54 % (809936)Instruction limit reached! % 264.63/37.54 % (809936)------------------------------ % 264.63/37.54 % (809936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.63/37.54 % (809936)CaDiCaL version: 2.1.3 % 264.63/37.54 % (809936)Termination reason: Instruction limit % 264.63/37.54 % (809936)Termination phase: Saturation % 264.63/37.54 % (809936)Time elapsed: 0.168 s % 264.63/37.54 % (809936)Peak memory usage: 15 MB % 264.63/37.54 % (809936)Instructions burned: 262 (million) % 264.63/37.54 % (809938)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=2582326363:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/1368Mi) % 264.63/37.54 % (809938)Instruction limit reached! % 264.63/37.54 % (809938)------------------------------ % 264.63/37.54 % (809938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.63/37.54 % (809938)CaDiCaL version: 2.1.3 % 264.63/37.54 % (809938)Termination reason: Instruction limit % 264.63/37.54 % (809938)Termination phase: Saturation % 264.63/37.54 % (809938)Time elapsed: 0.713 s % 264.63/37.54 % (809938)Peak memory usage: 16 MB % 264.63/37.54 % (809938)Instructions burned: 1369 (million) % 264.63/37.54 % (809940)ott-21_1_sil=16000:si=on:fs=off:random_seed=685611382:i=360:av=off:fsr=off:rtra=on_2729 on theBenchmark for (2729ds/360Mi) % 264.63/37.54 % (809940)Instruction limit reached! % 264.63/37.54 % (809940)------------------------------ % 264.63/37.54 % (809940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.63/37.54 % (809940)CaDiCaL version: 2.1.3 % 264.63/37.54 % (809940)Termination reason: Instruction limit % 264.63/37.54 % (809940)Termination phase: Saturation % 264.63/37.54 % (809940)Time elapsed: 0.187 s % 264.63/37.54 % (809940)Peak memory usage: 14 MB % 264.63/37.54 % (809940)Instructions burned: 360 (million) % 264.63/37.54 % (809942)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=648056513:i=954:bd=all:rtra=on_2727 on theBenchmark for (2727ds/954Mi) % 264.63/37.54 % (809908)Instruction limit reached! % 264.63/37.54 % (809908)------------------------------ % 264.63/37.54 % (809908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.63/37.54 % (809908)CaDiCaL version: 2.1.3 % 264.63/37.54 % (809908)Termination reason: Instruction limit % 264.63/37.54 % (809908)Termination phase: Saturation % 264.63/37.54 % (809908)Time elapsed: 10.135 s % 264.63/37.54 % (809908)Peak memory usage: 24 MB % 264.63/37.54 % (809908)Instructions burned: 28123 (million) % 264.63/37.54 % (809944)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=86951699:fmbsr=1.3:i=1730:ins=25:rtra=on_2726 on theBenchmark for (2726ds/1730Mi) % 264.63/37.54 % Exception at run slice level % 264.63/37.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 264.63/37.54 % (809946)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3124761503:i=2358:rtra=on_2726 on theBenchmark for (2726ds/2358Mi) % 264.63/37.54 % (809942)Instruction limit reached! % 264.63/37.54 % (809942)------------------------------ % 264.63/37.54 % (809942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.63/37.54 % (809942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.59/41.31 % (809942)CaDiCaL version: 2.1.3 % 291.59/41.31 % (809942)Termination reason: Instruction limit % 291.59/41.31 % (809942)Termination phase: Saturation % 291.59/41.31 % (809942)Time elapsed: 0.616 s % 291.59/41.31 % (809942)Peak memory usage: 16 MB % 291.59/41.31 % (809942)Instructions burned: 955 (million) % 291.59/41.31 % (809948)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2802710218:i=1778:ins=1:rtra=on_2720 on theBenchmark for (2720ds/1778Mi) % 291.59/41.31 % Exception at run slice level % 291.59/41.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.59/41.31 % (809950)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=1318163077:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2720 on theBenchmark for (2720ds/1384Mi) % 291.59/41.31 % (809950)Instruction limit reached! % 291.59/41.31 % (809950)------------------------------ % 291.59/41.31 % (809950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.59/41.31 % (809950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.59/41.31 % (809950)CaDiCaL version: 2.1.3 % 291.59/41.31 % (809950)Termination reason: Instruction limit % 291.59/41.31 % (809950)Termination phase: Saturation % 291.59/41.31 % (809950)Time elapsed: 0.794 s % 291.59/41.31 % (809950)Peak memory usage: 37 MB % 291.59/41.31 % (809950)Instructions burned: 1384 (million) % 291.59/41.31 % (809952)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2406110743:i=1758:kws=inv_precedence:fsr=off:rtra=on_2712 on theBenchmark for (2712ds/1758Mi) % 291.59/41.31 % (809946)Instruction limit reached! % 291.59/41.31 % (809946)------------------------------ % 291.59/41.31 % (809946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.59/41.31 % (809946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.59/41.31 % (809946)CaDiCaL version: 2.1.3 % 291.59/41.31 % (809946)Termination reason: Instruction limit % 291.59/41.31 % (809946)Termination phase: Saturation % 291.59/41.31 % (809946)Time elapsed: 1.418 s % 291.59/41.31 % (809946)Peak memory usage: 24 MB % 291.59/41.31 % (809946)Instructions burned: 2358 (million) % 291.59/41.31 % (809954)fmb+10_1_sil=64000:si=on:random_seed=3359922002:i=44122:nm=2:rtra=on:gsp=on_2711 on theBenchmark for (2711ds/44122Mi) % 291.59/41.31 % (809954)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.59/41.31 % Exception at run slice level % 291.59/41.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.59/41.31 % (809956)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1739238063:i=19030:nm=5:rtra=on_2711 on theBenchmark for (2711ds/19030Mi) % 291.59/41.31 % Exception at run slice level % 291.59/41.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.59/41.31 % (809958)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=70991162:fmbsr=1.7:i=1840:rtra=on_2711 on theBenchmark for (2711ds/1840Mi) % 291.59/41.31 % Exception at run slice level % 291.59/41.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 291.59/41.31 % (809960)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1619858314:i=10262:rtra=on_2711 on theBenchmark for (2711ds/10262Mi) % 291.59/41.31 % (809952)Instruction limit reached! % 291.59/41.31 % (809952)------------------------------ % 291.59/41.31 % (809952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.59/41.31 % (809952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.59/41.31 % (809952)CaDiCaL version: 2.1.3 % 291.59/41.31 % (809952)Termination reason: Instruction limit % 291.59/41.31 % (809952)Termination phase: Saturation % 291.59/41.31 % (809952)Time elapsed: 1.021 s % 291.59/41.31 % (809952)Peak memory usage: 25 MB % 291.59/41.31 % (809952)Instructions burned: 1760 (million) % 291.59/41.31 % (810114)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2124953577:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2701 on theBenchmark for (2701ds/2944Mi) % 291.59/41.31 % (810114)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.59/41.31 % (810114)Instruction limit reached! % 291.59/41.31 % (810114)------------------------------ % 291.59/41.31 % (810114)Version: Vampire 5.0.1 (Release build, commit 5ef7c26Terminated % 300.13/42.54 % Vampire exiting %------------------------------------------------------------------------------