; @xtcfilename "./TRS_Standard/Hydras/lepper_8.xml"
(format TRS)
(fun a 1)
(fun o 1)
(fun l 1)
(fun S 1)
(fun + 2)
(fun P 9)
(fun M 9)
(fun J1 2)
(fun J2 3)
(fun J3 4)
(fun J4 5)
(fun J5 6)
(fun J6 7)
(fun J7 8)
(fun J8 9)
(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 Q51 6)
(fun Q52 6)
(fun Q53 6)
(fun Q54 6)
(fun Q55 6)
(fun Q61 7)
(fun Q62 7)
(fun Q63 7)
(fun Q64 7)
(fun Q65 7)
(fun Q66 7)
(fun Q71 8)
(fun Q72 8)
(fun Q73 8)
(fun Q74 8)
(fun Q75 8)
(fun Q76 8)
(fun Q77 8)
(fun Q81 9)
(fun Q82 9)
(fun Q83 9)
(fun Q84 9)
(fun Q85 9)
(fun Q86 9)
(fun Q87 9)
(fun Q88 9)
(fun R1 3)
(fun R2 4)
(fun R3 5)
(fun R4 6)
(fun R5 7)
(fun R6 8)
(fun R7 9)
(fun R8 10)
(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 x6 x7 x8 x9) x9)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 x9) 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 (J5 x1 x2 x3 x4 x5 x6) x6)
(rule (J5 x1 x2 x3 x4 x5 x6) x5)
(rule (J5 x1 x2 x3 x4 x5 x6) x4)
(rule (J5 x1 x2 x3 x4 x5 x6) x3)
(rule (J5 x1 x2 x3 x4 x5 x6) x2)
(rule (J5 x1 x2 x3 x4 x5 x6) x1)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (J6 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (J7 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (J8 x1 x2 x3 x4 x5 x6 x7 x8 x9) 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 (Q51 x1 x2 x3 x4 x5 x6) x6)
(rule (Q51 x1 x2 x3 x4 x5 x6) x5)
(rule (Q51 x1 x2 x3 x4 x5 x6) x4)
(rule (Q51 x1 x2 x3 x4 x5 x6) x3)
(rule (Q51 x1 x2 x3 x4 x5 x6) x2)
(rule (Q51 x1 x2 x3 x4 x5 x6) x1)
(rule (Q52 x1 x2 x3 x4 x5 x6) x6)
(rule (Q52 x1 x2 x3 x4 x5 x6) x5)
(rule (Q52 x1 x2 x3 x4 x5 x6) x4)
(rule (Q52 x1 x2 x3 x4 x5 x6) x3)
(rule (Q52 x1 x2 x3 x4 x5 x6) x2)
(rule (Q52 x1 x2 x3 x4 x5 x6) x1)
(rule (Q53 x1 x2 x3 x4 x5 x6) x6)
(rule (Q53 x1 x2 x3 x4 x5 x6) x5)
(rule (Q53 x1 x2 x3 x4 x5 x6) x4)
(rule (Q53 x1 x2 x3 x4 x5 x6) x3)
(rule (Q53 x1 x2 x3 x4 x5 x6) x2)
(rule (Q53 x1 x2 x3 x4 x5 x6) x1)
(rule (Q54 x1 x2 x3 x4 x5 x6) x6)
(rule (Q54 x1 x2 x3 x4 x5 x6) x5)
(rule (Q54 x1 x2 x3 x4 x5 x6) x4)
(rule (Q54 x1 x2 x3 x4 x5 x6) x3)
(rule (Q54 x1 x2 x3 x4 x5 x6) x2)
(rule (Q54 x1 x2 x3 x4 x5 x6) x1)
(rule (Q55 x1 x2 x3 x4 x5 x6) x6)
(rule (Q55 x1 x2 x3 x4 x5 x6) x5)
(rule (Q55 x1 x2 x3 x4 x5 x6) x4)
(rule (Q55 x1 x2 x3 x4 x5 x6) x3)
(rule (Q55 x1 x2 x3 x4 x5 x6) x2)
(rule (Q55 x1 x2 x3 x4 x5 x6) x1)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q61 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q62 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q63 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q64 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q65 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (Q66 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q71 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q72 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q73 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q74 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q75 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q76 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (Q77 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 x8 x9) 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 (R5 x1 x2 x3 x4 x5 x6 x7) x7)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x6)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x5)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x4)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x3)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x2)
(rule (R5 x1 x2 x3 x4 x5 x6 x7) x1)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x8)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x7)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x6)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x5)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x4)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x3)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x2)
(rule (R6 x1 x2 x3 x4 x5 x6 x7 x8) x1)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x9)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x8)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x7)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x6)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x5)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x4)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x3)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x2)
(rule (R7 x1 x2 x3 x4 x5 x6 x7 x8 x9) x1)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x10)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x9)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x8)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x7)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x6)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x5)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x4)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x3)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x2)
(rule (R8 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) x1)
(rule (P |0| |0| |0| |0| |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 x6 x7 x8 x9)) (P x1 x2 x3 x4 x5 x6 x7 x8 (l x9)))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 x3 x4 x5 x6 x7 (l x8) x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 x3 x4 x5 x6 (l x7) x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 x3 x4 x5 (l x6) x7 x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 x3 x4 (l x5) x6 x7 x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 x3 (l x4) x5 x6 x7 x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 x2 (l x3) x4 x5 x6 x7 x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P x1 (l x2) x3 x4 x5 x6 x7 x8 x9))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 x9)) (P (l x1) x2 x3 x4 x5 x6 x7 x8 x9))
(rule (+ x (o y)) (o (+ x y)))
(rule (P x1 x2 x3 x4 x5 x6 x7 x8 (o x9)) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 x3 x4 x5 x6 x7 (o x8) x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 x3 x4 x5 x6 (o x7) x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 x3 x4 x5 (o x6) x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 x3 x4 (o x5) x6 x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 x3 (o x4) x5 x6 x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 x2 (o x3) x4 x5 x6 x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P x1 (o x2) x3 x4 x5 x6 x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (P (o x1) x2 x3 x4 x5 x6 x7 x8 x9) (o (P x1 x2 x3 x4 x5 x6 x7 x8 x9)))
(rule (M x1 x2 x3 x4 x5 x6 x7 x8 (l y)) (+ (M x1 x2 x3 x4 x5 x6 x7 x8 y) (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (J8 x1 x2 x3 x4 x5 x6 x7 (l x8) y) (P x1 x2 x3 x4 x5 x6 x7 (J8 x1 x2 x3 x4 x5 x6 x7 x8 y) |0|))
(rule (J7 x1 x2 x3 x4 x5 x6 (l x7) y) (P x1 x2 x3 x4 x5 x6 (J7 x1 x2 x3 x4 x5 x6 x7 y) |0| |0|))
(rule (J6 x1 x2 x3 x4 x5 (l x6) y) (P x1 x2 x3 x4 x5 (J6 x1 x2 x3 x4 x5 x6 y) |0| |0| |0|))
(rule (J5 x1 x2 x3 x4 (l x5) y) (P x1 x2 x3 x4 (J5 x1 x2 x3 x4 x5 y) |0| |0| |0| |0|))
(rule (J4 x1 x2 x3 (l x4) y) (P x1 x2 x3 (J4 x1 x2 x3 x4 y) |0| |0| |0| |0| |0|))
(rule (J3 x1 x2 (l x3) y) (P x1 x2 (J3 x1 x2 x3 y) |0| |0| |0| |0| |0| |0|))
(rule (J2 x1 (l x2) y) (P x1 (J2 x1 x2 y) |0| |0| |0| |0| |0| |0| |0|))
(rule (J1 (l x1) y) (P (J1 x1 y) |0| |0| |0| |0| |0| |0| |0| |0|))
(rule (a (S x)) (o x))
(rule (P |0| |0| |0| |0| |0| |0| |0| |0| (S y)) (o (M |0| |0| |0| |0| |0| |0| |0| |0| y)))
(rule (P |0| |0| |0| |0| |0| |0| |0| |0| (P x1 x2 x3 x4 x5 x6 x7 x8 y)) (o (M x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (P x1 x2 x3 x4 x5 x6 x7 (S x8) y) (o (J8 x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (P x1 x2 x3 x4 x5 x6 (S x7) |0| y) (o (J7 x1 x2 x3 x4 x5 x6 x7 y)))
(rule (P x1 x2 x3 x4 x5 (S x6) |0| |0| y) (o (J6 x1 x2 x3 x4 x5 x6 y)))
(rule (P x1 x2 x3 x4 (S x5) |0| |0| |0| y) (o (J5 x1 x2 x3 x4 x5 y)))
(rule (P x1 x2 x3 (S x4) |0| |0| |0| |0| y) (o (J4 x1 x2 x3 x4 y)))
(rule (P x1 x2 (S x3) |0| |0| |0| |0| |0| y) (o (J3 x1 x2 x3 y)))
(rule (P x1 (S x2) |0| |0| |0| |0| |0| |0| y) (o (J2 x1 x2 y)))
(rule (P (S x1) |0| |0| |0| |0| |0| |0| |0| y) (o (J1 x1 y)))
(rule (P x1 x2 x3 x4 x5 x6 x7 (S x8) (S y)) (o (J8 x1 x2 x3 x4 x5 x6 x7 x8 (P x1 x2 x3 x4 x5 x6 x7 (S x8) y))))
(rule (P x1 x2 x3 x4 x5 x6 (S x7) |0| (S y)) (o (J7 x1 x2 x3 x4 x5 x6 x7 (P x1 x2 x3 x4 x5 x6 (S x7) |0| y))))
(rule (P x1 x2 x3 x4 x5 (S x6) |0| |0| (S y)) (o (J6 x1 x2 x3 x4 x5 x6 (P x1 x2 x3 x4 x5 (S x6) |0| |0| y))))
(rule (P x1 x2 x3 x4 (S x5) |0| |0| |0| (S y)) (o (J5 x1 x2 x3 x4 x5 (P x1 x2 x3 x4 (S x5) |0| |0| |0| y))))
(rule (P x1 x2 x3 (S x4) |0| |0| |0| |0| (S y)) (o (J4 x1 x2 x3 x4 (P x1 x2 x3 (S x4) |0| |0| |0| |0| y))))
(rule (P x1 x2 (S x3) |0| |0| |0| |0| |0| (S y)) (o (J3 x1 x2 x3 (P x1 x2 (S x3) |0| |0| |0| |0| |0| y))))
(rule (P x1 (S x2) |0| |0| |0| |0| |0| |0| (S y)) (o (J2 x1 x2 (P x1 (S x2) |0| |0| |0| |0| |0| |0| y))))
(rule (P (S x1) |0| |0| |0| |0| |0| |0| |0| (S y)) (o (J1 x1 (P (S x1) |0| |0| |0| |0| |0| |0| |0| y))))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q88 x1 x2 x3 x4 x5 x6 x7 (a x8) x8))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q87 x1 x2 x3 x4 x5 x6 x7 (a x8) x7))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q86 x1 x2 x3 x4 x5 x6 x7 (a x8) x6))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q85 x1 x2 x3 x4 x5 x6 x7 (a x8) x5))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q84 x1 x2 x3 x4 x5 x6 x7 (a x8) x4))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q83 x1 x2 x3 x4 x5 x6 x7 (a x8) x3))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q82 x1 x2 x3 x4 x5 x6 x7 (a x8) x2))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 |0|)) (Q81 x1 x2 x3 x4 x5 x6 x7 (a x8) x1))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q77 x1 x2 x3 x4 x5 x6 (a x7) x7))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q76 x1 x2 x3 x4 x5 x6 (a x7) x6))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q75 x1 x2 x3 x4 x5 x6 (a x7) x5))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q74 x1 x2 x3 x4 x5 x6 (a x7) x4))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q73 x1 x2 x3 x4 x5 x6 (a x7) x3))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q72 x1 x2 x3 x4 x5 x6 (a x7) x2))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| |0|)) (Q71 x1 x2 x3 x4 x5 x6 (a x7) x1))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q66 x1 x2 x3 x4 x5 (a x6) x6))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q65 x1 x2 x3 x4 x5 (a x6) x5))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q64 x1 x2 x3 x4 x5 (a x6) x4))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q63 x1 x2 x3 x4 x5 (a x6) x3))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q62 x1 x2 x3 x4 x5 (a x6) x2))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| |0|)) (Q61 x1 x2 x3 x4 x5 (a x6) x1))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| |0|)) (Q55 x1 x2 x3 x4 (a x5) x5))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| |0|)) (Q54 x1 x2 x3 x4 (a x5) x4))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| |0|)) (Q53 x1 x2 x3 x4 (a x5) x3))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| |0|)) (Q52 x1 x2 x3 x4 (a x5) x2))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| |0|)) (Q51 x1 x2 x3 x4 (a x5) x1))
(rule (a (P x1 x2 x3 x4 |0| |0| |0| |0| |0|)) (Q44 x1 x2 x3 (a x4) x4))
(rule (a (P x1 x2 x3 x4 |0| |0| |0| |0| |0|)) (Q43 x1 x2 x3 (a x4) x3))
(rule (a (P x1 x2 x3 x4 |0| |0| |0| |0| |0|)) (Q42 x1 x2 x3 (a x4) x2))
(rule (a (P x1 x2 x3 x4 |0| |0| |0| |0| |0|)) (Q41 x1 x2 x3 (a x4) x1))
(rule (a (P x1 x2 x3 |0| |0| |0| |0| |0| |0|)) (Q33 x1 x2 (a x3) x3))
(rule (a (P x1 x2 x3 |0| |0| |0| |0| |0| |0|)) (Q32 x1 x2 (a x3) x2))
(rule (a (P x1 x2 x3 |0| |0| |0| |0| |0| |0|)) (Q31 x1 x2 (a x3) x1))
(rule (a (P x1 x2 |0| |0| |0| |0| |0| |0| |0|)) (Q22 x1 (a x2) x2))
(rule (a (P x1 x2 |0| |0| |0| |0| |0| |0| |0|)) (Q21 x1 (a x2) x1))
(rule (a (P x1 |0| |0| |0| |0| |0| |0| |0| |0|)) (Q11 (a x1) x1))
(rule (Q88 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q87 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q86 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q85 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q84 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q83 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q82 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q81 x1 x2 x3 x4 x5 x6 x7 (o x8) y) (o (P x1 x2 x3 x4 x5 x6 x7 x8 y)))
(rule (Q77 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q76 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q75 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q74 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q73 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q72 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q71 x1 x2 x3 x4 x5 x6 (o x7) y) (o (P x1 x2 x3 x4 x5 x6 x7 |0| y)))
(rule (Q66 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q65 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q64 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q63 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q62 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q61 x1 x2 x3 x4 x5 (o x6) y) (o (P x1 x2 x3 x4 x5 x6 |0| |0| y)))
(rule (Q55 x1 x2 x3 x4 (o x5) y) (o (P x1 x2 x3 x4 x5 |0| |0| |0| y)))
(rule (Q54 x1 x2 x3 x4 (o x5) y) (o (P x1 x2 x3 x4 x5 |0| |0| |0| y)))
(rule (Q53 x1 x2 x3 x4 (o x5) y) (o (P x1 x2 x3 x4 x5 |0| |0| |0| y)))
(rule (Q52 x1 x2 x3 x4 (o x5) y) (o (P x1 x2 x3 x4 x5 |0| |0| |0| y)))
(rule (Q51 x1 x2 x3 x4 (o x5) y) (o (P x1 x2 x3 x4 x5 |0| |0| |0| y)))
(rule (Q44 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 |0| |0| |0| |0| y)))
(rule (Q43 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 |0| |0| |0| |0| y)))
(rule (Q42 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 |0| |0| |0| |0| y)))
(rule (Q41 x1 x2 x3 (o x4) y) (o (P x1 x2 x3 x4 |0| |0| |0| |0| y)))
(rule (Q33 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| |0| |0| |0| |0| y)))
(rule (Q32 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| |0| |0| |0| |0| y)))
(rule (Q31 x1 x2 (o x3) y) (o (P x1 x2 x3 |0| |0| |0| |0| |0| y)))
(rule (Q22 x1 (o x2) y) (o (P x1 x2 |0| |0| |0| |0| |0| |0| y)))
(rule (Q21 x1 (o x2) y) (o (P x1 x2 |0| |0| |0| |0| |0| |0| y)))
(rule (Q11 (o x1) y) (o (P x1 |0| |0| |0| |0| |0| |0| |0| y)))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 x8 (S y))) (R8 x1 x2 x3 x4 x5 x6 x7 (a x8) x8 y))
(rule (a (P x1 x2 x3 x4 x5 x6 x7 |0| (S y))) (R7 x1 x2 x3 x4 x5 x6 (a x7) x7 y))
(rule (a (P x1 x2 x3 x4 x5 x6 |0| |0| (S y))) (R6 x1 x2 x3 x4 x5 (a x6) x6 y))
(rule (a (P x1 x2 x3 x4 x5 |0| |0| |0| (S y))) (R5 x1 x2 x3 x4 (a x5) x5 y))
(rule (a (P x1 x2 x3 x4 |0| |0| |0| |0| (S y))) (R4 x1 x2 x3 (a x4) x4 y))
(rule (a (P x1 x2 x3 |0| |0| |0| |0| |0| (S y))) (R3 x1 x2 (a x3) x3 y))
(rule (a (P x1 x2 |0| |0| |0| |0| |0| |0| (S y))) (R2 x1 (a x2) x2 y))
(rule (a (P x1 |0| |0| |0| |0| |0| |0| |0| (S y))) (R1 (a x1) x1 y))
(rule (R8 x1 x2 x3 x4 x5 x6 x7 (o x8) y z) (o (P x1 x2 x3 x4 x5 x6 x7 x8 (P x1 x2 x3 x4 x5 x6 x7 y z))))
(rule (R7 x1 x2 x3 x4 x5 x6 (o x7) y z) (o (P x1 x2 x3 x4 x5 x6 x7 |0| (P x1 x2 x3 x4 x5 x6 y |0| z))))
(rule (R6 x1 x2 x3 x4 x5 (o x6) y z) (o (P x1 x2 x3 x4 x5 x6 |0| |0| (P x1 x2 x3 x4 x5 y |0| |0| z))))
(rule (R5 x1 x2 x3 x4 (o x5) y z) (o (P x1 x2 x3 x4 x5 |0| |0| |0| (P x1 x2 x3 x4 y |0| |0| |0| z))))
(rule (R4 x1 x2 x3 (o x4) y z) (o (P x1 x2 x3 x4 |0| |0| |0| |0| (P x1 x2 x3 y |0| |0| |0| |0| z))))
(rule (R3 x1 x2 (o x3) y z) (o (P x1 x2 x3 |0| |0| |0| |0| |0| (P x1 x2 y |0| |0| |0| |0| |0| z))))
(rule (R2 x1 (o x2) y z) (o (P x1 x2 |0| |0| |0| |0| |0| |0| (P x1 y |0| |0| |0| |0| |0| |0| z))))
(rule (R1 (o x1) y z) (o (P x1 |0| |0| |0| |0| |0| |0| |0| (P y |0| |0| |0| |0| |0| |0| |0| z))))