metagraphoptimization.jl/input/ABAB->ABC.txt

['A1', 'B1', 'A2', 'B2', 'A3', 'B3', 'C1', 'B(C1,A1)', 'C(B(C1,A1),A2)', 'A(C(B(C1,A1),A2),B1)', 'C(A(C(B(C1,A1),A2),B1),B2)', 'M(C(A(C(B(C1,A1),A2),B1),B2),A3,B3)', 'C(A(C(B(C1,A1),A2),B1),B3)', 'M(C(A(C(B(C1,A1),A2),B1),B3),B2,A3)', 'A(C(B(C1,A1),A2),B2)', 'C(A(C(B(C1,A1),A2),B2),B1)', 'M(C(A(C(B(C1,A1),A2),B2),B1),A3,B3)', 'C(A(C(B(C1,A1),A2),B2),B3)', 'M(C(A(C(B(C1,A1),A2),B2),B3),B1,A3)', 'A(C(B(C1,A1),A2),B3)', 'C(A(C(B(C1,A1),A2),B3),B1)', 'M(C(A(C(B(C1,A1),A2),B3),B1),B2,A3)', 'C(A(C(B(C1,A1),A2),B3),B2)', 'M(C(A(C(B(C1,A1),A2),B3),B2),B1,A3)', 'C(B(C1,A1),A3)', 'A(C(B(C1,A1),A3),B1)', 'C(A(C(B(C1,A1),A3),B1),B2)', 'M(C(A(C(B(C1,A1),A3),B1),B2),A2,B3)', 'C(A(C(B(C1,A1),A3),B1),B3)', 'M(C(A(C(B(C1,A1),A3),B1),B3),A2,B2)', 'A(C(B(C1,A1),A3),B2)', 'C(A(C(B(C1,A1),A3),B2),B1)', 'M(C(A(C(B(C1,A1),A3),B2),B1),A2,B3)', 'C(A(C(B(C1,A1),A3),B2),B3)', 'M(C(A(C(B(C1,A1),A3),B2),B3),B1,A2)', 'A(C(B(C1,A1),A3),B3)', 'C(A(C(B(C1,A1),A3),B3),B1)', 'M(C(A(C(B(C1,A1),A3),B3),B1),A2,B2)', 'C(A(C(B(C1,A1),A3),B3),B2)', 'M(C(A(C(B(C1,A1),A3),B3),B2),B1,A2)', 'A(C1,B1)', 'C(A(C1,B1),B2)', 'B(C(A(C1,B1),B2),A1)', 'C(B(C(A(C1,B1),B2),A1),A2)', 'M(C(B(C(A(C1,B1),B2),A1),A2),A3,B3)', 'C(B(C(A(C1,B1),B2),A1),A3)', 'M(C(B(C(A(C1,B1),B2),A1),A3),A2,B3)', 'B(C(A(C1,B1),B2),A2)', 'C(B(C(A(C1,B1),B2),A2),A1)', 'M(C(B(C(A(C1,B1),B2),A2),A1),A3,B3)', 'C(B(C(A(C1,B1),B2),A2),A3)', 'M(C(B(C(A(C1,B1),B2),A2),A3),A1,B3)', 'B(C(A(C1,B1),B2),A3)', 'C(B(C(A(C1,B1),B2),A3),A1)', 'M(C(B(C(A(C1,B1),B2),A3),A1),A2,B3)', 'C(B(C(A(C1,B1),B2),A3),A2)', 'M(C(B(C(A(C1,B1),B2),A3),A2),A1,B3)', 'C(A(C1,B1),B3)', 'B(C(A(C1,B1),B3),A1)', 'C(B(C(A(C1,B1),B3),A1),A2)', 'M(C(B(C(A(C1,B1),B3),A1),A2),B2,A3)', 'C(B(C(A(C1,B1),B3),A1),A3)', 'M(C(B(C(A(C1,B1),B3),A1),A3),A2,B2)', 'B(C(A(C1,B1),B3),A2)', 'C(B(C(A(C1,B1),B3),A2),A1)', 'M(C(B(C(A(C1,B1),B3),A2),A1),B2,A3)', 'C(B(C(A(C1,B1),B3),A2),A3)', 'M(C(B(C(A(C1,B1),B3),A2),A3),A1,B2)', 'B(C(A(C1,B1),B3),A3)', 'C(B(C(A(C1,B1),B3),A3),A1)', 'M(C(B(C(A(C1,B1),B3),A3),A1),A2,B2)', 'C(B(C(A(C1,B1),B3),A3),A2)', 'M(C(B(C(A(C1,B1),B3),A3),A2),A1,B2)', 'B(C1,A2)', 'C(B(C1,A2),A1)', 'A(C(B(C1,A2),A1),B1)', 'C(A(C(B(C1,A2),A1),B1),B2)', 'M(C(A(C(B(C1,A2),A1),B1),B2),A3,B3)', 'C(A(C(B(C1,A2),A1),B1),B3)', 'M(C(A(C(B(C1,A2),A1),B1),B3),B2,A3)', 'A(C(B(C1,A2),A1),B2)', 'C(A(C(B(C1,A2),A1),B2),B1)', 'M(C(A(C(B(C1,A2),A1),B2),B1),A3,B3)', 'C(A(C(B(C1,A2),A1),B2),B3)', 'M(C(A(C(B(C1,A2),A1),B2),B3),B1,A3)', 'A(C(B(C1,A2),A1),B3)', 'C(A(C(B(C1,A2),A1),B3),B1)', 'M(C(A(C(B(C1,A2),A1),B3),B1),B2,A3)', 'C(A(C(B(C1,A2),A1),B3),B2)', 'M(C(A(C(B(C1,A2),A1),B3),B2),B1,A3)', 'C(B(C1,A2),A3)', 'A(C(B(C1,A2),A3),B1)', 'C(A(C(B(C1,A2),A3),B1),B2)', 'M(C(A(C(B(C1,A2),A3),B1),B2),A1,B3)', 'C(A(C(B(C1,A2),A3),B1),B3)', 'M(C(A(C(B(C1,A2),A3),B1),B3),A1,B2)', 'A(C(B(C1,A2),A3),B2)', 'C(A(C(B(C1,A2),A3),B2),B1)', 'M(C(A(C(B(C1,A2),A3),B2),B1),A1,B3)', 'C(A(C(B(C1,A2),A3),B2),B3)', 'M(C(A(C(B(C1,A2),A3),B2),B3),A1,B1)', 'A(C(B(C1,A2),A3),B3)', 'C(A(C(B(C1,A2),A3),B3),B1)', 'M(C(A(C(B(C1,A2),A3),B3),B1),A1,B2)', 'C(A(C(B(C1,A2),A3),B3),B2)', 'M(C(A(C(B(C1,A2),A3),B3),B2),A1,B1)', 'A(C1,B2)', 'C(A(C1,B2),B1)', 'B(C(A(C1,B2),B1),A1)', 'C(B(C(A(C1,B2),B1),A1),A2)', 'M(C(B(C(A(C1,B2),B1),A1),A2),A3,B3)', 'C(B(C(A(C1,B2),B1),A1),A3)', 'M(C(B(C(A(C1,B2),B1),A1),A3),A2,B3)', 'B(C(A(C1,B2),B1),A2)', 'C(B(C(A(C1,B2),B1),A2),A1)', 'M(C(B(C(A(C1,B2),B1),A2),A1),A3,B3)', 'C(B(C(A(C1,B2),B1),A2),A3)', 'M(C(B(C(A(C1,B2),B1),A2),A3),A1,B3)', 'B(C(A(C1,B2),B1),A3)', 'C(B(C(A(C1,B2),B1),A3),A1)', 'M(C(B(C(A(C1,B2),B1),A3),A1),A2,B3)', 'C(B(C(A(C1,B2),B1),A3),A2)', 'M(C(B(C(A(C1,B2),B1),A3),A2),A1,B3)', 'C(A(C1,B2),B3)', 'B(C(A(C1,B2),B3),A1)', 'C(B(C(A(C1,B2),B3),A1),A2)', 'M(C(B(C(A(C1,B2),B3),A1),A2),B1,A3)', 'C(B(C(A(C1,B2),B3),A1),A3)', 'M(C(B(C(A(C1,B2),B3),A1),A3),B1,A2)', 'B(C(A(C1,B2),B3),A2)', 'C(B(C(A(C1,B2),B3),A2),A1)', 'M(C(B(C(A(C1,B2),B3),A2),A1),B1,A3)', 'C(B(C(A(C1,B2),B3),A2),A3)', 'M(C(B(C(A(C1,B2),B3),A2),A3),A1,B1)', 'B(C(A(C1,B2),B3),A3)', 'C(B(C(A(C1,B2),B3),A3),A1)', 'M(C(B(C(A(C1,B2),B3),A3),A1),B1,A2)', 'C(B(C(A(C1,B2),B3),A3),A2)', 'M(C(B(C(A(C1,B2),B3),A3),A2),A1,B1)', 'B(C1,A3)', 'C(B(C1,A3),A1)', 'A(C(B(C1,A3),A1),B1)', 'C(A(C(B(C1,A3),A1),B1),B2)', 'M(C(A(C(B(C1,A3),A1),B1),B2),A2,B3)', 'C(A(C(B(C1,A3),A1),B1),B3)', 'M(C(A(C(B(C1,A3),A1),B1),B3),A2,B2)', 'A(C(B(C1,A3),A1),B2)', 'C(A(C(B(C1,A3),A1),B2),B1)', 'M(C(A(C(B(C1,A3),A1),B2),B1),A2,B3)', 'C(A(C(B(C1,A3),A1),B2),B3)', 'M(C(A(C(B(C1,A3),A1),B2),B3),B1,A2)', 'A(C(B(C1,A3),A1),B3)', 'C(A(C(B(C1,A3),A1),B3),B1)', 'M(C(A(C(B(C1,A3),A1),B3),B1),A2,B2)', 'C(A(C(B(C1,A3),A1),B3),B2)', 'M(C(A(C(B(C1,A3),A1),B3),B2),B1,A2)', 'C(B(C1,A3),A2)', 'A(C(B(C1,A3),A2),B1)', 'C(A(C(B(C1,A3),A2),B1),B2)', 'M(C(A(C(B(C1,A3),A2),B1),B2),A1,B3)', 'C(A(C(B(C1,A3),A2),B1),B3)', 'M(C(A(C(B(C1,A3),A2),B1),B3),A1,B2)', 'A(C(B(C1,A3),A2),B2)', 'C(A(C(B(C1,A3),A2),B2),B1)', 'M(C(A(C(B(C1,A3),A2),B2),B1),A1,B3)', 'C(A(C(B(C1,A3),A2),B2),B3)', 'M(C(A(C(B(C1,A3),A2),B2),B3),A1,B1)', 'A(C(B(C1,A3),A2),B3)', 'C(A(C(B(C1,A3),A2),B3),B1)', 'M(C(A(C(B(C1,A3),A2),B3),B1),A1,B2)', 'C(A(C(B(C1,A3),A2),B3),B2)', 'M(C(A(C(B(C1,A3),A2),B3),B2),A1,B1)', 'A(C1,B3)', 'C(A(C1,B3),B1)', 'B(C(A(C1,B3),B1),A1)', 'C(B(C(A(C1,B3),B1),A1),A2)', 'M(C(B(C(A(C1,B3),B1),A1),A2),B2,A3)', 'C(B(C(A(C1,B3),B1),A1),A3)', 'M(C(B(C(A(C1,B3),B1),A1),A3),A2,B2)', 'B(C(A(C1,B3),B1),A2)', 'C(B(C(A(C1,B3),B1),A2),A1)', 'M(C(B(C(A(C1,B3),B1),A2),A1),B2,A3)', 'C(B(C(A(C1,B3),B1),A2),A3)', 'M(C(B(C(A(C1,B3),B1),A2),A3),A1,B2)', 'B(C(A(C1,B3),B1),A3)', 'C(B(C(A(C1,B3),B1),A3),A1)', 'M(C(B(C(A(C1,B3),B1),A3),A1),A2,B2)', 'C(B(C(A(C1,B3),B1),A3),A2)', 'M(C(B(C(A(C1,B3),B1),A3),A2),A1,B2)', 'C(A(C1,B3),B2)', 'B(C(A(C1,B3),B2),A1)', 'C(B(C(A(C1,B3),B2),A1),A2)', 'M(C(B(C(A(C1,B3),B2),A1),A2),B1,A3)', 'C(B(C(A(C1,B3),B2),A1),A3)', 'M(C(B(C(A(C1,B3),B2),A1),A3),B1,A2)', 'B(C(A(C1,B3),B2),A2)', 'C(B(C(A(C1,B3),B2),A2),A1)', 'M(C(B(C(A(C1,B3),B2),A2),A1),B1,A3)', 'C(B(C(A(C1,B3),B2),A2),A3)', 'M(C(B(C(A(C1,B3),B2),A2),A3),A1,B1)', 'B(C(A(C1,B3),B2),A3)', 'C(B(C(A(C1,B3),B2),A3),A1)', 'M(C(B(C(A(C1,B3),B2),A3),A1),B1,A2)', 'C(B(C(A(C1,B3),B2),A3),A2)', 'M(C(B(C(A(C1,B3),B2),A3),A2),A1,B1)', '+']
[('A1', 'B(C1,A1)'), ('A1', 'B(C(A(C1,B1),B2),A1)'), ('A1', 'C(B(C(A(C1,B1),B2),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B1),B2),A2),A3),A1,B3)'), ('A1', 'C(B(C(A(C1,B1),B2),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B1),B2),A3),A2),A1,B3)'), ('A1', 'B(C(A(C1,B1),B3),A1)'), ('A1', 'C(B(C(A(C1,B1),B3),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B1),B3),A2),A3),A1,B2)'), ('A1', 'C(B(C(A(C1,B1),B3),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B1),B3),A3),A2),A1,B2)'), ('A1', 'C(B(C1,A2),A1)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B1),B2),A1,B3)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B1),B3),A1,B2)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B2),B1),A1,B3)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B2),B3),A1,B1)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B3),B1),A1,B2)'), ('A1', 'M(C(A(C(B(C1,A2),A3),B3),B2),A1,B1)'), ('A1', 'B(C(A(C1,B2),B1),A1)'), ('A1', 'C(B(C(A(C1,B2),B1),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B2),B1),A2),A3),A1,B3)'), ('A1', 'C(B(C(A(C1,B2),B1),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B2),B1),A3),A2),A1,B3)'), ('A1', 'B(C(A(C1,B2),B3),A1)'), ('A1', 'C(B(C(A(C1,B2),B3),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B2),B3),A2),A3),A1,B1)'), ('A1', 'C(B(C(A(C1,B2),B3),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B2),B3),A3),A2),A1,B1)'), ('A1', 'C(B(C1,A3),A1)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B1),B2),A1,B3)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B1),B3),A1,B2)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B2),B1),A1,B3)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B2),B3),A1,B1)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B3),B1),A1,B2)'), ('A1', 'M(C(A(C(B(C1,A3),A2),B3),B2),A1,B1)'), ('A1', 'B(C(A(C1,B3),B1),A1)'), ('A1', 'C(B(C(A(C1,B3),B1),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B3),B1),A2),A3),A1,B2)'), ('A1', 'C(B(C(A(C1,B3),B1),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B3),B1),A3),A2),A1,B2)'), ('A1', 'B(C(A(C1,B3),B2),A1)'), ('A1', 'C(B(C(A(C1,B3),B2),A2),A1)'), ('A1', 'M(C(B(C(A(C1,B3),B2),A2),A3),A1,B1)'), ('A1', 'C(B(C(A(C1,B3),B2),A3),A1)'), ('A1', 'M(C(B(C(A(C1,B3),B2),A3),A2),A1,B1)'), ('B1', 'A(C(B(C1,A1),A2),B1)'), ('B1', 'C(A(C(B(C1,A1),A2),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A1),A2),B2),B3),B1,A3)'), ('B1', 'C(A(C(B(C1,A1),A2),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A1),A2),B3),B2),B1,A3)'), ('B1', 'A(C(B(C1,A1),A3),B1)'), ('B1', 'C(A(C(B(C1,A1),A3),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A1),A3),B2),B3),B1,A2)'), ('B1', 'C(A(C(B(C1,A1),A3),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A1),A3),B3),B2),B1,A2)'), ('B1', 'A(C1,B1)'), ('B1', 'A(C(B(C1,A2),A1),B1)'), ('B1', 'C(A(C(B(C1,A2),A1),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A2),A1),B2),B3),B1,A3)'), ('B1', 'C(A(C(B(C1,A2),A1),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A2),A1),B3),B2),B1,A3)'), ('B1', 'A(C(B(C1,A2),A3),B1)'), ('B1', 'C(A(C(B(C1,A2),A3),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A2),A3),B2),B3),A1,B1)'), ('B1', 'C(A(C(B(C1,A2),A3),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A2),A3),B3),B2),A1,B1)'), ('B1', 'C(A(C1,B2),B1)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A1),A2),B1,A3)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A1),A3),B1,A2)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A2),A1),B1,A3)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A2),A3),A1,B1)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A3),A1),B1,A2)'), ('B1', 'M(C(B(C(A(C1,B2),B3),A3),A2),A1,B1)'), ('B1', 'A(C(B(C1,A3),A1),B1)'), ('B1', 'C(A(C(B(C1,A3),A1),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A3),A1),B2),B3),B1,A2)'), ('B1', 'C(A(C(B(C1,A3),A1),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A3),A1),B3),B2),B1,A2)'), ('B1', 'A(C(B(C1,A3),A2),B1)'), ('B1', 'C(A(C(B(C1,A3),A2),B2),B1)'), ('B1', 'M(C(A(C(B(C1,A3),A2),B2),B3),A1,B1)'), ('B1', 'C(A(C(B(C1,A3),A2),B3),B1)'), ('B1', 'M(C(A(C(B(C1,A3),A2),B3),B2),A1,B1)'), ('B1', 'C(A(C1,B3),B1)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A1),A2),B1,A3)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A1),A3),B1,A2)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A2),A1),B1,A3)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A2),A3),A1,B1)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A3),A1),B1,A2)'), ('B1', 'M(C(B(C(A(C1,B3),B2),A3),A2),A1,B1)'), ('A2', 'C(B(C1,A1),A2)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B1),B2),A2,B3)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B1),B3),A2,B2)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B2),B1),A2,B3)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B2),B3),B1,A2)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B3),B1),A2,B2)'), ('A2', 'M(C(A(C(B(C1,A1),A3),B3),B2),B1,A2)'), ('A2', 'C(B(C(A(C1,B1),B2),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B1),B2),A1),A3),A2,B3)'), ('A2', 'B(C(A(C1,B1),B2),A2)'), ('A2', 'M(C(B(C(A(C1,B1),B2),A3),A1),A2,B3)'), ('A2', 'C(B(C(A(C1,B1),B2),A3),A2)'), ('A2', 'C(B(C(A(C1,B1),B3),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B1),B3),A1),A3),A2,B2)'), ('A2', 'B(C(A(C1,B1),B3),A2)'), ('A2', 'M(C(B(C(A(C1,B1),B3),A3),A1),A2,B2)'), ('A2', 'C(B(C(A(C1,B1),B3),A3),A2)'), ('A2', 'B(C1,A2)'), ('A2', 'C(B(C(A(C1,B2),B1),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B2),B1),A1),A3),A2,B3)'), ('A2', 'B(C(A(C1,B2),B1),A2)'), ('A2', 'M(C(B(C(A(C1,B2),B1),A3),A1),A2,B3)'), ('A2', 'C(B(C(A(C1,B2),B1),A3),A2)'), ('A2', 'C(B(C(A(C1,B2),B3),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B2),B3),A1),A3),B1,A2)'), ('A2', 'B(C(A(C1,B2),B3),A2)'), ('A2', 'M(C(B(C(A(C1,B2),B3),A3),A1),B1,A2)'), ('A2', 'C(B(C(A(C1,B2),B3),A3),A2)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B1),B2),A2,B3)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B1),B3),A2,B2)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B2),B1),A2,B3)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B2),B3),B1,A2)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B3),B1),A2,B2)'), ('A2', 'M(C(A(C(B(C1,A3),A1),B3),B2),B1,A2)'), ('A2', 'C(B(C1,A3),A2)'), ('A2', 'C(B(C(A(C1,B3),B1),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B3),B1),A1),A3),A2,B2)'), ('A2', 'B(C(A(C1,B3),B1),A2)'), ('A2', 'M(C(B(C(A(C1,B3),B1),A3),A1),A2,B2)'), ('A2', 'C(B(C(A(C1,B3),B1),A3),A2)'), ('A2', 'C(B(C(A(C1,B3),B2),A1),A2)'), ('A2', 'M(C(B(C(A(C1,B3),B2),A1),A3),B1,A2)'), ('A2', 'B(C(A(C1,B3),B2),A2)'), ('A2', 'M(C(B(C(A(C1,B3),B2),A3),A1),B1,A2)'), ('A2', 'C(B(C(A(C1,B3),B2),A3),A2)'), ('B2', 'C(A(C(B(C1,A1),A2),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A1),A2),B1),B3),B2,A3)'), ('B2', 'A(C(B(C1,A1),A2),B2)'), ('B2', 'M(C(A(C(B(C1,A1),A2),B3),B1),B2,A3)'), ('B2', 'C(A(C(B(C1,A1),A2),B3),B2)'), ('B2', 'C(A(C(B(C1,A1),A3),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A1),A3),B1),B3),A2,B2)'), ('B2', 'A(C(B(C1,A1),A3),B2)'), ('B2', 'M(C(A(C(B(C1,A1),A3),B3),B1),A2,B2)'), ('B2', 'C(A(C(B(C1,A1),A3),B3),B2)'), ('B2', 'C(A(C1,B1),B2)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A1),A2),B2,A3)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A1),A3),A2,B2)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A2),A1),B2,A3)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A2),A3),A1,B2)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A3),A1),A2,B2)'), ('B2', 'M(C(B(C(A(C1,B1),B3),A3),A2),A1,B2)'), ('B2', 'C(A(C(B(C1,A2),A1),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A2),A1),B1),B3),B2,A3)'), ('B2', 'A(C(B(C1,A2),A1),B2)'), ('B2', 'M(C(A(C(B(C1,A2),A1),B3),B1),B2,A3)'), ('B2', 'C(A(C(B(C1,A2),A1),B3),B2)'), ('B2', 'C(A(C(B(C1,A2),A3),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A2),A3),B1),B3),A1,B2)'), ('B2', 'A(C(B(C1,A2),A3),B2)'), ('B2', 'M(C(A(C(B(C1,A2),A3),B3),B1),A1,B2)'), ('B2', 'C(A(C(B(C1,A2),A3),B3),B2)'), ('B2', 'A(C1,B2)'), ('B2', 'C(A(C(B(C1,A3),A1),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A3),A1),B1),B3),A2,B2)'), ('B2', 'A(C(B(C1,A3),A1),B2)'), ('B2', 'M(C(A(C(B(C1,A3),A1),B3),B1),A2,B2)'), ('B2', 'C(A(C(B(C1,A3),A1),B3),B2)'), ('B2', 'C(A(C(B(C1,A3),A2),B1),B2)'), ('B2', 'M(C(A(C(B(C1,A3),A2),B1),B3),A1,B2)'), ('B2', 'A(C(B(C1,A3),A2),B2)'), ('B2', 'M(C(A(C(B(C1,A3),A2),B3),B1),A1,B2)'), ('B2', 'C(A(C(B(C1,A3),A2),B3),B2)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A1),A2),B2,A3)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A1),A3),A2,B2)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A2),A1),B2,A3)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A2),A3),A1,B2)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A3),A1),A2,B2)'), ('B2', 'M(C(B(C(A(C1,B3),B1),A3),A2),A1,B2)'), ('B2', 'C(A(C1,B3),B2)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B1),B2),A3,B3)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B1),B3),B2,A3)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B2),B1),A3,B3)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B2),B3),B1,A3)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B3),B1),B2,A3)'), ('A3', 'M(C(A(C(B(C1,A1),A2),B3),B2),B1,A3)'), ('A3', 'C(B(C1,A1),A3)'), ('A3', 'M(C(B(C(A(C1,B1),B2),A1),A2),A3,B3)'), ('A3', 'C(B(C(A(C1,B1),B2),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B1),B2),A2),A1),A3,B3)'), ('A3', 'C(B(C(A(C1,B1),B2),A2),A3)'), ('A3', 'B(C(A(C1,B1),B2),A3)'), ('A3', 'M(C(B(C(A(C1,B1),B3),A1),A2),B2,A3)'), ('A3', 'C(B(C(A(C1,B1),B3),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B1),B3),A2),A1),B2,A3)'), ('A3', 'C(B(C(A(C1,B1),B3),A2),A3)'), ('A3', 'B(C(A(C1,B1),B3),A3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B1),B2),A3,B3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B1),B3),B2,A3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B2),B1),A3,B3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B2),B3),B1,A3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B3),B1),B2,A3)'), ('A3', 'M(C(A(C(B(C1,A2),A1),B3),B2),B1,A3)'), ('A3', 'C(B(C1,A2),A3)'), ('A3', 'M(C(B(C(A(C1,B2),B1),A1),A2),A3,B3)'), ('A3', 'C(B(C(A(C1,B2),B1),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B2),B1),A2),A1),A3,B3)'), ('A3', 'C(B(C(A(C1,B2),B1),A2),A3)'), ('A3', 'B(C(A(C1,B2),B1),A3)'), ('A3', 'M(C(B(C(A(C1,B2),B3),A1),A2),B1,A3)'), ('A3', 'C(B(C(A(C1,B2),B3),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B2),B3),A2),A1),B1,A3)'), ('A3', 'C(B(C(A(C1,B2),B3),A2),A3)'), ('A3', 'B(C(A(C1,B2),B3),A3)'), ('A3', 'B(C1,A3)'), ('A3', 'M(C(B(C(A(C1,B3),B1),A1),A2),B2,A3)'), ('A3', 'C(B(C(A(C1,B3),B1),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B3),B1),A2),A1),B2,A3)'), ('A3', 'C(B(C(A(C1,B3),B1),A2),A3)'), ('A3', 'B(C(A(C1,B3),B1),A3)'), ('A3', 'M(C(B(C(A(C1,B3),B2),A1),A2),B1,A3)'), ('A3', 'C(B(C(A(C1,B3),B2),A1),A3)'), ('A3', 'M(C(B(C(A(C1,B3),B2),A2),A1),B1,A3)'), ('A3', 'C(B(C(A(C1,B3),B2),A2),A3)'), ('A3', 'B(C(A(C1,B3),B2),A3)'), ('B3', 'M(C(A(C(B(C1,A1),A2),B1),B2),A3,B3)'), ('B3', 'C(A(C(B(C1,A1),A2),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A1),A2),B2),B1),A3,B3)'), ('B3', 'C(A(C(B(C1,A1),A2),B2),B3)'), ('B3', 'A(C(B(C1,A1),A2),B3)'), ('B3', 'M(C(A(C(B(C1,A1),A3),B1),B2),A2,B3)'), ('B3', 'C(A(C(B(C1,A1),A3),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A1),A3),B2),B1),A2,B3)'), ('B3', 'C(A(C(B(C1,A1),A3),B2),B3)'), ('B3', 'A(C(B(C1,A1),A3),B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A1),A2),A3,B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A1),A3),A2,B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A2),A1),A3,B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A2),A3),A1,B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A3),A1),A2,B3)'), ('B3', 'M(C(B(C(A(C1,B1),B2),A3),A2),A1,B3)'), ('B3', 'C(A(C1,B1),B3)'), ('B3', 'M(C(A(C(B(C1,A2),A1),B1),B2),A3,B3)'), ('B3', 'C(A(C(B(C1,A2),A1),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A2),A1),B2),B1),A3,B3)'), ('B3', 'C(A(C(B(C1,A2),A1),B2),B3)'), ('B3', 'A(C(B(C1,A2),A1),B3)'), ('B3', 'M(C(A(C(B(C1,A2),A3),B1),B2),A1,B3)'), ('B3', 'C(A(C(B(C1,A2),A3),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A2),A3),B2),B1),A1,B3)'), ('B3', 'C(A(C(B(C1,A2),A3),B2),B3)'), ('B3', 'A(C(B(C1,A2),A3),B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A1),A2),A3,B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A1),A3),A2,B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A2),A1),A3,B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A2),A3),A1,B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A3),A1),A2,B3)'), ('B3', 'M(C(B(C(A(C1,B2),B1),A3),A2),A1,B3)'), ('B3', 'C(A(C1,B2),B3)'), ('B3', 'M(C(A(C(B(C1,A3),A1),B1),B2),A2,B3)'), ('B3', 'C(A(C(B(C1,A3),A1),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A3),A1),B2),B1),A2,B3)'), ('B3', 'C(A(C(B(C1,A3),A1),B2),B3)'), ('B3', 'A(C(B(C1,A3),A1),B3)'), ('B3', 'M(C(A(C(B(C1,A3),A2),B1),B2),A1,B3)'), ('B3', 'C(A(C(B(C1,A3),A2),B1),B3)'), ('B3', 'M(C(A(C(B(C1,A3),A2),B2),B1),A1,B3)'), ('B3', 'C(A(C(B(C1,A3),A2),B2),B3)'), ('B3', 'A(C(B(C1,A3),A2),B3)'), ('B3', 'A(C1,B3)'), ('C1', 'B(C1,A1)'), ('C1', 'A(C1,B1)'), ('C1', 'B(C1,A2)'), ('C1', 'A(C1,B2)'), ('C1', 'B(C1,A3)'), ('C1', 'A(C1,B3)'), ('B(C1,A1)', 'C(B(C1,A1),A2)'), ('B(C1,A1)', 'C(B(C1,A1),A3)'), ('C(B(C1,A1),A2)', 'A(C(B(C1,A1),A2),B1)'), ('C(B(C1,A1),A2)', 'A(C(B(C1,A1),A2),B2)'), ('C(B(C1,A1),A2)', 'A(C(B(C1,A1),A2),B3)'), ('A(C(B(C1,A1),A2),B1)', 'C(A(C(B(C1,A1),A2),B1),B2)'), ('A(C(B(C1,A1),A2),B1)', 'C(A(C(B(C1,A1),A2),B1),B3)'), ('C(A(C(B(C1,A1),A2),B1),B2)', 'M(C(A(C(B(C1,A1),A2),B1),B2),A3,B3)'), ('M(C(A(C(B(C1,A1),A2),B1),B2),A3,B3)', '+'), ('C(A(C(B(C1,A1),A2),B1),B3)', 'M(C(A(C(B(C1,A1),A2),B1),B3),B2,A3)'), ('M(C(A(C(B(C1,A1),A2),B1),B3),B2,A3)', '+'), ('A(C(B(C1,A1),A2),B2)', 'C(A(C(B(C1,A1),A2),B2),B1)'), ('A(C(B(C1,A1),A2),B2)', 'C(A(C(B(C1,A1),A2),B2),B3)'), ('C(A(C(B(C1,A1),A2),B2),B1)', 'M(C(A(C(B(C1,A1),A2),B2),B1),A3,B3)'), ('M(C(A(C(B(C1,A1),A2),B2),B1),A3,B3)', '+'), ('C(A(C(B(C1,A1),A2),B2),B3)', 'M(C(A(C(B(C1,A1),A2),B2),B3),B1,A3)'), ('M(C(A(C(B(C1,A1),A2),B2),B3),B1,A3)', '+'), ('A(C(B(C1,A1),A2),B3)', 'C(A(C(B(C1,A1),A2),B3),B1)'), ('A(C(B(C1,A1),A2),B3)', 'C(A(C(B(C1,A1),A2),B3),B2)'), ('C(A(C(B(C1,A1),A2),B3),B1)', 'M(C(A(C(B(C1,A1),A2),B3),B1),B2,A3)'), ('M(C(A(C(B(C1,A1),A2),B3),B1),B2,A3)', '+'), ('C(A(C(B(C1,A1),A2),B3),B2)', 'M(C(A(C(B(C1,A1),A2),B3),B2),B1,A3)'), ('M(C(A(C(B(C1,A1),A2),B3),B2),B1,A3)', '+'), ('C(B(C1,A1),A3)', 'A(C(B(C1,A1),A3),B1)'), ('C(B(C1,A1),A3)', 'A(C(B(C1,A1),A3),B2)'), ('C(B(C1,A1),A3)', 'A(C(B(C1,A1),A3),B3)'), ('A(C(B(C1,A1),A3),B1)', 'C(A(C(B(C1,A1),A3),B1),B2)'), ('A(C(B(C1,A1),A3),B1)', 'C(A(C(B(C1,A1),A3),B1),B3)'), ('C(A(C(B(C1,A1),A3),B1),B2)', 'M(C(A(C(B(C1,A1),A3),B1),B2),A2,B3)'), ('M(C(A(C(B(C1,A1),A3),B1),B2),A2,B3)', '+'), ('C(A(C(B(C1,A1),A3),B1),B3)', 'M(C(A(C(B(C1,A1),A3),B1),B3),A2,B2)'), ('M(C(A(C(B(C1,A1),A3),B1),B3),A2,B2)', '+'), ('A(C(B(C1,A1),A3),B2)', 'C(A(C(B(C1,A1),A3),B2),B1)'), ('A(C(B(C1,A1),A3),B2)', 'C(A(C(B(C1,A1),A3),B2),B3)'), ('C(A(C(B(C1,A1),A3),B2),B1)', 'M(C(A(C(B(C1,A1),A3),B2),B1),A2,B3)'), ('M(C(A(C(B(C1,A1),A3),B2),B1),A2,B3)', '+'), ('C(A(C(B(C1,A1),A3),B2),B3)', 'M(C(A(C(B(C1,A1),A3),B2),B3),B1,A2)'), ('M(C(A(C(B(C1,A1),A3),B2),B3),B1,A2)', '+'), ('A(C(B(C1,A1),A3),B3)', 'C(A(C(B(C1,A1),A3),B3),B1)'), ('A(C(B(C1,A1),A3),B3)', 'C(A(C(B(C1,A1),A3),B3),B2)'), ('C(A(C(B(C1,A1),A3),B3),B1)', 'M(C(A(C(B(C1,A1),A3),B3),B1),A2,B2)'), ('M(C(A(C(B(C1,A1),A3),B3),B1),A2,B2)', '+'), ('C(A(C(B(C1,A1),A3),B3),B2)', 'M(C(A(C(B(C1,A1),A3),B3),B2),B1,A2)'), ('M(C(A(C(B(C1,A1),A3),B3),B2),B1,A2)', '+'), ('A(C1,B1)', 'C(A(C1,B1),B2)'), ('A(C1,B1)', 'C(A(C1,B1),B3)'), ('C(A(C1,B1),B2)', 'B(C(A(C1,B1),B2),A1)'), ('C(A(C1,B1),B2)', 'B(C(A(C1,B1),B2),A2)'), ('C(A(C1,B1),B2)', 'B(C(A(C1,B1),B2),A3)'), ('B(C(A(C1,B1),B2),A1)', 'C(B(C(A(C1,B1),B2),A1),A2)'), ('B(C(A(C1,B1),B2),A1)', 'C(B(C(A(C1,B1),B2),A1),A3)'), ('C(B(C(A(C1,B1),B2),A1),A2)', 'M(C(B(C(A(C1,B1),B2),A1),A2),A3,B3)'), ('M(C(B(C(A(C1,B1),B2),A1),A2),A3,B3)', '+'), ('C(B(C(A(C1,B1),B2),A1),A3)', 'M(C(B(C(A(C1,B1),B2),A1),A3),A2,B3)'), ('M(C(B(C(A(C1,B1),B2),A1),A3),A2,B3)', '+'), ('B(C(A(C1,B1),B2),A2)', 'C(B(C(A(C1,B1),B2),A2),A1)'), ('B(C(A(C1,B1),B2),A2)', 'C(B(C(A(C1,B1),B2),A2),A3)'), ('C(B(C(A(C1,B1),B2),A2),A1)', 'M(C(B(C(A(C1,B1),B2),A2),A1),A3,B3)'), ('M(C(B(C(A(C1,B1),B2),A2),A1),A3,B3)', '+'), ('C(B(C(A(C1,B1),B2),A2),A3)', 'M(C(B(C(A(C1,B1),B2),A2),A3),A1,B3)'), ('M(C(B(C(A(C1,B1),B2),A2),A3),A1,B3)', '+'), ('B(C(A(C1,B1),B2),A3)', 'C(B(C(A(C1,B1),B2),A3),A1)'), ('B(C(A(C1,B1),B2),A3)', 'C(B(C(A(C1,B1),B2),A3),A2)'), ('C(B(C(A(C1,B1),B2),A3),A1)', 'M(C(B(C(A(C1,B1),B2),A3),A1),A2,B3)'), ('M(C(B(C(A(C1,B1),B2),A3),A1),A2,B3)', '+'), ('C(B(C(A(C1,B1),B2),A3),A2)', 'M(C(B(C(A(C1,B1),B2),A3),A2),A1,B3)'), ('M(C(B(C(A(C1,B1),B2),A3),A2),A1,B3)', '+'), ('C(A(C1,B1),B3)', 'B(C(A(C1,B1),B3),A1)'), ('C(A(C1,B1),B3)', 'B(C(A(C1,B1),B3),A2)'), ('C(A(C1,B1),B3)', 'B(C(A(C1,B1),B3),A3)'), ('B(C(A(C1,B1),B3),A1)', 'C(B(C(A(C1,B1),B3),A1),A2)'), ('B(C(A(C1,B1),B3),A1)', 'C(B(C(A(C1,B1),B3),A1),A3)'), ('C(B(C(A(C1,B1),B3),A1),A2)', 'M(C(B(C(A(C1,B1),B3),A1),A2),B2,A3)'), ('M(C(B(C(A(C1,B1),B3),A1),A2),B2,A3)', '+'), ('C(B(C(A(C1,B1),B3),A1),A3)', 'M(C(B(C(A(C1,B1),B3),A1),A3),A2,B2)'), ('M(C(B(C(A(C1,B1),B3),A1),A3),A2,B2)', '+'), ('B(C(A(C1,B1),B3),A2)', 'C(B(C(A(C1,B1),B3),A2),A1)'), ('B(C(A(C1,B1),B3),A2)', 'C(B(C(A(C1,B1),B3),A2),A3)'), ('C(B(C(A(C1,B1),B3),A2),A1)', 'M(C(B(C(A(C1,B1),B3),A2),A1),B2,A3)'), ('M(C(B(C(A(C1,B1),B3),A2),A1),B2,A3)', '+'), ('C(B(C(A(C1,B1),B3),A2),A3)', 'M(C(B(C(A(C1,B1),B3),A2),A3),A1,B2)'), ('M(C(B(C(A(C1,B1),B3),A2),A3),A1,B2)', '+'), ('B(C(A(C1,B1),B3),A3)', 'C(B(C(A(C1,B1),B3),A3),A1)'), ('B(C(A(C1,B1),B3),A3)', 'C(B(C(A(C1,B1),B3),A3),A2)'), ('C(B(C(A(C1,B1),B3),A3),A1)', 'M(C(B(C(A(C1,B1),B3),A3),A1),A2,B2)'), ('M(C(B(C(A(C1,B1),B3),A3),A1),A2,B2)', '+'), ('C(B(C(A(C1,B1),B3),A3),A2)', 'M(C(B(C(A(C1,B1),B3),A3),A2),A1,B2)'), ('M(C(B(C(A(C1,B1),B3),A3),A2),A1,B2)', '+'), ('B(C1,A2)', 'C(B(C1,A2),A1)'), ('B(C1,A2)', 'C(B(C1,A2),A3)'), ('C(B(C1,A2),A1)', 'A(C(B(C1,A2),A1),B1)'), ('C(B(C1,A2),A1)', 'A(C(B(C1,A2),A1),B2)'), ('C(B(C1,A2),A1)', 'A(C(B(C1,A2),A1),B3)'), ('A(C(B(C1,A2),A1),B1)', 'C(A(C(B(C1,A2),A1),B1),B2)'), ('A(C(B(C1,A2),A1),B1)', 'C(A(C(B(C1,A2),A1),B1),B3)'), ('C(A(C(B(C1,A2),A1),B1),B2)', 'M(C(A(C(B(C1,A2),A1),B1),B2),A3,B3)'), ('M(C(A(C(B(C1,A2),A1),B1),B2),A3,B3)', '+'), ('C(A(C(B(C1,A2),A1),B1),B3)', 'M(C(A(C(B(C1,A2),A1),B1),B3),B2,A3)'), ('M(C(A(C(B(C1,A2),A1),B1),B3),B2,A3)', '+'), ('A(C(B(C1,A2),A1),B2)', 'C(A(C(B(C1,A2),A1),B2),B1)'), ('A(C(B(C1,A2),A1),B2)', 'C(A(C(B(C1,A2),A1),B2),B3)'), ('C(A(C(B(C1,A2),A1),B2),B1)', 'M(C(A(C(B(C1,A2),A1),B2),B1),A3,B3)'), ('M(C(A(C(B(C1,A2),A1),B2),B1),A3,B3)', '+'), ('C(A(C(B(C1,A2),A1),B2),B3)', 'M(C(A(C(B(C1,A2),A1),B2),B3),B1,A3)'), ('M(C(A(C(B(C1,A2),A1),B2),B3),B1,A3)', '+'), ('A(C(B(C1,A2),A1),B3)', 'C(A(C(B(C1,A2),A1),B3),B1)'), ('A(C(B(C1,A2),A1),B3)', 'C(A(C(B(C1,A2),A1),B3),B2)'), ('C(A(C(B(C1,A2),A1),B3),B1)', 'M(C(A(C(B(C1,A2),A1),B3),B1),B2,A3)'), ('M(C(A(C(B(C1,A2),A1),B3),B1),B2,A3)', '+'), ('C(A(C(B(C1,A2),A1),B3),B2)', 'M(C(A(C(B(C1,A2),A1),B3),B2),B1,A3)'), ('M(C(A(C(B(C1,A2),A1),B3),B2),B1,A3)', '+'), ('C(B(C1,A2),A3)', 'A(C(B(C1,A2),A3),B1)'), ('C(B(C1,A2),A3)', 'A(C(B(C1,A2),A3),B2)'), ('C(B(C1,A2),A3)', 'A(C(B(C1,A2),A3),B3)'), ('A(C(B(C1,A2),A3),B1)', 'C(A(C(B(C1,A2),A3),B1),B2)'), ('A(C(B(C1,A2),A3),B1)', 'C(A(C(B(C1,A2),A3),B1),B3)'), ('C(A(C(B(C1,A2),A3),B1),B2)', 'M(C(A(C(B(C1,A2),A3),B1),B2),A1,B3)'), ('M(C(A(C(B(C1,A2),A3),B1),B2),A1,B3)', '+'), ('C(A(C(B(C1,A2),A3),B1),B3)', 'M(C(A(C(B(C1,A2),A3),B1),B3),A1,B2)'), ('M(C(A(C(B(C1,A2),A3),B1),B3),A1,B2)', '+'), ('A(C(B(C1,A2),A3),B2)', 'C(A(C(B(C1,A2),A3),B2),B1)'), ('A(C(B(C1,A2),A3),B2)', 'C(A(C(B(C1,A2),A3),B2),B3)'), ('C(A(C(B(C1,A2),A3),B2),B1)', 'M(C(A(C(B(C1,A2),A3),B2),B1),A1,B3)'), ('M(C(A(C(B(C1,A2),A3),B2),B1),A1,B3)', '+'), ('C(A(C(B(C1,A2),A3),B2),B3)', 'M(C(A(C(B(C1,A2),A3),B2),B3),A1,B1)'), ('M(C(A(C(B(C1,A2),A3),B2),B3),A1,B1)', '+'), ('A(C(B(C1,A2),A3),B3)', 'C(A(C(B(C1,A2),A3),B3),B1)'), ('A(C(B(C1,A2),A3),B3)', 'C(A(C(B(C1,A2),A3),B3),B2)'), ('C(A(C(B(C1,A2),A3),B3),B1)', 'M(C(A(C(B(C1,A2),A3),B3),B1),A1,B2)'), ('M(C(A(C(B(C1,A2),A3),B3),B1),A1,B2)', '+'), ('C(A(C(B(C1,A2),A3),B3),B2)', 'M(C(A(C(B(C1,A2),A3),B3),B2),A1,B1)'), ('M(C(A(C(B(C1,A2),A3),B3),B2),A1,B1)', '+'), ('A(C1,B2)', 'C(A(C1,B2),B1)'), ('A(C1,B2)', 'C(A(C1,B2),B3)'), ('C(A(C1,B2),B1)', 'B(C(A(C1,B2),B1),A1)'), ('C(A(C1,B2),B1)', 'B(C(A(C1,B2),B1),A2)'), ('C(A(C1,B2),B1)', 'B(C(A(C1,B2),B1),A3)'), ('B(C(A(C1,B2),B1),A1)', 'C(B(C(A(C1,B2),B1),A1),A2)'), ('B(C(A(C1,B2),B1),A1)', 'C(B(C(A(C1,B2),B1),A1),A3)'), ('C(B(C(A(C1,B2),B1),A1),A2)', 'M(C(B(C(A(C1,B2),B1),A1),A2),A3,B3)'), ('M(C(B(C(A(C1,B2),B1),A1),A2),A3,B3)', '+'), ('C(B(C(A(C1,B2),B1),A1),A3)', 'M(C(B(C(A(C1,B2),B1),A1),A3),A2,B3)'), ('M(C(B(C(A(C1,B2),B1),A1),A3),A2,B3)', '+'), ('B(C(A(C1,B2),B1),A2)', 'C(B(C(A(C1,B2),B1),A2),A1)'), ('B(C(A(C1,B2),B1),A2)', 'C(B(C(A(C1,B2),B1),A2),A3)'), ('C(B(C(A(C1,B2),B1),A2),A1)', 'M(C(B(C(A(C1,B2),B1),A2),A1),A3,B3)'), ('M(C(B(C(A(C1,B2),B1),A2),A1),A3,B3)', '+'), ('C(B(C(A(C1,B2),B1),A2),A3)', 'M(C(B(C(A(C1,B2),B1),A2),A3),A1,B3)'), ('M(C(B(C(A(C1,B2),B1),A2),A3),A1,B3)', '+'), ('B(C(A(C1,B2),B1),A3)', 'C(B(C(A(C1,B2),B1),A3),A1)'), ('B(C(A(C1,B2),B1),A3)', 'C(B(C(A(C1,B2),B1),A3),A2)'), ('C(B(C(A(C1,B2),B1),A3),A1)', 'M(C(B(C(A(C1,B2),B1),A3),A1),A2,B3)'), ('M(C(B(C(A(C1,B2),B1),A3),A1),A2,B3)', '+'), ('C(B(C(A(C1,B2),B1),A3),A2)', 'M(C(B(C(A(C1,B2),B1),A3),A2),A1,B3)'), ('M(C(B(C(A(C1,B2),B1),A3),A2),A1,B3)', '+'), ('C(A(C1,B2),B3)', 'B(C(A(C1,B2),B3),A1)'), ('C(A(C1,B2),B3)', 'B(C(A(C1,B2),B3),A2)'), ('C(A(C1,B2),B3)', 'B(C(A(C1,B2),B3),A3)'), ('B(C(A(C1,B2),B3),A1)', 'C(B(C(A(C1,B2),B3),A1),A2)'), ('B(C(A(C1,B2),B3),A1)', 'C(B(C(A(C1,B2),B3),A1),A3)'), ('C(B(C(A(C1,B2),B3),A1),A2)', 'M(C(B(C(A(C1,B2),B3),A1),A2),B1,A3)'), ('M(C(B(C(A(C1,B2),B3),A1),A2),B1,A3)', '+'), ('C(B(C(A(C1,B2),B3),A1),A3)', 'M(C(B(C(A(C1,B2),B3),A1),A3),B1,A2)'), ('M(C(B(C(A(C1,B2),B3),A1),A3),B1,A2)', '+'), ('B(C(A(C1,B2),B3),A2)', 'C(B(C(A(C1,B2),B3),A2),A1)'), ('B(C(A(C1,B2),B3),A2)', 'C(B(C(A(C1,B2),B3),A2),A3)'), ('C(B(C(A(C1,B2),B3),A2),A1)', 'M(C(B(C(A(C1,B2),B3),A2),A1),B1,A3)'), ('M(C(B(C(A(C1,B2),B3),A2),A1),B1,A3)', '+'), ('C(B(C(A(C1,B2),B3),A2),A3)', 'M(C(B(C(A(C1,B2),B3),A2),A3),A1,B1)'), ('M(C(B(C(A(C1,B2),B3),A2),A3),A1,B1)', '+'), ('B(C(A(C1,B2),B3),A3)', 'C(B(C(A(C1,B2),B3),A3),A1)'), ('B(C(A(C1,B2),B3),A3)', 'C(B(C(A(C1,B2),B3),A3),A2)'), ('C(B(C(A(C1,B2),B3),A3),A1)', 'M(C(B(C(A(C1,B2),B3),A3),A1),B1,A2)'), ('M(C(B(C(A(C1,B2),B3),A3),A1),B1,A2)', '+'), ('C(B(C(A(C1,B2),B3),A3),A2)', 'M(C(B(C(A(C1,B2),B3),A3),A2),A1,B1)'), ('M(C(B(C(A(C1,B2),B3),A3),A2),A1,B1)', '+'), ('B(C1,A3)', 'C(B(C1,A3),A1)'), ('B(C1,A3)', 'C(B(C1,A3),A2)'), ('C(B(C1,A3),A1)', 'A(C(B(C1,A3),A1),B1)'), ('C(B(C1,A3),A1)', 'A(C(B(C1,A3),A1),B2)'), ('C(B(C1,A3),A1)', 'A(C(B(C1,A3),A1),B3)'), ('A(C(B(C1,A3),A1),B1)', 'C(A(C(B(C1,A3),A1),B1),B2)'), ('A(C(B(C1,A3),A1),B1)', 'C(A(C(B(C1,A3),A1),B1),B3)'), ('C(A(C(B(C1,A3),A1),B1),B2)', 'M(C(A(C(B(C1,A3),A1),B1),B2),A2,B3)'), ('M(C(A(C(B(C1,A3),A1),B1),B2),A2,B3)', '+'), ('C(A(C(B(C1,A3),A1),B1),B3)', 'M(C(A(C(B(C1,A3),A1),B1),B3),A2,B2)'), ('M(C(A(C(B(C1,A3),A1),B1),B3),A2,B2)', '+'), ('A(C(B(C1,A3),A1),B2)', 'C(A(C(B(C1,A3),A1),B2),B1)'), ('A(C(B(C1,A3),A1),B2)', 'C(A(C(B(C1,A3),A1),B2),B3)'), ('C(A(C(B(C1,A3),A1),B2),B1)', 'M(C(A(C(B(C1,A3),A1),B2),B1),A2,B3)'), ('M(C(A(C(B(C1,A3),A1),B2),B1),A2,B3)', '+'), ('C(A(C(B(C1,A3),A1),B2),B3)', 'M(C(A(C(B(C1,A3),A1),B2),B3),B1,A2)'), ('M(C(A(C(B(C1,A3),A1),B2),B3),B1,A2)', '+'), ('A(C(B(C1,A3),A1),B3)', 'C(A(C(B(C1,A3),A1),B3),B1)'), ('A(C(B(C1,A3),A1),B3)', 'C(A(C(B(C1,A3),A1),B3),B2)'), ('C(A(C(B(C1,A3),A1),B3),B1)', 'M(C(A(C(B(C1,A3),A1),B3),B1),A2,B2)'), ('M(C(A(C(B(C1,A3),A1),B3),B1),A2,B2)', '+'), ('C(A(C(B(C1,A3),A1),B3),B2)', 'M(C(A(C(B(C1,A3),A1),B3),B2),B1,A2)'), ('M(C(A(C(B(C1,A3),A1),B3),B2),B1,A2)', '+'), ('C(B(C1,A3),A2)', 'A(C(B(C1,A3),A2),B1)'), ('C(B(C1,A3),A2)', 'A(C(B(C1,A3),A2),B2)'), ('C(B(C1,A3),A2)', 'A(C(B(C1,A3),A2),B3)'), ('A(C(B(C1,A3),A2),B1)', 'C(A(C(B(C1,A3),A2),B1),B2)'), ('A(C(B(C1,A3),A2),B1)', 'C(A(C(B(C1,A3),A2),B1),B3)'), ('C(A(C(B(C1,A3),A2),B1),B2)', 'M(C(A(C(B(C1,A3),A2),B1),B2),A1,B3)'), ('M(C(A(C(B(C1,A3),A2),B1),B2),A1,B3)', '+'), ('C(A(C(B(C1,A3),A2),B1),B3)', 'M(C(A(C(B(C1,A3),A2),B1),B3),A1,B2)'), ('M(C(A(C(B(C1,A3),A2),B1),B3),A1,B2)', '+'), ('A(C(B(C1,A3),A2),B2)', 'C(A(C(B(C1,A3),A2),B2),B1)'), ('A(C(B(C1,A3),A2),B2)', 'C(A(C(B(C1,A3),A2),B2),B3)'), ('C(A(C(B(C1,A3),A2),B2),B1)', 'M(C(A(C(B(C1,A3),A2),B2),B1),A1,B3)'), ('M(C(A(C(B(C1,A3),A2),B2),B1),A1,B3)', '+'), ('C(A(C(B(C1,A3),A2),B2),B3)', 'M(C(A(C(B(C1,A3),A2),B2),B3),A1,B1)'), ('M(C(A(C(B(C1,A3),A2),B2),B3),A1,B1)', '+'), ('A(C(B(C1,A3),A2),B3)', 'C(A(C(B(C1,A3),A2),B3),B1)'), ('A(C(B(C1,A3),A2),B3)', 'C(A(C(B(C1,A3),A2),B3),B2)'), ('C(A(C(B(C1,A3),A2),B3),B1)', 'M(C(A(C(B(C1,A3),A2),B3),B1),A1,B2)'), ('M(C(A(C(B(C1,A3),A2),B3),B1),A1,B2)', '+'), ('C(A(C(B(C1,A3),A2),B3),B2)', 'M(C(A(C(B(C1,A3),A2),B3),B2),A1,B1)'), ('M(C(A(C(B(C1,A3),A2),B3),B2),A1,B1)', '+'), ('A(C1,B3)', 'C(A(C1,B3),B1)'), ('A(C1,B3)', 'C(A(C1,B3),B2)'), ('C(A(C1,B3),B1)', 'B(C(A(C1,B3),B1),A1)'), ('C(A(C1,B3),B1)', 'B(C(A(C1,B3),B1),A2)'), ('C(A(C1,B3),B1)', 'B(C(A(C1,B3),B1),A3)'), ('B(C(A(C1,B3),B1),A1)', 'C(B(C(A(C1,B3),B1),A1),A2)'), ('B(C(A(C1,B3),B1),A1)', 'C(B(C(A(C1,B3),B1),A1),A3)'), ('C(B(C(A(C1,B3),B1),A1),A2)', 'M(C(B(C(A(C1,B3),B1),A1),A2),B2,A3)'), ('M(C(B(C(A(C1,B3),B1),A1),A2),B2,A3)', '+'), ('C(B(C(A(C1,B3),B1),A1),A3)', 'M(C(B(C(A(C1,B3),B1),A1),A3),A2,B2)'), ('M(C(B(C(A(C1,B3),B1),A1),A3),A2,B2)', '+'), ('B(C(A(C1,B3),B1),A2)', 'C(B(C(A(C1,B3),B1),A2),A1)'), ('B(C(A(C1,B3),B1),A2)', 'C(B(C(A(C1,B3),B1),A2),A3)'), ('C(B(C(A(C1,B3),B1),A2),A1)', 'M(C(B(C(A(C1,B3),B1),A2),A1),B2,A3)'), ('M(C(B(C(A(C1,B3),B1),A2),A1),B2,A3)', '+'), ('C(B(C(A(C1,B3),B1),A2),A3)', 'M(C(B(C(A(C1,B3),B1),A2),A3),A1,B2)'), ('M(C(B(C(A(C1,B3),B1),A2),A3),A1,B2)', '+'), ('B(C(A(C1,B3),B1),A3)', 'C(B(C(A(C1,B3),B1),A3),A1)'), ('B(C(A(C1,B3),B1),A3)', 'C(B(C(A(C1,B3),B1),A3),A2)'), ('C(B(C(A(C1,B3),B1),A3),A1)', 'M(C(B(C(A(C1,B3),B1),A3),A1),A2,B2)'), ('M(C(B(C(A(C1,B3),B1),A3),A1),A2,B2)', '+'), ('C(B(C(A(C1,B3),B1),A3),A2)', 'M(C(B(C(A(C1,B3),B1),A3),A2),A1,B2)'), ('M(C(B(C(A(C1,B3),B1),A3),A2),A1,B2)', '+'), ('C(A(C1,B3),B2)', 'B(C(A(C1,B3),B2),A1)'), ('C(A(C1,B3),B2)', 'B(C(A(C1,B3),B2),A2)'), ('C(A(C1,B3),B2)', 'B(C(A(C1,B3),B2),A3)'), ('B(C(A(C1,B3),B2),A1)', 'C(B(C(A(C1,B3),B2),A1),A2)'), ('B(C(A(C1,B3),B2),A1)', 'C(B(C(A(C1,B3),B2),A1),A3)'), ('C(B(C(A(C1,B3),B2),A1),A2)', 'M(C(B(C(A(C1,B3),B2),A1),A2),B1,A3)'), ('M(C(B(C(A(C1,B3),B2),A1),A2),B1,A3)', '+'), ('C(B(C(A(C1,B3),B2),A1),A3)', 'M(C(B(C(A(C1,B3),B2),A1),A3),B1,A2)'), ('M(C(B(C(A(C1,B3),B2),A1),A3),B1,A2)', '+'), ('B(C(A(C1,B3),B2),A2)', 'C(B(C(A(C1,B3),B2),A2),A1)'), ('B(C(A(C1,B3),B2),A2)', 'C(B(C(A(C1,B3),B2),A2),A3)'), ('C(B(C(A(C1,B3),B2),A2),A1)', 'M(C(B(C(A(C1,B3),B2),A2),A1),B1,A3)'), ('M(C(B(C(A(C1,B3),B2),A2),A1),B1,A3)', '+'), ('C(B(C(A(C1,B3),B2),A2),A3)', 'M(C(B(C(A(C1,B3),B2),A2),A3),A1,B1)'), ('M(C(B(C(A(C1,B3),B2),A2),A3),A1,B1)', '+'), ('B(C(A(C1,B3),B2),A3)', 'C(B(C(A(C1,B3),B2),A3),A1)'), ('B(C(A(C1,B3),B2),A3)', 'C(B(C(A(C1,B3),B2),A3),A2)'), ('C(B(C(A(C1,B3),B2),A3),A1)', 'M(C(B(C(A(C1,B3),B2),A3),A1),B1,A2)'), ('M(C(B(C(A(C1,B3),B2),A3),A1),B1,A2)', '+'), ('C(B(C(A(C1,B3),B2),A3),A2)', 'M(C(B(C(A(C1,B3),B2),A3),A2),A1,B1)'), ('M(C(B(C(A(C1,B3),B2),A3),A2),A1,B1)', '+')]