cer_precond = []
x, y, z = Consts('x y z', PeopleSort)
cer_precond.append(ForAll([x, y], (x == y) == (R(x, y) == self)))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == brother), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == sister), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == brother), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == sister), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == sister), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == brother), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == sister), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == brother), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == aunt), Or(R(x, z) == daughter, R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == uncle), Or(R(x, z) == son, R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == aunt), Or(R(x, z) == daughter, R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == uncle), Or(R(x, z) == son, R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == father), Or(R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == grandfather), Or(R(x, z) == father, R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == mother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == brother), Or(R(x, z) == father, R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == father), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == sister), Or(R(x, z) == mother, R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == daughter_in_law), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == daughter_in_law), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == son_in_law), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == son_in_law), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == grandson), Or(R(x, z) == son, R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == granddaughter), Or(R(x, z) == daughter, R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == grandmother), Or(R(x, z) == mother, R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == grandfather), Or(R(x, z) == father, R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == mother), Or(R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == father), Or(R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == niece), Or(R(x, z) == daughter, R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == nephew), Or(R(x, z) == son, R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == grandmother), Or(R(x, z) == wife))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == grandfather), Or(R(x, z) == husband))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == granddaughter), Or(R(x, z) == daughter, R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == grandson), Or(R(x, z) == son, R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == mother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == brother), Or(R(x, z) == father, R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == father), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == sister), Or(R(x, z) == mother, R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == uncle), Or(R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == aunt), Or(R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == niece), Or(R(x, z) == daughter, R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == nephew), Or(R(x, z) == son, R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == uncle), Or(R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == aunt), Or(R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == father), Or(R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == mother), Or(R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == mother), Or(R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == father), Or(R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == mother), Or(R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother_in_law, R(y, z) == daughter), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father_in_law, R(y, z) == daughter), Or(R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == husband), Or(R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == wife), Or(R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother_in_law, R(y, z) == son), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == grandmother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == grandfather), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == grandmother), Or(R(x, z) == mother, R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == uncle), Or(R(x, z) == brother, R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == niece, R(y, z) == aunt), Or(R(x, z) == sister, R(x, z) == wife, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == uncle), Or(R(x, z) == husband, R(x, z) == brother, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == nephew, R(y, z) == aunt), Or(R(x, z) == wife, R(x, z) == sister, R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == uncle), Or(R(x, z) == father, R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == aunt), Or(R(x, z) == mother, R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == grandfather), Or(R(x, z) == husband))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == grandmother), Or(R(x, z) == wife))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == mother), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == father), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == sister), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == cousin, R(y, z) == brother), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father_in_law, R(y, z) == son), Or(R(x, z) == husband, R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == father), Or(R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == mother), Or(R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == son), Or(R(x, z) == son))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == daughter), Or(R(x, z) == daughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == brother), Or(R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == sister), Or(R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == mother_in_law), Or(R(x, z) == mother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == father_in_law), Or(R(x, z) == father))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == son_in_law), Or(R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == daughter_in_law), Or(R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == grandson), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == husband, R(y, z) == granddaughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == father), Or(R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == mother), Or(R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == son), Or(R(x, z) == son))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == daughter), Or(R(x, z) == daughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == brother), Or(R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == sister), Or(R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == mother_in_law), Or(R(x, z) == mother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == father_in_law), Or(R(x, z) == father))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == son_in_law), Or(R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == daughter_in_law), Or(R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == grandson), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == wife, R(y, z) == granddaughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == father), Or(R(x, z) == husband))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == mother), Or(R(x, z) == wife))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == brother), Or(R(x, z) == son))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == sister), Or(R(x, z) == daughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == son), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == daughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == wife), Or(R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == grandfather), Or(R(x, z) == father, R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son, R(y, z) == grandmother), Or(R(x, z) == mother, R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == father), Or(R(x, z) == husband))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == mother), Or(R(x, z) == wife))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == brother), Or(R(x, z) == son))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == sister), Or(R(x, z) == daughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == son), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == daughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == husband), Or(R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == grandfather), Or(R(x, z) == father, R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter, R(y, z) == grandmother), Or(R(x, z) == mother, R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == father), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == mother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == wife), Or(R(x, z) == mother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == son), Or(R(x, z) == brother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == daughter), Or(R(x, z) == sister))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == sister), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == brother), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == father_in_law), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father, R(y, z) == mother_in_law), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == father), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == mother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == husband), Or(R(x, z) == father))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == son), Or(R(x, z) == brother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == daughter), Or(R(x, z) == sister))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == brother), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == sister), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == father_in_law), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother, R(y, z) == mother_in_law), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == brother), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == sister), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == father), Or(R(x, z) == son, R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandson, R(y, z) == mother), Or(R(x, z) == daughter, R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == brother), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == sister), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == father), Or(R(x, z) == son, R(x, z) == son_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == granddaughter, R(y, z) == mother), Or(R(x, z) == daughter, R(x, z) == daughter_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == grandmother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == grandfather), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == father), Or(R(x, z) == father))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == mother), Or(R(x, z) == mother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == wife), Or(R(x, z) == sister_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == son), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == daughter), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == brother), Or(R(x, z) == brother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == sister), Or(R(x, z) == sister))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == uncle), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother, R(y, z) == aunt), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == grandmother), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == grandfather), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == father), Or(R(x, z) == father))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == mother), Or(R(x, z) == mother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == husband), Or(R(x, z) == brother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == son), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == daughter), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == brother), Or(R(x, z) == brother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == sister), Or(R(x, z) == sister))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == uncle), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister, R(y, z) == aunt), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandfather, R(y, z) == wife), Or(R(x, z) == grandmother))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandfather, R(y, z) == son), Or(R(x, z) == father, R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandfather, R(y, z) == daughter), Or(R(x, z) == mother, R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandmother, R(y, z) == husband), Or(R(x, z) == grandfather))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandmother, R(y, z) == son), Or(R(x, z) == father, R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == grandmother, R(y, z) == daughter), Or(R(x, z) == mother, R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son_in_law, R(y, z) == son), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == son_in_law, R(y, z) == daughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter_in_law, R(y, z) == son), Or(R(x, z) == grandson))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == daughter_in_law, R(y, z) == daughter), Or(R(x, z) == granddaughter))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == mother_in_law, R(y, z) == husband), Or(R(x, z) == father_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == father_in_law, R(y, z) == wife), Or(R(x, z) == mother_in_law))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == son), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == son), Or(R(x, z) == nephew))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == brother_in_law, R(y, z) == daughter), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == sister_in_law, R(y, z) == daughter), Or(R(x, z) == niece))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == wife), Or(R(x, z) == aunt))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == son), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == uncle, R(y, z) == daughter), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == husband), Or(R(x, z) == uncle))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == son), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(x != z, R(x, y) == aunt, R(y, z) == daughter), Or(R(x, z) == cousin))))
cer_precond.append(ForAll([x, y, z], Implies(And(R(x, y) == father, R(x, z) == father), y == z)))
cer_precond.append(ForAll([x, y, z], Implies(And(R(x, y) == mother, R(x, z) == mother), y == z)))
cer_precond.append(ForAll([x, y, z], Implies(And(R(x, y) == husband, R(x, z) == husband), y == z)))
cer_precond.append(ForAll([x, y, z], Implies(And(R(x, y) == wife, R(x, z) == wife), y == z)))
cer_precond.append(ForAll([x, y], Or(R(x, y) == father, R(x, y) == mother) == Or(R(y, x) == son, R(y, x) == daughter)))
cer_precond.append(ForAll([x, y], Or(R(x, y) == brother, R(x, y) == sister) == Or(R(y, x) == brother, R(y, x) == sister)))
cer_precond.append(ForAll([x, y], Or(R(x, y) == husband) == Or(R(y, x) == wife)))
