Problem SK90 4.57

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.57

stdout:

MAYBE

Problem:
f(x,y,z) -> g(<=(x,y),x,y,z)
g(true(),x,y,z) -> z
g(false(),x,y,z) -> f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
p(0()) -> 0()
p(s(x)) -> x

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.57

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	SK90 4.57

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair2rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool rc

Execution Time	Unknown
Answer	TIMEOUT
Input	SK90 4.57

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool tup3irc

Execution Time	0.35369992ms
Answer	YES(O(1),O(1))
Input	SK90 4.57

stdout:

YES(O(1),O(1))

We consider the following Problem:

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(O(1),O(1))

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.

  We abort the transformation and continue with the subprocessor on the problem

  Strict Trs:
    {  f(x, y, z) -> g(<=(x, y), x, y, z)
     , g(true(), x, y, z) -> z
     , g(false(), x, y, z) ->
       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
     , p(0()) -> 0()
     , p(s(x)) -> x}
  StartTerms: basic terms
  Strategy: innermost

  1) 'dp' proved the goal fastest:

     We have computed the following dependency pairs

     Strict Dependency Pairs:
       {  f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))
        , g^#(true(), x, y, z) -> c_2()
        , g^#(false(), x, y, z) ->
          c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
              f^#(p(x), y, z),
              p^#(x),
              f^#(p(y), z, x),
              p^#(y),
              f^#(p(z), x, y),
              p^#(z))
        , p^#(0()) -> c_4()
        , p^#(s(x)) -> c_5()}

     We consider the following Problem:

       Strict DPs:
         {  f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))
          , g^#(true(), x, y, z) -> c_2()
          , g^#(false(), x, y, z) ->
            c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
                f^#(p(x), y, z),
                p^#(x),
                f^#(p(y), z, x),
                p^#(y),
                f^#(p(z), x, y),
                p^#(z))
          , p^#(0()) -> c_4()
          , p^#(s(x)) -> c_5()}
       Weak Trs:
         {  f(x, y, z) -> g(<=(x, y), x, y, z)
          , g(true(), x, y, z) -> z
          , g(false(), x, y, z) ->
            f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
          , p(0()) -> 0()
          , p(s(x)) -> x}
       StartTerms: basic terms
       Strategy: innermost

     Certificate: YES(O(1),O(1))

     Application of 'Fastest':
     -------------------------
       'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:

       Compose is inapplicable since some weak rule is size increasing

       We abort the transformation and continue with the subprocessor on the problem

       Strict DPs:
         {  f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))
          , g^#(true(), x, y, z) -> c_2()
          , g^#(false(), x, y, z) ->
            c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
                f^#(p(x), y, z),
                p^#(x),
                f^#(p(y), z, x),
                p^#(y),
                f^#(p(z), x, y),
                p^#(z))
          , p^#(0()) -> c_4()
          , p^#(s(x)) -> c_5()}
       Weak Trs:
         {  f(x, y, z) -> g(<=(x, y), x, y, z)
          , g(true(), x, y, z) -> z
          , g(false(), x, y, z) ->
            f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
          , p(0()) -> 0()
          , p(s(x)) -> x}
       StartTerms: basic terms
       Strategy: innermost

       1) We consider the the dependency-graph

            1: f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))

            2: g^#(true(), x, y, z) -> c_2()

            3: g^#(false(), x, y, z) ->
               c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
                   f^#(p(x), y, z),
                   p^#(x),
                   f^#(p(y), z, x),
                   p^#(y),
                   f^#(p(z), x, y),
                   p^#(z))
                 --> p^#(s(x)) -> c_5(): 5
                 --> p^#(0()) -> c_4(): 4
                 --> f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z)): 1

            4: p^#(0()) -> c_4()

            5: p^#(s(x)) -> c_5()


          together with the congruence-graph

            ->{2}                                                       Noncyclic, trivial, SCC

            ->{3}                                                       Noncyclic, trivial, SCC
               |
               |->{1}                                                   Noncyclic, trivial, SCC
               |
               |->{4}                                                   Noncyclic, trivial, SCC
               |
               `->{5}                                                   Noncyclic, trivial, SCC


            Here rules are as follows:

              {  1: f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))
               , 2: g^#(true(), x, y, z) -> c_2()
               , 3: g^#(false(), x, y, z) ->
                    c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
                        f^#(p(x), y, z),
                        p^#(x),
                        f^#(p(y), z, x),
                        p^#(y),
                        f^#(p(z), x, y),
                        p^#(z))
               , 4: p^#(0()) -> c_4()
               , 5: p^#(s(x)) -> c_5()}

          The following rules are either leafs or part of trailing weak paths, and thus they can be removed:

            {  3: g^#(false(), x, y, z) ->
                  c_3(f^#(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)),
                      f^#(p(x), y, z),
                      p^#(x),
                      f^#(p(y), z, x),
                      p^#(y),
                      f^#(p(z), x, y),
                      p^#(z))
             , 4: p^#(0()) -> c_4()
             , 5: p^#(s(x)) -> c_5()
             , 2: g^#(true(), x, y, z) -> c_2()
             , 1: f^#(x, y, z) -> c_1(g^#(<=(x, y), x, y, z))}

          We consider the following Problem:

            Weak Trs:
              {  f(x, y, z) -> g(<=(x, y), x, y, z)
               , g(true(), x, y, z) -> z
               , g(false(), x, y, z) ->
                 f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
               , p(0()) -> 0()
               , p(s(x)) -> x}
            StartTerms: basic terms
            Strategy: innermost

          Certificate: YES(O(1),O(1))

          Application of 'simpDPRHS >>> ...':
          -----------------------------------
            No rule was simplified

            We apply the transformation 'usablerules' on the resulting sub-problems:
            Sub-problem 1:
            --------------
              We consider the problem

              Weak Trs:
                {  f(x, y, z) -> g(<=(x, y), x, y, z)
                 , g(true(), x, y, z) -> z
                 , g(false(), x, y, z) ->
                   f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                 , p(0()) -> 0()
                 , p(s(x)) -> x}
              StartTerms: basic terms
              Strategy: innermost

              The input problem is not a DP-problem.

            We abort the transformation and continue with the subprocessor on the problem

            Weak Trs:
              {  f(x, y, z) -> g(<=(x, y), x, y, z)
               , g(true(), x, y, z) -> z
               , g(false(), x, y, z) ->
                 f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
               , p(0()) -> 0()
               , p(s(x)) -> x}
            StartTerms: basic terms
            Strategy: innermost

            1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'

                 All strict components are empty, nothing to further orient

               We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem

               Weak Trs:
                 {  f(x, y, z) -> g(<=(x, y), x, y, z)
                  , g(true(), x, y, z) -> z
                  , g(false(), x, y, z) ->
                    f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                  , p(0()) -> 0()
                  , p(s(x)) -> x}
               StartTerms: basic terms
               Strategy: innermost

                 We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'

                   All strict components are empty, nothing to further orient

                 We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem

                 Weak Trs:
                   {  f(x, y, z) -> g(<=(x, y), x, y, z)
                    , g(true(), x, y, z) -> z
                    , g(false(), x, y, z) ->
                      f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                    , p(0()) -> 0()
                    , p(s(x)) -> x}
                 StartTerms: basic terms
                 Strategy: innermost

                   All strict components are empty, nothing to further orient

               We abort the transformation and continue with the subprocessor on the problem

               Weak Trs:
                 {  f(x, y, z) -> g(<=(x, y), x, y, z)
                  , g(true(), x, y, z) -> z
                  , g(false(), x, y, z) ->
                    f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                  , p(0()) -> 0()
                  , p(s(x)) -> x}
               StartTerms: basic terms
               Strategy: innermost

               1) No dependency-pair could be removed

                  We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                  Sub-problem 1:
                  --------------
                    We consider the problem

                    Weak Trs:
                      {  f(x, y, z) -> g(<=(x, y), x, y, z)
                       , g(true(), x, y, z) -> z
                       , g(false(), x, y, z) ->
                         f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                       , p(0()) -> 0()
                       , p(s(x)) -> x}
                    StartTerms: basic terms
                    Strategy: innermost

                    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'

                      All strict components are empty, nothing to further orient

                    We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem

                    Weak Trs:
                      {  f(x, y, z) -> g(<=(x, y), x, y, z)
                       , g(true(), x, y, z) -> z
                       , g(false(), x, y, z) ->
                         f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                       , p(0()) -> 0()
                       , p(s(x)) -> x}
                    StartTerms: basic terms
                    Strategy: innermost

                      We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'

                        All strict components are empty, nothing to further orient

                      We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem

                      Weak Trs:
                        {  f(x, y, z) -> g(<=(x, y), x, y, z)
                         , g(true(), x, y, z) -> z
                         , g(false(), x, y, z) ->
                           f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                         , p(0()) -> 0()
                         , p(s(x)) -> x}
                      StartTerms: basic terms
                      Strategy: innermost

                        All strict components are empty, nothing to further orient

                  We abort the transformation and continue with the subprocessor on the problem

                  Weak Trs:
                    {  f(x, y, z) -> g(<=(x, y), x, y, z)
                     , g(true(), x, y, z) -> z
                     , g(false(), x, y, z) ->
                       f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y))
                     , p(0()) -> 0()
                     , p(s(x)) -> x}
                  StartTerms: basic terms
                  Strategy: innermost

                  1) 'empty' succeeded:

                     Empty rules are trivially bounded






Hurray, we answered YES(O(1),O(1))