; @origtpdbfilename ./TRS/Rubio/bn129.trs
; @xtcfilename "./TRS_Standard/Rubio_04/bn129.xml"
(format TRS)
(fun plus 2)
(fun s 1)
(rule (plus (s X) (plus Y Z)) (plus X (plus (s (s Y)) Z)))
(rule (plus (s X1) (plus X2 (plus X3 X4))) (plus X1 (plus X3 (plus X2 X4))))