%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : PUZ152_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n014.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 : Tue Sep 29 12:32:36 PM UTC 2026 % Result : Satisfiable 1.71s 0.74s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : PUZ152_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.37 % Computer : n014.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 27 22:46:16 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.40 Running first-order model finding % 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/0.74 % (1244828)Will run a generic schedule for satisfiability detection. % 1.71/0.74 % (1244838)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1383109195:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.71/0.74 % (1244834)% WARNING: option uhcvi not known. % 1.71/0.74 % (1244834)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=720367348:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.71/0.74 % (1244833)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1498888456_2999 on theBenchmark for (2999ds/0Mi) % 1.71/0.74 % (1244835)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1037234692:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.71/0.74 % (1244836)dis+10_1_sil=32000:sp=arity:random_seed=310519249:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.71/0.74 % (1244837)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2265677726:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.71/0.74 % (1244839)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2355318063:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.71/0.74 % Detected minimum model sizes of [1,1] % 1.71/0.74 % Detected maximum model sizes of [6,5] % 1.71/0.74 % TRYING [1,1] % 1.71/0.74 % TRYING [1,2] % 1.71/0.74 % TRYING [2,2] % 1.71/0.74 % Finite Model Found! % 1.71/0.74 % SZS status Satisfiable for theBenchmark % 1.71/0.74 % (1244833)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/0.74 % (1244833)------------------------------ % 1.71/0.74 % (1244833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.74 % (1244833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.74 % (1244833)CaDiCaL version: 2.1.3 % 1.71/0.74 % (1244833)Termination reason: Unknown % 1.71/0.74 % (1244833)Termination phase: Finite model building constraint generation % 1.71/0.74 % (1244833)Time elapsed: 0.003 s % 1.71/0.74 % (1244833)Peak memory usage: 11 MB % 1.71/0.74 % (1244833)Instructions burned: 3 (million) % 1.71/0.74 % (1244847)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3455465869:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.71/0.74 % (1244838)Instruction limit reached! % 1.71/0.74 % (1244838)------------------------------ % 1.71/0.74 % (1244838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.74 % (1244838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.74 % (1244838)CaDiCaL version: 2.1.3 % 1.71/0.74 % (1244838)Termination reason: Instruction limit % 1.71/0.74 % (1244838)Termination phase: Saturation % 1.71/0.74 % (1244838)Time elapsed: 0.031 s % 1.71/0.74 % (1244838)Peak memory usage: 11 MB % 1.71/0.74 % (1244838)Instructions burned: 133 (million) % 1.71/0.74 % Detected minimum model sizes of [1] % 1.71/0.74 % Detected maximum model sizes of [13] % 1.71/0.74 % TRYING [1] % 1.71/0.74 % TRYING [2] % 1.71/0.74 % Finite Model Found! % 1.71/0.74 % SZS status Satisfiable for theBenchmark % 1.71/0.74 % (1244847)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/0.74 % (1244847)------------------------------ % 1.71/0.74 % (1244847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.74 % (1244847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.74 % (1244847)CaDiCaL version: 2.1.3 % 1.71/0.74 % (1244847)Termination reason: Unknown % 1.71/0.74 % (1244847)Termination phase: Finite model building constraint generation % 1.71/0.74 % (1244847)Time elapsed: 0.002 s % 1.71/0.74 % (1244847)Peak memory usage: 11 MB % 1.71/0.74 % (1244847)Instructions burned: 2 (million) % 1.71/0.74 % (1244849)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3649695464:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 1.71/0.74 % (1244850)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=3978687787:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 1.71/0.74 % (1244836)Instruction limit reached! % 1.71/0.74 % (1244836)------------------------------ % 1.71/0.74 % (1244836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.71/0.74 % (1244836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.71/0.74 % (1244836)CaDiCaL version: 2.1.3 % 1.71/0.74 % (1244836)Termination reason: Instruction limit % 1.71/0.74 % (1244836)Termination phase: Saturation % 1.71/0.74 % (1244836)Time elapsed: 0.049 s % 2.71/1.01 % (1244836)Peak memory usage: 11 MB % 2.71/1.01 % (1244836)Instructions burned: 105 (million) % 2.71/1.01 % (1244837)Instruction limit reached! % 2.71/1.01 % (1244837)------------------------------ % 2.71/1.01 % (1244837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.71/1.01 % (1244837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.71/1.01 % (1244837)CaDiCaL version: 2.1.3 % 2.71/1.01 % (1244837)Termination reason: Instruction limit % 2.71/1.01 % (1244837)Termination phase: Saturation % 2.71/1.01 % (1244837)Time elapsed: 0.050 s % 2.71/1.01 % (1244837)Peak memory usage: 11 MB % 2.71/1.01 % (1244837)Instructions burned: 116 (million) % 2.71/1.01 % (1244853)ott-21_1_sil=16000:fs=off:random_seed=945201112:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 2.71/1.01 % (1244849)Instruction limit reached! % 2.71/1.01 % (1244849)------------------------------ % 2.71/1.01 % (1244849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.71/1.01 % (1244849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.71/1.01 % (1244849)CaDiCaL version: 2.1.3 % 2.71/1.01 % (1244849)Termination reason: Instruction limit % 2.71/1.01 % (1244849)Termination phase: Saturation % 2.71/1.01 % (1244849)Time elapsed: 0.033 s % 2.71/1.01 % (1244849)Peak memory usage: 12 MB % 2.71/1.01 % (1244849)Instructions burned: 134 (million) % 2.71/1.01 % (1244854)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4214611082:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 2.71/1.01 % (1244839)Instruction limit reached! % 2.71/1.01 % (1244839)------------------------------ % 2.71/1.01 % (1244839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.71/1.01 % (1244839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.71/1.01 % (1244839)CaDiCaL version: 2.1.3 % 2.71/1.01 % (1244839)Termination reason: Instruction limit % 2.71/1.01 % (1244839)Termination phase: Saturation % 2.71/1.01 % (1244839)Time elapsed: 0.073 s % 2.71/1.01 % (1244839)Peak memory usage: 12 MB % 2.71/1.01 % (1244839)Instructions burned: 159 (million) % 2.71/1.01 % (1244857)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=105452837:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 2.71/1.01 % Detected minimum model sizes of [1,1] % 2.71/1.01 % Detected maximum model sizes of [6,5] % 2.71/1.01 % TRYING [1,1] % 2.71/1.01 % TRYING [1,2] % 2.71/1.01 % TRYING [2,2] % 2.71/1.01 % Finite Model Found! % 2.71/1.01 % SZS status Satisfiable for theBenchmark % 2.71/1.01 % (1244857)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.71/1.01 % (1244857)------------------------------ % 2.71/1.01 % (1244857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.71/1.01 % (1244857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.71/1.01 % (1244857)CaDiCaL version: 2.1.3 % 2.71/1.01 % (1244857)Termination reason: Unknown % 2.71/1.01 % (1244857)Termination phase: Finite model building constraint generation % 2.71/1.01 % (1244857)Time elapsed: 0.001 s % 2.71/1.01 % (1244857)Peak memory usage: 10 MB % 2.71/1.01 % (1244857)Instructions burned: 3 (million) % 2.71/1.01 % (1244860)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1974819803:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 2.71/1.01 % Detected minimum model sizes of [1,1] % 2.71/1.01 % Detected maximum model sizes of [6,5] % 2.71/1.01 % fmb_start_size (= 14) larger than a detected sort maximum size! % 2.71/1.01 % (1244860)Refutation not found, incomplete strategy % 2.71/1.01 % (1244860)------------------------------ % 2.71/1.01 % (1244860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.71/1.01 % (1244860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.71/1.01 % (1244860)CaDiCaL version: 2.1.3 % 2.71/1.01 % (1244860)Termination reason: Refutation not found, incomplete strategy % 2.71/1.01 % (1244860)Time elapsed: 0.0000 s % 2.71/1.01 % (1244860)Peak memory usage: 11 MB % 2.71/1.01 % (1244860)Instructions burned: 1 (million) % 2.71/1.01 % (1244860)------------------------------ % 2.71/1.01 % (1244860)------------------------------ % 2.71/1.01 % (1244858)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4278145168:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 2.71/1.01 % (1244862)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=3451222456: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) % 11.39/2.13 % (1244853)Instruction limit reached! % 11.39/2.13 % (1244853)------------------------------ % 11.39/2.13 % (1244853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244853)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244853)Termination reason: Instruction limit % 11.39/2.13 % (1244853)Termination phase: Saturation % 11.39/2.13 % (1244853)Time elapsed: 0.084 s % 11.39/2.13 % (1244853)Peak memory usage: 13 MB % 11.39/2.13 % (1244853)Instructions burned: 182 (million) % 11.39/2.13 % (1244865)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3002595335:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.39/2.13 % (1244862)Instruction limit reached! % 11.39/2.13 % (1244862)------------------------------ % 11.39/2.13 % (1244862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244862)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244862)Termination reason: Instruction limit % 11.39/2.13 % (1244862)Termination phase: Saturation % 11.39/2.13 % (1244862)Time elapsed: 0.149 s % 11.39/2.13 % (1244862)Peak memory usage: 13 MB % 11.39/2.13 % (1244862)Instructions burned: 692 (million) % 11.39/2.13 % (1244867)fmb+10_1_sil=64000:random_seed=2764477437:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.39/2.13 % Detected minimum model sizes of [1,1] % 11.39/2.13 % Detected maximum model sizes of [6,5] % 11.39/2.13 % TRYING [1,1] % 11.39/2.13 % TRYING [1,2] % 11.39/2.13 % TRYING [2,2] % 11.39/2.13 % Finite Model Found! % 11.39/2.13 % SZS status Satisfiable for theBenchmark % 11.39/2.13 % (1244867)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.39/2.13 % (1244867)------------------------------ % 11.39/2.13 % (1244867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244867)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244867)Termination reason: Unknown % 11.39/2.13 % (1244867)Termination phase: Finite model building constraint generation % 11.39/2.13 % (1244867)Time elapsed: 0.001 s % 11.39/2.13 % (1244867)Peak memory usage: 10 MB % 11.39/2.13 % (1244867)Instructions burned: 3 (million) % 11.39/2.13 % (1244869)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3126340660:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 11.39/2.13 % Detected minimum model sizes of [1,1] % 11.39/2.13 % Detected maximum model sizes of [6,5] % 11.39/2.13 % fmb_start_size (= 20) larger than a detected sort maximum size! % 11.39/2.13 % (1244869)Refutation not found, incomplete strategy % 11.39/2.13 % (1244869)------------------------------ % 11.39/2.13 % (1244869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244869)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244869)Termination reason: Refutation not found, incomplete strategy % 11.39/2.13 % (1244869)Time elapsed: 0.0000 s % 11.39/2.13 % (1244869)Peak memory usage: 10 MB % 11.39/2.13 % (1244869)Instructions burned: 1 (million) % 11.39/2.13 % (1244869)------------------------------ % 11.39/2.13 % (1244869)------------------------------ % 11.39/2.13 % (1244854)Instruction limit reached! % 11.39/2.13 % (1244854)------------------------------ % 11.39/2.13 % (1244854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244854)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244854)Termination reason: Instruction limit % 11.39/2.13 % (1244854)Termination phase: Saturation % 11.39/2.13 % (1244854)Time elapsed: 0.215 s % 11.39/2.13 % (1244854)Peak memory usage: 12 MB % 11.39/2.13 % (1244854)Instructions burned: 478 (million) % 11.39/2.13 % (1244871)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3121760678:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 11.39/2.13 % Detected minimum model sizes of [1,1] % 11.39/2.13 % Detected maximum model sizes of [6,5] % 11.39/2.13 % fmb_start_size (= 8) larger than a detected sort maximum size! % 11.39/2.13 % (1244871)Refutation not found, incomplete strategy % 11.39/2.13 % (1244871)------------------------------ % 11.39/2.13 % (1244871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.39/2.13 % (1244871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.39/2.13 % (1244871)CaDiCaL version: 2.1.3 % 11.39/2.13 % (1244871)Termination reason: Refutation not found, incomplete strategy % 14.69/2.75 % (1244871)Time elapsed: 0.0000 s % 14.69/2.75 % (1244871)Peak memory usage: 10 MB % 14.69/2.75 % (1244871)Instructions burned: 1 (million) % 14.69/2.75 % (1244871)------------------------------ % 14.69/2.75 % (1244871)------------------------------ % 14.69/2.75 % (1244874)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1235794014:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 14.69/2.75 % (1244873)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3440551061:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 14.69/2.75 % (1244850)Instruction limit reached! % 14.69/2.75 % (1244850)------------------------------ % 14.69/2.75 % (1244850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.69/2.75 % (1244850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.69/2.75 % (1244850)CaDiCaL version: 2.1.3 % 14.69/2.75 % (1244850)Termination reason: Instruction limit % 14.69/2.75 % (1244850)Termination phase: Saturation % 14.69/2.75 % (1244850)Time elapsed: 0.280 s % 14.69/2.75 % (1244850)Peak memory usage: 13 MB % 14.69/2.75 % (1244850)Instructions burned: 686 (million) % 14.69/2.75 % (1244877)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3431022842:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 14.69/2.75 % Detected minimum model sizes of [1,1] % 14.69/2.75 % Detected maximum model sizes of [6,5] % 14.69/2.75 % fmb_start_size (= 77) larger than a detected sort maximum size! % 14.69/2.75 % (1244877)Refutation not found, incomplete strategy % 14.69/2.75 % (1244877)------------------------------ % 14.69/2.75 % (1244877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.69/2.75 % (1244877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.69/2.75 % (1244877)CaDiCaL version: 2.1.3 % 14.69/2.75 % (1244877)Termination reason: Refutation not found, incomplete strategy % 14.69/2.75 % (1244877)Time elapsed: 0.001 s % 14.69/2.75 % (1244877)Peak memory usage: 10 MB % 14.69/2.75 % (1244877)Instructions burned: 1 (million) % 14.69/2.75 % (1244877)------------------------------ % 14.69/2.75 % (1244877)------------------------------ % 14.69/2.75 % (1244879)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4260051175:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 14.69/2.75 % Detected minimum model sizes of [1] % 14.69/2.75 % Detected maximum model sizes of [22] % 14.69/2.75 % TRYING [16] % 14.69/2.75 % Finite Model Found! % 14.69/2.75 % SZS status Satisfiable for theBenchmark % 14.69/2.75 % (1244879)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.69/2.75 % (1244879)------------------------------ % 14.69/2.75 % (1244879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.69/2.75 % (1244879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.69/2.75 % (1244879)CaDiCaL version: 2.1.3 % 14.69/2.75 % (1244879)Termination reason: Unknown % 14.69/2.75 % (1244879)Termination phase: Finite model building constraint generation % 14.69/2.75 % (1244879)Time elapsed: 0.016 s % 14.69/2.75 % (1244879)Peak memory usage: 12 MB % 14.69/2.75 % (1244879)Instructions burned: 40 (million) % 14.69/2.75 % (1244881)ott-2_1_sil=16000:newcnf=on:random_seed=1979185531:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 14.69/2.75 % (1244865)Instruction limit reached! % 14.69/2.75 % (1244865)------------------------------ % 14.69/2.75 % (1244865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.69/2.75 % (1244865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.69/2.75 % (1244865)CaDiCaL version: 2.1.3 % 14.69/2.75 % (1244865)Termination reason: Instruction limit % 14.69/2.75 % (1244865)Termination phase: Saturation % 14.69/2.75 % (1244865)Time elapsed: 0.337 s % 14.69/2.75 % (1244865)Peak memory usage: 13 MB % 14.69/2.75 % (1244865)Instructions burned: 882 (million) % 14.69/2.75 % (1244883)ott+10_1_sil=32000:tgt=ground:random_seed=1398779056:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 14.69/2.75 % (1244858)Instruction limit reached! % 14.69/2.75 % (1244858)------------------------------ % 14.69/2.75 % (1244858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.69/2.75 % (1244858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.69/2.75 % (1244858)CaDiCaL version: 2.1.3 % 14.69/2.75 % (1244858)Termination reason: Instruction limit % 14.69/2.75 % (1244858)Termination phase: Saturation % 14.69/2.75 % (1244858)Time elapsed: 0.459 s % 43.81/6.61 % (1244858)Peak memory usage: 12 MB % 43.81/6.61 % (1244858)Instructions burned: 1180 (million) % 43.81/6.61 % (1244885)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2453610124:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 43.81/6.61 % Detected minimum model sizes of [1,1] % 43.81/6.61 % Detected maximum model sizes of [6,5] % 43.81/6.61 % TRYING [1,1] % 43.81/6.61 % TRYING [1,2] % 43.81/6.61 % TRYING [2,2] % 43.81/6.61 % Finite Model Found! % 43.81/6.61 % SZS status Satisfiable for theBenchmark % 43.81/6.61 % (1244885)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.81/6.61 % (1244885)------------------------------ % 43.81/6.61 % (1244885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.81/6.61 % (1244885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.81/6.61 % (1244885)CaDiCaL version: 2.1.3 % 43.81/6.61 % (1244885)Termination reason: Unknown % 43.81/6.61 % (1244885)Termination phase: Finite model building constraint generation % 43.81/6.61 % (1244885)Time elapsed: 0.002 s % 43.81/6.61 % (1244885)Peak memory usage: 12 MB % 43.81/6.61 % (1244885)Instructions burned: 3 (million) % 43.81/6.61 % (1244887)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3734225848:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 43.81/6.61 % (1244874)Instruction limit reached! % 43.81/6.61 % (1244874)------------------------------ % 43.81/6.61 % (1244874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.81/6.61 % (1244874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.81/6.61 % (1244874)CaDiCaL version: 2.1.3 % 43.81/6.61 % (1244874)Termination reason: Instruction limit % 43.81/6.61 % (1244874)Termination phase: Saturation % 43.81/6.61 % (1244874)Time elapsed: 0.333 s % 43.81/6.61 % (1244874)Peak memory usage: 13 MB % 43.81/6.61 % (1244874)Instructions burned: 1474 (million) % 43.81/6.61 % (1244889)dis+21_1_sil=32000:sas=cadical:random_seed=3024967901:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 43.81/6.61 % (1244881)Instruction limit reached! % 43.81/6.61 % (1244881)------------------------------ % 43.81/6.61 % (1244881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.81/6.61 % (1244881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.81/6.61 % (1244881)CaDiCaL version: 2.1.3 % 43.81/6.61 % (1244881)Termination reason: Instruction limit % 43.81/6.61 % (1244881)Termination phase: Saturation % 43.81/6.61 % (1244881)Time elapsed: 0.344 s % 43.81/6.61 % (1244881)Peak memory usage: 12 MB % 43.81/6.61 % (1244881)Instructions burned: 870 (million) % 43.81/6.61 % (1244891)ott+11_1_sil=16000:gs=on:random_seed=791095939:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 43.81/6.61 % (1244889)Instruction limit reached! % 43.81/6.61 % (1244889)------------------------------ % 43.81/6.61 % (1244889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.81/6.61 % (1244889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.81/6.61 % (1244889)CaDiCaL version: 2.1.3 % 43.81/6.61 % (1244889)Termination reason: Instruction limit % 43.81/6.61 % (1244889)Termination phase: Saturation % 43.81/6.61 % (1244889)Time elapsed: 0.926 s % 43.81/6.61 % (1244889)Peak memory usage: 24 MB % 43.81/6.61 % (1244889)Instructions burned: 3776 (million) % 43.81/6.61 % (1244893)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3022377775:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 43.81/6.61 % Detected minimum model sizes of [1] % 43.81/6.61 % Detected maximum model sizes of [13] % 43.81/6.61 % TRYING [7] % 43.81/6.61 % Finite Model Found! % 43.81/6.61 % SZS status Satisfiable for theBenchmark % 43.81/6.61 % (1244893)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.81/6.61 % (1244893)------------------------------ % 43.81/6.61 % (1244893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.81/6.61 % (1244893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.81/6.61 % (1244893)CaDiCaL version: 2.1.3 % 43.81/6.61 % (1244893)Termination reason: Unknown % 43.81/6.61 % (1244893)Termination phase: Finite model building constraint generation % 43.81/6.61 % (1244893)Time elapsed: 0.002 s % 43.81/6.61 % (1244893)Peak memory usage: 11 MB % 43.81/6.61 % (1244893)Instructions burned: 6 (million) % 43.81/6.61 % (1244895)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3067419054:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 43.81/6.61 % (1244891)Instruction limit reached! % 79.80/11.71 % (1244891)------------------------------ % 79.80/11.71 % (1244891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.80/11.71 % (1244891)CaDiCaL version: 2.1.3 % 79.80/11.71 % (1244891)Termination reason: Instruction limit % 79.80/11.71 % (1244891)Termination phase: Saturation % 79.80/11.71 % (1244891)Time elapsed: 0.912 s % 79.80/11.71 % (1244891)Peak memory usage: 13 MB % 79.80/11.71 % (1244891)Instructions burned: 2253 (million) % 79.80/11.71 % (1244897)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3234591570:i=29340_2982 on theBenchmark for (2982ds/29340Mi) % 79.80/11.71 % (1244887)Instruction limit reached! % 79.80/11.71 % (1244887)------------------------------ % 79.80/11.71 % (1244887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.80/11.71 % (1244887)CaDiCaL version: 2.1.3 % 79.80/11.71 % (1244887)Termination reason: Instruction limit % 79.80/11.71 % (1244887)Termination phase: Saturation % 79.80/11.71 % (1244887)Time elapsed: 1.426 s % 79.80/11.71 % (1244887)Peak memory usage: 16 MB % 79.80/11.71 % (1244887)Instructions burned: 3513 (million) % 79.80/11.71 % (1244899)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3777485948:i=5211_2979 on theBenchmark for (2979ds/5211Mi) % 79.80/11.71 % (1244873)Instruction limit reached! % 79.80/11.71 % (1244873)------------------------------ % 79.80/11.71 % (1244873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.80/11.71 % (1244873)CaDiCaL version: 2.1.3 % 79.80/11.71 % (1244873)Termination reason: Instruction limit % 79.80/11.71 % (1244873)Termination phase: Saturation % 79.80/11.71 % (1244873)Time elapsed: 1.932 s % 79.80/11.71 % (1244873)Peak memory usage: 15 MB % 79.80/11.71 % (1244873)Instructions burned: 5132 (million) % 79.80/11.71 % (1244901)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2370413027:i=5497:nm=2_2977 on theBenchmark for (2977ds/5497Mi) % 79.80/11.71 % Detected minimum model sizes of [1,1] % 79.80/11.71 % Detected maximum model sizes of [6,5] % 79.80/11.71 % fmb_start_size (= 17) larger than a detected sort maximum size! % 79.80/11.71 % (1244901)Refutation not found, incomplete strategy % 79.80/11.71 % (1244901)------------------------------ % 79.80/11.71 % (1244901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.80/11.71 % (1244901)CaDiCaL version: 2.1.3 % 79.80/11.71 % (1244901)Termination reason: Refutation not found, incomplete strategy % 79.80/11.71 % (1244901)Time elapsed: 0.001 s % 79.80/11.71 % (1244901)Peak memory usage: 10 MB % 79.80/11.71 % (1244901)Instructions burned: 1 (million) % 79.80/11.71 % (1244901)------------------------------ % 79.80/11.71 % (1244901)------------------------------ % 79.80/11.71 % (1244903)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2309002207:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 79.80/11.71 % Detected minimum model sizes of [1] % 79.80/11.71 % Detected maximum model sizes of [13] % 79.80/11.71 % fmb_start_size (= 15) larger than a detected sort maximum size! % 79.80/11.71 % (1244903)Refutation not found, incomplete strategy % 79.80/11.71 % (1244903)------------------------------ % 79.80/11.71 % (1244903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.80/11.71 % (1244903)CaDiCaL version: 2.1.3 % 79.80/11.71 % (1244903)Termination reason: Refutation not found, incomplete strategy % 79.80/11.71 % (1244903)Time elapsed: 0.001 s % 79.80/11.71 % (1244903)Peak memory usage: 10 MB % 79.80/11.71 % (1244903)Instructions burned: 1 (million) % 79.80/11.71 % (1244903)------------------------------ % 79.80/11.71 % (1244903)------------------------------ % 79.80/11.71 % (1244905)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1115846266:i=14071_2976 on theBenchmark for (2976ds/14071Mi) % 79.80/11.71 % Detected minimum model sizes of [1,1] % 79.80/11.71 % Detected maximum model sizes of [6,5] % 79.80/11.71 % fmb_start_size (= 12) larger than a detected sort maximum size! % 79.80/11.71 % (1244905)Refutation not found, incomplete strategy % 79.80/11.71 % (1244905)------------------------------ % 79.80/11.71 % (1244905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.80/11.71 % (1244905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244905)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244905)Termination reason: Refutation not found, incomplete strategy % 80.32/11.81 % (1244905)Time elapsed: 0.001 s % 80.32/11.81 % (1244905)Peak memory usage: 10 MB % 80.32/11.81 % (1244905)Instructions burned: 1 (million) % 80.32/11.81 % (1244905)------------------------------ % 80.32/11.81 % (1244905)------------------------------ % 80.32/11.81 % (1244907)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=699260150:i=22565:add=on:rawr=on_2976 on theBenchmark for (2976ds/22565Mi) % 80.32/11.81 % (1244895)Instruction limit reached! % 80.32/11.81 % (1244895)------------------------------ % 80.32/11.81 % (1244895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.32/11.81 % (1244895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244895)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244895)Termination reason: Instruction limit % 80.32/11.81 % (1244895)Termination phase: Saturation % 80.32/11.81 % (1244895)Time elapsed: 0.957 s % 80.32/11.81 % (1244895)Peak memory usage: 14 MB % 80.32/11.81 % (1244895)Instructions burned: 4596 (million) % 80.32/11.81 % (1244909)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2987643848:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 80.32/11.81 % (1244883)Instruction limit reached! % 80.32/11.81 % (1244883)------------------------------ % 80.32/11.81 % (1244883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.32/11.81 % (1244883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244883)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244883)Termination reason: Instruction limit % 80.32/11.81 % (1244883)Termination phase: Saturation % 80.32/11.81 % (1244883)Time elapsed: 2.318 s % 80.32/11.81 % (1244883)Peak memory usage: 13 MB % 80.32/11.81 % (1244883)Instructions burned: 5115 (million) % 80.32/11.81 % (1244911)dis+10_16:1_sil=16000:random_seed=2126271624:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 80.32/11.81 % (1244899)Instruction limit reached! % 80.32/11.81 % (1244899)------------------------------ % 80.32/11.81 % (1244899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.32/11.81 % (1244899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244899)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244899)Termination reason: Instruction limit % 80.32/11.81 % (1244899)Termination phase: Saturation % 80.32/11.81 % (1244899)Time elapsed: 2.029 s % 80.32/11.81 % (1244899)Peak memory usage: 16 MB % 80.32/11.81 % (1244899)Instructions burned: 5213 (million) % 80.32/11.81 % (1244913)ott-3_8_sil=64000:random_seed=686405829:i=20139:bs=on_2958 on theBenchmark for (2958ds/20139Mi) % 80.32/11.81 % (1244909)Instruction limit reached! % 80.32/11.81 % (1244909)------------------------------ % 80.32/11.81 % (1244909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.32/11.81 % (1244909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244909)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244909)Termination reason: Instruction limit % 80.32/11.81 % (1244909)Termination phase: Saturation % 80.32/11.81 % (1244909)Time elapsed: 1.873 s % 80.32/11.81 % (1244909)Peak memory usage: 14 MB % 80.32/11.81 % (1244909)Instructions burned: 8176 (million) % 80.32/11.81 % (1244915)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3844852655:fmbsr=2:i=32576_2955 on theBenchmark for (2955ds/32576Mi) % 80.32/11.81 % Detected minimum model sizes of [1,1] % 80.32/11.81 % Detected maximum model sizes of [6,5] % 80.32/11.81 % fmb_start_size (= 9) larger than a detected sort maximum size! % 80.32/11.81 % (1244915)Refutation not found, incomplete strategy % 80.32/11.81 % (1244915)------------------------------ % 80.32/11.81 % (1244915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.32/11.81 % (1244915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.32/11.81 % (1244915)CaDiCaL version: 2.1.3 % 80.32/11.81 % (1244915)Termination reason: Refutation not found, incomplete strategy % 80.32/11.81 % (1244915)Time elapsed: 0.0000 s % 80.32/11.81 % (1244915)Peak memory usage: 10 MB % 80.32/11.81 % (1244915)Instructions burned: 1 (million) % 80.32/11.81 % (1244915)------------------------------ % 80.32/11.81 % (1244915)------------------------------ % 80.32/11.81 % (1244917)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=432089150:i=11404_2955 on theBenchmark for (2955ds/11404Mi) % 80.32/11.81 % (1244911)Instruction limit reached! % 80.32/11.81 % (1244911)------------------------------ % 80.32/11.81 % (1244911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244911)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244911)Termination reason: Instruction limit % 97.72/14.25 % (1244911)Termination phase: Saturation % 97.72/14.25 % (1244911)Time elapsed: 3.285 s % 97.72/14.25 % (1244911)Peak memory usage: 16 MB % 97.72/14.25 % (1244911)Instructions burned: 9157 (million) % 97.72/14.25 % (1244919)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2209768016:i=14134_2938 on theBenchmark for (2938ds/14134Mi) % 97.72/14.25 % (1244917)Instruction limit reached! % 97.72/14.25 % (1244917)------------------------------ % 97.72/14.25 % (1244917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244917)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244917)Termination reason: Instruction limit % 97.72/14.25 % (1244917)Termination phase: Saturation % 97.72/14.25 % (1244917)Time elapsed: 2.232 s % 97.72/14.25 % (1244917)Peak memory usage: 15 MB % 97.72/14.25 % (1244917)Instructions burned: 11406 (million) % 97.72/14.25 % (1244921)dis+33_16_sil=32000:sac=on:random_seed=2288588414:i=15851:nm=0_2932 on theBenchmark for (2932ds/15851Mi) % 97.72/14.25 % (1244921)Instruction limit reached! % 97.72/14.25 % (1244921)------------------------------ % 97.72/14.25 % (1244921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244921)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244921)Termination reason: Instruction limit % 97.72/14.25 % (1244921)Termination phase: Saturation % 97.72/14.25 % (1244921)Time elapsed: 3.220 s % 97.72/14.25 % (1244921)Peak memory usage: 18 MB % 97.72/14.25 % (1244921)Instructions burned: 15853 (million) % 97.72/14.25 % (1244923)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3376740025:avsq=on:i=17627:add=on:amm=off_2900 on theBenchmark for (2900ds/17627Mi) % 97.72/14.25 % (1244919)Instruction limit reached! % 97.72/14.25 % (1244919)------------------------------ % 97.72/14.25 % (1244919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244919)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244919)Termination reason: Instruction limit % 97.72/14.25 % (1244919)Termination phase: Saturation % 97.72/14.25 % (1244919)Time elapsed: 4.866 s % 97.72/14.25 % (1244919)Peak memory usage: 14 MB % 97.72/14.25 % (1244919)Instructions burned: 14135 (million) % 97.72/14.25 % (1244925)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=207100929:s2a=on:i=53295_2889 on theBenchmark for (2889ds/53295Mi) % 97.72/14.25 % (1244913)Instruction limit reached! % 97.72/14.25 % (1244913)------------------------------ % 97.72/14.25 % (1244913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244913)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244913)Termination reason: Instruction limit % 97.72/14.25 % (1244913)Termination phase: Saturation % 97.72/14.25 % (1244913)Time elapsed: 7.123 s % 97.72/14.25 % (1244913)Peak memory usage: 16 MB % 97.72/14.25 % (1244913)Instructions burned: 20141 (million) % 97.72/14.25 % (1244927)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1043815845:i=26857:ins=20_2887 on theBenchmark for (2887ds/26857Mi) % 97.72/14.25 % Detected minimum model sizes of [1,1] % 97.72/14.25 % Detected maximum model sizes of [6,5] % 97.72/14.25 % fmb_start_size (= 16) larger than a detected sort maximum size! % 97.72/14.25 % (1244927)Refutation not found, incomplete strategy % 97.72/14.25 % (1244927)------------------------------ % 97.72/14.25 % (1244927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.72/14.25 % (1244927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.72/14.25 % (1244927)CaDiCaL version: 2.1.3 % 97.72/14.25 % (1244927)Termination reason: Refutation not found, incomplete strategy % 97.72/14.25 % (1244927)Time elapsed: 0.001 s % 97.72/14.25 % (1244927)Peak memory usage: 10 MB % 97.72/14.25 % (1244927)Instructions burned: 1 (million) % 97.72/14.25 % (1244927)------------------------------ % 97.72/14.25 % (1244927)------------------------------ % 97.72/14.25 % (1244929)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1583948597:i=28120:bs=on:fsr=off_2887 on theBenchmark for (2887ds/28120Mi) % 97.72/14.25 % (1244907)Instruction limit reached! % 101.70/14.83 % (1244907)------------------------------ % 101.70/14.83 % (1244907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.70/14.83 % (1244907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.70/14.83 % (1244907)CaDiCaL version: 2.1.3 % 101.70/14.83 % (1244907)Termination reason: Instruction limit % 101.70/14.83 % (1244907)Termination phase: Saturation % 101.70/14.83 % (1244907)Time elapsed: 8.935 s % 101.70/14.83 % (1244907)Peak memory usage: 24 MB % 101.70/14.83 % (1244907)Instructions burned: 22566 (million) % 101.70/14.83 % (1244931)fmb+10_1_sil=256000:fmbss=7:random_seed=138885818:fmbsr=1.6:i=182295_2887 on theBenchmark for (2887ds/182295Mi) % 101.70/14.83 % Detected minimum model sizes of [1,1] % 101.70/14.83 % Detected maximum model sizes of [6,5] % 101.70/14.83 % fmb_start_size (= 7) larger than a detected sort maximum size! % 101.70/14.83 % (1244931)Refutation not found, incomplete strategy % 101.70/14.83 % (1244931)------------------------------ % 101.70/14.83 % (1244931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.70/14.83 % (1244931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.70/14.83 % (1244931)CaDiCaL version: 2.1.3 % 101.70/14.83 % (1244931)Termination reason: Refutation not found, incomplete strategy % 101.70/14.83 % (1244931)Time elapsed: 0.001 s % 101.70/14.83 % (1244931)Peak memory usage: 10 MB % 101.70/14.83 % (1244931)Instructions burned: 1 (million) % 101.70/14.83 % (1244931)------------------------------ % 101.70/14.83 % (1244931)------------------------------ % 101.70/14.83 % (1244933)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2841916388:i=44625:gsp=on_2886 on theBenchmark for (2886ds/44625Mi) % 101.70/14.83 % Detected minimum model sizes of [1,1] % 101.70/14.83 % Detected maximum model sizes of [6,2] % 101.70/14.83 % fmb_start_size (= 21) larger than a detected sort maximum size! % 101.70/14.83 % (1244933)Refutation not found, incomplete strategy % 101.70/14.83 % (1244933)------------------------------ % 101.70/14.83 % (1244933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.70/14.83 % (1244933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.70/14.83 % (1244933)CaDiCaL version: 2.1.3 % 101.70/14.83 % (1244933)Termination reason: Refutation not found, incomplete strategy % 101.70/14.83 % (1244933)Time elapsed: 0.001 s % 101.70/14.84 % (1244933)Peak memory usage: 10 MB % 101.70/14.84 % (1244933)Instructions burned: 1 (million) % 101.70/14.84 % (1244933)------------------------------ % 101.70/14.84 % (1244933)------------------------------ % 101.70/14.84 % (1244935)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2432589809:i=160505_2886 on theBenchmark for (2886ds/160505Mi) % 101.70/14.84 % Detected minimum model sizes of [1,1] % 101.70/14.84 % Detected maximum model sizes of [6,5] % 101.70/14.84 % fmb_start_size (= 15) larger than a detected sort maximum size! % 101.70/14.84 % (1244935)Refutation not found, incomplete strategy % 101.70/14.84 % (1244935)------------------------------ % 101.70/14.84 % (1244935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.70/14.84 % (1244935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.70/14.84 % (1244935)CaDiCaL version: 2.1.3 % 101.70/14.84 % (1244935)Termination reason: Refutation not found, incomplete strategy % 101.70/14.84 % (1244935)Time elapsed: 0.001 s % 101.70/14.84 % (1244935)Peak memory usage: 10 MB % 101.70/14.84 % (1244935)Instructions burned: 1 (million) % 101.70/14.84 % (1244935)------------------------------ % 101.70/14.84 % (1244935)------------------------------ % 101.70/14.84 % (1244937)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3878671035:fmbsr=1.3:i=225729_2886 on theBenchmark for (2886ds/225729Mi) % 101.70/14.84 % Detected minimum model sizes of [1,1] % 101.70/14.84 % Detected maximum model sizes of [6,5] % 101.70/14.84 % fmb_start_size (= 10) larger than a detected sort maximum size! % 101.70/14.84 % (1244937)Refutation not found, incomplete strategy % 101.70/14.84 % (1244937)------------------------------ % 101.70/14.84 % (1244937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.70/14.84 % (1244937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.70/14.84 % (1244937)CaDiCaL version: 2.1.3 % 101.70/14.84 % (1244937)Termination reason: Refutation not found, incomplete strategy % 101.70/14.84 % (1244937)Time elapsed: 0.001 s % 101.70/14.84 % (1244937)Peak memory usage: 10 MB % 101.70/14.84 % (1244937)Instructions burned: 1 (million) % 101.70/14.84 % (1244937)------------------------------ % 101.70/14.84 % (1244937)------------------------------ % 101.70/14.84 % (1244939)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=821285734:fmbsr=2:i=185024:ins=7_2886 on theBenchmark for (2886ds/185024Mi) % 109.61/16.01 % Detected minimum model sizes of [1,1] % 109.61/16.01 % Detected maximum model sizes of [6,5] % 109.61/16.01 % fmb_start_size (= 10) larger than a detected sort maximum size! % 109.61/16.01 % (1244939)Refutation not found, incomplete strategy % 109.61/16.01 % (1244939)------------------------------ % 109.61/16.01 % (1244939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.61/16.01 % (1244939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.61/16.01 % (1244939)CaDiCaL version: 2.1.3 % 109.61/16.01 % (1244939)Termination reason: Refutation not found, incomplete strategy % 109.61/16.01 % (1244939)Time elapsed: 0.001 s % 109.61/16.01 % (1244939)Peak memory usage: 10 MB % 109.61/16.01 % (1244939)Instructions burned: 1 (million) % 109.61/16.01 % (1244939)------------------------------ % 109.61/16.01 % (1244939)------------------------------ % 109.61/16.01 % (1244941)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2467547506:rtra=on_2885 on theBenchmark for (2885ds/0Mi) % 109.61/16.01 % Detected minimum model sizes of [1,1] % 109.61/16.01 % Detected maximum model sizes of [6,5] % 109.61/16.01 % TRYING [1,1] % 109.61/16.01 % TRYING [1,2] % 109.61/16.01 % TRYING [2,2] % 109.61/16.01 % Finite Model Found! % 109.61/16.01 % SZS status Satisfiable for theBenchmark % 109.61/16.01 % (1244941)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.61/16.01 % (1244941)------------------------------ % 109.61/16.01 % (1244941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.61/16.01 % (1244941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.61/16.01 % (1244941)CaDiCaL version: 2.1.3 % 109.61/16.01 % (1244941)Termination reason: Unknown % 109.61/16.01 % (1244941)Termination phase: Finite model building constraint generation % 109.61/16.01 % (1244941)Time elapsed: 0.002 s % 109.61/16.01 % (1244941)Peak memory usage: 11 MB % 109.61/16.01 % (1244941)Instructions burned: 3 (million) % 109.61/16.01 % (1244943)% WARNING: option uhcvi not known. % 109.61/16.01 % (1244943)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3444867735:i=271062:add=off:rtra=on:rawr=on_2885 on theBenchmark for (2885ds/271062Mi) % 109.61/16.01 % (1244897)Instruction limit reached! % 109.61/16.01 % (1244897)------------------------------ % 109.61/16.01 % (1244897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.61/16.01 % (1244897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.61/16.01 % (1244897)CaDiCaL version: 2.1.3 % 109.61/16.01 % (1244897)Termination reason: Instruction limit % 109.61/16.01 % (1244897)Termination phase: Saturation % 109.61/16.01 % (1244897)Time elapsed: 10.844 s % 109.61/16.01 % (1244897)Peak memory usage: 26 MB % 109.61/16.01 % (1244897)Instructions burned: 29341 (million) % 109.61/16.01 % (1244945)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4188750973:i=176048:add=on:rtra=on:rawr=on_2874 on theBenchmark for (2874ds/176048Mi) % 109.61/16.01 % (1244923)Instruction limit reached! % 109.61/16.01 % (1244923)------------------------------ % 109.61/16.01 % (1244923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.61/16.01 % (1244923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.61/16.01 % (1244923)CaDiCaL version: 2.1.3 % 109.61/16.01 % (1244923)Termination reason: Instruction limit % 109.61/16.01 % (1244923)Termination phase: Saturation % 109.61/16.01 % (1244923)Time elapsed: 3.723 s % 109.61/16.01 % (1244923)Peak memory usage: 21 MB % 109.61/16.01 % (1244923)Instructions burned: 17630 (million) % 109.61/16.01 % (1244947)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3314642133:i=206:fgj=on:rtra=on_2862 on theBenchmark for (2862ds/206Mi) % 109.61/16.01 % (1244947)Instruction limit reached! % 109.61/16.01 % (1244947)------------------------------ % 109.61/16.01 % (1244947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.61/16.01 % (1244947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.61/16.01 % (1244947)CaDiCaL version: 2.1.3 % 109.61/16.01 % (1244947)Termination reason: Instruction limit % 109.61/16.01 % (1244947)Termination phase: Saturation % 109.61/16.01 % (1244947)Time elapsed: 0.056 s % 109.61/16.01 % (1244947)Peak memory usage: 12 MB % 109.61/16.01 % (1244947)Instructions burned: 209 (million) % 109.61/16.01 % (1244949)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3734498851:i=232:rtra=on_2862 on theBenchmark for (2862ds/232Mi) % 109.61/16.01 % (1244949)Instruction limit reached! % 109.61/16.01 % (1244949)------------------------------ % 109.61/16.01 % (1244949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244949)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244949)Termination reason: Instruction limit % 127.57/18.49 % (1244949)Termination phase: Saturation % 127.57/18.49 % (1244949)Time elapsed: 0.059 s % 127.57/18.49 % (1244949)Peak memory usage: 12 MB % 127.57/18.49 % (1244949)Instructions burned: 234 (million) % 127.57/18.49 % (1244951)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=265585866:i=262:rtra=on_2861 on theBenchmark for (2861ds/262Mi) % 127.57/18.49 % (1244951)Instruction limit reached! % 127.57/18.49 % (1244951)------------------------------ % 127.57/18.49 % (1244951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244951)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244951)Termination reason: Instruction limit % 127.57/18.49 % (1244951)Termination phase: Saturation % 127.57/18.49 % (1244951)Time elapsed: 0.063 s % 127.57/18.49 % (1244951)Peak memory usage: 12 MB % 127.57/18.49 % (1244951)Instructions burned: 265 (million) % 127.57/18.49 % (1244953)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2354850290:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2860 on theBenchmark for (2860ds/318Mi) % 127.57/18.49 % (1244953)Instruction limit reached! % 127.57/18.49 % (1244953)------------------------------ % 127.57/18.49 % (1244953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244953)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244953)Termination reason: Instruction limit % 127.57/18.49 % (1244953)Termination phase: Saturation % 127.57/18.49 % (1244953)Time elapsed: 0.083 s % 127.57/18.49 % (1244953)Peak memory usage: 12 MB % 127.57/18.49 % (1244953)Instructions burned: 320 (million) % 127.57/18.49 % (1244955)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3339900211:i=1428:nm=2:rtra=on_2859 on theBenchmark for (2859ds/1428Mi) % 127.57/18.49 % Detected minimum model sizes of [1] % 127.57/18.49 % Detected maximum model sizes of [13] % 127.57/18.49 % TRYING [1] % 127.57/18.49 % TRYING [2] % 127.57/18.49 % Finite Model Found! % 127.57/18.49 % SZS status Satisfiable for theBenchmark % 127.57/18.49 % (1244955)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 127.57/18.49 % (1244955)------------------------------ % 127.57/18.49 % (1244955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244955)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244955)Termination reason: Unknown % 127.57/18.49 % (1244955)Termination phase: Finite model building constraint generation % 127.57/18.49 % (1244955)Time elapsed: 0.001 s % 127.57/18.49 % (1244955)Peak memory usage: 11 MB % 127.57/18.49 % (1244955)Instructions burned: 2 (million) % 127.57/18.49 % (1244957)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4223434614:i=262:bd=preordered:rtra=on:fsd=on_2859 on theBenchmark for (2859ds/262Mi) % 127.57/18.49 % (1244957)Instruction limit reached! % 127.57/18.49 % (1244957)------------------------------ % 127.57/18.49 % (1244957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244957)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244957)Termination reason: Instruction limit % 127.57/18.49 % (1244957)Termination phase: Saturation % 127.57/18.49 % (1244957)Time elapsed: 0.063 s % 127.57/18.49 % (1244957)Peak memory usage: 12 MB % 127.57/18.49 % (1244957)Instructions burned: 265 (million) % 127.57/18.49 % (1244959)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=2617690989:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/1368Mi) % 127.57/18.49 % (1244959)Instruction limit reached! % 127.57/18.49 % (1244959)------------------------------ % 127.57/18.49 % (1244959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.49 % (1244959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.49 % (1244959)CaDiCaL version: 2.1.3 % 127.57/18.49 % (1244959)Termination reason: Instruction limit % 127.57/18.49 % (1244959)Termination phase: Saturation % 127.57/18.49 % (1244959)Time elapsed: 0.311 s % 127.57/18.49 % (1244959)Peak memory usage: 14 MB % 127.57/18.49 % (1244959)Instructions burned: 1372 (million) % 127.57/18.49 % (1244961)ott-21_1_sil=16000:si=on:fs=off:random_seed=270887442:i=360:av=off:fsr=off:rtra=on_2855 on theBenchmark for (2855ds/360Mi) % 136.01/19.63 % (1244961)Instruction limit reached! % 136.01/19.63 % (1244961)------------------------------ % 136.01/19.63 % (1244961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.63 % (1244961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.63 % (1244961)CaDiCaL version: 2.1.3 % 136.01/19.63 % (1244961)Termination reason: Instruction limit % 136.01/19.63 % (1244961)Termination phase: Saturation % 136.01/19.63 % (1244961)Time elapsed: 0.091 s % 136.01/19.63 % (1244961)Peak memory usage: 14 MB % 136.01/19.63 % (1244961)Instructions burned: 363 (million) % 136.01/19.63 % (1244963)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1319198746:i=954:bd=all:rtra=on_2854 on theBenchmark for (2854ds/954Mi) % 136.01/19.63 % (1244963)Instruction limit reached! % 136.01/19.63 % (1244963)------------------------------ % 136.01/19.63 % (1244963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.63 % (1244963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.63 % (1244963)CaDiCaL version: 2.1.3 % 136.01/19.63 % (1244963)Termination reason: Instruction limit % 136.01/19.63 % (1244963)Termination phase: Saturation % 136.01/19.63 % (1244963)Time elapsed: 0.227 s % 136.01/19.63 % (1244963)Peak memory usage: 13 MB % 136.01/19.63 % (1244963)Instructions burned: 957 (million) % 136.01/19.63 % (1244965)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=431982749:fmbsr=1.3:i=1730:ins=25:rtra=on_2852 on theBenchmark for (2852ds/1730Mi) % 136.01/19.63 % Detected minimum model sizes of [1,1] % 136.01/19.63 % Detected maximum model sizes of [6,5] % 136.01/19.63 % TRYING [1,1] % 136.01/19.63 % TRYING [1,2] % 136.01/19.63 % TRYING [2,2] % 136.01/19.63 % Finite Model Found! % 136.01/19.63 % SZS status Satisfiable for theBenchmark % 136.01/19.63 % (1244965)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 136.01/19.63 % (1244965)------------------------------ % 136.01/19.63 % (1244965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.63 % (1244965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.63 % (1244965)CaDiCaL version: 2.1.3 % 136.01/19.63 % (1244965)Termination reason: Unknown % 136.01/19.63 % (1244965)Termination phase: Finite model building constraint generation % 136.01/19.63 % (1244965)Time elapsed: 0.001 s % 136.01/19.63 % (1244965)Peak memory usage: 10 MB % 136.01/19.63 % (1244965)Instructions burned: 4 (million) % 136.01/19.63 % (1244967)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3755448779:i=2358:rtra=on_2852 on theBenchmark for (2852ds/2358Mi) % 136.01/19.63 % (1244967)Instruction limit reached! % 136.01/19.63 % (1244967)------------------------------ % 136.01/19.63 % (1244967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.63 % (1244967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.63 % (1244967)CaDiCaL version: 2.1.3 % 136.01/19.63 % (1244967)Termination reason: Instruction limit % 136.01/19.63 % (1244967)Termination phase: Saturation % 136.01/19.63 % (1244967)Time elapsed: 0.490 s % 136.01/19.63 % (1244967)Peak memory usage: 12 MB % 136.01/19.63 % (1244967)Instructions burned: 2363 (million) % 136.01/19.63 % (1244969)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2897382426:i=1778:ins=1:rtra=on_2847 on theBenchmark for (2847ds/1778Mi) % 136.01/19.63 % Detected minimum model sizes of [1,1] % 136.01/19.63 % Detected maximum model sizes of [6,5] % 136.01/19.63 % fmb_start_size (= 14) larger than a detected sort maximum size! % 136.01/19.63 % (1244969)Refutation not found, incomplete strategy % 136.01/19.63 % (1244969)------------------------------ % 136.01/19.63 % (1244969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.63 % (1244969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.63 % (1244969)CaDiCaL version: 2.1.3 % 136.01/19.63 % (1244969)Termination reason: Refutation not found, incomplete strategy % 136.01/19.63 % (1244969)Time elapsed: 0.001 s % 136.01/19.63 % (1244969)Peak memory usage: 10 MB % 136.01/19.63 % (1244969)Instructions burned: 1 (million) % 136.01/19.63 % (1244969)------------------------------ % 136.01/19.63 % (1244969)------------------------------ % 136.01/19.63 % (1244971)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=665926481:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/1384Mi) % 136.01/19.63 % (1244971)Instruction limit reached! % 164.44/23.67 % (1244971)------------------------------ % 164.44/23.67 % (1244971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.44/23.67 % (1244971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.44/23.67 % (1244971)CaDiCaL version: 2.1.3 % 164.44/23.67 % (1244971)Termination reason: Instruction limit % 164.44/23.67 % (1244971)Termination phase: Saturation % 164.44/23.67 % (1244971)Time elapsed: 0.308 s % 164.44/23.67 % (1244971)Peak memory usage: 13 MB % 164.44/23.67 % (1244971)Instructions burned: 1389 (million) % 164.44/23.67 % (1244973)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4072417354:i=1758:kws=inv_precedence:fsr=off:rtra=on_2843 on theBenchmark for (2843ds/1758Mi) % 164.44/23.67 % (1244973)Instruction limit reached! % 164.44/23.67 % (1244973)------------------------------ % 164.44/23.67 % (1244973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.44/23.67 % (1244973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.44/23.67 % (1244973)CaDiCaL version: 2.1.3 % 164.44/23.67 % (1244973)Termination reason: Instruction limit % 164.44/23.67 % (1244973)Termination phase: Saturation % 164.44/23.67 % (1244973)Time elapsed: 0.359 s % 164.44/23.67 % (1244973)Peak memory usage: 13 MB % 164.44/23.67 % (1244973)Instructions burned: 1760 (million) % 164.44/23.67 % (1244975)fmb+10_1_sil=64000:si=on:random_seed=16085837:i=44122:nm=2:rtra=on:gsp=on_2840 on theBenchmark for (2840ds/44122Mi) % 164.44/23.67 % Detected minimum model sizes of [1,1] % 164.44/23.67 % Detected maximum model sizes of [6,5] % 164.44/23.67 % TRYING [1,1] % 164.44/23.67 % TRYING [1,2] % 164.44/23.67 % TRYING [2,2] % 164.44/23.67 % Finite Model Found! % 164.44/23.67 % SZS status Satisfiable for theBenchmark % 164.44/23.67 % (1244975)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.44/23.67 % (1244975)------------------------------ % 164.44/23.67 % (1244975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.44/23.67 % (1244975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.44/23.67 % (1244975)CaDiCaL version: 2.1.3 % 164.44/23.67 % (1244975)Termination reason: Unknown % 164.44/23.67 % (1244975)Termination phase: Finite model building constraint generation % 164.44/23.67 % (1244975)Time elapsed: 0.001 s % 164.44/23.67 % (1244975)Peak memory usage: 10 MB % 164.44/23.67 % (1244975)Instructions burned: 3 (million) % 164.44/23.67 % (1244977)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2955540591:i=19030:nm=5:rtra=on_2840 on theBenchmark for (2840ds/19030Mi) % 164.44/23.67 % Detected minimum model sizes of [1,1] % 164.44/23.67 % Detected maximum model sizes of [6,5] % 164.44/23.67 % fmb_start_size (= 20) larger than a detected sort maximum size! % 164.44/23.67 % (1244977)Refutation not found, incomplete strategy % 164.44/23.67 % (1244977)------------------------------ % 164.44/23.67 % (1244977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.44/23.67 % (1244977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.44/23.67 % (1244977)CaDiCaL version: 2.1.3 % 164.44/23.67 % (1244977)Termination reason: Refutation not found, incomplete strategy % 164.44/23.67 % (1244977)Time elapsed: 0.0000 s % 164.44/23.67 % (1244977)Peak memory usage: 10 MB % 164.44/23.67 % (1244977)Instructions burned: 1 (million) % 164.44/23.67 % (1244977)------------------------------ % 164.44/23.67 % (1244977)------------------------------ % 164.44/23.67 % (1244979)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2035099798:fmbsr=1.7:i=1840:rtra=on_2840 on theBenchmark for (2840ds/1840Mi) % 164.44/23.67 % Detected minimum model sizes of [1,1] % 164.44/23.67 % Detected maximum model sizes of [6,5] % 164.44/23.67 % fmb_start_size (= 8) larger than a detected sort maximum size! % 164.44/23.67 % (1244979)Refutation not found, incomplete strategy % 164.44/23.67 % (1244979)------------------------------ % 164.44/23.67 % (1244979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.44/23.67 % (1244979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.44/23.67 % (1244979)CaDiCaL version: 2.1.3 % 164.44/23.67 % (1244979)Termination reason: Refutation not found, incomplete strategy % 164.44/23.67 % (1244979)Time elapsed: 0.0000 s % 164.44/23.67 % (1244979)Peak memory usage: 10 MB % 164.44/23.67 % (1244979)Instructions burned: 1 (million) % 164.44/23.67 % (1244979)------------------------------ % 164.44/23.67 % (1244979)------------------------------ % 164.44/23.67 % (1244981)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2765781652:i=10262:rtra=on_2839 on theBenchmark for (2839ds/10262Mi) % 164.44/23.67 % (1244981)Instruction limit reached! % 164.44/23.67 % (1244981)------------------------------ % 192.84/27.64 % (1244981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244981)CaDiCaL version: 2.1.3 % 192.84/27.64 % (1244981)Termination reason: Instruction limit % 192.84/27.64 % (1244981)Termination phase: Saturation % 192.84/27.64 % (1244981)Time elapsed: 2.060 s % 192.84/27.64 % (1244981)Peak memory usage: 15 MB % 192.84/27.64 % (1244981)Instructions burned: 10268 (million) % 192.84/27.64 % (1244985)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1008687211:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2819 on theBenchmark for (2819ds/2944Mi) % 192.84/27.64 % (1244985)Instruction limit reached! % 192.84/27.64 % (1244985)------------------------------ % 192.84/27.64 % (1244985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244985)CaDiCaL version: 2.1.3 % 192.84/27.64 % (1244985)Termination reason: Instruction limit % 192.84/27.64 % (1244985)Termination phase: Saturation % 192.84/27.64 % (1244985)Time elapsed: 0.645 s % 192.84/27.64 % (1244985)Peak memory usage: 14 MB % 192.84/27.64 % (1244985)Instructions burned: 2946 (million) % 192.84/27.64 % (1244987)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=76800418:i=12648:rtra=on_2812 on theBenchmark for (2812ds/12648Mi) % 192.84/27.64 % Detected minimum model sizes of [1,1] % 192.84/27.64 % Detected maximum model sizes of [6,5] % 192.84/27.64 % fmb_start_size (= 77) larger than a detected sort maximum size! % 192.84/27.64 % (1244987)Refutation not found, incomplete strategy % 192.84/27.64 % (1244987)------------------------------ % 192.84/27.64 % (1244987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244987)CaDiCaL version: 2.1.3 % 192.84/27.64 % (1244987)Termination reason: Refutation not found, incomplete strategy % 192.84/27.64 % (1244987)Time elapsed: 0.001 s % 192.84/27.64 % (1244987)Peak memory usage: 10 MB % 192.84/27.64 % (1244987)Instructions burned: 1 (million) % 192.84/27.64 % (1244987)------------------------------ % 192.84/27.64 % (1244987)------------------------------ % 192.84/27.64 % (1244989)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3004857049:fmbsr=2.30978:i=4348:rtra=on_2812 on theBenchmark for (2812ds/4348Mi) % 192.84/27.64 % Detected minimum model sizes of [1] % 192.84/27.64 % Detected maximum model sizes of [22] % 192.84/27.64 % TRYING [16] % 192.84/27.64 % Finite Model Found! % 192.84/27.64 % SZS status Satisfiable for theBenchmark % 192.84/27.64 % (1244989)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 192.84/27.64 % (1244989)------------------------------ % 192.84/27.64 % (1244989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244989)CaDiCaL version: 2.1.3 % 192.84/27.64 % (1244989)Termination reason: Unknown % 192.84/27.64 % (1244989)Termination phase: Finite model building constraint generation % 192.84/27.64 % (1244989)Time elapsed: 0.008 s % 192.84/27.64 % (1244989)Peak memory usage: 13 MB % 192.84/27.64 % (1244989)Instructions burned: 36 (million) % 192.84/27.64 % (1244992)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3541530350:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2812 on theBenchmark for (2812ds/1738Mi) % 192.84/27.64 % (1244992)Instruction limit reached! % 192.84/27.64 % (1244992)------------------------------ % 192.84/27.64 % (1244992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244992)CaDiCaL version: 2.1.3 % 192.84/27.64 % (1244992)Termination reason: Instruction limit % 192.84/27.64 % (1244992)Termination phase: Saturation % 192.84/27.64 % (1244992)Time elapsed: 0.355 s % 192.84/27.64 % (1244992)Peak memory usage: 12 MB % 192.84/27.64 % (1244992)Instructions burned: 1744 (million) % 192.84/27.64 % (1244994)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1072709515:i=10228:av=off:rtra=on_2808 on theBenchmark for (2808ds/10228Mi) % 192.84/27.64 % (1244929)Instruction limit reached! % 192.84/27.64 % (1244929)------------------------------ % 192.84/27.64 % (1244929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.84/27.64 % (1244929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.84/27.64 % (1244929)CaDiCaL version: 2.1.3 % 290.68/41.47 % (1244929)Termination reason: Instruction limit % 290.68/41.47 % (1244929)Termination phase: Saturation % 290.68/41.47 % (1244929)Time elapsed: 7.919 s % 290.68/41.47 % (1244929)Peak memory usage: 16 MB % 290.68/41.47 % (1244929)Instructions burned: 28123 (million) % 290.68/41.47 % (1244996)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2120779945:i=108564:rtra=on_2807 on theBenchmark for (2807ds/108564Mi) % 290.68/41.47 % Detected minimum model sizes of [1,1] % 290.68/41.47 % Detected maximum model sizes of [6,5] % 290.68/41.47 % TRYING [1,1] % 290.68/41.47 % TRYING [1,2] % 290.68/41.47 % TRYING [2,2] % 290.68/41.47 % Finite Model Found! % 290.68/41.47 % SZS status Satisfiable for theBenchmark % 290.68/41.47 % (1244996)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 290.68/41.47 % (1244996)------------------------------ % 290.68/41.47 % (1244996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.68/41.47 % (1244996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.68/41.47 % (1244996)CaDiCaL version: 2.1.3 % 290.68/41.47 % (1244996)Termination reason: Unknown % 290.68/41.47 % (1244996)Termination phase: Finite model building constraint generation % 290.68/41.47 % (1244996)Time elapsed: 0.002 s % 290.68/41.47 % (1244996)Peak memory usage: 11 MB % 290.68/41.47 % (1244996)Instructions burned: 3 (million) % 290.68/41.47 % (1244998)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2718532671:i=7024:aac=none:rtra=on_2807 on theBenchmark for (2807ds/7024Mi) % 290.68/41.47 % (1244994)Instruction limit reached! % 290.68/41.47 % (1244994)------------------------------ % 290.68/41.47 % (1244994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.68/41.47 % (1244994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.68/41.47 % (1244994)CaDiCaL version: 2.1.3 % 290.68/41.47 % (1244994)Termination reason: Instruction limit % 290.68/41.47 % (1244994)Termination phase: Saturation % 290.68/41.47 % (1244994)Time elapsed: 2.440 s % 290.68/41.47 % (1244994)Peak memory usage: 13 MB % 290.68/41.47 % (1244994)Instructions burned: 10229 (million) % 290.68/41.47 % (1245000)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2770244714:i=7546:rtra=on:amm=off_2784 on theBenchmark for (2784ds/7546Mi) % 290.68/41.47 % (1244998)Instruction limit reached! % 290.68/41.47 % (1244998)------------------------------ % 290.68/41.47 % (1244998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.68/41.48 % (1244998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.68/41.48 % (1244998)CaDiCaL version: 2.1.3 % 290.68/41.48 % (1244998)Termination reason: Instruction limit % 290.68/41.48 % (1244998)Termination phase: Saturation % 290.68/41.48 % (1244998)Time elapsed: 3.004 s % 290.68/41.48 % (1244998)Peak memory usage: 18 MB % 290.68/41.48 % (1244998)Instructions burned: 7024 (million) % 290.68/41.48 % (1245002)ott+11_1_sil=16000:si=on:gs=on:random_seed=3619897578:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2777 on theBenchmark for (2777ds/4502Mi) % 290.68/41.48 % (1245000)Instruction limit reached! % 290.68/41.48 % (1245000)------------------------------ % 290.68/41.48 % (1245000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.68/41.48 % (1245000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.68/41.48 % (1245000)CaDiCaL version: 2.1.3 % 290.68/41.48 % (1245000)Termination reason: Instruction limit % 290.68/41.48 % (1245000)Termination phase: Saturation % 290.68/41.48 % (1245000)Time elapsed: 1.642 s % 290.68/41.48 % (1245000)Peak memory usage: 17 MB % 290.68/41.48 % (1245000)Instructions burned: 7550 (million) % 290.68/41.48 % (1245004)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1170498794:fmbsr=1.6:i=135068:rtra=on_2767 on theBenchmark for (2767ds/135068Mi) % 290.68/41.48 % Detected minimum model sizes of [1] % 290.68/41.48 % Detected maximum model sizes of [13] % 290.68/41.48 % TRYING [7] % 290.68/41.48 % Finite Model Found! % 290.68/41.48 % SZS status Satisfiable for theBenchmark % 290.68/41.48 % (1245004)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 290.68/41.48 % (1245004)------------------------------ % 290.68/41.48 % (1245004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.68/41.48 % (1245004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.68/41.48 % (1245004)CaDiCaL version: 2.1.3 % 290.68/41.48 % (1245004)Termination reason: Unknown % 290.68/41.48 % (1245004)Termination phase: Finite model building constraint generation % 290.68/41.48 % (1245004)Time elapsed: 0.003 s % 290.68/41.48 % (1245004)Peak memory usage: 10 MB % 290.68/41.48 % (1245004)Instructions burned: 8 (million) % 290.68/41.48 % (1245006)ott-22_32_sil=160Terminated % 300.23/42.83 % Vampire exiting % 300.23/42.83 Terminated %------------------------------------------------------------------------------