LMPO
Execution Time (secs) | 0.101 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
Execution Time (secs) | 0.189 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
Execution Time (secs) | 0.096 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
Execution Time (secs) | 0.152 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
Execution Time (secs) | 0.103 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
Execution Time (secs) | 0.121 |
Answer | MAYBE |
Input | TCT 09 ma7 |
MAYBE
We consider the following Problem:
Strict Trs:
{ ite(tt(), u, v) -> u
, ite(ff(), u, v) -> v
, find(u, v, nil()) -> ff()
, find(u, v, cons(cons(u, v), E)) -> tt()
, find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
, complete(u, nil(), E) -> tt()
, complete(u, cons(v, S), E) ->
ite(find(u, v, E), complete(u, S, E), ff())
, clique(nil(), E) -> tt()
, clique(cons(u, K), E) ->
ite(complete(u, K, E), clique(K, E), ff())
, choice(nil(), K, E) -> ite(clique(K, E), K, nil())
, choice(cons(u, S), K, E) -> choice(S, cons(u, K), E)
, choice(cons(u, S), K, E) -> choice(S, K, E)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..