Termination w.r.t. Q proof of /tmp/tmpTDrj5Q/s6.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a12(a12(x1)) → x1
a13(a13(x1)) → x1
a14(a14(x1)) → x1
a15(a15(x1)) → x1
a16(a16(x1)) → x1
a23(a23(x1)) → x1
a24(a24(x1)) → x1
a25(a25(x1)) → x1
a26(a26(x1)) → x1
a34(a34(x1)) → x1
a35(a35(x1)) → x1
a36(a36(x1)) → x1
a45(a45(x1)) → x1
a46(a46(x1)) → x1
a56(a56(x1)) → x1
a13(x1) → a12(a23(a12(x1)))
a14(x1) → a12(a23(a34(a23(a12(x1)))))
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1)))))))
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
a24(x1) → a23(a34(a23(x1)))
a25(x1) → a23(a34(a45(a34(a23(x1)))))
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1)))))))
a35(x1) → a34(a45(a34(x1)))
a36(x1) → a34(a45(a56(a45(a34(x1)))))
a46(x1) → a45(a56(a45(x1)))
a12(a23(a12(a23(a12(a23(x1)))))) → x1
a23(a34(a23(a34(a23(a34(x1)))))) → x1
a34(a45(a34(a45(a34(a45(x1)))))) → x1
a45(a56(a45(a56(a45(a56(x1)))))) → x1
a12(a34(x1)) → a34(a12(x1))
a12(a45(x1)) → a45(a12(x1))
a12(a56(x1)) → a56(a12(x1))
a23(a45(x1)) → a45(a23(x1))
a23(a56(x1)) → a56(a23(x1))
a34(a56(x1)) → a56(a34(x1))

Q is empty.

↳ QTRS

  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a12(a12(x1)) → x1
a13(a13(x1)) → x1
a14(a14(x1)) → x1
a15(a15(x1)) → x1
a16(a16(x1)) → x1
a23(a23(x1)) → x1
a24(a24(x1)) → x1
a25(a25(x1)) → x1
a26(a26(x1)) → x1
a34(a34(x1)) → x1
a35(a35(x1)) → x1
a36(a36(x1)) → x1
a45(a45(x1)) → x1
a46(a46(x1)) → x1
a56(a56(x1)) → x1
a13(x1) → a12(a23(a12(x1)))
a14(x1) → a12(a23(a34(a23(a12(x1)))))
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1)))))))
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
a24(x1) → a23(a34(a23(x1)))
a25(x1) → a23(a34(a45(a34(a23(x1)))))
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1)))))))
a35(x1) → a34(a45(a34(x1)))
a36(x1) → a34(a45(a56(a45(a34(x1)))))
a46(x1) → a45(a56(a45(x1)))
a12(a23(a12(a23(a12(a23(x1)))))) → x1
a23(a34(a23(a34(a23(a34(x1)))))) → x1
a34(a45(a34(a45(a34(a45(x1)))))) → x1
a45(a56(a45(a56(a45(a56(x1)))))) → x1
a12(a34(x1)) → a34(a12(x1))
a12(a45(x1)) → a45(a12(x1))
a12(a56(x1)) → a56(a12(x1))
a23(a45(x1)) → a45(a23(x1))
a23(a56(x1)) → a56(a23(x1))
a34(a56(x1)) → a56(a34(x1))

Q is empty.

We use [27] with the following order to prove termination.

Knuth-Bendix order [24] with precedence:

a23₁ > a45₁
a23₁ > a56₁
a12₁ > a45₁
a12₁ > a34₁ > a56₁

and weight map:

a46_1=4
a35_1=4
a45_1=1
a13_1=4
a15_1=8
a34_1=1
a56_1=1
a36_1=6
a14_1=6
a23_1=1
a16_1=10
a25_1=6
a26_1=8
a24_1=4
a12_1=1
dummyConstant=1