%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SEV440^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 : n017.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:39:30 AM UTC 2026 % Result : Satisfiable 1.71s 0.55s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SEV440^1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n017.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Tue Sep 29 15:42:22 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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.71/0.55 % (490138)Will run a generic schedule for satisfiability detection. % 1.71/0.55 % (490146)dis+10_1_sil=32000:sp=arity:random_seed=339464656:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.71/0.55 % (490144)% WARNING: option uhcvi not known. % 1.71/0.55 % (490144)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4028212895:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.71/0.55 % (490148)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4250437990:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.71/0.55 % (490149)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2778858789:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.71/0.55 % (490145)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3307295335:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.71/0.55 % (490144)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.71/0.55 % (490144)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 1.71/0.55 % (490147)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3500441218:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.71/0.55 % (490147)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.71/0.55 % (490146)Instruction limit reached! % 1.71/0.55 % (490146)------------------------------ % 1.71/0.55 % (490146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.55 % (490146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.55 % (490146)CaDiCaL version: 2.1.3 % 1.71/0.55 % (490146)Termination reason: Instruction limit % 1.71/0.55 % (490146)Termination phase: Saturation % 1.71/0.55 % (490146)Time elapsed: 0.025 s % 1.71/0.55 % (490146)Peak memory usage: 11 MB % 1.71/0.55 % (490146)Instructions burned: 106 (million) % 1.71/0.55 % (490143)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3736570228_2999 on theBenchmark for (2999ds/0Mi) % 1.71/0.55 % Detected minimum model sizes of [1] % 1.71/0.55 % Detected maximum model sizes of [2] % 1.71/0.55 % TRYING [1] % 1.71/0.55 % TRYING [2] % 1.71/0.55 % Finite Model Found! % 1.71/0.55 % SZS status Satisfiable for theBenchmark % 1.71/0.55 % (490143)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/0.55 % (490143)------------------------------ % 1.71/0.55 % (490143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.55 % (490143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.55 % (490143)CaDiCaL version: 2.1.3 % 1.71/0.55 % (490143)Termination reason: Unknown % 1.71/0.55 % (490143)Termination phase: Finite model building constraint generation % 1.71/0.55 % (490143)Time elapsed: 0.007 s % 1.71/0.55 % (490143)Peak memory usage: 11 MB % 1.71/0.55 % (490143)Instructions burned: 8 (million) % 1.71/0.55 % (490158)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1638291474:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 1.71/0.55 % (490157)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4254161723:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.71/0.55 % Detected minimum model sizes of [1] % 1.71/0.55 % Detected maximum model sizes of [3] % 1.71/0.55 % TRYING [1] % 1.71/0.55 % TRYING [2] % 1.71/0.55 % Finite Model Found! % 1.71/0.55 % SZS status Satisfiable for theBenchmark % 1.71/0.55 % (490157)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/0.55 % (490157)------------------------------ % 1.71/0.55 % (490157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.55 % (490157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.55 % (490157)CaDiCaL version: 2.1.3 % 1.71/0.55 % (490157)Termination reason: Unknown % 1.71/0.55 % (490157)Termination phase: Finite model building constraint generation % 1.71/0.55 % (490157)Time elapsed: 0.004 s % 1.71/0.55 % (490157)Peak memory usage: 11 MB % 1.71/0.55 % (490157)Instructions burned: 8 (million) % 1.71/0.55 % (490149)Instruction limit reached! % 1.71/0.55 % (490149)------------------------------ % 1.71/0.55 % (490149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.55 % (490149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.55 % (490149)CaDiCaL version: 2.1.3 % 1.71/0.55 % (490149)Termination reason: Instruction limit % 1.71/0.55 % (490149)Termination phase: Saturation % 1.71/0.55 % (490149)Time elapsed: 0.063 s % 3.49/0.87 % (490149)Peak memory usage: 12 MB % 3.49/0.87 % (490149)Instructions burned: 160 (million) % 3.49/0.87 % (490148)Instruction limit reached! % 3.49/0.87 % (490148)------------------------------ % 3.49/0.87 % (490148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.87 % (490148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.87 % (490148)CaDiCaL version: 2.1.3 % 3.49/0.87 % (490148)Termination reason: Instruction limit % 3.49/0.87 % (490148)Termination phase: Saturation % 3.49/0.87 % (490148)Time elapsed: 0.068 s % 3.49/0.87 % (490148)Peak memory usage: 11 MB % 3.49/0.87 % (490148)Instructions burned: 133 (million) % 3.49/0.87 % (490158)Instruction limit reached! % 3.49/0.87 % (490158)------------------------------ % 3.49/0.87 % (490158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.87 % (490158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.87 % (490158)CaDiCaL version: 2.1.3 % 3.49/0.87 % (490158)Termination reason: Instruction limit % 3.49/0.87 % (490158)Termination phase: Saturation % 3.49/0.87 % (490158)Time elapsed: 0.030 s % 3.49/0.87 % (490158)Peak memory usage: 12 MB % 3.49/0.87 % (490158)Instructions burned: 131 (million) % 3.49/0.87 % (490164)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1406704279:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.49/0.87 % (490147)Instruction limit reached! % 3.49/0.87 % (490147)------------------------------ % 3.49/0.87 % (490147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.87 % (490147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.87 % (490147)CaDiCaL version: 2.1.3 % 3.49/0.87 % (490147)Termination reason: Instruction limit % 3.49/0.87 % (490147)Termination phase: Saturation % 3.49/0.87 % (490147)Time elapsed: 0.071 s % 3.49/0.87 % (490147)Peak memory usage: 11 MB % 3.49/0.87 % (490147)Instructions burned: 117 (million) % 3.49/0.87 % (490161)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=662995021:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.49/0.87 % (490162)ott-21_1_sil=16000:fs=off:random_seed=2418001582:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.49/0.87 % Detected minimum model sizes of [1] % 3.49/0.87 % Detected maximum model sizes of [2] % 3.49/0.87 % TRYING [1] % 3.49/0.87 % TRYING [2] % 3.49/0.87 % Finite Model Found! % 3.49/0.87 % SZS status Satisfiable for theBenchmark % 3.49/0.87 % (490164)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.49/0.87 % (490164)------------------------------ % 3.49/0.87 % (490164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.87 % (490164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.87 % (490164)CaDiCaL version: 2.1.3 % 3.49/0.87 % (490164)Termination reason: Unknown % 3.49/0.87 % (490164)Termination phase: Finite model building constraint generation % 3.49/0.87 % (490164)Time elapsed: 0.002 s % 3.49/0.87 % (490164)Peak memory usage: 10 MB % 3.49/0.87 % (490164)Instructions burned: 8 (million) % 3.49/0.87 % (490163)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4094584937:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.49/0.87 % (490161)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.49/0.87 % (490161)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 3.49/0.87 % (490169)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=21994098:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.49/0.87 % Exception at run slice level % 3.49/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 3.49/0.87 % (490172)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=2471679291: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) % 3.49/0.87 % (490172)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.49/0.87 % (490167)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=652913602:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.49/0.87 % (490162)Instruction limit reached! % 3.49/0.87 % (490162)------------------------------ % 3.49/0.87 % (490162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.12/1.65 % (490162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.12/1.65 % (490162)CaDiCaL version: 2.1.3 % 9.12/1.65 % (490162)Termination reason: Instruction limit % 9.12/1.65 % (490162)Termination phase: Saturation % 9.12/1.65 % (490162)Time elapsed: 0.149 s % 9.12/1.65 % (490162)Peak memory usage: 13 MB % 9.12/1.65 % (490162)Instructions burned: 181 (million) % 9.12/1.65 % (490175)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2071726544:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 9.12/1.65 % (490172)Instruction limit reached! % 9.12/1.65 % (490172)------------------------------ % 9.12/1.65 % (490172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.12/1.65 % (490172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.12/1.65 % (490172)CaDiCaL version: 2.1.3 % 9.12/1.65 % (490172)Termination reason: Instruction limit % 9.12/1.65 % (490172)Termination phase: Saturation % 9.12/1.65 % (490172)Time elapsed: 0.148 s % 9.12/1.65 % (490172)Peak memory usage: 12 MB % 9.12/1.65 % (490172)Instructions burned: 692 (million) % 9.12/1.65 % (490175)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 9.12/1.65 % (490177)fmb+10_1_sil=64000:random_seed=1332565487:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 9.12/1.65 % (490177)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.12/1.65 % Detected minimum model sizes of [1] % 9.12/1.65 % Detected maximum model sizes of [2] % 9.12/1.65 % TRYING [1] % 9.12/1.65 % TRYING [2] % 9.12/1.65 % Finite Model Found! % 9.12/1.65 % SZS status Satisfiable for theBenchmark % 9.12/1.65 % (490177)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.12/1.65 % (490177)------------------------------ % 9.12/1.65 % (490177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.12/1.65 % (490177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.12/1.65 % (490177)CaDiCaL version: 2.1.3 % 9.12/1.65 % (490177)Termination reason: Unknown % 9.12/1.65 % (490177)Termination phase: Finite model building constraint generation % 9.12/1.65 % (490177)Time elapsed: 0.002 s % 9.12/1.65 % (490177)Peak memory usage: 10 MB % 9.12/1.65 % (490177)Instructions burned: 8 (million) % 9.12/1.65 % (490179)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4147762087:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 9.12/1.65 % Detected minimum model sizes of [1] % 9.12/1.65 % Detected maximum model sizes of [2] % 9.12/1.65 % fmb_start_size (= 20) larger than a detected sort maximum size! % 9.12/1.65 % (490179)Refutation not found, incomplete strategy % 9.12/1.65 % (490179)------------------------------ % 9.12/1.65 % (490179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.12/1.65 % (490179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.12/1.65 % (490179)CaDiCaL version: 2.1.3 % 9.12/1.65 % (490179)Termination reason: Refutation not found, incomplete strategy % 9.12/1.65 % (490179)Time elapsed: 0.002 s % 9.12/1.65 % (490179)Peak memory usage: 10 MB % 9.12/1.65 % (490179)Instructions burned: 8 (million) % 9.12/1.65 % (490179)------------------------------ % 9.12/1.65 % (490179)------------------------------ % 9.12/1.65 % (490181)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3366869003:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 9.12/1.65 % Detected minimum model sizes of [1] % 9.12/1.65 % Detected maximum model sizes of [2] % 9.12/1.65 % fmb_start_size (= 8) larger than a detected sort maximum size! % 9.12/1.65 % (490181)Refutation not found, incomplete strategy % 9.12/1.65 % (490181)------------------------------ % 9.12/1.65 % (490181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.12/1.65 % (490181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.12/1.65 % (490181)CaDiCaL version: 2.1.3 % 9.12/1.65 % (490181)Termination reason: Refutation not found, incomplete strategy % 9.12/1.65 % (490181)Time elapsed: 0.002 s % 9.12/1.65 % (490181)Peak memory usage: 10 MB % 9.12/1.65 % (490181)Instructions burned: 8 (million) % 9.12/1.65 % (490181)------------------------------ % 9.12/1.65 % (490181)------------------------------ % 9.12/1.65 % (490183)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=745792636:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 9.12/1.65 % (490183)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 9.12/1.65 % (490163)Instruction limit reached! % 9.12/1.65 % (490163)------------------------------ % 18.72/3.00 % (490163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.72/3.00 % (490163)CaDiCaL version: 2.1.3 % 18.72/3.00 % (490163)Termination reason: Instruction limit % 18.72/3.00 % (490163)Termination phase: Saturation % 18.72/3.00 % (490163)Time elapsed: 0.218 s % 18.72/3.00 % (490163)Peak memory usage: 12 MB % 18.72/3.00 % (490163)Instructions burned: 479 (million) % 18.72/3.00 % (490185)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3866256178:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 18.72/3.00 % (490185)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.72/3.00 % (490185)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 18.72/3.00 % (490161)Instruction limit reached! % 18.72/3.00 % (490161)------------------------------ % 18.72/3.00 % (490161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.72/3.00 % (490161)CaDiCaL version: 2.1.3 % 18.72/3.00 % (490161)Termination reason: Instruction limit % 18.72/3.00 % (490161)Termination phase: Saturation % 18.72/3.00 % (490161)Time elapsed: 0.352 s % 18.72/3.00 % (490161)Peak memory usage: 13 MB % 18.72/3.00 % (490161)Instructions burned: 685 (million) % 18.72/3.00 % (490187)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2510506743:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 18.72/3.00 % Detected minimum model sizes of [1] % 18.72/3.00 % Detected maximum model sizes of [2] % 18.72/3.00 % fmb_start_size (= 77) larger than a detected sort maximum size! % 18.72/3.00 % (490187)Refutation not found, incomplete strategy % 18.72/3.00 % (490187)------------------------------ % 18.72/3.00 % (490187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.72/3.00 % (490187)CaDiCaL version: 2.1.3 % 18.72/3.00 % (490187)Termination reason: Refutation not found, incomplete strategy % 18.72/3.00 % (490187)Time elapsed: 0.004 s % 18.72/3.00 % (490187)Peak memory usage: 10 MB % 18.72/3.00 % (490187)Instructions burned: 8 (million) % 18.72/3.00 % (490187)------------------------------ % 18.72/3.00 % (490187)------------------------------ % 18.72/3.00 % (490189)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3491022620:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 18.72/3.00 % TRYING [16] % 18.72/3.00 % Finite Model Found! % 18.72/3.00 % SZS status Satisfiable for theBenchmark % 18.72/3.00 % (490189)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.72/3.00 % (490189)------------------------------ % 18.72/3.00 % (490189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.72/3.00 % (490189)CaDiCaL version: 2.1.3 % 18.72/3.00 % (490189)Termination reason: Unknown % 18.72/3.00 % (490189)Termination phase: Finite model building constraint generation % 18.72/3.00 % (490189)Time elapsed: 0.006 s % 18.72/3.00 % (490189)Peak memory usage: 11 MB % 18.72/3.00 % (490189)Instructions burned: 11 (million) % 18.72/3.00 % (490191)ott-2_1_sil=16000:newcnf=on:random_seed=2814387616:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 18.72/3.00 % (490191)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 18.72/3.00 % (490167)Instruction limit reached! % 18.72/3.00 % (490167)------------------------------ % 18.72/3.00 % (490167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.72/3.00 % (490167)CaDiCaL version: 2.1.3 % 18.72/3.00 % (490167)Termination reason: Instruction limit % 18.72/3.00 % (490167)Termination phase: Saturation % 18.72/3.00 % (490167)Time elapsed: 0.450 s % 18.72/3.00 % (490167)Peak memory usage: 12 MB % 18.72/3.00 % (490167)Instructions burned: 1179 (million) % 18.72/3.00 % (490193)ott+10_1_sil=32000:tgt=ground:random_seed=3411597056:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 18.72/3.00 % (490175)Instruction limit reached! % 18.72/3.00 % (490175)------------------------------ % 18.72/3.00 % (490175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.72/3.00 % (490175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490175)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490175)Termination reason: Instruction limit % 43.77/6.45 % (490175)Termination phase: Saturation % 43.77/6.45 % (490175)Time elapsed: 0.365 s % 43.77/6.45 % (490175)Peak memory usage: 12 MB % 43.77/6.45 % (490175)Instructions burned: 882 (million) % 43.77/6.45 % (490195)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=323317385:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 43.77/6.45 % Detected minimum model sizes of [1] % 43.77/6.45 % Detected maximum model sizes of [2] % 43.77/6.45 % TRYING [1] % 43.77/6.45 % TRYING [2] % 43.77/6.45 % Finite Model Found! % 43.77/6.45 % SZS status Satisfiable for theBenchmark % 43.77/6.45 % (490195)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.77/6.45 % (490195)------------------------------ % 43.77/6.45 % (490195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.77/6.45 % (490195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490195)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490195)Termination reason: Unknown % 43.77/6.45 % (490195)Termination phase: Finite model building constraint generation % 43.77/6.45 % (490195)Time elapsed: 0.004 s % 43.77/6.45 % (490195)Peak memory usage: 11 MB % 43.77/6.45 % (490195)Instructions burned: 8 (million) % 43.77/6.45 % (490197)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3587539184:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 43.77/6.45 % (490197)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 43.77/6.45 % (490191)Instruction limit reached! % 43.77/6.45 % (490191)------------------------------ % 43.77/6.45 % (490191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.77/6.45 % (490191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490191)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490191)Termination reason: Instruction limit % 43.77/6.45 % (490191)Termination phase: Saturation % 43.77/6.45 % (490191)Time elapsed: 0.469 s % 43.77/6.45 % (490191)Peak memory usage: 12 MB % 43.77/6.45 % (490191)Instructions burned: 870 (million) % 43.77/6.45 % (490201)dis+21_1_sil=32000:sas=cadical:random_seed=784187684:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 43.77/6.45 % (490185)Instruction limit reached! % 43.77/6.45 % (490185)------------------------------ % 43.77/6.45 % (490185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.77/6.45 % (490185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490185)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490185)Termination reason: Instruction limit % 43.77/6.45 % (490185)Termination phase: Saturation % 43.77/6.45 % (490185)Time elapsed: 0.780 s % 43.77/6.45 % (490185)Peak memory usage: 13 MB % 43.77/6.45 % (490185)Instructions burned: 1472 (million) % 43.77/6.45 % (490203)ott+11_1_sil=16000:gs=on:random_seed=2024946460:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 43.77/6.45 % (490203)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 43.77/6.45 % (490183)Instruction limit reached! % 43.77/6.45 % (490183)------------------------------ % 43.77/6.45 % (490183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.77/6.45 % (490183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490183)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490183)Termination reason: Instruction limit % 43.77/6.45 % (490183)Termination phase: Saturation % 43.77/6.45 % (490183)Time elapsed: 1.073 s % 43.77/6.45 % (490183)Peak memory usage: 13 MB % 43.77/6.45 % (490183)Instructions burned: 5133 (million) % 43.77/6.45 % (490210)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3282955186:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 43.77/6.45 % Detected minimum model sizes of [1] % 43.77/6.45 % Detected maximum model sizes of [3] % 43.77/6.45 % fmb_start_size (= 7) larger than a detected sort maximum size! % 43.77/6.45 % (490210)Refutation not found, incomplete strategy % 43.77/6.45 % (490210)------------------------------ % 43.77/6.45 % (490210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.77/6.45 % (490210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.77/6.45 % (490210)CaDiCaL version: 2.1.3 % 43.77/6.45 % (490210)Termination reason: Refutation not found, incomplete strategy % 43.77/6.45 % (490210)Time elapsed: 0.004 s % 43.77/6.45 % (490210)Peak memory usage: 11 MB % 89.31/12.85 % (490210)Instructions burned: 8 (million) % 89.31/12.85 % (490210)------------------------------ % 89.31/12.85 % (490210)------------------------------ % 89.31/12.85 % (490212)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2386840296:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 89.31/12.85 % (490203)Instruction limit reached! % 89.31/12.85 % (490203)------------------------------ % 89.31/12.85 % (490203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.31/12.85 % (490203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.31/12.85 % (490203)CaDiCaL version: 2.1.3 % 89.31/12.85 % (490203)Termination reason: Instruction limit % 89.31/12.85 % (490203)Termination phase: Saturation % 89.31/12.85 % (490203)Time elapsed: 1.265 s % 89.31/12.85 % (490203)Peak memory usage: 12 MB % 89.31/12.85 % (490203)Instructions burned: 2252 (million) % 89.31/12.85 % (490222)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1582727377:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 89.31/12.85 % (490197)Instruction limit reached! % 89.31/12.85 % (490197)------------------------------ % 89.31/12.85 % (490197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.31/12.85 % (490197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.31/12.85 % (490197)CaDiCaL version: 2.1.3 % 89.31/12.85 % (490197)Termination reason: Instruction limit % 89.31/12.85 % (490197)Termination phase: Saturation % 89.31/12.85 % (490197)Time elapsed: 1.998 s % 89.31/12.85 % (490197)Peak memory usage: 14 MB % 89.31/12.85 % (490197)Instructions burned: 3513 (million) % 89.31/12.85 % (490224)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=664129927:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 89.31/12.85 % (490212)Instruction limit reached! % 89.31/12.85 % (490212)------------------------------ % 89.31/12.85 % (490212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.31/12.85 % (490212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.31/12.85 % (490212)CaDiCaL version: 2.1.3 % 89.31/12.85 % (490212)Termination reason: Instruction limit % 89.31/12.85 % (490212)Termination phase: Saturation % 89.31/12.85 % (490212)Time elapsed: 1.293 s % 89.31/12.85 % (490212)Peak memory usage: 13 MB % 89.31/12.85 % (490212)Instructions burned: 4595 (million) % 89.31/12.85 % (490226)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2590973154:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 89.31/12.85 % Detected minimum model sizes of [1] % 89.31/12.85 % Detected maximum model sizes of [2] % 89.31/12.85 % fmb_start_size (= 17) larger than a detected sort maximum size! % 89.31/12.85 % (490226)Refutation not found, incomplete strategy % 89.31/12.85 % (490226)------------------------------ % 89.31/12.85 % (490226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.31/12.85 % (490226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.31/12.85 % (490226)CaDiCaL version: 2.1.3 % 89.31/12.85 % (490226)Termination reason: Refutation not found, incomplete strategy % 89.31/12.85 % (490226)Time elapsed: 0.002 s % 89.31/12.85 % (490226)Peak memory usage: 10 MB % 89.31/12.85 % (490226)Instructions burned: 8 (million) % 89.31/12.85 % (490226)------------------------------ % 89.31/12.85 % (490226)------------------------------ % 89.31/12.85 % (490228)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=59647089:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 89.31/12.85 % Detected minimum model sizes of [1] % 89.31/12.85 % Detected maximum model sizes of [3] % 89.31/12.85 % fmb_start_size (= 15) larger than a detected sort maximum size! % 89.31/12.85 % (490228)Refutation not found, incomplete strategy % 89.31/12.85 % (490228)------------------------------ % 89.31/12.85 % (490228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.31/12.85 % (490228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.31/12.85 % (490228)CaDiCaL version: 2.1.3 % 89.31/12.85 % (490228)Termination reason: Refutation not found, incomplete strategy % 89.31/12.85 % (490228)Time elapsed: 0.002 s % 89.31/12.85 % (490228)Peak memory usage: 10 MB % 89.31/12.85 % (490228)Instructions burned: 8 (million) % 89.31/12.85 % (490228)------------------------------ % 89.31/12.85 % (490228)------------------------------ % 89.31/12.85 % (490230)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=565681124:i=14071_2972 on theBenchmark for (2972ds/14071Mi) % 89.31/12.85 % Detected minimum model sizes of [1] % 89.31/12.85 % Detected maximum model sizes of [2] % 92.86/13.33 % fmb_start_size (= 12) larger than a detected sort maximum size! % 92.86/13.33 % (490230)Refutation not found, incomplete strategy % 92.86/13.33 % (490230)------------------------------ % 92.86/13.33 % (490230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490230)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490230)Termination reason: Refutation not found, incomplete strategy % 92.86/13.33 % (490230)Time elapsed: 0.002 s % 92.86/13.33 % (490230)Peak memory usage: 10 MB % 92.86/13.33 % (490230)Instructions burned: 8 (million) % 92.86/13.33 % (490230)------------------------------ % 92.86/13.33 % (490230)------------------------------ % 92.86/13.33 % (490232)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3308491990:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi) % 92.86/13.33 % (490193)Instruction limit reached! % 92.86/13.33 % (490193)------------------------------ % 92.86/13.33 % (490193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490193)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490193)Termination reason: Instruction limit % 92.86/13.33 % (490193)Termination phase: Saturation % 92.86/13.33 % (490193)Time elapsed: 2.466 s % 92.86/13.33 % (490193)Peak memory usage: 12 MB % 92.86/13.33 % (490193)Instructions burned: 5115 (million) % 92.86/13.33 % (490234)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3000630898:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 92.86/13.33 % (490201)Instruction limit reached! % 92.86/13.33 % (490201)------------------------------ % 92.86/13.33 % (490201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490201)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490201)Termination reason: Instruction limit % 92.86/13.33 % (490201)Termination phase: Saturation % 92.86/13.33 % (490201)Time elapsed: 2.338 s % 92.86/13.33 % (490201)Peak memory usage: 15 MB % 92.86/13.33 % (490201)Instructions burned: 3775 (million) % 92.86/13.33 % (490237)dis+10_16:1_sil=16000:random_seed=1775902672:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 92.86/13.33 % (490224)Instruction limit reached! % 92.86/13.33 % (490224)------------------------------ % 92.86/13.33 % (490224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490224)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490224)Termination reason: Instruction limit % 92.86/13.33 % (490224)Termination phase: Saturation % 92.86/13.33 % (490224)Time elapsed: 2.362 s % 92.86/13.33 % (490224)Peak memory usage: 16 MB % 92.86/13.33 % (490224)Instructions burned: 5214 (million) % 92.86/13.33 % (490240)ott-3_8_sil=64000:random_seed=316589420:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 92.86/13.33 % (490232)Instruction limit reached! % 92.86/13.33 % (490232)------------------------------ % 92.86/13.33 % (490232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490232)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490232)Termination reason: Instruction limit % 92.86/13.33 % (490232)Termination phase: Saturation % 92.86/13.33 % (490232)Time elapsed: 3.418 s % 92.86/13.33 % (490232)Peak memory usage: 14 MB % 92.86/13.33 % (490232)Instructions burned: 22566 (million) % 92.86/13.33 % (490242)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=456132484:fmbsr=2:i=32576_2937 on theBenchmark for (2937ds/32576Mi) % 92.86/13.33 % Detected minimum model sizes of [1] % 92.86/13.33 % Detected maximum model sizes of [2] % 92.86/13.33 % fmb_start_size (= 9) larger than a detected sort maximum size! % 92.86/13.33 % (490242)Refutation not found, incomplete strategy % 92.86/13.33 % (490242)------------------------------ % 92.86/13.33 % (490242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.86/13.33 % (490242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.86/13.33 % (490242)CaDiCaL version: 2.1.3 % 92.86/13.33 % (490242)Termination reason: Refutation not found, incomplete strategy % 92.86/13.33 % (490242)Time elapsed: 0.002 s % 92.86/13.33 % (490242)Peak memory usage: 10 MB % 92.86/13.33 % (490242)Instructions burned: 8 (million) % 92.86/13.33 % (490242)------------------------------ % 92.86/13.33 % (490242)------------------------------ % 104.91/15.07 % (490244)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=513027736:i=11404_2937 on theBenchmark for (2937ds/11404Mi) % 104.91/15.07 % (490234)Instruction limit reached! % 104.91/15.07 % (490234)------------------------------ % 104.91/15.07 % (490234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490234)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490234)Termination reason: Instruction limit % 104.91/15.07 % (490234)Termination phase: Saturation % 104.91/15.07 % (490234)Time elapsed: 3.430 s % 104.91/15.07 % (490234)Peak memory usage: 12 MB % 104.91/15.07 % (490234)Instructions burned: 8176 (million) % 104.91/15.07 % (490246)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3271911818:i=14134_2934 on theBenchmark for (2934ds/14134Mi) % 104.91/15.07 % (490246)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 104.91/15.07 % (490237)Instruction limit reached! % 104.91/15.07 % (490237)------------------------------ % 104.91/15.07 % (490237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490237)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490237)Termination reason: Instruction limit % 104.91/15.07 % (490237)Termination phase: Saturation % 104.91/15.07 % (490237)Time elapsed: 3.378 s % 104.91/15.07 % (490237)Peak memory usage: 16 MB % 104.91/15.07 % (490237)Instructions burned: 9156 (million) % 104.91/15.07 % (490248)dis+33_16_sil=32000:sac=on:random_seed=544034222:i=15851:nm=0_2932 on theBenchmark for (2932ds/15851Mi) % 104.91/15.07 % (490244)Instruction limit reached! % 104.91/15.07 % (490244)------------------------------ % 104.91/15.07 % (490244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490244)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490244)Termination reason: Instruction limit % 104.91/15.07 % (490244)Termination phase: Saturation % 104.91/15.07 % (490244)Time elapsed: 2.322 s % 104.91/15.07 % (490244)Peak memory usage: 13 MB % 104.91/15.07 % (490244)Instructions burned: 11406 (million) % 104.91/15.07 % (490250)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3783576195:avsq=on:i=17627:add=on:amm=off_2914 on theBenchmark for (2914ds/17627Mi) % 104.91/15.07 % (490246)Instruction limit reached! % 104.91/15.07 % (490246)------------------------------ % 104.91/15.07 % (490246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490246)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490246)Termination reason: Instruction limit % 104.91/15.07 % (490246)Termination phase: Saturation % 104.91/15.07 % (490246)Time elapsed: 5.310 s % 104.91/15.07 % (490246)Peak memory usage: 12 MB % 104.91/15.07 % (490246)Instructions burned: 14136 (million) % 104.91/15.07 % (490253)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4105261367:s2a=on:i=53295_2881 on theBenchmark for (2881ds/53295Mi) % 104.91/15.07 % (490250)Instruction limit reached! % 104.91/15.07 % (490250)------------------------------ % 104.91/15.07 % (490250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490250)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490250)Termination reason: Instruction limit % 104.91/15.07 % (490250)Termination phase: Saturation % 104.91/15.07 % (490250)Time elapsed: 4.044 s % 104.91/15.07 % (490250)Peak memory usage: 22 MB % 104.91/15.07 % (490250)Instructions burned: 17632 (million) % 104.91/15.07 % (490256)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=947187021:i=26857:ins=20_2873 on theBenchmark for (2873ds/26857Mi) % 104.91/15.07 % Detected minimum model sizes of [1] % 104.91/15.07 % Detected maximum model sizes of [2] % 104.91/15.07 % fmb_start_size (= 16) larger than a detected sort maximum size! % 104.91/15.07 % (490256)Refutation not found, incomplete strategy % 104.91/15.07 % (490256)------------------------------ % 104.91/15.07 % (490256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.91/15.07 % (490256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.91/15.07 % (490256)CaDiCaL version: 2.1.3 % 104.91/15.07 % (490256)Termination reason: Refutation not found, incomplete strategy % 104.91/15.07 % (490256)Time elapsed: 0.002 s % 104.91/15.07 % (490256)Peak memory usage: 10 MB % 104.91/15.07 % (490256)Instructions burned: 8 (million) % 109.08/15.63 % (490256)------------------------------ % 109.08/15.63 % (490256)------------------------------ % 109.08/15.63 % (490258)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1407398317:i=28120:bs=on:fsr=off_2873 on theBenchmark for (2873ds/28120Mi) % 109.08/15.63 % (490240)Instruction limit reached! % 109.08/15.63 % (490240)------------------------------ % 109.08/15.63 % (490240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.08/15.63 % (490240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.08/15.63 % (490240)CaDiCaL version: 2.1.3 % 109.08/15.63 % (490240)Termination reason: Instruction limit % 109.08/15.63 % (490240)Termination phase: Saturation % 109.08/15.63 % (490240)Time elapsed: 7.908 s % 109.08/15.63 % (490240)Peak memory usage: 14 MB % 109.08/15.63 % (490240)Instructions burned: 20141 (million) % 109.08/15.63 % (490260)fmb+10_1_sil=256000:fmbss=7:random_seed=4210074175:fmbsr=1.6:i=182295_2869 on theBenchmark for (2869ds/182295Mi) % 109.08/15.63 % Detected minimum model sizes of [1] % 109.08/15.63 % Detected maximum model sizes of [2] % 109.08/15.63 % fmb_start_size (= 7) larger than a detected sort maximum size! % 109.08/15.63 % (490260)Refutation not found, incomplete strategy % 109.08/15.63 % (490260)------------------------------ % 109.08/15.63 % (490260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.08/15.63 % (490260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.08/15.63 % (490260)CaDiCaL version: 2.1.3 % 109.08/15.63 % (490260)Termination reason: Refutation not found, incomplete strategy % 109.08/15.63 % (490260)Time elapsed: 0.004 s % 109.08/15.63 % (490260)Peak memory usage: 10 MB % 109.08/15.63 % (490260)Instructions burned: 8 (million) % 109.08/15.63 % (490260)------------------------------ % 109.08/15.63 % (490260)------------------------------ % 109.08/15.63 % (490262)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1109501269:i=44625:gsp=on_2869 on theBenchmark for (2869ds/44625Mi) % 109.08/15.63 % (490262)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 109.08/15.63 % (490262)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 109.08/15.63 % Detected minimum model sizes of [1] % 109.08/15.63 % Detected maximum model sizes of [2] % 109.08/15.63 % fmb_start_size (= 21) larger than a detected sort maximum size! % 109.08/15.63 % (490262)Refutation not found, incomplete strategy % 109.08/15.63 % (490262)------------------------------ % 109.08/15.63 % (490262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.08/15.63 % (490262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.08/15.63 % (490262)CaDiCaL version: 2.1.3 % 109.08/15.63 % (490262)Termination reason: Refutation not found, incomplete strategy % 109.08/15.63 % (490262)Time elapsed: 0.004 s % 109.08/15.63 % (490262)Peak memory usage: 10 MB % 109.08/15.63 % (490262)Instructions burned: 8 (million) % 109.08/15.63 % (490262)------------------------------ % 109.08/15.63 % (490262)------------------------------ % 109.08/15.63 % (490264)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=517005727:i=160505_2869 on theBenchmark for (2869ds/160505Mi) % 109.08/15.63 % Detected minimum model sizes of [1] % 109.08/15.63 % Detected maximum model sizes of [2] % 109.08/15.63 % fmb_start_size (= 15) larger than a detected sort maximum size! % 109.08/15.63 % (490264)Refutation not found, incomplete strategy % 109.08/15.63 % (490264)------------------------------ % 109.08/15.63 % (490264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.08/15.63 % (490264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.08/15.63 % (490264)CaDiCaL version: 2.1.3 % 109.08/15.63 % (490264)Termination reason: Refutation not found, incomplete strategy % 109.08/15.63 % (490264)Time elapsed: 0.004 s % 109.08/15.63 % (490264)Peak memory usage: 10 MB % 109.08/15.63 % (490264)Instructions burned: 8 (million) % 109.08/15.63 % (490264)------------------------------ % 109.08/15.63 % (490264)------------------------------ % 109.08/15.63 % (490266)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1048253161:fmbsr=1.3:i=225729_2869 on theBenchmark for (2869ds/225729Mi) % 109.08/15.63 % Detected minimum model sizes of [1] % 109.08/15.63 % Detected maximum model sizes of [2] % 109.08/15.63 % fmb_start_size (= 10) larger than a detected sort maximum size! % 109.08/15.63 % (490266)Refutation not found, incomplete strategy % 109.08/15.63 % (490266)------------------------------ % 109.08/15.63 % (490266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.08/15.63 % (490266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.08/15.63 % (490266)CaDiCaL version: 2.1.3 % 124.08/17.78 % (490266)Termination reason: Refutation not found, incomplete strategy % 124.08/17.78 % (490266)Time elapsed: 0.004 s % 124.08/17.78 % (490266)Peak memory usage: 10 MB % 124.08/17.78 % (490266)Instructions burned: 8 (million) % 124.08/17.78 % (490266)------------------------------ % 124.08/17.78 % (490266)------------------------------ % 124.08/17.78 % (490268)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2099881473:fmbsr=2:i=185024:ins=7_2868 on theBenchmark for (2868ds/185024Mi) % 124.08/17.78 % Detected minimum model sizes of [1] % 124.08/17.78 % Detected maximum model sizes of [2] % 124.08/17.78 % fmb_start_size (= 10) larger than a detected sort maximum size! % 124.08/17.78 % (490268)Refutation not found, incomplete strategy % 124.08/17.78 % (490268)------------------------------ % 124.08/17.78 % (490268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.08/17.78 % (490268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.08/17.78 % (490268)CaDiCaL version: 2.1.3 % 124.08/17.78 % (490268)Termination reason: Refutation not found, incomplete strategy % 124.08/17.78 % (490268)Time elapsed: 0.004 s % 124.08/17.78 % (490268)Peak memory usage: 11 MB % 124.08/17.78 % (490268)Instructions burned: 8 (million) % 124.08/17.78 % (490268)------------------------------ % 124.08/17.78 % (490268)------------------------------ % 124.08/17.78 % (490270)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=680158412:rtra=on_2868 on theBenchmark for (2868ds/0Mi) % 124.08/17.78 % Detected minimum model sizes of [1] % 124.08/17.78 % Detected maximum model sizes of [2] % 124.08/17.78 % TRYING [1] % 124.08/17.78 % TRYING [2] % 124.08/17.78 % Finite Model Found! % 124.08/17.78 % SZS status Satisfiable for theBenchmark % 124.08/17.78 % (490270)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.08/17.78 % (490270)------------------------------ % 124.08/17.78 % (490270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.08/17.78 % (490270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.08/17.78 % (490270)CaDiCaL version: 2.1.3 % 124.08/17.78 % (490270)Termination reason: Unknown % 124.08/17.78 % (490270)Termination phase: Finite model building constraint generation % 124.08/17.78 % (490270)Time elapsed: 0.004 s % 124.08/17.78 % (490270)Peak memory usage: 11 MB % 124.08/17.78 % (490270)Instructions burned: 8 (million) % 124.08/17.78 % (490272)% WARNING: option uhcvi not known. % 124.08/17.78 % (490272)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3486087990:i=271062:add=off:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/271062Mi) % 124.08/17.78 % (490272)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 124.08/17.78 % (490272)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 124.08/17.78 % (490248)Instruction limit reached! % 124.08/17.78 % (490248)------------------------------ % 124.08/17.78 % (490248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.08/17.78 % (490248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.08/17.78 % (490248)CaDiCaL version: 2.1.3 % 124.08/17.78 % (490248)Termination reason: Instruction limit % 124.08/17.78 % (490248)Termination phase: Saturation % 124.08/17.78 % (490248)Time elapsed: 6.585 s % 124.08/17.78 % (490248)Peak memory usage: 14 MB % 124.08/17.78 % (490248)Instructions burned: 15854 (million) % 124.08/17.78 % (490274)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3308944011:i=176048:add=on:rtra=on:rawr=on_2866 on theBenchmark for (2866ds/176048Mi) % 124.08/17.78 % (490222)Instruction limit reached! % 124.08/17.78 % (490222)------------------------------ % 124.08/17.78 % (490222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.08/17.78 % (490222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.08/17.78 % (490222)CaDiCaL version: 2.1.3 % 124.08/17.78 % (490222)Termination reason: Instruction limit % 124.08/17.78 % (490222)Termination phase: Saturation % 124.08/17.78 % (490222)Time elapsed: 12.284 s % 124.08/17.78 % (490222)Peak memory usage: 16 MB % 124.08/17.78 % (490222)Instructions burned: 29341 (million) % 124.08/17.78 % (490277)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4203407521:i=206:fgj=on:rtra=on_2852 on theBenchmark for (2852ds/206Mi) % 124.08/17.78 % (490277)Instruction limit reached! % 124.08/17.78 % (490277)------------------------------ % 124.08/17.78 % (490277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.08/17.78 % (490277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490277)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490277)Termination reason: Instruction limit % 125.79/18.12 % (490277)Termination phase: Saturation % 125.79/18.12 % (490277)Time elapsed: 0.093 s % 125.79/18.12 % (490277)Peak memory usage: 12 MB % 125.79/18.12 % (490277)Instructions burned: 207 (million) % 125.79/18.12 % (490279)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3583737357:i=232:rtra=on_2851 on theBenchmark for (2851ds/232Mi) % 125.79/18.12 % (490279)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 125.79/18.12 % (490279)Instruction limit reached! % 125.79/18.12 % (490279)------------------------------ % 125.79/18.12 % (490279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.79/18.12 % (490279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490279)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490279)Termination reason: Instruction limit % 125.79/18.12 % (490279)Termination phase: Saturation % 125.79/18.12 % (490279)Time elapsed: 0.095 s % 125.79/18.12 % (490279)Peak memory usage: 12 MB % 125.79/18.12 % (490279)Instructions burned: 232 (million) % 125.79/18.12 % (490281)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2684720525:i=262:rtra=on_2850 on theBenchmark for (2850ds/262Mi) % 125.79/18.12 % (490281)Instruction limit reached! % 125.79/18.12 % (490281)------------------------------ % 125.79/18.12 % (490281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.79/18.12 % (490281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490281)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490281)Termination reason: Instruction limit % 125.79/18.12 % (490281)Termination phase: Saturation % 125.79/18.12 % (490281)Time elapsed: 0.107 s % 125.79/18.12 % (490281)Peak memory usage: 12 MB % 125.79/18.12 % (490281)Instructions burned: 263 (million) % 125.79/18.12 % (490283)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3903615075:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2848 on theBenchmark for (2848ds/318Mi) % 125.79/18.12 % (490283)Instruction limit reached! % 125.79/18.12 % (490283)------------------------------ % 125.79/18.12 % (490283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.79/18.12 % (490283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490283)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490283)Termination reason: Instruction limit % 125.79/18.12 % (490283)Termination phase: Saturation % 125.79/18.12 % (490283)Time elapsed: 0.124 s % 125.79/18.12 % (490283)Peak memory usage: 12 MB % 125.79/18.12 % (490283)Instructions burned: 319 (million) % 125.79/18.12 % (490285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1426053430:i=1428:nm=2:rtra=on_2847 on theBenchmark for (2847ds/1428Mi) % 125.79/18.12 % Detected minimum model sizes of [1] % 125.79/18.12 % Detected maximum model sizes of [3] % 125.79/18.12 % TRYING [1] % 125.79/18.12 % TRYING [2] % 125.79/18.12 % Finite Model Found! % 125.79/18.12 % SZS status Satisfiable for theBenchmark % 125.79/18.12 % (490285)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 125.79/18.12 % (490285)------------------------------ % 125.79/18.12 % (490285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.79/18.12 % (490285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490285)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490285)Termination reason: Unknown % 125.79/18.12 % (490285)Termination phase: Finite model building constraint generation % 125.79/18.12 % (490285)Time elapsed: 0.004 s % 125.79/18.12 % (490285)Peak memory usage: 11 MB % 125.79/18.12 % (490285)Instructions burned: 8 (million) % 125.79/18.12 % (490287)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1935474430:i=262:bd=preordered:rtra=on:fsd=on_2847 on theBenchmark for (2847ds/262Mi) % 125.79/18.12 % (490287)Instruction limit reached! % 125.79/18.12 % (490287)------------------------------ % 125.79/18.12 % (490287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.79/18.12 % (490287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.79/18.12 % (490287)CaDiCaL version: 2.1.3 % 125.79/18.12 % (490287)Termination reason: Instruction limit % 125.79/18.12 % (490287)Termination phase: Saturation % 125.79/18.12 % (490287)Time elapsed: 0.109 s % 125.79/18.12 % (490287)Peak memory usage: 12 MB % 125.79/18.12 % (490287)Instructions burned: 263 (million) % 125.79/18.12 % (490289)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=3749060356:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2846 on theBenchmark for (2846ds/1368Mi) % 142.03/20.24 % (490289)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 142.03/20.24 % (490289)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 142.03/20.24 % (490289)Instruction limit reached! % 142.03/20.24 % (490289)------------------------------ % 142.03/20.24 % (490289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490289)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490289)Termination reason: Instruction limit % 142.03/20.24 % (490289)Termination phase: Saturation % 142.03/20.24 % (490289)Time elapsed: 0.604 s % 142.03/20.24 % (490289)Peak memory usage: 14 MB % 142.03/20.24 % (490289)Instructions burned: 1369 (million) % 142.03/20.24 % (490291)ott-21_1_sil=16000:si=on:fs=off:random_seed=2319882404:i=360:av=off:fsr=off:rtra=on_2839 on theBenchmark for (2839ds/360Mi) % 142.03/20.24 % (490291)Instruction limit reached! % 142.03/20.24 % (490291)------------------------------ % 142.03/20.24 % (490291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490291)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490291)Termination reason: Instruction limit % 142.03/20.24 % (490291)Termination phase: Saturation % 142.03/20.24 % (490291)Time elapsed: 0.158 s % 142.03/20.24 % (490291)Peak memory usage: 14 MB % 142.03/20.24 % (490291)Instructions burned: 362 (million) % 142.03/20.24 % (490293)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=841484378:i=954:bd=all:rtra=on_2838 on theBenchmark for (2838ds/954Mi) % 142.03/20.24 % (490293)Instruction limit reached! % 142.03/20.24 % (490293)------------------------------ % 142.03/20.24 % (490293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490293)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490293)Termination reason: Instruction limit % 142.03/20.24 % (490293)Termination phase: Saturation % 142.03/20.24 % (490293)Time elapsed: 0.419 s % 142.03/20.24 % (490293)Peak memory usage: 12 MB % 142.03/20.24 % (490293)Instructions burned: 955 (million) % 142.03/20.24 % (490298)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3000924144:fmbsr=1.3:i=1730:ins=25:rtra=on_2833 on theBenchmark for (2833ds/1730Mi) % 142.03/20.24 % Detected minimum model sizes of [1] % 142.03/20.24 % Detected maximum model sizes of [2] % 142.03/20.24 % TRYING [1] % 142.03/20.24 % TRYING [2] % 142.03/20.24 % Finite Model Found! % 142.03/20.24 % SZS status Satisfiable for theBenchmark % 142.03/20.24 % (490298)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.03/20.24 % (490298)------------------------------ % 142.03/20.24 % (490298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490298)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490298)Termination reason: Unknown % 142.03/20.24 % (490298)Termination phase: Finite model building constraint generation % 142.03/20.24 % (490298)Time elapsed: 0.004 s % 142.03/20.24 % (490298)Peak memory usage: 10 MB % 142.03/20.24 % (490298)Instructions burned: 8 (million) % 142.03/20.24 % (490300)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2871774522:i=2358:rtra=on_2833 on theBenchmark for (2833ds/2358Mi) % 142.03/20.24 % (490300)Instruction limit reached! % 142.03/20.24 % (490300)------------------------------ % 142.03/20.24 % (490300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490300)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490300)Termination reason: Instruction limit % 142.03/20.24 % (490300)Termination phase: Saturation % 142.03/20.24 % (490300)Time elapsed: 0.879 s % 142.03/20.24 % (490300)Peak memory usage: 12 MB % 142.03/20.24 % (490300)Instructions burned: 2360 (million) % 142.03/20.24 % (490258)Instruction limit reached! % 142.03/20.24 % (490258)------------------------------ % 142.03/20.24 % (490258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.03/20.24 % (490258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.03/20.24 % (490258)CaDiCaL version: 2.1.3 % 142.03/20.24 % (490258)Termination reason: Instruction limit % 142.03/20.24 % (490258)Termination phase: Saturation % 142.03/20.24 % (490258)Time elapsed: 4.913 s % 142.03/20.24 % (490258)Peak memory usage: 16 MB % 142.03/20.24 % (490258)Instructions burned: 28125 (million) % 166.95/23.82 % (490453)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=72346028:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/1384Mi) % 166.95/23.82 % (490453)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 166.95/23.82 % (490452)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1369632419:i=1778:ins=1:rtra=on_2824 on theBenchmark for (2824ds/1778Mi) % 166.95/23.82 % Exception at run slice level % 166.95/23.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 166.95/23.82 % (490456)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3030822847:i=1758:kws=inv_precedence:fsr=off:rtra=on_2824 on theBenchmark for (2824ds/1758Mi) % 166.95/23.82 % (490456)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 166.95/23.82 % (490453)Instruction limit reached! % 166.95/23.82 % (490453)------------------------------ % 166.95/23.82 % (490453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.95/23.82 % (490453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.95/23.82 % (490453)CaDiCaL version: 2.1.3 % 166.95/23.82 % (490453)Termination reason: Instruction limit % 166.95/23.82 % (490453)Termination phase: Saturation % 166.95/23.82 % (490453)Time elapsed: 0.291 s % 166.95/23.82 % (490453)Peak memory usage: 13 MB % 166.95/23.82 % (490453)Instructions burned: 1384 (million) % 166.95/23.82 % (490458)fmb+10_1_sil=64000:si=on:random_seed=1894698105:i=44122:nm=2:rtra=on:gsp=on_2821 on theBenchmark for (2821ds/44122Mi) % 166.95/23.82 % (490458)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 166.95/23.82 % Detected minimum model sizes of [1] % 166.95/23.82 % Detected maximum model sizes of [2] % 166.95/23.82 % TRYING [1] % 166.95/23.82 % TRYING [2] % 166.95/23.82 % Finite Model Found! % 166.95/23.82 % SZS status Satisfiable for theBenchmark % 166.95/23.82 % (490458)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 166.95/23.82 % (490458)------------------------------ % 166.95/23.82 % (490458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.95/23.82 % (490458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.95/23.82 % (490458)CaDiCaL version: 2.1.3 % 166.95/23.82 % (490458)Termination reason: Unknown % 166.95/23.82 % (490458)Termination phase: Finite model building constraint generation % 166.95/23.82 % (490458)Time elapsed: 0.002 s % 166.95/23.82 % (490458)Peak memory usage: 10 MB % 166.95/23.82 % (490458)Instructions burned: 8 (million) % 166.95/23.82 % (490460)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=293024301:i=19030:nm=5:rtra=on_2821 on theBenchmark for (2821ds/19030Mi) % 166.95/23.82 % Detected minimum model sizes of [1] % 166.95/23.82 % Detected maximum model sizes of [2] % 166.95/23.82 % fmb_start_size (= 20) larger than a detected sort maximum size! % 166.95/23.82 % (490460)Refutation not found, incomplete strategy % 166.95/23.82 % (490460)------------------------------ % 166.95/23.82 % (490460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.95/23.82 % (490460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.95/23.82 % (490460)CaDiCaL version: 2.1.3 % 166.95/23.82 % (490460)Termination reason: Refutation not found, incomplete strategy % 166.95/23.82 % (490460)Time elapsed: 0.002 s % 166.95/23.82 % (490460)Peak memory usage: 10 MB % 166.95/23.82 % (490460)Instructions burned: 8 (million) % 166.95/23.82 % (490460)------------------------------ % 166.95/23.82 % (490460)------------------------------ % 166.95/23.82 % (490462)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2070474674:fmbsr=1.7:i=1840:rtra=on_2821 on theBenchmark for (2821ds/1840Mi) % 166.95/23.82 % Detected minimum model sizes of [1] % 166.95/23.82 % Detected maximum model sizes of [2] % 166.95/23.82 % fmb_start_size (= 8) larger than a detected sort maximum size! % 166.95/23.82 % (490462)Refutation not found, incomplete strategy % 166.95/23.82 % (490462)------------------------------ % 166.95/23.82 % (490462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.95/23.82 % (490462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.95/23.82 % (490462)CaDiCaL version: 2.1.3 % 166.95/23.82 % (490462)Termination reason: Refutation not found, incomplete strategy % 166.95/23.82 % (490462)Time elapsed: 0.002 s % 166.95/23.82 % (490462)Peak memory usage: 10 MB % 166.95/23.82 % (490462)Instructions burned: 8 (million) % 166.95/23.82 % (490462)------------------------------ % 180.29/25.79 % (490462)------------------------------ % 180.29/25.79 % (490464)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1241021780:i=10262:rtra=on_2820 on theBenchmark for (2820ds/10262Mi) % 180.29/25.79 % (490464)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 180.29/25.79 % (490456)Instruction limit reached! % 180.29/25.79 % (490456)------------------------------ % 180.29/25.79 % (490456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (490456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (490456)CaDiCaL version: 2.1.3 % 180.29/25.79 % (490456)Termination reason: Instruction limit % 180.29/25.79 % (490456)Termination phase: Saturation % 180.29/25.79 % (490456)Time elapsed: 0.631 s % 180.29/25.79 % (490456)Peak memory usage: 12 MB % 180.29/25.79 % (490456)Instructions burned: 1761 (million) % 180.29/25.79 % (490466)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=769719896:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2817 on theBenchmark for (2817ds/2944Mi) % 180.29/25.79 % (490466)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 180.29/25.79 % (490466)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 180.29/25.79 % (490466)Instruction limit reached! % 180.29/25.79 % (490466)------------------------------ % 180.29/25.79 % (490466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (490466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (490466)CaDiCaL version: 2.1.3 % 180.29/25.79 % (490466)Termination reason: Instruction limit % 180.29/25.79 % (490466)Termination phase: Saturation % 180.29/25.79 % (490466)Time elapsed: 1.201 s % 180.29/25.79 % (490466)Peak memory usage: 14 MB % 180.29/25.79 % (490466)Instructions burned: 2946 (million) % 180.29/25.79 % (490468)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4196880181:i=12648:rtra=on_2805 on theBenchmark for (2805ds/12648Mi) % 180.29/25.79 % Detected minimum model sizes of [1] % 180.29/25.79 % Detected maximum model sizes of [2] % 180.29/25.79 % fmb_start_size (= 77) larger than a detected sort maximum size! % 180.29/25.79 % (490468)Refutation not found, incomplete strategy % 180.29/25.79 % (490468)------------------------------ % 180.29/25.79 % (490468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (490468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (490468)CaDiCaL version: 2.1.3 % 180.29/25.79 % (490468)Termination reason: Refutation not found, incomplete strategy % 180.29/25.79 % (490468)Time elapsed: 0.004 s % 180.29/25.79 % (490468)Peak memory usage: 10 MB % 180.29/25.79 % (490468)Instructions burned: 8 (million) % 180.29/25.79 % (490468)------------------------------ % 180.29/25.79 % (490468)------------------------------ % 180.29/25.79 % (490470)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4137397191:fmbsr=2.30978:i=4348:rtra=on_2805 on theBenchmark for (2805ds/4348Mi) % 180.29/25.79 % TRYING [16] % 180.29/25.79 % Finite Model Found! % 180.29/25.79 % SZS status Satisfiable for theBenchmark % 180.29/25.79 % (490470)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 180.29/25.79 % (490470)------------------------------ % 180.29/25.79 % (490470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (490470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (490470)CaDiCaL version: 2.1.3 % 180.29/25.79 % (490470)Termination reason: Unknown % 180.29/25.79 % (490470)Termination phase: Finite model building constraint generation % 180.29/25.79 % (490470)Time elapsed: 0.006 s % 180.29/25.79 % (490470)Peak memory usage: 11 MB % 180.29/25.79 % (490470)Instructions burned: 12 (million) % 180.29/25.79 % (490472)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2980183115:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2804 on theBenchmark for (2804ds/1738Mi) % 180.29/25.79 % (490472)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 180.29/25.79 % (490464)Instruction limit reached! % 180.29/25.79 % (490464)------------------------------ % 180.29/25.79 % (490464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (490464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (490464)CaDiCaL version: 2.1.3 % 180.29/25.79 % (490464)Termination reason: Instruction limit % 180.29/25.79 % (490464)Termination phase: Saturation % 249.70/35.48 % (490464)Time elapsed: 2.108 s % 249.70/35.48 % (490464)Peak memory usage: 13 MB % 249.70/35.48 % (490464)Instructions burned: 10265 (million) % 249.70/35.48 % (490474)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3650542912:i=10228:av=off:rtra=on_2799 on theBenchmark for (2799ds/10228Mi) % 249.70/35.48 % (490472)Instruction limit reached! % 249.70/35.48 % (490472)------------------------------ % 249.70/35.48 % (490472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.48 % (490472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.48 % (490472)CaDiCaL version: 2.1.3 % 249.70/35.48 % (490472)Termination reason: Instruction limit % 249.70/35.48 % (490472)Termination phase: Saturation % 249.70/35.48 % (490472)Time elapsed: 0.682 s % 249.70/35.48 % (490472)Peak memory usage: 12 MB % 249.70/35.48 % (490472)Instructions burned: 1738 (million) % 249.70/35.48 % (490476)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3403625309:i=108564:rtra=on_2797 on theBenchmark for (2797ds/108564Mi) % 249.70/35.48 % Detected minimum model sizes of [1] % 249.70/35.48 % Detected maximum model sizes of [2] % 249.70/35.48 % TRYING [1] % 249.70/35.48 % TRYING [2] % 249.70/35.48 % Finite Model Found! % 249.70/35.48 % SZS status Satisfiable for theBenchmark % 249.70/35.48 % (490476)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 249.70/35.48 % (490476)------------------------------ % 249.70/35.48 % (490476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.48 % (490476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.48 % (490476)CaDiCaL version: 2.1.3 % 249.70/35.48 % (490476)Termination reason: Unknown % 249.70/35.48 % (490476)Termination phase: Finite model building constraint generation % 249.70/35.48 % (490476)Time elapsed: 0.004 s % 249.70/35.48 % (490476)Peak memory usage: 11 MB % 249.70/35.48 % (490476)Instructions burned: 8 (million) % 249.70/35.48 % (490478)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3693206147:i=7024:aac=none:rtra=on_2797 on theBenchmark for (2797ds/7024Mi) % 249.70/35.48 % (490478)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 249.70/35.48 % (490474)Instruction limit reached! % 249.70/35.48 % (490474)------------------------------ % 249.70/35.48 % (490474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.48 % (490474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.48 % (490474)CaDiCaL version: 2.1.3 % 249.70/35.48 % (490474)Termination reason: Instruction limit % 249.70/35.48 % (490474)Termination phase: Saturation % 249.70/35.48 % (490474)Time elapsed: 1.953 s % 249.70/35.48 % (490474)Peak memory usage: 12 MB % 249.70/35.48 % (490474)Instructions burned: 10228 (million) % 249.70/35.48 % (490480)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=857597813:i=7546:rtra=on:amm=off_2779 on theBenchmark for (2779ds/7546Mi) % 249.70/35.48 % (490478)Instruction limit reached! % 249.70/35.48 % (490478)------------------------------ % 249.70/35.48 % (490478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.48 % (490478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.48 % (490478)CaDiCaL version: 2.1.3 % 249.70/35.48 % (490478)Termination reason: Instruction limit % 249.70/35.48 % (490478)Termination phase: Saturation % 249.70/35.48 % (490478)Time elapsed: 2.915 s % 249.70/35.48 % (490478)Peak memory usage: 16 MB % 249.70/35.48 % (490478)Instructions burned: 7026 (million) % 249.70/35.48 % (490482)ott+11_1_sil=16000:si=on:gs=on:random_seed=2588358529:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2768 on theBenchmark for (2768ds/4502Mi) % 249.70/35.48 % (490482)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 249.70/35.48 % (490480)Instruction limit reached! % 249.70/35.48 % (490480)------------------------------ % 249.70/35.48 % (490480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.48 % (490480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.48 % (490480)CaDiCaL version: 2.1.3 % 249.70/35.48 % (490480)Termination reason: Instruction limit % 249.70/35.48 % (490480)Termination phase: Saturation % 249.70/35.48 % (490480)Time elapsed: 1.579 s % 249.70/35.48 % (490480)Peak memory usage: 17 MB % 249.70/35.48 % (490480)Instructions burned: 7550 (million) % 249.70/35.48 % (490484)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=911732178:fmbsr=1.6:i=135068:rtra=on_2764 on theBenchmark for (2764ds/135068Mi) % 249.70/35.48 % Detected minimum model sizes of [Terminated % 300.11/42.54 % Vampire exiting %------------------------------------------------------------------------------