LMPO
Execution Time (secs) | 0.084 |
Answer | YES(?,ELEMENTARY) |
Input | TCT 09 ma6 |
YES(?,ELEMENTARY)
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())}
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(ite) = {1, 2}, safe(tt) = {}, safe(ff) = {}, safe(find) = {2},
safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
safe(clique) = {}
and precedence
complete > ite, complete > find, clique > ite, clique > complete .
Following symbols are considered recursive:
{ite, find, complete, clique}
The recursion depth is 3 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ ite(v; tt(), u) -> u
, ite(v; ff(), u) -> v
, find(u, nil(); v) -> ff()
, find(u, cons(; cons(; u, v), E); v) -> tt()
, find(u, cons(; cons(; u2, v2), E); v) -> find(u, E; v)
, complete(u, nil(), E;) -> tt()
, complete(u, cons(; v, S), E;) ->
ite(ff(); find(u, E; v), complete(u, S, E;))
, clique(nil(), E;) -> tt()
, clique(cons(; u, K), E;) ->
ite(ff(); complete(u, K, E;), clique(K, E;))}
Weak Trs : {}
Hurray, we answered YES(?,ELEMENTARY)
MPO
Execution Time (secs) | 0.123 |
Answer | YES(?,PRIMREC) |
Input | TCT 09 ma6 |
YES(?,PRIMREC)
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())}
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
find > tt, nil > tt, nil > ff, cons > ff, complete > ite,
clique > ite, clique > complete, find ~ complete .
Hurray, we answered YES(?,PRIMREC)
POP*
Execution Time (secs) | 0.180 |
Answer | YES(?,POLY) |
Input | TCT 09 ma6 |
YES(?,POLY)
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())}
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(ite) = {2}, safe(tt) = {}, safe(ff) = {}, safe(find) = {1, 2},
safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
safe(clique) = {}
and precedence
complete > ite, complete > find, clique > ite, clique > complete .
Following symbols are considered recursive:
{ite, find, complete, clique}
The recursion depth is 3 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ ite(tt(), v; u) -> u
, ite(ff(), v; u) -> v
, find(nil(); u, v) -> ff()
, find(cons(; cons(; u, v), E); u, v) -> tt()
, find(cons(; cons(; u2, v2), E); u, v) -> find(E; u, v)
, complete(u, nil(), E;) -> tt()
, complete(u, cons(; v, S), E;) ->
ite(find(E; u, v), ff(); complete(u, S, E;))
, clique(nil(), E;) -> tt()
, clique(cons(; u, K), E;) ->
ite(complete(u, K, E;), ff(); clique(K, E;))}
Weak Trs : {}
Hurray, we answered YES(?,POLY)
POP* (PS)
Execution Time (secs) | 0.110 |
Answer | YES(?,POLY) |
Input | TCT 09 ma6 |
YES(?,POLY)
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())}
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(ite) = {2, 3}, safe(tt) = {}, safe(ff) = {}, safe(find) = {},
safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
safe(clique) = {}
and precedence
complete > ite, complete > find, clique > ite, clique > complete .
Following symbols are considered recursive:
{ite, find, complete, clique}
The recursion depth is 3 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
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())}
Weak Trs : {}
Hurray, we answered YES(?,POLY)
Small POP*
Execution Time (secs) | 0.197 |
Answer | YES(?,O(n^3)) |
Input | TCT 09 ma6 |
YES(?,O(n^3))
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^3))
Proof:
The input was oriented with the instance of
Small Polynomial Path Order (WSC) as induced by the safe mapping
safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {},
safe(find) = {1}, safe(nil) = {}, safe(cons) = {1, 2},
safe(complete) = {}, safe(clique) = {}
and precedence
complete > ite, complete > find, clique > ite, clique > complete .
Following symbols are considered recursive:
{ite, find, complete, clique}
The recursion depth is 3 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ ite(; tt(), u, v) -> u
, ite(; ff(), u, v) -> v
, find(v, nil(); u) -> ff()
, find(v, cons(; cons(; u, v), E); u) -> tt()
, find(v, cons(; cons(; u2, v2), E); u) -> find(v, E; u)
, complete(u, nil(), E;) -> tt()
, complete(u, cons(; v, S), E;) ->
ite(; find(v, E; u), complete(u, S, E;), ff())
, clique(nil(), E;) -> tt()
, clique(cons(; u, K), E;) ->
ite(; complete(u, K, E;), clique(K, E;), ff())}
Weak Trs : {}
Hurray, we answered YES(?,O(n^3))
Small POP* (PS)
Execution Time (secs) | 0.216 |
Answer | YES(?,O(n^3)) |
Input | TCT 09 ma6 |
YES(?,O(n^3))
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^3))
Proof:
The input was oriented with the instance of
Small Polynomial Path Order (WSC,
PS) as induced by the safe mapping
safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {},
safe(find) = {1, 2}, safe(nil) = {}, safe(cons) = {1, 2},
safe(complete) = {1}, safe(clique) = {}
and precedence
complete > ite, complete > find, clique > ite, clique > complete .
Following symbols are considered recursive:
{ite, find, complete, clique}
The recursion depth is 3 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ ite(; tt(), u, v) -> u
, ite(; ff(), u, v) -> v
, find(nil(); u, v) -> ff()
, find(cons(; cons(; u, v), E); u, v) -> tt()
, find(cons(; cons(; u2, v2), E); u, v) -> find(E; u, v)
, complete(nil(), E; u) -> tt()
, complete(cons(; v, S), E; u) ->
ite(; find(E; u, v), complete(S, E; u), ff())
, clique(nil(), E;) -> tt()
, clique(cons(; u, K), E;) ->
ite(; complete(K, E; u), clique(K, E;), ff())}
Weak Trs : {}
Hurray, we answered YES(?,O(n^3))