I actually read this. You expanded the clue into a very simplified form and worked it out rather well. Since the negation of an XOR is a biconditional, I can't fault your logic. Thanks.
Here's how I worked it out from my list of things I get from the two clues:
1) Vestor is 714,000 or PLC120
...
5) 47lightyears is Vestor or 650,000
...
8) PLC120 is not 47lightyears
Substituting #1 into #5 I get:
47 is 714,000 or PLC120 or 650,000
Applying #8 eliminates PLC120:
47 is 714,000 or 650,000
Mine is simple in English, but yours is more of a proof of why mine works. Given my screwup with the tautology approach, I'll take all the help I can get.
