TIME: 300


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

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

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

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

SCC: 20
=================================
Global Ranking Function: nat(1*B)

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