0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 PisEmptyProof (⇔)
↳8 TRUE
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))
F(c(c(a, y, a), b(x, z), a)) → F(c(f(a), z, z))
F(c(c(a, y, a), b(x, z), a)) → C(f(a), z, z)
F(c(c(a, y, a), b(x, z), a)) → F(a)
F(b(b(x, f(y)), z)) → C(z, x, f(b(b(f(a), y), y)))
F(b(b(x, f(y)), z)) → F(b(b(f(a), y), y))
F(b(b(x, f(y)), z)) → F(a)
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))
F(b(b(x, f(y)), z)) → F(b(b(f(a), y), y))
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(b(b(x, f(y)), z)) → F(b(b(f(a), y), y))
[b2, f1, a] > F1
F1: multiset
b2: [2,1]
f1: [1]
a: multiset
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))