Input TRS:
    1: a__from(X) -> cons(mark(X),from(s(X)))
    2: a__2ndspos(|0|(),Z) -> rnil()
    3: a__2ndspos(s(N),cons(X,Z)) -> a__2ndspos(s(mark(N)),cons2(X,mark(Z)))
    4: a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))
    5: a__2ndsneg(|0|(),Z) -> rnil()
    6: a__2ndsneg(s(N),cons(X,Z)) -> a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))
    7: a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))
    8: a__pi(X) -> a__2ndspos(mark(X),a__from(|0|()))
    9: a__plus(|0|(),Y) -> mark(Y)
    10: a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y)))
    11: a__times(|0|(),Y) -> |0|()
    12: a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y)))
    13: a__square(X) -> a__times(mark(X),mark(X))
    14: mark(from(X)) -> a__from(mark(X))
    15: mark(|2ndspos|(X1,X2)) -> a__2ndspos(mark(X1),mark(X2))
    16: mark(|2ndsneg|(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2))
    17: mark(pi(X)) -> a__pi(mark(X))
    18: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    19: mark(times(X1,X2)) -> a__times(mark(X1),mark(X2))
    20: mark(square(X)) -> a__square(mark(X))
    21: mark(|0|()) -> |0|()
    22: mark(s(X)) -> s(mark(X))
    23: mark(posrecip(X)) -> posrecip(mark(X))
    24: mark(negrecip(X)) -> negrecip(mark(X))
    25: mark(nil()) -> nil()
    26: mark(cons(X1,X2)) -> cons(mark(X1),X2)
    27: mark(cons2(X1,X2)) -> cons2(X1,mark(X2))
    28: mark(rnil()) -> rnil()
    29: mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2))
    30: a__from(X) -> from(X)
    31: a__2ndspos(X1,X2) -> |2ndspos|(X1,X2)
    32: a__2ndsneg(X1,X2) -> |2ndsneg|(X1,X2)
    33: a__pi(X) -> pi(X)
    34: a__plus(X1,X2) -> plus(X1,X2)
    35: a__times(X1,X2) -> times(X1,X2)
    36: a__square(X) -> square(X)
Number of strict rules: 36
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #mark(rcons(X1,X2)) -> #mark(X1)
   #2: #mark(rcons(X1,X2)) -> #mark(X2)
   #3: #a__2ndsneg(s(N),cons(X,Z)) -> #a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))
   #4: #a__2ndsneg(s(N),cons(X,Z)) -> #mark(N)
   #5: #a__2ndsneg(s(N),cons(X,Z)) -> #mark(Z)
   #6: #a__square(X) -> #a__times(mark(X),mark(X))
   #7: #a__square(X) -> #mark(X)
   #8: #a__square(X) -> #mark(X)
   #9: #a__plus(|0|(),Y) -> #mark(Y)
   #10: #mark(negrecip(X)) -> #mark(X)
   #11: #mark(posrecip(X)) -> #mark(X)
   #12: #a__times(s(X),Y) -> #a__plus(mark(Y),a__times(mark(X),mark(Y)))
   #13: #a__times(s(X),Y) -> #mark(Y)
   #14: #a__times(s(X),Y) -> #a__times(mark(X),mark(Y))
   #15: #a__times(s(X),Y) -> #mark(X)
   #16: #a__times(s(X),Y) -> #mark(Y)
   #17: #mark(from(X)) -> #a__from(mark(X))
   #18: #mark(from(X)) -> #mark(X)
   #19: #mark(square(X)) -> #a__square(mark(X))
   #20: #mark(square(X)) -> #mark(X)
   #21: #a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> #mark(Y)
   #22: #a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> #a__2ndspos(mark(N),mark(Z))
   #23: #a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> #mark(N)
   #24: #a__2ndsneg(s(N),cons2(X,cons(Y,Z))) -> #mark(Z)
   #25: #a__plus(s(X),Y) -> #a__plus(mark(X),mark(Y))
   #26: #a__plus(s(X),Y) -> #mark(X)
   #27: #a__plus(s(X),Y) -> #mark(Y)
   #28: #mark(s(X)) -> #mark(X)
   #29: #mark(cons2(X1,X2)) -> #mark(X2)
   #30: #mark(pi(X)) -> #a__pi(mark(X))
   #31: #mark(pi(X)) -> #mark(X)
   #32: #mark(times(X1,X2)) -> #a__times(mark(X1),mark(X2))
   #33: #mark(times(X1,X2)) -> #mark(X1)
   #34: #mark(times(X1,X2)) -> #mark(X2)
   #35: #mark(cons(X1,X2)) -> #mark(X1)
   #36: #mark(|2ndsneg|(X1,X2)) -> #a__2ndsneg(mark(X1),mark(X2))
   #37: #mark(|2ndsneg|(X1,X2)) -> #mark(X1)
   #38: #mark(|2ndsneg|(X1,X2)) -> #mark(X2)
   #39: #a__2ndspos(s(N),cons(X,Z)) -> #a__2ndspos(s(mark(N)),cons2(X,mark(Z)))
   #40: #a__2ndspos(s(N),cons(X,Z)) -> #mark(N)
   #41: #a__2ndspos(s(N),cons(X,Z)) -> #mark(Z)
   #42: #a__from(X) -> #mark(X)
   #43: #a__pi(X) -> #a__2ndspos(mark(X),a__from(|0|()))
   #44: #a__pi(X) -> #mark(X)
   #45: #a__pi(X) -> #a__from(|0|())
   #46: #mark(|2ndspos|(X1,X2)) -> #a__2ndspos(mark(X1),mark(X2))
   #47: #mark(|2ndspos|(X1,X2)) -> #mark(X1)
   #48: #mark(|2ndspos|(X1,X2)) -> #mark(X2)
   #49: #a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> #mark(Y)
   #50: #a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> #a__2ndsneg(mark(N),mark(Z))
   #51: #a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> #mark(N)
   #52: #a__2ndspos(s(N),cons2(X,cons(Y,Z))) -> #mark(Z)
   #53: #mark(plus(X1,X2)) -> #a__plus(mark(X1),mark(X2))
   #54: #mark(plus(X1,X2)) -> #mark(X1)
   #55: #mark(plus(X1,X2)) -> #mark(X2)
