; @origtpdbfilename ./TRS/various/08.trs
; @xtcfilename "./TRS_Standard/Various_04/08.xml"
(format TRS)
(fun f1 2)
(fun a 0)
(fun g1 2)
(fun g2 2)
(fun f2 2)
(fun h1 1)
(fun h2 1)
(fun i 0)
(fun e1 6)
(fun e2 6)
(fun e5 4)
(fun e3 12)
(fun e6 3)
(fun e4 12)
(rule (f1 a x) (g1 x x))
(rule (f1 x a) (g2 x x))
(rule (f2 a x) (g1 x x))
(rule (f2 x a) (g2 x x))
(rule (g1 a x) (h1 x))
(rule (g1 x a) (h2 x))
(rule (g2 a x) (h1 x))
(rule (g2 x a) (h2 x))
(rule (h1 a) i)
(rule (h2 a) i)
(rule (e1 (h1 w) (h2 w) x y z w) (e2 x x y z z w))
(rule (e1 x1 x1 x y z a) (e5 x1 x y z))
(rule (e2 (f1 w w) x y z (f2 w w) w) (e3 x y x y y z y z x y z w))
(rule (e2 x x y z z a) (e6 x y z))
(rule (e2 i x y z i a) (e6 x y z))
(rule (e3 x1 x1 x2 x2 x3 x3 x4 x4 x y z w) (e4 x1 x1 x2 x2 x3 x3 x4 x4 x y z w))
(rule (e3 x y x y y z y z x y z a) (e6 x y z))
(rule (e4 (g1 w w) x1 (g2 w w) x1 (g1 w w) x1 (g2 w w) x1 x y z w) (e1 x1 x1 x y z w))
(rule (e4 i x1 i x1 i x1 i x1 x y z a) (e5 x1 x y z))
(rule (e4 x x x x x x x x x x x a) (e6 x x x))
(rule (e5 i x y z) (e6 x y z))