If either A-2017 is both with a resolution of 1080p and produced by AOC or it is neither, then it is not equipped in the library.
¬(ResolutionLessThan(a-2017, p1080) ⊕ ProducedBy(x, aOC)) → ¬(In(a-2017, library))