%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW036_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:38:33 PM UTC 2026 % Result : Timeout 300.71s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW036_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n006.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 13:09:25 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.82/0.86 % (3952061)Will run a generic schedule for satisfiability detection. % 3.82/0.86 % (3952079)% WARNING: option uhcvi not known. % 3.82/0.86 % (3952079)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2601141808:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.82/0.86 % (3952078)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=675704343_2999 on theBenchmark for (2999ds/0Mi) % 3.82/0.86 % (3952082)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1122684701:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.82/0.86 % (3952080)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2666084757:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.82/0.86 % (3952081)dis+10_1_sil=32000:sp=arity:random_seed=712374314:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.82/0.86 % (3952083)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4132797776:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.82/0.86 % (3952084)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4260928068:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.82/0.86 % (3952078)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.82/0.86 % (3952078)Terminated due to inappropriate strategy. % 3.82/0.86 % (3952078)------------------------------ % 3.82/0.86 % (3952078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/0.86 % (3952078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/0.86 % (3952078)CaDiCaL version: 2.1.3 % 3.82/0.86 % (3952078)Termination reason: Inappropriate % 3.82/0.86 % (3952078)Time elapsed: 0.034 s % 3.82/0.86 % (3952078)Peak memory usage: 13 MB % 3.82/0.86 % (3952078)Instructions burned: 79 (million) % 3.82/0.86 % (3952078)------------------------------ % 3.82/0.86 % (3952078)------------------------------ % 3.82/0.86 % (3952081)Instruction limit reached! % 3.82/0.86 % (3952081)------------------------------ % 3.82/0.86 % (3952081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/0.86 % (3952081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/0.86 % (3952081)CaDiCaL version: 2.1.3 % 3.82/0.86 % (3952081)Termination reason: Instruction limit % 3.82/0.86 % (3952081)Termination phase: Saturation % 3.82/0.86 % (3952081)Time elapsed: 0.045 s % 3.82/0.86 % (3952081)Peak memory usage: 14 MB % 3.82/0.86 % (3952081)Instructions burned: 103 (million) % 3.82/0.86 % (3952082)Instruction limit reached! % 3.82/0.86 % (3952082)------------------------------ % 3.82/0.86 % (3952082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/0.86 % (3952082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/0.86 % (3952082)CaDiCaL version: 2.1.3 % 3.82/0.86 % (3952082)Termination reason: Instruction limit % 3.82/0.86 % (3952082)Termination phase: Saturation % 3.82/0.86 % (3952082)Time elapsed: 0.052 s % 3.82/0.86 % (3952082)Peak memory usage: 15 MB % 3.82/0.86 % (3952082)Instructions burned: 118 (million) % 3.82/0.86 % (3952083)Instruction limit reached! % 3.82/0.86 % (3952083)------------------------------ % 3.82/0.86 % (3952083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/0.86 % (3952083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/0.86 % (3952083)CaDiCaL version: 2.1.3 % 3.82/0.86 % (3952083)Termination reason: Instruction limit % 3.82/0.86 % (3952083)Termination phase: Saturation % 3.82/0.86 % (3952083)Time elapsed: 0.055 s % 3.82/0.86 % (3952083)Peak memory usage: 14 MB % 3.82/0.86 % (3952083)Instructions burned: 131 (million) % 3.82/0.86 % (3952109)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3924394862:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.82/0.86 % (3952117)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1002756606:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.82/0.86 % (3952084)Instruction limit reached! % 3.82/0.86 % (3952084)------------------------------ % 3.82/0.86 % (3952084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/0.86 % (3952084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/0.86 % (3952084)CaDiCaL version: 2.1.3 % 3.82/0.86 % (3952084)Termination reason: Instruction limit % 3.82/0.86 % (3952084)Termination phase: Saturation % 3.82/0.86 % (3952084)Time elapsed: 0.066 s % 3.82/0.86 % (3952084)Peak memory usage: 15 MB % 3.82/0.86 % (3952084)Instructions burned: 161 (million) % 5.57/1.06 % (3952122)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=3728244214:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.57/1.06 % (3952127)ott-21_1_sil=16000:fs=off:random_seed=3003246169:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.57/1.06 % (3952135)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2530585940:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.57/1.06 % (3952109)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.57/1.06 % (3952109)Terminated due to inappropriate strategy. % 5.57/1.06 % (3952109)------------------------------ % 5.57/1.06 % (3952109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.06 % (3952109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.06 % (3952109)CaDiCaL version: 2.1.3 % 5.57/1.06 % (3952109)Termination reason: Inappropriate % 5.57/1.06 % (3952109)Time elapsed: 0.034 s % 5.57/1.06 % (3952109)Peak memory usage: 13 MB % 5.57/1.06 % (3952109)Instructions burned: 79 (million) % 5.57/1.06 % (3952109)------------------------------ % 5.57/1.06 % (3952109)------------------------------ % 5.57/1.06 % (3952146)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=6975965:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.57/1.06 % (3952117)Instruction limit reached! % 5.57/1.06 % (3952117)------------------------------ % 5.57/1.06 % (3952117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.06 % (3952117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.06 % (3952117)CaDiCaL version: 2.1.3 % 5.57/1.06 % (3952117)Termination reason: Instruction limit % 5.57/1.06 % (3952117)Termination phase: Saturation % 5.57/1.06 % (3952117)Time elapsed: 0.055 s % 5.57/1.06 % (3952117)Peak memory usage: 15 MB % 5.57/1.06 % (3952117)Instructions burned: 132 (million) % 5.57/1.06 % (3952151)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1682889120:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.57/1.06 % (3952146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.57/1.06 % (3952146)Terminated due to inappropriate strategy. % 5.57/1.06 % (3952146)------------------------------ % 5.57/1.06 % (3952146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.06 % (3952146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.06 % (3952146)CaDiCaL version: 2.1.3 % 5.57/1.06 % (3952146)Termination reason: Inappropriate % 5.57/1.06 % (3952146)Time elapsed: 0.033 s % 5.57/1.06 % (3952146)Peak memory usage: 13 MB % 5.57/1.06 % (3952146)Instructions burned: 78 (million) % 5.57/1.06 % (3952146)------------------------------ % 5.57/1.06 % (3952146)------------------------------ % 5.57/1.06 % (3952127)Instruction limit reached! % 5.57/1.06 % (3952127)------------------------------ % 5.57/1.06 % (3952127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.06 % (3952127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.06 % (3952127)CaDiCaL version: 2.1.3 % 5.57/1.06 % (3952127)Termination reason: Instruction limit % 5.57/1.06 % (3952127)Termination phase: Saturation % 5.57/1.06 % (3952127)Time elapsed: 0.086 s % 5.57/1.06 % (3952127)Peak memory usage: 15 MB % 5.57/1.06 % (3952127)Instructions burned: 182 (million) % 5.57/1.06 % (3952153)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=529193156:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.57/1.06 % (3952154)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=1724424654: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) % 5.57/1.06 % (3952153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.57/1.06 % (3952153)Terminated due to inappropriate strategy. % 5.57/1.06 % (3952153)------------------------------ % 5.57/1.06 % (3952153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.06 % (3952153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.06 % (3952153)CaDiCaL version: 2.1.3 % 5.57/1.06 % (3952153)Termination reason: Inappropriate % 5.57/1.06 % (3952153)Time elapsed: 0.048 s % 5.57/1.06 % (3952153)Peak memory usage: 15 MB % 18.28/2.96 % (3952153)Instructions burned: 110 (million) % 18.28/2.96 % (3952153)------------------------------ % 18.28/2.96 % (3952153)------------------------------ % 18.28/2.96 % (3952157)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1924975322:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.28/2.96 % (3952135)Instruction limit reached! % 18.28/2.96 % (3952135)------------------------------ % 18.28/2.96 % (3952135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.28/2.96 % (3952135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/2.96 % (3952135)CaDiCaL version: 2.1.3 % 18.28/2.96 % (3952135)Termination reason: Instruction limit % 18.28/2.96 % (3952135)Termination phase: Saturation % 18.28/2.96 % (3952135)Time elapsed: 0.258 s % 18.28/2.96 % (3952135)Peak memory usage: 17 MB % 18.28/2.96 % (3952135)Instructions burned: 477 (million) % 18.28/2.96 % (3952159)fmb+10_1_sil=64000:random_seed=927717167:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.28/2.96 % (3952122)Instruction limit reached! % 18.28/2.96 % (3952122)------------------------------ % 18.28/2.96 % (3952122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.28/2.96 % (3952122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/2.96 % (3952122)CaDiCaL version: 2.1.3 % 18.28/2.96 % (3952122)Termination reason: Instruction limit % 18.28/2.96 % (3952122)Termination phase: Saturation % 18.28/2.96 % (3952122)Time elapsed: 0.325 s % 18.28/2.96 % (3952122)Peak memory usage: 19 MB % 18.28/2.96 % (3952122)Instructions burned: 684 (million) % 18.28/2.96 % (3952159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.28/2.96 % (3952159)Terminated due to inappropriate strategy. % 18.28/2.96 % (3952159)------------------------------ % 18.28/2.96 % (3952159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.28/2.96 % (3952159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/2.96 % (3952159)CaDiCaL version: 2.1.3 % 18.28/2.96 % (3952159)Termination reason: Inappropriate % 18.28/2.96 % (3952159)Time elapsed: 0.038 s % 18.28/2.96 % (3952159)Peak memory usage: 13 MB % 18.28/2.96 % (3952159)Instructions burned: 87 (million) % 18.28/2.96 % (3952159)------------------------------ % 18.28/2.96 % (3952159)------------------------------ % 18.28/2.96 % (3952161)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=767725418:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.28/2.96 % (3952162)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1955062672:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.28/2.96 % (3952161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.28/2.96 % (3952161)Terminated due to inappropriate strategy. % 18.28/2.96 % (3952161)------------------------------ % 18.28/2.96 % (3952161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.28/2.96 % (3952161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/2.96 % (3952161)CaDiCaL version: 2.1.3 % 18.28/2.96 % (3952161)Termination reason: Inappropriate % 18.28/2.96 % (3952161)Time elapsed: 0.033 s % 18.28/2.96 % (3952161)Peak memory usage: 13 MB % 18.28/2.96 % (3952161)Instructions burned: 79 (million) % 18.28/2.96 % (3952161)------------------------------ % 18.28/2.96 % (3952161)------------------------------ % 18.28/2.96 % (3952162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.28/2.96 % (3952162)Terminated due to inappropriate strategy. % 18.28/2.96 % (3952162)------------------------------ % 18.28/2.96 % (3952162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.28/2.96 % (3952162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/2.96 % (3952162)CaDiCaL version: 2.1.3 % 18.28/2.96 % (3952162)Termination reason: Inappropriate % 18.28/2.96 % (3952162)Time elapsed: 0.033 s % 18.28/2.96 % (3952162)Peak memory usage: 13 MB % 18.28/2.96 % (3952162)Instructions burned: 79 (million) % 18.28/2.96 % (3952162)------------------------------ % 18.28/2.96 % (3952162)------------------------------ % 18.28/2.96 % (3952165)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3155617359:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 18.28/2.96 % (3952166)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=891775666:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 18.28/2.96 % (3952154)Instruction limit reached! % 18.28/2.96 % (3952154)------------------------------ % 25.65/3.96 % (3952154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952154)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952154)Termination reason: Instruction limit % 25.65/3.96 % (3952154)Termination phase: Saturation % 25.65/3.96 % (3952154)Time elapsed: 0.398 s % 25.65/3.96 % (3952154)Peak memory usage: 22 MB % 25.65/3.96 % (3952154)Instructions burned: 693 (million) % 25.65/3.96 % (3952169)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1758050306:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 25.65/3.96 % (3952169)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.65/3.96 % (3952169)Terminated due to inappropriate strategy. % 25.65/3.96 % (3952169)------------------------------ % 25.65/3.96 % (3952169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952169)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952169)Termination reason: Inappropriate % 25.65/3.96 % (3952169)Time elapsed: 0.033 s % 25.65/3.96 % (3952169)Peak memory usage: 13 MB % 25.65/3.96 % (3952169)Instructions burned: 79 (million) % 25.65/3.96 % (3952169)------------------------------ % 25.65/3.96 % (3952169)------------------------------ % 25.65/3.96 % (3952171)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3370902227:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 25.65/3.96 % (3952151)Instruction limit reached! % 25.65/3.96 % (3952151)------------------------------ % 25.65/3.96 % (3952151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952151)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952151)Termination reason: Instruction limit % 25.65/3.96 % (3952151)Termination phase: Saturation % 25.65/3.96 % (3952151)Time elapsed: 0.537 s % 25.65/3.96 % (3952151)Peak memory usage: 19 MB % 25.65/3.96 % (3952151)Instructions burned: 1179 (million) % 25.65/3.96 % (3952171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.65/3.96 % (3952171)Terminated due to inappropriate strategy. % 25.65/3.96 % (3952171)------------------------------ % 25.65/3.96 % (3952171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952171)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952171)Termination reason: Inappropriate % 25.65/3.96 % (3952171)Time elapsed: 0.033 s % 25.65/3.96 % (3952171)Peak memory usage: 13 MB % 25.65/3.96 % (3952171)Instructions burned: 79 (million) % 25.65/3.96 % (3952171)------------------------------ % 25.65/3.96 % (3952171)------------------------------ % 25.65/3.96 % (3952173)ott-2_1_sil=16000:newcnf=on:random_seed=2442531425:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 25.65/3.96 % (3952174)ott+10_1_sil=32000:tgt=ground:random_seed=2317376376:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 25.65/3.96 % (3952157)Instruction limit reached! % 25.65/3.96 % (3952157)------------------------------ % 25.65/3.96 % (3952157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952157)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952157)Termination reason: Instruction limit % 25.65/3.96 % (3952157)Termination phase: Saturation % 25.65/3.96 % (3952157)Time elapsed: 0.491 s % 25.65/3.96 % (3952157)Peak memory usage: 21 MB % 25.65/3.96 % (3952157)Instructions burned: 879 (million) % 25.65/3.96 % (3952177)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1259848733:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 25.65/3.96 % (3952177)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.65/3.96 % (3952177)Terminated due to inappropriate strategy. % 25.65/3.96 % (3952177)------------------------------ % 25.65/3.96 % (3952177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.65/3.96 % (3952177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.65/3.96 % (3952177)CaDiCaL version: 2.1.3 % 25.65/3.96 % (3952177)Termination reason: Inappropriate % 25.65/3.96 % (3952177)Time elapsed: 0.033 s % 25.65/3.96 % (3952177)Peak memory usage: 13 MB % 25.65/3.96 % (3952177)Instructions burned: 79 (million) % 102.57/14.72 % (3952177)------------------------------ % 102.57/14.72 % (3952177)------------------------------ % 102.57/14.72 % (3952179)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3554605962:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 102.57/14.72 % (3952166)Instruction limit reached! % 102.57/14.72 % (3952166)------------------------------ % 102.57/14.72 % (3952166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952166)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952166)Termination reason: Instruction limit % 102.57/14.72 % (3952166)Termination phase: Saturation % 102.57/14.72 % (3952166)Time elapsed: 0.527 s % 102.57/14.72 % (3952166)Peak memory usage: 17 MB % 102.57/14.72 % (3952166)Instructions burned: 1473 (million) % 102.57/14.72 % (3952181)dis+21_1_sil=32000:sas=cadical:random_seed=3071160169:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 102.57/14.72 % (3952173)Instruction limit reached! % 102.57/14.72 % (3952173)------------------------------ % 102.57/14.72 % (3952173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952173)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952173)Termination reason: Instruction limit % 102.57/14.72 % (3952173)Termination phase: Saturation % 102.57/14.72 % (3952173)Time elapsed: 0.407 s % 102.57/14.72 % (3952173)Peak memory usage: 19 MB % 102.57/14.72 % (3952173)Instructions burned: 869 (million) % 102.57/14.72 % (3952183)ott+11_1_sil=16000:gs=on:random_seed=4237666901:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 102.57/14.72 % (3952183)Instruction limit reached! % 102.57/14.72 % (3952183)------------------------------ % 102.57/14.72 % (3952183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952183)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952183)Termination reason: Instruction limit % 102.57/14.72 % (3952183)Termination phase: Saturation % 102.57/14.72 % (3952183)Time elapsed: 0.873 s % 102.57/14.72 % (3952183)Peak memory usage: 20 MB % 102.57/14.72 % (3952183)Instructions burned: 2253 (million) % 102.57/14.72 % (3952185)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2596286372:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 102.57/14.72 % (3952185)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.57/14.72 % (3952185)Terminated due to inappropriate strategy. % 102.57/14.72 % (3952185)------------------------------ % 102.57/14.72 % (3952185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952185)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952185)Termination reason: Inappropriate % 102.57/14.72 % (3952185)Time elapsed: 0.045 s % 102.57/14.72 % (3952185)Peak memory usage: 13 MB % 102.57/14.72 % (3952185)Instructions burned: 107 (million) % 102.57/14.72 % (3952185)------------------------------ % 102.57/14.72 % (3952185)------------------------------ % 102.57/14.72 % (3952187)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2176033154:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 102.57/14.72 % (3952179)Instruction limit reached! % 102.57/14.72 % (3952179)------------------------------ % 102.57/14.72 % (3952179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952179)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952179)Termination reason: Instruction limit % 102.57/14.72 % (3952179)Termination phase: Saturation % 102.57/14.72 % (3952179)Time elapsed: 1.816 s % 102.57/14.72 % (3952179)Peak memory usage: 31 MB % 102.57/14.72 % (3952179)Instructions burned: 3513 (million) % 102.57/14.72 % (3952190)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2519649066:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 102.57/14.72 % (3952181)Instruction limit reached! % 102.57/14.72 % (3952181)------------------------------ % 102.57/14.72 % (3952181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.57/14.72 % (3952181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.57/14.72 % (3952181)CaDiCaL version: 2.1.3 % 102.57/14.72 % (3952181)Termination reason: Instruction limit % 136.00/19.42 % (3952181)Termination phase: Saturation % 136.00/19.42 % (3952181)Time elapsed: 1.653 s % 136.00/19.42 % (3952181)Peak memory usage: 23 MB % 136.00/19.42 % (3952181)Instructions burned: 3774 (million) % 136.00/19.42 % (3952192)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4045742327:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 136.00/19.42 % (3952165)Instruction limit reached! % 136.00/19.42 % (3952165)------------------------------ % 136.00/19.42 % (3952165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.00/19.42 % (3952165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.00/19.42 % (3952165)CaDiCaL version: 2.1.3 % 136.00/19.42 % (3952165)Termination reason: Instruction limit % 136.00/19.42 % (3952165)Termination phase: Saturation % 136.00/19.42 % (3952165)Time elapsed: 2.669 s % 136.00/19.42 % (3952165)Peak memory usage: 42 MB % 136.00/19.42 % (3952165)Instructions burned: 5133 (million) % 136.00/19.42 % (3952194)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=706473119:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 136.00/19.42 % (3952194)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.00/19.42 % (3952194)Terminated due to inappropriate strategy. % 136.00/19.42 % (3952194)------------------------------ % 136.00/19.42 % (3952194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.00/19.42 % (3952194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.00/19.42 % (3952194)CaDiCaL version: 2.1.3 % 136.00/19.42 % (3952194)Termination reason: Inappropriate % 136.00/19.42 % (3952194)Time elapsed: 0.034 s % 136.00/19.42 % (3952194)Peak memory usage: 13 MB % 136.00/19.42 % (3952194)Instructions burned: 79 (million) % 136.00/19.42 % (3952194)------------------------------ % 136.00/19.42 % (3952194)------------------------------ % 136.00/19.42 % (3952196)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2712683555:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 136.00/19.42 % (3952196)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.00/19.42 % (3952196)Terminated due to inappropriate strategy. % 136.00/19.42 % (3952196)------------------------------ % 136.00/19.42 % (3952196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.00/19.42 % (3952196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.00/19.42 % (3952196)CaDiCaL version: 2.1.3 % 136.00/19.42 % (3952196)Termination reason: Inappropriate % 136.00/19.42 % (3952196)Time elapsed: 0.045 s % 136.00/19.42 % (3952196)Peak memory usage: 13 MB % 136.00/19.42 % (3952196)Instructions burned: 110 (million) % 136.00/19.42 % (3952196)------------------------------ % 136.00/19.42 % (3952196)------------------------------ % 136.00/19.42 % (3952198)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3775876194:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 136.00/19.42 % (3952198)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.00/19.42 % (3952198)Terminated due to inappropriate strategy. % 136.00/19.42 % (3952198)------------------------------ % 136.00/19.42 % (3952198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.00/19.42 % (3952198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.00/19.42 % (3952198)CaDiCaL version: 2.1.3 % 136.00/19.42 % (3952198)Termination reason: Inappropriate % 136.00/19.42 % (3952198)Time elapsed: 0.045 s % 136.00/19.42 % (3952198)Peak memory usage: 13 MB % 136.00/19.42 % (3952198)Instructions burned: 110 (million) % 136.00/19.42 % (3952198)------------------------------ % 136.00/19.42 % (3952198)------------------------------ % 136.00/19.42 % (3952200)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=160532399:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 136.00/19.42 % (3952174)Instruction limit reached! % 136.00/19.42 % (3952174)------------------------------ % 136.00/19.42 % (3952174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.00/19.42 % (3952174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.00/19.42 % (3952174)CaDiCaL version: 2.1.3 % 136.00/19.42 % (3952174)Termination reason: Instruction limit % 136.00/19.42 % (3952174)Termination phase: Saturation % 136.00/19.42 % (3952174)Time elapsed: 2.949 s % 136.00/19.42 % (3952174)Peak memory usage: 32 MB % 136.00/19.42 % (3952174)Instructions burned: 5115 (million) % 136.00/19.42 % (3952202)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1253271455:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 138.10/19.73 % (3952187)Instruction limit reached! % 138.10/19.73 % (3952187)------------------------------ % 138.10/19.73 % (3952187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952187)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952187)Termination reason: Instruction limit % 138.10/19.73 % (3952187)Termination phase: Saturation % 138.10/19.73 % (3952187)Time elapsed: 2.377 s % 138.10/19.73 % (3952187)Peak memory usage: 43 MB % 138.10/19.73 % (3952187)Instructions burned: 4592 (million) % 138.10/19.73 % (3952205)dis+10_16:1_sil=16000:random_seed=788122137:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 138.10/19.73 % (3952192)Instruction limit reached! % 138.10/19.73 % (3952192)------------------------------ % 138.10/19.73 % (3952192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952192)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952192)Termination reason: Instruction limit % 138.10/19.73 % (3952192)Termination phase: Saturation % 138.10/19.73 % (3952192)Time elapsed: 2.757 s % 138.10/19.73 % (3952192)Peak memory usage: 48 MB % 138.10/19.73 % (3952192)Instructions burned: 5212 (million) % 138.10/19.73 % (3952207)ott-3_8_sil=64000:random_seed=1980423628:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 138.10/19.73 % (3952202)Instruction limit reached! % 138.10/19.73 % (3952202)------------------------------ % 138.10/19.73 % (3952202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952202)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952202)Termination reason: Instruction limit % 138.10/19.73 % (3952202)Termination phase: Saturation % 138.10/19.73 % (3952202)Time elapsed: 3.435 s % 138.10/19.73 % (3952202)Peak memory usage: 34 MB % 138.10/19.73 % (3952202)Instructions burned: 8174 (million) % 138.10/19.73 % (3952209)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1899458810:fmbsr=2:i=32576_2928 on theBenchmark for (2928ds/32576Mi) % 138.10/19.73 % (3952209)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.10/19.73 % (3952209)Terminated due to inappropriate strategy. % 138.10/19.73 % (3952209)------------------------------ % 138.10/19.73 % (3952209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952209)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952209)Termination reason: Inappropriate % 138.10/19.73 % (3952209)Time elapsed: 0.044 s % 138.10/19.73 % (3952209)Peak memory usage: 13 MB % 138.10/19.73 % (3952209)Instructions burned: 107 (million) % 138.10/19.73 % (3952209)------------------------------ % 138.10/19.73 % (3952209)------------------------------ % 138.10/19.73 % (3952211)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=151509864:i=11404_2927 on theBenchmark for (2927ds/11404Mi) % 138.10/19.73 % (3952205)Instruction limit reached! % 138.10/19.73 % (3952205)------------------------------ % 138.10/19.73 % (3952205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952205)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952205)Termination reason: Instruction limit % 138.10/19.73 % (3952205)Termination phase: Saturation % 138.10/19.73 % (3952205)Time elapsed: 4.653 s % 138.10/19.73 % (3952205)Peak memory usage: 53 MB % 138.10/19.73 % (3952205)Instructions burned: 9156 (million) % 138.10/19.73 % (3952213)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1378352888:i=14134_2907 on theBenchmark for (2907ds/14134Mi) % 138.10/19.73 % (3952200)Instruction limit reached! % 138.10/19.73 % (3952200)------------------------------ % 138.10/19.73 % (3952200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.10/19.73 % (3952200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.10/19.73 % (3952200)CaDiCaL version: 2.1.3 % 138.10/19.73 % (3952200)Termination reason: Instruction limit % 138.10/19.73 % (3952200)Termination phase: Saturation % 138.10/19.73 % (3952200)Time elapsed: 9.399 s % 138.10/19.73 % (3952200)Peak memory usage: 81 MB % 138.10/19.73 % (3952200)Instructions burned: 22565 (million) % 138.10/19.73 % (3952215)dis+33_16_sil=32000:sac=on:random_seed=3868249110:i=15851:nm=0_2871 on theBenchmark for (2871ds/15851Mi) % 138.10/19.73 % (3952211)Instruction limit reached! % 138.10/19.73 % (3952211)------------------------------ % 138.10/19.73 % (3952211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952211)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952211)Termination reason: Instruction limit % 173.49/24.77 % (3952211)Termination phase: Saturation % 173.49/24.77 % (3952211)Time elapsed: 7.233 s % 173.49/24.77 % (3952211)Peak memory usage: 47 MB % 173.49/24.77 % (3952211)Instructions burned: 11405 (million) % 173.49/24.77 % (3952342)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2072883024:avsq=on:i=17627:add=on:amm=off_2854 on theBenchmark for (2854ds/17627Mi) % 173.49/24.77 % (3952207)Instruction limit reached! % 173.49/24.77 % (3952207)------------------------------ % 173.49/24.77 % (3952207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952207)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952207)Termination reason: Instruction limit % 173.49/24.77 % (3952207)Termination phase: Saturation % 173.49/24.77 % (3952207)Time elapsed: 11.287 s % 173.49/24.77 % (3952207)Peak memory usage: 98 MB % 173.49/24.77 % (3952207)Instructions burned: 20139 (million) % 173.49/24.77 % (3952531)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=626461849:s2a=on:i=53295_2831 on theBenchmark for (2831ds/53295Mi) % 173.49/24.77 % (3952190)Instruction limit reached! % 173.49/24.77 % (3952190)------------------------------ % 173.49/24.77 % (3952190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952190)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952190)Termination reason: Instruction limit % 173.49/24.77 % (3952190)Termination phase: Saturation % 173.49/24.77 % (3952190)Time elapsed: 14.335 s % 173.49/24.77 % (3952190)Peak memory usage: 34 MB % 173.49/24.77 % (3952190)Instructions burned: 29340 (million) % 173.49/24.77 % (3952541)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=129566762:i=26857:ins=20_2829 on theBenchmark for (2829ds/26857Mi) % 173.49/24.77 % (3952541)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.49/24.77 % (3952541)Terminated due to inappropriate strategy. % 173.49/24.77 % (3952541)------------------------------ % 173.49/24.77 % (3952541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952541)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952541)Termination reason: Inappropriate % 173.49/24.77 % (3952541)Time elapsed: 0.054 s % 173.49/24.77 % (3952541)Peak memory usage: 13 MB % 173.49/24.77 % (3952541)Instructions burned: 79 (million) % 173.49/24.77 % (3952541)------------------------------ % 173.49/24.77 % (3952541)------------------------------ % 173.49/24.77 % (3952546)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4199707912:i=28120:bs=on:fsr=off_2828 on theBenchmark for (2828ds/28120Mi) % 173.49/24.77 % (3952213)Instruction limit reached! % 173.49/24.77 % (3952213)------------------------------ % 173.49/24.77 % (3952213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952213)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952213)Termination reason: Instruction limit % 173.49/24.77 % (3952213)Termination phase: Saturation % 173.49/24.77 % (3952213)Time elapsed: 9.885 s % 173.49/24.77 % (3952213)Peak memory usage: 54 MB % 173.49/24.77 % (3952213)Instructions burned: 14135 (million) % 173.49/24.77 % (3952627)fmb+10_1_sil=256000:fmbss=7:random_seed=1392509596:fmbsr=1.6:i=182295_2808 on theBenchmark for (2808ds/182295Mi) % 173.49/24.77 % (3952627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.49/24.77 % (3952627)Terminated due to inappropriate strategy. % 173.49/24.77 % (3952627)------------------------------ % 173.49/24.77 % (3952627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.49/24.77 % (3952627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.49/24.77 % (3952627)CaDiCaL version: 2.1.3 % 173.49/24.77 % (3952627)Termination reason: Inappropriate % 173.49/24.77 % (3952627)Time elapsed: 0.033 s % 173.49/24.77 % (3952627)Peak memory usage: 13 MB % 173.49/24.77 % (3952627)Instructions burned: 79 (million) % 173.49/24.77 % (3952627)------------------------------ % 173.49/24.77 % (3952627)------------------------------ % 173.49/24.77 % (3952629)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=979569195:i=44625:gsp=on_2808 on theBenchmark for (2808ds/44625Mi) % 186.36/26.52 % (3952629)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.36/26.52 % (3952629)Terminated due to inappropriate strategy. % 186.36/26.52 % (3952629)------------------------------ % 186.36/26.52 % (3952629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.36/26.52 % (3952629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.36/26.52 % (3952629)CaDiCaL version: 2.1.3 % 186.36/26.52 % (3952629)Termination reason: Inappropriate % 186.36/26.52 % (3952629)Time elapsed: 0.037 s % 186.36/26.52 % (3952629)Peak memory usage: 14 MB % 186.36/26.52 % (3952629)Instructions burned: 83 (million) % 186.36/26.52 % (3952629)------------------------------ % 186.36/26.52 % (3952629)------------------------------ % 186.36/26.52 % (3952631)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1678508275:i=160505_2807 on theBenchmark for (2807ds/160505Mi) % 186.36/26.52 % (3952631)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.36/26.52 % (3952631)Terminated due to inappropriate strategy. % 186.36/26.52 % (3952631)------------------------------ % 186.36/26.52 % (3952631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.36/26.52 % (3952631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.36/26.52 % (3952631)CaDiCaL version: 2.1.3 % 186.36/26.52 % (3952631)Termination reason: Inappropriate % 186.36/26.52 % (3952631)Time elapsed: 0.033 s % 186.36/26.52 % (3952631)Peak memory usage: 13 MB % 186.36/26.52 % (3952631)Instructions burned: 79 (million) % 186.36/26.52 % (3952631)------------------------------ % 186.36/26.52 % (3952631)------------------------------ % 186.36/26.52 % (3952633)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3941203401:fmbsr=1.3:i=225729_2807 on theBenchmark for (2807ds/225729Mi) % 186.36/26.52 % (3952633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.36/26.52 % (3952633)Terminated due to inappropriate strategy. % 186.36/26.52 % (3952633)------------------------------ % 186.36/26.52 % (3952633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.36/26.52 % (3952633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.36/26.52 % (3952633)CaDiCaL version: 2.1.3 % 186.36/26.52 % (3952633)Termination reason: Inappropriate % 186.36/26.52 % (3952633)Time elapsed: 0.045 s % 186.36/26.52 % (3952633)Peak memory usage: 13 MB % 186.36/26.52 % (3952633)Instructions burned: 110 (million) % 186.36/26.52 % (3952633)------------------------------ % 186.36/26.52 % (3952633)------------------------------ % 186.36/26.52 % (3952635)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=969041231:fmbsr=2:i=185024:ins=7_2806 on theBenchmark for (2806ds/185024Mi) % 186.36/26.52 % (3952635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.36/26.52 % (3952635)Terminated due to inappropriate strategy. % 186.36/26.52 % (3952635)------------------------------ % 186.36/26.52 % (3952635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.36/26.52 % (3952635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.36/26.52 % (3952635)CaDiCaL version: 2.1.3 % 186.36/26.52 % (3952635)Termination reason: Inappropriate % 186.36/26.52 % (3952635)Time elapsed: 0.045 s % 186.36/26.52 % (3952635)Peak memory usage: 13 MB % 186.36/26.52 % (3952635)Instructions burned: 110 (million) % 186.36/26.52 % (3952635)------------------------------ % 186.36/26.52 % (3952635)------------------------------ % 186.36/26.52 % (3952637)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2357520385:rtra=on_2805 on theBenchmark for (2805ds/0Mi) % 186.36/26.52 % (3952637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.36/26.52 % (3952637)Terminated due to inappropriate strategy. % 186.36/26.52 % (3952637)------------------------------ % 186.36/26.52 % (3952637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.36/26.52 % (3952637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.36/26.52 % (3952637)CaDiCaL version: 2.1.3 % 186.36/26.52 % (3952637)Termination reason: Inappropriate % 186.36/26.52 % (3952637)Time elapsed: 0.044 s % 186.36/26.52 % (3952637)Peak memory usage: 15 MB % 186.36/26.52 % (3952637)Instructions burned: 93 (million) % 186.36/26.52 % (3952637)------------------------------ % 186.36/26.52 % (3952637)------------------------------ % 186.36/26.52 % (3952639)% WARNING: option uhcvi not known. % 186.36/26.52 % (3952639)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3935327732:i=271062:add=off:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/271062Mi) % 205.52/29.24 % (3952215)Instruction limit reached! % 205.52/29.24 % (3952215)------------------------------ % 205.52/29.24 % (3952215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952215)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952215)Termination reason: Instruction limit % 205.52/29.24 % (3952215)Termination phase: Saturation % 205.52/29.24 % (3952215)Time elapsed: 8.330 s % 205.52/29.24 % (3952215)Peak memory usage: 34 MB % 205.52/29.24 % (3952215)Instructions burned: 15852 (million) % 205.52/29.24 % (3952641)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1798015175:i=176048:add=on:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/176048Mi) % 205.52/29.24 % (3952342)Instruction limit reached! % 205.52/29.24 % (3952342)------------------------------ % 205.52/29.24 % (3952342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952342)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952342)Termination reason: Instruction limit % 205.52/29.24 % (3952342)Termination phase: Saturation % 205.52/29.24 % (3952342)Time elapsed: 9.412 s % 205.52/29.24 % (3952342)Peak memory usage: 93 MB % 205.52/29.24 % (3952342)Instructions burned: 17628 (million) % 205.52/29.24 % (3952756)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2716558088:i=206:fgj=on:rtra=on_2760 on theBenchmark for (2760ds/206Mi) % 205.52/29.24 % (3952756)Instruction limit reached! % 205.52/29.24 % (3952756)------------------------------ % 205.52/29.24 % (3952756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952756)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952756)Termination reason: Instruction limit % 205.52/29.24 % (3952756)Termination phase: Saturation % 205.52/29.24 % (3952756)Time elapsed: 0.106 s % 205.52/29.24 % (3952756)Peak memory usage: 17 MB % 205.52/29.24 % (3952756)Instructions burned: 206 (million) % 205.52/29.24 % (3952758)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1686037391:i=232:rtra=on_2759 on theBenchmark for (2759ds/232Mi) % 205.52/29.24 % (3952758)Instruction limit reached! % 205.52/29.24 % (3952758)------------------------------ % 205.52/29.24 % (3952758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952758)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952758)Termination reason: Instruction limit % 205.52/29.24 % (3952758)Termination phase: Saturation % 205.52/29.24 % (3952758)Time elapsed: 0.110 s % 205.52/29.24 % (3952758)Peak memory usage: 17 MB % 205.52/29.24 % (3952758)Instructions burned: 232 (million) % 205.52/29.24 % (3952760)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4151566762:i=262:rtra=on_2757 on theBenchmark for (2757ds/262Mi) % 205.52/29.24 % (3952760)Instruction limit reached! % 205.52/29.24 % (3952760)------------------------------ % 205.52/29.24 % (3952760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952760)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952760)Termination reason: Instruction limit % 205.52/29.24 % (3952760)Termination phase: Saturation % 205.52/29.24 % (3952760)Time elapsed: 0.120 s % 205.52/29.24 % (3952760)Peak memory usage: 17 MB % 205.52/29.24 % (3952760)Instructions burned: 263 (million) % 205.52/29.24 % (3952762)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2178517427:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2756 on theBenchmark for (2756ds/318Mi) % 205.52/29.24 % (3952762)Instruction limit reached! % 205.52/29.24 % (3952762)------------------------------ % 205.52/29.24 % (3952762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.52/29.24 % (3952762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.52/29.24 % (3952762)CaDiCaL version: 2.1.3 % 205.52/29.24 % (3952762)Termination reason: Instruction limit % 205.52/29.24 % (3952762)Termination phase: Saturation % 205.52/29.24 % (3952762)Time elapsed: 0.159 s % 205.52/29.24 % (3952762)Peak memory usage: 18 MB % 205.52/29.24 % (3952762)Instructions burned: 318 (million) % 205.52/29.24 % (3952764)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3971245173:i=1428:nm=2:rtra=on_2754 on theBenchmark for (2754ds/1428Mi) % 228.20/32.42 % (3952764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.20/32.42 % (3952764)Terminated due to inappropriate strategy. % 228.20/32.42 % (3952764)------------------------------ % 228.20/32.42 % (3952764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952764)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952764)Termination reason: Inappropriate % 228.20/32.42 % (3952764)Time elapsed: 0.044 s % 228.20/32.42 % (3952764)Peak memory usage: 15 MB % 228.20/32.42 % (3952764)Instructions burned: 93 (million) % 228.20/32.42 % (3952764)------------------------------ % 228.20/32.42 % (3952764)------------------------------ % 228.20/32.42 % (3952766)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=395287137:i=262:bd=preordered:rtra=on:fsd=on_2754 on theBenchmark for (2754ds/262Mi) % 228.20/32.42 % (3952766)Instruction limit reached! % 228.20/32.42 % (3952766)------------------------------ % 228.20/32.42 % (3952766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952766)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952766)Termination reason: Instruction limit % 228.20/32.42 % (3952766)Termination phase: Saturation % 228.20/32.42 % (3952766)Time elapsed: 0.119 s % 228.20/32.42 % (3952766)Peak memory usage: 17 MB % 228.20/32.42 % (3952766)Instructions burned: 262 (million) % 228.20/32.42 % (3952768)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=2449926701:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2752 on theBenchmark for (2752ds/1368Mi) % 228.20/32.42 % (3952768)Instruction limit reached! % 228.20/32.42 % (3952768)------------------------------ % 228.20/32.42 % (3952768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952768)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952768)Termination reason: Instruction limit % 228.20/32.42 % (3952768)Termination phase: Saturation % 228.20/32.42 % (3952768)Time elapsed: 0.714 s % 228.20/32.42 % (3952768)Peak memory usage: 22 MB % 228.20/32.42 % (3952768)Instructions burned: 1368 (million) % 228.20/32.42 % (3952770)ott-21_1_sil=16000:si=on:fs=off:random_seed=376573718:i=360:av=off:fsr=off:rtra=on_2745 on theBenchmark for (2745ds/360Mi) % 228.20/32.42 % (3952770)Instruction limit reached! % 228.20/32.42 % (3952770)------------------------------ % 228.20/32.42 % (3952770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952770)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952770)Termination reason: Instruction limit % 228.20/32.42 % (3952770)Termination phase: Saturation % 228.20/32.42 % (3952770)Time elapsed: 0.179 s % 228.20/32.42 % (3952770)Peak memory usage: 17 MB % 228.20/32.42 % (3952770)Instructions burned: 362 (million) % 228.20/32.42 % (3952772)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1178838021:i=954:bd=all:rtra=on_2743 on theBenchmark for (2743ds/954Mi) % 228.20/32.42 % (3952772)Instruction limit reached! % 228.20/32.42 % (3952772)------------------------------ % 228.20/32.42 % (3952772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952772)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952772)Termination reason: Instruction limit % 228.20/32.42 % (3952772)Termination phase: Saturation % 228.20/32.42 % (3952772)Time elapsed: 0.546 s % 228.20/32.42 % (3952772)Peak memory usage: 19 MB % 228.20/32.42 % (3952772)Instructions burned: 954 (million) % 228.20/32.42 % (3952774)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=52823291:fmbsr=1.3:i=1730:ins=25:rtra=on_2737 on theBenchmark for (2737ds/1730Mi) % 228.20/32.42 % (3952774)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.20/32.42 % (3952774)Terminated due to inappropriate strategy. % 228.20/32.42 % (3952774)------------------------------ % 228.20/32.42 % (3952774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.42 % (3952774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.42 % (3952774)CaDiCaL version: 2.1.3 % 228.20/32.42 % (3952774)Termination reason: Inappropriate % 264.48/37.57 % (3952774)Time elapsed: 0.044 s % 264.48/37.57 % (3952774)Peak memory usage: 15 MB % 264.48/37.57 % (3952774)Instructions burned: 92 (million) % 264.48/37.57 % (3952774)------------------------------ % 264.48/37.57 % (3952774)------------------------------ % 264.48/37.57 % (3952776)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2057171324:i=2358:rtra=on_2736 on theBenchmark for (2736ds/2358Mi) % 264.48/37.57 % (3952776)Instruction limit reached! % 264.48/37.57 % (3952776)------------------------------ % 264.48/37.57 % (3952776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.48/37.57 % (3952776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.48/37.57 % (3952776)CaDiCaL version: 2.1.3 % 264.48/37.57 % (3952776)Termination reason: Instruction limit % 264.48/37.57 % (3952776)Termination phase: Saturation % 264.48/37.57 % (3952776)Time elapsed: 1.412 s % 264.48/37.57 % (3952776)Peak memory usage: 26 MB % 264.48/37.57 % (3952776)Instructions burned: 2359 (million) % 264.48/37.57 % (3952778)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3097883911:i=1778:ins=1:rtra=on_2722 on theBenchmark for (2722ds/1778Mi) % 264.48/37.57 % (3952778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.48/37.57 % (3952778)Terminated due to inappropriate strategy. % 264.48/37.57 % (3952778)------------------------------ % 264.48/37.57 % (3952778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.48/37.57 % (3952778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.48/37.57 % (3952778)CaDiCaL version: 2.1.3 % 264.48/37.57 % (3952778)Termination reason: Inappropriate % 264.48/37.57 % (3952778)Time elapsed: 0.059 s % 264.48/37.57 % (3952778)Peak memory usage: 16 MB % 264.48/37.57 % (3952778)Instructions burned: 124 (million) % 264.48/37.57 % (3952778)------------------------------ % 264.48/37.57 % (3952778)------------------------------ % 264.48/37.57 % (3952780)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=897084168:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/1384Mi) % 264.48/37.57 % (3952780)Instruction limit reached! % 264.48/37.57 % (3952780)------------------------------ % 264.48/37.57 % (3952780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.48/37.57 % (3952780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.48/37.57 % (3952780)CaDiCaL version: 2.1.3 % 264.48/37.57 % (3952780)Termination reason: Instruction limit % 264.48/37.57 % (3952780)Termination phase: Saturation % 264.48/37.57 % (3952780)Time elapsed: 0.834 s % 264.48/37.57 % (3952780)Peak memory usage: 25 MB % 264.48/37.57 % (3952780)Instructions burned: 1384 (million) % 264.48/37.57 % (3952782)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2165572220:i=1758:kws=inv_precedence:fsr=off:rtra=on_2713 on theBenchmark for (2713ds/1758Mi) % 264.48/37.57 % (3952546)Instruction limit reached! % 264.48/37.57 % (3952546)------------------------------ % 264.48/37.57 % (3952546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.48/37.57 % (3952546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.48/37.57 % (3952546)CaDiCaL version: 2.1.3 % 264.48/37.57 % (3952546)Termination reason: Instruction limit % 264.48/37.57 % (3952546)Termination phase: Saturation % 264.48/37.57 % (3952546)Time elapsed: 11.771 s % 264.48/37.57 % (3952546)Peak memory usage: 27 MB % 264.48/37.57 % (3952546)Instructions burned: 28122 (million) % 264.48/37.57 % (3952843)fmb+10_1_sil=64000:si=on:random_seed=967283453:i=44122:nm=2:rtra=on:gsp=on_2710 on theBenchmark for (2710ds/44122Mi) % 264.48/37.57 % (3952843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.48/37.57 % (3952843)Terminated due to inappropriate strategy. % 264.48/37.57 % (3952843)------------------------------ % 264.48/37.57 % (3952843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.48/37.57 % (3952843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.48/37.57 % (3952843)CaDiCaL version: 2.1.3 % 264.48/37.57 % (3952843)Termination reason: Inappropriate % 264.48/37.57 % (3952843)Time elapsed: 0.048 s % 264.48/37.57 % (3952843)Peak memory usage: 15 MB % 264.48/37.57 % (3952843)Instructions burned: 101 (million) % 264.48/37.57 % (3952843)------------------------------ % 264.48/37.57 % (3952843)------------------------------ % 264.48/37.57 % (3952884)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3854586605:i=19030:nm=5:rtra=on_2709 on theBenchmark for (2709ds/19030Mi) % 283.17/40.17 % (3952884)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.17/40.17 % (3952884)Terminated due to inappropriate strategy. % 283.17/40.17 % (3952884)------------------------------ % 283.17/40.17 % (3952884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.17/40.17 % (3952884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.17/40.17 % (3952884)CaDiCaL version: 2.1.3 % 283.17/40.17 % (3952884)Termination reason: Inappropriate % 283.17/40.17 % (3952884)Time elapsed: 0.044 s % 283.17/40.17 % (3952884)Peak memory usage: 15 MB % 283.17/40.17 % (3952884)Instructions burned: 93 (million) % 283.17/40.17 % (3952884)------------------------------ % 283.17/40.17 % (3952884)------------------------------ % 283.17/40.17 % (3952904)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1477445812:fmbsr=1.7:i=1840:rtra=on_2709 on theBenchmark for (2709ds/1840Mi) % 283.17/40.17 % (3952904)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.17/40.17 % (3952904)Terminated due to inappropriate strategy. % 283.17/40.17 % (3952904)------------------------------ % 283.17/40.17 % (3952904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.17/40.17 % (3952904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.17/40.17 % (3952904)CaDiCaL version: 2.1.3 % 283.17/40.17 % (3952904)Termination reason: Inappropriate % 283.17/40.17 % (3952904)Time elapsed: 0.044 s % 283.17/40.17 % (3952904)Peak memory usage: 15 MB % 283.17/40.17 % (3952904)Instructions burned: 93 (million) % 283.17/40.17 % (3952904)------------------------------ % 283.17/40.17 % (3952904)------------------------------ % 283.17/40.17 % (3952906)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2648800156:i=10262:rtra=on_2708 on theBenchmark for (2708ds/10262Mi) % 283.17/40.17 % (3952782)Instruction limit reached! % 283.17/40.17 % (3952782)------------------------------ % 283.17/40.17 % (3952782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.17/40.17 % (3952782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.17/40.17 % (3952782)CaDiCaL version: 2.1.3 % 283.17/40.17 % (3952782)Termination reason: Instruction limit % 283.17/40.17 % (3952782)Termination phase: Saturation % 283.17/40.17 % (3952782)Time elapsed: 1.026 s % 283.17/40.17 % (3952782)Peak memory usage: 28 MB % 283.17/40.17 % (3952782)Instructions burned: 1759 (million) % 283.17/40.17 % (3952999)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4199034343:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2702 on theBenchmark for (2702ds/2944Mi) % 283.17/40.17 % (3952999)Instruction limit reached! % 283.17/40.17 % (3952999)------------------------------ % 283.17/40.17 % (3952999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.17/40.17 % (3952999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.17/40.17 % (3952999)CaDiCaL version: 2.1.3 % 283.17/40.17 % (3952999)Termination reason: Instruction limit % 283.17/40.17 % (3952999)Termination phase: Saturation % 283.17/40.17 % (3952999)Time elapsed: 2.200 s % 283.17/40.17 % (3952999)Peak memory usage: 32 MB % 283.17/40.17 % (3952999)Instructions burned: 2945 (million) % 283.17/40.17 % (3953116)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2716824734:i=12648:rtra=on_2680 on theBenchmark for (2680ds/12648Mi) % 283.17/40.17 % (3953116)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.17/40.17 % (3953116)Terminated due to inappropriate strategy. % 283.17/40.17 % (3953116)------------------------------ % 283.17/40.17 % (3953116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.17/40.17 % (3953116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.17/40.17 % (3953116)CaDiCaL version: 2.1.3 % 283.17/40.17 % (3953116)Termination reason: Inappropriate % 283.17/40.17 % (3953116)Time elapsed: 0.069 s % 283.17/40.17 % (3953116)Peak memory usage: 15 MB % 283.17/40.17 % (3953116)Instructions burned: 93 (million) % 283.17/40.17 % (3953116)------------------------------ % 283.17/40.17 % (3953116)------------------------------ % 283.17/40.17 % (3953121)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=832511300:fmbsr=2.30978:i=4348:rtra=on_2679 on theBenchmark for (2679ds/4348Mi) % 283.17/40.17 % (3953121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.17/40.17 % (3953121)Terminated due to inappropriate strategy. % 283.17/40.17 % (3953121)---------------------Terminated % 300.71/42.64 % Vampire exiting %------------------------------------------------------------------------------