%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LCL698^1 : TPTP v9.3.1. Bugfixed v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:05 AM UTC 2026 % Result : Satisfiable 1.05s 0.49s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL698^1 : TPTP v9.3.1. Bugfixed v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n001.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Tue Sep 29 09:49:35 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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.05/0.49 % (1023525)Will run a generic schedule for satisfiability detection. % 1.05/0.49 % (1023533)dis+10_1_sil=32000:sp=arity:random_seed=3985768017:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.05/0.49 % (1023531)% WARNING: option uhcvi not known. % 1.05/0.49 % (1023532)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4066117005:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.05/0.49 % (1023530)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2699313306_2999 on theBenchmark for (2999ds/0Mi) % 1.05/0.49 % (1023531)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3806878222:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.05/0.49 % (1023534)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=283341964:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.05/0.49 % (1023531)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.05/0.49 % (1023534)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 1.05/0.49 % Detected minimum model sizes of [1] % 1.05/0.49 % Detected maximum model sizes of [2] % 1.05/0.49 % (1023531)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 1.05/0.49 % TRYING [1] % 1.05/0.49 % TRYING [2] % 1.05/0.49 % Finite Model Found! % 1.05/0.49 % SZS status Satisfiable for theBenchmark % 1.05/0.49 % (1023530)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.05/0.49 % (1023530)------------------------------ % 1.05/0.49 % (1023530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.05/0.49 % (1023530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.05/0.49 % (1023530)CaDiCaL version: 2.1.3 % 1.05/0.49 % (1023530)Termination reason: Unknown % 1.05/0.49 % (1023530)Termination phase: Finite model building constraint generation % 1.05/0.49 % (1023530)Time elapsed: 0.003 s % 1.05/0.49 % (1023530)Peak memory usage: 11 MB % 1.05/0.49 % (1023530)Instructions burned: 6 (million) % 1.05/0.49 % (1023536)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=464854667:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.05/0.49 % (1023535)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4046919103:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.05/0.49 % (1023533)Instruction limit reached! % 1.05/0.49 % (1023533)------------------------------ % 1.05/0.49 % (1023533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.05/0.49 % (1023533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.05/0.49 % (1023533)CaDiCaL version: 2.1.3 % 1.05/0.49 % (1023533)Termination reason: Instruction limit % 1.05/0.49 % (1023533)Termination phase: Saturation % 1.05/0.49 % (1023533)Time elapsed: 0.025 s % 1.05/0.49 % (1023533)Peak memory usage: 11 MB % 1.05/0.49 % (1023533)Instructions burned: 105 (million) % 1.05/0.49 % (1023545)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4119759142:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 1.05/0.49 % (1023542)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1023229580:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.05/0.49 % Detected minimum model sizes of [1] % 1.05/0.49 % Detected maximum model sizes of [3] % 1.05/0.49 % TRYING [1] % 1.05/0.49 % TRYING [2] % 1.05/0.49 % Finite Model Found! % 1.05/0.49 % SZS status Satisfiable for theBenchmark % 1.05/0.49 % (1023542)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.05/0.49 % (1023542)------------------------------ % 1.05/0.49 % (1023542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.05/0.49 % (1023542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.05/0.49 % (1023542)CaDiCaL version: 2.1.3 % 1.05/0.49 % (1023542)Termination reason: Unknown % 1.05/0.49 % (1023542)Termination phase: Finite model building constraint generation % 1.05/0.49 % (1023542)Time elapsed: 0.006 s % 1.05/0.49 % (1023542)Peak memory usage: 11 MB % 1.05/0.49 % (1023542)Instructions burned: 6 (million) % 1.05/0.49 % (1023534)Instruction limit reached! % 1.05/0.49 % (1023534)------------------------------ % 1.05/0.49 % (1023534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.05/0.49 % (1023534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.05/0.49 % (1023534)CaDiCaL version: 2.1.3 % 1.05/0.49 % (1023534)Termination reason: Instruction limit % 1.05/0.49 % (1023534)Termination phase: Saturation % 3.86/0.83 % (1023534)Time elapsed: 0.049 s % 3.86/0.83 % (1023534)Peak memory usage: 11 MB % 3.86/0.83 % (1023534)Instructions burned: 124 (million) % 3.86/0.83 % (1023545)Instruction limit reached! % 3.86/0.83 % (1023545)------------------------------ % 3.86/0.83 % (1023545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.83 % (1023545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.83 % (1023545)CaDiCaL version: 2.1.3 % 3.86/0.83 % (1023545)Termination reason: Instruction limit % 3.86/0.83 % (1023545)Termination phase: Saturation % 3.86/0.83 % (1023545)Time elapsed: 0.030 s % 3.86/0.83 % (1023545)Peak memory usage: 12 MB % 3.86/0.83 % (1023545)Instructions burned: 135 (million) % 3.86/0.83 % (1023548)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=845523590:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.86/0.83 % (1023548)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.86/0.83 % (1023535)Instruction limit reached! % 3.86/0.83 % (1023535)------------------------------ % 3.86/0.83 % (1023535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.83 % (1023535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.83 % (1023535)CaDiCaL version: 2.1.3 % 3.86/0.83 % (1023535)Termination reason: Instruction limit % 3.86/0.83 % (1023535)Termination phase: Saturation % 3.86/0.83 % (1023535)Time elapsed: 0.054 s % 3.86/0.83 % (1023535)Peak memory usage: 11 MB % 3.86/0.83 % (1023535)Instructions burned: 132 (million) % 3.86/0.83 % (1023548)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 3.86/0.83 % (1023549)ott-21_1_sil=16000:fs=off:random_seed=3715125590:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.86/0.83 % (1023550)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1609099879:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.86/0.83 % (1023536)Instruction limit reached! % 3.86/0.83 % (1023536)------------------------------ % 3.86/0.83 % (1023536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.83 % (1023536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.83 % (1023536)CaDiCaL version: 2.1.3 % 3.86/0.83 % (1023536)Termination reason: Instruction limit % 3.86/0.83 % (1023536)Termination phase: Saturation % 3.86/0.83 % (1023536)Time elapsed: 0.062 s % 3.86/0.83 % (1023536)Peak memory usage: 12 MB % 3.86/0.83 % (1023536)Instructions burned: 159 (million) % 3.86/0.83 % (1023552)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1357093219:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.86/0.83 % Detected minimum model sizes of [1] % 3.86/0.83 % Detected maximum model sizes of [2] % 3.86/0.83 % TRYING [1] % 3.86/0.83 % TRYING [2] % 3.86/0.83 % Finite Model Found! % 3.86/0.83 % SZS status Satisfiable for theBenchmark % 3.86/0.83 % (1023552)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.86/0.83 % (1023552)------------------------------ % 3.86/0.83 % (1023552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.83 % (1023552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.83 % (1023552)CaDiCaL version: 2.1.3 % 3.86/0.83 % (1023552)Termination reason: Unknown % 3.86/0.83 % (1023552)Termination phase: Finite model building constraint generation % 3.86/0.83 % (1023552)Time elapsed: 0.003 s % 3.86/0.83 % (1023552)Peak memory usage: 10 MB % 3.86/0.83 % (1023552)Instructions burned: 6 (million) % 3.86/0.83 % (1023555)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=311263112:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.86/0.83 % (1023557)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=896113436:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.86/0.83 % Exception at run slice level % 3.86/0.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 3.86/0.83 % (1023560)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=346212709: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.86/0.83 % (1023560)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.86/0.83 % (1023549)Instruction limit reached! % 8.90/1.62 % (1023549)------------------------------ % 8.90/1.62 % (1023549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.62 % (1023549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.62 % (1023549)CaDiCaL version: 2.1.3 % 8.90/1.62 % (1023549)Termination reason: Instruction limit % 8.90/1.62 % (1023549)Termination phase: Saturation % 8.90/1.62 % (1023549)Time elapsed: 0.076 s % 8.90/1.62 % (1023549)Peak memory usage: 13 MB % 8.90/1.62 % (1023549)Instructions burned: 180 (million) % 8.90/1.62 % (1023562)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1034394956:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 8.90/1.62 % (1023562)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.90/1.62 % (1023550)Instruction limit reached! % 8.90/1.62 % (1023550)------------------------------ % 8.90/1.62 % (1023550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.62 % (1023550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.62 % (1023550)CaDiCaL version: 2.1.3 % 8.90/1.62 % (1023550)Termination reason: Instruction limit % 8.90/1.62 % (1023550)Termination phase: Saturation % 8.90/1.62 % (1023550)Time elapsed: 0.107 s % 8.90/1.62 % (1023550)Peak memory usage: 12 MB % 8.90/1.62 % (1023550)Instructions burned: 482 (million) % 8.90/1.62 % (1023564)fmb+10_1_sil=64000:random_seed=2516576221:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 8.90/1.62 % (1023564)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 8.90/1.62 % Detected minimum model sizes of [1] % 8.90/1.62 % Detected maximum model sizes of [2] % 8.90/1.62 % TRYING [1] % 8.90/1.62 % TRYING [2] % 8.90/1.62 % Finite Model Found! % 8.90/1.62 % SZS status Satisfiable for theBenchmark % 8.90/1.62 % (1023564)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.90/1.62 % (1023564)------------------------------ % 8.90/1.62 % (1023564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.62 % (1023564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.62 % (1023564)CaDiCaL version: 2.1.3 % 8.90/1.62 % (1023564)Termination reason: Unknown % 8.90/1.62 % (1023564)Termination phase: Finite model building constraint generation % 8.90/1.62 % (1023564)Time elapsed: 0.001 s % 8.90/1.62 % (1023564)Peak memory usage: 10 MB % 8.90/1.62 % (1023564)Instructions burned: 6 (million) % 8.90/1.62 % (1023566)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1721329955:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 8.90/1.62 % Detected minimum model sizes of [1] % 8.90/1.62 % Detected maximum model sizes of [2] % 8.90/1.62 % fmb_start_size (= 20) larger than a detected sort maximum size! % 8.90/1.62 % (1023566)Refutation not found, incomplete strategy % 8.90/1.62 % (1023566)------------------------------ % 8.90/1.62 % (1023566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.62 % (1023566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.62 % (1023566)CaDiCaL version: 2.1.3 % 8.90/1.62 % (1023566)Termination reason: Refutation not found, incomplete strategy % 8.90/1.62 % (1023566)Time elapsed: 0.001 s % 8.90/1.62 % (1023566)Peak memory usage: 10 MB % 8.90/1.62 % (1023566)Instructions burned: 6 (million) % 8.90/1.62 % (1023566)------------------------------ % 8.90/1.62 % (1023566)------------------------------ % 8.90/1.62 % (1023568)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=761070034:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 8.90/1.62 % Detected minimum model sizes of [1] % 8.90/1.62 % Detected maximum model sizes of [2] % 8.90/1.62 % fmb_start_size (= 8) larger than a detected sort maximum size! % 8.90/1.62 % (1023568)Refutation not found, incomplete strategy % 8.90/1.62 % (1023568)------------------------------ % 8.90/1.62 % (1023568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.62 % (1023568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.62 % (1023568)CaDiCaL version: 2.1.3 % 8.90/1.62 % (1023568)Termination reason: Refutation not found, incomplete strategy % 8.90/1.62 % (1023568)Time elapsed: 0.001 s % 8.90/1.62 % (1023568)Peak memory usage: 10 MB % 8.90/1.62 % (1023568)Instructions burned: 6 (million) % 8.90/1.62 % (1023568)------------------------------ % 8.90/1.62 % (1023568)------------------------------ % 8.90/1.62 % (1023570)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3955322991:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 16.08/2.62 % (1023570)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.08/2.62 % (1023560)Instruction limit reached! % 16.08/2.62 % (1023560)------------------------------ % 16.08/2.62 % (1023560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.08/2.62 % (1023560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.08/2.62 % (1023560)CaDiCaL version: 2.1.3 % 16.08/2.62 % (1023560)Termination reason: Instruction limit % 16.08/2.62 % (1023560)Termination phase: Saturation % 16.08/2.62 % (1023560)Time elapsed: 0.281 s % 16.08/2.62 % (1023560)Peak memory usage: 12 MB % 16.08/2.62 % (1023560)Instructions burned: 694 (million) % 16.08/2.62 % (1023548)Instruction limit reached! % 16.08/2.62 % (1023548)------------------------------ % 16.08/2.62 % (1023548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.08/2.62 % (1023548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.08/2.62 % (1023548)CaDiCaL version: 2.1.3 % 16.08/2.62 % (1023548)Termination reason: Instruction limit % 16.08/2.62 % (1023548)Termination phase: Saturation % 16.08/2.62 % (1023548)Time elapsed: 0.366 s % 16.08/2.62 % (1023548)Peak memory usage: 13 MB % 16.08/2.62 % (1023548)Instructions burned: 685 (million) % 16.08/2.62 % (1023572)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2126237288:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.08/2.62 % (1023572)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.08/2.62 % (1023572)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 16.08/2.62 % (1023574)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=983997373:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 16.08/2.62 % Detected minimum model sizes of [1] % 16.08/2.62 % Detected maximum model sizes of [2] % 16.08/2.62 % fmb_start_size (= 77) larger than a detected sort maximum size! % 16.08/2.62 % (1023574)Refutation not found, incomplete strategy % 16.08/2.62 % (1023574)------------------------------ % 16.08/2.62 % (1023574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.08/2.62 % (1023574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.08/2.62 % (1023574)CaDiCaL version: 2.1.3 % 16.08/2.62 % (1023574)Termination reason: Refutation not found, incomplete strategy % 16.08/2.62 % (1023574)Time elapsed: 0.003 s % 16.08/2.62 % (1023574)Peak memory usage: 10 MB % 16.08/2.62 % (1023574)Instructions burned: 6 (million) % 16.08/2.62 % (1023574)------------------------------ % 16.08/2.62 % (1023574)------------------------------ % 16.08/2.62 % (1023576)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1881006388:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 16.08/2.62 % TRYING [16] % 16.08/2.62 % Finite Model Found! % 16.08/2.62 % SZS status Satisfiable for theBenchmark % 16.08/2.62 % (1023576)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.08/2.62 % (1023576)------------------------------ % 16.08/2.62 % (1023576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.08/2.62 % (1023576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.08/2.62 % (1023576)CaDiCaL version: 2.1.3 % 16.08/2.62 % (1023576)Termination reason: Unknown % 16.08/2.62 % (1023576)Termination phase: Finite model building constraint generation % 16.08/2.62 % (1023576)Time elapsed: 0.005 s % 16.08/2.62 % (1023576)Peak memory usage: 11 MB % 16.08/2.62 % (1023576)Instructions burned: 9 (million) % 16.08/2.62 % (1023578)ott-2_1_sil=16000:newcnf=on:random_seed=1405128227:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 16.08/2.62 % (1023578)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.08/2.62 % (1023555)Instruction limit reached! % 16.08/2.62 % (1023555)------------------------------ % 16.08/2.62 % (1023555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.08/2.62 % (1023555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.08/2.62 % (1023555)CaDiCaL version: 2.1.3 % 16.08/2.62 % (1023555)Termination reason: Instruction limit % 16.08/2.62 % (1023555)Termination phase: Saturation % 16.08/2.62 % (1023555)Time elapsed: 0.453 s % 16.08/2.62 % (1023555)Peak memory usage: 12 MB % 16.08/2.62 % (1023555)Instructions burned: 1181 (million) % 16.08/2.62 % (1023580)ott+10_1_sil=32000:tgt=ground:random_seed=3947407032:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 39.57/5.81 % (1023562)Instruction limit reached! % 39.57/5.81 % (1023562)------------------------------ % 39.57/5.81 % (1023562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/5.81 % (1023562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/5.81 % (1023562)CaDiCaL version: 2.1.3 % 39.57/5.81 % (1023562)Termination reason: Instruction limit % 39.57/5.81 % (1023562)Termination phase: Saturation % 39.57/5.81 % (1023562)Time elapsed: 0.414 s % 39.57/5.81 % (1023562)Peak memory usage: 12 MB % 39.57/5.81 % (1023562)Instructions burned: 879 (million) % 39.57/5.81 % (1023582)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=189826785:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 39.57/5.81 % Detected minimum model sizes of [1] % 39.57/5.81 % Detected maximum model sizes of [2] % 39.57/5.81 % TRYING [1] % 39.57/5.81 % TRYING [2] % 39.57/5.81 % Finite Model Found! % 39.57/5.81 % SZS status Satisfiable for theBenchmark % 39.57/5.81 % (1023582)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.57/5.81 % (1023582)------------------------------ % 39.57/5.81 % (1023582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/5.81 % (1023582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/5.81 % (1023582)CaDiCaL version: 2.1.3 % 39.57/5.81 % (1023582)Termination reason: Unknown % 39.57/5.81 % (1023582)Termination phase: Finite model building constraint generation % 39.57/5.81 % (1023582)Time elapsed: 0.003 s % 39.57/5.81 % (1023582)Peak memory usage: 11 MB % 39.57/5.81 % (1023582)Instructions burned: 6 (million) % 39.57/5.81 % (1023584)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2849162474:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 39.57/5.81 % (1023584)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 39.57/5.81 % (1023578)Instruction limit reached! % 39.57/5.81 % (1023578)------------------------------ % 39.57/5.81 % (1023578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/5.81 % (1023578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/5.81 % (1023578)CaDiCaL version: 2.1.3 % 39.57/5.81 % (1023578)Termination reason: Instruction limit % 39.57/5.81 % (1023578)Termination phase: Saturation % 39.57/5.81 % (1023578)Time elapsed: 0.358 s % 39.57/5.81 % (1023578)Peak memory usage: 12 MB % 39.57/5.81 % (1023578)Instructions burned: 871 (million) % 39.57/5.81 % (1023586)dis+21_1_sil=32000:sas=cadical:random_seed=2533617614:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 39.57/5.81 % (1023572)Instruction limit reached! % 39.57/5.81 % (1023572)------------------------------ % 39.57/5.81 % (1023572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/5.81 % (1023572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/5.81 % (1023572)CaDiCaL version: 2.1.3 % 39.57/5.81 % (1023572)Termination reason: Instruction limit % 39.57/5.81 % (1023572)Termination phase: Saturation % 39.57/5.81 % (1023572)Time elapsed: 0.606 s % 39.57/5.81 % (1023572)Peak memory usage: 13 MB % 39.57/5.81 % (1023572)Instructions burned: 1476 (million) % 39.57/5.81 % (1023588)ott+11_1_sil=16000:gs=on:random_seed=794588434:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 39.57/5.81 % (1023588)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 39.57/5.81 % (1023570)Instruction limit reached! % 39.57/5.81 % (1023570)------------------------------ % 39.57/5.81 % (1023570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/5.81 % (1023570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/5.81 % (1023570)CaDiCaL version: 2.1.3 % 39.57/5.81 % (1023570)Termination reason: Instruction limit % 39.57/5.81 % (1023570)Termination phase: Saturation % 39.57/5.81 % (1023570)Time elapsed: 1.120 s % 39.57/5.81 % (1023570)Peak memory usage: 13 MB % 39.57/5.81 % (1023570)Instructions burned: 5133 (million) % 39.57/5.81 % (1023590)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3967053105:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 39.57/5.81 % Detected minimum model sizes of [1] % 39.57/5.81 % Detected maximum model sizes of [3] % 39.57/5.81 % fmb_start_size (= 7) larger than a detected sort maximum size! % 39.57/5.81 % (1023590)Refutation not found, incomplete strategy % 39.57/5.81 % (1023590)------------------------------ % 39.57/5.81 % (1023590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023590)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023590)Termination reason: Refutation not found, incomplete strategy % 86.50/12.46 % (1023590)Time elapsed: 0.001 s % 86.50/12.46 % (1023590)Peak memory usage: 10 MB % 86.50/12.46 % (1023590)Instructions burned: 6 (million) % 86.50/12.46 % (1023590)------------------------------ % 86.50/12.46 % (1023590)------------------------------ % 86.50/12.46 % (1023592)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=113497186:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi) % 86.50/12.46 % (1023588)Instruction limit reached! % 86.50/12.46 % (1023588)------------------------------ % 86.50/12.46 % (1023588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023588)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023588)Termination reason: Instruction limit % 86.50/12.46 % (1023588)Termination phase: Saturation % 86.50/12.46 % (1023588)Time elapsed: 0.799 s % 86.50/12.46 % (1023588)Peak memory usage: 12 MB % 86.50/12.46 % (1023588)Instructions burned: 2254 (million) % 86.50/12.46 % (1023594)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4233265629:i=29340_2981 on theBenchmark for (2981ds/29340Mi) % 86.50/12.46 % (1023584)Instruction limit reached! % 86.50/12.46 % (1023584)------------------------------ % 86.50/12.46 % (1023584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023584)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023584)Termination reason: Instruction limit % 86.50/12.46 % (1023584)Termination phase: Saturation % 86.50/12.46 % (1023584)Time elapsed: 1.450 s % 86.50/12.46 % (1023584)Peak memory usage: 14 MB % 86.50/12.46 % (1023584)Instructions burned: 3513 (million) % 86.50/12.46 % (1023596)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1368487208:i=5211_2978 on theBenchmark for (2978ds/5211Mi) % 86.50/12.46 % (1023592)Instruction limit reached! % 86.50/12.46 % (1023592)------------------------------ % 86.50/12.46 % (1023592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023592)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023592)Termination reason: Instruction limit % 86.50/12.46 % (1023592)Termination phase: Saturation % 86.50/12.46 % (1023592)Time elapsed: 0.959 s % 86.50/12.46 % (1023592)Peak memory usage: 13 MB % 86.50/12.46 % (1023592)Instructions burned: 4596 (million) % 86.50/12.46 % (1023598)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3999234947:i=5497:nm=2_2976 on theBenchmark for (2976ds/5497Mi) % 86.50/12.46 % Detected minimum model sizes of [1] % 86.50/12.46 % Detected maximum model sizes of [2] % 86.50/12.46 % fmb_start_size (= 17) larger than a detected sort maximum size! % 86.50/12.46 % (1023598)Refutation not found, incomplete strategy % 86.50/12.46 % (1023598)------------------------------ % 86.50/12.46 % (1023598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023598)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023598)Termination reason: Refutation not found, incomplete strategy % 86.50/12.46 % (1023598)Time elapsed: 0.001 s % 86.50/12.46 % (1023598)Peak memory usage: 10 MB % 86.50/12.46 % (1023598)Instructions burned: 6 (million) % 86.50/12.46 % (1023598)------------------------------ % 86.50/12.46 % (1023598)------------------------------ % 86.50/12.46 % (1023600)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2831651632:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 86.50/12.46 % Detected minimum model sizes of [1] % 86.50/12.46 % Detected maximum model sizes of [3] % 86.50/12.46 % fmb_start_size (= 15) larger than a detected sort maximum size! % 86.50/12.46 % (1023600)Refutation not found, incomplete strategy % 86.50/12.46 % (1023600)------------------------------ % 86.50/12.46 % (1023600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.50/12.46 % (1023600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.50/12.46 % (1023600)CaDiCaL version: 2.1.3 % 86.50/12.46 % (1023600)Termination reason: Refutation not found, incomplete strategy % 86.50/12.46 % (1023600)Time elapsed: 0.001 s % 86.50/12.46 % (1023600)Peak memory usage: 10 MB % 87.21/12.60 % (1023600)Instructions burned: 6 (million) % 87.21/12.60 % (1023600)------------------------------ % 87.21/12.60 % (1023600)------------------------------ % 87.21/12.60 % (1023602)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1195920102:i=14071_2976 on theBenchmark for (2976ds/14071Mi) % 87.21/12.60 % Detected minimum model sizes of [1] % 87.21/12.60 % Detected maximum model sizes of [2] % 87.21/12.60 % fmb_start_size (= 12) larger than a detected sort maximum size! % 87.21/12.60 % (1023602)Refutation not found, incomplete strategy % 87.21/12.60 % (1023602)------------------------------ % 87.21/12.60 % (1023602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.21/12.60 % (1023602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.21/12.60 % (1023602)CaDiCaL version: 2.1.3 % 87.21/12.60 % (1023602)Termination reason: Refutation not found, incomplete strategy % 87.21/12.60 % (1023602)Time elapsed: 0.001 s % 87.21/12.60 % (1023602)Peak memory usage: 10 MB % 87.21/12.60 % (1023602)Instructions burned: 6 (million) % 87.21/12.60 % (1023602)------------------------------ % 87.21/12.60 % (1023602)------------------------------ % 87.21/12.60 % (1023604)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=755697942:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi) % 87.21/12.60 % (1023586)Instruction limit reached! % 87.21/12.60 % (1023586)------------------------------ % 87.21/12.60 % (1023586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.21/12.60 % (1023586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.21/12.60 % (1023586)CaDiCaL version: 2.1.3 % 87.21/12.60 % (1023586)Termination reason: Instruction limit % 87.21/12.60 % (1023586)Termination phase: Saturation % 87.21/12.60 % (1023586)Time elapsed: 1.538 s % 87.21/12.60 % (1023586)Peak memory usage: 15 MB % 87.21/12.60 % (1023586)Instructions burned: 3774 (million) % 87.21/12.60 % (1023606)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1254748284:i=8173:av=off_2975 on theBenchmark for (2975ds/8173Mi) % 87.21/12.60 % (1023580)Instruction limit reached! % 87.21/12.60 % (1023580)------------------------------ % 87.21/12.60 % (1023580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.21/12.60 % (1023580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.21/12.60 % (1023580)CaDiCaL version: 2.1.3 % 87.21/12.60 % (1023580)Termination reason: Instruction limit % 87.21/12.60 % (1023580)Termination phase: Saturation % 87.21/12.60 % (1023580)Time elapsed: 1.874 s % 87.21/12.60 % (1023580)Peak memory usage: 12 MB % 87.21/12.60 % (1023580)Instructions burned: 5120 (million) % 87.21/12.60 % (1023608)dis+10_16:1_sil=16000:random_seed=2072360318:i=9155:fsr=off_2975 on theBenchmark for (2975ds/9155Mi) % 87.21/12.60 % (1023596)Instruction limit reached! % 87.21/12.60 % (1023596)------------------------------ % 87.21/12.60 % (1023596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.21/12.60 % (1023596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.21/12.60 % (1023596)CaDiCaL version: 2.1.3 % 87.21/12.60 % (1023596)Termination reason: Instruction limit % 87.21/12.60 % (1023596)Termination phase: Saturation % 87.21/12.60 % (1023596)Time elapsed: 2.087 s % 87.21/12.60 % (1023596)Peak memory usage: 16 MB % 87.21/12.60 % (1023596)Instructions burned: 5214 (million) % 87.21/12.60 % (1023610)ott-3_8_sil=64000:random_seed=2994089119:i=20139:bs=on_2957 on theBenchmark for (2957ds/20139Mi) % 87.21/12.60 % (1023606)Instruction limit reached! % 87.21/12.60 % (1023606)------------------------------ % 87.21/12.60 % (1023606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.21/12.60 % (1023606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.21/12.60 % (1023606)CaDiCaL version: 2.1.3 % 87.21/12.60 % (1023606)Termination reason: Instruction limit % 87.21/12.60 % (1023606)Termination phase: Saturation % 87.21/12.60 % (1023606)Time elapsed: 3.091 s % 87.21/12.60 % (1023606)Peak memory usage: 12 MB % 87.21/12.60 % (1023606)Instructions burned: 8173 (million) % 87.21/12.60 % (1023612)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1565320380:fmbsr=2:i=32576_2944 on theBenchmark for (2944ds/32576Mi) % 87.21/12.60 % Detected minimum model sizes of [1] % 87.21/12.60 % Detected maximum model sizes of [2] % 87.21/12.60 % fmb_start_size (= 9) larger than a detected sort maximum size! % 87.21/12.60 % (1023612)Refutation not found, incomplete strategy % 87.21/12.60 % (1023612)------------------------------ % 87.21/12.60 % (1023612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023612)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023612)Termination reason: Refutation not found, incomplete strategy % 96.46/13.89 % (1023612)Time elapsed: 0.003 s % 96.46/13.89 % (1023612)Peak memory usage: 10 MB % 96.46/13.89 % (1023612)Instructions burned: 6 (million) % 96.46/13.89 % (1023612)------------------------------ % 96.46/13.89 % (1023612)------------------------------ % 96.46/13.89 % (1023614)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3483059217:i=11404_2944 on theBenchmark for (2944ds/11404Mi) % 96.46/13.89 % (1023604)Instruction limit reached! % 96.46/13.89 % (1023604)------------------------------ % 96.46/13.89 % (1023604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023604)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023604)Termination reason: Instruction limit % 96.46/13.89 % (1023604)Termination phase: Saturation % 96.46/13.89 % (1023604)Time elapsed: 3.312 s % 96.46/13.89 % (1023604)Peak memory usage: 14 MB % 96.46/13.89 % (1023604)Instructions burned: 22573 (million) % 96.46/13.89 % (1023616)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3944966303:i=14134_2942 on theBenchmark for (2942ds/14134Mi) % 96.46/13.89 % (1023616)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 96.46/13.89 % (1023608)Instruction limit reached! % 96.46/13.89 % (1023608)------------------------------ % 96.46/13.89 % (1023608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023608)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023608)Termination reason: Instruction limit % 96.46/13.89 % (1023608)Termination phase: Saturation % 96.46/13.89 % (1023608)Time elapsed: 3.377 s % 96.46/13.89 % (1023608)Peak memory usage: 16 MB % 96.46/13.89 % (1023608)Instructions burned: 9155 (million) % 96.46/13.89 % (1023618)dis+33_16_sil=32000:sac=on:random_seed=3211559703:i=15851:nm=0_2941 on theBenchmark for (2941ds/15851Mi) % 96.46/13.89 % (1023616)Instruction limit reached! % 96.46/13.89 % (1023616)------------------------------ % 96.46/13.89 % (1023616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023616)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023616)Termination reason: Instruction limit % 96.46/13.89 % (1023616)Termination phase: Saturation % 96.46/13.89 % (1023616)Time elapsed: 2.837 s % 96.46/13.89 % (1023616)Peak memory usage: 12 MB % 96.46/13.89 % (1023616)Instructions burned: 14142 (million) % 96.46/13.89 % (1023620)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=81503481:avsq=on:i=17627:add=on:amm=off_2914 on theBenchmark for (2914ds/17627Mi) % 96.46/13.89 % (1023614)Instruction limit reached! % 96.46/13.89 % (1023614)------------------------------ % 96.46/13.89 % (1023614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023614)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023614)Termination reason: Instruction limit % 96.46/13.89 % (1023614)Termination phase: Saturation % 96.46/13.89 % (1023614)Time elapsed: 4.394 s % 96.46/13.89 % (1023614)Peak memory usage: 13 MB % 96.46/13.89 % (1023614)Instructions burned: 11405 (million) % 96.46/13.89 % (1023622)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=619421638:s2a=on:i=53295_2900 on theBenchmark for (2900ds/53295Mi) % 96.46/13.89 % (1023610)Instruction limit reached! % 96.46/13.89 % (1023610)------------------------------ % 96.46/13.89 % (1023610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.46/13.89 % (1023610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/13.89 % (1023610)CaDiCaL version: 2.1.3 % 96.46/13.89 % (1023610)Termination reason: Instruction limit % 96.46/13.89 % (1023610)Termination phase: Saturation % 96.46/13.89 % (1023610)Time elapsed: 7.977 s % 96.46/13.89 % (1023610)Peak memory usage: 14 MB % 96.46/13.89 % (1023610)Instructions burned: 20140 (million) % 96.46/13.89 % (1023624)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1280160959:i=26857:ins=20_2877 on theBenchmark for (2877ds/26857Mi) % 96.46/13.89 % Detected minimum model sizes of [1] % 96.46/13.89 % Detected maximum model sizes of [2] % 96.46/13.89 % fmb_start_size (= 16) larger than a detected sort maximum size! % 96.46/13.89 % (1023624)Refutation not found, incomplete strategy % 101.37/14.54 % (1023624)------------------------------ % 101.37/14.54 % (1023624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.37/14.54 % (1023624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.37/14.54 % (1023624)CaDiCaL version: 2.1.3 % 101.37/14.54 % (1023624)Termination reason: Refutation not found, incomplete strategy % 101.37/14.54 % (1023624)Time elapsed: 0.003 s % 101.37/14.54 % (1023624)Peak memory usage: 10 MB % 101.37/14.54 % (1023624)Instructions burned: 6 (million) % 101.37/14.54 % (1023624)------------------------------ % 101.37/14.54 % (1023624)------------------------------ % 101.37/14.54 % (1023626)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=195985688:i=28120:bs=on:fsr=off_2877 on theBenchmark for (2877ds/28120Mi) % 101.37/14.54 % (1023618)Instruction limit reached! % 101.37/14.54 % (1023618)------------------------------ % 101.37/14.54 % (1023618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.37/14.54 % (1023618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.37/14.54 % (1023618)CaDiCaL version: 2.1.3 % 101.37/14.54 % (1023618)Termination reason: Instruction limit % 101.37/14.54 % (1023618)Termination phase: Saturation % 101.37/14.54 % (1023618)Time elapsed: 6.391 s % 101.37/14.54 % (1023618)Peak memory usage: 14 MB % 101.37/14.54 % (1023618)Instructions burned: 15853 (million) % 101.37/14.54 % (1023628)fmb+10_1_sil=256000:fmbss=7:random_seed=3959861982:fmbsr=1.6:i=182295_2877 on theBenchmark for (2877ds/182295Mi) % 101.37/14.54 % Detected minimum model sizes of [1] % 101.37/14.54 % Detected maximum model sizes of [2] % 101.37/14.54 % fmb_start_size (= 7) larger than a detected sort maximum size! % 101.37/14.54 % (1023628)Refutation not found, incomplete strategy % 101.37/14.54 % (1023628)------------------------------ % 101.37/14.54 % (1023628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.37/14.54 % (1023628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.37/14.54 % (1023628)CaDiCaL version: 2.1.3 % 101.37/14.54 % (1023628)Termination reason: Refutation not found, incomplete strategy % 101.37/14.54 % (1023628)Time elapsed: 0.003 s % 101.37/14.54 % (1023628)Peak memory usage: 10 MB % 101.37/14.54 % (1023628)Instructions burned: 6 (million) % 101.37/14.54 % (1023628)------------------------------ % 101.37/14.54 % (1023628)------------------------------ % 101.37/14.54 % (1023630)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=423023737:i=44625:gsp=on_2876 on theBenchmark for (2876ds/44625Mi) % 101.37/14.54 % (1023630)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 101.37/14.54 % (1023630)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 101.37/14.54 % Detected minimum model sizes of [1] % 101.37/14.54 % Detected maximum model sizes of [2] % 101.37/14.54 % fmb_start_size (= 21) larger than a detected sort maximum size! % 101.37/14.54 % (1023630)Refutation not found, incomplete strategy % 101.37/14.54 % (1023630)------------------------------ % 101.37/14.54 % (1023630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.37/14.54 % (1023630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.37/14.54 % (1023630)CaDiCaL version: 2.1.3 % 101.37/14.54 % (1023630)Termination reason: Refutation not found, incomplete strategy % 101.37/14.54 % (1023630)Time elapsed: 0.003 s % 101.37/14.54 % (1023630)Peak memory usage: 10 MB % 101.37/14.54 % (1023630)Instructions burned: 6 (million) % 101.37/14.54 % (1023630)------------------------------ % 101.37/14.54 % (1023630)------------------------------ % 101.37/14.54 % (1023632)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3179784851:i=160505_2876 on theBenchmark for (2876ds/160505Mi) % 101.37/14.54 % Detected minimum model sizes of [1] % 101.37/14.54 % Detected maximum model sizes of [2] % 101.37/14.54 % fmb_start_size (= 15) larger than a detected sort maximum size! % 101.37/14.54 % (1023632)Refutation not found, incomplete strategy % 101.37/14.54 % (1023632)------------------------------ % 101.37/14.54 % (1023632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.37/14.54 % (1023632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.37/14.54 % (1023632)CaDiCaL version: 2.1.3 % 101.37/14.54 % (1023632)Termination reason: Refutation not found, incomplete strategy % 101.37/14.54 % (1023632)Time elapsed: 0.003 s % 101.37/14.54 % (1023632)Peak memory usage: 10 MB % 101.37/14.54 % (1023632)Instructions burned: 6 (million) % 101.37/14.54 % (1023632)------------------------------ % 101.37/14.54 % (1023632)------------------------------ % 101.37/14.54 % (1023634)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=300934610:fmbsr=1.3:i=225729_2876 on theBenchmark for (2876ds/225729Mi) % 116.37/16.69 % Detected minimum model sizes of [1] % 116.37/16.69 % Detected maximum model sizes of [2] % 116.37/16.69 % fmb_start_size (= 10) larger than a detected sort maximum size! % 116.37/16.69 % (1023634)Refutation not found, incomplete strategy % 116.37/16.69 % (1023634)------------------------------ % 116.37/16.69 % (1023634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.37/16.69 % (1023634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.37/16.69 % (1023634)CaDiCaL version: 2.1.3 % 116.37/16.69 % (1023634)Termination reason: Refutation not found, incomplete strategy % 116.37/16.69 % (1023634)Time elapsed: 0.003 s % 116.37/16.69 % (1023634)Peak memory usage: 10 MB % 116.37/16.69 % (1023634)Instructions burned: 6 (million) % 116.37/16.69 % (1023634)------------------------------ % 116.37/16.69 % (1023634)------------------------------ % 116.37/16.69 % (1023636)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2094853996:fmbsr=2:i=185024:ins=7_2876 on theBenchmark for (2876ds/185024Mi) % 116.37/16.69 % Detected minimum model sizes of [1] % 116.37/16.69 % Detected maximum model sizes of [2] % 116.37/16.69 % fmb_start_size (= 10) larger than a detected sort maximum size! % 116.37/16.69 % (1023636)Refutation not found, incomplete strategy % 116.37/16.69 % (1023636)------------------------------ % 116.37/16.69 % (1023636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.37/16.69 % (1023636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.37/16.69 % (1023636)CaDiCaL version: 2.1.3 % 116.37/16.69 % (1023636)Termination reason: Refutation not found, incomplete strategy % 116.37/16.69 % (1023636)Time elapsed: 0.003 s % 116.37/16.69 % (1023636)Peak memory usage: 10 MB % 116.37/16.69 % (1023636)Instructions burned: 6 (million) % 116.37/16.69 % (1023636)------------------------------ % 116.37/16.69 % (1023636)------------------------------ % 116.37/16.69 % (1023638)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=488024012:rtra=on_2876 on theBenchmark for (2876ds/0Mi) % 116.37/16.69 % Detected minimum model sizes of [1] % 116.37/16.69 % Detected maximum model sizes of [2] % 116.37/16.69 % TRYING [1] % 116.37/16.69 % TRYING [2] % 116.37/16.69 % Finite Model Found! % 116.37/16.69 % SZS status Satisfiable for theBenchmark % 116.37/16.69 % (1023638)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.37/16.69 % (1023638)------------------------------ % 116.37/16.69 % (1023638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.37/16.69 % (1023638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.37/16.69 % (1023638)CaDiCaL version: 2.1.3 % 116.37/16.69 % (1023638)Termination reason: Unknown % 116.37/16.69 % (1023638)Termination phase: Finite model building constraint generation % 116.37/16.69 % (1023638)Time elapsed: 0.003 s % 116.37/16.69 % (1023638)Peak memory usage: 11 MB % 116.37/16.69 % (1023638)Instructions burned: 6 (million) % 116.37/16.69 % (1023640)% WARNING: option uhcvi not known. % 116.37/16.69 % (1023640)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2288225792:i=271062:add=off:rtra=on:rawr=on_2875 on theBenchmark for (2875ds/271062Mi) % 116.37/16.69 % (1023640)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 116.37/16.69 % (1023640)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 116.37/16.69 % (1023620)Instruction limit reached! % 116.37/16.69 % (1023620)------------------------------ % 116.37/16.69 % (1023620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.37/16.69 % (1023620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.37/16.69 % (1023620)CaDiCaL version: 2.1.3 % 116.37/16.69 % (1023620)Termination reason: Instruction limit % 116.37/16.69 % (1023620)Termination phase: Saturation % 116.37/16.69 % (1023620)Time elapsed: 3.953 s % 116.37/16.69 % (1023620)Peak memory usage: 22 MB % 116.37/16.69 % (1023620)Instructions burned: 17629 (million) % 116.37/16.69 % (1023642)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3779492081:i=176048:add=on:rtra=on:rawr=on_2874 on theBenchmark for (2874ds/176048Mi) % 116.37/16.69 % (1023594)Instruction limit reached! % 116.37/16.69 % (1023594)------------------------------ % 116.37/16.69 % (1023594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.37/16.69 % (1023594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.37/16.69 % (1023594)CaDiCaL version: 2.1.3 % 116.37/16.69 % (1023594)Termination reason: Instruction limit % 125.01/18.00 % (1023594)Termination phase: Saturation % 125.01/18.00 % (1023594)Time elapsed: 11.751 s % 125.01/18.00 % (1023594)Peak memory usage: 16 MB % 125.01/18.00 % (1023594)Instructions burned: 29340 (million) % 125.01/18.00 % (1023644)dis+10_1_sil=32000:si=on:sp=arity:random_seed=119187832:i=206:fgj=on:rtra=on_2863 on theBenchmark for (2863ds/206Mi) % 125.01/18.00 % (1023644)Instruction limit reached! % 125.01/18.00 % (1023644)------------------------------ % 125.01/18.00 % (1023644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.01/18.00 % (1023644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.01/18.00 % (1023644)CaDiCaL version: 2.1.3 % 125.01/18.00 % (1023644)Termination reason: Instruction limit % 125.01/18.00 % (1023644)Termination phase: Saturation % 125.01/18.00 % (1023644)Time elapsed: 0.091 s % 125.01/18.00 % (1023644)Peak memory usage: 12 MB % 125.01/18.00 % (1023644)Instructions burned: 206 (million) % 125.01/18.00 % (1023646)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1903579501:i=232:rtra=on_2862 on theBenchmark for (2862ds/232Mi) % 125.01/18.00 % (1023646)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 125.01/18.00 % (1023646)Instruction limit reached! % 125.01/18.00 % (1023646)------------------------------ % 125.01/18.00 % (1023646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.01/18.00 % (1023646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.01/18.00 % (1023646)CaDiCaL version: 2.1.3 % 125.01/18.00 % (1023646)Termination reason: Instruction limit % 125.01/18.00 % (1023646)Termination phase: Saturation % 125.01/18.00 % (1023646)Time elapsed: 0.096 s % 125.01/18.00 % (1023646)Peak memory usage: 12 MB % 125.01/18.00 % (1023646)Instructions burned: 234 (million) % 125.01/18.00 % (1023648)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=199484980:i=262:rtra=on_2861 on theBenchmark for (2861ds/262Mi) % 125.01/18.00 % (1023648)Instruction limit reached! % 125.01/18.00 % (1023648)------------------------------ % 125.01/18.00 % (1023648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.01/18.00 % (1023648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.01/18.00 % (1023648)CaDiCaL version: 2.1.3 % 125.01/18.00 % (1023648)Termination reason: Instruction limit % 125.01/18.00 % (1023648)Termination phase: Saturation % 125.01/18.00 % (1023648)Time elapsed: 0.106 s % 125.01/18.00 % (1023648)Peak memory usage: 12 MB % 125.01/18.00 % (1023648)Instructions burned: 263 (million) % 125.01/18.00 % (1023650)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1326188569:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2859 on theBenchmark for (2859ds/318Mi) % 125.01/18.00 % (1023650)Instruction limit reached! % 125.01/18.00 % (1023650)------------------------------ % 125.01/18.00 % (1023650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.01/18.00 % (1023650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.01/18.00 % (1023650)CaDiCaL version: 2.1.3 % 125.01/18.00 % (1023650)Termination reason: Instruction limit % 125.01/18.00 % (1023650)Termination phase: Saturation % 125.01/18.00 % (1023650)Time elapsed: 0.124 s % 125.01/18.00 % (1023650)Peak memory usage: 12 MB % 125.01/18.00 % (1023650)Instructions burned: 320 (million) % 125.01/18.00 % (1023652)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=690918334:i=1428:nm=2:rtra=on_2858 on theBenchmark for (2858ds/1428Mi) % 125.01/18.00 % Detected minimum model sizes of [1] % 125.01/18.00 % Detected maximum model sizes of [3] % 125.01/18.00 % TRYING [1] % 125.01/18.00 % TRYING [2] % 125.01/18.00 % Finite Model Found! % 125.01/18.00 % SZS status Satisfiable for theBenchmark % 125.01/18.00 % (1023652)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 125.01/18.00 % (1023652)------------------------------ % 125.01/18.00 % (1023652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.01/18.00 % (1023652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.01/18.00 % (1023652)CaDiCaL version: 2.1.3 % 125.01/18.00 % (1023652)Termination reason: Unknown % 125.01/18.00 % (1023652)Termination phase: Finite model building constraint generation % 125.01/18.00 % (1023652)Time elapsed: 0.004 s % 125.01/18.00 % (1023652)Peak memory usage: 11 MB % 125.01/18.00 % (1023652)Instructions burned: 6 (million) % 125.01/18.00 % (1023654)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2065752666:i=262:bd=preordered:rtra=on:fsd=on_2858 on theBenchmark for (2858ds/262Mi) % 125.01/18.00 % (1023654)Instruction limit reached! % 125.01/18.00 % (1023654)------------------------------ % 125.01/18.00 % (1023654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023654)CaDiCaL version: 2.1.3 % 155.93/22.17 % (1023654)Termination reason: Instruction limit % 155.93/22.17 % (1023654)Termination phase: Saturation % 155.93/22.17 % (1023654)Time elapsed: 0.109 s % 155.93/22.17 % (1023654)Peak memory usage: 12 MB % 155.93/22.17 % (1023654)Instructions burned: 263 (million) % 155.93/22.17 % (1023656)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=3537497505:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/1368Mi) % 155.93/22.17 % (1023656)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 155.93/22.17 % (1023656)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 155.93/22.17 % (1023656)Instruction limit reached! % 155.93/22.17 % (1023656)------------------------------ % 155.93/22.17 % (1023656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023656)CaDiCaL version: 2.1.3 % 155.93/22.17 % (1023656)Termination reason: Instruction limit % 155.93/22.17 % (1023656)Termination phase: Saturation % 155.93/22.17 % (1023656)Time elapsed: 0.601 s % 155.93/22.17 % (1023656)Peak memory usage: 14 MB % 155.93/22.17 % (1023656)Instructions burned: 1369 (million) % 155.93/22.17 % (1023658)ott-21_1_sil=16000:si=on:fs=off:random_seed=667218086:i=360:av=off:fsr=off:rtra=on_2850 on theBenchmark for (2850ds/360Mi) % 155.93/22.17 % (1023658)Instruction limit reached! % 155.93/22.17 % (1023658)------------------------------ % 155.93/22.17 % (1023658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023658)CaDiCaL version: 2.1.3 % 155.93/22.17 % (1023658)Termination reason: Instruction limit % 155.93/22.17 % (1023658)Termination phase: Saturation % 155.93/22.17 % (1023658)Time elapsed: 0.154 s % 155.93/22.17 % (1023658)Peak memory usage: 14 MB % 155.93/22.17 % (1023658)Instructions burned: 362 (million) % 155.93/22.17 % (1023660)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3645896028:i=954:bd=all:rtra=on_2848 on theBenchmark for (2848ds/954Mi) % 155.93/22.17 % (1023660)Instruction limit reached! % 155.93/22.17 % (1023660)------------------------------ % 155.93/22.17 % (1023660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023660)CaDiCaL version: 2.1.3 % 155.93/22.17 % (1023660)Termination reason: Instruction limit % 155.93/22.17 % (1023660)Termination phase: Saturation % 155.93/22.17 % (1023660)Time elapsed: 0.410 s % 155.93/22.17 % (1023660)Peak memory usage: 12 MB % 155.93/22.17 % (1023660)Instructions burned: 955 (million) % 155.93/22.17 % (1023662)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2729746340:fmbsr=1.3:i=1730:ins=25:rtra=on_2844 on theBenchmark for (2844ds/1730Mi) % 155.93/22.17 % Detected minimum model sizes of [1] % 155.93/22.17 % Detected maximum model sizes of [2] % 155.93/22.17 % TRYING [1] % 155.93/22.17 % TRYING [2] % 155.93/22.17 % Finite Model Found! % 155.93/22.17 % SZS status Satisfiable for theBenchmark % 155.93/22.17 % (1023662)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 155.93/22.17 % (1023662)------------------------------ % 155.93/22.17 % (1023662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023662)CaDiCaL version: 2.1.3 % 155.93/22.17 % (1023662)Termination reason: Unknown % 155.93/22.17 % (1023662)Termination phase: Finite model building constraint generation % 155.93/22.17 % (1023662)Time elapsed: 0.003 s % 155.93/22.17 % (1023662)Peak memory usage: 10 MB % 155.93/22.17 % (1023662)Instructions burned: 6 (million) % 155.93/22.17 % (1023664)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=169523354:i=2358:rtra=on_2844 on theBenchmark for (2844ds/2358Mi) % 155.93/22.17 % (1023664)Instruction limit reached! % 155.93/22.17 % (1023664)------------------------------ % 155.93/22.17 % (1023664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.93/22.17 % (1023664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.93/22.17 % (1023664)CaDiCaL version: 2.1.3 % 181.80/25.86 % (1023664)Termination reason: Instruction limit % 181.80/25.86 % (1023664)Termination phase: Saturation % 181.80/25.86 % (1023664)Time elapsed: 0.881 s % 181.80/25.86 % (1023664)Peak memory usage: 12 MB % 181.80/25.86 % (1023664)Instructions burned: 2360 (million) % 181.80/25.86 % (1023666)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4208084627:i=1778:ins=1:rtra=on_2835 on theBenchmark for (2835ds/1778Mi) % 181.80/25.86 % Exception at run slice level % 181.80/25.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.80/25.86 % (1023668)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=772383342:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/1384Mi) % 181.80/25.86 % (1023668)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 181.80/25.86 % (1023668)Instruction limit reached! % 181.80/25.86 % (1023668)------------------------------ % 181.80/25.86 % (1023668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/25.86 % (1023668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/25.86 % (1023668)CaDiCaL version: 2.1.3 % 181.80/25.86 % (1023668)Termination reason: Instruction limit % 181.80/25.86 % (1023668)Termination phase: Saturation % 181.80/25.86 % (1023668)Time elapsed: 0.544 s % 181.80/25.86 % (1023668)Peak memory usage: 13 MB % 181.80/25.86 % (1023668)Instructions burned: 1385 (million) % 181.80/25.86 % (1023670)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3863065079:i=1758:kws=inv_precedence:fsr=off:rtra=on_2829 on theBenchmark for (2829ds/1758Mi) % 181.80/25.86 % (1023670)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 181.80/25.86 % (1023670)Instruction limit reached! % 181.80/25.86 % (1023670)------------------------------ % 181.80/25.86 % (1023670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/25.86 % (1023670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/25.86 % (1023670)CaDiCaL version: 2.1.3 % 181.80/25.86 % (1023670)Termination reason: Instruction limit % 181.80/25.86 % (1023670)Termination phase: Saturation % 181.80/25.86 % (1023670)Time elapsed: 0.630 s % 181.80/25.86 % (1023670)Peak memory usage: 12 MB % 181.80/25.86 % (1023670)Instructions burned: 1761 (million) % 181.80/25.86 % (1023672)fmb+10_1_sil=64000:si=on:random_seed=3256270858:i=44122:nm=2:rtra=on:gsp=on_2822 on theBenchmark for (2822ds/44122Mi) % 181.80/25.86 % (1023672)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 181.80/25.86 % Detected minimum model sizes of [1] % 181.80/25.86 % Detected maximum model sizes of [2] % 181.80/25.86 % TRYING [1] % 181.80/25.86 % TRYING [2] % 181.80/25.86 % Finite Model Found! % 181.80/25.86 % SZS status Satisfiable for theBenchmark % 181.80/25.86 % (1023672)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 181.80/25.86 % (1023672)------------------------------ % 181.80/25.86 % (1023672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/25.86 % (1023672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/25.86 % (1023672)CaDiCaL version: 2.1.3 % 181.80/25.86 % (1023672)Termination reason: Unknown % 181.80/25.86 % (1023672)Termination phase: Finite model building constraint generation % 181.80/25.86 % (1023672)Time elapsed: 0.003 s % 181.80/25.86 % (1023672)Peak memory usage: 10 MB % 181.80/25.86 % (1023672)Instructions burned: 6 (million) % 181.80/25.86 % (1023674)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1159792353:i=19030:nm=5:rtra=on_2822 on theBenchmark for (2822ds/19030Mi) % 181.80/25.86 % Detected minimum model sizes of [1] % 181.80/25.86 % Detected maximum model sizes of [2] % 181.80/25.86 % fmb_start_size (= 20) larger than a detected sort maximum size! % 181.80/25.86 % (1023674)Refutation not found, incomplete strategy % 181.80/25.86 % (1023674)------------------------------ % 181.80/25.86 % (1023674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/25.86 % (1023674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/25.86 % (1023674)CaDiCaL version: 2.1.3 % 181.80/25.86 % (1023674)Termination reason: Refutation not found, incomplete strategy % 181.80/25.86 % (1023674)Time elapsed: 0.003 s % 181.80/25.86 % (1023674)Peak memory usage: 10 MB % 181.80/25.86 % (1023674)Instructions burned: 6 (million) % 181.80/25.86 % (1023674)------------------------------ % 181.80/25.86 % (1023674)------------------------------ % 181.80/25.86 % (1023676)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=649341321:fmbsr=1.7:i=1840:rtra=on_2822 on theBenchmark for (2822ds/1840Mi) % 210.97/29.97 % Detected minimum model sizes of [1] % 210.97/29.97 % Detected maximum model sizes of [2] % 210.97/29.97 % fmb_start_size (= 8) larger than a detected sort maximum size! % 210.97/29.97 % (1023676)Refutation not found, incomplete strategy % 210.97/29.97 % (1023676)------------------------------ % 210.97/29.97 % (1023676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.97/29.97 % (1023676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.97/29.97 % (1023676)CaDiCaL version: 2.1.3 % 210.97/29.97 % (1023676)Termination reason: Refutation not found, incomplete strategy % 210.97/29.97 % (1023676)Time elapsed: 0.003 s % 210.97/29.97 % (1023676)Peak memory usage: 10 MB % 210.97/29.97 % (1023676)Instructions burned: 6 (million) % 210.97/29.97 % (1023676)------------------------------ % 210.97/29.97 % (1023676)------------------------------ % 210.97/29.97 % (1023678)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1227927080:i=10262:rtra=on_2822 on theBenchmark for (2822ds/10262Mi) % 210.97/29.97 % (1023678)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 210.97/29.97 % (1023626)Instruction limit reached! % 210.97/29.97 % (1023626)------------------------------ % 210.97/29.97 % (1023626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.97/29.97 % (1023626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.97/29.97 % (1023626)CaDiCaL version: 2.1.3 % 210.97/29.97 % (1023626)Termination reason: Instruction limit % 210.97/29.97 % (1023626)Termination phase: Saturation % 210.97/29.97 % (1023626)Time elapsed: 9.098 s % 210.97/29.97 % (1023626)Peak memory usage: 16 MB % 210.97/29.97 % (1023626)Instructions burned: 28122 (million) % 210.97/29.97 % (1023681)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2036714513:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2786 on theBenchmark for (2786ds/2944Mi) % 210.97/29.97 % (1023681)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 210.97/29.97 % (1023681)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 210.97/29.97 % (1023678)Instruction limit reached! % 210.97/29.97 % (1023678)------------------------------ % 210.97/29.97 % (1023678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.97/29.97 % (1023678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.97/29.97 % (1023678)CaDiCaL version: 2.1.3 % 210.97/29.97 % (1023678)Termination reason: Instruction limit % 210.97/29.97 % (1023678)Termination phase: Saturation % 210.97/29.97 % (1023678)Time elapsed: 4.099 s % 210.97/29.97 % (1023678)Peak memory usage: 13 MB % 210.97/29.97 % (1023678)Instructions burned: 10262 (million) % 210.97/29.97 % (1023683)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1475293807:i=12648:rtra=on_2781 on theBenchmark for (2781ds/12648Mi) % 210.97/29.97 % Detected minimum model sizes of [1] % 210.97/29.97 % Detected maximum model sizes of [2] % 210.97/29.97 % fmb_start_size (= 77) larger than a detected sort maximum size! % 210.97/29.97 % (1023683)Refutation not found, incomplete strategy % 210.97/29.97 % (1023683)------------------------------ % 210.97/29.97 % (1023683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.97/29.97 % (1023683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.97/29.97 % (1023683)CaDiCaL version: 2.1.3 % 210.97/29.97 % (1023683)Termination reason: Refutation not found, incomplete strategy % 210.97/29.97 % (1023683)Time elapsed: 0.003 s % 210.97/29.97 % (1023683)Peak memory usage: 10 MB % 210.97/29.97 % (1023683)Instructions burned: 6 (million) % 210.97/29.97 % (1023683)------------------------------ % 210.97/29.97 % (1023683)------------------------------ % 210.97/29.97 % (1023685)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2977873093:fmbsr=2.30978:i=4348:rtra=on_2780 on theBenchmark for (2780ds/4348Mi) % 210.97/29.97 % TRYING [16] % 210.97/29.97 % Finite Model Found! % 210.97/29.97 % SZS status Satisfiable for theBenchmark % 210.97/29.97 % (1023685)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 210.97/29.97 % (1023685)------------------------------ % 210.97/29.97 % (1023685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.97/29.97 % (1023685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.97/29.97 % (1023685)CaDiCaL version: 2.1.3 % 210.97/29.97 % (1023685)Termination reason: Unknown % 257.19/36.40 % (1023685)Termination phase: Finite model building constraint generation % 257.19/36.40 % (1023685)Time elapsed: 0.005 s % 257.19/36.40 % (1023685)Peak memory usage: 11 MB % 257.19/36.40 % (1023685)Instructions burned: 10 (million) % 257.19/36.40 % (1023687)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=270053826:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2780 on theBenchmark for (2780ds/1738Mi) % 257.19/36.40 % (1023687)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 257.19/36.40 % (1023681)Instruction limit reached! % 257.19/36.40 % (1023681)------------------------------ % 257.19/36.40 % (1023681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.19/36.40 % (1023681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.19/36.40 % (1023681)CaDiCaL version: 2.1.3 % 257.19/36.40 % (1023681)Termination reason: Instruction limit % 257.19/36.40 % (1023681)Termination phase: Saturation % 257.19/36.40 % (1023681)Time elapsed: 1.197 s % 257.19/36.40 % (1023681)Peak memory usage: 14 MB % 257.19/36.40 % (1023681)Instructions burned: 2948 (million) % 257.19/36.40 % (1023689)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=216857586:i=10228:av=off:rtra=on_2774 on theBenchmark for (2774ds/10228Mi) % 257.19/36.40 % (1023687)Instruction limit reached! % 257.19/36.40 % (1023687)------------------------------ % 257.19/36.40 % (1023687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.19/36.40 % (1023687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.19/36.40 % (1023687)CaDiCaL version: 2.1.3 % 257.19/36.40 % (1023687)Termination reason: Instruction limit % 257.19/36.40 % (1023687)Termination phase: Saturation % 257.19/36.40 % (1023687)Time elapsed: 0.705 s % 257.19/36.40 % (1023687)Peak memory usage: 13 MB % 257.19/36.40 % (1023687)Instructions burned: 1739 (million) % 257.19/36.40 % (1023691)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1173492779:i=108564:rtra=on_2773 on theBenchmark for (2773ds/108564Mi) % 257.19/36.40 % Detected minimum model sizes of [1] % 257.19/36.40 % Detected maximum model sizes of [2] % 257.19/36.40 % TRYING [1] % 257.19/36.40 % TRYING [2] % 257.19/36.40 % Finite Model Found! % 257.19/36.40 % SZS status Satisfiable for theBenchmark % 257.19/36.40 % (1023691)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 257.19/36.40 % (1023691)------------------------------ % 257.19/36.40 % (1023691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.19/36.40 % (1023691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.19/36.40 % (1023691)CaDiCaL version: 2.1.3 % 257.19/36.40 % (1023691)Termination reason: Unknown % 257.19/36.40 % (1023691)Termination phase: Finite model building constraint generation % 257.19/36.40 % (1023691)Time elapsed: 0.003 s % 257.19/36.40 % (1023691)Peak memory usage: 11 MB % 257.19/36.40 % (1023691)Instructions burned: 6 (million) % 257.19/36.40 % (1023693)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2371630533:i=7024:aac=none:rtra=on_2773 on theBenchmark for (2773ds/7024Mi) % 257.19/36.40 % (1023693)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 257.19/36.40 % (1023532)Instruction limit reached! % 257.19/36.40 % (1023532)------------------------------ % 257.19/36.40 % (1023532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.19/36.40 % (1023532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.19/36.40 % (1023532)CaDiCaL version: 2.1.3 % 257.19/36.40 % (1023532)Termination reason: Instruction limit % 257.19/36.40 % (1023532)Termination phase: Saturation % 257.19/36.40 % (1023532)Time elapsed: 22.980 s % 257.19/36.40 % (1023532)Peak memory usage: 15 MB % 257.19/36.40 % (1023532)Instructions burned: 88027 (million) % 257.19/36.40 % (1023695)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3656300751:i=7546:rtra=on:amm=off_2769 on theBenchmark for (2769ds/7546Mi) % 257.19/36.40 % (1023693)Instruction limit reached! % 257.19/36.40 % (1023693)------------------------------ % 257.19/36.40 % (1023693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.19/36.40 % (1023693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.19/36.40 % (1023693)CaDiCaL version: 2.1.3 % 257.19/36.40 % (1023693)Termination reason: Instruction limit % 257.19/36.40 % (1023693)Termination phase: Saturation % 257.19/36.40 % (1023693)Time elapsed: 2.904 s % 257.19/36.40 % (1023693)Peak memory usage: 16 MB % 257.19/36.40 % (1023693)Instructions burned: 7026 (million) % 257.19/36.40 % (1023697)ott+11_1_sil=16000:si=on:gs=on:random_seed=1501844988:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2743 on theBenchmark for (2743ds/4502Mi) % 300.51/42.54 % (1023697)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 300.51/42.54 % (1023695)Instruction limit reached! % 300.51/42.54 % (1023695)------------------------------ % 300.51/42.54 % (1023695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.54 % (1023695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.54 % (1023695)CaDiCaL version: 2.1.3 % 300.51/42.54 % (1023695)Termination reason: Instruction limit % 300.51/42.54 % (1023695)Termination phase: Saturation % 300.51/42.54 % (1023695)Time elapsed: 3.026 s % 300.51/42.54 % (1023695)Peak memory usage: 17 MB % 300.51/42.54 % (1023695)Instructions burned: 7548 (million) % 300.51/42.54 % (1023699)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1542887020:fmbsr=1.6:i=135068:rtra=on_2739 on theBenchmark for (2739ds/135068Mi) % 300.51/42.54 % Detected minimum model sizes of [1] % 300.51/42.54 % Detected maximum model sizes of [3] % 300.51/42.54 % fmb_start_size (= 7) larger than a detected sort maximum size! % 300.51/42.54 % (1023699)Refutation not found, incomplete strategy % 300.51/42.54 % (1023699)------------------------------ % 300.51/42.54 % (1023699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.54 % (1023699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.54 % (1023699)CaDiCaL version: 2.1.3 % 300.51/42.54 % (1023699)Termination reason: Refutation not found, incomplete strategy % 300.51/42.54 % (1023699)Time elapsed: 0.003 s % 300.51/42.54 % (1023699)Peak memory usage: 10 MB % 300.51/42.54 % (1023699)Instructions burned: 6 (million) % 300.51/42.54 % (1023699)------------------------------ % 300.51/42.54 % (1023699)------------------------------ % 300.51/42.54 % (1023701)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=227501570:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2739 on theBenchmark for (2739ds/9182Mi) % 300.51/42.54 % (1023689)Instruction limit reached! % 300.51/42.54 % (1023689)------------------------------ % 300.51/42.54 % (1023689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.54 % (1023689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.54 % (1023689)CaDiCaL version: 2.1.3 % 300.51/42.54 % (1023689)Termination reason: Instruction limit % 300.51/42.54 % (1023689)Termination phase: Saturation % 300.51/42.54 % (1023689)Time elapsed: 3.822 s % 300.51/42.54 % (1023689)Peak memory usage: 12 MB % 300.51/42.54 % (1023689)Instructions burned: 10229 (million) % 300.51/42.54 % (1023703)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=3460200013:i=58680:rtra=on_2735 on theBenchmark for (2735ds/58680Mi) % 300.51/42.54 % (1023697)Instruction limit reached! % 300.51/42.54 % (1023697)------------------------------ % 300.51/42.54 % (1023697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.54 % (1023697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.54 % (1023697)CaDiCaL version: 2.1.3 % 300.51/42.54 % (1023697)Termination reason: Instruction limit % 300.51/42.54 % (1023697)Termination phase: Saturation % 300.51/42.54 % (1023697)Time elapsed: 1.647 s % 300.51/42.54 % (1023697)Peak memory usage: 12 MB % 300.51/42.54 % (1023697)Instructions burned: 4504 (million) % 300.51/42.54 % (1023705)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=1726320057:i=10422:rtra=on_2727 on theBenchmark for (2727ds/10422Mi) % 300.51/42.54 % (1023701)Instruction limit reached! % 300.51/42.54 % (1023701)------------------------------ % 300.51/42.54 % (1023701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.54 % (1023701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.54 % (1023701)CaDiCaL version: 2.1.3 % 300.51/42.54 % (1023701)Termination reason: Instruction limit % 300.51/42.54 % (1023701)Termination phase: Saturation % 300.51/42.54 % (1023701)Time elapsed: 3.616 s % 300.51/42.54 % (1023701)Peak memory usage: 14 MB % 300.51/42.54 % (1023701)Instructions burned: 9183 (million) % 300.51/42.54 % (1023707)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=1023517691:i=10994:nm=2:rtra=on_2702 on theBenchmark for (2702ds/10994Mi) % 300.51/42.54 % Detected minimum model sizes of [1] % 300.51/42.54 % Detected maximum model sizes of [2] % 300.51/42.54 % fmb_start_size (= 17) larger than a detected sort maximum size! % 300.51/42.54 % (1023707)Refutation not found, incomplete strategy % 300.51/42.54 % (1023707)------------------------------ % 300.51/42.54 % (1023707)Version: Vampire 5.0.1 (R % 300.51/42.54 Terminated % 300.51/42.54 % Vampire exiting % 300.51/42.54 Terminated %------------------------------------------------------------------------------