YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) a34(a56(x)) -> a56(a34(x))
(2) a23(a56(x)) -> a56(a23(x))
(3) a23(a45(x)) -> a45(a23(x))
(4) a12(a56(x)) -> a56(a12(x))
(5) a12(a45(x)) -> a45(a12(x))
(6) a12(a34(x)) -> a34(a12(x))
(7) a45(a56(a45(a56(a45(a56(x)))))) -> x
(8) a34(a45(a34(a45(a34(a45(x)))))) -> x
(9) a23(a34(a23(a34(a23(a34(x)))))) -> x
(10) a12(a23(a12(a23(a12(a23(x)))))) -> x
(11) a46(x) -> a45(a56(a45(x)))
(12) a36(x) -> a34(a45(a56(a45(a34(x)))))
(13) a35(x) -> a34(a45(a34(x)))
(14) a26(x) -> a23(a34(a45(a56(a45(a34(a23(x)))))))
(15) a25(x) -> a23(a34(a45(a34(a23(x)))))
(16) a24(x) -> a23(a34(a23(x)))
(17) a16(x) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x)))))))))
(18) a15(x) -> a12(a23(a34(a45(a34(a23(a12(x)))))))
(19) a14(x) -> a12(a23(a34(a23(a12(x)))))
(20) a13(x) -> a12(a23(a12(x)))
(21) a56(a56(x)) -> x
(22) a46(a46(x)) -> x
(23) a45(a45(x)) -> x
(24) a36(a36(x)) -> x
(25) a35(a35(x)) -> x
(26) a34(a34(x)) -> x
(27) a26(a26(x)) -> x
(28) a25(a25(x)) -> x
(29) a24(a24(x)) -> x
(30) a23(a23(x)) -> x
(31) a16(a16(x)) -> x
(32) a15(a15(x)) -> x
(33) a14(a14(x)) -> x
(34) a13(a13(x)) -> x
(35) a12(a12(x)) -> x

[2]  Use following polynomial interpretation:
[a13(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(20), (34)

[3]  Use following polynomial interpretation:
[a14(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(19), (33)

[4]  Use following polynomial interpretation:
[a15(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18), (32)

[5]  Use following polynomial interpretation:
[a16(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(17), (31)

[6]  Use following polynomial interpretation:
[a24(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16), (29)

[7]  Use following polynomial interpretation:
[a25(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(15), (28)

[8]  Use following polynomial interpretation:
[a26(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(14), (27)

[9]  Use following polynomial interpretation:
[a35(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(13), (25)

[10]  Use following polynomial interpretation:
[a36(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12), (24)

[11]  Use following polynomial interpretation:
[a46(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(11), (22)

[12]  Use following polynomial interpretation:
[a12(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(10), (35)

[13]  Use following polynomial interpretation:
[a45(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7)-(8), (23)

[14]  Use following polynomial interpretation:
[a23(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9), (30)

[15]  Use following polynomial interpretation:
[a56(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(21)

[16]  Use following polynomial interpretation:
[a34(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(26)

[17]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
a34 > a56
a12 > a34
a23 > a56
a12 > a56
a23 > a45
a12 > a45


../tpdb/SRS/Marche/s6.srs, 0.04, Y
Couldn't open file <60>: 60: No such file or directory