Number of SCCs: 1, DPs: 55, edges: 1024
	SCC { #1..55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: 0
a__plus(x1,x2)	weight: max{x2, x1}
a__2ndsneg(x1,x2)	weight: max{(/ 1 2) + x2, x1}
negrecip(x1)	weight: (/ 1 4) + x1
     s(x1)	weight: x1
#a__pi(x1)	weight: (/ 1 4) + x1
#a__from(x1)	weight: (/ 1 4) + x1
a__from(x1)	weight: x1
  rnil()	weight: (/ 1 2)
|2ndspos|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
square(x1)	weight: x1
#a__times(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
    pi(x1)	weight: (/ 1 2) + x1
 rcons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
a__2ndspos(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__2ndsneg(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
|2ndsneg|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__plus(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
#mark(x1)	weight: (/ 1 4) + x1
  from(x1)	weight: x1
 times(x1,x2)	weight: max{x2, x1}
 a__pi(x1)	weight: (/ 1 2) + x1
   nil()	weight: (/ 1 4)
  mark(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, x1}
 cons2(x1,x2)	weight: max{x2, x1}
a__square(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, x1}
a__times(x1,x2)	weight: max{x2, x1}
#a__square(x1)	weight: (/ 1 4) + x1
#a__2ndspos(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
posrecip(x1)	weight: (/ 1 4) + x1
    Usable rules: { 1..36 }
    Removed DPs: #1 #10 #11 #30 #31 #38 #48
Number of SCCs: 1, DPs: 45, edges: 625
	SCC { #2..9 #12..29 #32..37 #39..42 #46 #47 #49..55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: 0
a__plus(x1,x2)	weight: max{x2, x1}
a__2ndsneg(x1,x2)	weight: max{(/ 1 2) + x2, x1}
negrecip(x1)	weight: (/ 1 4) + x1
     s(x1)	weight: x1
#a__pi(x1)	weight: (/ 1 4) + x1
#a__from(x1)	weight: (/ 1 4) + x1
a__from(x1)	weight: x1
  rnil()	weight: (/ 1 2)
|2ndspos|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
square(x1)	weight: x1
#a__times(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
    pi(x1)	weight: (/ 1 2) + x1
 rcons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
a__2ndspos(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__2ndsneg(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
|2ndsneg|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__plus(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
#mark(x1)	weight: (/ 1 4) + x1
  from(x1)	weight: x1
 times(x1,x2)	weight: max{x2, x1}
 a__pi(x1)	weight: (/ 1 2) + x1
   nil()	weight: (/ 1 4)
  mark(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, x1}
 cons2(x1,x2)	weight: max{x2, x1}
a__square(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, x1}
a__times(x1,x2)	weight: max{x2, x1}
#a__square(x1)	weight: (/ 1 4) + x1
#a__2ndspos(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
posrecip(x1)	weight: (/ 1 4) + x1
    Usable rules: { 1..36 }
    Removed DPs: #5 #21 #24 #41 #49 #52
Number of SCCs: 1, DPs: 39, edges: 501
	SCC { #2..4 #6..9 #12..20 #22 #23 #25..29 #32..37 #39 #40 #42 #46 #47 #50 #51 #53..55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: 0
a__plus(x1,x2)	weight: max{x2, x1}
a__2ndsneg(x1,x2)	weight: max{(/ 1 2) + x2, x1}
negrecip(x1)	weight: (/ 1 4) + x1
     s(x1)	weight: x1
#a__pi(x1)	weight: (/ 1 4) + x1
#a__from(x1)	weight: (/ 1 2) + x1
a__from(x1)	weight: x1
  rnil()	weight: (/ 1 2)
|2ndspos|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
square(x1)	weight: (/ 1 2) + x1
#a__times(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 2) + x1}
    pi(x1)	weight: (/ 1 2) + x1
 rcons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
a__2ndspos(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__2ndsneg(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 2) + x1}
|2ndsneg|(x1,x2)	weight: max{(/ 1 2) + x2, x1}
#a__plus(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 2) + x1}
#mark(x1)	weight: (/ 1 2) + x1
  from(x1)	weight: x1
 times(x1,x2)	weight: max{x2, x1}
 a__pi(x1)	weight: (/ 1 2) + x1
   nil()	weight: (/ 1 4)
  mark(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, x1}
 cons2(x1,x2)	weight: max{x2, x1}
a__square(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: max{x2, x1}
a__times(x1,x2)	weight: max{x2, x1}
#a__square(x1)	weight: (/ 3 4) + x1
#a__2ndspos(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 2) + x1}
posrecip(x1)	weight: (/ 1 4) + x1
    Usable rules: { 1..36 }
    Removed DPs: #6..8 #19 #20
Number of SCCs: 1, DPs: 34, edges: 395
	SCC { #2..4 #9 #12..18 #22 #23 #25..29 #32..37 #39 #40 #42 #46 #47 #50 #51 #53..55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: 0
a__plus(x1,x2)	weight: max{x2, x1}
a__2ndsneg(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
negrecip(x1)	weight: (/ 1 8)
     s(x1)	weight: x1
#a__pi(x1)	weight: (/ 1 8) + x1
#a__from(x1)	weight: (/ 1 4) + x1
a__from(x1)	weight: x1
  rnil()	weight: (/ 3 8)
|2ndspos|(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
square(x1)	weight: (/ 1 4) + x1
#a__times(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
    pi(x1)	weight: (/ 1 2) + x1
 rcons(x1,x2)	weight: max{x2, (/ 3 8) + x1}
a__2ndspos(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
#a__2ndsneg(x1,x2)	weight: max{(/ 5 8) + x2, (/ 3 8) + x1}
|2ndsneg|(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
#a__plus(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
#mark(x1)	weight: (/ 1 4) + x1
  from(x1)	weight: x1
 times(x1,x2)	weight: max{x2, x1}
 a__pi(x1)	weight: (/ 1 2) + x1
   nil()	weight: (/ 1 8)
  mark(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, x1}
 cons2(x1,x2)	weight: max{x2, x1}
a__square(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: max{x2, x1}
a__times(x1,x2)	weight: max{x2, x1}
#a__square(x1)	weight: (/ 3 8) + x1
#a__2ndspos(x1,x2)	weight: max{(/ 5 8) + x2, (/ 3 8) + x1}
posrecip(x1)	weight: (/ 1 8) + x1
    Usable rules: { 1..36 }
    Removed DPs: #4 #23 #36 #37 #40 #46 #47 #51
Number of SCCs: 2, DPs: 26, edges: 221
	SCC { #3 #22 #39 #50 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above: rnil
a__plus(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s rnil rcons |2ndsneg| mark plus cons
a__2ndsneg(x1,x2)	status: [x1]	precedence above: negrecip rnil rcons |2ndsneg| cons
negrecip(x1)	status: []	precedence above: cons
     s(x1)	status: [x1]	precedence above: a__2ndsneg negrecip rnil rcons |2ndsneg| mark cons
#a__pi(x1)	status: []	precedence above:
#a__from(x1)	status: []	precedence above:
a__from(x1)	status: []	precedence above: rnil rcons from mark
  rnil()	status: []	precedence above:
|2ndspos|(x1,x2)	status: [x2]	precedence above: rnil rcons a__2ndspos cons posrecip
square(x1)	status: [x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil rcons |2ndsneg| times mark plus a__square cons a__times
#a__times(x1,x2)	status: [x2]	precedence above:
    pi(x1)	status: [x1]	precedence above: a__from rnil |2ndspos| rcons a__2ndspos from a__pi mark cons posrecip
 rcons(x1,x2)	status: [x1]	precedence above:
a__2ndspos(x1,x2)	status: [x2]	precedence above: rnil |2ndspos| rcons cons posrecip
#a__2ndsneg(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s a__from rnil rcons |2ndsneg| from mark cons #a__2ndspos
|2ndsneg|(x1,x2)	status: [x1]	precedence above: a__2ndsneg negrecip rnil rcons cons
#a__plus(x1,x2)	status: [x1]	precedence above:
#mark(x1)	status: []	precedence above:
  from(x1)	status: []	precedence above: a__from rnil rcons mark
 times(x1,x2)	status: [x2,x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil rcons |2ndsneg| mark plus cons a__times
 a__pi(x1)	status: [x1]	precedence above: a__from rnil |2ndspos| pi rcons a__2ndspos from mark cons posrecip
   nil()	status: []	precedence above:
  mark(x1)	status: x1
  plus(x1,x2)	status: [x1,x2]	precedence above: a__plus a__2ndsneg negrecip s rnil rcons |2ndsneg| mark cons
 cons2(x1,x2)	status: x2
a__square(x1)	status: [x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil square rcons |2ndsneg| times mark plus cons a__times
  cons(x1,x2)	status: x2
a__times(x1,x2)	status: [x2,x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil rcons |2ndsneg| times mark plus cons
#a__square(x1)	status: []	precedence above:
#a__2ndspos(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s a__from rnil rcons #a__2ndsneg |2ndsneg| from mark cons
posrecip(x1)	status: []	precedence above: cons
    Usable rules: { 1..36 }
    Removed DPs: #22 #50
Number of SCCs: 1, DPs: 22, edges: 215
	SCC { #2 #9 #12..18 #25..29 #32..35 #42 #53..55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 3 8)
a__plus(x1,x2)	weight: max{x2, (/ 1 8) + x1}
a__2ndsneg(x1,x2)	weight: 0
negrecip(x1)	weight: (/ 1 8)
     s(x1)	weight: x1
#a__pi(x1)	weight: (/ 1 8)
#a__from(x1)	weight: (/ 1 4) + x1
a__from(x1)	weight: (/ 1 4) + x1
  rnil()	weight: 0
|2ndspos|(x1,x2)	weight: 0
square(x1)	weight: (/ 3 8) + x1
#a__times(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 2) + x1}
    pi(x1)	weight: (/ 1 8)
 rcons(x1,x2)	weight: max{0, x2}
a__2ndspos(x1,x2)	weight: 0
#a__2ndsneg(x1,x2)	weight: 0
|2ndsneg|(x1,x2)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
#mark(x1)	weight: (/ 1 8) + x1
  from(x1)	weight: (/ 1 4) + x1
 times(x1,x2)	weight: max{(/ 1 4) + x2, (/ 3 8) + x1}
 a__pi(x1)	weight: (/ 1 8)
   nil()	weight: (/ 1 8)
  mark(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, (/ 1 8) + x1}
 cons2(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
a__square(x1)	weight: (/ 3 8) + x1
  cons(x1,x2)	weight: max{0, (/ 1 8) + x1}
a__times(x1,x2)	weight: max{(/ 1 4) + x2, (/ 3 8) + x1}
#a__square(x1)	weight: (/ 3 8)
#a__2ndspos(x1,x2)	weight: 0
posrecip(x1)	weight: 0
    Usable rules: { 1..36 }
    Removed DPs: #13 #15..18 #26 #29 #33..35 #42 #54
Number of SCCs: 1, DPs: 10, edges: 38
	SCC { #2 #9 #12 #14 #25 #27 #28 #32 #53 #55 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above:
a__plus(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s rnil |2ndspos| rcons a__2ndspos |2ndsneg| #a__plus #mark mark plus cons posrecip
a__2ndsneg(x1,x2)	status: [x1]	precedence above: negrecip s rnil |2ndspos| rcons a__2ndspos |2ndsneg| mark cons posrecip
negrecip(x1)	status: []	precedence above: cons
     s(x1)	status: [x1]	precedence above: a__2ndsneg negrecip rnil |2ndspos| rcons a__2ndspos |2ndsneg| mark cons posrecip
#a__pi(x1)	status: []	precedence above:
#a__from(x1)	status: []	precedence above:
a__from(x1)	status: []	precedence above: rnil rcons from mark
  rnil()	status: []	precedence above:
|2ndspos|(x1,x2)	status: [x1]	precedence above: rnil rcons a__2ndspos cons posrecip
square(x1)	status: [x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil |2ndspos| #a__times rcons a__2ndspos |2ndsneg| #a__plus #mark times mark plus a__square cons a__times posrecip
#a__times(x1,x2)	status: [x2,x1]	precedence above: a__plus a__2ndsneg negrecip s rnil |2ndspos| rcons a__2ndspos |2ndsneg| #a__plus #mark times mark plus cons a__times posrecip
    pi(x1)	status: [x1]	precedence above: a__from rnil |2ndspos| rcons a__2ndspos from a__pi mark cons posrecip
 rcons(x1,x2)	status: [x1,x2]	precedence above:
a__2ndspos(x1,x2)	status: [x1]	precedence above: rnil |2ndspos| rcons cons posrecip
#a__2ndsneg(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s a__from rnil |2ndspos| rcons a__2ndspos |2ndsneg| from mark cons #a__2ndspos posrecip
|2ndsneg|(x1,x2)	status: [x1]	precedence above: a__2ndsneg negrecip s rnil |2ndspos| rcons a__2ndspos mark cons posrecip
#a__plus(x1,x2)	status: [x1,x2]	precedence above: negrecip rnil |2ndspos| rcons a__2ndspos #mark mark cons posrecip
#mark(x1)	status: [x1]	precedence above: negrecip rnil |2ndspos| rcons a__2ndspos mark cons posrecip
  from(x1)	status: []	precedence above: a__from rnil rcons mark
 times(x1,x2)	status: [x2,x1]	precedence above: a__plus a__2ndsneg negrecip s rnil |2ndspos| #a__times rcons a__2ndspos |2ndsneg| #a__plus #mark mark plus cons a__times posrecip
 a__pi(x1)	status: [x1]	precedence above: a__from rnil |2ndspos| pi rcons a__2ndspos from mark cons posrecip
   nil()	status: []	precedence above:
  mark(x1)	status: x1
  plus(x1,x2)	status: [x1,x2]	precedence above: a__plus a__2ndsneg negrecip s rnil |2ndspos| rcons a__2ndspos |2ndsneg| #a__plus #mark mark cons posrecip
 cons2(x1,x2)	status: x2
a__square(x1)	status: [x1]	precedence above: |0| a__plus a__2ndsneg negrecip s rnil |2ndspos| square #a__times rcons a__2ndspos |2ndsneg| #a__plus #mark times mark plus cons a__times posrecip
  cons(x1,x2)	status: x2
a__times(x1,x2)	status: [x2,x1]	precedence above: a__plus a__2ndsneg negrecip s rnil |2ndspos| #a__times rcons a__2ndspos |2ndsneg| #a__plus #mark times mark plus cons posrecip
#a__square(x1)	status: []	precedence above:
#a__2ndspos(x1,x2)	status: [x1,x2]	precedence above: a__2ndsneg negrecip s a__from rnil |2ndspos| rcons a__2ndspos #a__2ndsneg |2ndsneg| from mark cons posrecip
posrecip(x1)	status: []	precedence above: cons
    Usable rules: { 1..36 }
    Removed DPs: #2 #9 #12 #14 #25 #27 #28 #32 #53 #55
Number of SCCs: 0, DPs: 0, edges: 0
YES