%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SYO176^5 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:49:06 AM UTC 2026 % Result : CounterSatisfiable 1.60s 0.55s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SYO176^5 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.18 % Computer : n001.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Tue Sep 29 16:43:06 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 Running first-order model finding % 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.60/0.55 % (1474466)Will run a generic schedule for satisfiability detection. % 1.60/0.55 % (1474475)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=958526747:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.60/0.55 % (1474472)% WARNING: option uhcvi not known. % 1.60/0.55 % (1474473)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2539003721:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.60/0.55 % (1474472)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1052522688:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.60/0.55 % (1474471)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2779560117_2999 on theBenchmark for (2999ds/0Mi) % 1.60/0.55 % (1474474)dis+10_1_sil=32000:sp=arity:random_seed=3483288897:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.60/0.55 % (1474477)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1611885129:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.60/0.55 % (1474476)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3426209021:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.60/0.55 % Detected minimum model sizes of [1] % 1.60/0.55 % Detected maximum model sizes of [13] % 1.60/0.55 % TRYING [1] % 1.60/0.55 % TRYING [2] % 1.60/0.55 % Finite Model Found! % 1.60/0.55 % SZS status CounterSatisfiable for theBenchmark % 1.60/0.55 % (1474471)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 1.60/0.55 % (1474471)------------------------------ % 1.60/0.55 % (1474471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.60/0.55 % (1474471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.60/0.55 % (1474471)CaDiCaL version: 2.1.3 % 1.60/0.55 % (1474471)Termination reason: Unknown % 1.60/0.55 % (1474471)Termination phase: Finite model building constraint generation % 1.60/0.55 % (1474471)Time elapsed: 0.003 s % 1.60/0.55 % (1474471)Peak memory usage: 11 MB % 1.60/0.55 % (1474471)Instructions burned: 4 (million) % 1.60/0.55 % (1474475)Instruction limit reached! % 1.60/0.55 % (1474475)------------------------------ % 1.60/0.55 % (1474475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.60/0.55 % (1474475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.60/0.55 % (1474475)CaDiCaL version: 2.1.3 % 1.60/0.55 % (1474475)Termination reason: Instruction limit % 1.60/0.55 % (1474475)Termination phase: Saturation % 1.60/0.55 % (1474475)Time elapsed: 0.026 s % 1.60/0.55 % (1474475)Peak memory usage: 12 MB % 1.60/0.55 % (1474475)Instructions burned: 120 (million) % 1.60/0.55 % (1474485)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1774505255:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.60/0.55 % Detected minimum model sizes of [1] % 1.60/0.55 % Detected maximum model sizes of [14] % 1.60/0.55 % TRYING [1] % 1.60/0.55 % TRYING [2] % 1.60/0.55 % Finite Model Found! % 1.60/0.55 % SZS status CounterSatisfiable for theBenchmark % 1.60/0.55 % (1474485)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 1.60/0.55 % (1474485)------------------------------ % 1.60/0.55 % (1474485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.60/0.55 % (1474485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.60/0.55 % (1474485)CaDiCaL version: 2.1.3 % 1.60/0.55 % (1474485)Termination reason: Unknown % 1.60/0.55 % (1474485)Termination phase: Finite model building constraint generation % 1.60/0.55 % (1474485)Time elapsed: 0.002 s % 1.60/0.55 % (1474485)Peak memory usage: 11 MB % 1.60/0.55 % (1474485)Instructions burned: 3 (million) % 1.60/0.55 % (1474488)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=1327405967:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 1.60/0.55 % (1474474)Instruction limit reached! % 1.60/0.55 % (1474474)------------------------------ % 1.60/0.55 % (1474474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.60/0.55 % (1474474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.60/0.55 % (1474474)CaDiCaL version: 2.1.3 % 1.60/0.55 % (1474474)Termination reason: Instruction limit % 1.60/0.55 % (1474474)Termination phase: Saturation % 1.60/0.55 % (1474474)Time elapsed: 0.044 s % 1.60/0.55 % (1474474)Peak memory usage: 11 MB % 1.60/0.55 % (1474474)Instructions burned: 105 (million) % 1.60/0.55 % (1474486)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1657821436:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.66/0.80 % (1474490)ott-21_1_sil=16000:fs=off:random_seed=2921932090:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.66/0.80 % (1474477)Instruction limit reached! % 3.66/0.80 % (1474477)------------------------------ % 3.66/0.80 % (1474477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474477)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474477)Termination reason: Instruction limit % 3.66/0.80 % (1474477)Termination phase: Saturation % 3.66/0.80 % (1474477)Time elapsed: 0.076 s % 3.66/0.80 % (1474477)Peak memory usage: 12 MB % 3.66/0.80 % (1474477)Instructions burned: 161 (million) % 3.66/0.80 % (1474476)Instruction limit reached! % 3.66/0.80 % (1474476)------------------------------ % 3.66/0.80 % (1474476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474476)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474476)Termination reason: Instruction limit % 3.66/0.80 % (1474476)Termination phase: Saturation % 3.66/0.80 % (1474476)Time elapsed: 0.081 s % 3.66/0.80 % (1474476)Peak memory usage: 12 MB % 3.66/0.80 % (1474476)Instructions burned: 134 (million) % 3.66/0.80 % (1474495)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=184670952:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.66/0.80 % (1474497)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2236139964:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.66/0.80 % Detected minimum model sizes of [1] % 3.66/0.80 % Detected maximum model sizes of [13] % 3.66/0.80 % TRYING [1] % 3.66/0.80 % TRYING [2] % 3.66/0.80 % Finite Model Found! % 3.66/0.80 % SZS status CounterSatisfiable for theBenchmark % 3.66/0.80 % (1474497)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 3.66/0.80 % (1474497)------------------------------ % 3.66/0.80 % (1474497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474497)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474497)Termination reason: Unknown % 3.66/0.80 % (1474497)Termination phase: Finite model building constraint generation % 3.66/0.80 % (1474497)Time elapsed: 0.002 s % 3.66/0.80 % (1474497)Peak memory usage: 11 MB % 3.66/0.80 % (1474497)Instructions burned: 3 (million) % 3.66/0.80 % (1474509)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1431537974:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.66/0.80 % (1474486)Instruction limit reached! % 3.66/0.80 % (1474486)------------------------------ % 3.66/0.80 % (1474486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474486)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474486)Termination reason: Instruction limit % 3.66/0.80 % (1474486)Termination phase: Saturation % 3.66/0.80 % (1474486)Time elapsed: 0.065 s % 3.66/0.80 % (1474486)Peak memory usage: 11 MB % 3.66/0.80 % (1474486)Instructions burned: 133 (million) % 3.66/0.80 % (1474520)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=435584701:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.66/0.80 % (1474490)Instruction limit reached! % 3.66/0.80 % (1474490)------------------------------ % 3.66/0.80 % (1474490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474490)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474490)Termination reason: Instruction limit % 3.66/0.80 % (1474490)Termination phase: Saturation % 3.66/0.80 % (1474490)Time elapsed: 0.081 s % 3.66/0.80 % (1474490)Peak memory usage: 12 MB % 3.66/0.80 % (1474490)Instructions burned: 182 (million) % 3.66/0.80 % Detected minimum model sizes of [1] % 3.66/0.80 % Detected maximum model sizes of [13] % 3.66/0.80 % fmb_start_size (= 14) larger than a detected sort maximum size! % 3.66/0.80 % (1474520)Refutation not found, incomplete strategy % 3.66/0.80 % (1474520)------------------------------ % 3.66/0.80 % (1474520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.80 % (1474520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.80 % (1474520)CaDiCaL version: 2.1.3 % 3.66/0.80 % (1474520)Termination reason: Refutation not found, incomplete strategy % 9.87/1.91 % (1474520)Time elapsed: 0.002 s % 9.87/1.91 % (1474520)Peak memory usage: 10 MB % 9.87/1.91 % (1474520)Instructions burned: 3 (million) % 9.87/1.91 % (1474520)------------------------------ % 9.87/1.91 % (1474520)------------------------------ % 9.87/1.91 % (1474529)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=1146219835: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) % 9.87/1.91 % (1474531)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3594736818:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 9.87/1.91 % (1474488)Instruction limit reached! % 9.87/1.91 % (1474488)------------------------------ % 9.87/1.91 % (1474488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.87/1.91 % (1474488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.87/1.91 % (1474488)CaDiCaL version: 2.1.3 % 9.87/1.91 % (1474488)Termination reason: Instruction limit % 9.87/1.91 % (1474488)Termination phase: Saturation % 9.87/1.91 % (1474488)Time elapsed: 0.140 s % 9.87/1.91 % (1474488)Peak memory usage: 13 MB % 9.87/1.91 % (1474488)Instructions burned: 685 (million) % 9.87/1.91 % (1474546)fmb+10_1_sil=64000:random_seed=495345718:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 9.87/1.91 % Detected minimum model sizes of [1] % 9.87/1.91 % Detected maximum model sizes of [13] % 9.87/1.91 % TRYING [1] % 9.87/1.91 % TRYING [2] % 9.87/1.91 % Finite Model Found! % 9.87/1.91 % SZS status CounterSatisfiable for theBenchmark % 9.87/1.91 % (1474546)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.87/1.91 % (1474546)------------------------------ % 9.87/1.91 % (1474546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.87/1.91 % (1474546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.87/1.91 % (1474546)CaDiCaL version: 2.1.3 % 9.87/1.91 % (1474546)Termination reason: Unknown % 9.87/1.91 % (1474546)Termination phase: Finite model building constraint generation % 9.87/1.91 % (1474546)Time elapsed: 0.001 s % 9.87/1.91 % (1474546)Peak memory usage: 11 MB % 9.87/1.91 % (1474546)Instructions burned: 4 (million) % 9.87/1.91 % (1474552)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2746162724:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 9.87/1.91 % Detected minimum model sizes of [1] % 9.87/1.91 % Detected maximum model sizes of [13] % 9.87/1.91 % fmb_start_size (= 20) larger than a detected sort maximum size! % 9.87/1.91 % (1474552)Refutation not found, incomplete strategy % 9.87/1.91 % (1474552)------------------------------ % 9.87/1.91 % (1474552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.87/1.91 % (1474552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.87/1.91 % (1474552)CaDiCaL version: 2.1.3 % 9.87/1.91 % (1474552)Termination reason: Refutation not found, incomplete strategy % 9.87/1.91 % (1474552)Time elapsed: 0.0000 s % 9.87/1.91 % (1474552)Peak memory usage: 11 MB % 9.87/1.91 % (1474552)Instructions burned: 2 (million) % 9.87/1.91 % (1474552)------------------------------ % 9.87/1.91 % (1474552)------------------------------ % 9.87/1.91 % (1474560)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2687140462:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 9.87/1.91 % Detected minimum model sizes of [1] % 9.87/1.91 % Detected maximum model sizes of [13] % 9.87/1.91 % TRYING [8] % 9.87/1.91 % Finite Model Found! % 9.87/1.91 % SZS status CounterSatisfiable for theBenchmark % 9.87/1.91 % (1474560)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.87/1.91 % (1474560)------------------------------ % 9.87/1.91 % (1474560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.87/1.91 % (1474560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.87/1.91 % (1474560)CaDiCaL version: 2.1.3 % 9.87/1.91 % (1474560)Termination reason: Unknown % 9.87/1.91 % (1474560)Termination phase: Finite model building constraint generation % 9.87/1.91 % (1474560)Time elapsed: 0.001 s % 9.87/1.91 % (1474560)Peak memory usage: 11 MB % 9.87/1.91 % (1474560)Instructions burned: 3 (million) % 9.87/1.91 % (1474567)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2966824383:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 9.87/1.91 % (1474495)Instruction limit reached! % 9.87/1.91 % (1474495)------------------------------ % 9.87/1.91 % (1474495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474495)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474495)Termination reason: Instruction limit % 15.09/2.45 % (1474495)Termination phase: Saturation % 15.09/2.45 % (1474495)Time elapsed: 0.188 s % 15.09/2.45 % (1474495)Peak memory usage: 12 MB % 15.09/2.45 % (1474495)Instructions burned: 477 (million) % 15.09/2.45 % (1474597)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=50340098:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 15.09/2.45 % (1474529)Instruction limit reached! % 15.09/2.45 % (1474529)------------------------------ % 15.09/2.45 % (1474529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474529)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474529)Termination reason: Instruction limit % 15.09/2.45 % (1474529)Termination phase: Saturation % 15.09/2.45 % (1474529)Time elapsed: 0.252 s % 15.09/2.45 % (1474529)Peak memory usage: 12 MB % 15.09/2.45 % (1474529)Instructions burned: 692 (million) % 15.09/2.45 % (1474643)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1121130417:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 15.09/2.45 % Detected minimum model sizes of [1] % 15.09/2.45 % Detected maximum model sizes of [13] % 15.09/2.45 % fmb_start_size (= 77) larger than a detected sort maximum size! % 15.09/2.45 % (1474643)Refutation not found, incomplete strategy % 15.09/2.45 % (1474643)------------------------------ % 15.09/2.45 % (1474643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474643)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474643)Termination reason: Refutation not found, incomplete strategy % 15.09/2.45 % (1474643)Time elapsed: 0.002 s % 15.09/2.45 % (1474643)Peak memory usage: 11 MB % 15.09/2.45 % (1474643)Instructions burned: 3 (million) % 15.09/2.45 % (1474643)------------------------------ % 15.09/2.45 % (1474643)------------------------------ % 15.09/2.45 % (1474660)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2151331766:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 15.09/2.45 % Detected minimum model sizes of [1] % 15.09/2.45 % Detected maximum model sizes of [26] % 15.09/2.45 % TRYING [16] % 15.09/2.45 % (1474531)Instruction limit reached! % 15.09/2.45 % (1474531)------------------------------ % 15.09/2.45 % (1474531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474531)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474531)Termination reason: Instruction limit % 15.09/2.45 % (1474531)Termination phase: Saturation % 15.09/2.45 % (1474531)Time elapsed: 0.318 s % 15.09/2.45 % (1474531)Peak memory usage: 12 MB % 15.09/2.45 % (1474531)Instructions burned: 879 (million) % 15.09/2.45 % Finite Model Found! % 15.09/2.45 % SZS status CounterSatisfiable for theBenchmark % 15.09/2.45 % (1474660)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 15.09/2.45 % (1474660)------------------------------ % 15.09/2.45 % (1474660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474660)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474660)Termination reason: Unknown % 15.09/2.45 % (1474660)Termination phase: Finite model building constraint generation % 15.09/2.45 % (1474660)Time elapsed: 0.035 s % 15.09/2.45 % (1474660)Peak memory usage: 13 MB % 15.09/2.45 % (1474660)Instructions burned: 96 (million) % 15.09/2.45 % (1474671)ott-2_1_sil=16000:newcnf=on:random_seed=3751999298:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 15.09/2.45 % (1474672)ott+10_1_sil=32000:tgt=ground:random_seed=2727624775:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 15.09/2.45 % (1474509)Instruction limit reached! % 15.09/2.45 % (1474509)------------------------------ % 15.09/2.45 % (1474509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.45 % (1474509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.45 % (1474509)CaDiCaL version: 2.1.3 % 15.09/2.45 % (1474509)Termination reason: Instruction limit % 15.09/2.45 % (1474509)Termination phase: Saturation % 15.09/2.45 % (1474509)Time elapsed: 0.415 s % 15.09/2.45 % (1474509)Peak memory usage: 12 MB % 38.60/5.74 % (1474509)Instructions burned: 1182 (million) % 38.60/5.74 % (1474675)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4247702288:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 38.60/5.74 % Detected minimum model sizes of [1] % 38.60/5.74 % Detected maximum model sizes of [13] % 38.60/5.74 % TRYING [1] % 38.60/5.74 % TRYING [2] % 38.60/5.74 % Finite Model Found! % 38.60/5.74 % SZS status CounterSatisfiable for theBenchmark % 38.60/5.74 % (1474675)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 38.60/5.74 % (1474675)------------------------------ % 38.60/5.74 % (1474675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.60/5.74 % (1474675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.60/5.74 % (1474675)CaDiCaL version: 2.1.3 % 38.60/5.74 % (1474675)Termination reason: Unknown % 38.60/5.74 % (1474675)Termination phase: Finite model building constraint generation % 38.60/5.74 % (1474675)Time elapsed: 0.002 s % 38.60/5.74 % (1474675)Peak memory usage: 11 MB % 38.60/5.74 % (1474675)Instructions burned: 4 (million) % 38.60/5.74 % (1474677)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2133763929:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 38.60/5.74 % (1474671)Instruction limit reached! % 38.60/5.74 % (1474671)------------------------------ % 38.60/5.74 % (1474671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.60/5.74 % (1474671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.60/5.74 % (1474671)CaDiCaL version: 2.1.3 % 38.60/5.74 % (1474671)Termination reason: Instruction limit % 38.60/5.74 % (1474671)Termination phase: Saturation % 38.60/5.74 % (1474671)Time elapsed: 0.317 s % 38.60/5.74 % (1474671)Peak memory usage: 12 MB % 38.60/5.74 % (1474671)Instructions burned: 869 (million) % 38.60/5.74 % (1474597)Instruction limit reached! % 38.60/5.74 % (1474597)------------------------------ % 38.60/5.74 % (1474597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.60/5.74 % (1474597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.60/5.74 % (1474597)CaDiCaL version: 2.1.3 % 38.60/5.74 % (1474597)Termination reason: Instruction limit % 38.60/5.74 % (1474597)Termination phase: Saturation % 38.60/5.74 % (1474597)Time elapsed: 0.527 s % 38.60/5.74 % (1474597)Peak memory usage: 13 MB % 38.60/5.74 % (1474597)Instructions burned: 1474 (million) % 38.60/5.74 % (1474679)dis+21_1_sil=32000:sas=cadical:random_seed=1500559736:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 38.60/5.74 % (1474680)ott+11_1_sil=16000:gs=on:random_seed=3617391043:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2991 on theBenchmark for (2991ds/2251Mi) % 38.60/5.74 % (1474567)Instruction limit reached! % 38.60/5.74 % (1474567)------------------------------ % 38.60/5.74 % (1474567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.60/5.74 % (1474567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.60/5.74 % (1474567)CaDiCaL version: 2.1.3 % 38.60/5.74 % (1474567)Termination reason: Instruction limit % 38.60/5.74 % (1474567)Termination phase: Saturation % 38.60/5.74 % (1474567)Time elapsed: 1.055 s % 38.60/5.74 % (1474567)Peak memory usage: 18 MB % 38.60/5.74 % (1474567)Instructions burned: 5134 (million) % 38.60/5.74 % (1474683)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3070196228:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 38.60/5.74 % Detected minimum model sizes of [1] % 38.60/5.74 % Detected maximum model sizes of [14] % 38.60/5.74 % TRYING [7] % 38.60/5.74 % Finite Model Found! % 38.60/5.74 % SZS status CounterSatisfiable for theBenchmark % 38.60/5.74 % (1474683)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 38.60/5.74 % (1474683)------------------------------ % 38.60/5.74 % (1474683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.60/5.74 % (1474683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.60/5.74 % (1474683)CaDiCaL version: 2.1.3 % 38.60/5.74 % (1474683)Termination reason: Unknown % 38.60/5.74 % (1474683)Termination phase: Finite model building constraint generation % 38.60/5.74 % (1474683)Time elapsed: 0.007 s % 38.60/5.74 % (1474683)Peak memory usage: 10 MB % 38.60/5.74 % (1474683)Instructions burned: 16 (million) % 38.60/5.74 % (1474685)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1482902360:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi) % 38.60/5.74 % (1474680)Instruction limit reached! % 38.60/5.74 % (1474680)------------------------------ % 82.73/11.95 % (1474680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/11.95 % (1474680)CaDiCaL version: 2.1.3 % 82.73/11.95 % (1474680)Termination reason: Instruction limit % 82.73/11.95 % (1474680)Termination phase: Saturation % 82.73/11.95 % (1474680)Time elapsed: 0.791 s % 82.73/11.95 % (1474680)Peak memory usage: 12 MB % 82.73/11.95 % (1474680)Instructions burned: 2253 (million) % 82.73/11.95 % (1474687)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2268338677:i=29340_2983 on theBenchmark for (2983ds/29340Mi) % 82.73/11.95 % (1474677)Instruction limit reached! % 82.73/11.95 % (1474677)------------------------------ % 82.73/11.95 % (1474677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/11.95 % (1474677)CaDiCaL version: 2.1.3 % 82.73/11.95 % (1474677)Termination reason: Instruction limit % 82.73/11.95 % (1474677)Termination phase: Saturation % 82.73/11.95 % (1474677)Time elapsed: 1.283 s % 82.73/11.95 % (1474677)Peak memory usage: 13 MB % 82.73/11.95 % (1474677)Instructions burned: 3513 (million) % 82.73/11.95 % (1474689)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2071458785:i=5211_2981 on theBenchmark for (2981ds/5211Mi) % 82.73/11.95 % (1474685)Instruction limit reached! % 82.73/11.95 % (1474685)------------------------------ % 82.73/11.95 % (1474685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/11.95 % (1474685)CaDiCaL version: 2.1.3 % 82.73/11.95 % (1474685)Termination reason: Instruction limit % 82.73/11.95 % (1474685)Termination phase: Saturation % 82.73/11.95 % (1474685)Time elapsed: 0.828 s % 82.73/11.95 % (1474685)Peak memory usage: 13 MB % 82.73/11.95 % (1474685)Instructions burned: 4596 (million) % 82.73/11.95 % (1474691)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1057198698:i=5497:nm=2_2978 on theBenchmark for (2978ds/5497Mi) % 82.73/11.95 % Detected minimum model sizes of [1] % 82.73/11.95 % Detected maximum model sizes of [13] % 82.73/11.95 % fmb_start_size (= 17) larger than a detected sort maximum size! % 82.73/11.95 % (1474691)Refutation not found, incomplete strategy % 82.73/11.95 % (1474691)------------------------------ % 82.73/11.95 % (1474691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/11.95 % (1474691)CaDiCaL version: 2.1.3 % 82.73/11.95 % (1474691)Termination reason: Refutation not found, incomplete strategy % 82.73/11.95 % (1474691)Time elapsed: 0.001 s % 82.73/11.95 % (1474691)Peak memory usage: 10 MB % 82.73/11.95 % (1474691)Instructions burned: 2 (million) % 82.73/11.95 % (1474691)------------------------------ % 82.73/11.95 % (1474691)------------------------------ % 82.73/11.95 % (1474693)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=160585163:fmbsr=2:i=46332_2978 on theBenchmark for (2978ds/46332Mi) % 82.73/11.95 % Detected minimum model sizes of [1] % 82.73/11.95 % Detected maximum model sizes of [14] % 82.73/11.95 % fmb_start_size (= 15) larger than a detected sort maximum size! % 82.73/11.95 % (1474693)Refutation not found, incomplete strategy % 82.73/11.95 % (1474693)------------------------------ % 82.73/11.95 % (1474693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/11.95 % (1474693)CaDiCaL version: 2.1.3 % 82.73/11.95 % (1474693)Termination reason: Refutation not found, incomplete strategy % 82.73/11.95 % (1474693)Time elapsed: 0.001 s % 82.73/11.95 % (1474693)Peak memory usage: 10 MB % 82.73/11.95 % (1474693)Instructions burned: 2 (million) % 82.73/11.95 % (1474693)------------------------------ % 82.73/11.95 % (1474693)------------------------------ % 82.73/11.95 % (1474695)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=186231969:i=14071_2977 on theBenchmark for (2977ds/14071Mi) % 82.73/11.95 % Detected minimum model sizes of [1] % 82.73/11.95 % Detected maximum model sizes of [13] % 82.73/11.95 % TRYING [12] % 82.73/11.95 % Finite Model Found! % 82.73/11.95 % SZS status CounterSatisfiable for theBenchmark % 82.73/11.95 % (1474695)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.73/11.95 % (1474695)------------------------------ % 82.73/11.95 % (1474695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.73/11.95 % (1474695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474695)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474695)Termination reason: Unknown % 83.69/12.06 % (1474695)Termination phase: Finite model building constraint generation % 83.69/12.06 % (1474695)Time elapsed: 0.001 s % 83.69/12.06 % (1474695)Peak memory usage: 11 MB % 83.69/12.06 % (1474695)Instructions burned: 3 (million) % 83.69/12.06 % (1474697)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=843200797:i=22565:add=on:rawr=on_2977 on theBenchmark for (2977ds/22565Mi) % 83.69/12.06 % (1474679)Instruction limit reached! % 83.69/12.06 % (1474679)------------------------------ % 83.69/12.06 % (1474679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.69/12.06 % (1474679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474679)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474679)Termination reason: Instruction limit % 83.69/12.06 % (1474679)Termination phase: Saturation % 83.69/12.06 % (1474679)Time elapsed: 1.424 s % 83.69/12.06 % (1474679)Peak memory usage: 17 MB % 83.69/12.06 % (1474679)Instructions burned: 3774 (million) % 83.69/12.06 % (1474699)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2311568573:i=8173:av=off_2976 on theBenchmark for (2976ds/8173Mi) % 83.69/12.06 % (1474672)Instruction limit reached! % 83.69/12.06 % (1474672)------------------------------ % 83.69/12.06 % (1474672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.69/12.06 % (1474672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474672)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474672)Termination reason: Instruction limit % 83.69/12.06 % (1474672)Termination phase: Saturation % 83.69/12.06 % (1474672)Time elapsed: 1.850 s % 83.69/12.06 % (1474672)Peak memory usage: 12 MB % 83.69/12.06 % (1474672)Instructions burned: 5116 (million) % 83.69/12.06 % (1474701)dis+10_16:1_sil=16000:random_seed=2883877824:i=9155:fsr=off_2975 on theBenchmark for (2975ds/9155Mi) % 83.69/12.06 % (1474689)Instruction limit reached! % 83.69/12.06 % (1474689)------------------------------ % 83.69/12.06 % (1474689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.69/12.06 % (1474689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474689)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474689)Termination reason: Instruction limit % 83.69/12.06 % (1474689)Termination phase: Saturation % 83.69/12.06 % (1474689)Time elapsed: 1.854 s % 83.69/12.06 % (1474689)Peak memory usage: 15 MB % 83.69/12.06 % (1474689)Instructions burned: 5214 (million) % 83.69/12.06 % (1474703)ott-3_8_sil=64000:random_seed=2432155803:i=20139:bs=on_2962 on theBenchmark for (2962ds/20139Mi) % 83.69/12.06 % (1474699)Instruction limit reached! % 83.69/12.06 % (1474699)------------------------------ % 83.69/12.06 % (1474699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.69/12.06 % (1474699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474699)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474699)Termination reason: Instruction limit % 83.69/12.06 % (1474699)Termination phase: Saturation % 83.69/12.06 % (1474699)Time elapsed: 2.963 s % 83.69/12.06 % (1474699)Peak memory usage: 15 MB % 83.69/12.06 % (1474699)Instructions burned: 8175 (million) % 83.69/12.06 % (1474705)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=209822331:fmbsr=2:i=32576_2947 on theBenchmark for (2947ds/32576Mi) % 83.69/12.06 % Detected minimum model sizes of [1] % 83.69/12.06 % Detected maximum model sizes of [13] % 83.69/12.06 % TRYING [9] % 83.69/12.06 % Finite Model Found! % 83.69/12.06 % SZS status CounterSatisfiable for theBenchmark % 83.69/12.06 % (1474705)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 83.69/12.06 % (1474705)------------------------------ % 83.69/12.06 % (1474705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.69/12.06 % (1474705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.69/12.06 % (1474705)CaDiCaL version: 2.1.3 % 83.69/12.06 % (1474705)Termination reason: Unknown % 83.69/12.06 % (1474705)Termination phase: Finite model building constraint generation % 83.69/12.06 % (1474705)Time elapsed: 0.002 s % 83.69/12.06 % (1474705)Peak memory usage: 11 MB % 83.69/12.06 % (1474705)Instructions burned: 4 (million) % 83.69/12.06 % (1474707)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2481221610:i=11404_2946 on theBenchmark for (2946ds/11404Mi) % 83.69/12.06 % (1474701)Instruction limit reached! % 83.69/12.06 % (1474701)------------------------------ % 83.69/12.06 % (1474701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474701)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474701)Termination reason: Instruction limit % 110.34/15.81 % (1474701)Termination phase: Saturation % 110.34/15.81 % (1474701)Time elapsed: 3.094 s % 110.34/15.81 % (1474701)Peak memory usage: 14 MB % 110.34/15.81 % (1474701)Instructions burned: 9158 (million) % 110.34/15.81 % (1474709)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3722258321:i=14134_2944 on theBenchmark for (2944ds/14134Mi) % 110.34/15.81 % (1474697)Instruction limit reached! % 110.34/15.81 % (1474697)------------------------------ % 110.34/15.81 % (1474697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474697)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474697)Termination reason: Instruction limit % 110.34/15.81 % (1474697)Termination phase: Saturation % 110.34/15.81 % (1474697)Time elapsed: 3.939 s % 110.34/15.81 % (1474697)Peak memory usage: 18 MB % 110.34/15.81 % (1474697)Instructions burned: 22571 (million) % 110.34/15.81 % (1474711)dis+33_16_sil=32000:sac=on:random_seed=204092706:i=15851:nm=0_2938 on theBenchmark for (2938ds/15851Mi) % 110.34/15.81 % (1474707)Instruction limit reached! % 110.34/15.81 % (1474707)------------------------------ % 110.34/15.81 % (1474707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474707)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474707)Termination reason: Instruction limit % 110.34/15.81 % (1474707)Termination phase: Saturation % 110.34/15.81 % (1474707)Time elapsed: 3.811 s % 110.34/15.81 % (1474707)Peak memory usage: 13 MB % 110.34/15.81 % (1474707)Instructions burned: 11405 (million) % 110.34/15.81 % (1474713)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=60349422:avsq=on:i=17627:add=on:amm=off_2908 on theBenchmark for (2908ds/17627Mi) % 110.34/15.81 % (1474709)Instruction limit reached! % 110.34/15.81 % (1474709)------------------------------ % 110.34/15.81 % (1474709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474709)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474709)Termination reason: Instruction limit % 110.34/15.81 % (1474709)Termination phase: Saturation % 110.34/15.81 % (1474709)Time elapsed: 4.701 s % 110.34/15.81 % (1474709)Peak memory usage: 13 MB % 110.34/15.81 % (1474709)Instructions burned: 14134 (million) % 110.34/15.81 % (1474715)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1715591324:s2a=on:i=53295_2897 on theBenchmark for (2897ds/53295Mi) % 110.34/15.81 % (1474703)Instruction limit reached! % 110.34/15.81 % (1474703)------------------------------ % 110.34/15.81 % (1474703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474703)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474703)Termination reason: Instruction limit % 110.34/15.81 % (1474703)Termination phase: Saturation % 110.34/15.81 % (1474703)Time elapsed: 6.513 s % 110.34/15.81 % (1474703)Peak memory usage: 13 MB % 110.34/15.81 % (1474703)Instructions burned: 20139 (million) % 110.34/15.81 % (1474717)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2627841393:i=26857:ins=20_2896 on theBenchmark for (2896ds/26857Mi) % 110.34/15.81 % Detected minimum model sizes of [1] % 110.34/15.81 % Detected maximum model sizes of [13] % 110.34/15.81 % fmb_start_size (= 16) larger than a detected sort maximum size! % 110.34/15.81 % (1474717)Refutation not found, incomplete strategy % 110.34/15.81 % (1474717)------------------------------ % 110.34/15.81 % (1474717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.34/15.81 % (1474717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.34/15.81 % (1474717)CaDiCaL version: 2.1.3 % 110.34/15.81 % (1474717)Termination reason: Refutation not found, incomplete strategy % 110.34/15.81 % (1474717)Time elapsed: 0.001 s % 110.34/15.81 % (1474717)Peak memory usage: 10 MB % 110.34/15.81 % (1474717)Instructions burned: 2 (million) % 110.34/15.81 % (1474717)------------------------------ % 110.34/15.81 % (1474717)------------------------------ % 110.34/15.81 % (1474719)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3333620799:i=28120:bs=on:fsr=off_2896 on theBenchmark for (2896ds/28120Mi) % 110.34/15.81 % (1474687)Instruction limit reached! % 110.34/15.81 % (1474687)------------------------------ % 116.95/16.82 % (1474687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.95/16.82 % (1474687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.95/16.82 % (1474687)CaDiCaL version: 2.1.3 % 116.95/16.82 % (1474687)Termination reason: Instruction limit % 116.95/16.82 % (1474687)Termination phase: Saturation % 116.95/16.82 % (1474687)Time elapsed: 10.018 s % 116.95/16.82 % (1474687)Peak memory usage: 56 MB % 116.95/16.82 % (1474687)Instructions burned: 29342 (million) % 116.95/16.82 % (1474721)fmb+10_1_sil=256000:fmbss=7:random_seed=4138219995:fmbsr=1.6:i=182295_2882 on theBenchmark for (2882ds/182295Mi) % 116.95/16.82 % Detected minimum model sizes of [1] % 116.95/16.82 % Detected maximum model sizes of [13] % 116.95/16.82 % TRYING [7] % 116.95/16.82 % Finite Model Found! % 116.95/16.82 % SZS status CounterSatisfiable for theBenchmark % 116.95/16.82 % (1474721)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 116.95/16.82 % (1474721)------------------------------ % 116.95/16.82 % (1474721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.95/16.82 % (1474721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.95/16.82 % (1474721)CaDiCaL version: 2.1.3 % 116.95/16.82 % (1474721)Termination reason: Unknown % 116.95/16.82 % (1474721)Termination phase: Finite model building constraint generation % 116.95/16.82 % (1474721)Time elapsed: 0.002 s % 116.95/16.82 % (1474721)Peak memory usage: 10 MB % 116.95/16.82 % (1474721)Instructions burned: 4 (million) % 116.95/16.82 % (1474723)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3033991588:i=44625:gsp=on_2882 on theBenchmark for (2882ds/44625Mi) % 116.95/16.82 % Detected minimum model sizes of [1] % 116.95/16.82 % Detected maximum model sizes of [13] % 116.95/16.82 % fmb_start_size (= 21) larger than a detected sort maximum size! % 116.95/16.82 % (1474723)Refutation not found, incomplete strategy % 116.95/16.82 % (1474723)------------------------------ % 116.95/16.82 % (1474723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.95/16.82 % (1474723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.95/16.82 % (1474723)CaDiCaL version: 2.1.3 % 116.95/16.82 % (1474723)Termination reason: Refutation not found, incomplete strategy % 116.95/16.82 % (1474723)Time elapsed: 0.002 s % 116.95/16.82 % (1474723)Peak memory usage: 10 MB % 116.95/16.82 % (1474723)Instructions burned: 3 (million) % 116.95/16.82 % (1474723)------------------------------ % 116.95/16.82 % (1474723)------------------------------ % 116.95/16.82 % (1474725)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1067105526:i=160505_2882 on theBenchmark for (2882ds/160505Mi) % 116.95/16.82 % Detected minimum model sizes of [1] % 116.95/16.82 % Detected maximum model sizes of [13] % 116.95/16.82 % fmb_start_size (= 15) larger than a detected sort maximum size! % 116.95/16.82 % (1474725)Refutation not found, incomplete strategy % 116.95/16.82 % (1474725)------------------------------ % 116.95/16.82 % (1474725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.95/16.82 % (1474725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.95/16.82 % (1474725)CaDiCaL version: 2.1.3 % 116.95/16.82 % (1474725)Termination reason: Refutation not found, incomplete strategy % 116.95/16.82 % (1474725)Time elapsed: 0.002 s % 116.95/16.82 % (1474725)Peak memory usage: 11 MB % 116.95/16.82 % (1474725)Instructions burned: 2 (million) % 116.95/16.82 % (1474725)------------------------------ % 116.95/16.82 % (1474725)------------------------------ % 116.95/16.82 % (1474727)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2026193030:fmbsr=1.3:i=225729_2882 on theBenchmark for (2882ds/225729Mi) % 116.95/16.82 % Detected minimum model sizes of [1] % 116.95/16.82 % Detected maximum model sizes of [13] % 116.95/16.82 % TRYING [10] % 116.95/16.82 % Finite Model Found! % 116.95/16.82 % SZS status CounterSatisfiable for theBenchmark % 116.95/16.82 % (1474727)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 116.95/16.82 % (1474727)------------------------------ % 116.95/16.82 % (1474727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.95/16.82 % (1474727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.95/16.82 % (1474727)CaDiCaL version: 2.1.3 % 116.95/16.82 % (1474727)Termination reason: Unknown % 116.95/16.82 % (1474727)Termination phase: Finite model building constraint generation % 116.95/16.82 % (1474727)Time elapsed: 0.003 s % 116.95/16.82 % (1474727)Peak memory usage: 11 MB % 116.95/16.82 % (1474727)Instructions burned: 4 (million) % 116.95/16.82 % (1474729)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1201642347:fmbsr=2:i=185024:ins=7_2881 on theBenchmark for (2881ds/185024Mi) % 131.17/18.82 % Detected minimum model sizes of [1] % 131.17/18.82 % Detected maximum model sizes of [13] % 131.17/18.82 % TRYING [10] % 131.17/18.82 % Finite Model Found! % 131.17/18.82 % SZS status CounterSatisfiable for theBenchmark % 131.17/18.82 % (1474729)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 131.17/18.82 % (1474729)------------------------------ % 131.17/18.82 % (1474729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.17/18.82 % (1474729)CaDiCaL version: 2.1.3 % 131.17/18.82 % (1474729)Termination reason: Unknown % 131.17/18.82 % (1474729)Termination phase: Finite model building constraint generation % 131.17/18.82 % (1474729)Time elapsed: 0.002 s % 131.17/18.82 % (1474729)Peak memory usage: 11 MB % 131.17/18.82 % (1474729)Instructions burned: 3 (million) % 131.17/18.82 % (1474731)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=13917340:rtra=on_2881 on theBenchmark for (2881ds/0Mi) % 131.17/18.82 % Detected minimum model sizes of [1] % 131.17/18.82 % Detected maximum model sizes of [13] % 131.17/18.82 % TRYING [1] % 131.17/18.82 % TRYING [2] % 131.17/18.82 % Finite Model Found! % 131.17/18.82 % SZS status CounterSatisfiable for theBenchmark % 131.17/18.82 % (1474731)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 131.17/18.82 % (1474731)------------------------------ % 131.17/18.82 % (1474731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.17/18.82 % (1474731)CaDiCaL version: 2.1.3 % 131.17/18.82 % (1474731)Termination reason: Unknown % 131.17/18.82 % (1474731)Termination phase: Finite model building constraint generation % 131.17/18.82 % (1474731)Time elapsed: 0.003 s % 131.17/18.82 % (1474731)Peak memory usage: 11 MB % 131.17/18.82 % (1474731)Instructions burned: 4 (million) % 131.17/18.82 % (1474733)% WARNING: option uhcvi not known. % 131.17/18.82 % (1474733)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1136420352:i=271062:add=off:rtra=on:rawr=on_2881 on theBenchmark for (2881ds/271062Mi) % 131.17/18.82 % (1474711)Instruction limit reached! % 131.17/18.82 % (1474711)------------------------------ % 131.17/18.82 % (1474711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.17/18.82 % (1474711)CaDiCaL version: 2.1.3 % 131.17/18.82 % (1474711)Termination reason: Instruction limit % 131.17/18.82 % (1474711)Termination phase: Clausification % 131.17/18.82 % (1474711)Time elapsed: 7.246 s % 131.17/18.82 % (1474711)Peak memory usage: 5655 MB % 131.17/18.82 % (1474711)Instructions burned: 15852 (million) % 131.17/18.82 % (1474736)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2539714630:i=176048:add=on:rtra=on:rawr=on_2861 on theBenchmark for (2861ds/176048Mi) % 131.17/18.82 % (1474713)Instruction limit reached! % 131.17/18.82 % (1474713)------------------------------ % 131.17/18.82 % (1474713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.17/18.82 % (1474713)CaDiCaL version: 2.1.3 % 131.17/18.82 % (1474713)Termination reason: Instruction limit % 131.17/18.82 % (1474713)Termination phase: Saturation % 131.17/18.82 % (1474713)Time elapsed: 6.199 s % 131.17/18.82 % (1474713)Peak memory usage: 17 MB % 131.17/18.82 % (1474713)Instructions burned: 17630 (million) % 131.17/18.82 % (1474799)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4245322626:i=206:fgj=on:rtra=on_2846 on theBenchmark for (2846ds/206Mi) % 131.17/18.82 % (1474799)Instruction limit reached! % 131.17/18.82 % (1474799)------------------------------ % 131.17/18.82 % (1474799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.17/18.82 % (1474799)CaDiCaL version: 2.1.3 % 131.17/18.82 % (1474799)Termination reason: Instruction limit % 131.17/18.82 % (1474799)Termination phase: Saturation % 131.17/18.82 % (1474799)Time elapsed: 0.089 s % 131.17/18.82 % (1474799)Peak memory usage: 12 MB % 131.17/18.82 % (1474799)Instructions burned: 207 (million) % 131.17/18.82 % (1474801)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2646314833:i=232:rtra=on_2845 on theBenchmark for (2845ds/232Mi) % 131.17/18.82 % (1474801)Instruction limit reached! % 131.17/18.82 % (1474801)------------------------------ % 131.17/18.82 % (1474801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.17/18.82 % (1474801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474801)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474801)Termination reason: Instruction limit % 137.33/19.63 % (1474801)Termination phase: Saturation % 137.33/19.63 % (1474801)Time elapsed: 0.097 s % 137.33/19.63 % (1474801)Peak memory usage: 12 MB % 137.33/19.63 % (1474801)Instructions burned: 234 (million) % 137.33/19.63 % (1474803)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1723636763:i=262:rtra=on_2844 on theBenchmark for (2844ds/262Mi) % 137.33/19.63 % (1474803)Instruction limit reached! % 137.33/19.63 % (1474803)------------------------------ % 137.33/19.63 % (1474803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.33/19.63 % (1474803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474803)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474803)Termination reason: Instruction limit % 137.33/19.63 % (1474803)Termination phase: Saturation % 137.33/19.63 % (1474803)Time elapsed: 0.109 s % 137.33/19.63 % (1474803)Peak memory usage: 12 MB % 137.33/19.63 % (1474803)Instructions burned: 262 (million) % 137.33/19.63 % (1474805)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1147703519:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2842 on theBenchmark for (2842ds/318Mi) % 137.33/19.63 % (1474805)Instruction limit reached! % 137.33/19.63 % (1474805)------------------------------ % 137.33/19.63 % (1474805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.33/19.63 % (1474805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474805)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474805)Termination reason: Instruction limit % 137.33/19.63 % (1474805)Termination phase: Saturation % 137.33/19.63 % (1474805)Time elapsed: 0.132 s % 137.33/19.63 % (1474805)Peak memory usage: 12 MB % 137.33/19.63 % (1474805)Instructions burned: 319 (million) % 137.33/19.63 % (1474807)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2507458235:i=1428:nm=2:rtra=on_2841 on theBenchmark for (2841ds/1428Mi) % 137.33/19.63 % Detected minimum model sizes of [1] % 137.33/19.63 % Detected maximum model sizes of [14] % 137.33/19.63 % TRYING [1] % 137.33/19.63 % TRYING [2] % 137.33/19.63 % Finite Model Found! % 137.33/19.63 % SZS status CounterSatisfiable for theBenchmark % 137.33/19.63 % (1474807)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 137.33/19.63 % (1474807)------------------------------ % 137.33/19.63 % (1474807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.33/19.63 % (1474807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474807)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474807)Termination reason: Unknown % 137.33/19.63 % (1474807)Termination phase: Finite model building constraint generation % 137.33/19.63 % (1474807)Time elapsed: 0.002 s % 137.33/19.63 % (1474807)Peak memory usage: 11 MB % 137.33/19.63 % (1474807)Instructions burned: 3 (million) % 137.33/19.63 % (1474809)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3789112746:i=262:bd=preordered:rtra=on:fsd=on_2841 on theBenchmark for (2841ds/262Mi) % 137.33/19.63 % (1474809)Instruction limit reached! % 137.33/19.63 % (1474809)------------------------------ % 137.33/19.63 % (1474809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.33/19.63 % (1474809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474809)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474809)Termination reason: Instruction limit % 137.33/19.63 % (1474809)Termination phase: Saturation % 137.33/19.63 % (1474809)Time elapsed: 0.110 s % 137.33/19.63 % (1474809)Peak memory usage: 12 MB % 137.33/19.63 % (1474809)Instructions burned: 264 (million) % 137.33/19.63 % (1474811)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=2108971987:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/1368Mi) % 137.33/19.63 % (1474811)Instruction limit reached! % 137.33/19.63 % (1474811)------------------------------ % 137.33/19.63 % (1474811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.33/19.63 % (1474811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.33/19.63 % (1474811)CaDiCaL version: 2.1.3 % 137.33/19.63 % (1474811)Termination reason: Instruction limit % 137.33/19.63 % (1474811)Termination phase: Saturation % 137.33/19.63 % (1474811)Time elapsed: 0.530 s % 137.33/19.63 % (1474811)Peak memory usage: 13 MB % 137.33/19.63 % (1474811)Instructions burned: 1368 (million) % 137.33/19.63 % (1474813)ott-21_1_sil=16000:si=on:fs=off:random_seed=3648738852:i=360:av=off:fsr=off:rtra=on_2834 on theBenchmark for (2834ds/360Mi) % 167.20/23.85 % (1474813)Instruction limit reached! % 167.20/23.85 % (1474813)------------------------------ % 167.20/23.85 % (1474813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.85 % (1474813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.85 % (1474813)CaDiCaL version: 2.1.3 % 167.20/23.85 % (1474813)Termination reason: Instruction limit % 167.20/23.85 % (1474813)Termination phase: Saturation % 167.20/23.85 % (1474813)Time elapsed: 0.163 s % 167.20/23.85 % (1474813)Peak memory usage: 14 MB % 167.20/23.85 % (1474813)Instructions burned: 361 (million) % 167.20/23.85 % (1474815)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3644061015:i=954:bd=all:rtra=on_2832 on theBenchmark for (2832ds/954Mi) % 167.20/23.85 % (1474815)Instruction limit reached! % 167.20/23.85 % (1474815)------------------------------ % 167.20/23.85 % (1474815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.85 % (1474815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.85 % (1474815)CaDiCaL version: 2.1.3 % 167.20/23.85 % (1474815)Termination reason: Instruction limit % 167.20/23.85 % (1474815)Termination phase: Saturation % 167.20/23.85 % (1474815)Time elapsed: 0.368 s % 167.20/23.85 % (1474815)Peak memory usage: 12 MB % 167.20/23.85 % (1474815)Instructions burned: 956 (million) % 167.20/23.85 % (1474818)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2822839788:fmbsr=1.3:i=1730:ins=25:rtra=on_2828 on theBenchmark for (2828ds/1730Mi) % 167.20/23.85 % Detected minimum model sizes of [1] % 167.20/23.85 % Detected maximum model sizes of [13] % 167.20/23.85 % TRYING [1] % 167.20/23.85 % TRYING [2] % 167.20/23.85 % Finite Model Found! % 167.20/23.85 % SZS status CounterSatisfiable for theBenchmark % 167.20/23.85 % (1474818)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 167.20/23.85 % (1474818)------------------------------ % 167.20/23.85 % (1474818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.85 % (1474818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.85 % (1474818)CaDiCaL version: 2.1.3 % 167.20/23.85 % (1474818)Termination reason: Unknown % 167.20/23.85 % (1474818)Termination phase: Finite model building constraint generation % 167.20/23.85 % (1474818)Time elapsed: 0.002 s % 167.20/23.85 % (1474818)Peak memory usage: 10 MB % 167.20/23.85 % (1474818)Instructions burned: 4 (million) % 167.20/23.85 % (1474820)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4203771930:i=2358:rtra=on_2828 on theBenchmark for (2828ds/2358Mi) % 167.20/23.85 % (1474820)Instruction limit reached! % 167.20/23.85 % (1474820)------------------------------ % 167.20/23.85 % (1474820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.85 % (1474820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.85 % (1474820)CaDiCaL version: 2.1.3 % 167.20/23.85 % (1474820)Termination reason: Instruction limit % 167.20/23.85 % (1474820)Termination phase: Saturation % 167.20/23.85 % (1474820)Time elapsed: 0.846 s % 167.20/23.85 % (1474820)Peak memory usage: 12 MB % 167.20/23.85 % (1474820)Instructions burned: 2358 (million) % 167.20/23.85 % (1474822)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3144466308:i=1778:ins=1:rtra=on_2819 on theBenchmark for (2819ds/1778Mi) % 167.20/23.85 % Detected minimum model sizes of [1] % 167.20/23.85 % Detected maximum model sizes of [13] % 167.20/23.85 % fmb_start_size (= 14) larger than a detected sort maximum size! % 167.20/23.85 % (1474822)Refutation not found, incomplete strategy % 167.20/23.85 % (1474822)------------------------------ % 167.20/23.85 % (1474822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.85 % (1474822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.85 % (1474822)CaDiCaL version: 2.1.3 % 167.20/23.85 % (1474822)Termination reason: Refutation not found, incomplete strategy % 167.20/23.85 % (1474822)Time elapsed: 0.002 s % 167.20/23.85 % (1474822)Peak memory usage: 10 MB % 167.20/23.85 % (1474822)Instructions burned: 3 (million) % 167.20/23.85 % (1474822)------------------------------ % 167.20/23.85 % (1474822)------------------------------ % 167.20/23.85 % (1474824)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=3150995090:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/1384Mi) % 167.20/23.85 % (1474824)Instruction limit reached! % 167.20/23.85 % (1474824)------------------------------ % 167.10/27.75 % (1474824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.10/27.75 % (1474824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.10/27.75 % (1474824)CaDiCaL version: 2.1.3 % 167.10/27.75 % (1474824)Termination reason: Instruction limit % 167.10/27.75 % (1474824)Termination phase: Saturation % 167.10/27.75 % (1474824)Time elapsed: 0.518 s % 167.10/27.75 % (1474824)Peak memory usage: 13 MB % 167.10/27.75 % (1474824)Instructions burned: 1384 (million) % 167.10/27.75 % (1474826)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2375417511:i=1758:kws=inv_precedence:fsr=off:rtra=on_2814 on theBenchmark for (2814ds/1758Mi) % 167.10/27.75 % (1474826)Instruction limit reached! % 167.10/27.75 % (1474826)------------------------------ % 167.10/27.75 % (1474826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.10/27.75 % (1474826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.10/27.75 % (1474826)CaDiCaL version: 2.1.3 % 167.10/27.75 % (1474826)Termination reason: Instruction limit % 167.10/27.75 % (1474826)Termination phase: Saturation % 167.10/27.75 % (1474826)Time elapsed: 0.633 s % 167.10/27.75 % (1474826)Peak memory usage: 13 MB % 167.10/27.75 % (1474826)Instructions burned: 1759 (million) % 167.10/27.75 % (1475000)fmb+10_1_sil=64000:si=on:random_seed=1281071744:i=44122:nm=2:rtra=on:gsp=on_2807 on theBenchmark for (2807ds/44122Mi) % 167.10/27.75 % Detected minimum model sizes of [1] % 167.10/27.75 % Detected maximum model sizes of [13] % 167.10/27.75 % TRYING [1] % 167.10/27.75 % TRYING [2] % 167.10/27.75 % Finite Model Found! % 167.10/27.75 % SZS status CounterSatisfiable for theBenchmark % 167.10/27.75 % (1475000)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 167.10/27.75 % (1475000)------------------------------ % 167.10/27.75 % (1475000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.10/27.75 % (1475000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.10/27.75 % (1475000)CaDiCaL version: 2.1.3 % 167.10/27.75 % (1475000)Termination reason: Unknown % 167.10/27.75 % (1475000)Termination phase: Finite model building constraint generation % 167.10/27.75 % (1475000)Time elapsed: 0.003 s % 167.10/27.75 % (1475000)Peak memory usage: 10 MB % 167.10/27.75 % (1475000)Instructions burned: 5 (million) % 167.10/27.75 % (1475007)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1536272422:i=19030:nm=5:rtra=on_2807 on theBenchmark for (2807ds/19030Mi) % 167.10/27.75 % Detected minimum model sizes of [1] % 167.10/27.75 % Detected maximum model sizes of [13] % 167.10/27.75 % fmb_start_size (= 20) larger than a detected sort maximum size! % 167.10/27.75 % (1475007)Refutation not found, incomplete strategy % 167.10/27.75 % (1475007)------------------------------ % 167.10/27.75 % (1475007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.10/27.75 % (1475007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.10/27.75 % (1475007)CaDiCaL version: 2.1.3 % 167.10/27.75 % (1475007)Termination reason: Refutation not found, incomplete strategy % 167.10/27.75 % (1475007)Time elapsed: 0.001 s % 167.10/27.75 % (1475007)Peak memory usage: 10 MB % 167.10/27.75 % (1475007)Instructions burned: 2 (million) % 167.10/27.75 % (1475007)------------------------------ % 167.10/27.75 % (1475007)------------------------------ % 167.10/27.75 % (1475014)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1819603043:fmbsr=1.7:i=1840:rtra=on_2807 on theBenchmark for (2807ds/1840Mi) % 167.10/27.75 % Detected minimum model sizes of [1] % 167.10/27.75 % Detected maximum model sizes of [13] % 167.10/27.75 % TRYING [8] % 167.10/27.75 % Finite Model Found! % 167.10/27.75 % SZS status CounterSatisfiable for theBenchmark % 167.10/27.75 % (1475014)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 167.10/27.75 % (1475014)------------------------------ % 167.10/27.75 % (1475014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.10/27.75 % (1475014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.10/27.75 % (1475014)CaDiCaL version: 2.1.3 % 167.10/27.75 % (1475014)Termination reason: Unknown % 167.10/27.75 % (1475014)Termination phase: Finite model building constraint generation % 167.10/27.75 % (1475014)Time elapsed: 0.002 s % 167.10/27.75 % (1475014)Peak memory usage: 11 MB % 167.10/27.75 % (1475014)Instructions burned: 3 (million) % 167.10/27.75 % (1475021)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=77680921:i=10262:rtra=on_2806 on theBenchmark for (2806ds/10262Mi) % 167.10/27.75 % (1474719)Instruction limit reached! % 167.10/27.75 % (1474719)------------------------------ % 167.10/27.75 % (1474719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1474719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1474719)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1474719)Termination reason: Instruction limit % 200.74/28.66 % (1474719)Termination phase: Saturation % 200.74/28.66 % (1474719)Time elapsed: 9.052 s % 200.74/28.66 % (1474719)Peak memory usage: 13 MB % 200.74/28.66 % (1474719)Instructions burned: 28121 (million) % 200.74/28.66 % (1475053)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1470004332:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2805 on theBenchmark for (2805ds/2944Mi) % 200.74/28.66 % (1475053)Instruction limit reached! % 200.74/28.66 % (1475053)------------------------------ % 200.74/28.66 % (1475053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1475053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1475053)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1475053)Termination reason: Instruction limit % 200.74/28.66 % (1475053)Termination phase: Saturation % 200.74/28.66 % (1475053)Time elapsed: 1.053 s % 200.74/28.66 % (1475053)Peak memory usage: 13 MB % 200.74/28.66 % (1475053)Instructions burned: 2945 (million) % 200.74/28.66 % (1475207)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=393611503:i=12648:rtra=on_2795 on theBenchmark for (2795ds/12648Mi) % 200.74/28.66 % Detected minimum model sizes of [1] % 200.74/28.66 % Detected maximum model sizes of [13] % 200.74/28.66 % fmb_start_size (= 77) larger than a detected sort maximum size! % 200.74/28.66 % (1475207)Refutation not found, incomplete strategy % 200.74/28.66 % (1475207)------------------------------ % 200.74/28.66 % (1475207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1475207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1475207)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1475207)Termination reason: Refutation not found, incomplete strategy % 200.74/28.66 % (1475207)Time elapsed: 0.002 s % 200.74/28.66 % (1475207)Peak memory usage: 10 MB % 200.74/28.66 % (1475207)Instructions burned: 3 (million) % 200.74/28.66 % (1475207)------------------------------ % 200.74/28.66 % (1475207)------------------------------ % 200.74/28.66 % (1475209)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2960558135:fmbsr=2.30978:i=4348:rtra=on_2794 on theBenchmark for (2794ds/4348Mi) % 200.74/28.66 % Detected minimum model sizes of [1] % 200.74/28.66 % Detected maximum model sizes of [26] % 200.74/28.66 % TRYING [16] % 200.74/28.66 % Finite Model Found! % 200.74/28.66 % SZS status CounterSatisfiable for theBenchmark % 200.74/28.66 % (1475209)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 200.74/28.66 % (1475209)------------------------------ % 200.74/28.66 % (1475209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1475209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1475209)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1475209)Termination reason: Unknown % 200.74/28.66 % (1475209)Termination phase: Finite model building constraint generation % 200.74/28.66 % (1475209)Time elapsed: 0.018 s % 200.74/28.66 % (1475209)Peak memory usage: 13 MB % 200.74/28.66 % (1475209)Instructions burned: 42 (million) % 200.74/28.66 % (1475211)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4014555820:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2794 on theBenchmark for (2794ds/1738Mi) % 200.74/28.66 % (1475211)Instruction limit reached! % 200.74/28.66 % (1475211)------------------------------ % 200.74/28.66 % (1475211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1475211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1475211)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1475211)Termination reason: Instruction limit % 200.74/28.66 % (1475211)Termination phase: Saturation % 200.74/28.66 % (1475211)Time elapsed: 0.651 s % 200.74/28.66 % (1475211)Peak memory usage: 12 MB % 200.74/28.66 % (1475211)Instructions burned: 1738 (million) % 200.74/28.66 % (1475213)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2088099496:i=10228:av=off:rtra=on_2787 on theBenchmark for (2787ds/10228Mi) % 200.74/28.66 % (1475021)Instruction limit reached! % 200.74/28.66 % (1475021)------------------------------ % 200.74/28.66 % (1475021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.74/28.66 % (1475021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.74/28.66 % (1475021)CaDiCaL version: 2.1.3 % 200.74/28.66 % (1475021)Termination reason: Instruction limit % 270.08/38.32 % (1475021)Termination phase: Saturation % 270.08/38.32 % (1475021)Time elapsed: 4.293 s % 270.08/38.32 % (1475021)Peak memory usage: 21 MB % 270.08/38.32 % (1475021)Instructions burned: 10262 (million) % 270.08/38.32 % (1475215)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1045242692:i=108564:rtra=on_2763 on theBenchmark for (2763ds/108564Mi) % 270.08/38.32 % Detected minimum model sizes of [1] % 270.08/38.32 % Detected maximum model sizes of [13] % 270.08/38.32 % TRYING [1] % 270.08/38.32 % TRYING [2] % 270.08/38.32 % Finite Model Found! % 270.08/38.32 % SZS status CounterSatisfiable for theBenchmark % 270.08/38.32 % (1475215)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 270.08/38.32 % (1475215)------------------------------ % 270.08/38.32 % (1475215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.08/38.32 % (1475215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.08/38.32 % (1475215)CaDiCaL version: 2.1.3 % 270.08/38.32 % (1475215)Termination reason: Unknown % 270.08/38.32 % (1475215)Termination phase: Finite model building constraint generation % 270.08/38.32 % (1475215)Time elapsed: 0.003 s % 270.08/38.32 % (1475215)Peak memory usage: 11 MB % 270.08/38.32 % (1475215)Instructions burned: 4 (million) % 270.08/38.32 % (1475217)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2398154836:i=7024:aac=none:rtra=on_2763 on theBenchmark for (2763ds/7024Mi) % 270.08/38.32 % (1475213)Instruction limit reached! % 270.08/38.32 % (1475213)------------------------------ % 270.08/38.32 % (1475213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.08/38.32 % (1475213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.08/38.32 % (1475213)CaDiCaL version: 2.1.3 % 270.08/38.32 % (1475213)Termination reason: Instruction limit % 270.08/38.32 % (1475213)Termination phase: Saturation % 270.08/38.32 % (1475213)Time elapsed: 4.132 s % 270.08/38.32 % (1475213)Peak memory usage: 12 MB % 270.08/38.32 % (1475213)Instructions burned: 10229 (million) % 270.08/38.32 % (1475219)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1309486319:i=7546:rtra=on:amm=off_2746 on theBenchmark for (2746ds/7546Mi) % 270.08/38.32 % (1475217)Instruction limit reached! % 270.08/38.32 % (1475217)------------------------------ % 270.08/38.32 % (1475217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.08/38.32 % (1475217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.08/38.32 % (1475217)CaDiCaL version: 2.1.3 % 270.08/38.32 % (1475217)Termination reason: Instruction limit % 270.08/38.32 % (1475217)Termination phase: Saturation % 270.08/38.32 % (1475217)Time elapsed: 2.641 s % 270.08/38.32 % (1475217)Peak memory usage: 14 MB % 270.08/38.32 % (1475217)Instructions burned: 7025 (million) % 270.08/38.32 % (1475221)ott+11_1_sil=16000:si=on:gs=on:random_seed=3634837615:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2736 on theBenchmark for (2736ds/4502Mi) % 270.08/38.32 % (1474473)Instruction limit reached! % 270.08/38.32 % (1474473)------------------------------ % 270.08/38.32 % (1474473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.08/38.32 % (1474473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.08/38.32 % (1474473)CaDiCaL version: 2.1.3 % 270.08/38.32 % (1474473)Termination reason: Instruction limit % 270.08/38.32 % (1474473)Termination phase: Saturation % 270.08/38.32 % (1474473)Time elapsed: 27.433 s % 270.08/38.32 % (1474473)Peak memory usage: 23 MB % 270.08/38.32 % (1474473)Instructions burned: 88026 (million) % 270.08/38.32 % (1475223)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1908795013:fmbsr=1.6:i=135068:rtra=on_2725 on theBenchmark for (2725ds/135068Mi) % 270.08/38.32 % Detected minimum model sizes of [1] % 270.08/38.32 % Detected maximum model sizes of [14] % 270.08/38.32 % TRYING [7] % 270.08/38.32 % Finite Model Found! % 270.08/38.32 % SZS status CounterSatisfiable for theBenchmark % 270.08/38.32 % (1475223)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 270.08/38.32 % (1475223)------------------------------ % 270.08/38.32 % (1475223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.08/38.32 % (1475223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.08/38.32 % (1475223)CaDiCaL version: 2.1.3 % 270.08/38.32 % (1475223)Termination reason: Unknown % 270.08/38.32 % (1475223)Termination phase: Finite model building constraint generation % 270.08/38.32 % (1475223)Time elapsed: 0.009 s % 270.08/38.32 % (1475223)Peak memory usage: 11 MB % 270.08/38.32 % (1475223)Instructions burned: 18 (million) % 270.08/38.32 % (1475225)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2603077711:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2725 on theBenchmark for (2725ds/9182Mi) % 300.59/42.63 % (1474715)Instruction limit reached! % 300.59/42.63 % (1474715)------------------------------ % 300.59/42.63 % (1474715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (1474715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (1474715)CaDiCaL version: 2.1.3 % 300.59/42.63 % (1474715)Termination reason: Instruction limit % 300.59/42.63 % (1474715)Termination phase: Saturation % 300.59/42.63 % (1474715)Time elapsed: 17.360 s % 300.59/42.63 % (1474715)Peak memory usage: 15 MB % 300.59/42.63 % (1474715)Instructions burned: 53297 (million) % 300.59/42.63 % (1475227)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=1596960621:i=58680:rtra=on_2723 on theBenchmark for (2723ds/58680Mi) % 300.59/42.63 % (1475221)Instruction limit reached! % 300.59/42.63 % (1475221)------------------------------ % 300.59/42.63 % (1475221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (1475221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (1475221)CaDiCaL version: 2.1.3 % 300.59/42.63 % (1475221)Termination reason: Instruction limit % 300.59/42.63 % (1475221)Termination phase: Saturation % 300.59/42.63 % (1475221)Time elapsed: 1.535 s % 300.59/42.63 % (1475221)Peak memory usage: 12 MB % 300.59/42.63 % (1475221)Instructions burned: 4503 (million) % 300.59/42.63 % (1475229)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=784872104:i=10422:rtra=on_2721 on theBenchmark for (2721ds/10422Mi) % 300.59/42.63 % (1475219)Instruction limit reached! % 300.59/42.63 % (1475219)------------------------------ % 300.59/42.63 % (1475219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (1475219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (1475219)CaDiCaL version: 2.1.3 % 300.59/42.63 % (1475219)Termination reason: Instruction limit % 300.59/42.63 % (1475219)Termination phase: Saturation % 300.59/42.63 % (1475219)Time elapsed: 2.988 s % 300.59/42.63 % (1475219)Peak memory usage: 19 MB % 300.59/42.63 % (1475219)Instructions burned: 7547 (million) % 300.59/42.63 % (1475231)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=1823103463:i=10994:nm=2:rtra=on_2716 on theBenchmark for (2716ds/10994Mi) % 300.59/42.63 % Detected minimum model sizes of [1] % 300.59/42.63 % Detected maximum model sizes of [13] % 300.59/42.63 % fmb_start_size (= 17) larger than a detected sort maximum size! % 300.59/42.63 % (1475231)Refutation not found, incomplete strategy % 300.59/42.63 % (1475231)------------------------------ % 300.59/42.63 % (1475231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (1475231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (1475231)CaDiCaL version: 2.1.3 % 300.59/42.63 % (1475231)Termination reason: Refutation not found, incomplete strategy % 300.59/42.63 % (1475231)Time elapsed: 0.002 s % 300.59/42.63 % (1475231)Peak memory usage: 10 MB % 300.59/42.63 % (1475231)Instructions burned: 3 (million) % 300.59/42.63 % (1475231)------------------------------ % 300.59/42.63 % (1475231)------------------------------ % 300.59/42.63 % (1475233)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=3294104829:fmbsr=2:i=92664:rtra=on_2716 on theBenchmark for (2716ds/92664Mi) % 300.59/42.63 % Detected minimum model sizes of [1] % 300.59/42.63 % Detected maximum model sizes of [14] % 300.59/42.63 % fmb_start_size (= 15) larger than a detected sort maximum size! % 300.59/42.63 % (1475233)Refutation not found, incomplete strategy % 300.59/42.63 % (1475233)------------------------------ % 300.59/42.63 % (1475233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.63 % (1475233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.63 % (1475233)CaDiCaL version: 2.1.3 % 300.59/42.63 % (1475233)Termination reason: Refutation not found, incomplete strategy % 300.59/42.63 % (1475233)Time elapsed: 0.001 s % 300.59/42.63 % (1475233)Peak memory usage: 10 MB % 300.59/42.63 % (1475233)Instructions burned: 2 (million) % 300.59/42.63 % (1475233)------------------------------ % 300.59/42.63 % (1475233)------------------------------ % 300.59/42.63 % (1475235)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=3410525700:i=28142:rtra=on_2715 on theBenchmark for (2715ds/28142Mi) % 300.59/42.63 % Detected minimum model sizes of [1] % 300.59/42.63 % Detected maximum model sizes of [13] % 300.59/42.63 % TRYING [12] % 300.59/42.63 % Finite Model Found! % 300.59/42.63 % SZS status CounterSatisfiable for th % 300.59/42.64 Terminated % 300.59/42.64 % Vampire exiting % 300.59/42.64 Terminated %------------------------------------------------------------------------------