System BV is NP-complete

System is an extension of multiplicative linear logic () with the rules mix, nullary mix, and a self-dual, noncommutative logical operator, called seq. While the rules mix and nullary mix extend the deductive system, the operator seq extends the language of . Due to the operator seq, system extends the applications of to those where the sequential composition is crucial, e.g., concurrency theory. System is an extension of with the rules mix and nullary mix. In this paper, by relying on the fact that system is a conservative extension of system , I show that system is NP-complete by encoding the 3-Partition problem in . I provide a simple completeness proof of this encoding by resorting to a novel proof theoretical method for reducing nondeterminism in proof search, which is also of independent interest.