s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
S(b(s(x1))) → T(x1)
T(s(x1)) → T(t(x1))
T(b(x1)) → S(x1)
B(u(x1)) → B(s(x1))
S(u(x1)) → S(s(x1))
S(b(x1)) → S(s(x1))
S(b(x1)) → B(s(s(s(x1))))
S(b(x1)) → S(x1)
T(b(s(x1))) → T(b(x1))
T(b(s(x1))) → B(x1)
T(u(x1)) → T(x1)
T(s(x1)) → T(x1)
B(u(x1)) → S(x1)
S(b(x1)) → S(s(s(x1)))
S(b(s(x1))) → B(t(x1))
S(u(x1)) → S(x1)
T(b(x1)) → B(s(x1))
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
S(b(s(x1))) → T(x1)
T(s(x1)) → T(t(x1))
T(b(x1)) → S(x1)
B(u(x1)) → B(s(x1))
S(u(x1)) → S(s(x1))
S(b(x1)) → S(s(x1))
S(b(x1)) → B(s(s(s(x1))))
S(b(x1)) → S(x1)
T(b(s(x1))) → T(b(x1))
T(b(s(x1))) → B(x1)
T(u(x1)) → T(x1)
T(s(x1)) → T(x1)
B(u(x1)) → S(x1)
S(b(x1)) → S(s(s(x1)))
S(b(s(x1))) → B(t(x1))
S(u(x1)) → S(x1)
T(b(x1)) → B(s(x1))
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(b(s(x1))) → T(x1)
T(b(x1)) → S(x1)
S(b(x1)) → S(s(x1))
S(b(x1)) → B(s(s(s(x1))))
S(b(x1)) → S(x1)
T(b(s(x1))) → B(x1)
B(u(x1)) → S(x1)
S(b(x1)) → S(s(s(x1)))
S(b(s(x1))) → B(t(x1))
T(b(x1)) → B(s(x1))
Used ordering: Polynomial interpretation [25,35]:
T(s(x1)) → T(t(x1))
B(u(x1)) → B(s(x1))
S(u(x1)) → S(s(x1))
T(b(s(x1))) → T(b(x1))
T(u(x1)) → T(x1)
T(s(x1)) → T(x1)
S(u(x1)) → S(x1)
The value of delta used in the strict ordering is 2.
POL(T(x1)) = (4)x_1
POL(B(x1)) = 2 + (4)x_1
POL(t(x1)) = x_1
POL(u(x1)) = x_1
POL(s(x1)) = x_1
POL(b(x1)) = 1 + (4)x_1
POL(S(x1)) = (4)x_1
s(b(s(x1))) → b(t(x1))
s(b(x1)) → b(s(s(s(x1))))
t(b(s(x1))) → u(t(b(x1)))
t(b(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
b(u(x1)) → b(s(x1))
s(u(x1)) → s(s(x1))
t(u(x1)) → u(t(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
T(s(x1)) → T(t(x1))
T(u(x1)) → T(x1)
T(s(x1)) → T(x1)
B(u(x1)) → B(s(x1))
S(u(x1)) → S(x1)
S(u(x1)) → S(s(x1))
T(b(s(x1))) → T(b(x1))
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
S(u(x1)) → S(s(x1))
S(u(x1)) → S(x1)
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
B(u(x1)) → B(s(x1))
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(u(x1)) → B(s(x1))
The value of delta used in the strict ordering is 2.
POL(B(x1)) = (2)x_1
POL(t(x1)) = 1
POL(u(x1)) = 1
POL(s(x1)) = 0
POL(b(x1)) = 0
s(b(s(x1))) → b(t(x1))
s(b(x1)) → b(s(s(s(x1))))
t(b(s(x1))) → u(t(b(x1)))
t(b(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
b(u(x1)) → b(s(x1))
s(u(x1)) → s(s(x1))
t(u(x1)) → u(t(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
T(s(x1)) → T(t(x1))
T(u(x1)) → T(x1)
T(s(x1)) → T(x1)
T(b(s(x1))) → T(b(x1))
s(b(x1)) → b(s(s(s(x1))))
s(b(s(x1))) → b(t(x1))
t(b(x1)) → b(s(x1))
t(b(s(x1))) → u(t(b(x1)))
b(u(x1)) → b(s(x1))
t(s(x1)) → t(t(x1))
t(u(x1)) → u(t(x1))
s(u(x1)) → s(s(x1))