YES

Problem:
 F(x,x) -> G(x)
 A() -> B()

Proof:
 Polynomial Interpretation Processor:
  dimension: 1
  interpretation:
   [B] = 0,
   
   [A] = 1,
   
   [G](x0) = -2x0 + 7x0x0,
   
   [F](x0, x1) = x0 + -1x1 + 7x0x1 + 1
  orientation:
   F(x,x) = 7x*x + 1 >= -2x + 7x*x = G(x)
   
   A() = 1 >= 0 = B()
  problem:
   
  Qed