LMPO

Execution Time (secs)	0.043
Answer	YES(?,ELEMENTARY)
Input	SK90 2.19

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs:
    {  sqr(0()) -> 0()
     , sqr(s(x)) -> +(sqr(x), s(double(x)))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , sqr(s(x)) -> s(+(sqr(x), double(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,ELEMENTARY)

Proof:
  The input was oriented with the instance of
  Lightweight Multiset Path Order () as induced by the safe mapping

   safe(sqr) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1},
   safe(double) = {}

  and precedence

   sqr > +, sqr > double .

  Following symbols are considered recursive:

   {sqr, +, double}

  The recursion depth is 2 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  sqr(0();) -> 0()
      , sqr(s(; x);) -> +(s(; double(x;)); sqr(x;))
      , double(0();) -> 0()
      , double(s(; x);) -> s(; s(; double(x;)))
      , +(0(); x) -> x
      , +(s(; y); x) -> s(; +(y; x))
      , sqr(s(; x);) -> s(; +(double(x;); sqr(x;)))}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

MPO

Execution Time (secs)	0.056
Answer	YES(?,PRIMREC)
Input	SK90 2.19

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  sqr(0()) -> 0()
     , sqr(s(x)) -> +(sqr(x), s(double(x)))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , sqr(s(x)) -> s(+(sqr(x), double(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,PRIMREC)

Proof:
  The input was oriented with the instance of
  'multiset path orders' as induced by the precedence

   sqr > s, sqr > +, sqr > double, + > s, double > s .

Hurray, we answered YES(?,PRIMREC)

POP*

Execution Time (secs)	0.092
Answer	YES(?,POLY)
Input	SK90 2.19

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  sqr(0()) -> 0()
     , sqr(s(x)) -> +(sqr(x), s(double(x)))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , sqr(s(x)) -> s(+(sqr(x), double(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order () as induced by the safe mapping

   safe(sqr) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1},
   safe(double) = {}

  and precedence

   sqr > +, sqr > double .

  Following symbols are considered recursive:

   {sqr, +, double}

  The recursion depth is 2 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  sqr(0();) -> 0()
      , sqr(s(; x);) -> +(s(; double(x;)); sqr(x;))
      , double(0();) -> 0()
      , double(s(; x);) -> s(; s(; double(x;)))
      , +(0(); x) -> x
      , +(s(; y); x) -> s(; +(y; x))
      , sqr(s(; x);) -> s(; +(double(x;); sqr(x;)))}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

POP* (PS)

Execution Time (secs)	0.060
Answer	YES(?,POLY)
Input	SK90 2.19

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  sqr(0()) -> 0()
     , sqr(s(x)) -> +(sqr(x), s(double(x)))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , sqr(s(x)) -> s(+(sqr(x), double(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order (PS) as induced by the safe mapping

   safe(sqr) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1},
   safe(double) = {}

  and precedence

   sqr > +, sqr > double .

  Following symbols are considered recursive:

   {sqr, +, double}

  The recursion depth is 2 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  sqr(0();) -> 0()
      , sqr(s(; x);) -> +(s(; double(x;)); sqr(x;))
      , double(0();) -> 0()
      , double(s(; x);) -> s(; s(; double(x;)))
      , +(0(); x) -> x
      , +(s(; y); x) -> s(; +(y; x))
      , sqr(s(; x);) -> s(; +(double(x;); sqr(x;)))}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

Small POP*

Execution Time (secs)	0.051
Answer	MAYBE
Input	SK90 2.19

MAYBE

We consider the following Problem:

  Strict Trs:
    {  sqr(0()) -> 0()
     , sqr(s(x)) -> +(sqr(x), s(double(x)))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , +(x, 0()) -> x
     , +(x, s(y)) -> s(+(x, y))
     , sqr(s(x)) -> s(+(sqr(x), double(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)	0.045
Answer	MAYBE
Input	SK90 2.19