G (a -> (X b))
G (b -> (X a))
a
G ( (b | (X a)) -> p ) 
F (- p)
p