Changed isSingleAtom method to isDefinite to better reflect its purpose. Added logic to manually expand F <-> G into a conjuction of implications to get around F2LP's incompatibility with equivalence in the body of the rule.