; @origtpdbfilename ./TRS/HM/t005.trs
; @xtcfilename "./TRS_Standard/HirokawaMiddeldorp_04/t005.xml"
(format TRS)
(fun c 2)
(fun |0| 0)
(fun + 2)
(fun |1| 0)
(fun |2| 0)
(fun |3| 0)
(fun |4| 0)
(fun |5| 0)
(fun |6| 0)
(fun |7| 0)
(fun |8| 0)
(fun |9| 0)
(fun * 2)
(rule (c |0| x) x)
(rule (c x (c y z)) (c (+ x y) z))
(rule (+ |0| |0|) |0|)
(rule (+ |0| |1|) |1|)
(rule (+ |0| |2|) |2|)
(rule (+ |0| |3|) |3|)
(rule (+ |0| |4|) |4|)
(rule (+ |0| |5|) |5|)
(rule (+ |0| |6|) |6|)
(rule (+ |0| |7|) |7|)
(rule (+ |0| |8|) |8|)
(rule (+ |0| |9|) |9|)
(rule (+ |1| |0|) |1|)
(rule (+ |1| |1|) |2|)
(rule (+ |1| |2|) |3|)
(rule (+ |1| |3|) |4|)
(rule (+ |1| |4|) |5|)
(rule (+ |1| |5|) |6|)
(rule (+ |1| |6|) |7|)
(rule (+ |1| |7|) |8|)
(rule (+ |1| |8|) |9|)
(rule (+ |1| |9|) (c |1| |0|))
(rule (+ |2| |0|) |2|)
(rule (+ |2| |1|) |3|)
(rule (+ |2| |2|) |4|)
(rule (+ |2| |3|) |5|)
(rule (+ |2| |4|) |6|)
(rule (+ |2| |5|) |7|)
(rule (+ |2| |6|) |8|)
(rule (+ |2| |7|) |9|)
(rule (+ |2| |8|) (c |1| |0|))
(rule (+ |2| |9|) (c |1| |1|))
(rule (+ |3| |0|) |3|)
(rule (+ |3| |1|) |4|)
(rule (+ |3| |2|) |5|)
(rule (+ |3| |3|) |6|)
(rule (+ |3| |4|) |7|)
(rule (+ |3| |5|) |8|)
(rule (+ |3| |6|) |9|)
(rule (+ |3| |7|) (c |1| |0|))
(rule (+ |3| |8|) (c |1| |1|))
(rule (+ |3| |9|) (c |1| |2|))
(rule (+ |4| |0|) |4|)
(rule (+ |4| |1|) |5|)
(rule (+ |4| |2|) |6|)
(rule (+ |4| |3|) |7|)
(rule (+ |4| |4|) |8|)
(rule (+ |4| |5|) |9|)
(rule (+ |4| |6|) (c |1| |0|))
(rule (+ |4| |7|) (c |1| |1|))
(rule (+ |4| |8|) (c |1| |2|))
(rule (+ |4| |9|) (c |1| |3|))
(rule (+ |5| |0|) |5|)
(rule (+ |5| |1|) |6|)
(rule (+ |5| |2|) |7|)
(rule (+ |5| |3|) |8|)
(rule (+ |5| |4|) |9|)
(rule (+ |5| |5|) (c |1| |0|))
(rule (+ |5| |6|) (c |1| |1|))
(rule (+ |5| |7|) (c |1| |2|))
(rule (+ |5| |8|) (c |1| |3|))
(rule (+ |5| |9|) (c |1| |4|))
(rule (+ |6| |0|) |6|)
(rule (+ |6| |1|) |7|)
(rule (+ |6| |2|) |8|)
(rule (+ |6| |3|) |9|)
(rule (+ |6| |4|) (c |1| |0|))
(rule (+ |6| |5|) (c |1| |1|))
(rule (+ |6| |6|) (c |1| |2|))
(rule (+ |6| |7|) (c |1| |3|))
(rule (+ |6| |8|) (c |1| |4|))
(rule (+ |6| |9|) (c |1| |5|))
(rule (+ |7| |0|) |7|)
(rule (+ |7| |1|) |8|)
(rule (+ |7| |2|) |9|)
(rule (+ |7| |3|) (c |1| |0|))
(rule (+ |7| |4|) (c |1| |1|))
(rule (+ |7| |5|) (c |1| |2|))
(rule (+ |7| |6|) (c |1| |3|))
(rule (+ |7| |7|) (c |1| |4|))
(rule (+ |7| |8|) (c |1| |5|))
(rule (+ |7| |9|) (c |1| |6|))
(rule (+ |8| |0|) |8|)
(rule (+ |8| |1|) |9|)
(rule (+ |8| |2|) (c |1| |0|))
(rule (+ |8| |3|) (c |1| |1|))
(rule (+ |8| |4|) (c |1| |2|))
(rule (+ |8| |5|) (c |1| |3|))
(rule (+ |8| |6|) (c |1| |4|))
(rule (+ |8| |7|) (c |1| |5|))
(rule (+ |8| |8|) (c |1| |6|))
(rule (+ |8| |9|) (c |1| |7|))
(rule (+ |9| |0|) |9|)
(rule (+ |9| |1|) (c |1| |0|))
(rule (+ |9| |2|) (c |1| |1|))
(rule (+ |9| |3|) (c |1| |2|))
(rule (+ |9| |4|) (c |1| |3|))
(rule (+ |9| |5|) (c |1| |4|))
(rule (+ |9| |6|) (c |1| |5|))
(rule (+ |9| |7|) (c |1| |6|))
(rule (+ |9| |8|) (c |1| |7|))
(rule (+ |9| |9|) (c |1| |8|))
(rule (+ x (c y z)) (c y (+ x z)))
(rule (+ (c x y) z) (c x (+ y z)))
(rule (* |0| |0|) |0|)
(rule (* |0| |1|) |0|)
(rule (* |0| |2|) |0|)
(rule (* |0| |3|) |0|)
(rule (* |0| |4|) |0|)
(rule (* |0| |5|) |0|)
(rule (* |0| |6|) |0|)
(rule (* |0| |7|) |0|)
(rule (* |0| |8|) |0|)
(rule (* |0| |9|) |0|)
(rule (* |1| |0|) |0|)
(rule (* |1| |1|) |1|)
(rule (* |1| |2|) |2|)
(rule (* |1| |3|) |3|)
(rule (* |1| |4|) |4|)
(rule (* |1| |5|) |5|)
(rule (* |1| |6|) |6|)
(rule (* |1| |7|) |7|)
(rule (* |1| |8|) |8|)
(rule (* |1| |9|) |9|)
(rule (* |2| |0|) |0|)
(rule (* |2| |1|) |2|)
(rule (* |2| |2|) |4|)
(rule (* |2| |3|) |6|)
(rule (* |2| |4|) |8|)
(rule (* |2| |5|) (c |1| |0|))
(rule (* |2| |6|) (c |1| |2|))
(rule (* |2| |7|) (c |1| |4|))
(rule (* |2| |8|) (c |1| |6|))
(rule (* |2| |9|) (c |1| |8|))
(rule (* |3| |0|) |0|)
(rule (* |3| |1|) |3|)
(rule (* |3| |2|) |6|)
(rule (* |3| |3|) |9|)
(rule (* |3| |4|) (c |1| |2|))
(rule (* |3| |5|) (c |1| |5|))
(rule (* |3| |6|) (c |1| |8|))
(rule (* |3| |7|) (c |2| |1|))
(rule (* |3| |8|) (c |2| |4|))
(rule (* |3| |9|) (c |2| |7|))
(rule (* |4| |0|) |0|)
(rule (* |4| |1|) |4|)
(rule (* |4| |2|) |8|)
(rule (* |4| |3|) (c |1| |2|))
(rule (* |4| |4|) (c |1| |6|))
(rule (* |4| |5|) (c |2| |0|))
(rule (* |4| |6|) (c |2| |4|))
(rule (* |4| |7|) (c |2| |8|))
(rule (* |4| |8|) (c |3| |2|))
(rule (* |4| |9|) (c |3| |6|))
(rule (* |5| |0|) |0|)
(rule (* |5| |1|) |5|)
(rule (* |5| |2|) (c |1| |0|))
(rule (* |5| |3|) (c |1| |5|))
(rule (* |5| |4|) (c |2| |0|))
(rule (* |5| |5|) (c |2| |5|))
(rule (* |5| |6|) (c |3| |0|))
(rule (* |5| |7|) (c |3| |5|))
(rule (* |5| |8|) (c |4| |0|))
(rule (* |5| |9|) (c |4| |5|))
(rule (* |6| |0|) |0|)
(rule (* |6| |1|) |6|)
(rule (* |6| |2|) (c |1| |2|))
(rule (* |6| |3|) (c |1| |8|))
(rule (* |6| |4|) (c |2| |4|))
(rule (* |6| |5|) (c |3| |0|))
(rule (* |6| |6|) (c |3| |6|))
(rule (* |6| |7|) (c |4| |2|))
(rule (* |6| |8|) (c |4| |8|))
(rule (* |6| |9|) (c |5| |4|))
(rule (* |7| |0|) |0|)
(rule (* |7| |1|) |7|)
(rule (* |7| |2|) (c |1| |4|))
(rule (* |7| |3|) (c |2| |1|))
(rule (* |7| |4|) (c |2| |8|))
(rule (* |7| |5|) (c |3| |5|))
(rule (* |7| |6|) (c |4| |2|))
(rule (* |7| |7|) (c |4| |9|))
(rule (* |7| |8|) (c |5| |6|))
(rule (* |7| |9|) (c |6| |3|))
(rule (* |8| |0|) |0|)
(rule (* |8| |1|) |8|)
(rule (* |8| |2|) (c |1| |8|))
(rule (* |8| |3|) (c |2| |4|))
(rule (* |8| |4|) (c |3| |2|))
(rule (* |8| |5|) (c |4| |0|))
(rule (* |8| |6|) (c |4| |8|))
(rule (* |8| |7|) (c |5| |6|))
(rule (* |8| |8|) (c |6| |4|))
(rule (* |8| |9|) (c |7| |2|))
(rule (* |9| |0|) |0|)
(rule (* |9| |1|) |9|)
(rule (* |9| |2|) (c |1| |8|))
(rule (* |9| |3|) (c |2| |7|))
(rule (* |9| |4|) (c |3| |6|))
(rule (* |9| |5|) (c |4| |5|))
(rule (* |9| |6|) (c |5| |4|))
(rule (* |9| |7|) (c |6| |3|))
(rule (* |9| |8|) (c |7| |2|))
(rule (* |9| |9|) (c |8| |1|))
(rule (* x (c y z)) (c (* x y) (* x z)))
(rule (* (c x y) z) (c (* x z) (* y z)))