TIME: 520


SCC: 18
=================================
Global Ranking Function: nat(1*B+ -1)

  AProVEMathRecursive_power(II)I(A,B) :- AProVEMathRecursive_power(II)I(C,D) [-1*A>= -1,1*D>=1,1*A+ -1*C=0,1*B+ -1*D=1]
  AProVEMathRecursive_power(II)I(A,B) :- AProVEMathRecursive_power(II)I(C,D) [-1*A>= -1,1*B>=2,-1*B+2*D>= -1,1*B+ -2*D>=0,1*A+ -1*C=0]
  AProVEMathRecursive_power(II)I(A,B) :- AProVEMathRecursive_power(II)I(C,D) [1*B>=2,1*A>=3,1*A+ -1*C=0,1*B+ -1*D=1]
  AProVEMathRecursive_power(II)I(A,B) :- AProVEMathRecursive_power(II)I(C,D) [1*B>=2,1*A>=3,-1*B+2*D>= -1,1*B+ -2*D>=0,1*A+ -1*C=0]
=================================