A Few Pointers

Make sure your CTL formulae refer to the Blifmv variable names (These are not the same as Verilog names).
Use the ordering file provided.
Remember that latched variables are output at the next clock cycle, but wires are output immediately.
Keep in mind your property may be wrongly formulated.