MAYBE
Termination Proof using AProVETerm Rewriting System R:
[N, A, D, O, Atts, Key, Val, RS, C, Val', KR, D', M, R, R', X, z, y, x]
----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(N, N) -> N
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, getReq-osb-K$Elt-csb(Key))) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, A, getReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key))))
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, setReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined), true), A, Atts, D, Key, O)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, setReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U21(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined)), true), A, Atts, D, Key, O, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(RS)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, C, lookupReq-osb-K$Elt-csb(Key))) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined)), true), A, C, D, Key, O, RS)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(RS)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, C, lookupReq-osb-K$Elt-csb(Key))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined), true), A, C, D, Key, O, RS)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, lookupReq-osb-K$Elt-csb(Key))))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, getReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U51(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(Val, undefined), true), A, C, D, Key, O, RS, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, lookupReq-osb-K$Elt-csb(Key))))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, getReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U61(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(Val, undefined)), true), A, C, D, Key, O, RS, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, tellReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, setReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val'))) -> U71(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(Val', undefined)), true), A, C, D, Key, O, RS, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, tellReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, O, setReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val'))) -> U81(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(Val', undefined), true), A, C, D, Key, O, RS, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), pal`:--osb-Oid-csb(O)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, C, tellReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U101(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined)), true), A, C, D, Key, O, RS, Val)
---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), pal`:--osb-Oid-csb(O)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(A, C, tellReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val))) -> U91(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key), undefined), true), A, C, D, Key, O, RS, Val)
-==--osb-K$Elt-csb-osb-K$Elt-csb(D, D) -> true
-==--osb-V$Elt-csb-osb-V$Elt-csb(KR, KR) -> true
U101(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(Key, Val, D)), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), pal`:--osb-Oid-csb(O)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, tellReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U11(tt, A, Atts, D, Key, O) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, A, setReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, undefined)))
U111(tt, D', M) -> lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(M, D')
U121(tt, R) -> R
U131(tt) -> undefined
U141(tt, D', D, M, R', R) -> ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(D, R, M), -|->--osb-K$Elt-csb-osb-V$Elt-csb(D', R'))
U21(tt, A, Atts, D, Key, O, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(Key, Val, D)), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), Atts))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, A, setReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U31(tt, A, C, D, Key, O, RS) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(RS)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, lookupReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(D, Key))))
U41(tt, A, C, D, Key, O, RS) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, lookupReq-osb-K$Elt-csb(Key))))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, A, getReq-osb-K$Elt-csb(Key)))
U51(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), data`:--osb-Dictocb-K-V-ccb-csb(D)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, lookupReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U61(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), data`:--osb-Dictocb-K-V-ccb-csb(update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(Key, Val, D))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, lookupReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U71(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), data`:--osb-Dictocb-K-V-ccb-csb(D)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, tellReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U81(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(pal`:--osb-Oid-csb(O), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(RS), data`:--osb-Dictocb-K-V-ccb-csb(update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(Key, Val, D))))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(C, A, tellReply-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
U91(tt, A, C, D, Key, O, RS, Val) -> ---osb-Configuration-csb-osb-Configuration-csb(<-:-|->-osb-Oid-csb-osb-Cid-csb-osb-AttributeSet-csb(A, DataAgent, ----osb-AttributeSet-csb-osb-AttributeSet-csb(data`:--osb-Dictocb-K-V-ccb-csb(D), ----osb-AttributeSet-csb-osb-AttributeSet-csb(requests`:--osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(RS, w4-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, C, tellReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))), pal`:--osb-Oid-csb(O)))), msg-osb-Oid-csb-osb-Oid-csb-osb-MsgBody-csb(O, A, setReq-osb-K$Elt-csb-osb-V$Elt-csb(Key, Val)))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(empty, D) -> undefined
lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(M, -|->--osb-K$Elt-csb-osb-V$Elt-csb(D, R)), D') -> U111(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-K$Elt-csb-osb-K$Elt-csb(D, D')), true), D', M)
lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(M, -|->--osb-K$Elt-csb-osb-V$Elt-csb(D, R)), D) -> U121(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(M, D), R), true), R)
lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(M, -|->--osb-K$Elt-csb-osb-V$Elt-csb(D, R)), D) -> U131(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-V$Elt-csb-osb-V$Elt-csb(lookup-osb-Dictocb-K-V-ccb-csb-osb-K$Elt-csb(M, D), R)), true))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(D, R, empty) -> -|->--osb-K$Elt-csb-osb-V$Elt-csb(D, R)
update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(D, R, ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(M, -|->--osb-K$Elt-csb-osb-V$Elt-csb(D', R'))) -> U141(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-K$Elt-csb-osb-K$Elt-csb(D, D')), true), D', D, M, R', R)
update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(D, R, ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(M, -|->--osb-K$Elt-csb-osb-V$Elt-csb(D, R'))) -> update-osb-K$Elt-csb-osb-V$Elt-csb-osb-Dictocb-K-V-ccb-csb(D, R, M)
----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(x, ----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(y, z)) == ----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(x, y), z)
----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(x, y) == ----osb-Setocb-Request-ccb-csb-osb-Setocb-Request-ccb-csb(y, x)
---osb-Configuration-csb-osb-Configuration-csb(x, ---osb-Configuration-csb-osb-Configuration-csb(y, z)) == ---osb-Configuration-csb-osb-Configuration-csb(---osb-Configuration-csb-osb-Configuration-csb(x, y), z)
---osb-Configuration-csb-osb-Configuration-csb(x, y) == ---osb-Configuration-csb-osb-Configuration-csb(y, x)
----osb-AttributeSet-csb-osb-AttributeSet-csb(----osb-AttributeSet-csb-osb-AttributeSet-csb(x, y), z) == ----osb-AttributeSet-csb-osb-AttributeSet-csb(x, ----osb-AttributeSet-csb-osb-AttributeSet-csb(y, z))
----osb-AttributeSet-csb-osb-AttributeSet-csb(x, y) == ----osb-AttributeSet-csb-osb-AttributeSet-csb(y, x)
----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(x, y), z) == ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(x, ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(y, z))
----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(x, y) == ----osb-Dictocb-K-V-ccb-csb-osb-Dictocb-K-V-ccb-csb(y, x)
Termination of R to be shown.
R
↳Failure
↳Fail
DirectTerminationTRS ran out time!
Trying another alternative:
R
↳Fail
↳Failure
DependencyPairs ran out time!
The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
5:00 minutes