; @xtcfilename "./TRS_Standard/Hydras/lepper_4.xml"
(format TRS)
(fun a 1)
(fun o 1)
(fun l 1)
(fun S 1)
(fun + 2)
(fun P 5)
(fun M 5)
(fun J1 2)
(fun J2 3)
(fun J3 4)
(fun J4 5)
(fun Q11 2)
(fun Q21 3)
(fun Q22 3)
(fun Q31 4)
(fun Q32 4)
(fun Q33 4)
(fun Q41 5)
(fun Q42 5)
(fun Q43 5)
(fun Q44 5)
(fun R1 3)
(fun R2 4)
(fun R3 5)
(fun R4 6)
(fun |0| 0)
(rule (a x1) x1)
(rule (o x1) x1)
(rule (l x1) x1)
(rule (S x1) x1)
(rule (+ x1 x2) x2)
(rule (+ x1 x2) x1)
(rule (P x1 x2 x3 x4 x5) x5)
(rule (P x1 x2 x3 x4 x5) x4)
(rule (P x1 x2 x3 x4 x5) x3)
(rule (P x1 x2 x3 x4 x5) x2)
(rule (P x1 x2 x3 x4 x5) x1)
(rule (M x1 x2 x3 x4 x5) x5)
(rule (M x1 x2 x3 x4 x5) x4)
(rule (M x1 x2 x3 x4 x5) x3)
(rule (M x1 x2 x3 x4 x5) x2)
(rule (M x1 x2 x3 x4 x5) x1)
(rule (J1 x1 x2) x2)
(rule (J1 x1 x2) x1)
(rule (J2 x1 x2 x3) x3)
(rule (J2 x1 x2 x3) x2)
(rule (J2 x1 x2 x3) x1)
(rule (J3 x1 x2 x3 x4) x4)
(rule (J3 x1 x2 x3 x4) x3)
(rule (J3 x1 x2 x3 x4) x2)
(rule (J3 x1 x2 x3 x4) x1)
(rule (J4 x1 x2 x3 x4 x5) x5)
(rule (J4 x1 x2 x3 x4 x5) x4)
(rule (J4 x1 x2 x3 x4 x5) x3)
(rule (J4 x1 x2 x3 x4 x5) x2)
(rule (J4 x1 x2 x3 x4 x5) x1)
(rule (Q11 x1 x2) x2)
(rule (Q11 x1 x2) x1)
(rule (Q21 x1 x2 x3) x3)
(rule (Q21 x1 x2 x3) x2)
(rule (Q21 x1 x2 x3) x1)
(rule (Q22 x1 x2 x3) x3)
(rule (Q22 x1 x2 x3) x2)
(rule (Q22 x1 x2 x3) x1)
(rule (Q31 x1 x2 x3 x4) x4)
(rule (Q31 x1 x2 x3 x4) x3)
(rule (Q31 x1 x2 x3 x4) x2)
(rule (Q31 x1 x2 x3 x4) x1)
(rule (Q32 x1 x2 x3 x4) x4)
(rule (Q32 x1 x2 x3 x4) x3)
(rule (Q32 x1 x2 x3 x4) x2)
(rule (Q32 x1 x2 x3 x4) x1)
(rule (Q33 x1 x2 x3 x4) x4)
(rule (Q33 x1 x2 x3 x4) x3)
(rule (Q33 x1 x2 x3 x4) x2)
(rule (Q33 x1 x2 x3 x4) x1)
(rule (Q41 x1 x2 x3 x4 x5) x5)
(rule (Q41 x1 x2 x3 x4 x5) x4)
(rule (Q41 x1 x2 x3 x4 x5) x3)
(rule (Q41 x1 x2 x3 x4 x5) x2)
(rule (Q41 x1 x2 x3 x4 x5) x1)
(rule (Q42 x1 x2 x3 x4 x5) x5)
(rule (Q42 x1 x2 x3 x4 x5) x4)
(rule (Q42 x1 x2 x3 x4 x5) x3)
(rule (Q42 x1 x2 x3 x4 x5) x2)
(rule (Q42 x1 x2 x3 x4 x5) x1)
(rule (Q43 x1 x2 x3 x4 x5) x5)
(rule (Q43 x1 x2 x3 x4 x5) x4)
(rule (Q43 x1 x2 x3 x4 x5) x3)
(rule (Q43 x1 x2 x3 x4 x5) x2)
(rule (Q43 x1 x2 x3 x4 x5) x1)
(rule (Q44 x1 x2 x3 x4 x5) x5)
(rule (Q44 x1 x2 x3 x4 x5) x4)
(rule (Q44 x1 x2 x3 x4 x5) x3)
(rule (Q44 x1 x2 x3 x4 x5) x2)
(rule (Q44 x1 x2 x3 x4 x5) x1)
(rule (R1 x1 x2 x3) x3)
(rule (R1 x1 x2 x3) x2)
(rule (R1 x1 x2 x3) x1)
(rule (R2 x1 x2 x3 x4) x4)
(rule (R2 x1 x2 x3 x4) x3)
(rule (R2 x1 x2 x3 x4) x2)
(rule (R2 x1 x2 x3 x4) x1)
(rule (R3 x1 x2 x3 x4 x5) x5)
(rule (R3 x1 x2 x3 x4 x5) x4)
(rule (R3 x1 x2 x3 x4 x5) x3)
(rule (R3 x1 x2 x3 x4 x5) x2)
(rule (R3 x1 x2 x3 x4 x5) x1)
(rule (R4 x1 x2 x3 x4 x5 x6) x6)
(rule (R4 x1 x2 x3 x4 x5 x6) x5)
(rule (R4 x1 x2 x3 x4 x5 x6) x4)
(rule (R4 x1 x2 x3 x4 x5 x6) x3)
(rule (R4 x1 x2 x3 x4 x5 x6) x2)
(rule (R4 x1 x2 x3 x4 x5 x6) x1)
(rule (P |0| |0| |0| |0| |0|) (S |0|))
(rule (+ x (S y)) (S (+ x y)))
(rule (a (l x)) (l (a (a x))))
(rule (l (o x)) (o (l (l x))))
(rule (o x) (l x))
(rule (l x) (a x))
(rule (a (S x)) (S (l x)))
(rule (a (+ x y)) (+ (l x) y))
(rule (a (+ x y)) (+ x (l y)))
(rule (a (P x1 x2 x3 x4 x5)) (P x1 x2 x3 x4 (l x5)))
(rule (a (P x1 x2 x3 x4 x5)) (P x1 x2 x3 (l x4) x5))
(rule (a (P x1 x2 x3 x4 x5)) (P x1 x2 (l x3) x4 x5))
(rule (a (P x1 x2 x3 x4 x5)) (P x1 (l x2) x3 x4 x5))
(rule (a (P x1 x2 x3 x4 x5)) (P (l x1) x2 x3 x4 x5))
(rule (+ x (o y)) (o (+ x y)))
(rule (P x1 x2 x3 x4 (o x5)) (o (P x1 x2 x3 x4 x5)))
(rule (P x1 x2 x3 (o x4) x5) (o (P x1 x2 x3 x4 x5)))
(rule (P x1 x2 (o x3) x4 x5) (o (P x1 x2 x3 x4 x5)))
(rule (P x1 (o x2) x3 x4 x5) (o (P x1 x2 x3 x4 x5)))
(rule (P (o x1) x2 x3 x4 x5) (o (P x1 x2 x3 x4 x5)))
(rule (M x1 x2 x3 x4 (l y)) (+ (M x1 x2 x3 x4 y) (P x1 x2 x3 x4 y)))
(rule (J4 x1 x2 x3 (l x4) y) (P x1 x2 x3 (J4 x1 x2 x3 x4 y) |0|))
(rule (J3 x1 x2 (l x3) y) (P x1 x2 (J3 x1 x2 x3 y) |0| |0|))
(rule (J2 x1 (l x2) y) (P x1 (J2 x1 x2 y) |0| |0| |0|))
(rule (J1 (l x1) y) (P (J1 x1 y) |0| |0| |0| |0|))
(rule (a (S x)) (o x))
(rule (P |0| |0| |0| |0| (S y)) (o (M |0| |0| |0| |0| y)))
(rule (P |0| |0| |0| |0| (P x1 x2 x3 x4 y)) (o (M x1 x2 x3 x4 y)))
(rule (P x1 x2 x3 (S x4) y) (o (J4 x1 x2 x3 x4 y)))
(rule (P x1 x2 (S x3) |0| y) (o (J3 x1 x2 x3 y)))
(rule (P x1 (S x2) |0| |0| y) (o (J2 x1 x2 y)))
(rule (P (S x1) |0| |0| |0| y) (o (J1 x1 y)))
(rule (P x1 x2 x3 (S x4) (S y)) (o (J4 x1 x2 x3 x4 (P x1 x2 x3 (S x4) y))))
(rule (P x1 x2 (S x3) |0| (S y)) (o (J3 x1 x2 x3 (P x1 x2 (S x3) |0| y))))
(rule (P x1 (S x2) |0| |0| (S y)) (o (J2 x1 x2 (P x1 (S x2) |0| |0| y))))
(rule (P (S x1) |0| |0| |0| (S y)) (o (J1 x1 (P (S x1) |0| |0| |0| y))))
(rule (a (P x1 x2 x3 x4 |0|)) (Q44 x1 x2 x3 (a x4) x4))
(rule (a (P x1 x2 x3 x4 |0|)) (Q43 x1 x2 x3 (a x4) x3))
(rule (a (P x1 x2 x3 x4 |0|)) (Q42 x1 x2 x3 (a x4) x2))
(rule (a (P x1 x2 x3 x4 |0|)) (Q41 x1 x2 x3 (a x4) x1))
(rule (a (P x1 x2 x3 |0| |0|)) (Q33 x1 x2 (a x3) x3))
(rule (a (P x1 x2 x3 |0| |0|)) (Q32 x1 x2 (a x3) x2))
(rule (a (P x1 x2 x3 |0| |0|)) (Q31 x1 x2 (a x3) x1))
(rule (a (P x1 x2 |0| |0| |0|)) (Q22 x1 (a x2) x2))
(rule (a (P x1 x2 |0| |0| |0|)) (Q21 x1 (a x2) x1))
(rule (a (P x1 |0| |0| |0| |0|)) (Q11 (a x1) x1))
(rule (Q44 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 y)))
(rule (Q43 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 y)))
(rule (Q42 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 y)))
(rule (Q41 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 y)))
(rule (Q33 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| y)))
(rule (Q32 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| y)))
(rule (Q31 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| y)))
(rule (Q22 x1 (o x2) y) (o (P x1 x2 |0| |0| y)))
(rule (Q21 x1 (o x2) y) (o (P x1 x2 |0| |0| y)))
(rule (Q11 (o x1) y) (o (P x1 |0| |0| |0| y)))
(rule (a (P x1 x2 x3 x4 (S y))) (R4 x1 x2 x3 (a x4) x4 y))
(rule (a (P x1 x2 x3 |0| (S y))) (R3 x1 x2 (a x3) x3 y))
(rule (a (P x1 x2 |0| |0| (S y))) (R2 x1 (a x2) x2 y))
(rule (a (P x1 |0| |0| |0| (S y))) (R1 (a x1) x1 y))
(rule (R4 x1 x2 x3 (o x4) y z) (o (P x1 x2 x3 x4 (P x1 x2 x3 y z))))
(rule (R3 x1 x2 (o x3) y z) (o (P x1 x2 x3 |0| (P x1 x2 y |0| z))))
(rule (R2 x1 (o x2) y z) (o (P x1 x2 |0| |0| (P x1 y |0| |0| z))))
(rule (R1 (o x1) y z) (o (P x1 |0| |0| |0| (P y |0| |0| |0| z))))