UPDATED: This problem now uses a grading server instead of asking for the size of the CNF.

I've got a task for you involving a program language I've created! It's called Prop (short for Proposition), and as you might expect, it's a simple language for propositional logic. It consists of the following expressions (denoted e):

Boolean constants, written true and false.
Boolean variables, written as any alphabetical string.
Implies, written e -> e.
Equivalence, written e <-> e.
Negation, written !e.
And, written e && e.
Or, written e || e.

You can also parenthesize any expressions or subexpressions (so, you can write (a || b) && c). Here's another example program:

(a || b) && c && d && (!d || b) || (b -> c) && (d <-> a)

So, what I'd like from you is for you to calculate the conjunctive normal form (CNF) of the attached program. You can submit the CNF here