%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LCL918^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 : n013.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:14 AM UTC 2026 % Result : Satisfiable 3.48s 0.97s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL918^1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.13/0.27 % Computer : n013.cluster.edu % 0.13/0.27 % Model : x86_64 x86_64 % 0.13/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.27 % Memory : 8046.5625MB % 0.13/0.27 % OS : Linux 6.8.0-71-generic % 0.13/0.27 % CPULimit : 300 % 0.13/0.27 % WCLimit : 300 % 0.13/0.27 % DateTime : Tue Sep 29 10:25:06 UTC 2026 % 0.13/0.27 % CPUTime : % 0.13/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.29/0.33 Running first-order model finding % 0.29/0.33 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 % 3.48/0.97 % (1917667)Will run a generic schedule for satisfiability detection. % 3.48/0.97 % (1917672)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3039066173_2999 on theBenchmark for (2999ds/0Mi) % 3.48/0.97 % Detected minimum model sizes of [1] % 3.48/0.97 % Detected maximum model sizes of [2] % 3.48/0.97 % TRYING [1] % 3.48/0.97 % TRYING [2] % 3.48/0.97 % Finite Model Found! % 3.48/0.97 % SZS status Satisfiable for theBenchmark % 3.48/0.97 % (1917672)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.48/0.97 % (1917672)------------------------------ % 3.48/0.97 % (1917672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.48/0.97 % (1917672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.48/0.97 % (1917672)CaDiCaL version: 2.1.3 % 3.48/0.97 % (1917672)Termination reason: Unknown % 3.48/0.97 % (1917672)Termination phase: Finite model building constraint generation % 3.48/0.97 % (1917672)Time elapsed: 0.003 s % 3.48/0.97 % (1917672)Peak memory usage: 11 MB % 3.48/0.97 % (1917672)Instructions burned: 6 (million) % 3.48/0.97 % (1917673)% WARNING: option uhcvi not known. % 3.48/0.97 % (1917675)dis+10_1_sil=32000:sp=arity:random_seed=4124636754:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.48/0.97 % (1917674)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=954461099:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.48/0.97 % (1917677)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3088230692:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.48/0.97 % (1917673)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1353865603:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.48/0.97 % (1917676)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1779590453:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.48/0.97 % (1917678)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1402617770:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.48/0.97 % (1917673)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.48/0.97 % (1917676)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.48/0.97 % (1917673)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 3.48/0.97 % (1917680)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1184301563:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.48/0.97 % Detected minimum model sizes of [1] % 3.48/0.97 % Detected maximum model sizes of [3] % 3.48/0.97 % TRYING [1] % 3.48/0.97 % TRYING [2] % 3.48/0.97 % Finite Model Found! % 3.48/0.97 % SZS status Satisfiable for theBenchmark % 3.48/0.97 % (1917680)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.48/0.97 % (1917680)------------------------------ % 3.48/0.97 % (1917680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.48/0.97 % (1917680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.48/0.97 % (1917680)CaDiCaL version: 2.1.3 % 3.48/0.97 % (1917680)Termination reason: Unknown % 3.48/0.97 % (1917680)Termination phase: Finite model building constraint generation % 3.48/0.97 % (1917680)Time elapsed: 0.004 s % 3.48/0.97 % (1917680)Peak memory usage: 11 MB % 3.48/0.97 % (1917680)Instructions burned: 6 (million) % 3.48/0.97 % (1917675)Instruction limit reached! % 3.48/0.97 % (1917675)------------------------------ % 3.48/0.97 % (1917675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.48/0.97 % (1917675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.48/0.97 % (1917675)CaDiCaL version: 2.1.3 % 3.48/0.97 % (1917675)Termination reason: Instruction limit % 3.48/0.97 % (1917675)Termination phase: Saturation % 3.48/0.97 % (1917675)Time elapsed: 0.070 s % 3.48/0.97 % (1917675)Peak memory usage: 11 MB % 3.48/0.97 % (1917675)Instructions burned: 104 (million) % 3.48/0.97 % (1917676)Instruction limit reached! % 3.48/0.97 % (1917676)------------------------------ % 3.48/0.97 % (1917676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.48/0.97 % (1917676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.48/0.97 % (1917676)CaDiCaL version: 2.1.3 % 3.48/0.97 % (1917676)Termination reason: Instruction limit % 3.48/0.97 % (1917676)Termination phase: Saturation % 3.48/0.97 % (1917676)Time elapsed: 0.079 s % 3.48/0.97 % (1917676)Peak memory usage: 11 MB % 3.48/0.97 % (1917676)Instructions burned: 117 (million) % 5.34/1.13 % (1917688)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2105185344:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.34/1.13 % (1917677)Instruction limit reached! % 5.34/1.13 % (1917677)------------------------------ % 5.34/1.13 % (1917677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.34/1.13 % (1917677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.34/1.13 % (1917677)CaDiCaL version: 2.1.3 % 5.34/1.13 % (1917677)Termination reason: Instruction limit % 5.34/1.13 % (1917677)Termination phase: Saturation % 5.34/1.13 % (1917677)Time elapsed: 0.091 s % 5.34/1.13 % (1917677)Peak memory usage: 11 MB % 5.34/1.13 % (1917677)Instructions burned: 132 (million) % 5.34/1.13 % (1917689)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=3937059809:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.34/1.13 % (1917689)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 5.34/1.13 % (1917689)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 5.34/1.13 % (1917678)Instruction limit reached! % 5.34/1.13 % (1917678)------------------------------ % 5.34/1.13 % (1917678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.34/1.13 % (1917678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.34/1.13 % (1917678)CaDiCaL version: 2.1.3 % 5.34/1.13 % (1917678)Termination reason: Instruction limit % 5.34/1.13 % (1917678)Termination phase: Saturation % 5.34/1.13 % (1917678)Time elapsed: 0.107 s % 5.34/1.13 % (1917678)Peak memory usage: 12 MB % 5.34/1.13 % (1917678)Instructions burned: 160 (million) % 5.34/1.13 % (1917690)ott-21_1_sil=16000:fs=off:random_seed=314966578:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.34/1.13 % (1917692)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3736391743:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.34/1.13 % (1917694)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=739823283:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.34/1.13 % (1917688)Instruction limit reached! % 5.34/1.13 % (1917688)------------------------------ % 5.34/1.13 % (1917688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.34/1.13 % (1917688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.34/1.13 % (1917688)CaDiCaL version: 2.1.3 % 5.34/1.13 % (1917688)Termination reason: Instruction limit % 5.34/1.13 % (1917688)Termination phase: Saturation % 5.34/1.13 % (1917688)Time elapsed: 0.066 s % 5.34/1.13 % (1917688)Peak memory usage: 12 MB % 5.34/1.13 % (1917688)Instructions burned: 132 (million) % 5.34/1.13 % Detected minimum model sizes of [1] % 5.34/1.13 % Detected maximum model sizes of [2] % 5.34/1.13 % TRYING [1] % 5.34/1.13 % TRYING [2] % 5.34/1.13 % Finite Model Found! % 5.34/1.13 % SZS status Satisfiable for theBenchmark % 5.34/1.13 % (1917694)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.34/1.13 % (1917694)------------------------------ % 5.34/1.13 % (1917694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.34/1.13 % (1917694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.34/1.13 % (1917694)CaDiCaL version: 2.1.3 % 5.34/1.13 % (1917694)Termination reason: Unknown % 5.34/1.13 % (1917694)Termination phase: Finite model building constraint generation % 5.34/1.13 % (1917694)Time elapsed: 0.006 s % 5.34/1.13 % (1917694)Peak memory usage: 11 MB % 5.34/1.13 % (1917694)Instructions burned: 6 (million) % 5.34/1.13 % (1917699)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1419714777:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.34/1.13 % (1917698)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2233414671:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.34/1.13 % Exception at run slice level % 5.34/1.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 5.34/1.13 % (1917702)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=3208083832:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 5.34/1.13 % (1917702)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 5.34/1.13 % (1917690)Instruction limit reached! % 16.79/2.74 % (1917690)------------------------------ % 16.79/2.74 % (1917690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.74 % (1917690)CaDiCaL version: 2.1.3 % 16.79/2.74 % (1917690)Termination reason: Instruction limit % 16.79/2.74 % (1917690)Termination phase: Saturation % 16.79/2.74 % (1917690)Time elapsed: 0.145 s % 16.79/2.74 % (1917690)Peak memory usage: 12 MB % 16.79/2.74 % (1917690)Instructions burned: 181 (million) % 16.79/2.74 % (1917704)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1270882112:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 16.79/2.74 % (1917704)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.79/2.74 % (1917692)Instruction limit reached! % 16.79/2.74 % (1917692)------------------------------ % 16.79/2.74 % (1917692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.74 % (1917692)CaDiCaL version: 2.1.3 % 16.79/2.74 % (1917692)Termination reason: Instruction limit % 16.79/2.74 % (1917692)Termination phase: Saturation % 16.79/2.74 % (1917692)Time elapsed: 0.332 s % 16.79/2.74 % (1917692)Peak memory usage: 12 MB % 16.79/2.74 % (1917692)Instructions burned: 478 (million) % 16.79/2.74 % (1917706)fmb+10_1_sil=64000:random_seed=2393945327:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 16.79/2.74 % (1917706)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.79/2.74 % Detected minimum model sizes of [1] % 16.79/2.74 % Detected maximum model sizes of [2] % 16.79/2.74 % TRYING [1] % 16.79/2.74 % TRYING [2] % 16.79/2.74 % Finite Model Found! % 16.79/2.74 % SZS status Satisfiable for theBenchmark % 16.79/2.74 % (1917706)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.79/2.74 % (1917706)------------------------------ % 16.79/2.74 % (1917706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.74 % (1917706)CaDiCaL version: 2.1.3 % 16.79/2.74 % (1917706)Termination reason: Unknown % 16.79/2.74 % (1917706)Termination phase: Finite model building constraint generation % 16.79/2.74 % (1917706)Time elapsed: 0.007 s % 16.79/2.74 % (1917706)Peak memory usage: 10 MB % 16.79/2.74 % (1917706)Instructions burned: 6 (million) % 16.79/2.74 % (1917689)Instruction limit reached! % 16.79/2.74 % (1917689)------------------------------ % 16.79/2.74 % (1917689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.74 % (1917689)CaDiCaL version: 2.1.3 % 16.79/2.74 % (1917689)Termination reason: Instruction limit % 16.79/2.74 % (1917689)Termination phase: Saturation % 16.79/2.74 % (1917689)Time elapsed: 0.450 s % 16.79/2.74 % (1917689)Peak memory usage: 13 MB % 16.79/2.74 % (1917689)Instructions burned: 684 (million) % 16.79/2.74 % (1917708)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3875481834:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 16.79/2.74 % Detected minimum model sizes of [1] % 16.79/2.74 % Detected maximum model sizes of [2] % 16.79/2.74 % fmb_start_size (= 20) larger than a detected sort maximum size! % 16.79/2.74 % (1917708)Refutation not found, incomplete strategy % 16.79/2.74 % (1917708)------------------------------ % 16.79/2.74 % (1917708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.74 % (1917708)CaDiCaL version: 2.1.3 % 16.79/2.74 % (1917708)Termination reason: Refutation not found, incomplete strategy % 16.79/2.74 % (1917708)Time elapsed: 0.007 s % 16.79/2.74 % (1917708)Peak memory usage: 10 MB % 16.79/2.74 % (1917708)Instructions burned: 6 (million) % 16.79/2.74 % (1917708)------------------------------ % 16.79/2.74 % (1917708)------------------------------ % 16.79/2.74 % (1917709)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2353004006:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 16.79/2.74 % Detected minimum model sizes of [1] % 16.79/2.74 % Detected maximum model sizes of [2] % 16.79/2.74 % fmb_start_size (= 8) larger than a detected sort maximum size! % 16.79/2.74 % (1917709)Refutation not found, incomplete strategy % 16.79/2.74 % (1917709)------------------------------ % 16.79/2.74 % (1917709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.74 % (1917709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.24 % (1917709)CaDiCaL version: 2.1.3 % 27.41/4.24 % (1917709)Termination reason: Refutation not found, incomplete strategy % 27.41/4.24 % (1917709)Time elapsed: 0.005 s % 27.41/4.24 % (1917709)Peak memory usage: 10 MB % 27.41/4.24 % (1917709)Instructions burned: 6 (million) % 27.41/4.24 % (1917709)------------------------------ % 27.41/4.24 % (1917709)------------------------------ % 27.41/4.24 % (1917698)Instruction limit reached! % 27.41/4.24 % (1917698)------------------------------ % 27.41/4.24 % (1917698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.24 % (1917698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.24 % (1917698)CaDiCaL version: 2.1.3 % 27.41/4.24 % (1917698)Termination reason: Instruction limit % 27.41/4.24 % (1917698)Termination phase: Saturation % 27.41/4.24 % (1917698)Time elapsed: 0.404 s % 27.41/4.24 % (1917698)Peak memory usage: 12 MB % 27.41/4.24 % (1917698)Instructions burned: 1182 (million) % 27.41/4.24 % (1917714)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2375673008:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.41/4.24 % Detected minimum model sizes of [1] % 27.41/4.24 % Detected maximum model sizes of [2] % 27.41/4.24 % (1917711)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=187429934:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 27.41/4.24 % fmb_start_size (= 77) larger than a detected sort maximum size! % 27.41/4.24 % (1917714)Refutation not found, incomplete strategy % 27.41/4.24 % (1917714)------------------------------ % 27.41/4.24 % (1917714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.24 % (1917714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.24 % (1917714)CaDiCaL version: 2.1.3 % 27.41/4.24 % (1917714)Termination reason: Refutation not found, incomplete strategy % 27.41/4.24 % (1917714)Time elapsed: 0.003 s % 27.41/4.24 % (1917714)Peak memory usage: 10 MB % 27.41/4.24 % (1917714)Instructions burned: 6 (million) % 27.41/4.24 % (1917714)------------------------------ % 27.41/4.24 % (1917714)------------------------------ % 27.41/4.24 % (1917711)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 27.41/4.24 % (1917713)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2398062270:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 27.41/4.24 % (1917713)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.41/4.24 % (1917713)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 27.41/4.24 % (1917717)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2406607890:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.41/4.24 % TRYING [16] % 27.41/4.24 % Finite Model Found! % 27.41/4.24 % SZS status Satisfiable for theBenchmark % 27.41/4.24 % (1917717)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.41/4.24 % (1917717)------------------------------ % 27.41/4.24 % (1917717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.24 % (1917717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.24 % (1917717)CaDiCaL version: 2.1.3 % 27.41/4.24 % (1917717)Termination reason: Unknown % 27.41/4.24 % (1917717)Termination phase: Finite model building constraint generation % 27.41/4.24 % (1917717)Time elapsed: 0.005 s % 27.41/4.24 % (1917717)Peak memory usage: 11 MB % 27.41/4.24 % (1917717)Instructions burned: 9 (million) % 27.41/4.24 % (1917720)ott-2_1_sil=16000:newcnf=on:random_seed=3167168864:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.41/4.24 % (1917720)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 27.41/4.24 % (1917702)Instruction limit reached! % 27.41/4.24 % (1917702)------------------------------ % 27.41/4.24 % (1917702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.24 % (1917702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.24 % (1917702)CaDiCaL version: 2.1.3 % 27.41/4.24 % (1917702)Termination reason: Instruction limit % 27.41/4.24 % (1917702)Termination phase: Saturation % 27.41/4.24 % (1917702)Time elapsed: 0.459 s % 27.41/4.24 % (1917702)Peak memory usage: 12 MB % 27.41/4.24 % (1917702)Instructions burned: 693 (million) % 27.41/4.24 % (1917722)ott+10_1_sil=32000:tgt=ground:random_seed=3599129049:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 57.91/8.56 % (1917704)Instruction limit reached! % 57.91/8.56 % (1917704)------------------------------ % 57.91/8.56 % (1917704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.91/8.56 % (1917704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.91/8.56 % (1917704)CaDiCaL version: 2.1.3 % 57.91/8.56 % (1917704)Termination reason: Instruction limit % 57.91/8.56 % (1917704)Termination phase: Saturation % 57.91/8.56 % (1917704)Time elapsed: 0.563 s % 57.91/8.56 % (1917704)Peak memory usage: 12 MB % 57.91/8.56 % (1917704)Instructions burned: 879 (million) % 57.91/8.56 % (1917724)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2062222370:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 57.91/8.56 % Detected minimum model sizes of [1] % 57.91/8.56 % Detected maximum model sizes of [2] % 57.91/8.56 % TRYING [1] % 57.91/8.56 % TRYING [2] % 57.91/8.56 % Finite Model Found! % 57.91/8.56 % SZS status Satisfiable for theBenchmark % 57.91/8.56 % (1917724)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.91/8.56 % (1917724)------------------------------ % 57.91/8.56 % (1917724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.91/8.56 % (1917724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.91/8.56 % (1917724)CaDiCaL version: 2.1.3 % 57.91/8.56 % (1917724)Termination reason: Unknown % 57.91/8.56 % (1917724)Termination phase: Finite model building constraint generation % 57.91/8.56 % (1917724)Time elapsed: 0.007 s % 57.91/8.56 % (1917724)Peak memory usage: 11 MB % 57.91/8.56 % (1917724)Instructions burned: 6 (million) % 57.91/8.56 % (1917726)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4248226714:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 57.91/8.56 % (1917720)Instruction limit reached! % 57.91/8.56 % (1917720)------------------------------ % 57.91/8.56 % (1917720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.91/8.56 % (1917720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.91/8.56 % (1917720)CaDiCaL version: 2.1.3 % 57.91/8.56 % (1917720)Termination reason: Instruction limit % 57.91/8.56 % (1917720)Termination phase: Saturation % 57.91/8.56 % (1917720)Time elapsed: 0.298 s % 57.91/8.56 % (1917720)Peak memory usage: 12 MB % 57.91/8.56 % (1917720)Instructions burned: 871 (million) % 57.91/8.56 % (1917726)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 57.91/8.56 % (1917728)dis+21_1_sil=32000:sas=cadical:random_seed=1794294142:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 57.91/8.56 % (1917713)Instruction limit reached! % 57.91/8.56 % (1917713)------------------------------ % 57.91/8.56 % (1917713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.91/8.56 % (1917713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.91/8.56 % (1917713)CaDiCaL version: 2.1.3 % 57.91/8.56 % (1917713)Termination reason: Instruction limit % 57.91/8.56 % (1917713)Termination phase: Saturation % 57.91/8.56 % (1917713)Time elapsed: 0.917 s % 57.91/8.56 % (1917713)Peak memory usage: 13 MB % 57.91/8.56 % (1917713)Instructions burned: 1472 (million) % 57.91/8.56 % (1917730)ott+11_1_sil=16000:gs=on:random_seed=2704817876:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 57.91/8.56 % (1917730)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 57.91/8.56 % (1917728)Instruction limit reached! % 57.91/8.56 % (1917728)------------------------------ % 57.91/8.56 % (1917728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.91/8.56 % (1917728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.91/8.56 % (1917728)CaDiCaL version: 2.1.3 % 57.91/8.56 % (1917728)Termination reason: Instruction limit % 57.91/8.56 % (1917728)Termination phase: Saturation % 57.91/8.56 % (1917728)Time elapsed: 1.321 s % 57.91/8.56 % (1917728)Peak memory usage: 15 MB % 57.91/8.56 % (1917728)Instructions burned: 3776 (million) % 57.91/8.56 % (1917732)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=684424742:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 57.91/8.56 % Detected minimum model sizes of [1] % 57.91/8.56 % Detected maximum model sizes of [3] % 57.91/8.56 % fmb_start_size (= 7) larger than a detected sort maximum size! % 57.91/8.56 % (1917732)Refutation not found, incomplete strategy % 57.91/8.56 % (1917732)------------------------------ % 57.91/8.56 % (1917732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917732)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917732)Termination reason: Refutation not found, incomplete strategy % 99.79/14.46 % (1917732)Time elapsed: 0.007 s % 99.79/14.46 % (1917732)Peak memory usage: 10 MB % 99.79/14.46 % (1917732)Instructions burned: 6 (million) % 99.79/14.46 % (1917732)------------------------------ % 99.79/14.46 % (1917732)------------------------------ % 99.79/14.46 % (1917734)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=520401391:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 99.79/14.46 % (1917730)Instruction limit reached! % 99.79/14.46 % (1917730)------------------------------ % 99.79/14.46 % (1917730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917730)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917730)Termination reason: Instruction limit % 99.79/14.46 % (1917730)Termination phase: Saturation % 99.79/14.46 % (1917730)Time elapsed: 1.245 s % 99.79/14.46 % (1917730)Peak memory usage: 13 MB % 99.79/14.46 % (1917730)Instructions burned: 2251 (million) % 99.79/14.46 % (1917736)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3936370660:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 99.79/14.46 % (1917726)Instruction limit reached! % 99.79/14.46 % (1917726)------------------------------ % 99.79/14.46 % (1917726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917726)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917726)Termination reason: Instruction limit % 99.79/14.46 % (1917726)Termination phase: Saturation % 99.79/14.46 % (1917726)Time elapsed: 2.442 s % 99.79/14.46 % (1917726)Peak memory usage: 14 MB % 99.79/14.46 % (1917726)Instructions burned: 3513 (million) % 99.79/14.46 % (1917738)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=900871662:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 99.79/14.46 % (1917722)Instruction limit reached! % 99.79/14.46 % (1917722)------------------------------ % 99.79/14.46 % (1917722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917722)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917722)Termination reason: Instruction limit % 99.79/14.46 % (1917722)Termination phase: Saturation % 99.79/14.46 % (1917722)Time elapsed: 2.997 s % 99.79/14.46 % (1917722)Peak memory usage: 12 MB % 99.79/14.46 % (1917722)Instructions burned: 5117 (million) % 99.79/14.46 % (1917740)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3545540641:i=5497:nm=2_2962 on theBenchmark for (2962ds/5497Mi) % 99.79/14.46 % Detected minimum model sizes of [1] % 99.79/14.46 % Detected maximum model sizes of [2] % 99.79/14.46 % fmb_start_size (= 17) larger than a detected sort maximum size! % 99.79/14.46 % (1917740)Refutation not found, incomplete strategy % 99.79/14.46 % (1917740)------------------------------ % 99.79/14.46 % (1917740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917740)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917740)Termination reason: Refutation not found, incomplete strategy % 99.79/14.46 % (1917740)Time elapsed: 0.007 s % 99.79/14.46 % (1917740)Peak memory usage: 10 MB % 99.79/14.46 % (1917740)Instructions burned: 6 (million) % 99.79/14.46 % (1917740)------------------------------ % 99.79/14.46 % (1917740)------------------------------ % 99.79/14.46 % (1917711)Instruction limit reached! % 99.79/14.46 % (1917711)------------------------------ % 99.79/14.46 % (1917711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.46 % (1917711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.46 % (1917711)CaDiCaL version: 2.1.3 % 99.79/14.46 % (1917711)Termination reason: Instruction limit % 99.79/14.46 % (1917711)Termination phase: Saturation % 99.79/14.46 % (1917711)Time elapsed: 3.201 s % 99.79/14.46 % (1917711)Peak memory usage: 13 MB % 99.79/14.46 % (1917711)Instructions burned: 5132 (million) % 99.79/14.46 % (1917743)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4105910462:i=14071_2961 on theBenchmark for (2961ds/14071Mi) % 99.79/14.46 % Detected minimum model sizes of [1] % 99.79/14.46 % Detected maximum model sizes of [2] % 99.79/14.46 % fmb_start_size (= 12) larger than a detected sort maximum size! % 105.15/15.18 % (1917743)Refutation not found, incomplete strategy % 105.15/15.18 % (1917743)------------------------------ % 105.15/15.18 % (1917743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.15/15.18 % (1917743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.15/15.18 % (1917743)CaDiCaL version: 2.1.3 % 105.15/15.18 % (1917743)Termination reason: Refutation not found, incomplete strategy % 105.15/15.18 % (1917743)Time elapsed: 0.006 s % 105.15/15.18 % (1917743)Peak memory usage: 10 MB % 105.15/15.18 % (1917743)Instructions burned: 6 (million) % 105.15/15.18 % (1917743)------------------------------ % 105.15/15.18 % (1917743)------------------------------ % 105.15/15.18 % (1917742)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2309083080:fmbsr=2:i=46332_2961 on theBenchmark for (2961ds/46332Mi) % 105.15/15.18 % Detected minimum model sizes of [1] % 105.15/15.18 % Detected maximum model sizes of [3] % 105.15/15.18 % fmb_start_size (= 15) larger than a detected sort maximum size! % 105.15/15.18 % (1917742)Refutation not found, incomplete strategy % 105.15/15.18 % (1917742)------------------------------ % 105.15/15.18 % (1917742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.15/15.18 % (1917742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.15/15.18 % (1917742)CaDiCaL version: 2.1.3 % 105.15/15.18 % (1917742)Termination reason: Refutation not found, incomplete strategy % 105.15/15.18 % (1917742)Time elapsed: 0.007 s % 105.15/15.18 % (1917742)Peak memory usage: 10 MB % 105.15/15.18 % (1917742)Instructions burned: 6 (million) % 105.15/15.18 % (1917742)------------------------------ % 105.15/15.18 % (1917742)------------------------------ % 105.15/15.18 % (1917746)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2111543846:i=22565:add=on:rawr=on_2960 on theBenchmark for (2960ds/22565Mi) % 105.15/15.18 % (1917747)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1972730416:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 105.15/15.18 % (1917734)Instruction limit reached! % 105.15/15.18 % (1917734)------------------------------ % 105.15/15.18 % (1917734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.15/15.18 % (1917734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.15/15.18 % (1917734)CaDiCaL version: 2.1.3 % 105.15/15.18 % (1917734)Termination reason: Instruction limit % 105.15/15.18 % (1917734)Termination phase: Saturation % 105.15/15.18 % (1917734)Time elapsed: 2.317 s % 105.15/15.18 % (1917734)Peak memory usage: 13 MB % 105.15/15.18 % (1917734)Instructions burned: 4592 (million) % 105.15/15.18 % (1917750)dis+10_16:1_sil=16000:random_seed=2901361227:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi) % 105.15/15.18 % (1917738)Instruction limit reached! % 105.15/15.18 % (1917738)------------------------------ % 105.15/15.18 % (1917738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.15/15.18 % (1917738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.15/15.18 % (1917738)CaDiCaL version: 2.1.3 % 105.15/15.18 % (1917738)Termination reason: Instruction limit % 105.15/15.18 % (1917738)Termination phase: Saturation % 105.15/15.18 % (1917738)Time elapsed: 3.487 s % 105.15/15.18 % (1917738)Peak memory usage: 16 MB % 105.15/15.18 % (1917738)Instructions burned: 5212 (million) % 105.15/15.18 % (1917752)ott-3_8_sil=64000:random_seed=461655786:i=20139:bs=on_2930 on theBenchmark for (2930ds/20139Mi) % 105.15/15.18 % (1917747)Instruction limit reached! % 105.15/15.18 % (1917747)------------------------------ % 105.15/15.18 % (1917747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.15/15.18 % (1917747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.15/15.18 % (1917747)CaDiCaL version: 2.1.3 % 105.15/15.18 % (1917747)Termination reason: Instruction limit % 105.15/15.18 % (1917747)Termination phase: Saturation % 105.15/15.18 % (1917747)Time elapsed: 4.237 s % 105.15/15.18 % (1917747)Peak memory usage: 12 MB % 105.15/15.18 % (1917747)Instructions burned: 8178 (million) % 105.15/15.18 % (1917793)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2765397964:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 105.15/15.18 % Detected minimum model sizes of [1] % 105.15/15.18 % Detected maximum model sizes of [2] % 105.15/15.18 % fmb_start_size (= 9) larger than a detected sort maximum size! % 105.15/15.18 % (1917793)Refutation not found, incomplete strategy % 105.15/15.18 % (1917793)------------------------------ % 105.15/15.18 % (1917793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917793)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917793)Termination reason: Refutation not found, incomplete strategy % 154.82/22.15 % (1917793)Time elapsed: 0.003 s % 154.82/22.15 % (1917793)Peak memory usage: 10 MB % 154.82/22.15 % (1917793)Instructions burned: 6 (million) % 154.82/22.15 % (1917793)------------------------------ % 154.82/22.15 % (1917793)------------------------------ % 154.82/22.15 % (1917804)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2455005964:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 154.82/22.15 % (1917750)Instruction limit reached! % 154.82/22.15 % (1917750)------------------------------ % 154.82/22.15 % (1917750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917750)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917750)Termination reason: Instruction limit % 154.82/22.15 % (1917750)Termination phase: Saturation % 154.82/22.15 % (1917750)Time elapsed: 4.471 s % 154.82/22.15 % (1917750)Peak memory usage: 16 MB % 154.82/22.15 % (1917750)Instructions burned: 9157 (million) % 154.82/22.15 % (1917911)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3057784435:i=14134_2907 on theBenchmark for (2907ds/14134Mi) % 154.82/22.15 % (1917911)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 154.82/22.15 % (1917736)Instruction limit reached! % 154.82/22.15 % (1917736)------------------------------ % 154.82/22.15 % (1917736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917736)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917736)Termination reason: Instruction limit % 154.82/22.15 % (1917736)Termination phase: Saturation % 154.82/22.15 % (1917736)Time elapsed: 7.865 s % 154.82/22.15 % (1917736)Peak memory usage: 16 MB % 154.82/22.15 % (1917736)Instructions burned: 29345 (million) % 154.82/22.15 % (1917913)dis+33_16_sil=32000:sac=on:random_seed=199151084:i=15851:nm=0_2891 on theBenchmark for (2891ds/15851Mi) % 154.82/22.15 % (1917746)Instruction limit reached! % 154.82/22.15 % (1917746)------------------------------ % 154.82/22.15 % (1917746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917746)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917746)Termination reason: Instruction limit % 154.82/22.15 % (1917746)Termination phase: Saturation % 154.82/22.15 % (1917746)Time elapsed: 7.727 s % 154.82/22.15 % (1917746)Peak memory usage: 14 MB % 154.82/22.15 % (1917746)Instructions burned: 22566 (million) % 154.82/22.15 % (1917915)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=565258316:avsq=on:i=17627:add=on:amm=off_2883 on theBenchmark for (2883ds/17627Mi) % 154.82/22.15 % (1917804)Instruction limit reached! % 154.82/22.15 % (1917804)------------------------------ % 154.82/22.15 % (1917804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917804)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917804)Termination reason: Instruction limit % 154.82/22.15 % (1917804)Termination phase: Saturation % 154.82/22.15 % (1917804)Time elapsed: 4.354 s % 154.82/22.15 % (1917804)Peak memory usage: 13 MB % 154.82/22.15 % (1917804)Instructions burned: 11405 (million) % 154.82/22.15 % (1917917)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=107943749:s2a=on:i=53295_2874 on theBenchmark for (2874ds/53295Mi) % 154.82/22.15 % (1917913)Instruction limit reached! % 154.82/22.15 % (1917913)------------------------------ % 154.82/22.15 % (1917913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.82/22.15 % (1917913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.82/22.15 % (1917913)CaDiCaL version: 2.1.3 % 154.82/22.15 % (1917913)Termination reason: Instruction limit % 154.82/22.15 % (1917913)Termination phase: Saturation % 154.82/22.15 % (1917913)Time elapsed: 3.300 s % 154.82/22.15 % (1917913)Peak memory usage: 14 MB % 154.82/22.15 % (1917913)Instructions burned: 15854 (million) % 154.82/22.15 % (1918035)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3502706676:i=26857:ins=20_2858 on theBenchmark for (2858ds/26857Mi) % 154.82/22.15 % Detected minimum model sizes of [1] % 154.82/22.15 % Detected maximum model sizes of [2] % 154.82/22.15 % fmb_start_size (= 16) larger than a detected sort maximum size! % 154.82/22.15 % (1918035)Refutation not found, incomplete strategy % 159.33/22.86 % (1918035)------------------------------ % 159.33/22.86 % (1918035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.33/22.86 % (1918035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.33/22.86 % (1918035)CaDiCaL version: 2.1.3 % 159.33/22.86 % (1918035)Termination reason: Refutation not found, incomplete strategy % 159.33/22.86 % (1918035)Time elapsed: 0.001 s % 159.33/22.86 % (1918035)Peak memory usage: 10 MB % 159.33/22.86 % (1918035)Instructions burned: 6 (million) % 159.33/22.86 % (1918035)------------------------------ % 159.33/22.86 % (1918035)------------------------------ % 159.33/22.86 % (1918043)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1538161301:i=28120:bs=on:fsr=off_2858 on theBenchmark for (2858ds/28120Mi) % 159.33/22.86 % (1917911)Instruction limit reached! % 159.33/22.86 % (1917911)------------------------------ % 159.33/22.86 % (1917911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.33/22.86 % (1917911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.33/22.86 % (1917911)CaDiCaL version: 2.1.3 % 159.33/22.86 % (1917911)Termination reason: Instruction limit % 159.33/22.86 % (1917911)Termination phase: Saturation % 159.33/22.86 % (1917911)Time elapsed: 5.385 s % 159.33/22.86 % (1917911)Peak memory usage: 12 MB % 159.33/22.86 % (1917911)Instructions burned: 14135 (million) % 159.33/22.86 % (1918170)fmb+10_1_sil=256000:fmbss=7:random_seed=1149549419:fmbsr=1.6:i=182295_2853 on theBenchmark for (2853ds/182295Mi) % 159.33/22.86 % Detected minimum model sizes of [1] % 159.33/22.86 % Detected maximum model sizes of [2] % 159.33/22.86 % fmb_start_size (= 7) larger than a detected sort maximum size! % 159.33/22.86 % (1918170)Refutation not found, incomplete strategy % 159.33/22.86 % (1918170)------------------------------ % 159.33/22.86 % (1918170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.33/22.86 % (1918170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.33/22.86 % (1918170)CaDiCaL version: 2.1.3 % 159.33/22.86 % (1918170)Termination reason: Refutation not found, incomplete strategy % 159.33/22.86 % (1918170)Time elapsed: 0.007 s % 159.33/22.86 % (1918170)Peak memory usage: 10 MB % 159.33/22.86 % (1918170)Instructions burned: 6 (million) % 159.33/22.86 % (1918170)------------------------------ % 159.33/22.86 % (1918170)------------------------------ % 159.33/22.86 % (1918178)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3453780838:i=44625:gsp=on_2852 on theBenchmark for (2852ds/44625Mi) % 159.33/22.86 % (1918178)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 159.33/22.86 % (1918178)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 159.33/22.86 % Detected minimum model sizes of [1] % 159.33/22.86 % Detected maximum model sizes of [2] % 159.33/22.86 % fmb_start_size (= 21) larger than a detected sort maximum size! % 159.33/22.86 % (1918178)Refutation not found, incomplete strategy % 159.33/22.86 % (1918178)------------------------------ % 159.33/22.86 % (1918178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.33/22.86 % (1918178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.33/22.86 % (1918178)CaDiCaL version: 2.1.3 % 159.33/22.86 % (1918178)Termination reason: Refutation not found, incomplete strategy % 159.33/22.86 % (1918178)Time elapsed: 0.008 s % 159.33/22.86 % (1918178)Peak memory usage: 10 MB % 159.33/22.86 % (1918178)Instructions burned: 6 (million) % 159.33/22.86 % (1918178)------------------------------ % 159.33/22.86 % (1918178)------------------------------ % 159.33/22.86 % (1918182)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3853445181:i=160505_2852 on theBenchmark for (2852ds/160505Mi) % 159.33/22.86 % Detected minimum model sizes of [1] % 159.33/22.86 % Detected maximum model sizes of [2] % 159.33/22.86 % fmb_start_size (= 15) larger than a detected sort maximum size! % 159.33/22.86 % (1918182)Refutation not found, incomplete strategy % 159.33/22.86 % (1918182)------------------------------ % 159.33/22.86 % (1918182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.33/22.86 % (1918182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.33/22.86 % (1918182)CaDiCaL version: 2.1.3 % 159.33/22.86 % (1918182)Termination reason: Refutation not found, incomplete strategy % 159.33/22.86 % (1918182)Time elapsed: 0.004 s % 159.33/22.86 % (1918182)Peak memory usage: 10 MB % 159.33/22.86 % (1918182)Instructions burned: 6 (million) % 159.33/22.86 % (1918182)------------------------------ % 159.33/22.86 % (1918182)------------------------------ % 159.33/22.86 % (1918185)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=38237802:fmbsr=1.3:i=225729_2851 on theBenchmark for (2851ds/225729Mi) % 165.42/23.77 % Detected minimum model sizes of [1] % 165.42/23.77 % Detected maximum model sizes of [2] % 165.42/23.77 % fmb_start_size (= 10) larger than a detected sort maximum size! % 165.42/23.77 % (1918185)Refutation not found, incomplete strategy % 165.42/23.77 % (1918185)------------------------------ % 165.42/23.77 % (1918185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.42/23.77 % (1918185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.42/23.77 % (1918185)CaDiCaL version: 2.1.3 % 165.42/23.77 % (1918185)Termination reason: Refutation not found, incomplete strategy % 165.42/23.77 % (1918185)Time elapsed: 0.006 s % 165.42/23.77 % (1918185)Peak memory usage: 10 MB % 165.42/23.77 % (1918185)Instructions burned: 6 (million) % 165.42/23.77 % (1918185)------------------------------ % 165.42/23.77 % (1918185)------------------------------ % 165.42/23.77 % (1918189)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1266171918:fmbsr=2:i=185024:ins=7_2851 on theBenchmark for (2851ds/185024Mi) % 165.42/23.77 % Detected minimum model sizes of [1] % 165.42/23.77 % Detected maximum model sizes of [2] % 165.42/23.77 % fmb_start_size (= 10) larger than a detected sort maximum size! % 165.42/23.77 % (1918189)Refutation not found, incomplete strategy % 165.42/23.77 % (1918189)------------------------------ % 165.42/23.77 % (1918189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.42/23.77 % (1918189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.42/23.77 % (1918189)CaDiCaL version: 2.1.3 % 165.42/23.77 % (1918189)Termination reason: Refutation not found, incomplete strategy % 165.42/23.77 % (1918189)Time elapsed: 0.006 s % 165.42/23.77 % (1918189)Peak memory usage: 10 MB % 165.42/23.77 % (1918189)Instructions burned: 6 (million) % 165.42/23.77 % (1918189)------------------------------ % 165.42/23.77 % (1918189)------------------------------ % 165.42/23.77 % (1918193)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=196519213:rtra=on_2851 on theBenchmark for (2851ds/0Mi) % 165.42/23.77 % Detected minimum model sizes of [1] % 165.42/23.77 % Detected maximum model sizes of [2] % 165.42/23.77 % TRYING [1] % 165.42/23.77 % TRYING [2] % 165.42/23.77 % Finite Model Found! % 165.42/23.77 % SZS status Satisfiable for theBenchmark % 165.42/23.77 % (1918193)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 165.42/23.77 % (1918193)------------------------------ % 165.42/23.77 % (1918193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.42/23.77 % (1918193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.42/23.77 % (1918193)CaDiCaL version: 2.1.3 % 165.42/23.77 % (1918193)Termination reason: Unknown % 165.42/23.77 % (1918193)Termination phase: Finite model building constraint generation % 165.42/23.77 % (1918193)Time elapsed: 0.004 s % 165.42/23.77 % (1918193)Peak memory usage: 11 MB % 165.42/23.77 % (1918193)Instructions burned: 6 (million) % 165.42/23.77 % (1918195)% WARNING: option uhcvi not known. % 165.42/23.77 % (1918195)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2110954744:i=271062:add=off:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/271062Mi) % 165.42/23.77 % (1918195)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 165.42/23.77 % (1918195)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 165.42/23.77 % (1917752)Instruction limit reached! % 165.42/23.77 % (1917752)------------------------------ % 165.42/23.77 % (1917752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.42/23.77 % (1917752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.42/23.77 % (1917752)CaDiCaL version: 2.1.3 % 165.42/23.77 % (1917752)Termination reason: Instruction limit % 165.42/23.77 % (1917752)Termination phase: Saturation % 165.42/23.77 % (1917752)Time elapsed: 8.571 s % 165.42/23.77 % (1917752)Peak memory usage: 14 MB % 165.42/23.77 % (1917752)Instructions burned: 20140 (million) % 165.42/23.77 % (1918221)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=599299280:i=176048:add=on:rtra=on:rawr=on_2843 on theBenchmark for (2843ds/176048Mi) % 165.42/23.77 % (1917915)Instruction limit reached! % 165.42/23.77 % (1917915)------------------------------ % 165.42/23.77 % (1917915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.42/23.77 % (1917915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.42/23.77 % (1917915)CaDiCaL version: 2.1.3 % 165.42/23.77 % (1917915)Termination reason: Instruction limit % 174.44/25.00 % (1917915)Termination phase: Saturation % 174.44/25.00 % (1917915)Time elapsed: 10.121 s % 174.44/25.00 % (1917915)Peak memory usage: 22 MB % 174.44/25.00 % (1917915)Instructions burned: 17629 (million) % 174.44/25.00 % (1918358)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2518966965:i=206:fgj=on:rtra=on_2781 on theBenchmark for (2781ds/206Mi) % 174.44/25.00 % (1918358)Instruction limit reached! % 174.44/25.00 % (1918358)------------------------------ % 174.44/25.00 % (1918358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.44/25.00 % (1918358)CaDiCaL version: 2.1.3 % 174.44/25.00 % (1918358)Termination reason: Instruction limit % 174.44/25.00 % (1918358)Termination phase: Saturation % 174.44/25.00 % (1918358)Time elapsed: 0.113 s % 174.44/25.00 % (1918358)Peak memory usage: 12 MB % 174.44/25.00 % (1918358)Instructions burned: 207 (million) % 174.44/25.00 % (1918364)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=846388867:i=232:rtra=on_2780 on theBenchmark for (2780ds/232Mi) % 174.44/25.00 % (1918364)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 174.44/25.00 % (1918364)Instruction limit reached! % 174.44/25.00 % (1918364)------------------------------ % 174.44/25.00 % (1918364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.44/25.00 % (1918364)CaDiCaL version: 2.1.3 % 174.44/25.00 % (1918364)Termination reason: Instruction limit % 174.44/25.00 % (1918364)Termination phase: Saturation % 174.44/25.00 % (1918364)Time elapsed: 0.101 s % 174.44/25.00 % (1918364)Peak memory usage: 11 MB % 174.44/25.00 % (1918364)Instructions burned: 234 (million) % 174.44/25.00 % (1918367)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=340904174:i=262:rtra=on_2779 on theBenchmark for (2779ds/262Mi) % 174.44/25.00 % (1918367)Instruction limit reached! % 174.44/25.00 % (1918367)------------------------------ % 174.44/25.00 % (1918367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.44/25.00 % (1918367)CaDiCaL version: 2.1.3 % 174.44/25.00 % (1918367)Termination reason: Instruction limit % 174.44/25.00 % (1918367)Termination phase: Saturation % 174.44/25.00 % (1918367)Time elapsed: 0.175 s % 174.44/25.00 % (1918367)Peak memory usage: 12 MB % 174.44/25.00 % (1918367)Instructions burned: 263 (million) % 174.44/25.00 % (1918375)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=210850610:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2777 on theBenchmark for (2777ds/318Mi) % 174.44/25.00 % (1918043)Instruction limit reached! % 174.44/25.00 % (1918043)------------------------------ % 174.44/25.00 % (1918043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.44/25.00 % (1918043)CaDiCaL version: 2.1.3 % 174.44/25.00 % (1918043)Termination reason: Instruction limit % 174.44/25.00 % (1918043)Termination phase: Saturation % 174.44/25.00 % (1918043)Time elapsed: 8.347 s % 174.44/25.00 % (1918043)Peak memory usage: 16 MB % 174.44/25.00 % (1918043)Instructions burned: 28122 (million) % 174.44/25.00 % (1918381)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2489122123:i=1428:nm=2:rtra=on_2775 on theBenchmark for (2775ds/1428Mi) % 174.44/25.00 % (1918375)Instruction limit reached! % 174.44/25.00 % (1918375)------------------------------ % 174.44/25.00 % (1918375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.44/25.00 % (1918375)CaDiCaL version: 2.1.3 % 174.44/25.00 % (1918375)Termination reason: Instruction limit % 174.44/25.00 % (1918375)Termination phase: Saturation % 174.44/25.00 % (1918375)Time elapsed: 0.212 s % 174.44/25.00 % (1918375)Peak memory usage: 12 MB % 174.44/25.00 % (1918375)Instructions burned: 318 (million) % 174.44/25.00 % Detected minimum model sizes of [1] % 174.44/25.00 % Detected maximum model sizes of [3] % 174.44/25.00 % TRYING [1] % 174.44/25.00 % TRYING [2] % 174.44/25.00 % Finite Model Found! % 174.44/25.00 % SZS status Satisfiable for theBenchmark % 174.44/25.00 % (1918381)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 174.44/25.00 % (1918381)------------------------------ % 174.44/25.00 % (1918381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.44/25.00 % (1918381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918381)CaDiCaL version: 2.1.3 % 188.60/26.92 % (1918381)Termination reason: Unknown % 188.60/26.92 % (1918381)Termination phase: Finite model building constraint generation % 188.60/26.92 % (1918381)Time elapsed: 0.003 s % 188.60/26.92 % (1918381)Peak memory usage: 11 MB % 188.60/26.92 % (1918381)Instructions burned: 7 (million) % 188.60/26.92 % (1918383)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=201763347:i=262:bd=preordered:rtra=on:fsd=on_2774 on theBenchmark for (2774ds/262Mi) % 188.60/26.92 % (1918384)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=3429565023:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/1368Mi) % 188.60/26.92 % (1918384)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 188.60/26.92 % (1918384)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 188.60/26.92 % (1918383)Instruction limit reached! % 188.60/26.92 % (1918383)------------------------------ % 188.60/26.92 % (1918383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.60/26.92 % (1918383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918383)CaDiCaL version: 2.1.3 % 188.60/26.92 % (1918383)Termination reason: Instruction limit % 188.60/26.92 % (1918383)Termination phase: Saturation % 188.60/26.92 % (1918383)Time elapsed: 0.183 s % 188.60/26.92 % (1918383)Peak memory usage: 12 MB % 188.60/26.92 % (1918383)Instructions burned: 262 (million) % 188.60/26.92 % (1918390)ott-21_1_sil=16000:si=on:fs=off:random_seed=541621961:i=360:av=off:fsr=off:rtra=on_2772 on theBenchmark for (2772ds/360Mi) % 188.60/26.92 % (1918390)Instruction limit reached! % 188.60/26.92 % (1918390)------------------------------ % 188.60/26.92 % (1918390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.60/26.92 % (1918390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918390)CaDiCaL version: 2.1.3 % 188.60/26.92 % (1918390)Termination reason: Instruction limit % 188.60/26.92 % (1918390)Termination phase: Saturation % 188.60/26.92 % (1918390)Time elapsed: 0.163 s % 188.60/26.92 % (1918390)Peak memory usage: 14 MB % 188.60/26.92 % (1918390)Instructions burned: 361 (million) % 188.60/26.92 % (1918394)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3131498295:i=954:bd=all:rtra=on_2770 on theBenchmark for (2770ds/954Mi) % 188.60/26.92 % (1918384)Instruction limit reached! % 188.60/26.92 % (1918384)------------------------------ % 188.60/26.92 % (1918384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.60/26.92 % (1918384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918384)CaDiCaL version: 2.1.3 % 188.60/26.92 % (1918384)Termination reason: Instruction limit % 188.60/26.92 % (1918384)Termination phase: Saturation % 188.60/26.92 % (1918384)Time elapsed: 0.794 s % 188.60/26.92 % (1918384)Peak memory usage: 14 MB % 188.60/26.92 % (1918384)Instructions burned: 1369 (million) % 188.60/26.92 % (1918404)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2081594332:fmbsr=1.3:i=1730:ins=25:rtra=on_2766 on theBenchmark for (2766ds/1730Mi) % 188.60/26.92 % Detected minimum model sizes of [1] % 188.60/26.92 % Detected maximum model sizes of [2] % 188.60/26.92 % TRYING [1] % 188.60/26.92 % TRYING [2] % 188.60/26.92 % Finite Model Found! % 188.60/26.92 % SZS status Satisfiable for theBenchmark % 188.60/26.92 % (1918404)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 188.60/26.92 % (1918404)------------------------------ % 188.60/26.92 % (1918404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.60/26.92 % (1918404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918404)CaDiCaL version: 2.1.3 % 188.60/26.92 % (1918404)Termination reason: Unknown % 188.60/26.92 % (1918404)Termination phase: Finite model building constraint generation % 188.60/26.92 % (1918404)Time elapsed: 0.006 s % 188.60/26.92 % (1918404)Peak memory usage: 11 MB % 188.60/26.92 % (1918404)Instructions burned: 6 (million) % 188.60/26.92 % (1918406)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=390331721:i=2358:rtra=on_2766 on theBenchmark for (2766ds/2358Mi) % 188.60/26.92 % (1918394)Instruction limit reached! % 188.60/26.92 % (1918394)------------------------------ % 188.60/26.92 % (1918394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.60/26.92 % (1918394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.60/26.92 % (1918394)CaDiCaL version: 2.1.3 % 236.29/33.69 % (1918394)Termination reason: Instruction limit % 236.29/33.69 % (1918394)Termination phase: Saturation % 236.29/33.69 % (1918394)Time elapsed: 0.491 s % 236.29/33.69 % (1918394)Peak memory usage: 12 MB % 236.29/33.69 % (1918394)Instructions burned: 955 (million) % 236.29/33.69 % (1918408)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=689058843:i=1778:ins=1:rtra=on_2765 on theBenchmark for (2765ds/1778Mi) % 236.29/33.69 % Exception at run slice level % 236.29/33.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.29/33.69 % (1918412)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=489408733:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2765 on theBenchmark for (2765ds/1384Mi) % 236.29/33.69 % (1918412)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 236.29/33.69 % (1918412)Instruction limit reached! % 236.29/33.69 % (1918412)------------------------------ % 236.29/33.69 % (1918412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.29/33.69 % (1918412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.29/33.69 % (1918412)CaDiCaL version: 2.1.3 % 236.29/33.69 % (1918412)Termination reason: Instruction limit % 236.29/33.69 % (1918412)Termination phase: Saturation % 236.29/33.69 % (1918412)Time elapsed: 0.480 s % 236.29/33.69 % (1918412)Peak memory usage: 13 MB % 236.29/33.69 % (1918412)Instructions burned: 1386 (million) % 236.29/33.69 % (1918426)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1544157224:i=1758:kws=inv_precedence:fsr=off:rtra=on_2760 on theBenchmark for (2760ds/1758Mi) % 236.29/33.69 % (1918426)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 236.29/33.69 % (1918426)Instruction limit reached! % 236.29/33.69 % (1918426)------------------------------ % 236.29/33.69 % (1918426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.29/33.69 % (1918426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.29/33.69 % (1918426)CaDiCaL version: 2.1.3 % 236.29/33.69 % (1918426)Termination reason: Instruction limit % 236.29/33.69 % (1918426)Termination phase: Saturation % 236.29/33.69 % (1918426)Time elapsed: 0.574 s % 236.29/33.69 % (1918426)Peak memory usage: 12 MB % 236.29/33.69 % (1918426)Instructions burned: 1761 (million) % 236.29/33.69 % (1918440)fmb+10_1_sil=64000:si=on:random_seed=2365834381:i=44122:nm=2:rtra=on:gsp=on_2754 on theBenchmark for (2754ds/44122Mi) % 236.29/33.69 % (1918440)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 236.29/33.69 % Detected minimum model sizes of [1] % 236.29/33.69 % Detected maximum model sizes of [2] % 236.29/33.69 % TRYING [1] % 236.29/33.69 % TRYING [2] % 236.29/33.69 % Finite Model Found! % 236.29/33.69 % SZS status Satisfiable for theBenchmark % 236.29/33.69 % (1918440)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 236.29/33.69 % (1918440)------------------------------ % 236.29/33.69 % (1918440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.29/33.69 % (1918440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.29/33.69 % (1918440)CaDiCaL version: 2.1.3 % 236.29/33.69 % (1918440)Termination reason: Unknown % 236.29/33.69 % (1918440)Termination phase: Finite model building constraint generation % 236.29/33.69 % (1918440)Time elapsed: 0.006 s % 236.29/33.69 % (1918440)Peak memory usage: 11 MB % 236.29/33.69 % (1918440)Instructions burned: 6 (million) % 236.29/33.69 % (1918443)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4279849616:i=19030:nm=5:rtra=on_2754 on theBenchmark for (2754ds/19030Mi) % 236.29/33.69 % Detected minimum model sizes of [1] % 236.29/33.69 % Detected maximum model sizes of [2] % 236.29/33.69 % fmb_start_size (= 20) larger than a detected sort maximum size! % 236.29/33.69 % (1918443)Refutation not found, incomplete strategy % 236.29/33.69 % (1918443)------------------------------ % 236.29/33.69 % (1918443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.29/33.69 % (1918443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.29/33.69 % (1918443)CaDiCaL version: 2.1.3 % 236.29/33.69 % (1918443)Termination reason: Refutation not found, incomplete strategy % 236.29/33.69 % (1918443)Time elapsed: 0.006 s % 236.29/33.69 % (1918443)Peak memory usage: 10 MB % 236.29/33.69 % (1918443)Instructions burned: 6 (million) % 236.29/33.69 % (1918443)------------------------------ % 236.29/33.69 % (1918443)------------------------------ % 236.29/33.69 % (1918445)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=466297492:fmbsr=1.7:i=1840:rtra=on_2753 on theBenchmark for (2753ds/1840Mi) % 267.84/38.07 % Detected minimum model sizes of [1] % 267.84/38.07 % Detected maximum model sizes of [2] % 267.84/38.07 % fmb_start_size (= 8) larger than a detected sort maximum size! % 267.84/38.07 % (1918445)Refutation not found, incomplete strategy % 267.84/38.07 % (1918445)------------------------------ % 267.84/38.07 % (1918445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.84/38.07 % (1918445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.84/38.07 % (1918445)CaDiCaL version: 2.1.3 % 267.84/38.07 % (1918445)Termination reason: Refutation not found, incomplete strategy % 267.84/38.07 % (1918445)Time elapsed: 0.003 s % 267.84/38.07 % (1918445)Peak memory usage: 10 MB % 267.84/38.07 % (1918445)Instructions burned: 6 (million) % 267.84/38.07 % (1918445)------------------------------ % 267.84/38.07 % (1918445)------------------------------ % 267.84/38.07 % (1918449)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3236866410:i=10262:rtra=on_2753 on theBenchmark for (2753ds/10262Mi) % 267.84/38.07 % (1918449)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 267.84/38.07 % (1918406)Instruction limit reached! % 267.84/38.07 % (1918406)------------------------------ % 267.84/38.07 % (1918406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.84/38.07 % (1918406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.84/38.07 % (1918406)CaDiCaL version: 2.1.3 % 267.84/38.07 % (1918406)Termination reason: Instruction limit % 267.84/38.07 % (1918406)Termination phase: Saturation % 267.84/38.07 % (1918406)Time elapsed: 1.293 s % 267.84/38.07 % (1918406)Peak memory usage: 12 MB % 267.84/38.07 % (1918406)Instructions burned: 2358 (million) % 267.84/38.07 % (1918455)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1459958098:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2752 on theBenchmark for (2752ds/2944Mi) % 267.84/38.07 % (1918455)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 267.84/38.07 % (1918455)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 267.84/38.07 % (1918455)Instruction limit reached! % 267.84/38.07 % (1918455)------------------------------ % 267.84/38.07 % (1918455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.84/38.07 % (1918455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.84/38.07 % (1918455)CaDiCaL version: 2.1.3 % 267.84/38.07 % (1918455)Termination reason: Instruction limit % 267.84/38.07 % (1918455)Termination phase: Saturation % 267.84/38.07 % (1918455)Time elapsed: 1.773 s % 267.84/38.07 % (1918455)Peak memory usage: 14 MB % 267.84/38.07 % (1918455)Instructions burned: 2944 (million) % 267.84/38.07 % (1918492)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1651004089:i=12648:rtra=on_2734 on theBenchmark for (2734ds/12648Mi) % 267.84/38.07 % Detected minimum model sizes of [1] % 267.84/38.07 % Detected maximum model sizes of [2] % 267.84/38.07 % fmb_start_size (= 77) larger than a detected sort maximum size! % 267.84/38.07 % (1918492)Refutation not found, incomplete strategy % 267.84/38.07 % (1918492)------------------------------ % 267.84/38.07 % (1918492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.84/38.07 % (1918492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.84/38.07 % (1918492)CaDiCaL version: 2.1.3 % 267.84/38.07 % (1918492)Termination reason: Refutation not found, incomplete strategy % 267.84/38.07 % (1918492)Time elapsed: 0.004 s % 267.84/38.07 % (1918492)Peak memory usage: 11 MB % 267.84/38.07 % (1918492)Instructions burned: 6 (million) % 267.84/38.07 % (1918492)------------------------------ % 267.84/38.07 % (1918492)------------------------------ % 267.84/38.07 % (1918494)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=713888804:fmbsr=2.30978:i=4348:rtra=on_2734 on theBenchmark for (2734ds/4348Mi) % 267.84/38.07 % TRYING [16] % 267.84/38.07 % Finite Model Found! % 267.84/38.07 % SZS status Satisfiable for theBenchmark % 267.84/38.07 % (1918494)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 267.84/38.07 % (1918494)------------------------------ % 267.84/38.07 % (1918494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.84/38.07 % (1918494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.84/38.07 % (1918494)CaDiCaL version: 2.1.3 % 267.84/38.07 % (1918494)Termination reason: UTerminated % 300.22/42.64 % Vampire exiting % 300.22/42.64 Terminated %------------------------------------------------------------------------------