%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LCL930^1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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 : Wed Sep 30 08:15:15 AM UTC 2026 % Result : Satisfiable 1.35s 0.37s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL930^1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Tue Sep 29 10:33:34 UTC 2026 % 0.09/0.11 % CPUTime : % 0.09/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.13 Running first-order model finding % 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.35/0.37 % (4118167)Will run a generic schedule for satisfiability detection. % 1.35/0.37 % (4118172)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3234077737_2999 on theBenchmark for (2999ds/0Mi) % 1.35/0.37 % (4118174)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1390324228:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.35/0.37 % (4118175)dis+10_1_sil=32000:sp=arity:random_seed=4289090242:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.35/0.37 % (4118176)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=227460815:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.35/0.37 % (4118176)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.35/0.37 % Detected minimum model sizes of [1] % 1.35/0.37 % Detected maximum model sizes of [2] % 1.35/0.37 % TRYING [1] % 1.35/0.37 % TRYING [2] % 1.35/0.37 % Finite Model Found! % 1.35/0.37 % SZS status Satisfiable for theBenchmark % 1.35/0.37 % (4118172)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.35/0.37 % (4118172)------------------------------ % 1.35/0.37 % (4118172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.35/0.37 % (4118172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.35/0.37 % (4118172)CaDiCaL version: 2.1.3 % 1.35/0.37 % (4118172)Termination reason: Unknown % 1.35/0.37 % (4118172)Termination phase: Finite model building constraint generation % 1.35/0.37 % (4118172)Time elapsed: 0.001 s % 1.35/0.37 % (4118172)Peak memory usage: 11 MB % 1.35/0.37 % (4118172)Instructions burned: 2 (million) % 1.35/0.37 % (4118177)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2220032719:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.35/0.37 % (4118173)% WARNING: option uhcvi not known. % 1.35/0.37 % (4118178)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=989440139:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.35/0.37 % (4118173)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=719879400:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.35/0.37 % (4118173)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.35/0.37 % (4118173)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 1.35/0.37 % (4118184)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=944674590:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.35/0.37 % Detected minimum model sizes of [1] % 1.35/0.37 % Detected maximum model sizes of [3] % 1.35/0.37 % TRYING [1] % 1.35/0.37 % TRYING [2] % 1.35/0.37 % Finite Model Found! % 1.35/0.37 % SZS status Satisfiable for theBenchmark % 1.35/0.37 % (4118184)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.35/0.37 % (4118184)------------------------------ % 1.35/0.37 % (4118184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.35/0.37 % (4118184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.35/0.37 % (4118184)CaDiCaL version: 2.1.3 % 1.35/0.37 % (4118184)Termination reason: Unknown % 1.35/0.37 % (4118184)Termination phase: Finite model building constraint generation % 1.35/0.37 % (4118184)Time elapsed: 0.001 s % 1.35/0.37 % (4118184)Peak memory usage: 11 MB % 1.35/0.37 % (4118184)Instructions burned: 3 (million) % 1.35/0.37 % (4118176)Instruction limit reached! % 1.35/0.37 % (4118176)------------------------------ % 1.35/0.37 % (4118176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.35/0.37 % (4118176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.35/0.37 % (4118176)CaDiCaL version: 2.1.3 % 1.35/0.37 % (4118176)Termination reason: Instruction limit % 1.35/0.37 % (4118176)Termination phase: Saturation % 1.35/0.37 % (4118176)Time elapsed: 0.024 s % 1.35/0.37 % (4118176)Peak memory usage: 11 MB % 1.35/0.37 % (4118176)Instructions burned: 117 (million) % 1.35/0.37 % (4118175)Instruction limit reached! % 1.35/0.37 % (4118175)------------------------------ % 1.35/0.37 % (4118175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.35/0.37 % (4118175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.35/0.37 % (4118175)CaDiCaL version: 2.1.3 % 1.35/0.37 % (4118175)Termination reason: Instruction limit % 1.35/0.37 % (4118175)Termination phase: Saturation % 1.35/0.37 % (4118175)Time elapsed: 0.028 s % 1.35/0.37 % (4118175)Peak memory usage: 11 MB % 1.35/0.37 % (4118175)Instructions burned: 107 (million) % 2.03/0.50 % (4118188)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1934735243:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.03/0.50 % (4118177)Instruction limit reached! % 2.03/0.50 % (4118177)------------------------------ % 2.03/0.50 % (4118177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.50 % (4118177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.50 % (4118177)CaDiCaL version: 2.1.3 % 2.03/0.50 % (4118177)Termination reason: Instruction limit % 2.03/0.50 % (4118177)Termination phase: Saturation % 2.03/0.50 % (4118177)Time elapsed: 0.032 s % 2.03/0.50 % (4118177)Peak memory usage: 12 MB % 2.03/0.50 % (4118177)Instructions burned: 134 (million) % 2.03/0.50 % (4118189)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=1028461535:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.03/0.50 % (4118189)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 2.03/0.50 % (4118189)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 2.03/0.50 % (4118190)ott-21_1_sil=16000:fs=off:random_seed=1833464765:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 2.03/0.50 % (4118192)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2414416863:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 2.03/0.50 % (4118178)Instruction limit reached! % 2.03/0.50 % (4118178)------------------------------ % 2.03/0.50 % (4118178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.50 % (4118178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.50 % (4118178)CaDiCaL version: 2.1.3 % 2.03/0.50 % (4118178)Termination reason: Instruction limit % 2.03/0.50 % (4118178)Termination phase: Saturation % 2.03/0.50 % (4118178)Time elapsed: 0.036 s % 2.03/0.50 % (4118178)Peak memory usage: 11 MB % 2.03/0.50 % (4118178)Instructions burned: 161 (million) % 2.03/0.50 % (4118196)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2984399122:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 2.03/0.50 % Detected minimum model sizes of [1] % 2.03/0.51 % Detected maximum model sizes of [2] % 2.03/0.51 % TRYING [1] % 2.03/0.51 % TRYING [2] % 2.03/0.51 % Finite Model Found! % 2.03/0.51 % SZS status Satisfiable for theBenchmark % 2.03/0.51 % (4118196)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.03/0.51 % (4118196)------------------------------ % 2.03/0.51 % (4118196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.51 % (4118196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.51 % (4118196)CaDiCaL version: 2.1.3 % 2.03/0.51 % (4118196)Termination reason: Unknown % 2.03/0.51 % (4118196)Termination phase: Finite model building constraint generation % 2.03/0.51 % (4118196)Time elapsed: 0.001 s % 2.03/0.51 % (4118196)Peak memory usage: 10 MB % 2.03/0.51 % (4118196)Instructions burned: 2 (million) % 2.03/0.51 % (4118188)Instruction limit reached! % 2.03/0.51 % (4118188)------------------------------ % 2.03/0.51 % (4118188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.51 % (4118188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.51 % (4118188)CaDiCaL version: 2.1.3 % 2.03/0.51 % (4118188)Termination reason: Instruction limit % 2.03/0.51 % (4118188)Termination phase: Saturation % 2.03/0.51 % (4118188)Time elapsed: 0.031 s % 2.03/0.51 % (4118188)Peak memory usage: 12 MB % 2.03/0.51 % (4118188)Instructions burned: 135 (million) % 2.03/0.51 % (4118198)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2647467519:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 2.03/0.51 % (4118199)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2049736865:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 2.03/0.51 % Exception at run slice level % 2.03/0.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 2.03/0.51 % (4118190)Instruction limit reached! % 2.03/0.51 % (4118190)------------------------------ % 2.03/0.51 % (4118190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.51 % (4118190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.51 % (4118190)CaDiCaL version: 2.1.3 % 2.03/0.51 % (4118190)Termination reason: Instruction limit % 2.03/0.51 % (4118190)Termination phase: Saturation % 8.09/1.32 % (4118190)Time elapsed: 0.041 s % 8.09/1.32 % (4118190)Peak memory usage: 13 MB % 8.09/1.32 % (4118190)Instructions burned: 183 (million) % 8.09/1.32 % (4118202)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=3134288541: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) % 8.09/1.32 % (4118202)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.09/1.32 % (4118203)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=869067862:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 8.09/1.32 % (4118203)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.09/1.32 % (4118192)Instruction limit reached! % 8.09/1.32 % (4118192)------------------------------ % 8.09/1.32 % (4118192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.32 % (4118192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.32 % (4118192)CaDiCaL version: 2.1.3 % 8.09/1.32 % (4118192)Termination reason: Instruction limit % 8.09/1.32 % (4118192)Termination phase: Saturation % 8.09/1.32 % (4118192)Time elapsed: 0.116 s % 8.09/1.32 % (4118192)Peak memory usage: 12 MB % 8.09/1.32 % (4118192)Instructions burned: 488 (million) % 8.09/1.32 % (4118206)fmb+10_1_sil=64000:random_seed=932160988:i=22061:nm=2:gsp=on_2998 on theBenchmark for (2998ds/22061Mi) % 8.09/1.32 % (4118206)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 8.09/1.32 % Detected minimum model sizes of [1] % 8.09/1.32 % Detected maximum model sizes of [2] % 8.09/1.32 % TRYING [1] % 8.09/1.32 % TRYING [2] % 8.09/1.32 % Finite Model Found! % 8.09/1.32 % SZS status Satisfiable for theBenchmark % 8.09/1.32 % (4118206)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.09/1.32 % (4118206)------------------------------ % 8.09/1.32 % (4118206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.32 % (4118206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.32 % (4118206)CaDiCaL version: 2.1.3 % 8.09/1.32 % (4118206)Termination reason: Unknown % 8.09/1.32 % (4118206)Termination phase: Finite model building constraint generation % 8.09/1.32 % (4118206)Time elapsed: 0.001 s % 8.09/1.32 % (4118206)Peak memory usage: 10 MB % 8.09/1.32 % (4118206)Instructions burned: 2 (million) % 8.09/1.32 % (4118208)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3615733913:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 8.09/1.32 % Detected minimum model sizes of [1] % 8.09/1.32 % Detected maximum model sizes of [2] % 8.09/1.32 % fmb_start_size (= 20) larger than a detected sort maximum size! % 8.09/1.32 % (4118208)Refutation not found, incomplete strategy % 8.09/1.32 % (4118208)------------------------------ % 8.09/1.32 % (4118208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.32 % (4118208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.32 % (4118208)CaDiCaL version: 2.1.3 % 8.09/1.32 % (4118208)Termination reason: Refutation not found, incomplete strategy % 8.09/1.32 % (4118208)Time elapsed: 0.001 s % 8.09/1.32 % (4118208)Peak memory usage: 10 MB % 8.09/1.32 % (4118208)Instructions burned: 2 (million) % 8.09/1.32 % (4118208)------------------------------ % 8.09/1.32 % (4118208)------------------------------ % 8.09/1.32 % (4118210)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3563421992:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 8.09/1.32 % Detected minimum model sizes of [1] % 8.09/1.32 % Detected maximum model sizes of [2] % 8.09/1.32 % fmb_start_size (= 8) larger than a detected sort maximum size! % 8.09/1.32 % (4118210)Refutation not found, incomplete strategy % 8.09/1.32 % (4118210)------------------------------ % 8.09/1.32 % (4118210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.32 % (4118210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.32 % (4118210)CaDiCaL version: 2.1.3 % 8.09/1.32 % (4118210)Termination reason: Refutation not found, incomplete strategy % 8.09/1.32 % (4118210)Time elapsed: 0.001 s % 8.09/1.32 % (4118210)Peak memory usage: 10 MB % 8.09/1.32 % (4118210)Instructions burned: 2 (million) % 8.09/1.32 % (4118210)------------------------------ % 8.09/1.32 % (4118210)------------------------------ % 8.09/1.32 % (4118212)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2927196570:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 10.60/1.81 % (4118212)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 10.60/1.81 % (4118189)Instruction limit reached! % 10.60/1.81 % (4118189)------------------------------ % 10.60/1.81 % (4118189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.60/1.81 % (4118189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.60/1.81 % (4118189)CaDiCaL version: 2.1.3 % 10.60/1.81 % (4118189)Termination reason: Instruction limit % 10.60/1.81 % (4118189)Termination phase: Saturation % 10.60/1.81 % (4118189)Time elapsed: 0.198 s % 10.60/1.81 % (4118189)Peak memory usage: 13 MB % 10.60/1.81 % (4118189)Instructions burned: 688 (million) % 10.60/1.81 % (4118214)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3256727171:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 10.60/1.81 % (4118214)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.60/1.81 % (4118214)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 10.60/1.81 % (4118202)Instruction limit reached! % 10.60/1.81 % (4118202)------------------------------ % 10.60/1.81 % (4118202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.60/1.81 % (4118202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.60/1.81 % (4118202)CaDiCaL version: 2.1.3 % 10.60/1.81 % (4118202)Termination reason: Instruction limit % 10.60/1.81 % (4118202)Termination phase: Saturation % 10.60/1.81 % (4118202)Time elapsed: 0.204 s % 10.60/1.81 % (4118202)Peak memory usage: 12 MB % 10.60/1.81 % (4118202)Instructions burned: 693 (million) % 10.60/1.81 % (4118216)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=170619523:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 10.60/1.81 % Detected minimum model sizes of [1] % 10.60/1.81 % Detected maximum model sizes of [2] % 10.60/1.81 % fmb_start_size (= 77) larger than a detected sort maximum size! % 10.60/1.81 % (4118216)Refutation not found, incomplete strategy % 10.60/1.81 % (4118216)------------------------------ % 10.60/1.81 % (4118216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.60/1.81 % (4118216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.60/1.81 % (4118216)CaDiCaL version: 2.1.3 % 10.60/1.81 % (4118216)Termination reason: Refutation not found, incomplete strategy % 10.60/1.81 % (4118216)Time elapsed: 0.001 s % 10.60/1.81 % (4118216)Peak memory usage: 11 MB % 10.60/1.81 % (4118216)Instructions burned: 2 (million) % 10.60/1.81 % (4118216)------------------------------ % 10.60/1.81 % (4118216)------------------------------ % 10.60/1.81 % (4118218)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2796442535:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 10.60/1.81 % TRYING [16] % 10.60/1.81 % Finite Model Found! % 10.60/1.81 % SZS status Satisfiable for theBenchmark % 10.60/1.81 % (4118218)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.60/1.81 % (4118218)------------------------------ % 10.60/1.81 % (4118218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.60/1.81 % (4118218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.60/1.81 % (4118218)CaDiCaL version: 2.1.3 % 10.60/1.81 % (4118218)Termination reason: Unknown % 10.60/1.81 % (4118218)Termination phase: Finite model building constraint generation % 10.60/1.81 % (4118218)Time elapsed: 0.001 s % 10.60/1.81 % (4118218)Peak memory usage: 11 MB % 10.60/1.81 % (4118218)Instructions burned: 6 (million) % 10.60/1.81 % (4118220)ott-2_1_sil=16000:newcnf=on:random_seed=4222753828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 10.60/1.81 % (4118220)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 10.60/1.81 % (4118198)Instruction limit reached! % 10.60/1.81 % (4118198)------------------------------ % 10.60/1.81 % (4118198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.60/1.81 % (4118198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.60/1.81 % (4118198)CaDiCaL version: 2.1.3 % 10.60/1.81 % (4118198)Termination reason: Instruction limit % 10.60/1.81 % (4118198)Termination phase: Saturation % 10.60/1.81 % (4118198)Time elapsed: 0.263 s % 10.60/1.81 % (4118198)Peak memory usage: 12 MB % 10.60/1.81 % (4118198)Instructions burned: 1185 (million) % 10.60/1.81 % (4118222)ott+10_1_sil=32000:tgt=ground:random_seed=437644607:i=5114:av=off_2996 on theBenchmark for (2996ds/5114Mi) % 28.52/4.29 % (4118203)Instruction limit reached! % 28.52/4.29 % (4118203)------------------------------ % 28.52/4.29 % (4118203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.52/4.29 % (4118203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.52/4.29 % (4118203)CaDiCaL version: 2.1.3 % 28.52/4.29 % (4118203)Termination reason: Instruction limit % 28.52/4.29 % (4118203)Termination phase: Saturation % 28.52/4.29 % (4118203)Time elapsed: 0.268 s % 28.52/4.29 % (4118203)Peak memory usage: 12 MB % 28.52/4.29 % (4118203)Instructions burned: 879 (million) % 28.52/4.29 % (4118224)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=565032739:i=54282_2996 on theBenchmark for (2996ds/54282Mi) % 28.52/4.29 % Detected minimum model sizes of [1] % 28.52/4.29 % Detected maximum model sizes of [2] % 28.52/4.29 % TRYING [1] % 28.52/4.29 % TRYING [2] % 28.52/4.29 % Finite Model Found! % 28.52/4.29 % SZS status Satisfiable for theBenchmark % 28.52/4.29 % (4118224)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.52/4.29 % (4118224)------------------------------ % 28.52/4.29 % (4118224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.52/4.29 % (4118224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.52/4.29 % (4118224)CaDiCaL version: 2.1.3 % 28.52/4.29 % (4118224)Termination reason: Unknown % 28.52/4.29 % (4118224)Termination phase: Finite model building constraint generation % 28.52/4.29 % (4118224)Time elapsed: 0.001 s % 28.52/4.29 % (4118224)Peak memory usage: 11 MB % 28.52/4.29 % (4118224)Instructions burned: 2 (million) % 28.52/4.29 % (4118226)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3097110655:i=3512:aac=none_2995 on theBenchmark for (2995ds/3512Mi) % 28.52/4.29 % (4118226)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 28.52/4.29 % (4118214)Instruction limit reached! % 28.52/4.29 % (4118214)------------------------------ % 28.52/4.29 % (4118214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.52/4.29 % (4118214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.52/4.29 % (4118214)CaDiCaL version: 2.1.3 % 28.52/4.29 % (4118214)Termination reason: Instruction limit % 28.52/4.29 % (4118214)Termination phase: Saturation % 28.52/4.29 % (4118214)Time elapsed: 0.342 s % 28.52/4.29 % (4118214)Peak memory usage: 13 MB % 28.52/4.29 % (4118214)Instructions burned: 1472 (million) % 28.52/4.29 % (4118228)dis+21_1_sil=32000:sas=cadical:random_seed=3595696329:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 28.52/4.29 % (4118220)Instruction limit reached! % 28.52/4.29 % (4118220)------------------------------ % 28.52/4.29 % (4118220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.52/4.29 % (4118220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.52/4.29 % (4118220)CaDiCaL version: 2.1.3 % 28.52/4.29 % (4118220)Termination reason: Instruction limit % 28.52/4.29 % (4118220)Termination phase: Saturation % 28.52/4.29 % (4118220)Time elapsed: 0.268 s % 28.52/4.29 % (4118220)Peak memory usage: 12 MB % 28.52/4.29 % (4118220)Instructions burned: 869 (million) % 28.52/4.29 % (4118230)ott+11_1_sil=16000:gs=on:random_seed=2630822795:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi) % 28.52/4.29 % (4118230)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 28.52/4.29 % (4118226)Instruction limit reached! % 28.52/4.29 % (4118226)------------------------------ % 28.52/4.29 % (4118226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.52/4.29 % (4118226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.52/4.29 % (4118226)CaDiCaL version: 2.1.3 % 28.52/4.29 % (4118226)Termination reason: Instruction limit % 28.52/4.29 % (4118226)Termination phase: Saturation % 28.52/4.29 % (4118226)Time elapsed: 0.755 s % 28.52/4.29 % (4118226)Peak memory usage: 14 MB % 28.52/4.29 % (4118226)Instructions burned: 3512 (million) % 28.52/4.29 % (4118239)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2210428415:fmbsr=1.6:i=67534_2988 on theBenchmark for (2988ds/67534Mi) % 28.52/4.29 % Detected minimum model sizes of [1] % 28.52/4.29 % Detected maximum model sizes of [3] % 28.52/4.29 % fmb_start_size (= 7) larger than a detected sort maximum size! % 28.52/4.29 % (4118239)Refutation not found, incomplete strategy % 28.52/4.29 % (4118239)------------------------------ % 28.52/4.29 % (4118239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118239)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118239)Termination reason: Refutation not found, incomplete strategy % 63.82/9.22 % (4118239)Time elapsed: 0.001 s % 63.82/9.22 % (4118239)Peak memory usage: 10 MB % 63.82/9.22 % (4118239)Instructions burned: 2 (million) % 63.82/9.22 % (4118239)------------------------------ % 63.82/9.22 % (4118239)------------------------------ % 63.82/9.22 % (4118241)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1761623240:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2988 on theBenchmark for (2988ds/4591Mi) % 63.82/9.22 % (4118230)Instruction limit reached! % 63.82/9.22 % (4118230)------------------------------ % 63.82/9.22 % (4118230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118230)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118230)Termination reason: Instruction limit % 63.82/9.22 % (4118230)Termination phase: Saturation % 63.82/9.22 % (4118230)Time elapsed: 0.593 s % 63.82/9.22 % (4118230)Peak memory usage: 12 MB % 63.82/9.22 % (4118230)Instructions burned: 2255 (million) % 63.82/9.22 % (4118243)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2604541701:i=29340_2987 on theBenchmark for (2987ds/29340Mi) % 63.82/9.22 % (4118212)Instruction limit reached! % 63.82/9.22 % (4118212)------------------------------ % 63.82/9.22 % (4118212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118212)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118212)Termination reason: Instruction limit % 63.82/9.22 % (4118212)Termination phase: Saturation % 63.82/9.22 % (4118212)Time elapsed: 1.294 s % 63.82/9.22 % (4118212)Peak memory usage: 13 MB % 63.82/9.22 % (4118212)Instructions burned: 5136 (million) % 63.82/9.22 % (4118245)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4194445769:i=5211_2984 on theBenchmark for (2984ds/5211Mi) % 63.82/9.22 % (4118222)Instruction limit reached! % 63.82/9.22 % (4118222)------------------------------ % 63.82/9.22 % (4118222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118222)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118222)Termination reason: Instruction limit % 63.82/9.22 % (4118222)Termination phase: Saturation % 63.82/9.22 % (4118222)Time elapsed: 1.259 s % 63.82/9.22 % (4118222)Peak memory usage: 12 MB % 63.82/9.22 % (4118222)Instructions burned: 5119 (million) % 63.82/9.22 % (4118247)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2909607534:i=5497:nm=2_2983 on theBenchmark for (2983ds/5497Mi) % 63.82/9.22 % Detected minimum model sizes of [1] % 63.82/9.22 % Detected maximum model sizes of [2] % 63.82/9.22 % fmb_start_size (= 17) larger than a detected sort maximum size! % 63.82/9.22 % (4118247)Refutation not found, incomplete strategy % 63.82/9.22 % (4118247)------------------------------ % 63.82/9.22 % (4118247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118247)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118247)Termination reason: Refutation not found, incomplete strategy % 63.82/9.22 % (4118247)Time elapsed: 0.001 s % 63.82/9.22 % (4118247)Peak memory usage: 10 MB % 63.82/9.22 % (4118247)Instructions burned: 2 (million) % 63.82/9.22 % (4118247)------------------------------ % 63.82/9.22 % (4118247)------------------------------ % 63.82/9.22 % (4118249)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1850019326:fmbsr=2:i=46332_2983 on theBenchmark for (2983ds/46332Mi) % 63.82/9.22 % Detected minimum model sizes of [1] % 63.82/9.22 % Detected maximum model sizes of [3] % 63.82/9.22 % fmb_start_size (= 15) larger than a detected sort maximum size! % 63.82/9.22 % (4118249)Refutation not found, incomplete strategy % 63.82/9.22 % (4118249)------------------------------ % 63.82/9.22 % (4118249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.82/9.22 % (4118249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.82/9.22 % (4118249)CaDiCaL version: 2.1.3 % 63.82/9.22 % (4118249)Termination reason: Refutation not found, incomplete strategy % 63.82/9.22 % (4118249)Time elapsed: 0.001 s % 63.82/9.22 % (4118249)Peak memory usage: 10 MB % 75.86/10.93 % (4118249)Instructions burned: 2 (million) % 75.86/10.93 % (4118249)------------------------------ % 75.86/10.93 % (4118249)------------------------------ % 75.86/10.93 % (4118251)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2723862028:i=14071_2983 on theBenchmark for (2983ds/14071Mi) % 75.86/10.93 % Detected minimum model sizes of [1] % 75.86/10.93 % Detected maximum model sizes of [2] % 75.86/10.93 % fmb_start_size (= 12) larger than a detected sort maximum size! % 75.86/10.93 % (4118251)Refutation not found, incomplete strategy % 75.86/10.93 % (4118251)------------------------------ % 75.86/10.93 % (4118251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.86/10.93 % (4118251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/10.93 % (4118251)CaDiCaL version: 2.1.3 % 75.86/10.93 % (4118251)Termination reason: Refutation not found, incomplete strategy % 75.86/10.93 % (4118251)Time elapsed: 0.001 s % 75.86/10.93 % (4118251)Peak memory usage: 10 MB % 75.86/10.93 % (4118251)Instructions burned: 2 (million) % 75.86/10.93 % (4118251)------------------------------ % 75.86/10.93 % (4118251)------------------------------ % 75.86/10.93 % (4118228)Instruction limit reached! % 75.86/10.93 % (4118228)------------------------------ % 75.86/10.93 % (4118228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.86/10.93 % (4118228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/10.93 % (4118228)CaDiCaL version: 2.1.3 % 75.86/10.93 % (4118228)Termination reason: Instruction limit % 75.86/10.93 % (4118228)Termination phase: Saturation % 75.86/10.93 % (4118228)Time elapsed: 1.072 s % 75.86/10.93 % (4118228)Peak memory usage: 15 MB % 75.86/10.93 % (4118228)Instructions burned: 3774 (million) % 75.86/10.93 % (4118253)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4042258474:i=22565:add=on:rawr=on_2983 on theBenchmark for (2983ds/22565Mi) % 75.86/10.93 % (4118254)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3792228165:i=8173:av=off_2983 on theBenchmark for (2983ds/8173Mi) % 75.86/10.93 % (4118241)Instruction limit reached! % 75.86/10.93 % (4118241)------------------------------ % 75.86/10.93 % (4118241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.86/10.93 % (4118241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/10.93 % (4118241)CaDiCaL version: 2.1.3 % 75.86/10.93 % (4118241)Termination reason: Instruction limit % 75.86/10.93 % (4118241)Termination phase: Saturation % 75.86/10.93 % (4118241)Time elapsed: 0.947 s % 75.86/10.93 % (4118241)Peak memory usage: 13 MB % 75.86/10.93 % (4118241)Instructions burned: 4593 (million) % 75.86/10.93 % (4118262)dis+10_16:1_sil=16000:random_seed=3441413396:i=9155:fsr=off_2978 on theBenchmark for (2978ds/9155Mi) % 75.86/10.93 % (4118245)Instruction limit reached! % 75.86/10.93 % (4118245)------------------------------ % 75.86/10.93 % (4118245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.86/10.93 % (4118245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/10.93 % (4118245)CaDiCaL version: 2.1.3 % 75.86/10.93 % (4118245)Termination reason: Instruction limit % 75.86/10.93 % (4118245)Termination phase: Saturation % 75.86/10.93 % (4118245)Time elapsed: 1.701 s % 75.86/10.93 % (4118245)Peak memory usage: 15 MB % 75.86/10.93 % (4118245)Instructions burned: 5213 (million) % 75.86/10.93 % (4118269)ott-3_8_sil=64000:random_seed=876451854:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 75.86/10.93 % (4118254)Instruction limit reached! % 75.86/10.93 % (4118254)------------------------------ % 75.86/10.93 % (4118254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.86/10.93 % (4118254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/10.93 % (4118254)CaDiCaL version: 2.1.3 % 75.86/10.93 % (4118254)Termination reason: Instruction limit % 75.86/10.93 % (4118254)Termination phase: Saturation % 75.86/10.93 % (4118254)Time elapsed: 2.427 s % 75.86/10.93 % (4118254)Peak memory usage: 12 MB % 75.86/10.93 % (4118254)Instructions burned: 8176 (million) % 75.86/10.93 % (4118271)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1746417038:fmbsr=2:i=32576_2958 on theBenchmark for (2958ds/32576Mi) % 75.86/10.93 % Detected minimum model sizes of [1] % 75.86/10.93 % Detected maximum model sizes of [2] % 75.86/10.93 % fmb_start_size (= 9) larger than a detected sort maximum size! % 75.86/10.93 % (4118271)Refutation not found, incomplete strategy % 75.86/10.93 % (4118271)------------------------------ % 75.86/10.93 % (4118271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118271)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118271)Termination reason: Refutation not found, incomplete strategy % 86.28/12.43 % (4118271)Time elapsed: 0.001 s % 86.28/12.43 % (4118271)Peak memory usage: 10 MB % 86.28/12.43 % (4118271)Instructions burned: 2 (million) % 86.28/12.43 % (4118271)------------------------------ % 86.28/12.43 % (4118271)------------------------------ % 86.28/12.43 % (4118273)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3310306744:i=11404_2958 on theBenchmark for (2958ds/11404Mi) % 86.28/12.43 % (4118262)Instruction limit reached! % 86.28/12.43 % (4118262)------------------------------ % 86.28/12.43 % (4118262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118262)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118262)Termination reason: Instruction limit % 86.28/12.43 % (4118262)Termination phase: Saturation % 86.28/12.43 % (4118262)Time elapsed: 2.230 s % 86.28/12.43 % (4118262)Peak memory usage: 16 MB % 86.28/12.43 % (4118262)Instructions burned: 9156 (million) % 86.28/12.43 % (4118275)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1145914766:i=14134_2956 on theBenchmark for (2956ds/14134Mi) % 86.28/12.43 % (4118275)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 86.28/12.43 % (4118253)Instruction limit reached! % 86.28/12.43 % (4118253)------------------------------ % 86.28/12.43 % (4118253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118253)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118253)Termination reason: Instruction limit % 86.28/12.43 % (4118253)Termination phase: Saturation % 86.28/12.43 % (4118253)Time elapsed: 5.679 s % 86.28/12.43 % (4118253)Peak memory usage: 14 MB % 86.28/12.43 % (4118253)Instructions burned: 22568 (million) % 86.28/12.43 % (4118277)dis+33_16_sil=32000:sac=on:random_seed=2268374412:i=15851:nm=0_2926 on theBenchmark for (2926ds/15851Mi) % 86.28/12.43 % (4118275)Instruction limit reached! % 86.28/12.43 % (4118275)------------------------------ % 86.28/12.43 % (4118275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118275)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118275)Termination reason: Instruction limit % 86.28/12.43 % (4118275)Termination phase: Saturation % 86.28/12.43 % (4118275)Time elapsed: 3.055 s % 86.28/12.43 % (4118275)Peak memory usage: 12 MB % 86.28/12.43 % (4118275)Instructions burned: 14138 (million) % 86.28/12.43 % (4118279)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2777379355:avsq=on:i=17627:add=on:amm=off_2925 on theBenchmark for (2925ds/17627Mi) % 86.28/12.43 % (4118273)Instruction limit reached! % 86.28/12.43 % (4118273)------------------------------ % 86.28/12.43 % (4118273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118273)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118273)Termination reason: Instruction limit % 86.28/12.43 % (4118273)Termination phase: Saturation % 86.28/12.43 % (4118273)Time elapsed: 3.327 s % 86.28/12.43 % (4118273)Peak memory usage: 13 MB % 86.28/12.43 % (4118273)Instructions burned: 11406 (million) % 86.28/12.43 % (4118281)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=178918153:s2a=on:i=53295_2925 on theBenchmark for (2925ds/53295Mi) % 86.28/12.43 % (4118269)Instruction limit reached! % 86.28/12.43 % (4118269)------------------------------ % 86.28/12.43 % (4118269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.28/12.43 % (4118269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.28/12.43 % (4118269)CaDiCaL version: 2.1.3 % 86.28/12.43 % (4118269)Termination reason: Instruction limit % 86.28/12.43 % (4118269)Termination phase: Saturation % 86.28/12.43 % (4118269)Time elapsed: 5.791 s % 86.28/12.43 % (4118269)Peak memory usage: 14 MB % 86.28/12.43 % (4118269)Instructions burned: 20140 (million) % 86.28/12.43 % (4118283)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=111399152:i=26857:ins=20_2909 on theBenchmark for (2909ds/26857Mi) % 86.28/12.43 % Detected minimum model sizes of [1] % 86.28/12.43 % Detected maximum model sizes of [2] % 86.28/12.43 % fmb_start_size (= 16) larger than a detected sort maximum size! % 86.28/12.43 % (4118283)Refutation not found, incomplete strategy % 88.66/12.81 % (4118283)------------------------------ % 88.66/12.81 % (4118283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.66/12.81 % (4118283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.66/12.81 % (4118283)CaDiCaL version: 2.1.3 % 88.66/12.81 % (4118283)Termination reason: Refutation not found, incomplete strategy % 88.66/12.81 % (4118283)Time elapsed: 0.001 s % 88.66/12.81 % (4118283)Peak memory usage: 10 MB % 88.66/12.81 % (4118283)Instructions burned: 2 (million) % 88.66/12.81 % (4118283)------------------------------ % 88.66/12.81 % (4118283)------------------------------ % 88.66/12.81 % (4118285)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=798335811:i=28120:bs=on:fsr=off_2909 on theBenchmark for (2909ds/28120Mi) % 88.66/12.81 % (4118243)Instruction limit reached! % 88.66/12.81 % (4118243)------------------------------ % 88.66/12.81 % (4118243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.66/12.81 % (4118243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.66/12.81 % (4118243)CaDiCaL version: 2.1.3 % 88.66/12.81 % (4118243)Termination reason: Instruction limit % 88.66/12.81 % (4118243)Termination phase: Saturation % 88.66/12.81 % (4118243)Time elapsed: 9.489 s % 88.66/12.81 % (4118243)Peak memory usage: 16 MB % 88.66/12.81 % (4118243)Instructions burned: 29343 (million) % 88.66/12.81 % (4118288)fmb+10_1_sil=256000:fmbss=7:random_seed=2045372794:fmbsr=1.6:i=182295_2892 on theBenchmark for (2892ds/182295Mi) % 88.66/12.81 % Detected minimum model sizes of [1] % 88.66/12.81 % Detected maximum model sizes of [2] % 88.66/12.81 % fmb_start_size (= 7) larger than a detected sort maximum size! % 88.66/12.81 % (4118288)Refutation not found, incomplete strategy % 88.66/12.81 % (4118288)------------------------------ % 88.66/12.81 % (4118288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.66/12.81 % (4118288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.66/12.81 % (4118288)CaDiCaL version: 2.1.3 % 88.66/12.81 % (4118288)Termination reason: Refutation not found, incomplete strategy % 88.66/12.81 % (4118288)Time elapsed: 0.001 s % 88.66/12.81 % (4118288)Peak memory usage: 11 MB % 88.66/12.81 % (4118288)Instructions burned: 2 (million) % 88.66/12.81 % (4118288)------------------------------ % 88.66/12.81 % (4118288)------------------------------ % 88.66/12.81 % (4118290)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3737919419:i=44625:gsp=on_2892 on theBenchmark for (2892ds/44625Mi) % 88.66/12.81 % (4118290)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 88.66/12.81 % (4118290)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 88.66/12.81 % Detected minimum model sizes of [1] % 88.66/12.81 % Detected maximum model sizes of [2] % 88.66/12.81 % fmb_start_size (= 21) larger than a detected sort maximum size! % 88.66/12.81 % (4118290)Refutation not found, incomplete strategy % 88.66/12.81 % (4118290)------------------------------ % 88.66/12.81 % (4118290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.66/12.81 % (4118290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.66/12.81 % (4118290)CaDiCaL version: 2.1.3 % 88.66/12.81 % (4118290)Termination reason: Refutation not found, incomplete strategy % 88.66/12.81 % (4118290)Time elapsed: 0.001 s % 88.66/12.81 % (4118290)Peak memory usage: 11 MB % 88.66/12.81 % (4118290)Instructions burned: 2 (million) % 88.66/12.81 % (4118290)------------------------------ % 88.66/12.81 % (4118290)------------------------------ % 88.66/12.81 % (4118292)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=960467712:i=160505_2892 on theBenchmark for (2892ds/160505Mi) % 88.66/12.81 % Detected minimum model sizes of [1] % 88.66/12.81 % Detected maximum model sizes of [2] % 88.66/12.81 % fmb_start_size (= 15) larger than a detected sort maximum size! % 88.66/12.81 % (4118292)Refutation not found, incomplete strategy % 88.66/12.81 % (4118292)------------------------------ % 88.66/12.81 % (4118292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.66/12.81 % (4118292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.66/12.81 % (4118292)CaDiCaL version: 2.1.3 % 88.66/12.81 % (4118292)Termination reason: Refutation not found, incomplete strategy % 88.66/12.81 % (4118292)Time elapsed: 0.001 s % 88.66/12.81 % (4118292)Peak memory usage: 11 MB % 88.66/12.81 % (4118292)Instructions burned: 2 (million) % 88.66/12.81 % (4118292)------------------------------ % 88.66/12.81 % (4118292)------------------------------ % 88.66/12.81 % (4118294)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1289641848:fmbsr=1.3:i=225729_2892 on theBenchmark for (2892ds/225729Mi) % 94.07/13.59 % Detected minimum model sizes of [1] % 94.07/13.59 % Detected maximum model sizes of [2] % 94.07/13.59 % fmb_start_size (= 10) larger than a detected sort maximum size! % 94.07/13.59 % (4118294)Refutation not found, incomplete strategy % 94.07/13.59 % (4118294)------------------------------ % 94.07/13.59 % (4118294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.07/13.59 % (4118294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.07/13.59 % (4118294)CaDiCaL version: 2.1.3 % 94.07/13.59 % (4118294)Termination reason: Refutation not found, incomplete strategy % 94.07/13.59 % (4118294)Time elapsed: 0.001 s % 94.07/13.59 % (4118294)Peak memory usage: 10 MB % 94.07/13.59 % (4118294)Instructions burned: 2 (million) % 94.07/13.59 % (4118294)------------------------------ % 94.07/13.59 % (4118294)------------------------------ % 94.07/13.59 % (4118296)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1543149233:fmbsr=2:i=185024:ins=7_2891 on theBenchmark for (2891ds/185024Mi) % 94.07/13.59 % Detected minimum model sizes of [1] % 94.07/13.59 % Detected maximum model sizes of [2] % 94.07/13.59 % fmb_start_size (= 10) larger than a detected sort maximum size! % 94.07/13.59 % (4118296)Refutation not found, incomplete strategy % 94.07/13.59 % (4118296)------------------------------ % 94.07/13.59 % (4118296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.07/13.59 % (4118296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.07/13.59 % (4118296)CaDiCaL version: 2.1.3 % 94.07/13.59 % (4118296)Termination reason: Refutation not found, incomplete strategy % 94.07/13.59 % (4118296)Time elapsed: 0.001 s % 94.07/13.59 % (4118296)Peak memory usage: 10 MB % 94.07/13.59 % (4118296)Instructions burned: 2 (million) % 94.07/13.59 % (4118296)------------------------------ % 94.07/13.59 % (4118296)------------------------------ % 94.07/13.59 % (4118298)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=418988258:rtra=on_2891 on theBenchmark for (2891ds/0Mi) % 94.07/13.59 % Detected minimum model sizes of [1] % 94.07/13.59 % Detected maximum model sizes of [2] % 94.07/13.59 % TRYING [1] % 94.07/13.59 % TRYING [2] % 94.07/13.59 % Finite Model Found! % 94.07/13.59 % SZS status Satisfiable for theBenchmark % 94.07/13.59 % (4118298)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 94.07/13.59 % (4118298)------------------------------ % 94.07/13.59 % (4118298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.07/13.59 % (4118298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.07/13.59 % (4118298)CaDiCaL version: 2.1.3 % 94.07/13.59 % (4118298)Termination reason: Unknown % 94.07/13.59 % (4118298)Termination phase: Finite model building constraint generation % 94.07/13.59 % (4118298)Time elapsed: 0.001 s % 94.07/13.59 % (4118298)Peak memory usage: 11 MB % 94.07/13.59 % (4118298)Instructions burned: 2 (million) % 94.07/13.59 % (4118300)% WARNING: option uhcvi not known. % 94.07/13.59 % (4118300)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4222679156:i=271062:add=off:rtra=on:rawr=on_2891 on theBenchmark for (2891ds/271062Mi) % 94.07/13.59 % (4118300)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 94.07/13.59 % (4118300)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 94.07/13.59 % (4118277)Instruction limit reached! % 94.07/13.59 % (4118277)------------------------------ % 94.07/13.59 % (4118277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.07/13.59 % (4118277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.07/13.59 % (4118277)CaDiCaL version: 2.1.3 % 94.07/13.59 % (4118277)Termination reason: Instruction limit % 94.07/13.59 % (4118277)Termination phase: Saturation % 94.07/13.59 % (4118277)Time elapsed: 4.690 s % 94.07/13.59 % (4118277)Peak memory usage: 14 MB % 94.07/13.59 % (4118277)Instructions burned: 15853 (million) % 94.07/13.59 % (4118305)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3837894766:i=176048:add=on:rtra=on:rawr=on_2879 on theBenchmark for (2879ds/176048Mi) % 94.07/13.59 % (4118279)Instruction limit reached! % 94.07/13.59 % (4118279)------------------------------ % 94.07/13.59 % (4118279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.07/13.59 % (4118279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.07/13.59 % (4118279)CaDiCaL version: 2.1.3 % 94.07/13.59 % (4118279)Termination reason: Instruction limit % 97.92/14.10 % (4118279)Termination phase: Saturation % 97.92/14.10 % (4118279)Time elapsed: 4.827 s % 97.92/14.10 % (4118279)Peak memory usage: 22 MB % 97.92/14.10 % (4118279)Instructions burned: 17631 (million) % 97.92/14.10 % (4118307)dis+10_1_sil=32000:si=on:sp=arity:random_seed=529952302:i=206:fgj=on:rtra=on_2877 on theBenchmark for (2877ds/206Mi) % 97.92/14.10 % (4118307)Instruction limit reached! % 97.92/14.10 % (4118307)------------------------------ % 97.92/14.10 % (4118307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.10 % (4118307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.10 % (4118307)CaDiCaL version: 2.1.3 % 97.92/14.10 % (4118307)Termination reason: Instruction limit % 97.92/14.10 % (4118307)Termination phase: Saturation % 97.92/14.10 % (4118307)Time elapsed: 0.056 s % 97.92/14.10 % (4118307)Peak memory usage: 12 MB % 97.92/14.10 % (4118307)Instructions burned: 242 (million) % 97.92/14.10 % (4118309)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2272029568:i=232:rtra=on_2876 on theBenchmark for (2876ds/232Mi) % 97.92/14.10 % (4118309)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 97.92/14.10 % (4118309)Instruction limit reached! % 97.92/14.10 % (4118309)------------------------------ % 97.92/14.10 % (4118309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.10 % (4118309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.10 % (4118309)CaDiCaL version: 2.1.3 % 97.92/14.10 % (4118309)Termination reason: Instruction limit % 97.92/14.10 % (4118309)Termination phase: Saturation % 97.92/14.10 % (4118309)Time elapsed: 0.055 s % 97.92/14.10 % (4118309)Peak memory usage: 11 MB % 97.92/14.10 % (4118309)Instructions burned: 232 (million) % 97.92/14.10 % (4118311)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2637655170:i=262:rtra=on_2875 on theBenchmark for (2875ds/262Mi) % 97.92/14.10 % (4118311)Instruction limit reached! % 97.92/14.10 % (4118311)------------------------------ % 97.92/14.10 % (4118311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.10 % (4118311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.10 % (4118311)CaDiCaL version: 2.1.3 % 97.92/14.10 % (4118311)Termination reason: Instruction limit % 97.92/14.10 % (4118311)Termination phase: Saturation % 97.92/14.10 % (4118311)Time elapsed: 0.061 s % 97.92/14.10 % (4118311)Peak memory usage: 12 MB % 97.92/14.10 % (4118311)Instructions burned: 264 (million) % 97.92/14.10 % (4118313)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4053278271:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2874 on theBenchmark for (2874ds/318Mi) % 97.92/14.10 % (4118313)Instruction limit reached! % 97.92/14.10 % (4118313)------------------------------ % 97.92/14.10 % (4118313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.10 % (4118313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.10 % (4118313)CaDiCaL version: 2.1.3 % 97.92/14.10 % (4118313)Termination reason: Instruction limit % 97.92/14.10 % (4118313)Termination phase: Saturation % 97.92/14.10 % (4118313)Time elapsed: 0.069 s % 97.92/14.10 % (4118313)Peak memory usage: 12 MB % 97.92/14.10 % (4118313)Instructions burned: 318 (million) % 97.92/14.10 % (4118315)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3732736828:i=1428:nm=2:rtra=on_2874 on theBenchmark for (2874ds/1428Mi) % 97.92/14.10 % Detected minimum model sizes of [1] % 97.92/14.10 % Detected maximum model sizes of [3] % 97.92/14.10 % TRYING [1] % 97.92/14.10 % TRYING [2] % 97.92/14.10 % Finite Model Found! % 97.92/14.10 % SZS status Satisfiable for theBenchmark % 97.92/14.10 % (4118315)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 97.92/14.10 % (4118315)------------------------------ % 97.92/14.10 % (4118315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.92/14.10 % (4118315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.92/14.10 % (4118315)CaDiCaL version: 2.1.3 % 97.92/14.10 % (4118315)Termination reason: Unknown % 97.92/14.10 % (4118315)Termination phase: Finite model building constraint generation % 97.92/14.10 % (4118315)Time elapsed: 0.001 s % 97.92/14.10 % (4118315)Peak memory usage: 11 MB % 97.92/14.10 % (4118315)Instructions burned: 3 (million) % 97.92/14.10 % (4118317)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2826331331:i=262:bd=preordered:rtra=on:fsd=on_2873 on theBenchmark for (2873ds/262Mi) % 97.92/14.10 % (4118317)Instruction limit reached! % 97.92/14.10 % (4118317)------------------------------ % 101.66/14.74 % (4118317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118317)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118317)Termination reason: Instruction limit % 101.66/14.74 % (4118317)Termination phase: Saturation % 101.66/14.74 % (4118317)Time elapsed: 0.059 s % 101.66/14.74 % (4118317)Peak memory usage: 12 MB % 101.66/14.74 % (4118317)Instructions burned: 264 (million) % 101.66/14.74 % (4118319)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=4153551086:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2873 on theBenchmark for (2873ds/1368Mi) % 101.66/14.74 % (4118319)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 101.66/14.74 % (4118319)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 101.66/14.74 % (4118319)Instruction limit reached! % 101.66/14.74 % (4118319)------------------------------ % 101.66/14.74 % (4118319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118319)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118319)Termination reason: Instruction limit % 101.66/14.74 % (4118319)Termination phase: Saturation % 101.66/14.74 % (4118319)Time elapsed: 0.421 s % 101.66/14.74 % (4118319)Peak memory usage: 13 MB % 101.66/14.74 % (4118319)Instructions burned: 1370 (million) % 101.66/14.74 % (4118322)ott-21_1_sil=16000:si=on:fs=off:random_seed=1171038615:i=360:av=off:fsr=off:rtra=on_2868 on theBenchmark for (2868ds/360Mi) % 101.66/14.74 % (4118322)Instruction limit reached! % 101.66/14.74 % (4118322)------------------------------ % 101.66/14.74 % (4118322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118322)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118322)Termination reason: Instruction limit % 101.66/14.74 % (4118322)Termination phase: Saturation % 101.66/14.74 % (4118322)Time elapsed: 0.082 s % 101.66/14.74 % (4118322)Peak memory usage: 14 MB % 101.66/14.74 % (4118322)Instructions burned: 361 (million) % 101.66/14.74 % (4118324)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3229822967:i=954:bd=all:rtra=on_2868 on theBenchmark for (2868ds/954Mi) % 101.66/14.74 % (4118174)Instruction limit reached! % 101.66/14.74 % (4118174)------------------------------ % 101.66/14.74 % (4118174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118174)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118174)Termination reason: Instruction limit % 101.66/14.74 % (4118174)Termination phase: Saturation % 101.66/14.74 % (4118174)Time elapsed: 13.418 s % 101.66/14.74 % (4118174)Peak memory usage: 15 MB % 101.66/14.74 % (4118174)Instructions burned: 88029 (million) % 101.66/14.74 % (4118324)Instruction limit reached! % 101.66/14.74 % (4118324)------------------------------ % 101.66/14.74 % (4118324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118324)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118324)Termination reason: Instruction limit % 101.66/14.74 % (4118324)Termination phase: Saturation % 101.66/14.74 % (4118324)Time elapsed: 0.241 s % 101.66/14.74 % (4118324)Peak memory usage: 12 MB % 101.66/14.74 % (4118324)Instructions burned: 958 (million) % 101.66/14.74 % (4118326)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=336783295:fmbsr=1.3:i=1730:ins=25:rtra=on_2865 on theBenchmark for (2865ds/1730Mi) % 101.66/14.74 % Detected minimum model sizes of [1] % 101.66/14.74 % Detected maximum model sizes of [2] % 101.66/14.74 % TRYING [1] % 101.66/14.74 % TRYING [2] % 101.66/14.74 % Finite Model Found! % 101.66/14.74 % SZS status Satisfiable for theBenchmark % 101.66/14.74 % (4118326)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 101.66/14.74 % (4118326)------------------------------ % 101.66/14.74 % (4118326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.66/14.74 % (4118326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.66/14.74 % (4118326)CaDiCaL version: 2.1.3 % 101.66/14.74 % (4118326)Termination reason: Unknown % 101.66/14.74 % (4118326)Termination phase: Finite model building constraint generation % 101.66/14.74 % (4118326)Time elapsed: 0.001 s % 101.66/14.74 % (4118326)Peak memory usage: 10 MB % 116.32/16.78 % (4118326)Instructions burned: 2 (million) % 116.32/16.78 % (4118327)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1134735027:i=2358:rtra=on_2865 on theBenchmark for (2865ds/2358Mi) % 116.32/16.78 % (4118329)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2700745560:i=1778:ins=1:rtra=on_2865 on theBenchmark for (2865ds/1778Mi) % 116.32/16.78 % Exception at run slice level % 116.32/16.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 116.32/16.78 % (4118332)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=714783562:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2865 on theBenchmark for (2865ds/1384Mi) % 116.32/16.78 % (4118332)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 116.32/16.78 % (4118332)Instruction limit reached! % 116.32/16.78 % (4118332)------------------------------ % 116.32/16.78 % (4118332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.32/16.78 % (4118332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.32/16.78 % (4118332)CaDiCaL version: 2.1.3 % 116.32/16.78 % (4118332)Termination reason: Instruction limit % 116.32/16.78 % (4118332)Termination phase: Saturation % 116.32/16.78 % (4118332)Time elapsed: 0.277 s % 116.32/16.78 % (4118332)Peak memory usage: 13 MB % 116.32/16.78 % (4118332)Instructions burned: 1389 (million) % 116.32/16.78 % (4118335)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1870627719:i=1758:kws=inv_precedence:fsr=off:rtra=on_2862 on theBenchmark for (2862ds/1758Mi) % 116.32/16.78 % (4118335)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 116.32/16.78 % (4118327)Instruction limit reached! % 116.32/16.78 % (4118327)------------------------------ % 116.32/16.78 % (4118327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.32/16.78 % (4118327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.32/16.78 % (4118327)CaDiCaL version: 2.1.3 % 116.32/16.78 % (4118327)Termination reason: Instruction limit % 116.32/16.78 % (4118327)Termination phase: Saturation % 116.32/16.78 % (4118327)Time elapsed: 0.468 s % 116.32/16.78 % (4118327)Peak memory usage: 12 MB % 116.32/16.78 % (4118327)Instructions burned: 2362 (million) % 116.32/16.78 % (4118337)fmb+10_1_sil=64000:si=on:random_seed=3516082921:i=44122:nm=2:rtra=on:gsp=on_2860 on theBenchmark for (2860ds/44122Mi) % 116.32/16.78 % (4118337)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 116.32/16.78 % Detected minimum model sizes of [1] % 116.32/16.78 % Detected maximum model sizes of [2] % 116.32/16.78 % TRYING [1] % 116.32/16.78 % TRYING [2] % 116.32/16.78 % Finite Model Found! % 116.32/16.78 % SZS status Satisfiable for theBenchmark % 116.32/16.78 % (4118337)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.32/16.78 % (4118337)------------------------------ % 116.32/16.78 % (4118337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.32/16.78 % (4118337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.32/16.78 % (4118337)CaDiCaL version: 2.1.3 % 116.32/16.78 % (4118337)Termination reason: Unknown % 116.32/16.78 % (4118337)Termination phase: Finite model building constraint generation % 116.32/16.78 % (4118337)Time elapsed: 0.001 s % 116.32/16.78 % (4118337)Peak memory usage: 10 MB % 116.32/16.78 % (4118337)Instructions burned: 2 (million) % 116.32/16.78 % (4118339)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1964269142:i=19030:nm=5:rtra=on_2860 on theBenchmark for (2860ds/19030Mi) % 116.32/16.78 % Detected minimum model sizes of [1] % 116.32/16.78 % Detected maximum model sizes of [2] % 116.32/16.78 % fmb_start_size (= 20) larger than a detected sort maximum size! % 116.32/16.78 % (4118339)Refutation not found, incomplete strategy % 116.32/16.78 % (4118339)------------------------------ % 116.32/16.78 % (4118339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.32/16.78 % (4118339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.32/16.78 % (4118339)CaDiCaL version: 2.1.3 % 116.32/16.78 % (4118339)Termination reason: Refutation not found, incomplete strategy % 116.32/16.78 % (4118339)Time elapsed: 0.001 s % 116.32/16.78 % (4118339)Peak memory usage: 10 MB % 116.32/16.78 % (4118339)Instructions burned: 2 (million) % 116.32/16.78 % (4118339)------------------------------ % 116.32/16.78 % (4118339)------------------------------ % 116.32/16.78 % (4118341)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1644930006:fmbsr=1.7:i=1840:rtra=on_2860 on theBenchmark for (2860ds/1840Mi) % 130.28/18.72 % Detected minimum model sizes of [1] % 130.28/18.72 % Detected maximum model sizes of [2] % 130.28/18.72 % fmb_start_size (= 8) larger than a detected sort maximum size! % 130.28/18.72 % (4118341)Refutation not found, incomplete strategy % 130.28/18.72 % (4118341)------------------------------ % 130.28/18.72 % (4118341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.28/18.72 % (4118341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.28/18.72 % (4118341)CaDiCaL version: 2.1.3 % 130.28/18.72 % (4118341)Termination reason: Refutation not found, incomplete strategy % 130.28/18.72 % (4118341)Time elapsed: 0.001 s % 130.28/18.72 % (4118341)Peak memory usage: 10 MB % 130.28/18.72 % (4118341)Instructions burned: 2 (million) % 130.28/18.72 % (4118341)------------------------------ % 130.28/18.72 % (4118341)------------------------------ % 130.28/18.72 % (4118343)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1922579837:i=10262:rtra=on_2860 on theBenchmark for (2860ds/10262Mi) % 130.28/18.72 % (4118343)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 130.28/18.72 % (4118335)Instruction limit reached! % 130.28/18.72 % (4118335)------------------------------ % 130.28/18.72 % (4118335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.28/18.72 % (4118335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.28/18.72 % (4118335)CaDiCaL version: 2.1.3 % 130.28/18.72 % (4118335)Termination reason: Instruction limit % 130.28/18.72 % (4118335)Termination phase: Saturation % 130.28/18.72 % (4118335)Time elapsed: 0.362 s % 130.28/18.72 % (4118335)Peak memory usage: 12 MB % 130.28/18.72 % (4118335)Instructions burned: 1761 (million) % 130.28/18.72 % (4118345)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3396655790:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2858 on theBenchmark for (2858ds/2944Mi) % 130.28/18.72 % (4118345)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 130.28/18.72 % (4118345)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 130.28/18.72 % (4118285)Instruction limit reached! % 130.28/18.72 % (4118285)------------------------------ % 130.28/18.72 % (4118285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.28/18.72 % (4118285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.28/18.72 % (4118285)CaDiCaL version: 2.1.3 % 130.28/18.72 % (4118285)Termination reason: Instruction limit % 130.28/18.72 % (4118285)Termination phase: Saturation % 130.28/18.72 % (4118285)Time elapsed: 5.486 s % 130.28/18.72 % (4118285)Peak memory usage: 16 MB % 130.28/18.72 % (4118285)Instructions burned: 28124 (million) % 130.28/18.72 % (4118347)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=680610821:i=12648:rtra=on_2854 on theBenchmark for (2854ds/12648Mi) % 130.28/18.72 % Detected minimum model sizes of [1] % 130.28/18.72 % Detected maximum model sizes of [2] % 130.28/18.72 % fmb_start_size (= 77) larger than a detected sort maximum size! % 130.28/18.72 % (4118347)Refutation not found, incomplete strategy % 130.28/18.72 % (4118347)------------------------------ % 130.28/18.72 % (4118347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.28/18.72 % (4118347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.28/18.72 % (4118347)CaDiCaL version: 2.1.3 % 130.28/18.72 % (4118347)Termination reason: Refutation not found, incomplete strategy % 130.28/18.72 % (4118347)Time elapsed: 0.001 s % 130.28/18.72 % (4118347)Peak memory usage: 10 MB % 130.28/18.72 % (4118347)Instructions burned: 2 (million) % 130.28/18.72 % (4118347)------------------------------ % 130.28/18.72 % (4118347)------------------------------ % 130.28/18.72 % (4118349)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4286359276:fmbsr=2.30978:i=4348:rtra=on_2854 on theBenchmark for (2854ds/4348Mi) % 130.28/18.72 % TRYING [16] % 130.28/18.72 % Finite Model Found! % 130.28/18.72 % SZS status Satisfiable for theBenchmark % 130.28/18.72 % (4118349)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.28/18.72 % (4118349)------------------------------ % 130.28/18.72 % (4118349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.28/18.72 % (4118349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.28/18.72 % (4118349)CaDiCaL version: 2.1.3 % 130.28/18.72 % (4118349)Termination reason: Unknown % 160.57/23.03 % (4118349)Termination phase: Finite model building constraint generation % 160.57/23.03 % (4118349)Time elapsed: 0.002 s % 160.57/23.03 % (4118349)Peak memory usage: 11 MB % 160.57/23.03 % (4118349)Instructions burned: 6 (million) % 160.57/23.03 % (4118351)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4204669119:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2853 on theBenchmark for (2853ds/1738Mi) % 160.57/23.03 % (4118351)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 160.57/23.03 % (4118345)Instruction limit reached! % 160.57/23.03 % (4118345)------------------------------ % 160.57/23.03 % (4118345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.57/23.03 % (4118345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.57/23.03 % (4118345)CaDiCaL version: 2.1.3 % 160.57/23.03 % (4118345)Termination reason: Instruction limit % 160.57/23.03 % (4118345)Termination phase: Saturation % 160.57/23.03 % (4118345)Time elapsed: 0.728 s % 160.57/23.03 % (4118345)Peak memory usage: 14 MB % 160.57/23.03 % (4118345)Instructions burned: 2945 (million) % 160.57/23.03 % (4118353)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3168435679:i=10228:av=off:rtra=on_2851 on theBenchmark for (2851ds/10228Mi) % 160.57/23.03 % (4118351)Instruction limit reached! % 160.57/23.03 % (4118351)------------------------------ % 160.57/23.03 % (4118351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.57/23.03 % (4118351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.57/23.03 % (4118351)CaDiCaL version: 2.1.3 % 160.57/23.03 % (4118351)Termination reason: Instruction limit % 160.57/23.03 % (4118351)Termination phase: Saturation % 160.57/23.03 % (4118351)Time elapsed: 0.373 s % 160.57/23.03 % (4118351)Peak memory usage: 12 MB % 160.57/23.03 % (4118351)Instructions burned: 1743 (million) % 160.57/23.03 % (4118356)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=164108373:i=108564:rtra=on_2850 on theBenchmark for (2850ds/108564Mi) % 160.57/23.03 % Detected minimum model sizes of [1] % 160.57/23.03 % Detected maximum model sizes of [2] % 160.57/23.03 % TRYING [1] % 160.57/23.03 % TRYING [2] % 160.57/23.03 % Finite Model Found! % 160.57/23.03 % SZS status Satisfiable for theBenchmark % 160.57/23.03 % (4118356)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 160.57/23.03 % (4118356)------------------------------ % 160.57/23.03 % (4118356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.57/23.03 % (4118356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.57/23.03 % (4118356)CaDiCaL version: 2.1.3 % 160.57/23.03 % (4118356)Termination reason: Unknown % 160.57/23.03 % (4118356)Termination phase: Finite model building constraint generation % 160.57/23.03 % (4118356)Time elapsed: 0.001 s % 160.57/23.03 % (4118356)Peak memory usage: 11 MB % 160.57/23.03 % (4118356)Instructions burned: 2 (million) % 160.57/23.03 % (4118358)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3194364108:i=7024:aac=none:rtra=on_2849 on theBenchmark for (2849ds/7024Mi) % 160.57/23.03 % (4118358)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 160.57/23.03 % (4118343)Instruction limit reached! % 160.57/23.03 % (4118343)------------------------------ % 160.57/23.03 % (4118343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.57/23.03 % (4118343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.57/23.03 % (4118343)CaDiCaL version: 2.1.3 % 160.57/23.03 % (4118343)Termination reason: Instruction limit % 160.57/23.03 % (4118343)Termination phase: Saturation % 160.57/23.03 % (4118343)Time elapsed: 2.116 s % 160.57/23.03 % (4118343)Peak memory usage: 13 MB % 160.57/23.03 % (4118343)Instructions burned: 10265 (million) % 160.57/23.03 % (4118361)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3353558909:i=7546:rtra=on:amm=off_2839 on theBenchmark for (2839ds/7546Mi) % 160.57/23.03 % (4118358)Instruction limit reached! % 160.57/23.03 % (4118358)------------------------------ % 160.57/23.03 % (4118358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.57/23.03 % (4118358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.57/23.03 % (4118358)CaDiCaL version: 2.1.3 % 160.57/23.03 % (4118358)Termination reason: Instruction limit % 160.57/23.03 % (4118358)Termination phase: Saturation % 160.57/23.03 % (4118358)Time elapsed: 1.618 s % 160.57/23.03 % (4118358)Peak memory usage: 16 MB % 160.57/23.03 % (4118358)Instructions burned: 7025 (million) % 160.57/23.03 % (4118363)ott+11_1_sil=16000:si=on:gs=on:random_seed=3562397002:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2833 on theBenchmark for (2833ds/4502Mi) % 217.06/30.93 % (4118363)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 217.06/30.93 % (4118363)Instruction limit reached! % 217.06/30.93 % (4118363)------------------------------ % 217.06/30.93 % (4118363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.06/30.93 % (4118363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.06/30.93 % (4118363)CaDiCaL version: 2.1.3 % 217.06/30.93 % (4118363)Termination reason: Instruction limit % 217.06/30.93 % (4118363)Termination phase: Saturation % 217.06/30.93 % (4118363)Time elapsed: 0.992 s % 217.06/30.93 % (4118363)Peak memory usage: 13 MB % 217.06/30.93 % (4118363)Instructions burned: 4503 (million) % 217.06/30.93 % (4118375)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1268043730:fmbsr=1.6:i=135068:rtra=on_2823 on theBenchmark for (2823ds/135068Mi) % 217.06/30.93 % Detected minimum model sizes of [1] % 217.06/30.93 % Detected maximum model sizes of [3] % 217.06/30.93 % fmb_start_size (= 7) larger than a detected sort maximum size! % 217.06/30.93 % (4118375)Refutation not found, incomplete strategy % 217.06/30.93 % (4118375)------------------------------ % 217.06/30.93 % (4118375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.06/30.93 % (4118375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.06/30.93 % (4118375)CaDiCaL version: 2.1.3 % 217.06/30.93 % (4118375)Termination reason: Refutation not found, incomplete strategy % 217.06/30.93 % (4118375)Time elapsed: 0.001 s % 217.06/30.93 % (4118375)Peak memory usage: 10 MB % 217.06/30.93 % (4118375)Instructions burned: 2 (million) % 217.06/30.93 % (4118375)------------------------------ % 217.06/30.93 % (4118375)------------------------------ % 217.06/30.93 % (4118377)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=340221403:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2823 on theBenchmark for (2823ds/9182Mi) % 217.06/30.93 % (4118353)Instruction limit reached! % 217.06/30.93 % (4118353)------------------------------ % 217.06/30.93 % (4118353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.06/30.93 % (4118353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.06/30.93 % (4118353)CaDiCaL version: 2.1.3 % 217.06/30.93 % (4118353)Termination reason: Instruction limit % 217.06/30.93 % (4118353)Termination phase: Saturation % 217.06/30.93 % (4118353)Time elapsed: 2.891 s % 217.06/30.93 % (4118353)Peak memory usage: 12 MB % 217.06/30.93 % (4118353)Instructions burned: 10229 (million) % 217.06/30.93 % (4118379)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=16123051:i=58680:rtra=on_2822 on theBenchmark for (2822ds/58680Mi) % 217.06/30.93 % (4118361)Instruction limit reached! % 217.06/30.93 % (4118361)------------------------------ % 217.06/30.93 % (4118361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.06/30.93 % (4118361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.06/30.93 % (4118361)CaDiCaL version: 2.1.3 % 217.06/30.93 % (4118361)Termination reason: Instruction limit % 217.06/30.93 % (4118361)Termination phase: Saturation % 217.06/30.93 % (4118361)Time elapsed: 1.834 s % 217.06/30.93 % (4118361)Peak memory usage: 17 MB % 217.06/30.93 % (4118361)Instructions burned: 7546 (million) % 217.06/30.93 % (4118382)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3507921570:i=10422:rtra=on_2820 on theBenchmark for (2820ds/10422Mi) % 217.06/30.93 % (4118281)Instruction limit reached! % 217.06/30.93 % (4118281)------------------------------ % 217.06/30.93 % (4118281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.06/30.93 % (4118281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.06/30.93 % (4118281)CaDiCaL version: 2.1.3 % 217.06/30.93 % (4118281)Termination reason: Instruction limit % 217.06/30.93 % (4118281)Termination phase: Saturation % 217.06/30.93 % (4118281)Time elapsed: 11.065 s % 217.06/30.93 % (4118281)Peak memory usage: 20 MB % 217.06/30.93 % (4118281)Instructions burned: 53298 (million) % 217.06/30.93 % (4118385)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=148783066:i=10994:nm=2:rtra=on_2814 on theBenchmark for (2814ds/10994Mi) % 217.06/30.93 % Detected minimum model sizes of [1] % 217.06/30.93 % Detected maximum model sizes of [2] % 217.06/30.93 % fmb_start_size (= 17) larger than a detected sort maximum size! % 217.06/30.93 % (4118385)Refutation not found, incomplete strategy % 217.06/30.93 % (4118385)------------------------------ % 217.06/30.93 % (4118385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118385)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118385)Termination reason: Refutation not found, incomplete strategy % 220.37/31.41 % (4118385)Time elapsed: 0.001 s % 220.37/31.41 % (4118385)Peak memory usage: 10 MB % 220.37/31.41 % (4118385)Instructions burned: 2 (million) % 220.37/31.41 % (4118385)------------------------------ % 220.37/31.41 % (4118385)------------------------------ % 220.37/31.41 % (4118387)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=314569295:fmbsr=2:i=92664:rtra=on_2814 on theBenchmark for (2814ds/92664Mi) % 220.37/31.41 % Detected minimum model sizes of [1] % 220.37/31.41 % Detected maximum model sizes of [3] % 220.37/31.41 % fmb_start_size (= 15) larger than a detected sort maximum size! % 220.37/31.41 % (4118387)Refutation not found, incomplete strategy % 220.37/31.41 % (4118387)------------------------------ % 220.37/31.41 % (4118387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118387)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118387)Termination reason: Refutation not found, incomplete strategy % 220.37/31.41 % (4118387)Time elapsed: 0.001 s % 220.37/31.41 % (4118387)Peak memory usage: 10 MB % 220.37/31.41 % (4118387)Instructions burned: 2 (million) % 220.37/31.41 % (4118387)------------------------------ % 220.37/31.41 % (4118387)------------------------------ % 220.37/31.41 % (4118389)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=1299737872:i=28142:rtra=on_2814 on theBenchmark for (2814ds/28142Mi) % 220.37/31.41 % Detected minimum model sizes of [1] % 220.37/31.41 % Detected maximum model sizes of [2] % 220.37/31.41 % fmb_start_size (= 12) larger than a detected sort maximum size! % 220.37/31.41 % (4118389)Refutation not found, incomplete strategy % 220.37/31.41 % (4118389)------------------------------ % 220.37/31.41 % (4118389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118389)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118389)Termination reason: Refutation not found, incomplete strategy % 220.37/31.41 % (4118389)Time elapsed: 0.001 s % 220.37/31.41 % (4118389)Peak memory usage: 10 MB % 220.37/31.41 % (4118389)Instructions burned: 2 (million) % 220.37/31.41 % (4118389)------------------------------ % 220.37/31.41 % (4118389)------------------------------ % 220.37/31.41 % (4118391)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3378822005:i=45130:add=on:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/45130Mi) % 220.37/31.41 % (4118377)Instruction limit reached! % 220.37/31.41 % (4118377)------------------------------ % 220.37/31.41 % (4118377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118377)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118377)Termination reason: Instruction limit % 220.37/31.41 % (4118377)Termination phase: Saturation % 220.37/31.41 % (4118377)Time elapsed: 1.909 s % 220.37/31.41 % (4118377)Peak memory usage: 14 MB % 220.37/31.41 % (4118377)Instructions burned: 9187 (million) % 220.37/31.41 % (4118393)ott+4_1_sil=16000:si=on:sp=arity:gs=on:random_seed=2727373115:i=16346:av=off:rtra=on_2804 on theBenchmark for (2804ds/16346Mi) % 220.37/31.41 % (4118382)Instruction limit reached! % 220.37/31.41 % (4118382)------------------------------ % 220.37/31.41 % (4118382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118382)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118382)Termination reason: Instruction limit % 220.37/31.41 % (4118382)Termination phase: Saturation % 220.37/31.41 % (4118382)Time elapsed: 2.212 s % 220.37/31.41 % (4118382)Peak memory usage: 17 MB % 220.37/31.41 % (4118382)Instructions burned: 10425 (million) % 220.37/31.41 % (4118395)dis+10_16:1_sil=16000:si=on:random_seed=3125812559:i=18310:fsr=off:rtra=on_2798 on theBenchmark for (2798ds/18310Mi) % 220.37/31.41 % (4118393)Instruction limit reached! % 220.37/31.41 % (4118393)------------------------------ % 220.37/31.41 % (4118393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.41 % (4118393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.41 % (4118393)CaDiCaL version: 2.1.3 % 220.37/31.41 % (4118393)Termination reason: Instruction limit % 220.37/31.45 % (4118393)Termination phase: Saturation % 220.37/31.45 % (4118393)Time elapsed: 3.305 s % 220.37/31.45 % (4118393)Peak memory usage: 12 MB % 220.37/31.45 % (4118393)Instructions burned: 16350 (million) % 220.37/31.45 % (4118397)ott-3_8_sil=64000:si=on:random_seed=3694445908:i=40278:bs=on:rtra=on_2771 on theBenchmark for (2771ds/40278Mi) % 220.37/31.45 % (4118395)Instruction limit reached! % 220.37/31.45 % (4118395)------------------------------ % 220.37/31.45 % (4118395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.45 % (4118395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.45 % (4118395)CaDiCaL version: 2.1.3 % 220.37/31.45 % (4118395)Termination reason: Instruction limit % 220.37/31.45 % (4118395)Termination phase: Saturation % 220.37/31.45 % (4118395)Time elapsed: 3.406 s % 220.37/31.45 % (4118395)Peak memory usage: 18 MB % 220.37/31.45 % (4118395)Instructions burned: 18311 (million) % 220.37/31.45 % (4118399)fmb+10_1_sil=64000:tgt=ground:sas=cadical:si=on:bce=on:fmbss=9:random_seed=4232426975:fmbsr=2:i=65152:rtra=on_2764 on theBenchmark for (2764ds/65152Mi) % 220.37/31.45 % Detected minimum model sizes of [1] % 220.37/31.45 % Detected maximum model sizes of [2] % 220.37/31.45 % fmb_start_size (= 9) larger than a detected sort maximum size! % 220.37/31.45 % (4118399)Refutation not found, incomplete strategy % 220.37/31.45 % (4118399)------------------------------ % 220.37/31.45 % (4118399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.45 % (4118399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.45 % (4118399)CaDiCaL version: 2.1.3 % 220.37/31.45 % (4118399)Termination reason: Refutation not found, incomplete strategy % 220.37/31.45 % (4118399)Time elapsed: 0.001 s % 220.37/31.45 % (4118399)Peak memory usage: 10 MB % 220.37/31.45 % (4118399)Instructions burned: 2 (million) % 220.37/31.45 % (4118399)------------------------------ % 220.37/31.45 % (4118399)------------------------------ % 220.37/31.45 % (4118401)ott+10_8:1_sil=16000:si=on:sp=arity:gs=on:random_seed=3934616609:i=22808:rtra=on_2763 on theBenchmark for (2763ds/22808Mi) % 220.37/31.45 % (4118391)Instruction limit reached! % 220.37/31.45 % (4118391)------------------------------ % 220.37/31.45 % (4118391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.45 % (4118391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.45 % (4118391)CaDiCaL version: 2.1.3 % 220.37/31.45 % (4118391)Termination reason: Instruction limit % 220.37/31.45 % (4118391)Termination phase: Saturation % 220.37/31.45 % (4118391)Time elapsed: 6.651 s % 220.37/31.45 % (4118391)Peak memory usage: 12 MB % 220.37/31.45 % (4118391)Instructions burned: 45134 (million) % 220.37/31.45 % (4118403)ott-11_1_sil=16000:si=on:alpa=false:sac=on:random_seed=2994836417:i=28268:rtra=on_2747 on theBenchmark for (2747ds/28268Mi) % 220.37/31.45 % (4118403)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 220.37/31.45 % (4118401)Instruction limit reached! % 220.37/31.45 % (4118401)------------------------------ % 220.37/31.45 % (4118401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.45 % (4118401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.45 % (4118401)CaDiCaL version: 2.1.3 % 220.37/31.45 % (4118401)Termination reason: Instruction limit % 220.37/31.45 % (4118401)Termination phase: Saturation % 220.37/31.45 % (4118401)Time elapsed: 4.245 s % 220.37/31.45 % (4118401)Peak memory usage: 13 MB % 220.37/31.45 % (4118401)Instructions burned: 22816 (million) % 220.37/31.45 % (4118406)dis+33_16_sil=32000:si=on:sac=on:random_seed=1909171743:i=31702:nm=0:rtra=on_2721 on theBenchmark for (2721ds/31702Mi) % 220.37/31.45 % (4118379)Instruction limit reached! % 220.37/31.45 % (4118379)------------------------------ % 220.37/31.45 % (4118379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.37/31.45 % (4118379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/31.45 % (4118379)CaDiCaL version: 2.1.3 % 220.37/31.45 % (4118379)Termination reason: Instruction limit % 220.37/31.45 % (4118379)Termination phase: Saturation % 220.37/31.45 % (4118379)Time elapsed: 12.029 s % 220.37/31.45 % (4118379)Peak memory usage: 18 MB % 220.37/31.45 % (4118379)Instructions burned: 58685 (million) % 220.37/31.45 % (4118409)dis+4_1024_sil=32000:si=on:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=709346782:avsq=on:i=35254:add=on:rtra=on:amm=off_2701 on theBenchmark for (2701ds/35254Mi) % 220.37/31.45 % (4118173)Instruction limit reached! % 220.37/31.45 % (4118173)------------------------------ % 220.37/31.45 % (4118173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.19/38.38 % (4118173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.19/38.38 % (4118173)CaDiCaL version: 2.1.3 % 269.19/38.38 % (4118173)Termination reason: Instruction limit % 269.19/38.38 % (4118173)Termination phase: Saturation % 269.19/38.38 % (4118173)Time elapsed: 30.753 s % 269.19/38.38 % (4118173)Peak memory usage: 43 MB % 269.19/38.38 % (4118173)Instructions burned: 135533 (million) % 269.19/38.38 % (4118412)ott+10_64_anc=all:sil=128000:sas=cadical:si=on:bsr=unit_only:nwc=1:cn=on:random_seed=483629550:s2a=on:i=106590:rtra=on_2692 on theBenchmark for (2692ds/106590Mi) % 269.19/38.38 % (4118397)Instruction limit reached! % 269.19/38.38 % (4118397)------------------------------ % 269.19/38.38 % (4118397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.19/38.38 % (4118397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.19/38.38 % (4118397)CaDiCaL version: 2.1.3 % 269.19/38.38 % (4118397)Termination reason: Instruction limit % 269.19/38.38 % (4118397)Termination phase: Saturation % 269.19/38.38 % (4118397)Time elapsed: 8.124 s % 269.19/38.38 % (4118397)Peak memory usage: 16 MB % 269.19/38.38 % (4118397)Instructions burned: 40279 (million) % 269.19/38.38 % (4118414)fmb+10_1_sil=32000:sas=cadical:si=on:fmbss=16:random_seed=832309694:i=53714:ins=20:rtra=on_2689 on theBenchmark for (2689ds/53714Mi) % 269.19/38.38 % Detected minimum model sizes of [1] % 269.19/38.38 % Detected maximum model sizes of [2] % 269.19/38.38 % fmb_start_size (= 16) larger than a detected sort maximum size! % 269.19/38.38 % (4118414)Refutation not found, incomplete strategy % 269.19/38.38 % (4118414)------------------------------ % 269.19/38.38 % (4118414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.19/38.38 % (4118414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.19/38.38 % (4118414)CaDiCaL version: 2.1.3 % 269.19/38.38 % (4118414)Termination reason: Refutation not found, incomplete strategy % 269.19/38.38 % (4118414)Time elapsed: 0.001 s % 269.19/38.38 % (4118414)Peak memory usage: 10 MB % 269.19/38.38 % (4118414)Instructions burned: 2 (million) % 269.19/38.38 % (4118414)------------------------------ % 269.19/38.38 % (4118414)------------------------------ % 269.19/38.38 % (4118416)ott+10_1_sil=64000:plsq=on:plsqc=4:si=on:bsr=unit_only:gs=on:random_seed=2766306182:i=56240:bs=on:fsr=off:rtra=on_2689 on theBenchmark for (2689ds/56240Mi) % 269.19/38.38 % (4118403)Instruction limit reached! % 269.19/38.38 % (4118403)------------------------------ % 269.19/38.38 % (4118403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.19/38.38 % (4118403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.19/38.38 % (4118403)CaDiCaL version: 2.1.3 % 269.19/38.38 % (4118403)Termination reason: Instruction limit % 269.19/38.38 % (4118403)Termination phase: Saturation % 269.19/38.38 % (4118403)Time elapsed: 5.964 s % 269.19/38.38 % (4118403)Peak memory usage: 13 MB % 269.19/38.38 % (4118403)Instructions burned: 28271 (million) % 269.19/38.38 % (4118418)fmb+10_1_sil=256000:si=on:fmbss=7:random_seed=2902168401:fmbsr=1.6:i=364590:rtra=on_2687 on theBenchmark for (2687ds/364590Mi) % 269.19/38.38 % Detected minimum model sizes of [1] % 269.19/38.38 % Detected maximum model sizes of [2] % 269.19/38.38 % fmb_start_size (= 7) larger than a detected sort maximum size! % 269.19/38.38 % (4118418)Refutation not found, incomplete strategy % 269.19/38.38 % (4118418)------------------------------ % 269.19/38.38 % (4118418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.19/38.38 % (4118418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.19/38.38 % (4118418)CaDiCaL version: 2.1.3 % 269.19/38.38 % (4118418)Termination reason: Refutation not found, incomplete strategy % 269.19/38.38 % (4118418)Time elapsed: 0.001 s % 269.19/38.38 % (4118418)Peak memory usage: 10 MB % 269.19/38.38 % (4118418)Instructions burned: 2 (million) % 269.19/38.38 % (4118418)------------------------------ % 269.19/38.38 % (4118418)------------------------------ % 269.19/38.38 % (4118420)fmb+10_1_sil=128000:si=on:fmbss=21:newcnf=on:random_seed=1925427743:i=89250:rtra=on:gsp=on_2687 on theBenchmark for (2687ds/89250Mi) % 269.19/38.38 % (4118420)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 269.19/38.38 % (4118420)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 269.19/38.38 % Detected minimum model sizes of [1] % 269.19/38.38 % Detected maximum model sizes of [2] % 269.19/38.38 % fmb_start_size (= 21) larger than a detected sort maximum size! % 269.19/38.38 % (4118420)Refutation not found, incomplete strategy % 278.74/39.77 % (4118420)------------------------------ % 278.74/39.77 % (4118420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.74/39.77 % (4118420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.74/39.77 % (4118420)CaDiCaL version: 2.1.3 % 278.74/39.77 % (4118420)Termination reason: Refutation not found, incomplete strategy % 278.74/39.77 % (4118420)Time elapsed: 0.0000 s % 278.74/39.77 % (4118420)Peak memory usage: 10 MB % 278.74/39.77 % (4118420)Instructions burned: 2 (million) % 278.74/39.77 % (4118420)------------------------------ % 278.74/39.77 % (4118420)------------------------------ % 278.74/39.77 % (4118422)fmb+10_1_sil=256000:sas=cadical:si=on:fmbss=15:random_seed=3495197912:i=321010:rtra=on_2687 on theBenchmark for (2687ds/321010Mi) % 278.74/39.77 % Detected minimum model sizes of [1] % 278.74/39.77 % Detected maximum model sizes of [2] % 278.74/39.77 % fmb_start_size (= 15) larger than a detected sort maximum size! % 278.74/39.77 % (4118422)Refutation not found, incomplete strategy % 278.74/39.77 % (4118422)------------------------------ % 278.74/39.77 % (4118422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.74/39.77 % (4118422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.74/39.77 % (4118422)CaDiCaL version: 2.1.3 % 278.74/39.77 % (4118422)Termination reason: Refutation not found, incomplete strategy % 278.74/39.77 % (4118422)Time elapsed: 0.0000 s % 278.74/39.77 % (4118422)Peak memory usage: 10 MB % 278.74/39.77 % (4118422)Instructions burned: 2 (million) % 278.74/39.77 % (4118422)------------------------------ % 278.74/39.77 % (4118422)------------------------------ % 278.74/39.77 % (4118424)fmb+10_1_sil=256000:tgt=full:si=on:fmbss=10:random_seed=445402180:fmbsr=1.3:i=451458:rtra=on_2687 on theBenchmark for (2687ds/451458Mi) % 278.74/39.77 % Detected minimum model sizes of [1] % 278.74/39.77 % Detected maximum model sizes of [2] % 278.74/39.77 % fmb_start_size (= 10) larger than a detected sort maximum size! % 278.74/39.77 % (4118424)Refutation not found, incomplete strategy % 278.74/39.77 % (4118424)------------------------------ % 278.74/39.77 % (4118424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.74/39.77 % (4118424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.74/39.77 % (4118424)CaDiCaL version: 2.1.3 % 278.74/39.77 % (4118424)Termination reason: Refutation not found, incomplete strategy % 278.74/39.77 % (4118424)Time elapsed: 0.001 s % 278.74/39.77 % (4118424)Peak memory usage: 10 MB % 278.74/39.77 % (4118424)Instructions burned: 2 (million) % 278.74/39.77 % (4118424)------------------------------ % 278.74/39.77 % (4118424)------------------------------ % 278.74/39.77 % (4118426)fmb+10_1_sil=256000:tgt=full:sas=cadical:si=on:fmbss=10:random_seed=148590066:fmbsr=2:i=370048:ins=7:rtra=on_2687 on theBenchmark for (2687ds/370048Mi) % 278.74/39.77 % Detected minimum model sizes of [1] % 278.74/39.77 % Detected maximum model sizes of [2] % 278.74/39.77 % fmb_start_size (= 10) larger than a detected sort maximum size! % 278.74/39.77 % (4118426)Refutation not found, incomplete strategy % 278.74/39.77 % (4118426)------------------------------ % 278.74/39.77 % (4118426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.74/39.77 % (4118426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.74/39.77 % (4118426)CaDiCaL version: 2.1.3 % 278.74/39.77 % (4118426)Termination reason: Refutation not found, incomplete strategy % 278.74/39.77 % (4118426)Time elapsed: 0.0000 s % 278.74/39.77 % (4118426)Peak memory usage: 10 MB % 278.74/39.77 % (4118426)Instructions burned: 2 (million) % 278.74/39.77 % (4118426)------------------------------ % 278.74/39.77 % (4118426)------------------------------ % 278.74/39.77 % (4118428)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=838142704:rtra=on_2686 on theBenchmark for (2686ds/0Mi) % 278.74/39.77 % Detected minimum model sizes of [1] % 278.74/39.77 % Detected maximum model sizes of [2] % 278.74/39.77 % TRYING [1] % 278.74/39.77 % TRYING [2] % 278.74/39.77 % Finite Model Found! % 278.74/39.77 % SZS status Satisfiable for theBenchmark % 278.74/39.77 % (4118428)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 278.74/39.77 % (4118428)------------------------------ % 278.74/39.77 % (4118428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.74/39.77 % (4118428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.74/39.77 % (4118428)CaDiCaL version: 2.1.3 % 278.74/39.77 % (4118428)Termination reason: Unknown % 278.74/39.77 % (4118428)Termination phase: Finite model building constraint generation % 278.74/39.77 % (4118428)Time elapsed: 0.001 s % 278.74/39.77 % (4118428)Peak memory usage: 11 MB % 278.74/39.77 % (4118428)Instructions burned: 2 (million) % 286.10/40.72 % (4118430)% WARNING: option uhcvi not known. % 286.10/40.72 % (4118430)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3221066128:i=542124:add=off:rtra=on:rawr=on_2686 on theBenchmark for (2686ds/542124Mi) % 286.10/40.72 % (4118430)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 286.10/40.72 % (4118430)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 286.10/40.72 % (4118406)Instruction limit reached! % 286.10/40.72 % (4118406)------------------------------ % 286.10/40.72 % (4118406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.10/40.72 % (4118406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.10/40.72 % (4118406)CaDiCaL version: 2.1.3 % 286.10/40.72 % (4118406)Termination reason: Instruction limit % 286.10/40.72 % (4118406)Termination phase: Saturation % 286.10/40.72 % (4118406)Time elapsed: 6.624 s % 286.10/40.72 % (4118406)Peak memory usage: 16 MB % 286.10/40.72 % (4118406)Instructions burned: 31703 (million) % 286.10/40.72 % (4118585)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2635010547:i=352096:add=on:rtra=on:rawr=on_2654 on theBenchmark for (2654ds/352096Mi) % 286.10/40.72 % (4118409)Instruction limit reached! % 286.10/40.72 % (4118409)------------------------------ % 286.10/40.72 % (4118409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.10/40.72 % (4118409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.10/40.72 % (4118409)CaDiCaL version: 2.1.3 % 286.10/40.72 % (4118409)Termination reason: Instruction limit % 286.10/40.72 % (4118409)Termination phase: Saturation % 286.10/40.72 % (4118409)Time elapsed: 7.924 s % 286.10/40.72 % (4118409)Peak memory usage: 28 MB % 286.10/40.72 % (4118409)Instructions burned: 35255 (million) % 286.10/40.72 % (4118587)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4030766776:i=412:fgj=on:rtra=on_2622 on theBenchmark for (2622ds/412Mi) % 286.10/40.72 % (4118587)Instruction limit reached! % 286.10/40.72 % (4118587)------------------------------ % 286.10/40.72 % (4118587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.10/40.72 % (4118587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.10/40.72 % (4118587)CaDiCaL version: 2.1.3 % 286.10/40.72 % (4118587)Termination reason: Instruction limit % 286.10/40.72 % (4118587)Termination phase: Saturation % 286.10/40.72 % (4118587)Time elapsed: 0.095 s % 286.10/40.72 % (4118587)Peak memory usage: 12 MB % 286.10/40.72 % (4118587)Instructions burned: 415 (million) % 286.10/40.72 % (4118589)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2930413853:i=464:rtra=on_2621 on theBenchmark for (2621ds/464Mi) % 286.10/40.72 % (4118589)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 286.10/40.72 % (4118589)Instruction limit reached! % 286.10/40.72 % (4118589)------------------------------ % 286.10/40.72 % (4118589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.10/40.72 % (4118589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.10/40.72 % (4118589)CaDiCaL version: 2.1.3 % 286.10/40.72 % (4118589)Termination reason: Instruction limit % 286.10/40.72 % (4118589)Termination phase: Saturation % 286.10/40.72 % (4118589)Time elapsed: 0.098 s % 286.10/40.72 % (4118589)Peak memory usage: 12 MB % 286.10/40.72 % (4118589)Instructions burned: 466 (million) % 286.10/40.72 % (4118591)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2505004650:i=524:rtra=on_2620 on theBenchmark for (2620ds/524Mi) % 286.10/40.72 % (4118591)Instruction limit reached! % 286.10/40.72 % (4118591)------------------------------ % 286.10/40.72 % (4118591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.10/40.72 % (4118591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.10/40.72 % (4118591)CaDiCaL version: 2.1.3 % 286.10/40.72 % (4118591)Termination reason: Instruction limit % 286.10/40.72 % (4118591)Termination phase: Saturation % 286.10/40.72 % (4118591)Time elapsed: 0.113 s % 286.10/40.72 % (4118591)Peak memory usage: 12 MB % 286.10/40.72 % (4118591)Instructions burned: 524 (million) % 286.10/40.72 % (4118593)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4074921180:i=636:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2618 on theBenchmark for (2618ds/636Mi) % 286.10/40.72 % (4118593)Instruction limit reached! % 286.10/40.72 % (4118593)------------------------------ % 286.10/40.72 % (4118593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118593)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118593)Termination reason: Instruction limit % 290.10/41.31 % (4118593)Termination phase: Saturation % 290.10/41.31 % (4118593)Time elapsed: 0.132 s % 290.10/41.31 % (4118593)Peak memory usage: 12 MB % 290.10/41.31 % (4118593)Instructions burned: 638 (million) % 290.10/41.31 % (4118595)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3384404695:i=2856:nm=2:rtra=on_2617 on theBenchmark for (2617ds/2856Mi) % 290.10/41.31 % Detected minimum model sizes of [1] % 290.10/41.31 % Detected maximum model sizes of [3] % 290.10/41.31 % TRYING [1] % 290.10/41.31 % TRYING [2] % 290.10/41.31 % Finite Model Found! % 290.10/41.31 % SZS status Satisfiable for theBenchmark % 290.10/41.31 % (4118595)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 290.10/41.31 % (4118595)------------------------------ % 290.10/41.31 % (4118595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118595)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118595)Termination reason: Unknown % 290.10/41.31 % (4118595)Termination phase: Finite model building constraint generation % 290.10/41.31 % (4118595)Time elapsed: 0.001 s % 290.10/41.31 % (4118595)Peak memory usage: 11 MB % 290.10/41.31 % (4118595)Instructions burned: 3 (million) % 290.10/41.31 % (4118597)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2739962829:i=524:bd=preordered:rtra=on:fsd=on_2617 on theBenchmark for (2617ds/524Mi) % 290.10/41.31 % (4118597)Instruction limit reached! % 290.10/41.31 % (4118597)------------------------------ % 290.10/41.31 % (4118597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118597)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118597)Termination reason: Instruction limit % 290.10/41.31 % (4118597)Termination phase: Saturation % 290.10/41.31 % (4118597)Time elapsed: 0.113 s % 290.10/41.31 % (4118597)Peak memory usage: 12 MB % 290.10/41.31 % (4118597)Instructions burned: 527 (million) % 290.10/41.31 % (4118599)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=380211986:i=2736:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2616 on theBenchmark for (2616ds/2736Mi) % 290.10/41.31 % (4118599)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 290.10/41.31 % (4118599)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 290.10/41.31 % (4118599)Instruction limit reached! % 290.10/41.31 % (4118599)------------------------------ % 290.10/41.31 % (4118599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118599)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118599)Termination reason: Instruction limit % 290.10/41.31 % (4118599)Termination phase: Saturation % 290.10/41.31 % (4118599)Time elapsed: 0.629 s % 290.10/41.31 % (4118599)Peak memory usage: 14 MB % 290.10/41.31 % (4118599)Instructions burned: 2741 (million) % 290.10/41.31 % (4118601)ott-21_1_sil=16000:si=on:fs=off:random_seed=3253167868:i=720:av=off:fsr=off:rtra=on_2609 on theBenchmark for (2609ds/720Mi) % 290.10/41.31 % (4118601)Instruction limit reached! % 290.10/41.31 % (4118601)------------------------------ % 290.10/41.31 % (4118601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118601)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118601)Termination reason: Instruction limit % 290.10/41.31 % (4118601)Termination phase: Saturation % 290.10/41.31 % (4118601)Time elapsed: 0.167 s % 290.10/41.31 % (4118601)Peak memory usage: 17 MB % 290.10/41.31 % (4118601)Instructions burned: 721 (million) % 290.10/41.31 % (4118603)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3367927477:i=1908:bd=all:rtra=on_2607 on theBenchmark for (2607ds/1908Mi) % 290.10/41.31 % (4118603)Instruction limit reached! % 290.10/41.31 % (4118603)------------------------------ % 290.10/41.31 % (4118603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.10/41.31 % (4118603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.10/41.31 % (4118603)CaDiCaL version: 2.1.3 % 290.10/41.31 % (4118603)Termination reason: Instruction limit % 290.10/41.31 % (4118603)Termination phase: Saturation % 297.20/42.30 % (4118603)Time elapsed: 0.417 s % 297.20/42.30 % (4118603)Peak memory usage: 12 MB % 297.20/42.30 % (4118603)Instructions burned: 1910 (million) % 297.20/42.30 % (4118605)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4199582075:fmbsr=1.3:i=3460:ins=25:rtra=on_2603 on theBenchmark for (2603ds/3460Mi) % 297.20/42.30 % Detected minimum model sizes of [1] % 297.20/42.30 % Detected maximum model sizes of [2] % 297.20/42.30 % TRYING [1] % 297.20/42.30 % TRYING [2] % 297.20/42.30 % Finite Model Found! % 297.20/42.30 % SZS status Satisfiable for theBenchmark % 297.20/42.30 % (4118605)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.20/42.30 % (4118605)------------------------------ % 297.20/42.30 % (4118605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.20/42.30 % (4118605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.20/42.30 % (4118605)CaDiCaL version: 2.1.3 % 297.20/42.30 % (4118605)Termination reason: Unknown % 297.20/42.30 % (4118605)Termination phase: Finite model building constraint generation % 297.20/42.30 % (4118605)Time elapsed: 0.001 s % 297.20/42.30 % (4118605)Peak memory usage: 10 MB % 297.20/42.30 % (4118605)Instructions burned: 2 (million) % 297.20/42.30 % (4118607)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2371589494:i=4716:rtra=on_2603 on theBenchmark for (2603ds/4716Mi) % 297.20/42.30 % (4118305)Instruction limit reached! % 297.20/42.30 % (4118305)------------------------------ % 297.20/42.30 % (4118305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.20/42.30 % (4118305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.20/42.30 % (4118305)CaDiCaL version: 2.1.3 % 297.20/42.30 % (4118305)Termination reason: Instruction limit % 297.20/42.30 % (4118305)Termination phase: Saturation % 297.20/42.30 % (4118305)Time elapsed: 27.812 s % 297.20/42.30 % (4118305)Peak memory usage: 13 MB % 297.20/42.30 % (4118305)Instructions burned: 176050 (million) % 297.20/42.30 % (4118609)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=478086084:i=3556:ins=1:rtra=on_2600 on theBenchmark for (2600ds/3556Mi) % 297.20/42.30 % Exception at run slice level % 297.20/42.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 297.20/42.30 % (4118611)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=1315012985:avsq=on:s2a=on:i=2768:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2600 on theBenchmark for (2600ds/2768Mi) % 297.20/42.30 % (4118611)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 297.20/42.30 % (4118611)Instruction limit reached! % 297.20/42.30 % (4118611)------------------------------ % 297.20/42.30 % (4118611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.20/42.30 % (4118611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.20/42.30 % (4118611)CaDiCaL version: 2.1.3 % 297.20/42.30 % (4118611)Termination reason: Instruction limit % 297.20/42.30 % (4118611)Termination phase: Saturation % 297.20/42.30 % (4118611)Time elapsed: 0.573 s % 297.20/42.30 % (4118611)Peak memory usage: 13 MB % 297.20/42.30 % (4118611)Instructions burned: 2770 (million) % 297.20/42.30 % (4118613)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=523545476:i=3516:kws=inv_precedence:fsr=off:rtra=on_2594 on theBenchmark for (2594ds/3516Mi) % 297.20/42.30 % (4118613)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 297.20/42.30 % (4118607)Instruction limit reached! % 297.20/42.30 % (4118607)------------------------------ % 297.20/42.30 % (4118607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.20/42.30 % (4118607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.20/42.30 % (4118607)CaDiCaL version: 2.1.3 % 297.20/42.30 % (4118607)Termination reason: Instruction limit % 297.20/42.30 % (4118607)Termination phase: Saturation % 297.20/42.30 % (4118607)Time elapsed: 0.914 s % 297.20/42.30 % (4118607)Peak memory usage: 12 MB % 297.20/42.30 % (4118607)Instructions burned: 4718 (million) % 297.20/42.30 % (4118615)fmb+10_1_sil=64000:si=on:random_seed=1569660159:i=88244:nm=2:rtra=on:gsp=on_2594 on theBenchmark for (2594ds/88244Mi) % 297.20/42.30 % (4118615)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 297.20/42.30 % Detected minimum model sizes of [1] % 297.20/42.30 % Detected maximum model sizes of [2] % 297.20/42.30 % TRYING [1] % 297.20/42.30 % TRYING [2] % 297.20/42.30 % Finite Model Found! % 297.20/42.30 % SZS status Satisfiable for theBenchmark % 300.24/42.92 % (4118615)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.24/42.92 % (4118615)------------------------------ % 300.24/42.92 % (4118615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.92 % (4118615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.92 % (4118615)CaDiCaL version: 2.1.3 % 300.24/42.92 % (4118615)Termination reason: Unknown % 300.24/42.92 % (4118615)Termination phase: Finite model building constraint generation % 300.24/42.92 % (4118615)Time elapsed: 0.001 s % 300.24/42.92 % (4118615)Peak memory usage: 10 MB % 300.24/42.92 % (4118615)Instructions burned: 2 (million) % 300.24/42.92 % (4118617)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2675603498:i=38060:nm=5:rtra=on_2594 on theBenchmark for (2594ds/38060Mi) % 300.24/42.92 % Detected minimum model sizes of [1] % 300.24/42.92 % Detected maximum model sizes of [2] % 300.24/42.92 % fmb_start_size (= 20) larger than a detected sort maximum size! % 300.24/42.92 % (4118617)Refutation not found, incomplete strategy % 300.24/42.92 % (4118617)------------------------------ % 300.24/42.92 % (4118617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.92 % (4118617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.92 % (4118617)CaDiCaL version: 2.1.3 % 300.24/42.92 % (4118617)Termination reason: Refutation not found, incomplete strategy % 300.24/42.92 % (4118617)Time elapsed: 0.001 s % 300.24/42.92 % (4118617)Peak memory usage: 11 MB % 300.24/42.92 % (4118617)Instructions burned: 2 (million) % 300.24/42.92 % (4118617)------------------------------ % 300.24/42.92 % (4118617)------------------------------ % 300.24/42.92 % (4118619)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2195471270:fmbsr=1.7:i=3680:rtra=on_2594 on theBenchmark for (2594ds/3680Mi) % 300.24/42.92 % Detected minimum model sizes of [1] % 300.24/42.92 % Detected maximum model sizes of [2] % 300.24/42.92 % fmb_start_size (= 8) larger than a detected sort maximum size! % 300.24/42.92 % (4118619)Refutation not found, incomplete strategy % 300.24/42.92 % (4118619)------------------------------ % 300.24/42.92 % (4118619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.92 % (4118619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.92 % (4118619)CaDiCaL version: 2.1.3 % 300.24/42.92 % (4118619)Termination reason: Refutation not found, incomplete strategy % 300.24/42.92 % (4118619)Time elapsed: 0.001 s % 300.24/42.92 % (4118619)Peak memory usage: 10 MB % 300.24/42.92 % (4118619)Instructions burned: 2 (million) % 300.24/42.92 % (4118619)------------------------------ % 300.24/42.92 % (4118619)------------------------------ % 300.24/42.92 % (4118621)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2945507041:i=20524:rtra=on_2593 on theBenchmark for (2593ds/20524Mi) % 300.24/42.92 % (4118621)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 300.24/42.92 % (4118416)Instruction limit reached! % 300.24/42.92 % (4118416)------------------------------ % 300.24/42.92 % (4118416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.92 % (4118416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.92 % (4118416)CaDiCaL version: 2.1.3 % 300.24/42.92 % (4118416)Termination reason: Instruction limit % 300.24/42.92 % (4118416)Termination phase: Saturation % 300.24/42.92 % (4118416)Time elapsed: 9.828 s % 300.24/42.92 % (4118416)Peak memory usage: 18 MB % 300.24/42.92 % (4118416)Instructions burned: 56244 (million) % 300.24/42.92 % (4118623)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2748294881:i=5888:ins=7:rtra=on:fdi=8:gsp=on_2591 on theBenchmark for (2591ds/5888Mi) % 300.24/42.92 % (4118623)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.24/42.92 % (4118623)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 300.24/42.92 % (4118613)Instruction limit reached! % 300.24/42.92 % (4118613)------------------------------ % 300.24/42.92 % (4118613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.92 % (4118613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.92 % (4118613)CaDiCaL version: 2.1.3 % 300.24/42.92 % (4118613)Termination reason: Instruction limit % 300.24/42.92 % (4118613)Termination phase: Saturation % 300.24/42.92 % (4118613)Time elapsed: 0.644 s % 300.24/42.92 % (4118613)Peak memory usage: 12 MB % 300.24/42.92 % (4118613)Instructions burned: 3522 (million) % 300.24/42.92 % (4118625)fmb+1 % 300.24/42.92 Terminated % 300.24/42.92 % Vampire exiting %------------------------------------------------------------------------------