%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SYO156^5 : TPTP v9.3.1. Released v4.0.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 : Wed Sep 30 08:49:04 AM UTC 2026 % Result : CounterSatisfiable 3.49s 0.82s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYO156^5 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 % Computer : n014.cluster.edu % 0.09/0.23 % Model : x86_64 x86_64 % 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.23 % Memory : 8046.5625MB % 0.09/0.23 % OS : Linux 6.8.0-71-generic % 0.09/0.23 % CPULimit : 300 % 0.09/0.23 % WCLimit : 300 % 0.09/0.23 % DateTime : Tue Sep 29 16:35:30 UTC 2026 % 0.09/0.23 % CPUTime : % 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.28 Running first-order model finding % 0.25/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.49/0.82 % (2897888)Will run a generic schedule for satisfiability detection. % 3.49/0.82 % (2897897)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3599647105:i=116_3000 on theBenchmark for (3000ds/116Mi) % 3.49/0.82 % (2897899)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2709836881:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi) % 3.49/0.82 % (2897894)% WARNING: option uhcvi not known. % 3.49/0.82 % (2897896)dis+10_1_sil=32000:sp=arity:random_seed=2416631481:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi) % 3.49/0.82 % (2897893)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3013165269_3000 on theBenchmark for (3000ds/0Mi) % 3.49/0.82 % (2897894)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=459929708:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi) % 3.49/0.82 % (2897895)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4085675377:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi) % 3.49/0.82 % (2897898)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=404516115:i=131_3000 on theBenchmark for (3000ds/131Mi) % 3.49/0.82 % Detected minimum model sizes of [1] % 3.49/0.82 % Detected maximum model sizes of [5] % 3.49/0.82 % TRYING [1] % 3.49/0.82 % TRYING [2] % 3.49/0.82 % Finite Model Found! % 3.49/0.82 % SZS status CounterSatisfiable for theBenchmark % 3.49/0.82 % (2897893)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.49/0.82 % (2897893)------------------------------ % 3.49/0.82 % (2897893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.82 % (2897893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.82 % (2897893)CaDiCaL version: 2.1.3 % 3.49/0.82 % (2897893)Termination reason: Unknown % 3.49/0.82 % (2897893)Termination phase: Finite model building constraint generation % 3.49/0.82 % (2897893)Time elapsed: 0.002 s % 3.49/0.82 % (2897893)Peak memory usage: 11 MB % 3.49/0.82 % (2897893)Instructions burned: 1 (million) % 3.49/0.82 % (2897897)Instruction limit reached! % 3.49/0.82 % (2897897)------------------------------ % 3.49/0.82 % (2897897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.82 % (2897897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.82 % (2897897)CaDiCaL version: 2.1.3 % 3.49/0.82 % (2897897)Termination reason: Instruction limit % 3.49/0.82 % (2897897)Termination phase: Saturation % 3.49/0.82 % (2897897)Time elapsed: 0.042 s % 3.49/0.82 % (2897897)Peak memory usage: 11 MB % 3.49/0.82 % (2897897)Instructions burned: 117 (million) % 3.49/0.82 % (2897907)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3405311868:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.49/0.82 % Detected minimum model sizes of [1] % 3.49/0.82 % Detected maximum model sizes of [6] % 3.49/0.82 % TRYING [1] % 3.49/0.82 % TRYING [2] % 3.49/0.82 % Finite Model Found! % 3.49/0.82 % SZS status CounterSatisfiable for theBenchmark % 3.49/0.82 % (2897907)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.49/0.82 % (2897907)------------------------------ % 3.49/0.82 % (2897907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.82 % (2897907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.82 % (2897907)CaDiCaL version: 2.1.3 % 3.49/0.82 % (2897907)Termination reason: Unknown % 3.49/0.82 % (2897907)Termination phase: Finite model building constraint generation % 3.49/0.82 % (2897907)Time elapsed: 0.002 s % 3.49/0.82 % (2897907)Peak memory usage: 11 MB % 3.49/0.82 % (2897907)Instructions burned: 1 (million) % 3.49/0.82 % (2897908)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2423748165:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.49/0.82 % (2897910)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=388064234:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.49/0.82 % (2897896)Instruction limit reached! % 3.49/0.82 % (2897896)------------------------------ % 3.49/0.82 % (2897896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.49/0.82 % (2897896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.49/0.82 % (2897896)CaDiCaL version: 2.1.3 % 3.49/0.82 % (2897896)Termination reason: Instruction limit % 3.49/0.82 % (2897896)Termination phase: Saturation % 3.49/0.82 % (2897896)Time elapsed: 0.075 s % 6.10/1.16 % (2897896)Peak memory usage: 11 MB % 6.10/1.16 % (2897896)Instructions burned: 103 (million) % 6.10/1.16 % (2897898)Instruction limit reached! % 6.10/1.16 % (2897898)------------------------------ % 6.10/1.16 % (2897898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.16 % (2897898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.16 % (2897898)CaDiCaL version: 2.1.3 % 6.10/1.16 % (2897898)Termination reason: Instruction limit % 6.10/1.16 % (2897898)Termination phase: Saturation % 6.10/1.16 % (2897898)Time elapsed: 0.092 s % 6.10/1.16 % (2897898)Peak memory usage: 11 MB % 6.10/1.16 % (2897898)Instructions burned: 131 (million) % 6.10/1.16 % (2897913)ott-21_1_sil=16000:fs=off:random_seed=3521767612:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.10/1.16 % (2897908)Instruction limit reached! % 6.10/1.16 % (2897908)------------------------------ % 6.10/1.16 % (2897908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.16 % (2897908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.16 % (2897908)CaDiCaL version: 2.1.3 % 6.10/1.16 % (2897908)Termination reason: Instruction limit % 6.10/1.16 % (2897908)Termination phase: Saturation % 6.10/1.16 % (2897908)Time elapsed: 0.052 s % 6.10/1.16 % (2897908)Peak memory usage: 12 MB % 6.10/1.16 % (2897908)Instructions burned: 133 (million) % 6.10/1.16 % (2897899)Instruction limit reached! % 6.10/1.16 % (2897899)------------------------------ % 6.10/1.16 % (2897899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.16 % (2897899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.16 % (2897899)CaDiCaL version: 2.1.3 % 6.10/1.16 % (2897899)Termination reason: Instruction limit % 6.10/1.16 % (2897899)Termination phase: Saturation % 6.10/1.16 % (2897899)Time elapsed: 0.116 s % 6.10/1.16 % (2897899)Peak memory usage: 12 MB % 6.10/1.16 % (2897899)Instructions burned: 160 (million) % 6.10/1.16 % (2897917)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4277794494:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.10/1.16 % (2897914)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=871225511:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.10/1.16 % (2897916)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2908741581:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.10/1.16 % Detected minimum model sizes of [1] % 6.10/1.16 % Detected maximum model sizes of [5] % 6.10/1.16 % TRYING [1] % 6.10/1.16 % TRYING [2] % 6.10/1.16 % Finite Model Found! % 6.10/1.16 % SZS status CounterSatisfiable for theBenchmark % 6.10/1.16 % (2897916)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.10/1.16 % (2897916)------------------------------ % 6.10/1.16 % (2897916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.16 % (2897916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.16 % (2897916)CaDiCaL version: 2.1.3 % 6.10/1.16 % (2897916)Termination reason: Unknown % 6.10/1.16 % (2897916)Termination phase: Finite model building constraint generation % 6.10/1.16 % (2897916)Time elapsed: 0.003 s % 6.10/1.16 % (2897916)Peak memory usage: 10 MB % 6.10/1.16 % (2897916)Instructions burned: 2 (million) % 6.10/1.16 % (2897921)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=824312242:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.10/1.16 % Detected minimum model sizes of [1] % 6.10/1.16 % Detected maximum model sizes of [5] % 6.10/1.16 % fmb_start_size (= 14) larger than a detected sort maximum size! % 6.10/1.16 % (2897921)Refutation not found, incomplete strategy % 6.10/1.16 % (2897921)------------------------------ % 6.10/1.16 % (2897921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.10/1.16 % (2897921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.16 % (2897921)CaDiCaL version: 2.1.3 % 6.10/1.16 % (2897921)Termination reason: Refutation not found, incomplete strategy % 6.10/1.16 % (2897921)Time elapsed: 0.002 s % 6.10/1.16 % (2897921)Peak memory usage: 10 MB % 6.10/1.16 % (2897921)Instructions burned: 2 (million) % 6.10/1.16 % (2897921)------------------------------ % 6.10/1.16 % (2897921)------------------------------ % 6.10/1.16 % (2897923)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=2391459402:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.10/1.16 % (2897913)Instruction limit reached! % 17.45/2.89 % (2897913)------------------------------ % 17.45/2.89 % (2897913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897913)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897913)Termination reason: Instruction limit % 17.45/2.89 % (2897913)Termination phase: Saturation % 17.45/2.89 % (2897913)Time elapsed: 0.139 s % 17.45/2.89 % (2897913)Peak memory usage: 12 MB % 17.45/2.89 % (2897913)Instructions burned: 181 (million) % 17.45/2.89 % (2897925)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1888240959:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.45/2.89 % (2897914)Instruction limit reached! % 17.45/2.89 % (2897914)------------------------------ % 17.45/2.89 % (2897914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897914)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897914)Termination reason: Instruction limit % 17.45/2.89 % (2897914)Termination phase: Saturation % 17.45/2.89 % (2897914)Time elapsed: 0.318 s % 17.45/2.89 % (2897914)Peak memory usage: 12 MB % 17.45/2.89 % (2897914)Instructions burned: 478 (million) % 17.45/2.89 % (2897917)Instruction limit reached! % 17.45/2.89 % (2897917)------------------------------ % 17.45/2.89 % (2897917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897917)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897917)Termination reason: Instruction limit % 17.45/2.89 % (2897917)Termination phase: Saturation % 17.45/2.89 % (2897917)Time elapsed: 0.333 s % 17.45/2.89 % (2897917)Peak memory usage: 12 MB % 17.45/2.89 % (2897917)Instructions burned: 1181 (million) % 17.45/2.89 % (2897928)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=54694125:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.45/2.89 % Detected minimum model sizes of [1] % 17.45/2.89 % Detected maximum model sizes of [5] % 17.45/2.89 % fmb_start_size (= 20) larger than a detected sort maximum size! % 17.45/2.89 % (2897928)Refutation not found, incomplete strategy % 17.45/2.89 % (2897928)------------------------------ % 17.45/2.89 % (2897928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897928)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897928)Termination reason: Refutation not found, incomplete strategy % 17.45/2.89 % (2897928)Time elapsed: 0.001 s % 17.45/2.89 % (2897928)Peak memory usage: 10 MB % 17.45/2.89 % (2897927)fmb+10_1_sil=64000:random_seed=1436226601:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 17.45/2.89 % (2897928)------------------------------ % 17.45/2.89 % (2897928)------------------------------ % 17.45/2.89 % Detected minimum model sizes of [1] % 17.45/2.89 % Detected maximum model sizes of [5] % 17.45/2.89 % TRYING [1] % 17.45/2.89 % TRYING [2] % 17.45/2.89 % Finite Model Found! % 17.45/2.89 % SZS status CounterSatisfiable for theBenchmark % 17.45/2.89 % (2897927)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.45/2.89 % (2897927)------------------------------ % 17.45/2.89 % (2897927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897927)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897927)Termination reason: Unknown % 17.45/2.89 % (2897927)Termination phase: Finite model building constraint generation % 17.45/2.89 % (2897927)Time elapsed: 0.002 s % 17.45/2.89 % (2897927)Peak memory usage: 11 MB % 17.45/2.89 % (2897927)Instructions burned: 1 (million) % 17.45/2.89 % (2897931)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3082566672:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 17.45/2.89 % Detected minimum model sizes of [1] % 17.45/2.89 % Detected maximum model sizes of [5] % 17.45/2.89 % fmb_start_size (= 8) larger than a detected sort maximum size! % 17.45/2.89 % (2897931)Refutation not found, incomplete strategy % 17.45/2.89 % (2897931)------------------------------ % 17.45/2.89 % (2897931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.45/2.89 % (2897931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/2.89 % (2897931)CaDiCaL version: 2.1.3 % 17.45/2.89 % (2897931)Termination reason: Refutation not found, incomplete strategy % 17.45/2.89 % (2897931)Time elapsed: 0.001 s % 17.45/2.89 % (2897931)Peak memory usage: 11 MB % 25.61/3.98 % (2897931)Instructions burned: 1 (million) % 25.61/3.98 % (2897931)------------------------------ % 25.61/3.98 % (2897931)------------------------------ % 25.61/3.98 % (2897932)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3620073431:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 25.61/3.98 % (2897934)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=849615802:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 25.61/3.98 % (2897910)Instruction limit reached! % 25.61/3.98 % (2897910)------------------------------ % 25.61/3.98 % (2897910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.61/3.98 % (2897910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.61/3.98 % (2897910)CaDiCaL version: 2.1.3 % 25.61/3.98 % (2897910)Termination reason: Instruction limit % 25.61/3.98 % (2897910)Termination phase: Saturation % 25.61/3.98 % (2897910)Time elapsed: 0.463 s % 25.61/3.98 % (2897910)Peak memory usage: 13 MB % 25.61/3.98 % (2897910)Instructions burned: 684 (million) % 25.61/3.98 % (2897937)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=106021350:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 25.61/3.98 % Detected minimum model sizes of [1] % 25.61/3.98 % Detected maximum model sizes of [5] % 25.61/3.98 % fmb_start_size (= 77) larger than a detected sort maximum size! % 25.61/3.98 % (2897937)Refutation not found, incomplete strategy % 25.61/3.98 % (2897937)------------------------------ % 25.61/3.98 % (2897937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.61/3.98 % (2897937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.61/3.98 % (2897937)CaDiCaL version: 2.1.3 % 25.61/3.98 % (2897937)Termination reason: Refutation not found, incomplete strategy % 25.61/3.98 % (2897937)Time elapsed: 0.001 s % 25.61/3.98 % (2897937)Peak memory usage: 10 MB % 25.61/3.98 % (2897937)------------------------------ % 25.61/3.98 % (2897937)------------------------------ % 25.61/3.98 % (2897939)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2675567991:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 25.61/3.98 % Detected minimum model sizes of [1] % 25.61/3.98 % Detected maximum model sizes of [10] % 25.61/3.98 % fmb_start_size (= 16) larger than a detected sort maximum size! % 25.61/3.98 % (2897939)Refutation not found, incomplete strategy % 25.61/3.98 % (2897939)------------------------------ % 25.61/3.98 % (2897939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.61/3.98 % (2897939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.61/3.98 % (2897939)CaDiCaL version: 2.1.3 % 25.61/3.98 % (2897939)Termination reason: Refutation not found, incomplete strategy % 25.61/3.98 % (2897939)Time elapsed: 0.001 s % 25.61/3.98 % (2897939)Peak memory usage: 10 MB % 25.61/3.98 % (2897939)Instructions burned: 2 (million) % 25.61/3.98 % (2897939)------------------------------ % 25.61/3.98 % (2897939)------------------------------ % 25.61/3.98 % (2897941)ott-2_1_sil=16000:newcnf=on:random_seed=1689250141:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 25.61/3.98 % (2897923)Instruction limit reached! % 25.61/3.98 % (2897923)------------------------------ % 25.61/3.98 % (2897923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.61/3.98 % (2897923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.61/3.98 % (2897923)CaDiCaL version: 2.1.3 % 25.61/3.98 % (2897923)Termination reason: Instruction limit % 25.61/3.98 % (2897923)Termination phase: Saturation % 25.61/3.98 % (2897923)Time elapsed: 0.428 s % 25.61/3.98 % (2897923)Peak memory usage: 12 MB % 25.61/3.98 % (2897923)Instructions burned: 692 (million) % 25.61/3.98 % (2897943)ott+10_1_sil=32000:tgt=ground:random_seed=1092532463:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 25.61/3.98 % (2897925)Instruction limit reached! % 25.61/3.98 % (2897925)------------------------------ % 25.61/3.98 % (2897925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.61/3.98 % (2897925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.61/3.98 % (2897925)CaDiCaL version: 2.1.3 % 25.61/3.98 % (2897925)Termination reason: Instruction limit % 25.61/3.98 % (2897925)Termination phase: Saturation % 25.61/3.98 % (2897925)Time elapsed: 0.546 s % 25.61/3.98 % (2897925)Peak memory usage: 12 MB % 25.61/3.98 % (2897925)Instructions burned: 879 (million) % 25.61/3.98 % (2897945)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1534967644:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 65.78/9.67 % Detected minimum model sizes of [1] % 65.78/9.67 % Detected maximum model sizes of [5] % 65.78/9.67 % TRYING [1] % 65.78/9.67 % TRYING [2] % 65.78/9.67 % Finite Model Found! % 65.78/9.67 % SZS status CounterSatisfiable for theBenchmark % 65.78/9.67 % (2897945)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.78/9.67 % (2897945)------------------------------ % 65.78/9.67 % (2897945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.78/9.67 % (2897945)CaDiCaL version: 2.1.3 % 65.78/9.67 % (2897945)Termination reason: Unknown % 65.78/9.67 % (2897945)Termination phase: Finite model building constraint generation % 65.78/9.67 % (2897945)Time elapsed: 0.001 s % 65.78/9.67 % (2897945)Peak memory usage: 11 MB % 65.78/9.67 % (2897945)Instructions burned: 1 (million) % 65.78/9.67 % (2897947)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=695681418:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 65.78/9.67 % (2897934)Instruction limit reached! % 65.78/9.67 % (2897934)------------------------------ % 65.78/9.67 % (2897934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.78/9.67 % (2897934)CaDiCaL version: 2.1.3 % 65.78/9.67 % (2897934)Termination reason: Instruction limit % 65.78/9.67 % (2897934)Termination phase: Saturation % 65.78/9.67 % (2897934)Time elapsed: 0.611 s % 65.78/9.67 % (2897934)Peak memory usage: 12 MB % 65.78/9.67 % (2897934)Instructions burned: 1472 (million) % 65.78/9.67 % (2897941)Instruction limit reached! % 65.78/9.67 % (2897941)------------------------------ % 65.78/9.67 % (2897941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.78/9.67 % (2897941)CaDiCaL version: 2.1.3 % 65.78/9.67 % (2897941)Termination reason: Instruction limit % 65.78/9.67 % (2897941)Termination phase: Saturation % 65.78/9.67 % (2897941)Time elapsed: 0.526 s % 65.78/9.67 % (2897941)Peak memory usage: 11 MB % 65.78/9.67 % (2897941)Instructions burned: 870 (million) % 65.78/9.67 % (2897949)dis+21_1_sil=32000:sas=cadical:random_seed=1673162569:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 65.78/9.67 % (2897950)ott+11_1_sil=16000:gs=on:random_seed=3727671608:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 65.78/9.67 % (2897947)Instruction limit reached! % 65.78/9.67 % (2897947)------------------------------ % 65.78/9.67 % (2897947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.78/9.67 % (2897947)CaDiCaL version: 2.1.3 % 65.78/9.67 % (2897947)Termination reason: Instruction limit % 65.78/9.67 % (2897947)Termination phase: Saturation % 65.78/9.67 % (2897947)Time elapsed: 1.124 s % 65.78/9.67 % (2897947)Peak memory usage: 13 MB % 65.78/9.67 % (2897947)Instructions burned: 3516 (million) % 65.78/9.67 % (2897953)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=469319637:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 65.78/9.67 % Detected minimum model sizes of [1] % 65.78/9.67 % Detected maximum model sizes of [6] % 65.78/9.67 % fmb_start_size (= 7) larger than a detected sort maximum size! % 65.78/9.67 % (2897953)Refutation not found, incomplete strategy % 65.78/9.67 % (2897953)------------------------------ % 65.78/9.67 % (2897953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.78/9.67 % (2897953)CaDiCaL version: 2.1.3 % 65.78/9.67 % (2897953)Termination reason: Refutation not found, incomplete strategy % 65.78/9.67 % (2897953)Time elapsed: 0.002 s % 65.78/9.67 % (2897953)Peak memory usage: 10 MB % 65.78/9.67 % (2897953)Instructions burned: 1 (million) % 65.78/9.67 % (2897953)------------------------------ % 65.78/9.67 % (2897953)------------------------------ % 65.78/9.67 % (2897955)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2845661786:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 65.78/9.67 % (2897950)Instruction limit reached! % 65.78/9.67 % (2897950)------------------------------ % 65.78/9.67 % (2897950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.78/9.67 % (2897950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897950)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897950)Termination reason: Instruction limit % 123.80/17.79 % (2897950)Termination phase: Saturation % 123.80/17.79 % (2897950)Time elapsed: 1.388 s % 123.80/17.79 % (2897950)Peak memory usage: 12 MB % 123.80/17.79 % (2897950)Instructions burned: 2252 (million) % 123.80/17.79 % (2897957)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=260364876:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 123.80/17.79 % (2897955)Instruction limit reached! % 123.80/17.79 % (2897955)------------------------------ % 123.80/17.79 % (2897955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.80/17.79 % (2897955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897955)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897955)Termination reason: Instruction limit % 123.80/17.79 % (2897955)Termination phase: Saturation % 123.80/17.79 % (2897955)Time elapsed: 1.430 s % 123.80/17.79 % (2897955)Peak memory usage: 12 MB % 123.80/17.79 % (2897955)Instructions burned: 4592 (million) % 123.80/17.79 % (2897959)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1867490108:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 123.80/17.79 % (2897949)Instruction limit reached! % 123.80/17.79 % (2897949)------------------------------ % 123.80/17.79 % (2897949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.80/17.79 % (2897949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897949)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897949)Termination reason: Instruction limit % 123.80/17.79 % (2897949)Termination phase: Saturation % 123.80/17.79 % (2897949)Time elapsed: 2.419 s % 123.80/17.79 % (2897949)Peak memory usage: 14 MB % 123.80/17.79 % (2897949)Instructions burned: 3773 (million) % 123.80/17.79 % (2897961)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1267275735:i=5497:nm=2_2963 on theBenchmark for (2963ds/5497Mi) % 123.80/17.79 % Detected minimum model sizes of [1] % 123.80/17.79 % Detected maximum model sizes of [5] % 123.80/17.79 % fmb_start_size (= 17) larger than a detected sort maximum size! % 123.80/17.79 % (2897961)Refutation not found, incomplete strategy % 123.80/17.79 % (2897961)------------------------------ % 123.80/17.79 % (2897961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.80/17.79 % (2897961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897961)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897961)Termination reason: Refutation not found, incomplete strategy % 123.80/17.79 % (2897961)Time elapsed: 0.001 s % 123.80/17.79 % (2897961)Peak memory usage: 10 MB % 123.80/17.79 % (2897961)------------------------------ % 123.80/17.79 % (2897961)------------------------------ % 123.80/17.79 % (2897963)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3797027282:fmbsr=2:i=46332_2963 on theBenchmark for (2963ds/46332Mi) % 123.80/17.79 % Detected minimum model sizes of [1] % 123.80/17.79 % Detected maximum model sizes of [6] % 123.80/17.79 % fmb_start_size (= 15) larger than a detected sort maximum size! % 123.80/17.79 % (2897963)Refutation not found, incomplete strategy % 123.80/17.79 % (2897963)------------------------------ % 123.80/17.79 % (2897963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.80/17.79 % (2897963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897963)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897963)Termination reason: Refutation not found, incomplete strategy % 123.80/17.79 % (2897963)Time elapsed: 0.001 s % 123.80/17.79 % (2897963)Peak memory usage: 11 MB % 123.80/17.79 % (2897963)Instructions burned: 1 (million) % 123.80/17.79 % (2897963)------------------------------ % 123.80/17.79 % (2897963)------------------------------ % 123.80/17.79 % (2897965)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=385385315:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 123.80/17.79 % Detected minimum model sizes of [1] % 123.80/17.79 % Detected maximum model sizes of [5] % 123.80/17.79 % fmb_start_size (= 12) larger than a detected sort maximum size! % 123.80/17.79 % (2897965)Refutation not found, incomplete strategy % 123.80/17.79 % (2897965)------------------------------ % 123.80/17.79 % (2897965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.80/17.79 % (2897965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.80/17.79 % (2897965)CaDiCaL version: 2.1.3 % 123.80/17.79 % (2897965)Termination reason: Refutation not found, incomplete strategy % 123.80/17.79 % (2897965)Time elapsed: 0.001 s % 123.80/17.79 % (2897965)Peak memory usage: 11 MB % 123.80/17.79 % (2897965)Instructions burned: 1 (million) % 125.22/17.92 % (2897965)------------------------------ % 125.22/17.92 % (2897965)------------------------------ % 125.22/17.92 % (2897967)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4218703025:i=22565:add=on:rawr=on_2963 on theBenchmark for (2963ds/22565Mi) % 125.22/17.92 % (2897943)Instruction limit reached! % 125.22/17.92 % (2897943)------------------------------ % 125.22/17.92 % (2897943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897943)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897943)Termination reason: Instruction limit % 125.22/17.92 % (2897943)Termination phase: Saturation % 125.22/17.92 % (2897943)Time elapsed: 3.160 s % 125.22/17.92 % (2897943)Peak memory usage: 12 MB % 125.22/17.92 % (2897943)Instructions burned: 5115 (million) % 125.22/17.92 % (2897969)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3740884082:i=8173:av=off_2961 on theBenchmark for (2961ds/8173Mi) % 125.22/17.92 % (2897932)Instruction limit reached! % 125.22/17.92 % (2897932)------------------------------ % 125.22/17.92 % (2897932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897932)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897932)Termination reason: Instruction limit % 125.22/17.92 % (2897932)Termination phase: Saturation % 125.22/17.92 % (2897932)Time elapsed: 3.378 s % 125.22/17.92 % (2897932)Peak memory usage: 15 MB % 125.22/17.92 % (2897932)Instructions burned: 5132 (million) % 125.22/17.92 % (2897971)dis+10_16:1_sil=16000:random_seed=3485695069:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 125.22/17.92 % (2897959)Instruction limit reached! % 125.22/17.92 % (2897959)------------------------------ % 125.22/17.92 % (2897959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897959)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897959)Termination reason: Instruction limit % 125.22/17.92 % (2897959)Termination phase: Saturation % 125.22/17.92 % (2897959)Time elapsed: 1.722 s % 125.22/17.92 % (2897959)Peak memory usage: 14 MB % 125.22/17.92 % (2897959)Instructions burned: 5213 (million) % 125.22/17.92 % (2897973)ott-3_8_sil=64000:random_seed=2027718673:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 125.22/17.92 % (2897969)Instruction limit reached! % 125.22/17.92 % (2897969)------------------------------ % 125.22/17.92 % (2897969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897969)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897969)Termination reason: Instruction limit % 125.22/17.92 % (2897969)Termination phase: Saturation % 125.22/17.92 % (2897969)Time elapsed: 4.938 s % 125.22/17.92 % (2897969)Peak memory usage: 12 MB % 125.22/17.92 % (2897969)Instructions burned: 8174 (million) % 125.22/17.92 % (2897975)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3154780857:fmbsr=2:i=32576_2911 on theBenchmark for (2911ds/32576Mi) % 125.22/17.92 % Detected minimum model sizes of [1] % 125.22/17.92 % Detected maximum model sizes of [5] % 125.22/17.92 % fmb_start_size (= 9) larger than a detected sort maximum size! % 125.22/17.92 % (2897975)Refutation not found, incomplete strategy % 125.22/17.92 % (2897975)------------------------------ % 125.22/17.92 % (2897975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897975)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897975)Termination reason: Refutation not found, incomplete strategy % 125.22/17.92 % (2897975)Time elapsed: 0.001 s % 125.22/17.92 % (2897975)Peak memory usage: 10 MB % 125.22/17.92 % (2897975)------------------------------ % 125.22/17.92 % (2897975)------------------------------ % 125.22/17.92 % (2897977)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1662421981:i=11404_2911 on theBenchmark for (2911ds/11404Mi) % 125.22/17.92 % (2897971)Instruction limit reached! % 125.22/17.92 % (2897971)------------------------------ % 125.22/17.92 % (2897971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.22/17.92 % (2897971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.22/17.92 % (2897971)CaDiCaL version: 2.1.3 % 125.22/17.92 % (2897971)Termination reason: Instruction limit % 125.22/17.92 % (2897971)Termination phase: Saturation % 186.40/26.51 % (2897971)Time elapsed: 5.415 s % 186.40/26.51 % (2897971)Peak memory usage: 14 MB % 186.40/26.51 % (2897971)Instructions burned: 9158 (million) % 186.40/26.51 % (2897979)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2526811022:i=14134_2906 on theBenchmark for (2906ds/14134Mi) % 186.40/26.51 % (2897973)Instruction limit reached! % 186.40/26.51 % (2897973)------------------------------ % 186.40/26.51 % (2897973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.51 % (2897973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.51 % (2897973)CaDiCaL version: 2.1.3 % 186.40/26.51 % (2897973)Termination reason: Instruction limit % 186.40/26.51 % (2897973)Termination phase: Saturation % 186.40/26.51 % (2897973)Time elapsed: 5.953 s % 186.40/26.51 % (2897973)Peak memory usage: 13 MB % 186.40/26.51 % (2897973)Instructions burned: 20142 (million) % 186.40/26.51 % (2897981)dis+33_16_sil=32000:sac=on:random_seed=2543862811:i=15851:nm=0_2887 on theBenchmark for (2887ds/15851Mi) % 186.40/26.51 % (2897977)Instruction limit reached! % 186.40/26.51 % (2897977)------------------------------ % 186.40/26.51 % (2897977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.52 % (2897977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.52 % (2897977)CaDiCaL version: 2.1.3 % 186.40/26.52 % (2897977)Termination reason: Instruction limit % 186.40/26.52 % (2897977)Termination phase: Saturation % 186.40/26.52 % (2897977)Time elapsed: 6.486 s % 186.40/26.52 % (2897977)Peak memory usage: 12 MB % 186.40/26.52 % (2897977)Instructions burned: 11405 (million) % 186.40/26.52 % (2898133)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2756547908:avsq=on:i=17627:add=on:amm=off_2846 on theBenchmark for (2846ds/17627Mi) % 186.40/26.52 % (2897981)Instruction limit reached! % 186.40/26.52 % (2897981)------------------------------ % 186.40/26.52 % (2897981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.52 % (2897981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.52 % (2897981)CaDiCaL version: 2.1.3 % 186.40/26.52 % (2897981)Termination reason: Instruction limit % 186.40/26.52 % (2897981)Termination phase: Saturation % 186.40/26.52 % (2897981)Time elapsed: 4.524 s % 186.40/26.52 % (2897981)Peak memory usage: 12 MB % 186.40/26.52 % (2897981)Instructions burned: 15854 (million) % 186.40/26.52 % (2898135)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1709887502:s2a=on:i=53295_2842 on theBenchmark for (2842ds/53295Mi) % 186.40/26.52 % (2897967)Instruction limit reached! % 186.40/26.52 % (2897967)------------------------------ % 186.40/26.52 % (2897967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.52 % (2897967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.52 % (2897967)CaDiCaL version: 2.1.3 % 186.40/26.52 % (2897967)Termination reason: Instruction limit % 186.40/26.52 % (2897967)Termination phase: Saturation % 186.40/26.52 % (2897967)Time elapsed: 12.898 s % 186.40/26.52 % (2897967)Peak memory usage: 16 MB % 186.40/26.52 % (2897967)Instructions burned: 22567 (million) % 186.40/26.52 % (2898137)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1283651907:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi) % 186.40/26.52 % Detected minimum model sizes of [1] % 186.40/26.52 % Detected maximum model sizes of [5] % 186.40/26.52 % fmb_start_size (= 16) larger than a detected sort maximum size! % 186.40/26.52 % (2898137)Refutation not found, incomplete strategy % 186.40/26.52 % (2898137)------------------------------ % 186.40/26.52 % (2898137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.52 % (2898137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.52 % (2898137)CaDiCaL version: 2.1.3 % 186.40/26.52 % (2898137)Termination reason: Refutation not found, incomplete strategy % 186.40/26.52 % (2898137)Time elapsed: 0.002 s % 186.40/26.52 % (2898137)Peak memory usage: 10 MB % 186.40/26.52 % (2898137)Instructions burned: 1 (million) % 186.40/26.52 % (2898137)------------------------------ % 186.40/26.52 % (2898137)------------------------------ % 186.40/26.52 % (2898139)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3175413254:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 186.40/26.52 % (2897979)Instruction limit reached! % 186.40/26.52 % (2897979)------------------------------ % 186.40/26.52 % (2897979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.40/26.52 % (2897979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.40/26.52 % (2897979)CaDiCaL version: 2.1.3 % 186.40/26.52 % (2897979)Termination reason: Instruction limit % 197.26/28.09 % (2897979)Termination phase: Saturation % 197.26/28.09 % (2897979)Time elapsed: 8.096 s % 197.26/28.09 % (2897979)Peak memory usage: 12 MB % 197.26/28.09 % (2897979)Instructions burned: 14135 (million) % 197.26/28.09 % (2898141)fmb+10_1_sil=256000:fmbss=7:random_seed=1317030287:fmbsr=1.6:i=182295_2825 on theBenchmark for (2825ds/182295Mi) % 197.26/28.09 % Detected minimum model sizes of [1] % 197.26/28.09 % Detected maximum model sizes of [5] % 197.26/28.09 % fmb_start_size (= 7) larger than a detected sort maximum size! % 197.26/28.09 % (2898141)Refutation not found, incomplete strategy % 197.26/28.09 % (2898141)------------------------------ % 197.26/28.09 % (2898141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.26/28.09 % (2898141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.26/28.09 % (2898141)CaDiCaL version: 2.1.3 % 197.26/28.09 % (2898141)Termination reason: Refutation not found, incomplete strategy % 197.26/28.09 % (2898141)Time elapsed: 0.002 s % 197.26/28.09 % (2898141)Peak memory usage: 10 MB % 197.26/28.09 % (2898141)Instructions burned: 1 (million) % 197.26/28.09 % (2898141)------------------------------ % 197.26/28.09 % (2898141)------------------------------ % 197.26/28.09 % (2898143)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4141768176:i=44625:gsp=on_2824 on theBenchmark for (2824ds/44625Mi) % 197.26/28.09 % Detected minimum model sizes of [1] % 197.26/28.09 % Detected maximum model sizes of [5] % 197.26/28.09 % fmb_start_size (= 21) larger than a detected sort maximum size! % 197.26/28.09 % (2898143)Refutation not found, incomplete strategy % 197.26/28.09 % (2898143)------------------------------ % 197.26/28.09 % (2898143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.26/28.09 % (2898143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.26/28.09 % (2898143)CaDiCaL version: 2.1.3 % 197.26/28.09 % (2898143)Termination reason: Refutation not found, incomplete strategy % 197.26/28.09 % (2898143)Time elapsed: 0.001 s % 197.26/28.09 % (2898143)Peak memory usage: 11 MB % 197.26/28.09 % (2898143)------------------------------ % 197.26/28.09 % (2898143)------------------------------ % 197.26/28.09 % (2898145)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2418341295:i=160505_2824 on theBenchmark for (2824ds/160505Mi) % 197.26/28.09 % Detected minimum model sizes of [1] % 197.26/28.09 % Detected maximum model sizes of [5] % 197.26/28.09 % fmb_start_size (= 15) larger than a detected sort maximum size! % 197.26/28.09 % (2898145)Refutation not found, incomplete strategy % 197.26/28.09 % (2898145)------------------------------ % 197.26/28.09 % (2898145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.26/28.09 % (2898145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.26/28.09 % (2898145)CaDiCaL version: 2.1.3 % 197.26/28.09 % (2898145)Termination reason: Refutation not found, incomplete strategy % 197.26/28.09 % (2898145)Time elapsed: 0.001 s % 197.26/28.09 % (2898145)Peak memory usage: 11 MB % 197.26/28.09 % (2898145)Instructions burned: 1 (million) % 197.26/28.09 % (2898145)------------------------------ % 197.26/28.09 % (2898145)------------------------------ % 197.26/28.09 % (2898147)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1962719824:fmbsr=1.3:i=225729_2824 on theBenchmark for (2824ds/225729Mi) % 197.26/28.09 % Detected minimum model sizes of [1] % 197.26/28.09 % Detected maximum model sizes of [5] % 197.26/28.09 % fmb_start_size (= 10) larger than a detected sort maximum size! % 197.26/28.09 % (2898147)Refutation not found, incomplete strategy % 197.26/28.09 % (2898147)------------------------------ % 197.26/28.09 % (2898147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.26/28.09 % (2898147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.26/28.09 % (2898147)CaDiCaL version: 2.1.3 % 197.26/28.09 % (2898147)Termination reason: Refutation not found, incomplete strategy % 197.26/28.09 % (2898147)Time elapsed: 0.001 s % 197.26/28.09 % (2898147)Peak memory usage: 11 MB % 197.26/28.09 % (2898147)Instructions burned: 1 (million) % 197.26/28.09 % (2898147)------------------------------ % 197.26/28.09 % (2898147)------------------------------ % 197.26/28.09 % (2898149)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3631817560:fmbsr=2:i=185024:ins=7_2824 on theBenchmark for (2824ds/185024Mi) % 197.26/28.09 % Detected minimum model sizes of [1] % 197.26/28.09 % Detected maximum model sizes of [5] % 197.26/28.09 % fmb_start_size (= 10) larger than a detected sort maximum size! % 197.26/28.09 % (2898149)Refutation not found, incomplete strategy % 197.26/28.09 % (2898149)------------------------------ % 197.26/28.09 % (2898149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2898149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2898149)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2898149)Termination reason: Refutation not found, incomplete strategy % 209.34/29.88 % (2898149)Time elapsed: 0.003 s % 209.34/29.88 % (2898149)Peak memory usage: 10 MB % 209.34/29.88 % (2898149)Instructions burned: 1 (million) % 209.34/29.88 % (2898149)------------------------------ % 209.34/29.88 % (2898149)------------------------------ % 209.34/29.88 % (2898151)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2533227005:rtra=on_2823 on theBenchmark for (2823ds/0Mi) % 209.34/29.88 % Detected minimum model sizes of [1] % 209.34/29.88 % Detected maximum model sizes of [5] % 209.34/29.88 % TRYING [1] % 209.34/29.88 % TRYING [2] % 209.34/29.88 % Finite Model Found! % 209.34/29.88 % SZS status CounterSatisfiable for theBenchmark % 209.34/29.88 % (2898151)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 209.34/29.88 % (2898151)------------------------------ % 209.34/29.88 % (2898151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2898151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2898151)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2898151)Termination reason: Unknown % 209.34/29.88 % (2898151)Termination phase: Finite model building constraint generation % 209.34/29.88 % (2898151)Time elapsed: 0.001 s % 209.34/29.88 % (2898151)Peak memory usage: 12 MB % 209.34/29.88 % (2898151)Instructions burned: 1 (million) % 209.34/29.88 % (2898153)% WARNING: option uhcvi not known. % 209.34/29.88 % (2898153)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=410751704:i=271062:add=off:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/271062Mi) % 209.34/29.88 % (2897957)Instruction limit reached! % 209.34/29.88 % (2897957)------------------------------ % 209.34/29.88 % (2897957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2897957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2897957)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2897957)Termination reason: Instruction limit % 209.34/29.88 % (2897957)Termination phase: Saturation % 209.34/29.88 % (2897957)Time elapsed: 16.341 s % 209.34/29.88 % (2897957)Peak memory usage: 14 MB % 209.34/29.88 % (2897957)Instructions burned: 29341 (million) % 209.34/29.88 % (2898155)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=666255120:i=176048:add=on:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/176048Mi) % 209.34/29.88 % (2898133)Instruction limit reached! % 209.34/29.88 % (2898133)------------------------------ % 209.34/29.88 % (2898133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2898133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2898133)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2898133)Termination reason: Instruction limit % 209.34/29.88 % (2898133)Termination phase: Saturation % 209.34/29.88 % (2898133)Time elapsed: 10.469 s % 209.34/29.88 % (2898133)Peak memory usage: 16 MB % 209.34/29.88 % (2898133)Instructions burned: 17629 (million) % 209.34/29.88 % (2898157)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1759901772:i=206:fgj=on:rtra=on_2741 on theBenchmark for (2741ds/206Mi) % 209.34/29.88 % (2898157)Instruction limit reached! % 209.34/29.88 % (2898157)------------------------------ % 209.34/29.88 % (2898157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2898157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2898157)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2898157)Termination reason: Instruction limit % 209.34/29.88 % (2898157)Termination phase: Saturation % 209.34/29.88 % (2898157)Time elapsed: 0.101 s % 209.34/29.88 % (2898157)Peak memory usage: 12 MB % 209.34/29.88 % (2898157)Instructions burned: 206 (million) % 209.34/29.88 % (2898159)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3329108869:i=232:rtra=on_2740 on theBenchmark for (2740ds/232Mi) % 209.34/29.88 % (2898159)Instruction limit reached! % 209.34/29.88 % (2898159)------------------------------ % 209.34/29.88 % (2898159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.34/29.88 % (2898159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.34/29.88 % (2898159)CaDiCaL version: 2.1.3 % 209.34/29.88 % (2898159)Termination reason: Instruction limit % 209.34/29.88 % (2898159)Termination phase: Saturation % 209.34/29.88 % (2898159)Time elapsed: 0.183 s % 209.34/29.88 % (2898159)Peak memory usage: 12 MB % 209.34/29.88 % (2898159)Instructions burned: 233 (million) % 209.34/29.88 % (2898161)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2029253670:i=262:rtra=on_2738 on theBenchmark for (2738ds/262Mi) % 213.75/30.46 % (2898161)Instruction limit reached! % 213.75/30.46 % (2898161)------------------------------ % 213.75/30.46 % (2898161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.75/30.46 % (2898161)CaDiCaL version: 2.1.3 % 213.75/30.46 % (2898161)Termination reason: Instruction limit % 213.75/30.46 % (2898161)Termination phase: Saturation % 213.75/30.46 % (2898161)Time elapsed: 0.148 s % 213.75/30.46 % (2898161)Peak memory usage: 12 MB % 213.75/30.46 % (2898161)Instructions burned: 263 (million) % 213.75/30.46 % (2898163)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=347547217:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2736 on theBenchmark for (2736ds/318Mi) % 213.75/30.46 % (2898163)Instruction limit reached! % 213.75/30.46 % (2898163)------------------------------ % 213.75/30.46 % (2898163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.75/30.46 % (2898163)CaDiCaL version: 2.1.3 % 213.75/30.46 % (2898163)Termination reason: Instruction limit % 213.75/30.46 % (2898163)Termination phase: Saturation % 213.75/30.46 % (2898163)Time elapsed: 0.242 s % 213.75/30.46 % (2898163)Peak memory usage: 12 MB % 213.75/30.46 % (2898163)Instructions burned: 319 (million) % 213.75/30.46 % (2898165)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4196807465:i=1428:nm=2:rtra=on_2733 on theBenchmark for (2733ds/1428Mi) % 213.75/30.46 % Detected minimum model sizes of [1] % 213.75/30.46 % Detected maximum model sizes of [6] % 213.75/30.46 % TRYING [1] % 213.75/30.46 % TRYING [2] % 213.75/30.46 % Finite Model Found! % 213.75/30.46 % SZS status CounterSatisfiable for theBenchmark % 213.75/30.46 % (2898165)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 213.75/30.46 % (2898165)------------------------------ % 213.75/30.46 % (2898165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.75/30.46 % (2898165)CaDiCaL version: 2.1.3 % 213.75/30.46 % (2898165)Termination reason: Unknown % 213.75/30.46 % (2898165)Termination phase: Finite model building constraint generation % 213.75/30.46 % (2898165)Time elapsed: 0.001 s % 213.75/30.46 % (2898165)Peak memory usage: 11 MB % 213.75/30.46 % (2898165)Instructions burned: 1 (million) % 213.75/30.46 % (2898167)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2037223715:i=262:bd=preordered:rtra=on:fsd=on_2733 on theBenchmark for (2733ds/262Mi) % 213.75/30.46 % (2898167)Instruction limit reached! % 213.75/30.46 % (2898167)------------------------------ % 213.75/30.46 % (2898167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.75/30.46 % (2898167)CaDiCaL version: 2.1.3 % 213.75/30.46 % (2898167)Termination reason: Instruction limit % 213.75/30.46 % (2898167)Termination phase: Saturation % 213.75/30.46 % (2898167)Time elapsed: 0.183 s % 213.75/30.46 % (2898167)Peak memory usage: 12 MB % 213.75/30.46 % (2898167)Instructions burned: 262 (million) % 213.75/30.46 % (2898169)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=2016819526:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2731 on theBenchmark for (2731ds/1368Mi) % 213.75/30.46 % (2898169)Instruction limit reached! % 213.75/30.46 % (2898169)------------------------------ % 213.75/30.46 % (2898169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.75/30.46 % (2898169)CaDiCaL version: 2.1.3 % 213.75/30.46 % (2898169)Termination reason: Instruction limit % 213.75/30.46 % (2898169)Termination phase: Saturation % 213.75/30.46 % (2898169)Time elapsed: 0.731 s % 213.75/30.46 % (2898169)Peak memory usage: 14 MB % 213.75/30.46 % (2898169)Instructions burned: 1370 (million) % 213.75/30.46 % (2898220)ott-21_1_sil=16000:si=on:fs=off:random_seed=1932981389:i=360:av=off:fsr=off:rtra=on_2723 on theBenchmark for (2723ds/360Mi) % 213.75/30.46 % (2898220)Instruction limit reached! % 213.75/30.46 % (2898220)------------------------------ % 213.75/30.46 % (2898220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.75/30.46 % (2898220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898220)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898220)Termination reason: Instruction limit % 221.57/31.59 % (2898220)Termination phase: Saturation % 221.57/31.59 % (2898220)Time elapsed: 0.157 s % 221.57/31.59 % (2898220)Peak memory usage: 14 MB % 221.57/31.59 % (2898220)Instructions burned: 360 (million) % 221.57/31.59 % (2898277)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3105177680:i=954:bd=all:rtra=on_2722 on theBenchmark for (2722ds/954Mi) % 221.57/31.59 % (2898277)Instruction limit reached! % 221.57/31.59 % (2898277)------------------------------ % 221.57/31.59 % (2898277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.57/31.59 % (2898277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898277)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898277)Termination reason: Instruction limit % 221.57/31.59 % (2898277)Termination phase: Saturation % 221.57/31.59 % (2898277)Time elapsed: 0.364 s % 221.57/31.59 % (2898277)Peak memory usage: 12 MB % 221.57/31.59 % (2898277)Instructions burned: 956 (million) % 221.57/31.59 % (2898331)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2886233175:fmbsr=1.3:i=1730:ins=25:rtra=on_2718 on theBenchmark for (2718ds/1730Mi) % 221.57/31.59 % Detected minimum model sizes of [1] % 221.57/31.59 % Detected maximum model sizes of [5] % 221.57/31.59 % TRYING [1] % 221.57/31.59 % TRYING [2] % 221.57/31.59 % Finite Model Found! % 221.57/31.59 % SZS status CounterSatisfiable for theBenchmark % 221.57/31.59 % (2898331)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.57/31.59 % (2898331)------------------------------ % 221.57/31.59 % (2898331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.57/31.59 % (2898331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898331)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898331)Termination reason: Unknown % 221.57/31.59 % (2898331)Termination phase: Finite model building constraint generation % 221.57/31.59 % (2898331)Time elapsed: 0.002 s % 221.57/31.59 % (2898331)Peak memory usage: 11 MB % 221.57/31.59 % (2898331)Instructions burned: 3 (million) % 221.57/31.59 % (2898333)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=210497526:i=2358:rtra=on_2717 on theBenchmark for (2717ds/2358Mi) % 221.57/31.59 % (2898333)Instruction limit reached! % 221.57/31.59 % (2898333)------------------------------ % 221.57/31.59 % (2898333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.57/31.59 % (2898333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898333)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898333)Termination reason: Instruction limit % 221.57/31.59 % (2898333)Termination phase: Saturation % 221.57/31.59 % (2898333)Time elapsed: 0.813 s % 221.57/31.59 % (2898333)Peak memory usage: 12 MB % 221.57/31.59 % (2898333)Instructions burned: 2360 (million) % 221.57/31.59 % (2898335)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3835432783:i=1778:ins=1:rtra=on_2709 on theBenchmark for (2709ds/1778Mi) % 221.57/31.59 % Detected minimum model sizes of [1] % 221.57/31.59 % Detected maximum model sizes of [5] % 221.57/31.59 % fmb_start_size (= 14) larger than a detected sort maximum size! % 221.57/31.59 % (2898335)Refutation not found, incomplete strategy % 221.57/31.59 % (2898335)------------------------------ % 221.57/31.59 % (2898335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.57/31.59 % (2898335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898335)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898335)Termination reason: Refutation not found, incomplete strategy % 221.57/31.59 % (2898335)Time elapsed: 0.001 s % 221.57/31.59 % (2898335)Peak memory usage: 10 MB % 221.57/31.59 % (2898335)Instructions burned: 2 (million) % 221.57/31.59 % (2898335)------------------------------ % 221.57/31.59 % (2898335)------------------------------ % 221.57/31.59 % (2898337)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=2776297015:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/1384Mi) % 221.57/31.59 % (2898337)Instruction limit reached! % 221.57/31.59 % (2898337)------------------------------ % 221.57/31.59 % (2898337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.57/31.59 % (2898337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.57/31.59 % (2898337)CaDiCaL version: 2.1.3 % 221.57/31.59 % (2898337)Termination reason: Instruction limit % 221.57/31.59 % (2898337)Termination phase: Saturation % 221.57/31.59 % (2898337)Time elapsed: 0.508 s % 243.47/34.62 % (2898337)Peak memory usage: 12 MB % 243.47/34.62 % (2898337)Instructions burned: 1385 (million) % 243.47/34.62 % (2898339)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3834900761:i=1758:kws=inv_precedence:fsr=off:rtra=on_2704 on theBenchmark for (2704ds/1758Mi) % 243.47/34.62 % (2898135)Instruction limit reached! % 243.47/34.62 % (2898135)------------------------------ % 243.47/34.62 % (2898135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.47/34.62 % (2898135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.47/34.62 % (2898135)CaDiCaL version: 2.1.3 % 243.47/34.62 % (2898135)Termination reason: Instruction limit % 243.47/34.62 % (2898135)Termination phase: Saturation % 243.47/34.62 % (2898135)Time elapsed: 13.982 s % 243.47/34.62 % (2898135)Peak memory usage: 16 MB % 243.47/34.62 % (2898135)Instructions burned: 53301 (million) % 243.47/34.62 % (2898341)fmb+10_1_sil=64000:si=on:random_seed=1747883664:i=44122:nm=2:rtra=on:gsp=on_2702 on theBenchmark for (2702ds/44122Mi) % 243.47/34.62 % Detected minimum model sizes of [1] % 243.47/34.62 % Detected maximum model sizes of [5] % 243.47/34.62 % TRYING [1] % 243.47/34.62 % TRYING [2] % 243.47/34.62 % Finite Model Found! % 243.47/34.62 % SZS status CounterSatisfiable for theBenchmark % 243.47/34.62 % (2898341)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 243.47/34.62 % (2898341)------------------------------ % 243.47/34.62 % (2898341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.47/34.62 % (2898341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.47/34.62 % (2898341)CaDiCaL version: 2.1.3 % 243.47/34.62 % (2898341)Termination reason: Unknown % 243.47/34.62 % (2898341)Termination phase: Finite model building constraint generation % 243.47/34.62 % (2898341)Time elapsed: 0.0000 s % 243.47/34.62 % (2898341)Peak memory usage: 10 MB % 243.47/34.62 % (2898341)Instructions burned: 1 (million) % 243.47/34.62 % (2898343)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3006772083:i=19030:nm=5:rtra=on_2702 on theBenchmark for (2702ds/19030Mi) % 243.47/34.62 % Detected minimum model sizes of [1] % 243.47/34.62 % Detected maximum model sizes of [5] % 243.47/34.62 % fmb_start_size (= 20) larger than a detected sort maximum size! % 243.47/34.62 % (2898343)Refutation not found, incomplete strategy % 243.47/34.62 % (2898343)------------------------------ % 243.47/34.62 % (2898343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.47/34.62 % (2898343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.47/34.62 % (2898343)CaDiCaL version: 2.1.3 % 243.47/34.62 % (2898343)Termination reason: Refutation not found, incomplete strategy % 243.47/34.62 % (2898343)Time elapsed: 0.0000 s % 243.47/34.62 % (2898343)Peak memory usage: 10 MB % 243.47/34.62 % (2898343)------------------------------ % 243.47/34.62 % (2898343)------------------------------ % 243.47/34.62 % (2898345)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1321997429:fmbsr=1.7:i=1840:rtra=on_2702 on theBenchmark for (2702ds/1840Mi) % 243.47/34.62 % Detected minimum model sizes of [1] % 243.47/34.62 % Detected maximum model sizes of [5] % 243.47/34.62 % fmb_start_size (= 8) larger than a detected sort maximum size! % 243.47/34.62 % (2898345)Refutation not found, incomplete strategy % 243.47/34.62 % (2898345)------------------------------ % 243.47/34.62 % (2898345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.47/34.62 % (2898345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.47/34.62 % (2898345)CaDiCaL version: 2.1.3 % 243.47/34.62 % (2898345)Termination reason: Refutation not found, incomplete strategy % 243.47/34.62 % (2898345)Time elapsed: 0.0000 s % 243.47/34.62 % (2898345)Peak memory usage: 10 MB % 243.47/34.62 % (2898345)Instructions burned: 2 (million) % 243.47/34.62 % (2898345)------------------------------ % 243.47/34.62 % (2898345)------------------------------ % 243.47/34.62 % (2898347)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=408053099:i=10262:rtra=on_2702 on theBenchmark for (2702ds/10262Mi) % 243.47/34.62 % (2898139)Instruction limit reached! % 243.47/34.62 % (2898139)------------------------------ % 243.47/34.62 % (2898139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.47/34.62 % (2898139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.47/34.62 % (2898139)CaDiCaL version: 2.1.3 % 243.47/34.62 % (2898139)Termination reason: Instruction limit % 243.47/34.62 % (2898139)Termination phase: Saturation % 243.47/34.62 % (2898139)Time elapsed: 13.505 s % 243.47/34.62 % (2898139)Peak memory usage: 14 MB % 243.47/34.62 % (2898139)Instructions burned: 28122 (million) % 262.99/37.36 % (2898349)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2297289905:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2698 on theBenchmark for (2698ds/2944Mi) % 262.99/37.36 % (2898339)Instruction limit reached! % 262.99/37.36 % (2898339)------------------------------ % 262.99/37.36 % (2898339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.99/37.36 % (2898339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.99/37.36 % (2898339)CaDiCaL version: 2.1.3 % 262.99/37.36 % (2898339)Termination reason: Instruction limit % 262.99/37.36 % (2898339)Termination phase: Saturation % 262.99/37.36 % (2898339)Time elapsed: 0.617 s % 262.99/37.36 % (2898339)Peak memory usage: 12 MB % 262.99/37.36 % (2898339)Instructions burned: 1759 (million) % 262.99/37.36 % (2898351)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1969769491:i=12648:rtra=on_2697 on theBenchmark for (2697ds/12648Mi) % 262.99/37.36 % Detected minimum model sizes of [1] % 262.99/37.36 % Detected maximum model sizes of [5] % 262.99/37.36 % fmb_start_size (= 77) larger than a detected sort maximum size! % 262.99/37.36 % (2898351)Refutation not found, incomplete strategy % 262.99/37.36 % (2898351)------------------------------ % 262.99/37.36 % (2898351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.99/37.36 % (2898351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.99/37.36 % (2898351)CaDiCaL version: 2.1.3 % 262.99/37.36 % (2898351)Termination reason: Refutation not found, incomplete strategy % 262.99/37.36 % (2898351)Time elapsed: 0.001 s % 262.99/37.36 % (2898351)Peak memory usage: 10 MB % 262.99/37.36 % (2898351)Instructions burned: 1 (million) % 262.99/37.36 % (2898351)------------------------------ % 262.99/37.36 % (2898351)------------------------------ % 262.99/37.36 % (2898353)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2631999083:fmbsr=2.30978:i=4348:rtra=on_2697 on theBenchmark for (2697ds/4348Mi) % 262.99/37.36 % Detected minimum model sizes of [1] % 262.99/37.36 % Detected maximum model sizes of [10] % 262.99/37.36 % fmb_start_size (= 16) larger than a detected sort maximum size! % 262.99/37.36 % (2898353)Refutation not found, incomplete strategy % 262.99/37.36 % (2898353)------------------------------ % 262.99/37.36 % (2898353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.99/37.36 % (2898353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.99/37.36 % (2898353)CaDiCaL version: 2.1.3 % 262.99/37.36 % (2898353)Termination reason: Refutation not found, incomplete strategy % 262.99/37.36 % (2898353)Time elapsed: 0.001 s % 262.99/37.36 % (2898353)Peak memory usage: 10 MB % 262.99/37.36 % (2898353)Instructions burned: 2 (million) % 262.99/37.36 % (2898353)------------------------------ % 262.99/37.36 % (2898353)------------------------------ % 262.99/37.36 % (2898355)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2503422077:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2697 on theBenchmark for (2697ds/1738Mi) % 262.99/37.36 % (2898355)Instruction limit reached! % 262.99/37.36 % (2898355)------------------------------ % 262.99/37.36 % (2898355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.99/37.36 % (2898355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.99/37.36 % (2898355)CaDiCaL version: 2.1.3 % 262.99/37.36 % (2898355)Termination reason: Instruction limit % 262.99/37.36 % (2898355)Termination phase: Saturation % 262.99/37.36 % (2898355)Time elapsed: 0.628 s % 262.99/37.36 % (2898355)Peak memory usage: 12 MB % 262.99/37.36 % (2898355)Instructions burned: 1738 (million) % 262.99/37.36 % (2898357)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1350208446:i=10228:av=off:rtra=on_2690 on theBenchmark for (2690ds/10228Mi) % 262.99/37.36 % (2898349)Instruction limit reached! % 262.99/37.36 % (2898349)------------------------------ % 262.99/37.36 % (2898349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.99/37.36 % (2898349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.99/37.36 % (2898349)CaDiCaL version: 2.1.3 % 262.99/37.36 % (2898349)Termination reason: Instruction limit % 262.99/37.36 % (2898349)Termination phase: Saturation % 262.99/37.36 % (2898349)Time elapsed: 1.085 s % 262.99/37.36 % (2898349)Peak memory usage: 13 MB % 262.99/37.36 % (2898349)Instructions burned: 2945 (million) % 262.99/37.36 % (2898359)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2846693574:i=108564:rtra=on_2687 on theBenchmark for (2687ds/108564Mi) % 262.99/37.36 % Detected minimum model sizes of [1] % 262.99/37.36 % Detected maximum model sizes of [5] % 262.99/37.36 % TRYING [1] % 262.99/37.36 % TRYING Terminated % 300.61/42.64 % Vampire exiting %------------------------------------------------------------------------------