Input TRS:
    1: le(s(s(x)),s(s(y))) -> le(s(x),s(y))
    2: le(s(s(x)),s(s(y))) -> le(x,y)
    3: le(|0|(),y) ->= true()
    4: le(s(x),|0|()) ->= false()
    5: le(s(x),s(y)) ->= le(x,y)
    6: le(s(s(x)),s(s(y))) ->= le(x,y)
    7: pred(s(x)) ->= x
    8: minus(x,|0|()) ->= x
    9: minus(x,s(y)) ->= pred(minus(x,y))
    10: gcd(|0|(),y) ->= y
    11: gcd(s(x),|0|()) ->= s(x)
    12: gcd(s(x),s(y)) ->= if_gcd(le(y,x),s(x),s(y))
    13: if_gcd(true(),s(x),s(y)) ->= gcd(minus(x,y),s(y))
    14: if_gcd(false(),s(x),s(y)) ->= gcd(minus(y,x),s(x))
    15: if_gcd(error(),x,y) ->= if_gcd(error(),|0|(),|0|())
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Freezing if_gcd le
1: le❆1_s(s(x),s(s(y))) -> le❆1_s(x,s(y))
2: le❆1_s(s(x),s(s(y))) -> le(x,y)
3: le❆1_|0|(y) ->= true()
4: le❆1_s(x,|0|()) ->= false()
5: le❆1_s(x,s(y)) ->= le(x,y)
6: le❆1_s(s(x),s(s(y))) ->= le(x,y)
7: pred(s(x)) ->= x
8: minus(x,|0|()) ->= x
9: minus(x,s(y)) ->= pred(minus(x,y))
10: gcd(|0|(),y) ->= y
11: gcd(s(x),|0|()) ->= s(x)
12: gcd(s(x),s(y)) ->= if_gcd(le(y,x),s(x),s(y))
13: if_gcd❆1_true(s(x),s(y)) ->= gcd(minus(x,y),s(y))
14: if_gcd❆1_false(s(x),s(y)) ->= gcd(minus(y,x),s(x))
15: if_gcd❆1_error(x,y) ->= if_gcd❆1_error(|0|(),|0|())
16: le(|0|(),_1) ->= le❆1_|0|(_1)
17: le(s(_1),_2) ->= le❆1_s(_1,_2)
18: if_gcd(error(),_2,_3) ->= if_gcd❆1_error(_2,_3)
19: if_gcd(false(),_2,_3) ->= if_gcd❆1_false(_2,_3)
20: if_gcd(true(),_2,_3) ->= if_gcd❆1_true(_2,_3)
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #le❆1_s(s(x),s(s(y))) -> #le(x,y)
   #2: #le❆1_s(s(x),s(s(y))) ->? #le(x,y)
   #3: #if_gcd❆1_true(s(x),s(y)) ->? #gcd(minus(x,y),s(y))
   #4: #gcd(s(x),s(y)) ->? #if_gcd(le(y,x),s(x),s(y))
   #5: #gcd(s(x),s(y)) ->? #le(y,x)
   #6: #if_gcd❆1_false(s(x),s(y)) ->? #gcd(minus(y,x),s(x))
   #7: #if_gcd(true(),_2,_3) ->? #if_gcd❆1_true(_2,_3)
   #8: #le❆1_s(x,s(y)) ->? #le(x,y)
   #9: #le(s(_1),_2) ->? #le❆1_s(_1,_2)
   #10: #if_gcd(false(),_2,_3) ->? #if_gcd❆1_false(_2,_3)
   #11: #le❆1_s(s(x),s(s(y))) -> #le❆1_s(x,s(y))
Number of SCCs: 2, DPs: 10, edges: 17
	SCC { #1 #2 #8 #9 #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
  #le(x1,x2)	weight: (/ 1 8) + x2
if_gcd❆1_error(x1,x2)	weight: 0
 minus(x1,x2)	weight: 0
   gcd(x1,x2)	weight: 0
 false()	weight: 0
  true()	weight: 0
  pred(x1)	weight: 0
le❆1_s(x1,x2)	weight: 0
 error()	weight: 0
#if_gcd❆1_false(x1,x2)	weight: 0
le❆1_|0|(x1)	weight: 0
#if_gcd❆1_true(x1,x2)	weight: 0
#le❆1_s(x1,x2)	weight: x2
if_gcd(x1,x2,x3)	weight: 0
if_gcd❆1_false(x1,x2)	weight: 0
#if_gcd(x1,x2,x3)	weight: 0
if_gcd❆1_true(x1,x2)	weight: 0
 #gcd(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #1 #2 #8 #9 #11
Number of SCCs: 1, DPs: 5, edges: 6
	SCC { #3 #4 #6 #7 #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: (/ 1 16) + x2
     s(x1)	weight: (/ 1 4) + x1
  #le(x1,x2)	weight: (/ 1 16)
if_gcd❆1_error(x1,x2)	weight: 0
 minus(x1,x2)	weight: (/ 1 16) + x1
   gcd(x1,x2)	weight: 0
 false()	weight: 0
  true()	weight: 0
  pred(x1)	weight: x1
le❆1_s(x1,x2)	weight: 0
 error()	weight: 0
#if_gcd❆1_false(x1,x2)	weight: x1 + x2
le❆1_|0|(x1)	weight: (/ 1 8)
#if_gcd❆1_true(x1,x2)	weight: x1 + x2
#le❆1_s(x1,x2)	weight: 0
if_gcd(x1,x2,x3)	weight: 0
if_gcd❆1_false(x1,x2)	weight: 0
#if_gcd(x1,x2,x3)	weight: (/ 1 16) + x2 + x3
if_gcd❆1_true(x1,x2)	weight: 0
 #gcd(x1,x2)	weight: (/ 1 8) + x1 + x2
    Usable rules: { 7..9 }
    Removed DPs: #3 #4 #6 #7 #10
Number of SCCs: 0, DPs: 0, edges: 0
YES