%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX140_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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 01:46:33 PM UTC 2026 % Result : Timeout 300.30s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX140_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.16 % Computer : n005.cluster.edu % 0.09/0.16 % Model : x86_64 x86_64 % 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.16 % Memory : 8046.5625MB % 0.09/0.16 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 15:04:31 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 Running first-order model finding % 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.85/1.10 % (846700)Will run a generic schedule for satisfiability detection. % 3.85/1.10 % (846815)dis+10_1_sil=32000:sp=arity:random_seed=3164078545:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 3.85/1.10 % (846813)% WARNING: option uhcvi not known. % 3.85/1.10 % (846816)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=47787470:i=116_2996 on theBenchmark for (2996ds/116Mi) % 3.85/1.10 % (846812)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1978220295_2996 on theBenchmark for (2996ds/0Mi) % 3.85/1.10 % (846813)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=125123156:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 3.85/1.10 % (846814)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1134923603:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 3.85/1.10 % (846818)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2572364543:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 3.85/1.10 % (846817)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=81945265:i=131_2996 on theBenchmark for (2996ds/131Mi) % 3.85/1.10 % (846815)Instruction limit reached! % 3.85/1.10 % (846815)------------------------------ % 3.85/1.10 % (846815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.85/1.10 % (846815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.10 % (846815)CaDiCaL version: 2.1.3 % 3.85/1.10 % (846815)Termination reason: Instruction limit % 3.85/1.10 % (846815)Termination phase: Property scanning % 3.85/1.10 % (846815)Time elapsed: 0.023 s % 3.85/1.10 % (846815)Peak memory usage: 10 MB % 3.85/1.10 % (846815)Instructions burned: 105 (million) % 3.85/1.10 % (846826)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=685012070:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi) % 3.85/1.10 % (846816)Instruction limit reached! % 3.85/1.10 % (846816)------------------------------ % 3.85/1.10 % (846816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.85/1.10 % (846816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.10 % (846816)CaDiCaL version: 2.1.3 % 3.85/1.10 % (846816)Termination reason: Instruction limit % 3.85/1.10 % (846816)Termination phase: Property scanning % 3.85/1.10 % (846816)Time elapsed: 0.047 s % 3.85/1.10 % (846816)Peak memory usage: 10 MB % 3.85/1.10 % (846816)Instructions burned: 117 (million) % 3.85/1.10 % (846817)Instruction limit reached! % 3.85/1.10 % (846817)------------------------------ % 3.85/1.10 % (846817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.85/1.10 % (846817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.10 % (846817)CaDiCaL version: 2.1.3 % 3.85/1.10 % (846817)Termination reason: Instruction limit % 3.85/1.10 % (846817)Termination phase: Property scanning % 3.85/1.10 % (846817)Time elapsed: 0.053 s % 3.85/1.10 % (846817)Peak memory usage: 10 MB % 3.85/1.10 % (846817)Instructions burned: 132 (million) % 3.85/1.10 % (846818)Instruction limit reached! % 3.85/1.10 % (846818)------------------------------ % 3.85/1.10 % (846818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.85/1.10 % (846818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.10 % (846818)CaDiCaL version: 2.1.3 % 3.85/1.10 % (846818)Termination reason: Instruction limit % 3.85/1.10 % (846818)Termination phase: Property scanning % 3.85/1.10 % (846818)Time elapsed: 0.064 s % 3.85/1.10 % (846818)Peak memory usage: 10 MB % 3.85/1.10 % (846818)Instructions burned: 161 (million) % 3.85/1.10 % (846828)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=720217105:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi) % 3.85/1.10 % (846829)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=880067208:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi) % 3.85/1.10 % (846830)ott-21_1_sil=16000:fs=off:random_seed=3834615222:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 3.85/1.10 % (846828)Instruction limit reached! % 3.85/1.10 % (846828)------------------------------ % 3.85/1.10 % (846828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.85/1.10 % (846828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.10 % (846828)CaDiCaL version: 2.1.3 % 3.85/1.10 % (846828)Termination reason: Instruction limit % 6.03/1.63 % (846828)Termination phase: Property scanning % 6.03/1.63 % (846828)Time elapsed: 0.052 s % 6.03/1.63 % (846828)Peak memory usage: 10 MB % 6.03/1.63 % (846828)Instructions burned: 132 (million) % 6.03/1.63 % (846826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.03/1.63 % (846826)Terminated due to inappropriate strategy. % 6.03/1.63 % (846826)------------------------------ % 6.03/1.63 % (846826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.03/1.63 % (846826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.63 % (846826)CaDiCaL version: 2.1.3 % 6.03/1.63 % (846826)Termination reason: Inappropriate % 6.03/1.63 % (846826)Time elapsed: 0.095 s % 6.03/1.63 % (846826)Peak memory usage: 11 MB % 6.03/1.63 % (846826)Instructions burned: 467 (million) % 6.03/1.63 % (846826)------------------------------ % 6.03/1.63 % (846826)------------------------------ % 6.03/1.63 % (846835)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=11766596:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 6.03/1.63 % (846834)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3821639092:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 6.03/1.63 % (846830)Instruction limit reached! % 6.03/1.63 % (846830)------------------------------ % 6.03/1.63 % (846830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.03/1.63 % (846830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.63 % (846830)CaDiCaL version: 2.1.3 % 6.03/1.63 % (846830)Termination reason: Instruction limit % 6.03/1.63 % (846830)Termination phase: Property scanning % 6.03/1.63 % (846830)Time elapsed: 0.071 s % 6.03/1.63 % (846830)Peak memory usage: 10 MB % 6.03/1.63 % (846830)Instructions burned: 180 (million) % 6.03/1.63 % (846838)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=105602016:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 6.03/1.63 % (846812)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.03/1.63 % (846812)Terminated due to inappropriate strategy. % 6.03/1.63 % (846812)------------------------------ % 6.03/1.63 % (846812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.03/1.63 % (846812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.63 % (846812)CaDiCaL version: 2.1.3 % 6.03/1.63 % (846812)Termination reason: Inappropriate % 6.03/1.63 % (846812)Time elapsed: 0.178 s % 6.03/1.63 % (846812)Peak memory usage: 11 MB % 6.03/1.63 % (846812)Instructions burned: 467 (million) % 6.03/1.63 % (846812)------------------------------ % 6.03/1.63 % (846812)------------------------------ % 6.03/1.63 % (846840)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3705178944:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 6.03/1.63 % (846835)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.03/1.63 % (846835)Terminated due to inappropriate strategy. % 6.03/1.63 % (846835)------------------------------ % 6.03/1.63 % (846835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.03/1.63 % (846835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.63 % (846835)CaDiCaL version: 2.1.3 % 6.03/1.63 % (846835)Termination reason: Inappropriate % 6.03/1.63 % (846835)Time elapsed: 0.072 s % 6.03/1.63 % (846835)Peak memory usage: 11 MB % 6.03/1.63 % (846835)Instructions burned: 354 (million) % 6.03/1.63 % (846835)------------------------------ % 6.03/1.63 % (846835)------------------------------ % 6.03/1.63 % (846842)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=3928702381:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 6.03/1.63 % (846834)Instruction limit reached! % 6.03/1.63 % (846834)------------------------------ % 6.03/1.63 % (846834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.03/1.63 % (846834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.63 % (846834)CaDiCaL version: 2.1.3 % 6.03/1.63 % (846834)Termination reason: Instruction limit % 6.03/1.63 % (846834)Termination phase: Saturation % 6.03/1.63 % (846834)Time elapsed: 0.183 s % 6.03/1.63 % (846834)Peak memory usage: 12 MB % 6.03/1.63 % (846834)Instructions burned: 479 (million) % 6.03/1.63 % (846840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/3.15 % (846840)Terminated due to inappropriate strategy. % 18.77/3.15 % (846840)------------------------------ % 18.77/3.15 % (846840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846840)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846840)Termination reason: Inappropriate % 18.77/3.15 % (846840)Time elapsed: 0.136 s % 18.77/3.15 % (846840)Peak memory usage: 11 MB % 18.77/3.15 % (846840)Instructions burned: 354 (million) % 18.77/3.15 % (846840)------------------------------ % 18.77/3.15 % (846840)------------------------------ % 18.77/3.15 % (846829)Instruction limit reached! % 18.77/3.15 % (846829)------------------------------ % 18.77/3.15 % (846829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846829)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846829)Termination reason: Instruction limit % 18.77/3.15 % (846829)Termination phase: Saturation % 18.77/3.15 % (846829)Time elapsed: 0.264 s % 18.77/3.15 % (846829)Peak memory usage: 13 MB % 18.77/3.15 % (846829)Instructions burned: 686 (million) % 18.77/3.15 % (846844)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4269599763:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 18.77/3.15 % (846845)fmb+10_1_sil=64000:random_seed=2827055217:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 18.77/3.15 % (846846)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1348887856:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 18.77/3.15 % (846842)Instruction limit reached! % 18.77/3.15 % (846842)------------------------------ % 18.77/3.15 % (846842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846842)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846842)Termination reason: Instruction limit % 18.77/3.15 % (846842)Termination phase: Saturation % 18.77/3.15 % (846842)Time elapsed: 0.142 s % 18.77/3.15 % (846842)Peak memory usage: 13 MB % 18.77/3.15 % (846842)Instructions burned: 692 (million) % 18.77/3.15 % (846850)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2536398594:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 18.77/3.15 % (846850)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/3.15 % (846850)Terminated due to inappropriate strategy. % 18.77/3.15 % (846850)------------------------------ % 18.77/3.15 % (846850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846850)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846850)Termination reason: Inappropriate % 18.77/3.15 % (846850)Time elapsed: 0.094 s % 18.77/3.15 % (846850)Peak memory usage: 11 MB % 18.77/3.15 % (846850)Instructions burned: 467 (million) % 18.77/3.15 % (846850)------------------------------ % 18.77/3.15 % (846850)------------------------------ % 18.77/3.15 % (846852)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=737495328:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 18.77/3.15 % (846845)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/3.15 % (846845)Terminated due to inappropriate strategy. % 18.77/3.15 % (846845)------------------------------ % 18.77/3.15 % (846845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846845)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846845)Termination reason: Inappropriate % 18.77/3.15 % (846845)Time elapsed: 0.178 s % 18.77/3.15 % (846845)Peak memory usage: 11 MB % 18.77/3.15 % (846845)Instructions burned: 467 (million) % 18.77/3.15 % (846845)------------------------------ % 18.77/3.15 % (846845)------------------------------ % 18.77/3.15 % (846846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/3.15 % (846846)Terminated due to inappropriate strategy. % 18.77/3.15 % (846846)------------------------------ % 18.77/3.15 % (846846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/3.15 % (846846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/3.15 % (846846)CaDiCaL version: 2.1.3 % 18.77/3.15 % (846846)Termination reason: Inappropriate % 18.77/3.15 % (846846)Time elapsed: 0.182 s % 18.77/3.15 % (846846)Peak memory usage: 11 MB % 20.59/3.54 % (846846)Instructions burned: 467 (million) % 20.59/3.54 % (846846)------------------------------ % 20.59/3.54 % (846846)------------------------------ % 20.59/3.54 % (846854)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1531511955:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 20.59/3.54 % (846855)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4234563806:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 20.59/3.54 % (846838)Instruction limit reached! % 20.59/3.54 % (846838)------------------------------ % 20.59/3.54 % (846838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.59/3.54 % (846838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.54 % (846838)CaDiCaL version: 2.1.3 % 20.59/3.54 % (846838)Termination reason: Instruction limit % 20.59/3.54 % (846838)Termination phase: Saturation % 20.59/3.54 % (846838)Time elapsed: 0.472 s % 20.59/3.54 % (846838)Peak memory usage: 18 MB % 20.59/3.54 % (846838)Instructions burned: 1179 (million) % 20.59/3.54 % (846858)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3380093697:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 20.59/3.54 % (846844)Instruction limit reached! % 20.59/3.54 % (846844)------------------------------ % 20.59/3.54 % (846844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.59/3.54 % (846844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.54 % (846844)CaDiCaL version: 2.1.3 % 20.59/3.54 % (846844)Termination reason: Instruction limit % 20.59/3.54 % (846844)Termination phase: Saturation % 20.59/3.54 % (846844)Time elapsed: 0.350 s % 20.59/3.54 % (846844)Peak memory usage: 15 MB % 20.59/3.54 % (846844)Instructions burned: 879 (million) % 20.59/3.54 % (846860)ott-2_1_sil=16000:newcnf=on:random_seed=3433803442:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 20.59/3.54 % (846855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.59/3.54 % (846855)Terminated due to inappropriate strategy. % 20.59/3.54 % (846855)------------------------------ % 20.59/3.54 % (846855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.59/3.54 % (846855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.54 % (846855)CaDiCaL version: 2.1.3 % 20.59/3.54 % (846855)Termination reason: Inappropriate % 20.59/3.54 % (846855)Time elapsed: 0.178 s % 20.59/3.54 % (846855)Peak memory usage: 11 MB % 20.59/3.54 % (846855)Instructions burned: 467 (million) % 20.59/3.54 % (846855)------------------------------ % 20.59/3.54 % (846855)------------------------------ % 20.59/3.54 % (846862)ott+10_1_sil=32000:tgt=ground:random_seed=3559705333:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 20.59/3.54 % (846858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.59/3.54 % (846858)Terminated due to inappropriate strategy. % 20.59/3.54 % (846858)------------------------------ % 20.59/3.54 % (846858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.59/3.54 % (846858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.54 % (846858)CaDiCaL version: 2.1.3 % 20.59/3.54 % (846858)Termination reason: Inappropriate % 20.59/3.54 % (846858)Time elapsed: 0.177 s % 20.59/3.54 % (846858)Peak memory usage: 11 MB % 20.59/3.54 % (846858)Instructions burned: 467 (million) % 20.59/3.54 % (846858)------------------------------ % 20.59/3.54 % (846858)------------------------------ % 20.59/3.54 % (846864)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1502938568:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 20.59/3.54 % (846864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.59/3.54 % (846864)Terminated due to inappropriate strategy. % 20.59/3.54 % (846864)------------------------------ % 20.59/3.54 % (846864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.59/3.54 % (846864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.54 % (846864)CaDiCaL version: 2.1.3 % 20.59/3.54 % (846864)Termination reason: Inappropriate % 20.59/3.54 % (846864)Time elapsed: 0.178 s % 20.59/3.54 % (846864)Peak memory usage: 11 MB % 20.59/3.54 % (846864)Instructions burned: 467 (million) % 20.59/3.54 % (846864)------------------------------ % 20.59/3.54 % (846864)------------------------------ % 20.59/3.54 % (846866)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4288736467:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 66.25/10.01 % (846860)Instruction limit reached! % 66.25/10.01 % (846860)------------------------------ % 66.25/10.01 % (846860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846860)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846860)Termination reason: Instruction limit % 66.25/10.01 % (846860)Termination phase: Saturation % 66.25/10.01 % (846860)Time elapsed: 0.368 s % 66.25/10.01 % (846860)Peak memory usage: 17 MB % 66.25/10.01 % (846860)Instructions burned: 870 (million) % 66.25/10.01 % (846868)dis+21_1_sil=32000:sas=cadical:random_seed=1431438919:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 66.25/10.01 % (846854)Instruction limit reached! % 66.25/10.01 % (846854)------------------------------ % 66.25/10.01 % (846854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846854)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846854)Termination reason: Instruction limit % 66.25/10.01 % (846854)Termination phase: Saturation % 66.25/10.01 % (846854)Time elapsed: 0.598 s % 66.25/10.01 % (846854)Peak memory usage: 18 MB % 66.25/10.01 % (846854)Instructions burned: 1473 (million) % 66.25/10.01 % (846870)ott+11_1_sil=16000:gs=on:random_seed=1302542308:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 66.25/10.01 % (846852)Instruction limit reached! % 66.25/10.01 % (846852)------------------------------ % 66.25/10.01 % (846852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846852)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846852)Termination reason: Instruction limit % 66.25/10.01 % (846852)Termination phase: Saturation % 66.25/10.01 % (846852)Time elapsed: 1.200 s % 66.25/10.01 % (846852)Peak memory usage: 21 MB % 66.25/10.01 % (846852)Instructions burned: 5135 (million) % 66.25/10.01 % (846872)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4156857090:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 66.25/10.01 % (846872)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 66.25/10.01 % (846872)Terminated due to inappropriate strategy. % 66.25/10.01 % (846872)------------------------------ % 66.25/10.01 % (846872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846872)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846872)Termination reason: Inappropriate % 66.25/10.01 % (846872)Time elapsed: 0.094 s % 66.25/10.01 % (846872)Peak memory usage: 11 MB % 66.25/10.01 % (846872)Instructions burned: 467 (million) % 66.25/10.01 % (846872)------------------------------ % 66.25/10.01 % (846872)------------------------------ % 66.25/10.01 % (846874)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2658436975:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 66.25/10.01 % (846870)Instruction limit reached! % 66.25/10.01 % (846870)------------------------------ % 66.25/10.01 % (846870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846870)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846870)Termination reason: Instruction limit % 66.25/10.01 % (846870)Termination phase: Saturation % 66.25/10.01 % (846870)Time elapsed: 0.891 s % 66.25/10.01 % (846870)Peak memory usage: 19 MB % 66.25/10.01 % (846870)Instructions burned: 2254 (million) % 66.25/10.01 % (846876)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3485795446:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 66.25/10.01 % (846866)Instruction limit reached! % 66.25/10.01 % (846866)------------------------------ % 66.25/10.01 % (846866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.25/10.01 % (846866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.25/10.01 % (846866)CaDiCaL version: 2.1.3 % 66.25/10.01 % (846866)Termination reason: Instruction limit % 66.25/10.01 % (846866)Termination phase: Saturation % 66.25/10.01 % (846866)Time elapsed: 1.499 s % 66.25/10.01 % (846866)Peak memory usage: 20 MB % 66.25/10.01 % (846866)Instructions burned: 3514 (million) % 66.25/10.01 % (846878)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4001222294:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 89.67/13.17 % (846868)Instruction limit reached! % 89.67/13.17 % (846868)------------------------------ % 89.67/13.17 % (846868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846868)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846868)Termination reason: Instruction limit % 89.67/13.17 % (846868)Termination phase: Saturation % 89.67/13.17 % (846868)Time elapsed: 1.635 s % 89.67/13.17 % (846868)Peak memory usage: 19 MB % 89.67/13.17 % (846868)Instructions burned: 3777 (million) % 89.67/13.17 % (846880)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1397222602:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 89.67/13.17 % (846862)Instruction limit reached! % 89.67/13.17 % (846862)------------------------------ % 89.67/13.17 % (846862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846862)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846862)Termination reason: Instruction limit % 89.67/13.17 % (846862)Termination phase: Saturation % 89.67/13.17 % (846862)Time elapsed: 2.016 s % 89.67/13.17 % (846862)Peak memory usage: 29 MB % 89.67/13.17 % (846862)Instructions burned: 5116 (million) % 89.67/13.17 % (846882)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3249207497:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 89.67/13.17 % (846874)Instruction limit reached! % 89.67/13.17 % (846874)------------------------------ % 89.67/13.17 % (846874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846874)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846874)Termination reason: Instruction limit % 89.67/13.17 % (846874)Termination phase: Saturation % 89.67/13.17 % (846874)Time elapsed: 1.047 s % 89.67/13.17 % (846874)Peak memory usage: 18 MB % 89.67/13.17 % (846874)Instructions burned: 4594 (million) % 89.67/13.17 % (846884)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=497856006:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 89.67/13.17 % (846880)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.67/13.17 % (846880)Terminated due to inappropriate strategy. % 89.67/13.17 % (846880)------------------------------ % 89.67/13.17 % (846880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846880)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846880)Termination reason: Inappropriate % 89.67/13.17 % (846880)Time elapsed: 0.178 s % 89.67/13.17 % (846880)Peak memory usage: 11 MB % 89.67/13.17 % (846880)Instructions burned: 467 (million) % 89.67/13.17 % (846880)------------------------------ % 89.67/13.17 % (846880)------------------------------ % 89.67/13.17 % (846884)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.67/13.17 % (846884)Terminated due to inappropriate strategy. % 89.67/13.17 % (846884)------------------------------ % 89.67/13.17 % (846884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846884)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846884)Termination reason: Inappropriate % 89.67/13.17 % (846884)Time elapsed: 0.094 s % 89.67/13.17 % (846884)Peak memory usage: 11 MB % 89.67/13.17 % (846884)Instructions burned: 467 (million) % 89.67/13.17 % (846884)------------------------------ % 89.67/13.17 % (846884)------------------------------ % 89.67/13.17 % (846886)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=571412790:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 89.67/13.17 % (846887)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=79339749:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 89.67/13.17 % (846882)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.67/13.17 % (846882)Terminated due to inappropriate strategy. % 89.67/13.17 % (846882)------------------------------ % 89.67/13.17 % (846882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.67/13.17 % (846882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.67/13.17 % (846882)CaDiCaL version: 2.1.3 % 89.67/13.17 % (846882)Termination reason: Inappropriate % 89.67/13.17 % (846882)Time elapsed: 0.177 s % 99.41/14.58 % (846882)Peak memory usage: 11 MB % 99.41/14.58 % (846882)Instructions burned: 467 (million) % 99.41/14.58 % (846882)------------------------------ % 99.41/14.58 % (846882)------------------------------ % 99.41/14.58 % (846890)dis+10_16:1_sil=16000:random_seed=1699308009:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 99.41/14.58 % (846887)Instruction limit reached! % 99.41/14.58 % (846887)------------------------------ % 99.41/14.58 % (846887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846887)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846887)Termination reason: Instruction limit % 99.41/14.58 % (846887)Termination phase: Saturation % 99.41/14.58 % (846887)Time elapsed: 1.730 s % 99.41/14.58 % (846887)Peak memory usage: 29 MB % 99.41/14.58 % (846887)Instructions burned: 8175 (million) % 99.41/14.58 % (846892)ott-3_8_sil=64000:random_seed=2451219391:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 99.41/14.58 % (846878)Instruction limit reached! % 99.41/14.58 % (846878)------------------------------ % 99.41/14.58 % (846878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846878)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846878)Termination reason: Instruction limit % 99.41/14.58 % (846878)Termination phase: Saturation % 99.41/14.58 % (846878)Time elapsed: 2.247 s % 99.41/14.58 % (846878)Peak memory usage: 21 MB % 99.41/14.58 % (846878)Instructions burned: 5211 (million) % 99.41/14.58 % (846894)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=216241414:fmbsr=2:i=32576_2948 on theBenchmark for (2948ds/32576Mi) % 99.41/14.58 % (846894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.41/14.58 % (846894)Terminated due to inappropriate strategy. % 99.41/14.58 % (846894)------------------------------ % 99.41/14.58 % (846894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846894)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846894)Termination reason: Inappropriate % 99.41/14.58 % (846894)Time elapsed: 0.178 s % 99.41/14.58 % (846894)Peak memory usage: 11 MB % 99.41/14.58 % (846894)Instructions burned: 467 (million) % 99.41/14.58 % (846894)------------------------------ % 99.41/14.58 % (846894)------------------------------ % 99.41/14.58 % (846896)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=867858934:i=11404_2946 on theBenchmark for (2946ds/11404Mi) % 99.41/14.58 % (846890)Instruction limit reached! % 99.41/14.58 % (846890)------------------------------ % 99.41/14.58 % (846890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846890)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846890)Termination reason: Instruction limit % 99.41/14.58 % (846890)Termination phase: Saturation % 99.41/14.58 % (846890)Time elapsed: 3.563 s % 99.41/14.58 % (846890)Peak memory usage: 22 MB % 99.41/14.58 % (846890)Instructions burned: 9157 (million) % 99.41/14.58 % (846898)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=358268262:i=14134_2930 on theBenchmark for (2930ds/14134Mi) % 99.41/14.58 % (846892)Instruction limit reached! % 99.41/14.58 % (846892)------------------------------ % 99.41/14.58 % (846892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846892)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846892)Termination reason: Instruction limit % 99.41/14.58 % (846892)Termination phase: Saturation % 99.41/14.58 % (846892)Time elapsed: 4.067 s % 99.41/14.58 % (846892)Peak memory usage: 31 MB % 99.41/14.58 % (846892)Instructions burned: 20142 (million) % 99.41/14.58 % (846900)dis+33_16_sil=32000:sac=on:random_seed=1029051670:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 99.41/14.58 % (846896)Instruction limit reached! % 99.41/14.58 % (846896)------------------------------ % 99.41/14.58 % (846896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.41/14.58 % (846896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.41/14.58 % (846896)CaDiCaL version: 2.1.3 % 99.41/14.58 % (846896)Termination reason: Instruction limit % 99.41/14.58 % (846896)Termination phase: Saturation % 99.41/14.58 % (846896)Time elapsed: 4.375 s % 99.41/14.58 % (846896)Peak memory usage: 29 MB % 99.41/14.58 % (846896)Instructions burned: 11404 (million) % 99.41/14.58 % (846902)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3365891854:avsq=on:i=17627:add=on:amm=off_2902 on theBenchmark for (2902ds/17627Mi) % 134.84/19.55 % (846898)Instruction limit reached! % 134.84/19.55 % (846898)------------------------------ % 134.84/19.55 % (846898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846898)CaDiCaL version: 2.1.3 % 134.84/19.55 % (846898)Termination reason: Instruction limit % 134.84/19.55 % (846898)Termination phase: Saturation % 134.84/19.55 % (846898)Time elapsed: 5.425 s % 134.84/19.55 % (846898)Peak memory usage: 29 MB % 134.84/19.55 % (846898)Instructions burned: 14137 (million) % 134.84/19.55 % (846904)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3363192592:s2a=on:i=53295_2876 on theBenchmark for (2876ds/53295Mi) % 134.84/19.55 % (846886)Instruction limit reached! % 134.84/19.55 % (846886)------------------------------ % 134.84/19.55 % (846886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846886)CaDiCaL version: 2.1.3 % 134.84/19.55 % (846886)Termination reason: Instruction limit % 134.84/19.55 % (846886)Termination phase: Saturation % 134.84/19.55 % (846886)Time elapsed: 9.116 s % 134.84/19.55 % (846886)Peak memory usage: 18 MB % 134.84/19.55 % (846886)Instructions burned: 22566 (million) % 134.84/19.55 % (846906)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3264634613:i=26857:ins=20_2875 on theBenchmark for (2875ds/26857Mi) % 134.84/19.55 % (846906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.84/19.55 % (846906)Terminated due to inappropriate strategy. % 134.84/19.55 % (846906)------------------------------ % 134.84/19.55 % (846906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846906)CaDiCaL version: 2.1.3 % 134.84/19.55 % (846906)Termination reason: Inappropriate % 134.84/19.55 % (846906)Time elapsed: 0.178 s % 134.84/19.55 % (846906)Peak memory usage: 11 MB % 134.84/19.55 % (846906)Instructions burned: 467 (million) % 134.84/19.55 % (846906)------------------------------ % 134.84/19.55 % (846906)------------------------------ % 134.84/19.55 % (846908)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2997056469:i=28120:bs=on:fsr=off_2873 on theBenchmark for (2873ds/28120Mi) % 134.84/19.55 % (846900)Instruction limit reached! % 134.84/19.55 % (846900)------------------------------ % 134.84/19.55 % (846900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846900)CaDiCaL version: 2.1.3 % 134.84/19.55 % (846900)Termination reason: Instruction limit % 134.84/19.55 % (846900)Termination phase: Saturation % 134.84/19.55 % (846900)Time elapsed: 3.592 s % 134.84/19.55 % (846900)Peak memory usage: 27 MB % 134.84/19.55 % (846900)Instructions burned: 15856 (million) % 134.84/19.55 % (846910)fmb+10_1_sil=256000:fmbss=7:random_seed=1900805547:fmbsr=1.6:i=182295_2872 on theBenchmark for (2872ds/182295Mi) % 134.84/19.55 % (846910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.84/19.55 % (846910)Terminated due to inappropriate strategy. % 134.84/19.55 % (846910)------------------------------ % 134.84/19.55 % (846910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846910)CaDiCaL version: 2.1.3 % 134.84/19.55 % (846910)Termination reason: Inappropriate % 134.84/19.55 % (846910)Time elapsed: 0.094 s % 134.84/19.55 % (846910)Peak memory usage: 11 MB % 134.84/19.55 % (846910)Instructions burned: 467 (million) % 134.84/19.55 % (846910)------------------------------ % 134.84/19.55 % (846910)------------------------------ % 134.84/19.55 % (846912)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3297262035:i=44625:gsp=on_2871 on theBenchmark for (2871ds/44625Mi) % 134.84/19.55 % (846912)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.84/19.55 % (846912)Terminated due to inappropriate strategy. % 134.84/19.55 % (846912)------------------------------ % 134.84/19.55 % (846912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.84/19.55 % (846912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.84/19.55 % (846912)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846912)Termination reason: Inappropriate % 151.10/21.96 % (846912)Time elapsed: 0.095 s % 151.10/21.96 % (846912)Peak memory usage: 11 MB % 151.10/21.96 % (846912)Instructions burned: 467 (million) % 151.10/21.96 % (846912)------------------------------ % 151.10/21.96 % (846912)------------------------------ % 151.10/21.96 % (846914)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3895790421:i=160505_2870 on theBenchmark for (2870ds/160505Mi) % 151.10/21.96 % (846914)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.10/21.96 % (846914)Terminated due to inappropriate strategy. % 151.10/21.96 % (846914)------------------------------ % 151.10/21.96 % (846914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.10/21.96 % (846914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.10/21.96 % (846914)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846914)Termination reason: Inappropriate % 151.10/21.96 % (846914)Time elapsed: 0.094 s % 151.10/21.96 % (846914)Peak memory usage: 11 MB % 151.10/21.96 % (846914)Instructions burned: 467 (million) % 151.10/21.96 % (846914)------------------------------ % 151.10/21.96 % (846914)------------------------------ % 151.10/21.96 % (846916)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3586492724:fmbsr=1.3:i=225729_2869 on theBenchmark for (2869ds/225729Mi) % 151.10/21.96 % (846916)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.10/21.96 % (846916)Terminated due to inappropriate strategy. % 151.10/21.96 % (846916)------------------------------ % 151.10/21.96 % (846916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.10/21.96 % (846916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.10/21.96 % (846916)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846916)Termination reason: Inappropriate % 151.10/21.96 % (846916)Time elapsed: 0.097 s % 151.10/21.96 % (846916)Peak memory usage: 11 MB % 151.10/21.96 % (846916)Instructions burned: 467 (million) % 151.10/21.96 % (846916)------------------------------ % 151.10/21.96 % (846916)------------------------------ % 151.10/21.96 % (846918)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2397427348:fmbsr=2:i=185024:ins=7_2868 on theBenchmark for (2868ds/185024Mi) % 151.10/21.96 % (846918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.10/21.96 % (846918)Terminated due to inappropriate strategy. % 151.10/21.96 % (846918)------------------------------ % 151.10/21.96 % (846918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.10/21.96 % (846918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.10/21.96 % (846918)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846918)Termination reason: Inappropriate % 151.10/21.96 % (846918)Time elapsed: 0.094 s % 151.10/21.96 % (846918)Peak memory usage: 11 MB % 151.10/21.96 % (846918)Instructions burned: 467 (million) % 151.10/21.96 % (846918)------------------------------ % 151.10/21.96 % (846918)------------------------------ % 151.10/21.96 % (846920)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=547630539:rtra=on_2867 on theBenchmark for (2867ds/0Mi) % 151.10/21.96 % (846920)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.10/21.96 % (846920)Terminated due to inappropriate strategy. % 151.10/21.96 % (846920)------------------------------ % 151.10/21.96 % (846920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.10/21.96 % (846920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.10/21.96 % (846920)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846920)Termination reason: Inappropriate % 151.10/21.96 % (846920)Time elapsed: 0.095 s % 151.10/21.96 % (846920)Peak memory usage: 11 MB % 151.10/21.96 % (846920)Instructions burned: 469 (million) % 151.10/21.96 % (846920)------------------------------ % 151.10/21.96 % (846920)------------------------------ % 151.10/21.96 % (846922)% WARNING: option uhcvi not known. % 151.10/21.96 % (846922)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4116285550:i=271062:add=off:rtra=on:rawr=on_2866 on theBenchmark for (2866ds/271062Mi) % 151.10/21.96 % (846876)Instruction limit reached! % 151.10/21.96 % (846876)------------------------------ % 151.10/21.96 % (846876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.10/21.96 % (846876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.10/21.96 % (846876)CaDiCaL version: 2.1.3 % 151.10/21.96 % (846876)Termination reason: Instruction limit % 151.10/21.96 % (846876)Termination phase: Saturation % 151.10/21.96 % (846876)Time elapsed: 11.932 s % 151.10/21.96 % (846876)Peak memory usage: 17 MB % 165.29/23.81 % (846876)Instructions burned: 29341 (million) % 165.29/23.81 % (847056)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3400831019:i=176048:add=on:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/176048Mi) % 165.29/23.81 % (846902)Instruction limit reached! % 165.29/23.81 % (846902)------------------------------ % 165.29/23.81 % (846902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (846902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (846902)CaDiCaL version: 2.1.3 % 165.29/23.81 % (846902)Termination reason: Instruction limit % 165.29/23.81 % (846902)Termination phase: Saturation % 165.29/23.81 % (846902)Time elapsed: 8.849 s % 165.29/23.81 % (846902)Peak memory usage: 93 MB % 165.29/23.81 % (846902)Instructions burned: 17628 (million) % 165.29/23.81 % (847401)dis+10_1_sil=32000:si=on:sp=arity:random_seed=45165792:i=206:fgj=on:rtra=on_2813 on theBenchmark for (2813ds/206Mi) % 165.29/23.81 % (847401)Instruction limit reached! % 165.29/23.81 % (847401)------------------------------ % 165.29/23.81 % (847401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (847401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (847401)CaDiCaL version: 2.1.3 % 165.29/23.81 % (847401)Termination reason: Instruction limit % 165.29/23.81 % (847401)Termination phase: Property scanning % 165.29/23.81 % (847401)Time elapsed: 0.081 s % 165.29/23.81 % (847401)Peak memory usage: 10 MB % 165.29/23.81 % (847401)Instructions burned: 206 (million) % 165.29/23.81 % (847403)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2948323408:i=232:rtra=on_2812 on theBenchmark for (2812ds/232Mi) % 165.29/23.81 % (847403)Instruction limit reached! % 165.29/23.81 % (847403)------------------------------ % 165.29/23.81 % (847403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (847403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (847403)CaDiCaL version: 2.1.3 % 165.29/23.81 % (847403)Termination reason: Instruction limit % 165.29/23.81 % (847403)Termination phase: Property scanning % 165.29/23.81 % (847403)Time elapsed: 0.090 s % 165.29/23.81 % (847403)Peak memory usage: 10 MB % 165.29/23.81 % (847403)Instructions burned: 232 (million) % 165.29/23.81 % (847405)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3193018258:i=262:rtra=on_2811 on theBenchmark for (2811ds/262Mi) % 165.29/23.81 % (847405)Instruction limit reached! % 165.29/23.81 % (847405)------------------------------ % 165.29/23.81 % (847405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (847405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (847405)CaDiCaL version: 2.1.3 % 165.29/23.81 % (847405)Termination reason: Instruction limit % 165.29/23.81 % (847405)Termination phase: Property scanning % 165.29/23.81 % (847405)Time elapsed: 0.102 s % 165.29/23.81 % (847405)Peak memory usage: 11 MB % 165.29/23.81 % (847405)Instructions burned: 263 (million) % 165.29/23.81 % (847407)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1865748970:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2810 on theBenchmark for (2810ds/318Mi) % 165.29/23.81 % (847407)Instruction limit reached! % 165.29/23.81 % (847407)------------------------------ % 165.29/23.81 % (847407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (847407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (847407)CaDiCaL version: 2.1.3 % 165.29/23.81 % (847407)Termination reason: Instruction limit % 165.29/23.81 % (847407)Termination phase: Property scanning % 165.29/23.81 % (847407)Time elapsed: 0.123 s % 165.29/23.81 % (847407)Peak memory usage: 11 MB % 165.29/23.81 % (847407)Instructions burned: 318 (million) % 165.29/23.81 % (847409)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3642699882:i=1428:nm=2:rtra=on_2808 on theBenchmark for (2808ds/1428Mi) % 165.29/23.81 % (847409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.29/23.81 % (847409)Terminated due to inappropriate strategy. % 165.29/23.81 % (847409)------------------------------ % 165.29/23.81 % (847409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.81 % (847409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.81 % (847409)CaDiCaL version: 2.1.3 % 165.29/23.81 % (847409)Termination reason: Inappropriate % 165.29/23.81 % (847409)Time elapsed: 0.178 s % 165.29/23.81 % (847409)Peak memory usage: 11 MB % 190.29/27.30 % (847409)Instructions burned: 468 (million) % 190.29/27.30 % (847409)------------------------------ % 190.29/27.30 % (847409)------------------------------ % 190.29/27.30 % (847411)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=436209176:i=262:bd=preordered:rtra=on:fsd=on_2806 on theBenchmark for (2806ds/262Mi) % 190.29/27.30 % (847411)Instruction limit reached! % 190.29/27.30 % (847411)------------------------------ % 190.29/27.30 % (847411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.30 % (847411)CaDiCaL version: 2.1.3 % 190.29/27.30 % (847411)Termination reason: Instruction limit % 190.29/27.30 % (847411)Termination phase: Property scanning % 190.29/27.30 % (847411)Time elapsed: 0.103 s % 190.29/27.30 % (847411)Peak memory usage: 11 MB % 190.29/27.30 % (847411)Instructions burned: 264 (million) % 190.29/27.30 % (847413)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=1956801084:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/1368Mi) % 190.29/27.30 % (847413)Instruction limit reached! % 190.29/27.30 % (847413)------------------------------ % 190.29/27.30 % (847413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.30 % (847413)CaDiCaL version: 2.1.3 % 190.29/27.30 % (847413)Termination reason: Instruction limit % 190.29/27.30 % (847413)Termination phase: Saturation % 190.29/27.30 % (847413)Time elapsed: 0.572 s % 190.29/27.30 % (847413)Peak memory usage: 17 MB % 190.29/27.30 % (847413)Instructions burned: 1369 (million) % 190.29/27.30 % (847415)ott-21_1_sil=16000:si=on:fs=off:random_seed=767249847:i=360:av=off:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/360Mi) % 190.29/27.30 % (847415)Instruction limit reached! % 190.29/27.30 % (847415)------------------------------ % 190.29/27.30 % (847415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.30 % (847415)CaDiCaL version: 2.1.3 % 190.29/27.30 % (847415)Termination reason: Instruction limit % 190.29/27.30 % (847415)Termination phase: Property scanning % 190.29/27.30 % (847415)Time elapsed: 0.139 s % 190.29/27.30 % (847415)Peak memory usage: 11 MB % 190.29/27.30 % (847415)Instructions burned: 361 (million) % 190.29/27.30 % (847417)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1628035575:i=954:bd=all:rtra=on_2797 on theBenchmark for (2797ds/954Mi) % 190.29/27.30 % (847417)Instruction limit reached! % 190.29/27.30 % (847417)------------------------------ % 190.29/27.30 % (847417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.30 % (847417)CaDiCaL version: 2.1.3 % 190.29/27.30 % (847417)Termination reason: Instruction limit % 190.29/27.30 % (847417)Termination phase: Saturation % 190.29/27.30 % (847417)Time elapsed: 0.391 s % 190.29/27.30 % (847417)Peak memory usage: 16 MB % 190.29/27.30 % (847417)Instructions burned: 954 (million) % 190.29/27.30 % (847419)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3148199688:fmbsr=1.3:i=1730:ins=25:rtra=on_2793 on theBenchmark for (2793ds/1730Mi) % 190.29/27.30 % (847419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.30 % (847419)Terminated due to inappropriate strategy. % 190.29/27.30 % (847419)------------------------------ % 190.29/27.30 % (847419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.30 % (847419)CaDiCaL version: 2.1.3 % 190.29/27.30 % (847419)Termination reason: Inappropriate % 190.29/27.30 % (847419)Time elapsed: 0.137 s % 190.29/27.30 % (847419)Peak memory usage: 11 MB % 190.29/27.30 % (847419)Instructions burned: 356 (million) % 190.29/27.30 % (847419)------------------------------ % 190.29/27.30 % (847419)------------------------------ % 190.29/27.30 % (847421)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2066201770:i=2358:rtra=on_2792 on theBenchmark for (2792ds/2358Mi) % 190.29/27.30 % (847421)Instruction limit reached! % 190.29/27.30 % (847421)------------------------------ % 190.29/27.30 % (847421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.30 % (847421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847421)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847421)Termination reason: Instruction limit % 236.98/33.91 % (847421)Termination phase: Saturation % 236.98/33.91 % (847421)Time elapsed: 0.940 s % 236.98/33.91 % (847421)Peak memory usage: 15 MB % 236.98/33.91 % (847421)Instructions burned: 2360 (million) % 236.98/33.91 % (847423)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3303381676:i=1778:ins=1:rtra=on_2782 on theBenchmark for (2782ds/1778Mi) % 236.98/33.91 % (847423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.98/33.91 % (847423)Terminated due to inappropriate strategy. % 236.98/33.91 % (847423)------------------------------ % 236.98/33.91 % (847423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.98/33.91 % (847423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847423)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847423)Termination reason: Inappropriate % 236.98/33.91 % (847423)Time elapsed: 0.137 s % 236.98/33.91 % (847423)Peak memory usage: 11 MB % 236.98/33.91 % (847423)Instructions burned: 356 (million) % 236.98/33.91 % (847423)------------------------------ % 236.98/33.91 % (847423)------------------------------ % 236.98/33.91 % (847425)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=1745242504:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1384Mi) % 236.98/33.91 % (847425)Instruction limit reached! % 236.98/33.91 % (847425)------------------------------ % 236.98/33.91 % (847425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.98/33.91 % (847425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847425)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847425)Termination reason: Instruction limit % 236.98/33.91 % (847425)Termination phase: Saturation % 236.98/33.91 % (847425)Time elapsed: 0.574 s % 236.98/33.91 % (847425)Peak memory usage: 16 MB % 236.98/33.91 % (847425)Instructions burned: 1384 (million) % 236.98/33.91 % (847427)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3639067066:i=1758:kws=inv_precedence:fsr=off:rtra=on_2774 on theBenchmark for (2774ds/1758Mi) % 236.98/33.91 % (847427)Instruction limit reached! % 236.98/33.91 % (847427)------------------------------ % 236.98/33.91 % (847427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.98/33.91 % (847427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847427)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847427)Termination reason: Instruction limit % 236.98/33.91 % (847427)Termination phase: Saturation % 236.98/33.91 % (847427)Time elapsed: 0.678 s % 236.98/33.91 % (847427)Peak memory usage: 16 MB % 236.98/33.91 % (847427)Instructions burned: 1760 (million) % 236.98/33.91 % (847429)fmb+10_1_sil=64000:si=on:random_seed=2215707476:i=44122:nm=2:rtra=on:gsp=on_2767 on theBenchmark for (2767ds/44122Mi) % 236.98/33.91 % (847429)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.98/33.91 % (847429)Terminated due to inappropriate strategy. % 236.98/33.91 % (847429)------------------------------ % 236.98/33.91 % (847429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.98/33.91 % (847429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847429)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847429)Termination reason: Inappropriate % 236.98/33.91 % (847429)Time elapsed: 0.178 s % 236.98/33.91 % (847429)Peak memory usage: 11 MB % 236.98/33.91 % (847429)Instructions burned: 468 (million) % 236.98/33.91 % (847429)------------------------------ % 236.98/33.91 % (847429)------------------------------ % 236.98/33.91 % (847431)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=444455177:i=19030:nm=5:rtra=on_2765 on theBenchmark for (2765ds/19030Mi) % 236.98/33.91 % (847431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.98/33.91 % (847431)Terminated due to inappropriate strategy. % 236.98/33.91 % (847431)------------------------------ % 236.98/33.91 % (847431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.98/33.91 % (847431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.91 % (847431)CaDiCaL version: 2.1.3 % 236.98/33.91 % (847431)Termination reason: Inappropriate % 236.98/33.91 % (847431)Time elapsed: 0.179 s % 236.98/33.91 % (847431)Peak memory usage: 11 MB % 236.98/33.91 % (847431)Instructions burned: 468 (million) % 236.98/33.91 % (847431)------------------------------ % 236.98/33.91 % (847431)------------------------------ % 268.25/38.39 % (847433)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2437327978:fmbsr=1.7:i=1840:rtra=on_2763 on theBenchmark for (2763ds/1840Mi) % 268.25/38.39 % (847433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.25/38.39 % (847433)Terminated due to inappropriate strategy. % 268.25/38.39 % (847433)------------------------------ % 268.25/38.39 % (847433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.25/38.39 % (847433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.25/38.39 % (847433)CaDiCaL version: 2.1.3 % 268.25/38.39 % (847433)Termination reason: Inappropriate % 268.25/38.39 % (847433)Time elapsed: 0.178 s % 268.25/38.39 % (847433)Peak memory usage: 11 MB % 268.25/38.39 % (847433)Instructions burned: 468 (million) % 268.25/38.39 % (847433)------------------------------ % 268.25/38.39 % (847433)------------------------------ % 268.25/38.39 % (847435)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1888402231:i=10262:rtra=on_2761 on theBenchmark for (2761ds/10262Mi) % 268.25/38.39 % (846908)Instruction limit reached! % 268.25/38.39 % (846908)------------------------------ % 268.25/38.39 % (846908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.25/38.39 % (846908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.25/38.39 % (846908)CaDiCaL version: 2.1.3 % 268.25/38.39 % (846908)Termination reason: Instruction limit % 268.25/38.39 % (846908)Termination phase: Saturation % 268.25/38.39 % (846908)Time elapsed: 12.001 s % 268.25/38.39 % (846908)Peak memory usage: 29 MB % 268.25/38.39 % (846908)Instructions burned: 28121 (million) % 268.25/38.39 % (847437)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=238952606:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2753 on theBenchmark for (2753ds/2944Mi) % 268.25/38.39 % (847437)Instruction limit reached! % 268.25/38.39 % (847437)------------------------------ % 268.25/38.39 % (847437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.25/38.39 % (847437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.25/38.39 % (847437)CaDiCaL version: 2.1.3 % 268.25/38.39 % (847437)Termination reason: Instruction limit % 268.25/38.39 % (847437)Termination phase: Saturation % 268.25/38.39 % (847437)Time elapsed: 1.262 s % 268.25/38.39 % (847437)Peak memory usage: 20 MB % 268.25/38.39 % (847437)Instructions burned: 2945 (million) % 268.25/38.39 % (847439)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=280699058:i=12648:rtra=on_2740 on theBenchmark for (2740ds/12648Mi) % 268.25/38.39 % (847439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.25/38.39 % (847439)Terminated due to inappropriate strategy. % 268.25/38.39 % (847439)------------------------------ % 268.25/38.39 % (847439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.25/38.39 % (847439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.25/38.39 % (847439)CaDiCaL version: 2.1.3 % 268.25/38.39 % (847439)Termination reason: Inappropriate % 268.25/38.39 % (847439)Time elapsed: 0.178 s % 268.25/38.39 % (847439)Peak memory usage: 11 MB % 268.25/38.39 % (847439)Instructions burned: 468 (million) % 268.25/38.39 % (847439)------------------------------ % 268.25/38.39 % (847439)------------------------------ % 268.25/38.39 % (847441)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2562978920:fmbsr=2.30978:i=4348:rtra=on_2738 on theBenchmark for (2738ds/4348Mi) % 268.25/38.39 % (847441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.25/38.39 % (847441)Terminated due to inappropriate strategy. % 268.25/38.39 % (847441)------------------------------ % 268.25/38.39 % (847441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.25/38.39 % (847441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.25/38.39 % (847441)CaDiCaL version: 2.1.3 % 268.25/38.39 % (847441)Termination reason: Inappropriate % 268.25/38.39 % (847441)Time elapsed: 0.178 s % 268.25/38.39 % (847441)Peak memory usage: 11 MB % 268.25/38.39 % (847441)Instructions burned: 468 (million) % 268.25/38.39 % (847441)------------------------------ % 268.25/38.39 % (847441)------------------------------ % 268.25/38.39 % (847443)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3130151104:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2736 on theBenchmark for (2736ds/1738Mi) % 268.25/38.39 % (847443)Instruction limit reached! % 268.25/38.39 % (847443)------------------------------ % 268.25/38.39 % (847443)Version: Vampire 5.0.1Terminated % 300.30/42.83 % Vampire exiting %------------------------------------------------------------------------------