%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW028_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 : 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:38:26 PM UTC 2026 % Result : Timeout 300.50s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW028_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n002.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 13:11:52 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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.04/0.75 % (339268)Will run a generic schedule for satisfiability detection. % 3.04/0.75 % (339273)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4011979894_2999 on theBenchmark for (2999ds/0Mi) % 3.04/0.75 % (339274)% WARNING: option uhcvi not known. % 3.04/0.75 % (339275)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3939960726:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.04/0.75 % (339274)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=701507599:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.04/0.75 % (339276)dis+10_1_sil=32000:sp=arity:random_seed=1581673180:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.04/0.75 % (339277)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1616299981:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.04/0.75 % (339278)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=14785763:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.04/0.75 % (339279)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2102080005:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.04/0.75 % (339273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.04/0.75 % (339273)Terminated due to inappropriate strategy. % 3.04/0.75 % (339273)------------------------------ % 3.04/0.75 % (339273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.75 % (339273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.75 % (339273)CaDiCaL version: 2.1.3 % 3.04/0.75 % (339273)Termination reason: Inappropriate % 3.04/0.75 % (339273)Time elapsed: 0.017 s % 3.04/0.75 % (339273)Peak memory usage: 13 MB % 3.04/0.75 % (339273)Instructions burned: 75 (million) % 3.04/0.75 % (339273)------------------------------ % 3.04/0.75 % (339273)------------------------------ % 3.04/0.75 % (339287)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3412175357:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.04/0.75 % (339287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.04/0.75 % (339287)Terminated due to inappropriate strategy. % 3.04/0.75 % (339287)------------------------------ % 3.04/0.75 % (339287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.75 % (339287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.75 % (339287)CaDiCaL version: 2.1.3 % 3.04/0.75 % (339287)Termination reason: Inappropriate % 3.04/0.75 % (339287)Time elapsed: 0.017 s % 3.04/0.75 % (339287)Peak memory usage: 13 MB % 3.04/0.75 % (339287)Instructions burned: 74 (million) % 3.04/0.75 % (339287)------------------------------ % 3.04/0.75 % (339287)------------------------------ % 3.04/0.75 % (339276)Instruction limit reached! % 3.04/0.75 % (339276)------------------------------ % 3.04/0.75 % (339276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.75 % (339276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.75 % (339276)CaDiCaL version: 2.1.3 % 3.04/0.75 % (339276)Termination reason: Instruction limit % 3.04/0.75 % (339276)Termination phase: Saturation % 3.04/0.75 % (339276)Time elapsed: 0.047 s % 3.04/0.75 % (339276)Peak memory usage: 14 MB % 3.04/0.75 % (339276)Instructions burned: 105 (million) % 3.04/0.75 % (339289)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1606861559:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.04/0.76 % (339277)Instruction limit reached! % 3.04/0.76 % (339277)------------------------------ % 3.04/0.76 % (339277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.76 % (339277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.76 % (339277)CaDiCaL version: 2.1.3 % 3.04/0.76 % (339277)Termination reason: Instruction limit % 3.04/0.76 % (339277)Termination phase: Saturation % 3.04/0.76 % (339277)Time elapsed: 0.052 s % 3.04/0.76 % (339277)Peak memory usage: 15 MB % 3.04/0.76 % (339277)Instructions burned: 116 (million) % 3.04/0.76 % (339278)Instruction limit reached! % 3.04/0.76 % (339278)------------------------------ % 3.04/0.76 % (339278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.76 % (339278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.76 % (339278)CaDiCaL version: 2.1.3 % 3.04/0.76 % (339278)Termination reason: Instruction limit % 3.04/0.76 % (339278)Termination phase: Saturation % 7.11/1.34 % (339278)Time elapsed: 0.053 s % 7.11/1.34 % (339278)Peak memory usage: 14 MB % 7.11/1.34 % (339278)Instructions burned: 131 (million) % 7.11/1.34 % (339279)Instruction limit reached! % 7.11/1.34 % (339279)------------------------------ % 7.11/1.34 % (339279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.11/1.34 % (339279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.34 % (339279)CaDiCaL version: 2.1.3 % 7.11/1.34 % (339279)Termination reason: Instruction limit % 7.11/1.34 % (339279)Termination phase: Saturation % 7.11/1.34 % (339279)Time elapsed: 0.065 s % 7.11/1.34 % (339279)Peak memory usage: 15 MB % 7.11/1.34 % (339279)Instructions burned: 160 (million) % 7.11/1.34 % (339290)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=3271049184:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.11/1.34 % (339292)ott-21_1_sil=16000:fs=off:random_seed=3013646617:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.11/1.34 % (339293)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3311137126:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.11/1.34 % (339289)Instruction limit reached! % 7.11/1.34 % (339289)------------------------------ % 7.11/1.34 % (339289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.11/1.34 % (339289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.34 % (339289)CaDiCaL version: 2.1.3 % 7.11/1.34 % (339289)Termination reason: Instruction limit % 7.11/1.34 % (339289)Termination phase: Saturation % 7.11/1.34 % (339289)Time elapsed: 0.029 s % 7.11/1.34 % (339289)Peak memory usage: 15 MB % 7.11/1.34 % (339289)Instructions burned: 134 (million) % 7.11/1.34 % (339294)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2057547963:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.11/1.34 % (339298)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4181628817:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.11/1.34 % (339294)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.11/1.34 % (339294)Terminated due to inappropriate strategy. % 7.11/1.34 % (339294)------------------------------ % 7.11/1.34 % (339294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.11/1.34 % (339294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.34 % (339294)CaDiCaL version: 2.1.3 % 7.11/1.34 % (339294)Termination reason: Inappropriate % 7.11/1.34 % (339294)Time elapsed: 0.031 s % 7.11/1.34 % (339294)Peak memory usage: 13 MB % 7.11/1.34 % (339294)Instructions burned: 74 (million) % 7.11/1.34 % (339294)------------------------------ % 7.11/1.34 % (339294)------------------------------ % 7.11/1.34 % (339301)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1217943712:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.11/1.34 % (339292)Instruction limit reached! % 7.11/1.34 % (339292)------------------------------ % 7.11/1.34 % (339292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.11/1.34 % (339292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.34 % (339292)CaDiCaL version: 2.1.3 % 7.11/1.34 % (339292)Termination reason: Instruction limit % 7.11/1.34 % (339292)Termination phase: Saturation % 7.11/1.34 % (339292)Time elapsed: 0.077 s % 7.11/1.34 % (339292)Peak memory usage: 14 MB % 7.11/1.34 % (339292)Instructions burned: 180 (million) % 7.11/1.34 % (339301)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.11/1.34 % (339301)Terminated due to inappropriate strategy. % 7.11/1.34 % (339301)------------------------------ % 7.11/1.34 % (339301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.11/1.34 % (339301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.34 % (339301)CaDiCaL version: 2.1.3 % 7.11/1.34 % (339301)Termination reason: Inappropriate % 7.11/1.34 % (339301)Time elapsed: 0.026 s % 7.11/1.34 % (339301)Peak memory usage: 15 MB % 7.11/1.34 % (339301)Instructions burned: 104 (million) % 7.11/1.34 % (339301)------------------------------ % 7.11/1.34 % (339301)------------------------------ % 7.11/1.34 % (339303)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=4139627734: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) % 17.44/2.99 % (339304)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4174117733:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.44/2.99 % (339293)Instruction limit reached! % 17.44/2.99 % (339293)------------------------------ % 17.44/2.99 % (339293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339293)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339293)Termination reason: Instruction limit % 17.44/2.99 % (339293)Termination phase: Saturation % 17.44/2.99 % (339293)Time elapsed: 0.270 s % 17.44/2.99 % (339293)Peak memory usage: 16 MB % 17.44/2.99 % (339293)Instructions burned: 477 (million) % 17.44/2.99 % (339307)fmb+10_1_sil=64000:random_seed=187724639:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 17.44/2.99 % (339290)Instruction limit reached! % 17.44/2.99 % (339290)------------------------------ % 17.44/2.99 % (339290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339290)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339290)Termination reason: Instruction limit % 17.44/2.99 % (339290)Termination phase: Saturation % 17.44/2.99 % (339290)Time elapsed: 0.315 s % 17.44/2.99 % (339290)Peak memory usage: 19 MB % 17.44/2.99 % (339290)Instructions burned: 684 (million) % 17.44/2.99 % (339307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.99 % (339307)Terminated due to inappropriate strategy. % 17.44/2.99 % (339307)------------------------------ % 17.44/2.99 % (339307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339307)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339307)Termination reason: Inappropriate % 17.44/2.99 % (339307)Time elapsed: 0.035 s % 17.44/2.99 % (339307)Peak memory usage: 13 MB % 17.44/2.99 % (339307)Instructions burned: 82 (million) % 17.44/2.99 % (339307)------------------------------ % 17.44/2.99 % (339307)------------------------------ % 17.44/2.99 % (339309)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2537201622:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.44/2.99 % (339303)Instruction limit reached! % 17.44/2.99 % (339303)------------------------------ % 17.44/2.99 % (339303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339303)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339303)Termination reason: Instruction limit % 17.44/2.99 % (339303)Termination phase: Saturation % 17.44/2.99 % (339303)Time elapsed: 0.231 s % 17.44/2.99 % (339303)Peak memory usage: 21 MB % 17.44/2.99 % (339303)Instructions burned: 692 (million) % 17.44/2.99 % (339312)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3944930983:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 17.44/2.99 % (339310)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3572783013:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 17.44/2.99 % (339309)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.99 % (339309)Terminated due to inappropriate strategy. % 17.44/2.99 % (339309)------------------------------ % 17.44/2.99 % (339309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339309)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339309)Termination reason: Inappropriate % 17.44/2.99 % (339309)Time elapsed: 0.032 s % 17.44/2.99 % (339309)Peak memory usage: 13 MB % 17.44/2.99 % (339309)Instructions burned: 74 (million) % 17.44/2.99 % (339309)------------------------------ % 17.44/2.99 % (339309)------------------------------ % 17.44/2.99 % (339310)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.99 % (339310)Terminated due to inappropriate strategy. % 17.44/2.99 % (339310)------------------------------ % 17.44/2.99 % (339310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.99 % (339310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.99 % (339310)CaDiCaL version: 2.1.3 % 17.44/2.99 % (339310)Termination reason: Inappropriate % 17.44/2.99 % (339310)Time elapsed: 0.031 s % 17.44/2.99 % (339310)Peak memory usage: 13 MB % 17.44/2.99 % (339310)Instructions burned: 74 (million) % 24.67/3.92 % (339310)------------------------------ % 24.67/3.92 % (339310)------------------------------ % 24.67/3.92 % (339315)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3185997770:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 24.67/3.92 % (339316)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1827305405:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 24.67/3.92 % (339316)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.67/3.92 % (339316)Terminated due to inappropriate strategy. % 24.67/3.92 % (339316)------------------------------ % 24.67/3.92 % (339316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.67/3.92 % (339316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.67/3.92 % (339316)CaDiCaL version: 2.1.3 % 24.67/3.92 % (339316)Termination reason: Inappropriate % 24.67/3.92 % (339316)Time elapsed: 0.033 s % 24.67/3.92 % (339316)Peak memory usage: 13 MB % 24.67/3.92 % (339316)Instructions burned: 74 (million) % 24.67/3.92 % (339316)------------------------------ % 24.67/3.92 % (339316)------------------------------ % 24.67/3.92 % (339319)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3076296233:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.67/3.92 % (339319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.67/3.92 % (339319)Terminated due to inappropriate strategy. % 24.67/3.92 % (339319)------------------------------ % 24.67/3.92 % (339319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.67/3.92 % (339319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.67/3.92 % (339319)CaDiCaL version: 2.1.3 % 24.67/3.92 % (339319)Termination reason: Inappropriate % 24.67/3.92 % (339319)Time elapsed: 0.031 s % 24.67/3.92 % (339319)Peak memory usage: 13 MB % 24.67/3.92 % (339319)Instructions burned: 74 (million) % 24.67/3.92 % (339319)------------------------------ % 24.67/3.92 % (339319)------------------------------ % 24.67/3.92 % (339321)ott-2_1_sil=16000:newcnf=on:random_seed=2442247764:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.67/3.92 % (339304)Instruction limit reached! % 24.67/3.92 % (339304)------------------------------ % 24.67/3.92 % (339304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.67/3.92 % (339304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.67/3.92 % (339304)CaDiCaL version: 2.1.3 % 24.67/3.92 % (339304)Termination reason: Instruction limit % 24.67/3.92 % (339304)Termination phase: Saturation % 24.67/3.92 % (339304)Time elapsed: 0.491 s % 24.67/3.92 % (339304)Peak memory usage: 21 MB % 24.67/3.92 % (339304)Instructions burned: 879 (million) % 24.67/3.92 % (339298)Instruction limit reached! % 24.67/3.92 % (339298)------------------------------ % 24.67/3.92 % (339298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.67/3.92 % (339298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.67/3.92 % (339298)CaDiCaL version: 2.1.3 % 24.67/3.92 % (339298)Termination reason: Instruction limit % 24.67/3.92 % (339298)Termination phase: Saturation % 24.67/3.92 % (339298)Time elapsed: 0.590 s % 24.67/3.92 % (339298)Peak memory usage: 20 MB % 24.67/3.92 % (339298)Instructions burned: 1180 (million) % 24.67/3.92 % (339323)ott+10_1_sil=32000:tgt=ground:random_seed=2584107948:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 24.67/3.92 % (339324)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=584467991:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 24.67/3.92 % (339324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.67/3.92 % (339324)Terminated due to inappropriate strategy. % 24.67/3.92 % (339324)------------------------------ % 24.67/3.92 % (339324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.67/3.92 % (339324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.67/3.92 % (339324)CaDiCaL version: 2.1.3 % 24.67/3.92 % (339324)Termination reason: Inappropriate % 24.67/3.92 % (339324)Time elapsed: 0.032 s % 24.67/3.92 % (339324)Peak memory usage: 13 MB % 24.67/3.92 % (339324)Instructions burned: 75 (million) % 24.67/3.92 % (339324)------------------------------ % 24.67/3.92 % (339324)------------------------------ % 24.67/3.92 % (339327)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1908185302:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 24.67/3.92 % (339315)Instruction limit reached! % 87.53/12.60 % (339315)------------------------------ % 87.53/12.60 % (339315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339315)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339315)Termination reason: Instruction limit % 87.53/12.60 % (339315)Termination phase: Saturation % 87.53/12.60 % (339315)Time elapsed: 0.577 s % 87.53/12.60 % (339315)Peak memory usage: 18 MB % 87.53/12.60 % (339315)Instructions burned: 1474 (million) % 87.53/12.60 % (339321)Instruction limit reached! % 87.53/12.60 % (339321)------------------------------ % 87.53/12.60 % (339321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339321)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339321)Termination reason: Instruction limit % 87.53/12.60 % (339321)Termination phase: Saturation % 87.53/12.60 % (339321)Time elapsed: 0.466 s % 87.53/12.60 % (339321)Peak memory usage: 19 MB % 87.53/12.60 % (339321)Instructions burned: 870 (million) % 87.53/12.60 % (339329)dis+21_1_sil=32000:sas=cadical:random_seed=4040136523:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 87.53/12.60 % (339331)ott+11_1_sil=16000:gs=on:random_seed=4134541252:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 87.53/12.60 % (339312)Instruction limit reached! % 87.53/12.60 % (339312)------------------------------ % 87.53/12.60 % (339312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339312)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339312)Termination reason: Instruction limit % 87.53/12.60 % (339312)Termination phase: Saturation % 87.53/12.60 % (339312)Time elapsed: 1.443 s % 87.53/12.60 % (339312)Peak memory usage: 43 MB % 87.53/12.60 % (339312)Instructions burned: 5134 (million) % 87.53/12.60 % (339333)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1068800291:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 87.53/12.60 % (339333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.53/12.60 % (339333)Terminated due to inappropriate strategy. % 87.53/12.60 % (339333)------------------------------ % 87.53/12.60 % (339333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339333)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339333)Termination reason: Inappropriate % 87.53/12.60 % (339333)Time elapsed: 0.022 s % 87.53/12.60 % (339333)Peak memory usage: 13 MB % 87.53/12.60 % (339333)Instructions burned: 101 (million) % 87.53/12.60 % (339333)------------------------------ % 87.53/12.60 % (339333)------------------------------ % 87.53/12.60 % (339335)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2905067421:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 87.53/12.60 % (339331)Instruction limit reached! % 87.53/12.60 % (339331)------------------------------ % 87.53/12.60 % (339331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339331)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339331)Termination reason: Instruction limit % 87.53/12.60 % (339331)Termination phase: Saturation % 87.53/12.60 % (339331)Time elapsed: 0.965 s % 87.53/12.60 % (339331)Peak memory usage: 21 MB % 87.53/12.60 % (339331)Instructions burned: 2252 (million) % 87.53/12.60 % (339337)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1790864133:i=29340_2979 on theBenchmark for (2979ds/29340Mi) % 87.53/12.60 % (339327)Instruction limit reached! % 87.53/12.60 % (339327)------------------------------ % 87.53/12.60 % (339327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.53/12.60 % (339327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.53/12.60 % (339327)CaDiCaL version: 2.1.3 % 87.53/12.60 % (339327)Termination reason: Instruction limit % 87.53/12.60 % (339327)Termination phase: Saturation % 87.53/12.60 % (339327)Time elapsed: 1.851 s % 87.53/12.60 % (339327)Peak memory usage: 31 MB % 87.53/12.60 % (339327)Instructions burned: 3513 (million) % 87.53/12.60 % (339339)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3408818049:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 87.53/12.60 % (339329)Instruction limit reached! % 111.91/16.12 % (339329)------------------------------ % 111.91/16.12 % (339329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339329)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339329)Termination reason: Instruction limit % 111.91/16.12 % (339329)Termination phase: Saturation % 111.91/16.12 % (339329)Time elapsed: 1.633 s % 111.91/16.12 % (339329)Peak memory usage: 24 MB % 111.91/16.12 % (339329)Instructions burned: 3775 (million) % 111.91/16.12 % (339341)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2926807022:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 111.91/16.12 % (339341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.91/16.12 % (339341)Terminated due to inappropriate strategy. % 111.91/16.12 % (339341)------------------------------ % 111.91/16.12 % (339341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339341)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339341)Termination reason: Inappropriate % 111.91/16.12 % (339341)Time elapsed: 0.032 s % 111.91/16.12 % (339341)Peak memory usage: 13 MB % 111.91/16.12 % (339341)Instructions burned: 74 (million) % 111.91/16.12 % (339341)------------------------------ % 111.91/16.12 % (339341)------------------------------ % 111.91/16.12 % (339343)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=718387422:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 111.91/16.12 % (339343)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.91/16.12 % (339343)Terminated due to inappropriate strategy. % 111.91/16.12 % (339343)------------------------------ % 111.91/16.12 % (339343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339343)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339343)Termination reason: Inappropriate % 111.91/16.12 % (339343)Time elapsed: 0.043 s % 111.91/16.12 % (339343)Peak memory usage: 13 MB % 111.91/16.12 % (339343)Instructions burned: 104 (million) % 111.91/16.12 % (339343)------------------------------ % 111.91/16.12 % (339343)------------------------------ % 111.91/16.12 % (339345)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=617703761:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 111.91/16.12 % (339345)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.91/16.12 % (339345)Terminated due to inappropriate strategy. % 111.91/16.12 % (339345)------------------------------ % 111.91/16.12 % (339345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339345)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339345)Termination reason: Inappropriate % 111.91/16.12 % (339345)Time elapsed: 0.043 s % 111.91/16.12 % (339345)Peak memory usage: 13 MB % 111.91/16.12 % (339345)Instructions burned: 104 (million) % 111.91/16.12 % (339345)------------------------------ % 111.91/16.12 % (339345)------------------------------ % 111.91/16.12 % (339347)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2857416871:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 111.91/16.12 % (339335)Instruction limit reached! % 111.91/16.12 % (339335)------------------------------ % 111.91/16.12 % (339335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339335)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339335)Termination reason: Instruction limit % 111.91/16.12 % (339335)Termination phase: Saturation % 111.91/16.12 % (339335)Time elapsed: 1.270 s % 111.91/16.12 % (339335)Peak memory usage: 43 MB % 111.91/16.12 % (339335)Instructions burned: 4595 (million) % 111.91/16.12 % (339349)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2297659820:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 111.91/16.12 % (339323)Instruction limit reached! % 111.91/16.12 % (339323)------------------------------ % 111.91/16.12 % (339323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.91/16.12 % (339323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.91/16.12 % (339323)CaDiCaL version: 2.1.3 % 111.91/16.12 % (339323)Termination reason: Instruction limit % 111.91/16.12 % (339323)Termination phase: Saturation % 123.78/17.78 % (339323)Time elapsed: 2.927 s % 123.78/17.78 % (339323)Peak memory usage: 31 MB % 123.78/17.78 % (339323)Instructions burned: 5114 (million) % 123.78/17.78 % (339351)dis+10_16:1_sil=16000:random_seed=3465570478:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 123.78/17.78 % (339349)Instruction limit reached! % 123.78/17.78 % (339349)------------------------------ % 123.78/17.78 % (339349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339349)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339349)Termination reason: Instruction limit % 123.78/17.78 % (339349)Termination phase: Saturation % 123.78/17.78 % (339349)Time elapsed: 1.768 s % 123.78/17.78 % (339349)Peak memory usage: 30 MB % 123.78/17.78 % (339349)Instructions burned: 8178 (million) % 123.78/17.78 % (339353)ott-3_8_sil=64000:random_seed=1232124407:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 123.78/17.78 % (339339)Instruction limit reached! % 123.78/17.78 % (339339)------------------------------ % 123.78/17.78 % (339339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339339)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339339)Termination reason: Instruction limit % 123.78/17.78 % (339339)Termination phase: Saturation % 123.78/17.78 % (339339)Time elapsed: 2.771 s % 123.78/17.78 % (339339)Peak memory usage: 49 MB % 123.78/17.78 % (339339)Instructions burned: 5211 (million) % 123.78/17.78 % (339355)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=198774169:fmbsr=2:i=32576_2945 on theBenchmark for (2945ds/32576Mi) % 123.78/17.78 % (339355)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.78/17.78 % (339355)Terminated due to inappropriate strategy. % 123.78/17.78 % (339355)------------------------------ % 123.78/17.78 % (339355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339355)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339355)Termination reason: Inappropriate % 123.78/17.78 % (339355)Time elapsed: 0.041 s % 123.78/17.78 % (339355)Peak memory usage: 13 MB % 123.78/17.78 % (339355)Instructions burned: 101 (million) % 123.78/17.78 % (339355)------------------------------ % 123.78/17.78 % (339355)------------------------------ % 123.78/17.78 % (339357)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2956223383:i=11404_2944 on theBenchmark for (2944ds/11404Mi) % 123.78/17.78 % (339351)Instruction limit reached! % 123.78/17.78 % (339351)------------------------------ % 123.78/17.78 % (339351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339351)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339351)Termination reason: Instruction limit % 123.78/17.78 % (339351)Termination phase: Saturation % 123.78/17.78 % (339351)Time elapsed: 4.709 s % 123.78/17.78 % (339351)Peak memory usage: 56 MB % 123.78/17.78 % (339351)Instructions burned: 9155 (million) % 123.78/17.78 % (339359)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2604185645:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 123.78/17.78 % (339353)Instruction limit reached! % 123.78/17.78 % (339353)------------------------------ % 123.78/17.78 % (339353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339353)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339353)Termination reason: Instruction limit % 123.78/17.78 % (339353)Termination phase: Saturation % 123.78/17.78 % (339353)Time elapsed: 5.861 s % 123.78/17.78 % (339353)Peak memory usage: 67 MB % 123.78/17.78 % (339353)Instructions burned: 20140 (million) % 123.78/17.78 % (339361)dis+33_16_sil=32000:sac=on:random_seed=750344021:i=15851:nm=0_2891 on theBenchmark for (2891ds/15851Mi) % 123.78/17.78 % (339347)Instruction limit reached! % 123.78/17.78 % (339347)------------------------------ % 123.78/17.78 % (339347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/17.78 % (339347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/17.78 % (339347)CaDiCaL version: 2.1.3 % 123.78/17.78 % (339347)Termination reason: Instruction limit % 123.78/17.78 % (339347)Termination phase: Saturation % 123.78/17.78 % (339347)Time elapsed: 9.379 s % 123.78/17.78 % (339347)Peak memory usage: 79 MB % 123.78/17.78 % (339347)Instructions burned: 22565 (million) % 123.78/17.78 % (339363)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2533857526:avsq=on:i=17627:add=on:amm=off_2876 on theBenchmark for (2876ds/17627Mi) % 147.42/21.08 % (339357)Instruction limit reached! % 147.42/21.08 % (339357)------------------------------ % 147.42/21.08 % (339357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339357)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339357)Termination reason: Instruction limit % 147.42/21.08 % (339357)Termination phase: Saturation % 147.42/21.08 % (339357)Time elapsed: 7.338 s % 147.42/21.08 % (339357)Peak memory usage: 47 MB % 147.42/21.08 % (339357)Instructions burned: 11404 (million) % 147.42/21.08 % (339365)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1223872880:s2a=on:i=53295_2871 on theBenchmark for (2871ds/53295Mi) % 147.42/21.08 % (339361)Instruction limit reached! % 147.42/21.08 % (339361)------------------------------ % 147.42/21.08 % (339361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339361)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339361)Termination reason: Instruction limit % 147.42/21.08 % (339361)Termination phase: Saturation % 147.42/21.08 % (339361)Time elapsed: 3.584 s % 147.42/21.08 % (339361)Peak memory usage: 30 MB % 147.42/21.08 % (339361)Instructions burned: 15853 (million) % 147.42/21.08 % (339367)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=856261214:i=26857:ins=20_2855 on theBenchmark for (2855ds/26857Mi) % 147.42/21.08 % (339367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.42/21.08 % (339367)Terminated due to inappropriate strategy. % 147.42/21.08 % (339367)------------------------------ % 147.42/21.08 % (339367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339367)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339367)Termination reason: Inappropriate % 147.42/21.08 % (339367)Time elapsed: 0.017 s % 147.42/21.08 % (339367)Peak memory usage: 13 MB % 147.42/21.08 % (339367)Instructions burned: 74 (million) % 147.42/21.08 % (339367)------------------------------ % 147.42/21.08 % (339367)------------------------------ % 147.42/21.08 % (339369)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3396046615:i=28120:bs=on:fsr=off_2854 on theBenchmark for (2854ds/28120Mi) % 147.42/21.08 % (339337)Instruction limit reached! % 147.42/21.08 % (339337)------------------------------ % 147.42/21.08 % (339337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339337)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339337)Termination reason: Instruction limit % 147.42/21.08 % (339337)Termination phase: Saturation % 147.42/21.08 % (339337)Time elapsed: 13.646 s % 147.42/21.08 % (339337)Peak memory usage: 31 MB % 147.42/21.08 % (339337)Instructions burned: 29342 (million) % 147.42/21.08 % (339371)fmb+10_1_sil=256000:fmbss=7:random_seed=3353803624:fmbsr=1.6:i=182295_2842 on theBenchmark for (2842ds/182295Mi) % 147.42/21.08 % (339371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.42/21.08 % (339371)Terminated due to inappropriate strategy. % 147.42/21.08 % (339371)------------------------------ % 147.42/21.08 % (339371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339371)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339371)Termination reason: Inappropriate % 147.42/21.08 % (339371)Time elapsed: 0.032 s % 147.42/21.08 % (339371)Peak memory usage: 13 MB % 147.42/21.08 % (339371)Instructions burned: 74 (million) % 147.42/21.08 % (339371)------------------------------ % 147.42/21.08 % (339371)------------------------------ % 147.42/21.08 % (339373)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=427167186:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi) % 147.42/21.08 % (339373)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.42/21.08 % (339373)Terminated due to inappropriate strategy. % 147.42/21.08 % (339373)------------------------------ % 147.42/21.08 % (339373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.42/21.08 % (339373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.42/21.08 % (339373)CaDiCaL version: 2.1.3 % 147.42/21.08 % (339373)Termination reason: Inappropriate % 154.51/22.09 % (339373)Time elapsed: 0.035 s % 154.51/22.09 % (339373)Peak memory usage: 14 MB % 154.51/22.09 % (339373)Instructions burned: 78 (million) % 154.51/22.09 % (339373)------------------------------ % 154.51/22.09 % (339373)------------------------------ % 154.51/22.09 % (339375)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1991811903:i=160505_2841 on theBenchmark for (2841ds/160505Mi) % 154.51/22.09 % (339375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.51/22.09 % (339375)Terminated due to inappropriate strategy. % 154.51/22.09 % (339375)------------------------------ % 154.51/22.09 % (339375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.51/22.09 % (339375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.51/22.09 % (339375)CaDiCaL version: 2.1.3 % 154.51/22.09 % (339375)Termination reason: Inappropriate % 154.51/22.09 % (339375)Time elapsed: 0.032 s % 154.51/22.09 % (339375)Peak memory usage: 13 MB % 154.51/22.09 % (339375)Instructions burned: 74 (million) % 154.51/22.09 % (339375)------------------------------ % 154.51/22.09 % (339375)------------------------------ % 154.51/22.09 % (339377)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3852888547:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 154.51/22.10 % (339377)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.51/22.10 % (339377)Terminated due to inappropriate strategy. % 154.51/22.10 % (339377)------------------------------ % 154.51/22.10 % (339377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.51/22.10 % (339377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.51/22.10 % (339377)CaDiCaL version: 2.1.3 % 154.51/22.10 % (339377)Termination reason: Inappropriate % 154.51/22.10 % (339377)Time elapsed: 0.043 s % 154.51/22.10 % (339377)Peak memory usage: 13 MB % 154.51/22.10 % (339377)Instructions burned: 104 (million) % 154.51/22.10 % (339377)------------------------------ % 154.51/22.10 % (339377)------------------------------ % 154.51/22.10 % (339379)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3911684101:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi) % 154.51/22.10 % (339379)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.51/22.10 % (339379)Terminated due to inappropriate strategy. % 154.51/22.10 % (339379)------------------------------ % 154.51/22.10 % (339379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.51/22.10 % (339379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.51/22.10 % (339379)CaDiCaL version: 2.1.3 % 154.51/22.10 % (339379)Termination reason: Inappropriate % 154.51/22.10 % (339379)Time elapsed: 0.043 s % 154.51/22.10 % (339379)Peak memory usage: 13 MB % 154.51/22.10 % (339379)Instructions burned: 104 (million) % 154.51/22.10 % (339379)------------------------------ % 154.51/22.10 % (339379)------------------------------ % 154.51/22.10 % (339381)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=916127871:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 154.51/22.10 % (339381)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.51/22.10 % (339381)Terminated due to inappropriate strategy. % 154.51/22.10 % (339381)------------------------------ % 154.51/22.10 % (339381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.51/22.10 % (339381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.51/22.10 % (339381)CaDiCaL version: 2.1.3 % 154.51/22.10 % (339381)Termination reason: Inappropriate % 154.51/22.10 % (339381)Time elapsed: 0.042 s % 154.51/22.10 % (339381)Peak memory usage: 14 MB % 154.51/22.10 % (339381)Instructions burned: 88 (million) % 154.51/22.10 % (339381)------------------------------ % 154.51/22.10 % (339381)------------------------------ % 154.51/22.10 % (339383)% WARNING: option uhcvi not known. % 154.51/22.10 % (339383)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1737128660:i=271062:add=off:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/271062Mi) % 154.51/22.10 % (339359)Instruction limit reached! % 154.51/22.10 % (339359)------------------------------ % 154.51/22.10 % (339359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.51/22.10 % (339359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.51/22.10 % (339359)CaDiCaL version: 2.1.3 % 154.51/22.10 % (339359)Termination reason: Instruction limit % 154.51/22.10 % (339359)Termination phase: Saturation % 154.51/22.10 % (339359)Time elapsed: 9.101 s % 154.51/22.10 % (339359)Peak memory usage: 53 MB % 154.51/22.10 % (339359)Instructions burned: 14135 (million) % 162.34/23.19 % (339385)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4051262701:i=176048:add=on:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/176048Mi) % 162.34/23.19 % (339369)Instruction limit reached! % 162.34/23.19 % (339369)------------------------------ % 162.34/23.19 % (339369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339369)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339369)Termination reason: Instruction limit % 162.34/23.19 % (339369)Termination phase: Saturation % 162.34/23.19 % (339369)Time elapsed: 5.950 s % 162.34/23.19 % (339369)Peak memory usage: 26 MB % 162.34/23.19 % (339369)Instructions burned: 28122 (million) % 162.34/23.19 % (339387)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4075593864:i=206:fgj=on:rtra=on_2795 on theBenchmark for (2795ds/206Mi) % 162.34/23.19 % (339387)Instruction limit reached! % 162.34/23.19 % (339387)------------------------------ % 162.34/23.19 % (339387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339387)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339387)Termination reason: Instruction limit % 162.34/23.19 % (339387)Termination phase: Saturation % 162.34/23.19 % (339387)Time elapsed: 0.056 s % 162.34/23.19 % (339387)Peak memory usage: 17 MB % 162.34/23.19 % (339387)Instructions burned: 209 (million) % 162.34/23.19 % (339389)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1357644211:i=232:rtra=on_2794 on theBenchmark for (2794ds/232Mi) % 162.34/23.19 % (339389)Instruction limit reached! % 162.34/23.19 % (339389)------------------------------ % 162.34/23.19 % (339389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339389)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339389)Termination reason: Instruction limit % 162.34/23.19 % (339389)Termination phase: Saturation % 162.34/23.19 % (339389)Time elapsed: 0.059 s % 162.34/23.19 % (339389)Peak memory usage: 17 MB % 162.34/23.19 % (339389)Instructions burned: 232 (million) % 162.34/23.19 % (339391)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4110370387:i=262:rtra=on_2793 on theBenchmark for (2793ds/262Mi) % 162.34/23.19 % (339391)Instruction limit reached! % 162.34/23.19 % (339391)------------------------------ % 162.34/23.19 % (339391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339391)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339391)Termination reason: Instruction limit % 162.34/23.19 % (339391)Termination phase: Saturation % 162.34/23.19 % (339391)Time elapsed: 0.064 s % 162.34/23.19 % (339391)Peak memory usage: 17 MB % 162.34/23.19 % (339391)Instructions burned: 263 (million) % 162.34/23.19 % (339393)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3337055573:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2792 on theBenchmark for (2792ds/318Mi) % 162.34/23.19 % (339393)Instruction limit reached! % 162.34/23.19 % (339393)------------------------------ % 162.34/23.19 % (339393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339393)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339393)Termination reason: Instruction limit % 162.34/23.19 % (339393)Termination phase: Saturation % 162.34/23.19 % (339393)Time elapsed: 0.087 s % 162.34/23.19 % (339393)Peak memory usage: 18 MB % 162.34/23.19 % (339393)Instructions burned: 321 (million) % 162.34/23.19 % (339395)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=260129446:i=1428:nm=2:rtra=on_2791 on theBenchmark for (2791ds/1428Mi) % 162.34/23.19 % (339395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.34/23.19 % (339395)Terminated due to inappropriate strategy. % 162.34/23.19 % (339395)------------------------------ % 162.34/23.19 % (339395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.34/23.19 % (339395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.34/23.19 % (339395)CaDiCaL version: 2.1.3 % 162.34/23.19 % (339395)Termination reason: Inappropriate % 162.34/23.19 % (339395)Time elapsed: 0.023 s % 162.34/23.19 % (339395)Peak memory usage: 14 MB % 162.34/23.19 % (339395)Instructions burned: 88 (million) % 162.34/23.19 % (339395)------------------------------ % 175.82/25.06 % (339395)------------------------------ % 175.82/25.06 % (339397)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3738623065:i=262:bd=preordered:rtra=on:fsd=on_2791 on theBenchmark for (2791ds/262Mi) % 175.82/25.06 % (339397)Instruction limit reached! % 175.82/25.06 % (339397)------------------------------ % 175.82/25.06 % (339397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339397)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339397)Termination reason: Instruction limit % 175.82/25.06 % (339397)Termination phase: Saturation % 175.82/25.06 % (339397)Time elapsed: 0.064 s % 175.82/25.06 % (339397)Peak memory usage: 16 MB % 175.82/25.06 % (339397)Instructions burned: 265 (million) % 175.82/25.06 % (339399)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=2545422462:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/1368Mi) % 175.82/25.06 % (339399)Instruction limit reached! % 175.82/25.06 % (339399)------------------------------ % 175.82/25.06 % (339399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339399)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339399)Termination reason: Instruction limit % 175.82/25.06 % (339399)Termination phase: Saturation % 175.82/25.06 % (339399)Time elapsed: 0.383 s % 175.82/25.06 % (339399)Peak memory usage: 21 MB % 175.82/25.06 % (339399)Instructions burned: 1368 (million) % 175.82/25.06 % (339401)ott-21_1_sil=16000:si=on:fs=off:random_seed=409083562:i=360:av=off:fsr=off:rtra=on_2786 on theBenchmark for (2786ds/360Mi) % 175.82/25.06 % (339401)Instruction limit reached! % 175.82/25.06 % (339401)------------------------------ % 175.82/25.06 % (339401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339401)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339401)Termination reason: Instruction limit % 175.82/25.06 % (339401)Termination phase: Saturation % 175.82/25.06 % (339401)Time elapsed: 0.096 s % 175.82/25.06 % (339401)Peak memory usage: 16 MB % 175.82/25.06 % (339401)Instructions burned: 362 (million) % 175.82/25.06 % (339403)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=706675870:i=954:bd=all:rtra=on_2785 on theBenchmark for (2785ds/954Mi) % 175.82/25.06 % (339403)Instruction limit reached! % 175.82/25.06 % (339403)------------------------------ % 175.82/25.06 % (339403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339403)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339403)Termination reason: Instruction limit % 175.82/25.06 % (339403)Termination phase: Saturation % 175.82/25.06 % (339403)Time elapsed: 0.297 s % 175.82/25.06 % (339403)Peak memory usage: 20 MB % 175.82/25.06 % (339403)Instructions burned: 956 (million) % 175.82/25.06 % (339405)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=122152581:fmbsr=1.3:i=1730:ins=25:rtra=on_2782 on theBenchmark for (2782ds/1730Mi) % 175.82/25.06 % (339405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.82/25.06 % (339405)Terminated due to inappropriate strategy. % 175.82/25.06 % (339405)------------------------------ % 175.82/25.06 % (339405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339405)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339405)Termination reason: Inappropriate % 175.82/25.06 % (339405)Time elapsed: 0.022 s % 175.82/25.06 % (339405)Peak memory usage: 14 MB % 175.82/25.06 % (339405)Instructions burned: 87 (million) % 175.82/25.06 % (339405)------------------------------ % 175.82/25.06 % (339405)------------------------------ % 175.82/25.06 % (339407)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4068550583:i=2358:rtra=on_2782 on theBenchmark for (2782ds/2358Mi) % 175.82/25.06 % (339363)Instruction limit reached! % 175.82/25.06 % (339363)------------------------------ % 175.82/25.06 % (339363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.82/25.06 % (339363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.82/25.06 % (339363)CaDiCaL version: 2.1.3 % 175.82/25.06 % (339363)Termination reason: Instruction limit % 227.38/32.35 % (339363)Termination phase: Saturation % 227.38/32.35 % (339363)Time elapsed: 9.492 s % 227.38/32.35 % (339363)Peak memory usage: 96 MB % 227.38/32.35 % (339363)Instructions burned: 17627 (million) % 227.38/32.35 % (339409)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1017936376:i=1778:ins=1:rtra=on_2781 on theBenchmark for (2781ds/1778Mi) % 227.38/32.35 % (339409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.38/32.35 % (339409)Terminated due to inappropriate strategy. % 227.38/32.35 % (339409)------------------------------ % 227.38/32.35 % (339409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.38/32.35 % (339409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.38/32.35 % (339409)CaDiCaL version: 2.1.3 % 227.38/32.35 % (339409)Termination reason: Inappropriate % 227.38/32.35 % (339409)Time elapsed: 0.058 s % 227.38/32.35 % (339409)Peak memory usage: 16 MB % 227.38/32.35 % (339409)Instructions burned: 117 (million) % 227.38/32.35 % (339409)------------------------------ % 227.38/32.35 % (339409)------------------------------ % 227.38/32.35 % (339411)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=479742735:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1384Mi) % 227.38/32.35 % (339407)Instruction limit reached! % 227.38/32.35 % (339407)------------------------------ % 227.38/32.35 % (339407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.38/32.35 % (339407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.38/32.35 % (339407)CaDiCaL version: 2.1.3 % 227.38/32.35 % (339407)Termination reason: Instruction limit % 227.38/32.35 % (339407)Termination phase: Saturation % 227.38/32.35 % (339407)Time elapsed: 0.822 s % 227.38/32.35 % (339407)Peak memory usage: 27 MB % 227.38/32.35 % (339407)Instructions burned: 2359 (million) % 227.38/32.35 % (339413)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=110433481:i=1758:kws=inv_precedence:fsr=off:rtra=on_2773 on theBenchmark for (2773ds/1758Mi) % 227.38/32.35 % (339411)Instruction limit reached! % 227.38/32.35 % (339411)------------------------------ % 227.38/32.35 % (339411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.38/32.35 % (339411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.38/32.35 % (339411)CaDiCaL version: 2.1.3 % 227.38/32.35 % (339411)Termination reason: Instruction limit % 227.38/32.35 % (339411)Termination phase: Saturation % 227.38/32.35 % (339411)Time elapsed: 0.826 s % 227.38/32.35 % (339411)Peak memory usage: 26 MB % 227.38/32.35 % (339411)Instructions burned: 1385 (million) % 227.38/32.35 % (339415)fmb+10_1_sil=64000:si=on:random_seed=2265366418:i=44122:nm=2:rtra=on:gsp=on_2772 on theBenchmark for (2772ds/44122Mi) % 227.38/32.35 % (339415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.38/32.35 % (339415)Terminated due to inappropriate strategy. % 227.38/32.35 % (339415)------------------------------ % 227.38/32.35 % (339415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.38/32.35 % (339415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.38/32.35 % (339415)CaDiCaL version: 2.1.3 % 227.38/32.35 % (339415)Termination reason: Inappropriate % 227.38/32.35 % (339415)Time elapsed: 0.046 s % 227.38/32.35 % (339415)Peak memory usage: 14 MB % 227.38/32.35 % (339415)Instructions burned: 95 (million) % 227.38/32.35 % (339415)------------------------------ % 227.38/32.35 % (339415)------------------------------ % 227.38/32.35 % (339417)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2789222324:i=19030:nm=5:rtra=on_2771 on theBenchmark for (2771ds/19030Mi) % 227.38/32.35 % (339417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.38/32.35 % (339417)Terminated due to inappropriate strategy. % 227.38/32.35 % (339417)------------------------------ % 227.38/32.35 % (339417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.38/32.35 % (339417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.38/32.35 % (339417)CaDiCaL version: 2.1.3 % 227.38/32.35 % (339417)Termination reason: Inappropriate % 227.38/32.35 % (339417)Time elapsed: 0.042 s % 227.38/32.35 % (339417)Peak memory usage: 14 MB % 227.38/32.35 % (339417)Instructions burned: 88 (million) % 227.38/32.35 % (339417)------------------------------ % 227.38/32.35 % (339417)------------------------------ % 227.38/32.35 % (339419)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2590287668:fmbsr=1.7:i=1840:rtra=on_2770 on theBenchmark for (2770ds/1840Mi) % 257.86/36.61 % (339419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.86/36.61 % (339419)Terminated due to inappropriate strategy. % 257.86/36.61 % (339419)------------------------------ % 257.86/36.61 % (339419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/36.61 % (339419)CaDiCaL version: 2.1.3 % 257.86/36.61 % (339419)Termination reason: Inappropriate % 257.86/36.61 % (339419)Time elapsed: 0.042 s % 257.86/36.61 % (339419)Peak memory usage: 14 MB % 257.86/36.61 % (339419)Instructions burned: 88 (million) % 257.86/36.61 % (339419)------------------------------ % 257.86/36.61 % (339419)------------------------------ % 257.86/36.61 % (339421)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3163531557:i=10262:rtra=on_2770 on theBenchmark for (2770ds/10262Mi) % 257.86/36.61 % (339413)Instruction limit reached! % 257.86/36.61 % (339413)------------------------------ % 257.86/36.61 % (339413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/36.61 % (339413)CaDiCaL version: 2.1.3 % 257.86/36.61 % (339413)Termination reason: Instruction limit % 257.86/36.61 % (339413)Termination phase: Saturation % 257.86/36.61 % (339413)Time elapsed: 0.540 s % 257.86/36.61 % (339413)Peak memory usage: 28 MB % 257.86/36.61 % (339413)Instructions burned: 1761 (million) % 257.86/36.61 % (339423)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3031702761:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2768 on theBenchmark for (2768ds/2944Mi) % 257.86/36.61 % (339423)Instruction limit reached! % 257.86/36.61 % (339423)------------------------------ % 257.86/36.61 % (339423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/36.61 % (339423)CaDiCaL version: 2.1.3 % 257.86/36.61 % (339423)Termination reason: Instruction limit % 257.86/36.61 % (339423)Termination phase: Saturation % 257.86/36.61 % (339423)Time elapsed: 0.965 s % 257.86/36.61 % (339423)Peak memory usage: 36 MB % 257.86/36.61 % (339423)Instructions burned: 2945 (million) % 257.86/36.61 % (339425)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=205875271:i=12648:rtra=on_2758 on theBenchmark for (2758ds/12648Mi) % 257.86/36.61 % (339425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.86/36.61 % (339425)Terminated due to inappropriate strategy. % 257.86/36.61 % (339425)------------------------------ % 257.86/36.61 % (339425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/36.61 % (339425)CaDiCaL version: 2.1.3 % 257.86/36.61 % (339425)Termination reason: Inappropriate % 257.86/36.61 % (339425)Time elapsed: 0.023 s % 257.86/36.61 % (339425)Peak memory usage: 14 MB % 257.86/36.61 % (339425)Instructions burned: 88 (million) % 257.86/36.61 % (339425)------------------------------ % 257.86/36.61 % (339425)------------------------------ % 257.86/36.61 % (339427)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=197489268:fmbsr=2.30978:i=4348:rtra=on_2758 on theBenchmark for (2758ds/4348Mi) % 257.86/36.61 % (339427)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.86/36.61 % (339427)Terminated due to inappropriate strategy. % 257.86/36.61 % (339427)------------------------------ % 257.86/36.61 % (339427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/36.61 % (339427)CaDiCaL version: 2.1.3 % 257.86/36.61 % (339427)Termination reason: Inappropriate % 257.86/36.61 % (339427)Time elapsed: 0.023 s % 257.86/36.61 % (339427)Peak memory usage: 14 MB % 257.86/36.61 % (339427)Instructions burned: 88 (million) % 257.86/36.61 % (339427)------------------------------ % 257.86/36.61 % (339427)------------------------------ % 257.86/36.61 % (339429)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=362283390:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2757 on theBenchmark for (2757ds/1738Mi) % 257.86/36.61 % (339429)Instruction limit reached! % 257.86/36.61 % (339429)------------------------------ % 257.86/36.61 % (339429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.86/36.61 % (339429)Linked with Z3 4.14.0.0 3c4Terminated % 300.50/42.64 % Vampire exiting %------------------------------------------------------------------------------