%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW573_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n002.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:40:28 PM UTC 2026 % Result : Timeout 300.43s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW573_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.24 % Computer : n002.cluster.edu % 0.11/0.24 % Model : x86_64 x86_64 % 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.24 % Memory : 8046.5625MB % 0.11/0.24 % OS : Linux 6.8.0-71-generic % 0.11/0.24 % CPULimit : 300 % 0.11/0.24 % WCLimit : 300 % 0.11/0.24 % DateTime : Mon Sep 28 14:22:07 UTC 2026 % 0.11/0.24 % CPUTime : % 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.29 Running first-order model finding % 0.26/0.30 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 % 6.90/1.36 % (381078)Will run a generic schedule for satisfiability detection. % 6.90/1.36 % (381084)% WARNING: option uhcvi not known. % 6.90/1.36 % (381083)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2923884803_2999 on theBenchmark for (2999ds/0Mi) % 6.90/1.36 % (381084)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2214912860:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.90/1.36 % (381083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.90/1.36 % (381083)Terminated due to inappropriate strategy. % 6.90/1.36 % (381083)------------------------------ % 6.90/1.36 % (381083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.90/1.36 % (381083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.36 % (381083)CaDiCaL version: 2.1.3 % 6.90/1.36 % (381083)Termination reason: Inappropriate % 6.90/1.36 % (381083)Time elapsed: 0.008 s % 6.90/1.36 % (381083)Peak memory usage: 11 MB % 6.90/1.36 % (381083)Instructions burned: 16 (million) % 6.90/1.36 % (381083)------------------------------ % 6.90/1.36 % (381083)------------------------------ % 6.90/1.36 % (381087)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=986401823:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.90/1.36 % (381086)dis+10_1_sil=32000:sp=arity:random_seed=3463376540:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.90/1.36 % (381088)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1926681909:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.90/1.36 % (381089)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3352107064:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.90/1.36 % (381085)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=26537423:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.90/1.36 % (381092)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2101903378:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.90/1.36 % (381092)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.90/1.36 % (381092)Terminated due to inappropriate strategy. % 6.90/1.36 % (381092)------------------------------ % 6.90/1.36 % (381092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.90/1.36 % (381092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.36 % (381092)CaDiCaL version: 2.1.3 % 6.90/1.36 % (381092)Termination reason: Inappropriate % 6.90/1.36 % (381092)Time elapsed: 0.006 s % 6.90/1.36 % (381092)Peak memory usage: 11 MB % 6.90/1.36 % (381092)Instructions burned: 12 (million) % 6.90/1.36 % (381092)------------------------------ % 6.90/1.36 % (381092)------------------------------ % 6.90/1.36 % (381099)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=522848418:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.90/1.36 % (381086)Instruction limit reached! % 6.90/1.36 % (381086)------------------------------ % 6.90/1.36 % (381086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.90/1.36 % (381086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.36 % (381086)CaDiCaL version: 2.1.3 % 6.90/1.36 % (381086)Termination reason: Instruction limit % 6.90/1.36 % (381086)Termination phase: Saturation % 6.90/1.36 % (381086)Time elapsed: 0.107 s % 6.90/1.36 % (381086)Peak memory usage: 13 MB % 6.90/1.36 % (381086)Instructions burned: 103 (million) % 6.90/1.36 % (381099)Instruction limit reached! % 6.90/1.36 % (381099)------------------------------ % 6.90/1.36 % (381099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.90/1.36 % (381099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.36 % (381099)CaDiCaL version: 2.1.3 % 6.90/1.36 % (381099)Termination reason: Instruction limit % 6.90/1.36 % (381099)Termination phase: Saturation % 6.90/1.36 % (381099)Time elapsed: 0.077 s % 6.90/1.36 % (381099)Peak memory usage: 13 MB % 6.90/1.36 % (381099)Instructions burned: 132 (million) % 6.90/1.36 % (381087)Instruction limit reached! % 6.90/1.36 % (381087)------------------------------ % 6.90/1.36 % (381087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.90/1.36 % (381087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.36 % (381087)CaDiCaL version: 2.1.3 % 6.90/1.36 % (381087)Termination reason: Instruction limit % 6.90/1.36 % (381087)Termination phase: Saturation % 14.28/2.35 % (381087)Time elapsed: 0.124 s % 14.28/2.35 % (381087)Peak memory usage: 13 MB % 14.28/2.35 % (381087)Instructions burned: 116 (million) % 14.28/2.35 % (381101)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=610048987:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.28/2.35 % (381088)Instruction limit reached! % 14.28/2.35 % (381088)------------------------------ % 14.28/2.35 % (381088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.35 % (381088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.35 % (381088)CaDiCaL version: 2.1.3 % 14.28/2.35 % (381088)Termination reason: Instruction limit % 14.28/2.35 % (381088)Termination phase: Saturation % 14.28/2.35 % (381088)Time elapsed: 0.136 s % 14.28/2.35 % (381088)Peak memory usage: 13 MB % 14.28/2.35 % (381088)Instructions burned: 131 (million) % 14.28/2.35 % (381102)ott-21_1_sil=16000:fs=off:random_seed=3533834556:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.28/2.35 % (381103)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2146590589:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 14.28/2.35 % (381105)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3203464046:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 14.28/2.35 % (381105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.28/2.35 % (381105)Terminated due to inappropriate strategy. % 14.28/2.35 % (381105)------------------------------ % 14.28/2.35 % (381105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.35 % (381105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.35 % (381105)CaDiCaL version: 2.1.3 % 14.28/2.35 % (381105)Termination reason: Inappropriate % 14.28/2.35 % (381105)Time elapsed: 0.012 s % 14.28/2.35 % (381105)Peak memory usage: 10 MB % 14.28/2.35 % (381105)Instructions burned: 13 (million) % 14.28/2.35 % (381105)------------------------------ % 14.28/2.35 % (381105)------------------------------ % 14.28/2.35 % (381089)Instruction limit reached! % 14.28/2.35 % (381089)------------------------------ % 14.28/2.35 % (381089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.35 % (381089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.35 % (381089)CaDiCaL version: 2.1.3 % 14.28/2.35 % (381089)Termination reason: Instruction limit % 14.28/2.35 % (381089)Termination phase: Saturation % 14.28/2.35 % (381089)Time elapsed: 0.184 s % 14.28/2.35 % (381089)Peak memory usage: 14 MB % 14.28/2.35 % (381089)Instructions burned: 159 (million) % 14.28/2.35 % (381110)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=941038091:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 14.28/2.35 % (381111)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2230847273:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 14.28/2.35 % (381111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.28/2.35 % (381111)Terminated due to inappropriate strategy. % 14.28/2.35 % (381111)------------------------------ % 14.28/2.35 % (381111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.35 % (381111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.35 % (381111)CaDiCaL version: 2.1.3 % 14.28/2.35 % (381111)Termination reason: Inappropriate % 14.28/2.35 % (381111)Time elapsed: 0.025 s % 14.28/2.35 % (381111)Peak memory usage: 11 MB % 14.28/2.35 % (381111)Instructions burned: 12 (million) % 14.28/2.35 % (381111)------------------------------ % 14.28/2.35 % (381111)------------------------------ % 14.28/2.35 % (381114)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=1600806364: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) % 14.28/2.35 % (381102)Instruction limit reached! % 14.28/2.35 % (381102)------------------------------ % 14.28/2.35 % (381102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.35 % (381102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.35 % (381102)CaDiCaL version: 2.1.3 % 14.28/2.35 % (381102)Termination reason: Instruction limit % 14.28/2.35 % (381102)Termination phase: Saturation % 14.28/2.35 % (381102)Time elapsed: 0.172 s % 14.28/2.35 % (381102)Peak memory usage: 13 MB % 14.28/2.35 % (381102)Instructions burned: 180 (million) % 39.81/5.94 % (381116)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=20233018:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 39.81/5.94 % (381101)Instruction limit reached! % 39.81/5.94 % (381101)------------------------------ % 39.81/5.94 % (381101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.81/5.94 % (381101)CaDiCaL version: 2.1.3 % 39.81/5.94 % (381101)Termination reason: Instruction limit % 39.81/5.94 % (381101)Termination phase: Saturation % 39.81/5.94 % (381101)Time elapsed: 0.353 s % 39.81/5.94 % (381101)Peak memory usage: 17 MB % 39.81/5.94 % (381101)Instructions burned: 685 (million) % 39.81/5.94 % (381119)fmb+10_1_sil=64000:random_seed=3268189899:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 39.81/5.94 % (381119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.81/5.94 % (381119)Terminated due to inappropriate strategy. % 39.81/5.94 % (381119)------------------------------ % 39.81/5.94 % (381119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.81/5.94 % (381119)CaDiCaL version: 2.1.3 % 39.81/5.94 % (381119)Termination reason: Inappropriate % 39.81/5.94 % (381119)Time elapsed: 0.008 s % 39.81/5.94 % (381119)Peak memory usage: 11 MB % 39.81/5.94 % (381119)Instructions burned: 14 (million) % 39.81/5.94 % (381119)------------------------------ % 39.81/5.94 % (381119)------------------------------ % 39.81/5.94 % (381121)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=590541103:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 39.81/5.94 % (381121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.81/5.94 % (381121)Terminated due to inappropriate strategy. % 39.81/5.94 % (381121)------------------------------ % 39.81/5.94 % (381121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.81/5.94 % (381121)CaDiCaL version: 2.1.3 % 39.81/5.94 % (381121)Termination reason: Inappropriate % 39.81/5.94 % (381121)Time elapsed: 0.007 s % 39.81/5.94 % (381121)Peak memory usage: 11 MB % 39.81/5.94 % (381121)Instructions burned: 12 (million) % 39.81/5.94 % (381121)------------------------------ % 39.81/5.94 % (381121)------------------------------ % 39.81/5.94 % (381123)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3481449001:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 39.81/5.94 % (381123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.81/5.94 % (381123)Terminated due to inappropriate strategy. % 39.81/5.94 % (381123)------------------------------ % 39.81/5.94 % (381123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.81/5.94 % (381123)CaDiCaL version: 2.1.3 % 39.81/5.94 % (381123)Termination reason: Inappropriate % 39.81/5.94 % (381123)Time elapsed: 0.006 s % 39.81/5.94 % (381123)Peak memory usage: 11 MB % 39.81/5.94 % (381123)Instructions burned: 12 (million) % 39.81/5.94 % (381123)------------------------------ % 39.81/5.94 % (381123)------------------------------ % 39.81/5.94 % (381125)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1728095736:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 39.81/5.94 % (381103)Instruction limit reached! % 39.81/5.94 % (381103)------------------------------ % 39.81/5.94 % (381103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.81/5.94 % (381103)CaDiCaL version: 2.1.3 % 39.81/5.94 % (381103)Termination reason: Instruction limit % 39.81/5.94 % (381103)Termination phase: Saturation % 39.81/5.94 % (381103)Time elapsed: 0.524 s % 39.81/5.94 % (381103)Peak memory usage: 14 MB % 39.81/5.94 % (381103)Instructions burned: 477 (million) % 39.81/5.94 % (381128)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2710110451:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 39.81/5.94 % (381114)Instruction limit reached! % 39.81/5.94 % (381114)------------------------------ % 39.81/5.94 % (381114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.81/5.94 % (381114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381114)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381114)Termination reason: Instruction limit % 43.13/6.60 % (381114)Termination phase: Saturation % 43.13/6.60 % (381114)Time elapsed: 0.718 s % 43.13/6.60 % (381114)Peak memory usage: 20 MB % 43.13/6.60 % (381114)Instructions burned: 692 (million) % 43.13/6.60 % (381131)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1249797547:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 43.13/6.60 % (381131)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.13/6.60 % (381131)Terminated due to inappropriate strategy. % 43.13/6.60 % (381131)------------------------------ % 43.13/6.60 % (381131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.13/6.60 % (381131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381131)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381131)Termination reason: Inappropriate % 43.13/6.60 % (381131)Time elapsed: 0.009 s % 43.13/6.60 % (381131)Peak memory usage: 11 MB % 43.13/6.60 % (381131)Instructions burned: 16 (million) % 43.13/6.60 % (381131)------------------------------ % 43.13/6.60 % (381131)------------------------------ % 43.13/6.60 % (381133)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1421318902:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 43.13/6.60 % (381133)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.13/6.60 % (381133)Terminated due to inappropriate strategy. % 43.13/6.60 % (381133)------------------------------ % 43.13/6.60 % (381133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.13/6.60 % (381133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381133)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381133)Termination reason: Inappropriate % 43.13/6.60 % (381133)Time elapsed: 0.015 s % 43.13/6.60 % (381133)Peak memory usage: 11 MB % 43.13/6.60 % (381133)Instructions burned: 12 (million) % 43.13/6.60 % (381133)------------------------------ % 43.13/6.60 % (381133)------------------------------ % 43.13/6.60 % (381135)ott-2_1_sil=16000:newcnf=on:random_seed=1378629219:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 43.13/6.60 % (381116)Instruction limit reached! % 43.13/6.60 % (381116)------------------------------ % 43.13/6.60 % (381116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.13/6.60 % (381116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381116)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381116)Termination reason: Instruction limit % 43.13/6.60 % (381116)Termination phase: Saturation % 43.13/6.60 % (381116)Time elapsed: 0.857 s % 43.13/6.60 % (381116)Peak memory usage: 19 MB % 43.13/6.60 % (381116)Instructions burned: 879 (million) % 43.13/6.60 % (381138)ott+10_1_sil=32000:tgt=ground:random_seed=873150719:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 43.13/6.60 % (381110)Instruction limit reached! % 43.13/6.60 % (381110)------------------------------ % 43.13/6.60 % (381110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.13/6.60 % (381110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381110)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381110)Termination reason: Instruction limit % 43.13/6.60 % (381110)Termination phase: Saturation % 43.13/6.60 % (381110)Time elapsed: 1.184 s % 43.13/6.60 % (381110)Peak memory usage: 21 MB % 43.13/6.60 % (381110)Instructions burned: 1179 (million) % 43.13/6.60 % (381141)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1392535460:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 43.13/6.60 % (381141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.13/6.60 % (381141)Terminated due to inappropriate strategy. % 43.13/6.60 % (381141)------------------------------ % 43.13/6.60 % (381141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.13/6.60 % (381141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.13/6.60 % (381141)CaDiCaL version: 2.1.3 % 43.13/6.60 % (381141)Termination reason: Inappropriate % 43.13/6.60 % (381141)Time elapsed: 0.011 s % 43.13/6.60 % (381141)Peak memory usage: 11 MB % 43.13/6.60 % (381141)Instructions burned: 16 (million) % 43.13/6.60 % (381141)------------------------------ % 43.13/6.60 % (381141)------------------------------ % 43.13/6.60 % (381143)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1013758957:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 43.13/6.60 % (381135)Instruction limit reached! % 132.23/19.03 % (381135)------------------------------ % 132.23/19.03 % (381135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381135)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381135)Termination reason: Instruction limit % 132.23/19.03 % (381135)Termination phase: Saturation % 132.23/19.03 % (381135)Time elapsed: 0.890 s % 132.23/19.03 % (381135)Peak memory usage: 18 MB % 132.23/19.03 % (381135)Instructions burned: 869 (million) % 132.23/19.03 % (381149)dis+21_1_sil=32000:sas=cadical:random_seed=3439806390:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 132.23/19.03 % (381128)Instruction limit reached! % 132.23/19.03 % (381128)------------------------------ % 132.23/19.03 % (381128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381128)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381128)Termination reason: Instruction limit % 132.23/19.03 % (381128)Termination phase: Saturation % 132.23/19.03 % (381128)Time elapsed: 1.426 s % 132.23/19.03 % (381128)Peak memory usage: 25 MB % 132.23/19.03 % (381128)Instructions burned: 1472 (million) % 132.23/19.03 % (381152)ott+11_1_sil=16000:gs=on:random_seed=171094133:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 132.23/19.03 % (381125)Instruction limit reached! % 132.23/19.03 % (381125)------------------------------ % 132.23/19.03 % (381125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381125)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381125)Termination reason: Instruction limit % 132.23/19.03 % (381125)Termination phase: Saturation % 132.23/19.03 % (381125)Time elapsed: 2.540 s % 132.23/19.03 % (381125)Peak memory usage: 38 MB % 132.23/19.03 % (381125)Instructions burned: 5132 (million) % 132.23/19.03 % (381159)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2543837457:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 132.23/19.03 % (381159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.23/19.03 % (381159)Terminated due to inappropriate strategy. % 132.23/19.03 % (381159)------------------------------ % 132.23/19.03 % (381159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381159)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381159)Termination reason: Inappropriate % 132.23/19.03 % (381159)Time elapsed: 0.008 s % 132.23/19.03 % (381159)Peak memory usage: 11 MB % 132.23/19.03 % (381159)Instructions burned: 13 (million) % 132.23/19.03 % (381159)------------------------------ % 132.23/19.03 % (381159)------------------------------ % 132.23/19.03 % (381161)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2010977721:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2967 on theBenchmark for (2967ds/4591Mi) % 132.23/19.03 % (381152)Instruction limit reached! % 132.23/19.03 % (381152)------------------------------ % 132.23/19.03 % (381152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381152)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381152)Termination reason: Instruction limit % 132.23/19.03 % (381152)Termination phase: Saturation % 132.23/19.03 % (381152)Time elapsed: 2.145 s % 132.23/19.03 % (381152)Peak memory usage: 21 MB % 132.23/19.03 % (381152)Instructions burned: 2251 (million) % 132.23/19.03 % (381172)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=805050009:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 132.23/19.03 % (381143)Instruction limit reached! % 132.23/19.03 % (381143)------------------------------ % 132.23/19.03 % (381143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.23/19.03 % (381143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.23/19.03 % (381143)CaDiCaL version: 2.1.3 % 132.23/19.03 % (381143)Termination reason: Instruction limit % 132.23/19.03 % (381143)Termination phase: Saturation % 132.23/19.03 % (381143)Time elapsed: 3.161 s % 132.23/19.03 % (381143)Peak memory usage: 34 MB % 132.23/19.03 % (381143)Instructions burned: 3512 (million) % 132.23/19.03 % (381175)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=114611379:i=5211_2953 on theBenchmark for (2953ds/5211Mi) % 132.23/19.03 % (381161)Instruction limit reached! % 169.39/24.16 % (381161)------------------------------ % 169.39/24.16 % (381161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381161)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381161)Termination reason: Instruction limit % 169.39/24.16 % (381161)Termination phase: Saturation % 169.39/24.16 % (381161)Time elapsed: 2.400 s % 169.39/24.16 % (381161)Peak memory usage: 47 MB % 169.39/24.16 % (381161)Instructions burned: 4594 (million) % 169.39/24.16 % (381179)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=892090223:i=5497:nm=2_2943 on theBenchmark for (2943ds/5497Mi) % 169.39/24.16 % (381179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.39/24.16 % (381179)Terminated due to inappropriate strategy. % 169.39/24.16 % (381179)------------------------------ % 169.39/24.16 % (381179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381179)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381179)Termination reason: Inappropriate % 169.39/24.16 % (381179)Time elapsed: 0.009 s % 169.39/24.16 % (381179)Peak memory usage: 11 MB % 169.39/24.16 % (381179)Instructions burned: 15 (million) % 169.39/24.16 % (381179)------------------------------ % 169.39/24.16 % (381179)------------------------------ % 169.39/24.16 % (381149)Instruction limit reached! % 169.39/24.16 % (381149)------------------------------ % 169.39/24.16 % (381149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381149)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381149)Termination reason: Instruction limit % 169.39/24.16 % (381149)Termination phase: Saturation % 169.39/24.16 % (381149)Time elapsed: 3.598 s % 169.39/24.16 % (381149)Peak memory usage: 35 MB % 169.39/24.16 % (381149)Instructions burned: 3773 (million) % 169.39/24.16 % (381181)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1961827054:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 169.39/24.16 % (381181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.39/24.16 % (381181)Terminated due to inappropriate strategy. % 169.39/24.16 % (381181)------------------------------ % 169.39/24.16 % (381181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381181)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381181)Termination reason: Inappropriate % 169.39/24.16 % (381181)Time elapsed: 0.007 s % 169.39/24.16 % (381181)Peak memory usage: 11 MB % 169.39/24.16 % (381181)Instructions burned: 13 (million) % 169.39/24.16 % (381181)------------------------------ % 169.39/24.16 % (381181)------------------------------ % 169.39/24.16 % (381183)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2286487376:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 169.39/24.16 % (381183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.39/24.16 % (381183)Terminated due to inappropriate strategy. % 169.39/24.16 % (381183)------------------------------ % 169.39/24.16 % (381183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381183)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381183)Termination reason: Inappropriate % 169.39/24.16 % (381183)Time elapsed: 0.006 s % 169.39/24.16 % (381183)Peak memory usage: 11 MB % 169.39/24.16 % (381183)Instructions burned: 13 (million) % 169.39/24.16 % (381183)------------------------------ % 169.39/24.16 % (381183)------------------------------ % 169.39/24.16 % (381186)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2422856088:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 169.39/24.16 % (381184)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2318960171:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 169.39/24.16 % (381138)Instruction limit reached! % 169.39/24.16 % (381138)------------------------------ % 169.39/24.16 % (381138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.39/24.16 % (381138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.39/24.16 % (381138)CaDiCaL version: 2.1.3 % 169.39/24.16 % (381138)Termination reason: Instruction limit % 169.39/24.16 % (381138)Termination phase: Saturation % 169.84/24.29 % (381138)Time elapsed: 5.013 s % 169.84/24.29 % (381138)Peak memory usage: 44 MB % 169.84/24.29 % (381138)Instructions burned: 5115 (million) % 169.84/24.29 % (381192)dis+10_16:1_sil=16000:random_seed=3825239422:i=9155:fsr=off_2936 on theBenchmark for (2936ds/9155Mi) % 169.84/24.29 % (381175)Instruction limit reached! % 169.84/24.29 % (381175)------------------------------ % 169.84/24.29 % (381175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381175)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381175)Termination reason: Instruction limit % 169.84/24.29 % (381175)Termination phase: Saturation % 169.84/24.29 % (381175)Time elapsed: 4.350 s % 169.84/24.29 % (381175)Peak memory usage: 46 MB % 169.84/24.29 % (381175)Instructions burned: 5211 (million) % 169.84/24.29 % (381215)ott-3_8_sil=64000:random_seed=3647331519:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 169.84/24.29 % (381186)Instruction limit reached! % 169.84/24.29 % (381186)------------------------------ % 169.84/24.29 % (381186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381186)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381186)Termination reason: Instruction limit % 169.84/24.29 % (381186)Termination phase: Saturation % 169.84/24.29 % (381186)Time elapsed: 4.360 s % 169.84/24.29 % (381186)Peak memory usage: 80 MB % 169.84/24.29 % (381186)Instructions burned: 8178 (million) % 169.84/24.29 % (381225)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=637724325:fmbsr=2:i=32576_2898 on theBenchmark for (2898ds/32576Mi) % 169.84/24.29 % (381225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.84/24.29 % (381225)Terminated due to inappropriate strategy. % 169.84/24.29 % (381225)------------------------------ % 169.84/24.29 % (381225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381225)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381225)Termination reason: Inappropriate % 169.84/24.29 % (381225)Time elapsed: 0.010 s % 169.84/24.29 % (381225)Peak memory usage: 11 MB % 169.84/24.29 % (381225)Instructions burned: 16 (million) % 169.84/24.29 % (381225)------------------------------ % 169.84/24.29 % (381225)------------------------------ % 169.84/24.29 % (381227)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3544192373:i=11404_2898 on theBenchmark for (2898ds/11404Mi) % 169.84/24.29 % (381192)Instruction limit reached! % 169.84/24.29 % (381192)------------------------------ % 169.84/24.29 % (381192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381192)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381192)Termination reason: Instruction limit % 169.84/24.29 % (381192)Termination phase: Saturation % 169.84/24.29 % (381192)Time elapsed: 7.985 s % 169.84/24.29 % (381192)Peak memory usage: 59 MB % 169.84/24.29 % (381192)Instructions burned: 9155 (million) % 169.84/24.29 % (381399)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3344078654:i=14134_2856 on theBenchmark for (2856ds/14134Mi) % 169.84/24.29 % (381227)Instruction limit reached! % 169.84/24.29 % (381227)------------------------------ % 169.84/24.29 % (381227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381227)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381227)Termination reason: Instruction limit % 169.84/24.29 % (381227)Termination phase: Saturation % 169.84/24.29 % (381227)Time elapsed: 5.274 s % 169.84/24.29 % (381227)Peak memory usage: 82 MB % 169.84/24.29 % (381227)Instructions burned: 11407 (million) % 169.84/24.29 % (381401)dis+33_16_sil=32000:sac=on:random_seed=207235749:i=15851:nm=0_2845 on theBenchmark for (2845ds/15851Mi) % 169.84/24.29 % (381184)Instruction limit reached! % 169.84/24.29 % (381184)------------------------------ % 169.84/24.29 % (381184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.29 % (381184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.29 % (381184)CaDiCaL version: 2.1.3 % 169.84/24.29 % (381184)Termination reason: Instruction limit % 169.84/24.29 % (381184)Termination phase: Saturation % 169.84/24.29 % (381184)Time elapsed: 12.959 s % 169.84/24.29 % (381184)Peak memory usage: 23 MB % 169.84/24.29 % (381184)Instructions burned: 22565 (million) % 169.84/24.29 % (381404)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4100525143:avsq=on:i=17627:add=on:amm=off_2812 on theBenchmark for (2812ds/17627Mi) % 217.40/30.92 % (381401)Instruction limit reached! % 217.40/30.92 % (381401)------------------------------ % 217.40/30.92 % (381401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381401)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381401)Termination reason: Instruction limit % 217.40/30.92 % (381401)Termination phase: Saturation % 217.40/30.92 % (381401)Time elapsed: 4.382 s % 217.40/30.92 % (381401)Peak memory usage: 95 MB % 217.40/30.92 % (381401)Instructions burned: 15853 (million) % 217.40/30.92 % (381406)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1036049434:s2a=on:i=53295_2801 on theBenchmark for (2801ds/53295Mi) % 217.40/30.92 % (381399)Instruction limit reached! % 217.40/30.92 % (381399)------------------------------ % 217.40/30.92 % (381399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381399)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381399)Termination reason: Instruction limit % 217.40/30.92 % (381399)Termination phase: Saturation % 217.40/30.92 % (381399)Time elapsed: 8.917 s % 217.40/30.92 % (381399)Peak memory usage: 81 MB % 217.40/30.92 % (381399)Instructions burned: 14135 (million) % 217.40/30.92 % (381408)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1919166445:i=26857:ins=20_2767 on theBenchmark for (2767ds/26857Mi) % 217.40/30.92 % (381408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.40/30.92 % (381408)Terminated due to inappropriate strategy. % 217.40/30.92 % (381408)------------------------------ % 217.40/30.92 % (381408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381408)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381408)Termination reason: Inappropriate % 217.40/30.92 % (381408)Time elapsed: 0.007 s % 217.40/30.92 % (381408)Peak memory usage: 11 MB % 217.40/30.92 % (381408)Instructions burned: 12 (million) % 217.40/30.92 % (381408)------------------------------ % 217.40/30.92 % (381408)------------------------------ % 217.40/30.92 % (381410)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1238483526:i=28120:bs=on:fsr=off_2767 on theBenchmark for (2767ds/28120Mi) % 217.40/30.92 % (381215)Instruction limit reached! % 217.40/30.92 % (381215)------------------------------ % 217.40/30.92 % (381215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381215)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381215)Termination reason: Instruction limit % 217.40/30.92 % (381215)Termination phase: Saturation % 217.40/30.92 % (381215)Time elapsed: 14.710 s % 217.40/30.92 % (381215)Peak memory usage: 81 MB % 217.40/30.92 % (381215)Instructions burned: 20140 (million) % 217.40/30.92 % (381412)fmb+10_1_sil=256000:fmbss=7:random_seed=3167351981:fmbsr=1.6:i=182295_2762 on theBenchmark for (2762ds/182295Mi) % 217.40/30.92 % (381412)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.40/30.92 % (381412)Terminated due to inappropriate strategy. % 217.40/30.92 % (381412)------------------------------ % 217.40/30.92 % (381412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381412)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381412)Termination reason: Inappropriate % 217.40/30.92 % (381412)Time elapsed: 0.007 s % 217.40/30.92 % (381412)Peak memory usage: 11 MB % 217.40/30.92 % (381412)Instructions burned: 12 (million) % 217.40/30.92 % (381412)------------------------------ % 217.40/30.92 % (381412)------------------------------ % 217.40/30.92 % (381414)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1058055218:i=44625:gsp=on_2761 on theBenchmark for (2761ds/44625Mi) % 217.40/30.92 % (381414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.40/30.92 % (381414)Terminated due to inappropriate strategy. % 217.40/30.92 % (381414)------------------------------ % 217.40/30.92 % (381414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.40/30.92 % (381414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.40/30.92 % (381414)CaDiCaL version: 2.1.3 % 217.40/30.92 % (381414)Termination reason: Inappropriate % 228.04/32.46 % (381414)Time elapsed: 0.007 s % 228.04/32.46 % (381414)Peak memory usage: 11 MB % 228.04/32.46 % (381414)Instructions burned: 13 (million) % 228.04/32.46 % (381414)------------------------------ % 228.04/32.46 % (381414)------------------------------ % 228.04/32.46 % (381416)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2500993187:i=160505_2761 on theBenchmark for (2761ds/160505Mi) % 228.04/32.46 % (381416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.04/32.46 % (381416)Terminated due to inappropriate strategy. % 228.04/32.46 % (381416)------------------------------ % 228.04/32.46 % (381416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.04/32.46 % (381416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.04/32.46 % (381416)CaDiCaL version: 2.1.3 % 228.04/32.46 % (381416)Termination reason: Inappropriate % 228.04/32.46 % (381416)Time elapsed: 0.007 s % 228.04/32.46 % (381416)Peak memory usage: 11 MB % 228.04/32.46 % (381416)Instructions burned: 12 (million) % 228.04/32.46 % (381416)------------------------------ % 228.04/32.46 % (381416)------------------------------ % 228.04/32.46 % (381418)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=597608417:fmbsr=1.3:i=225729_2761 on theBenchmark for (2761ds/225729Mi) % 228.04/32.47 % (381418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.04/32.47 % (381418)Terminated due to inappropriate strategy. % 228.04/32.47 % (381418)------------------------------ % 228.04/32.47 % (381418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.04/32.47 % (381418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.04/32.47 % (381418)CaDiCaL version: 2.1.3 % 228.04/32.47 % (381418)Termination reason: Inappropriate % 228.04/32.47 % (381418)Time elapsed: 0.007 s % 228.04/32.47 % (381418)Peak memory usage: 11 MB % 228.04/32.47 % (381418)Instructions burned: 13 (million) % 228.04/32.47 % (381418)------------------------------ % 228.04/32.47 % (381418)------------------------------ % 228.04/32.47 % (381420)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1670058294:fmbsr=2:i=185024:ins=7_2760 on theBenchmark for (2760ds/185024Mi) % 228.04/32.47 % (381420)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.04/32.47 % (381420)Terminated due to inappropriate strategy. % 228.04/32.47 % (381420)------------------------------ % 228.04/32.47 % (381420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.04/32.47 % (381420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.04/32.47 % (381420)CaDiCaL version: 2.1.3 % 228.04/32.47 % (381420)Termination reason: Inappropriate % 228.04/32.47 % (381420)Time elapsed: 0.007 s % 228.04/32.47 % (381420)Peak memory usage: 11 MB % 228.04/32.47 % (381420)Instructions burned: 13 (million) % 228.04/32.47 % (381172)Instruction limit reached! % 228.04/32.47 % (381172)------------------------------ % 228.04/32.47 % (381172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.04/32.47 % (381172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.04/32.47 % (381172)CaDiCaL version: 2.1.3 % 228.04/32.47 % (381172)Termination reason: Instruction limit % 228.04/32.47 % (381172)Termination phase: Saturation % 228.04/32.47 % (381172)Time elapsed: 19.536 s % 228.04/32.47 % (381172)Peak memory usage: 919 MB % 228.04/32.47 % (381172)Instructions burned: 29341 (million) % 228.04/32.47 % (381420)------------------------------ % 228.04/32.47 % (381420)------------------------------ % 228.04/32.47 % (381422)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=373941642:rtra=on_2760 on theBenchmark for (2760ds/0Mi) % 228.04/32.47 % (381422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.04/32.47 % (381422)Terminated due to inappropriate strategy. % 228.04/32.47 % (381422)------------------------------ % 228.04/32.47 % (381422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.04/32.47 % (381422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.04/32.47 % (381422)CaDiCaL version: 2.1.3 % 228.04/32.47 % (381422)Termination reason: Inappropriate % 228.04/32.47 % (381422)Time elapsed: 0.010 s % 228.04/32.47 % (381422)Peak memory usage: 11 MB % 228.04/32.47 % (381422)Instructions burned: 17 (million) % 228.04/32.47 % (381422)------------------------------ % 228.04/32.47 % (381422)------------------------------ % 228.04/32.47 % (381424)% WARNING: option uhcvi not known. % 228.04/32.47 % (381424)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=243944436:i=271062:add=off:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/271062Mi) % 235.67/33.59 % (381426)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2372087907:i=176048:add=on:rtra=on:rawr=on_2759 on theBenchmark for (2759ds/176048Mi) % 235.67/33.59 % (381404)Instruction limit reached! % 235.67/33.59 % (381404)------------------------------ % 235.67/33.59 % (381404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381404)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381404)Termination reason: Instruction limit % 235.67/33.59 % (381404)Termination phase: Saturation % 235.67/33.59 % (381404)Time elapsed: 11.116 s % 235.67/33.59 % (381404)Peak memory usage: 88 MB % 235.67/33.59 % (381404)Instructions burned: 17628 (million) % 235.67/33.59 % (381771)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2168863633:i=206:fgj=on:rtra=on_2701 on theBenchmark for (2701ds/206Mi) % 235.67/33.59 % (381771)Instruction limit reached! % 235.67/33.59 % (381771)------------------------------ % 235.67/33.59 % (381771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381771)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381771)Termination reason: Instruction limit % 235.67/33.59 % (381771)Termination phase: Saturation % 235.67/33.59 % (381771)Time elapsed: 0.125 s % 235.67/33.59 % (381771)Peak memory usage: 13 MB % 235.67/33.59 % (381771)Instructions burned: 206 (million) % 235.67/33.59 % (381773)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1655669251:i=232:rtra=on_2700 on theBenchmark for (2700ds/232Mi) % 235.67/33.59 % (381773)Instruction limit reached! % 235.67/33.59 % (381773)------------------------------ % 235.67/33.59 % (381773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381773)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381773)Termination reason: Instruction limit % 235.67/33.59 % (381773)Termination phase: Saturation % 235.67/33.59 % (381773)Time elapsed: 0.148 s % 235.67/33.59 % (381773)Peak memory usage: 15 MB % 235.67/33.59 % (381773)Instructions burned: 232 (million) % 235.67/33.59 % (381775)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3401540948:i=262:rtra=on_2698 on theBenchmark for (2698ds/262Mi) % 235.67/33.59 % (381775)Instruction limit reached! % 235.67/33.59 % (381775)------------------------------ % 235.67/33.59 % (381775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381775)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381775)Termination reason: Instruction limit % 235.67/33.59 % (381775)Termination phase: Saturation % 235.67/33.59 % (381775)Time elapsed: 0.156 s % 235.67/33.59 % (381775)Peak memory usage: 14 MB % 235.67/33.59 % (381775)Instructions burned: 263 (million) % 235.67/33.59 % (381777)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3171811403:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2696 on theBenchmark for (2696ds/318Mi) % 235.67/33.59 % (381777)Instruction limit reached! % 235.67/33.59 % (381777)------------------------------ % 235.67/33.59 % (381777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381777)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381777)Termination reason: Instruction limit % 235.67/33.59 % (381777)Termination phase: Saturation % 235.67/33.59 % (381777)Time elapsed: 0.222 s % 235.67/33.59 % (381777)Peak memory usage: 16 MB % 235.67/33.59 % (381777)Instructions burned: 319 (million) % 235.67/33.59 % (381779)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3117407358:i=1428:nm=2:rtra=on_2694 on theBenchmark for (2694ds/1428Mi) % 235.67/33.59 % (381779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.67/33.59 % (381779)Terminated due to inappropriate strategy. % 235.67/33.59 % (381779)------------------------------ % 235.67/33.59 % (381779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.67/33.59 % (381779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.67/33.59 % (381779)CaDiCaL version: 2.1.3 % 235.67/33.59 % (381779)Termination reason: Inappropriate % 235.67/33.59 % (381779)Time elapsed: 0.008 s % 235.67/33.59 % (381779)Peak memory usage: 11 MB % 235.67/33.59 % (381779)Instructions burned: 14 (million) % 235.67/33.59 % (381779)------------------------------ % 244.46/34.95 % (381779)------------------------------ % 244.46/34.95 % (381781)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=506685940:i=262:bd=preordered:rtra=on:fsd=on_2693 on theBenchmark for (2693ds/262Mi) % 244.46/34.95 % (381781)Instruction limit reached! % 244.46/34.95 % (381781)------------------------------ % 244.46/34.95 % (381781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381781)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381781)Termination reason: Instruction limit % 244.46/34.95 % (381781)Termination phase: Saturation % 244.46/34.95 % (381781)Time elapsed: 0.177 s % 244.46/34.95 % (381781)Peak memory usage: 14 MB % 244.46/34.95 % (381781)Instructions burned: 264 (million) % 244.46/34.95 % (381783)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=570140385:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2691 on theBenchmark for (2691ds/1368Mi) % 244.46/34.95 % (381410)Instruction limit reached! % 244.46/34.95 % (381410)------------------------------ % 244.46/34.95 % (381410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381410)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381410)Termination reason: Instruction limit % 244.46/34.95 % (381410)Termination phase: Saturation % 244.46/34.95 % (381410)Time elapsed: 8.105 s % 244.46/34.95 % (381410)Peak memory usage: 16 MB % 244.46/34.95 % (381410)Instructions burned: 28122 (million) % 244.46/34.95 % (381785)ott-21_1_sil=16000:si=on:fs=off:random_seed=2215753394:i=360:av=off:fsr=off:rtra=on_2685 on theBenchmark for (2685ds/360Mi) % 244.46/34.95 % (381783)Instruction limit reached! % 244.46/34.95 % (381783)------------------------------ % 244.46/34.95 % (381783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381783)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381783)Termination reason: Instruction limit % 244.46/34.95 % (381783)Termination phase: Saturation % 244.46/34.95 % (381783)Time elapsed: 0.683 s % 244.46/34.95 % (381783)Peak memory usage: 19 MB % 244.46/34.95 % (381783)Instructions burned: 1369 (million) % 244.46/34.95 % (381787)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=705096780:i=954:bd=all:rtra=on_2684 on theBenchmark for (2684ds/954Mi) % 244.46/34.95 % (381785)Instruction limit reached! % 244.46/34.95 % (381785)------------------------------ % 244.46/34.95 % (381785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381785)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381785)Termination reason: Instruction limit % 244.46/34.95 % (381785)Termination phase: Saturation % 244.46/34.95 % (381785)Time elapsed: 0.195 s % 244.46/34.95 % (381785)Peak memory usage: 14 MB % 244.46/34.95 % (381785)Instructions burned: 360 (million) % 244.46/34.95 % (381789)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=632680285:fmbsr=1.3:i=1730:ins=25:rtra=on_2683 on theBenchmark for (2683ds/1730Mi) % 244.46/34.95 % (381789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.46/34.95 % (381789)Terminated due to inappropriate strategy. % 244.46/34.95 % (381789)------------------------------ % 244.46/34.95 % (381789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381789)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381789)Termination reason: Inappropriate % 244.46/34.95 % (381789)Time elapsed: 0.008 s % 244.46/34.95 % (381789)Peak memory usage: 11 MB % 244.46/34.95 % (381789)Instructions burned: 14 (million) % 244.46/34.95 % (381789)------------------------------ % 244.46/34.95 % (381789)------------------------------ % 244.46/34.95 % (381791)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2213255171:i=2358:rtra=on_2683 on theBenchmark for (2683ds/2358Mi) % 244.46/34.95 % (381787)Instruction limit reached! % 244.46/34.95 % (381787)------------------------------ % 244.46/34.95 % (381787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.46/34.95 % (381787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/34.95 % (381787)CaDiCaL version: 2.1.3 % 244.46/34.95 % (381787)Termination reason: Instruction limit % 244.46/34.95 % (381787)Termination phase: Saturation % 279.11/39.64 % (381787)Time elapsed: 0.607 s % 279.11/39.64 % (381787)Peak memory usage: 17 MB % 279.11/39.64 % (381787)Instructions burned: 955 (million) % 279.11/39.64 % (381793)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3274367751:i=1778:ins=1:rtra=on_2678 on theBenchmark for (2678ds/1778Mi) % 279.11/39.64 % (381793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.11/39.64 % (381793)Terminated due to inappropriate strategy. % 279.11/39.64 % (381793)------------------------------ % 279.11/39.64 % (381793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.11/39.64 % (381793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/39.64 % (381793)CaDiCaL version: 2.1.3 % 279.11/39.64 % (381793)Termination reason: Inappropriate % 279.11/39.64 % (381793)Time elapsed: 0.008 s % 279.11/39.64 % (381793)Peak memory usage: 11 MB % 279.11/39.64 % (381793)Instructions burned: 14 (million) % 279.11/39.64 % (381793)------------------------------ % 279.11/39.64 % (381793)------------------------------ % 279.11/39.64 % (381795)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=850414782:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/1384Mi) % 279.11/39.64 % (381795)Instruction limit reached! % 279.11/39.64 % (381795)------------------------------ % 279.11/39.64 % (381795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.11/39.64 % (381795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/39.64 % (381795)CaDiCaL version: 2.1.3 % 279.11/39.64 % (381795)Termination reason: Instruction limit % 279.11/39.64 % (381795)Termination phase: Saturation % 279.11/39.64 % (381795)Time elapsed: 0.785 s % 279.11/39.64 % (381795)Peak memory usage: 28 MB % 279.11/39.64 % (381795)Instructions burned: 1384 (million) % 279.11/39.64 % (381797)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3333170954:i=1758:kws=inv_precedence:fsr=off:rtra=on_2670 on theBenchmark for (2670ds/1758Mi) % 279.11/39.64 % (381791)Instruction limit reached! % 279.11/39.64 % (381791)------------------------------ % 279.11/39.64 % (381791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.11/39.64 % (381791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/39.64 % (381791)CaDiCaL version: 2.1.3 % 279.11/39.64 % (381791)Termination reason: Instruction limit % 279.11/39.64 % (381791)Termination phase: Saturation % 279.11/39.64 % (381791)Time elapsed: 1.514 s % 279.11/39.64 % (381791)Peak memory usage: 28 MB % 279.11/39.64 % (381791)Instructions burned: 2358 (million) % 279.11/39.64 % (381799)fmb+10_1_sil=64000:si=on:random_seed=2837631503:i=44122:nm=2:rtra=on:gsp=on_2667 on theBenchmark for (2667ds/44122Mi) % 279.11/39.64 % (381799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.11/39.64 % (381799)Terminated due to inappropriate strategy. % 279.11/39.64 % (381799)------------------------------ % 279.11/39.64 % (381799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.11/39.64 % (381799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/39.64 % (381799)CaDiCaL version: 2.1.3 % 279.11/39.64 % (381799)Termination reason: Inappropriate % 279.11/39.64 % (381799)Time elapsed: 0.008 s % 279.11/39.64 % (381799)Peak memory usage: 11 MB % 279.11/39.64 % (381799)Instructions burned: 15 (million) % 279.11/39.64 % (381799)------------------------------ % 279.11/39.64 % (381799)------------------------------ % 279.11/39.64 % (381801)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=983514144:i=19030:nm=5:rtra=on_2667 on theBenchmark for (2667ds/19030Mi) % 279.11/39.64 % (381801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.11/39.64 % (381801)Terminated due to inappropriate strategy. % 279.11/39.64 % (381801)------------------------------ % 279.11/39.64 % (381801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.11/39.64 % (381801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/39.64 % (381801)CaDiCaL version: 2.1.3 % 279.11/39.64 % (381801)Termination reason: Inappropriate % 279.11/39.64 % (381801)Time elapsed: 0.008 s % 279.11/39.64 % (381801)Peak memory usage: 11 MB % 279.11/39.64 % (381801)Instructions burned: 14 (million) % 279.11/39.64 % (381801)------------------------------ % 279.11/39.64 % (381801)------------------------------ % 279.11/39.64 % (381803)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=158696363:fmbsr=1.7:i=1840:rtra=on_2667 on theBenchmark for (2667ds/1840Mi) % 300.43/42.64 % (381803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.64 % (381803)Terminated due to inappropriate strategy. % 300.43/42.64 % (381803)------------------------------ % 300.43/42.64 % (381803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (381803)CaDiCaL version: 2.1.3 % 300.43/42.64 % (381803)Termination reason: Inappropriate % 300.43/42.64 % (381803)Time elapsed: 0.008 s % 300.43/42.64 % (381803)Peak memory usage: 11 MB % 300.43/42.64 % (381803)Instructions burned: 14 (million) % 300.43/42.64 % (381803)------------------------------ % 300.43/42.64 % (381803)------------------------------ % 300.43/42.64 % (381805)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2548793627:i=10262:rtra=on_2667 on theBenchmark for (2667ds/10262Mi) % 300.43/42.64 % (381406)Instruction limit reached! % 300.43/42.64 % (381406)------------------------------ % 300.43/42.64 % (381406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (381406)CaDiCaL version: 2.1.3 % 300.43/42.64 % (381406)Termination reason: Instruction limit % 300.43/42.64 % (381406)Termination phase: Saturation % 300.43/42.64 % (381406)Time elapsed: 13.878 s % 300.43/42.64 % (381406)Peak memory usage: 472 MB % 300.43/42.64 % (381406)Instructions burned: 53298 (million) % 300.43/42.64 % (381807)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1889677363:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2662 on theBenchmark for (2662ds/2944Mi) % 300.43/42.64 % (381797)Instruction limit reached! % 300.43/42.64 % (381797)------------------------------ % 300.43/42.64 % (381797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (381797)CaDiCaL version: 2.1.3 % 300.43/42.64 % (381797)Termination reason: Instruction limit % 300.43/42.64 % (381797)Termination phase: Saturation % 300.43/42.64 % (381797)Time elapsed: 1.005 s % 300.43/42.64 % (381797)Peak memory usage: 24 MB % 300.43/42.64 % (381797)Instructions burned: 1760 (million) % 300.43/42.64 % (381809)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=877452229:i=12648:rtra=on_2659 on theBenchmark for (2659ds/12648Mi) % 300.43/42.64 % (381809)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.64 % (381809)Terminated due to inappropriate strategy. % 300.43/42.64 % (381809)------------------------------ % 300.43/42.64 % (381809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (381809)CaDiCaL version: 2.1.3 % 300.43/42.64 % (381809)Termination reason: Inappropriate % 300.43/42.64 % (381809)Time elapsed: 0.009 s % 300.43/42.64 % (381809)Peak memory usage: 11 MB % 300.43/42.64 % (381809)Instructions burned: 17 (million) % 300.43/42.64 % (381809)------------------------------ % 300.43/42.64 % (381809)------------------------------ % 300.43/42.64 % (381811)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2924146794:fmbsr=2.30978:i=4348:rtra=on_2659 on theBenchmark for (2659ds/4348Mi) % 300.43/42.64 % (381811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.64 % (381811)Terminated due to inappropriate strategy. % 300.43/42.64 % (381811)------------------------------ % 300.43/42.64 % (381811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (381811)CaDiCaL version: 2.1.3 % 300.43/42.64 % (381811)Termination reason: Inappropriate % 300.43/42.64 % (381811)Time elapsed: 0.008 s % 300.43/42.64 % (381811)Peak memory usage: 11 MB % 300.43/42.64 % (381811)Instructions burned: 14 (million) % 300.43/42.64 % (381811)------------------------------ % 300.43/42.64 % (381811)------------------------------ % 300.43/42.64 % (381813)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=196191017:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2659 on theBenchmark for (2659ds/1738Mi) % 300.43/42.64 % (381807)Instruction limit reached! % 300.43/42.64 % (381807)------------------------------ % 300.43/42.64 % (381807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (381807)Linked with Z3 4.14.0.0 3c47fd96cf5 % 300.43/42.64 Terminated % 300.43/42.64 % Vampire exiting % 300.43/42.64 Terminated %------------------------------------------------------------------------------