TIME: 920


SCC: 9 (loops closed under composition)
=================================
  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [1*D>=0,1*C>=1,B>D,1*B>=1,C=A,1*A>=1]
  RF: 1*B

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [1*D>=2,D>C,1*C>=0,D>B,1*B>=1,D>A,A>C,1*A>=1]
  RF: 1*A

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [1*D=<1,1*D>=1,1*C>=0,D>B,C>=B,1*B=<0,A>=D,A>C,A>B,1*A>=1]
  RF: -1*B+1

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

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [1*A>=1,1*A+ -1*C>0,1*C>=0,1*B>=1,1*D=1]
  RF: 1*A

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [1*B>=1,1*D>=0,1*C>=1,1*A+ -1*C>0]
  RF: 1*A+ -1

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

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [-1*B>=0,1*A+ -1*C>0,1*C>=1,-1*D> -1,1*D>=0]
  RF: 1*A+ -1

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

  Ackermann_ack(II)I(A,B) :- Ackermann_ack(II)I(C,D) [-1*B>=0,1*D>=0,1*A+ -1*C>0,1*C>=1]
  RF: 1*A+ -1

=================================