Problem AG01 innermost 4.35

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAG01 innermost 4.35

stdout:

MAYBE

Problem:
 and(true(),y) -> y
 and(false(),y) -> false()
 eq(nil(),nil()) -> true()
 eq(cons(t,l),nil()) -> false()
 eq(nil(),cons(t,l)) -> false()
 eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
 eq(var(l),var(l')) -> eq(l,l')
 eq(var(l),apply(t,s)) -> false()
 eq(var(l),lambda(x,t)) -> false()
 eq(apply(t,s),var(l)) -> false()
 eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
 eq(apply(t,s),lambda(x,t)) -> false()
 eq(lambda(x,t),var(l)) -> false()
 eq(lambda(x,t),apply(t,s)) -> false()
 eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
 if(true(),var(k),var(l')) -> var(k)
 if(false(),var(k),var(l')) -> var(l')
 ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
 ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
 ren(x,y,lambda(z,t)) ->
 lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                 t)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 innermost 4.35

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 innermost 4.35

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  and(true(), y) -> y
     , and(false(), y) -> false()
     , eq(nil(), nil()) -> true()
     , eq(cons(t, l), nil()) -> false()
     , eq(nil(), cons(t, l)) -> false()
     , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
     , eq(var(l), var(l')) -> eq(l, l')
     , eq(var(l), apply(t, s)) -> false()
     , eq(var(l), lambda(x, t)) -> false()
     , eq(apply(t, s), var(l)) -> false()
     , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
     , eq(apply(t, s), lambda(x, t)) -> false()
     , eq(lambda(x, t), var(l)) -> false()
     , eq(lambda(x, t), apply(t, s)) -> false()
     , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
     , if(true(), var(k), var(l')) -> var(k)
     , if(false(), var(k), var(l')) -> var(l')
     , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))
     , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
     , ren(x, y, lambda(z, t)) ->
       lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
              ren(x,
                  y,
                  ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 innermost 4.35

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 innermost 4.35

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  and(true(), y) -> y
     , and(false(), y) -> false()
     , eq(nil(), nil()) -> true()
     , eq(cons(t, l), nil()) -> false()
     , eq(nil(), cons(t, l)) -> false()
     , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
     , eq(var(l), var(l')) -> eq(l, l')
     , eq(var(l), apply(t, s)) -> false()
     , eq(var(l), lambda(x, t)) -> false()
     , eq(apply(t, s), var(l)) -> false()
     , eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
     , eq(apply(t, s), lambda(x, t)) -> false()
     , eq(lambda(x, t), var(l)) -> false()
     , eq(lambda(x, t), apply(t, s)) -> false()
     , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
     , if(true(), var(k), var(l')) -> var(k)
     , if(false(), var(k), var(l')) -> var(l')
     , ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))
     , ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
     , ren(x, y, lambda(z, t)) ->
       lambda(var(cons(x, cons(y, cons(lambda(z, t), nil())))),
              ren(x,
                  y,
                  ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds