Problem AG01 3.13

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.13

stdout:

MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(0(),s(x)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 or(true(),y) -> true()
 or(false(),y) -> y
 union(empty(),h) -> h
 union(edge(x,y,i),h) -> edge(x,y,union(i,h))
 reach(x,y,empty(),h) -> false()
 reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
 if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
 if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
 if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
 if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.13

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.13

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool pair2rc

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}
  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 TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}
  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 TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}
  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 TimeUnknown
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}
  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 Time64.95926ms
Answer
TIMEOUT
InputAG01 3.13

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , union(empty(), h) -> h
     , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     , reach(x, y, empty(), h) -> false()
     , reach(x, y, edge(u, v, i), h) ->
       if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     , if_reach_1(true(), x, y, edge(u, v, i), h) ->
       if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
     , if_reach_2(false(), x, y, edge(u, v, i), h) ->
       or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))
     , if_reach_1(false(), x, y, edge(u, v, i), h) ->
       reach(x, y, i, edge(u, v, h))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

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

Arrrr..