YES (ignored inputs)COMMENT from the collection of \cite{AT2012} Rewrite Rules: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)), *(?x,0) -> 0, *(?x,s(?y)) -> +(*(?x,?y),?x), *(0,?y) -> 0, *(s(?x),?y) -> +(*(?x,?y),?y), +(+(?x,?y),?z) -> +(?x,+(?y,?z)), +(?x,?y) -> +(?y,?x), *(*(?x,?y),?z) -> *(?x,*(?y,?z)), *(?x,?y) -> *(?y,?x), *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)), *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) ] Apply Direct Methods... Inner CPs: [ +(?x,?z_8) = +(?x,+(0,?z_8)), +(s(+(?x_1,?y_1)),?z_8) = +(?x_1,+(s(?y_1),?z_8)), +(?y_2,?z_8) = +(0,+(?y_2,?z_8)), +(s(+(?x_3,?y_3)),?z_8) = +(s(?x_3),+(?y_3,?z_8)), +(+(?y_9,?x_9),?z_8) = +(?x_9,+(?y_9,?z_8)), *(0,?z_10) = *(?x_4,*(0,?z_10)), *(+(*(?x_5,?y_5),?x_5),?z_10) = *(?x_5,*(s(?y_5),?z_10)), *(0,?z_10) = *(0,*(?y_6,?z_10)), *(+(*(?x_7,?y_7),?y_7),?z_10) = *(s(?x_7),*(?y_7,?z_10)), *(*(?y_11,?x_11),?z_10) = *(?x_11,*(?y_11,?z_10)), *(+(*(?x_12,?y_12),*(?x_12,?z_12)),?z_10) = *(?x_12,*(+(?y_12,?z_12),?z_10)), *(+(*(?x_13,?z_13),*(?y_13,?z_13)),?z_10) = *(+(?x_13,?y_13),*(?z_13,?z_10)), *(?x_12,?x) = +(*(?x_12,?x),*(?x_12,0)), *(?x_12,s(+(?x_1,?y_1))) = +(*(?x_12,?x_1),*(?x_12,s(?y_1))), *(?x_12,?y_2) = +(*(?x_12,0),*(?x_12,?y_2)), *(?x_12,s(+(?x_3,?y_3))) = +(*(?x_12,s(?x_3)),*(?x_12,?y_3)), *(?x_12,+(?x_8,+(?y_8,?z_8))) = +(*(?x_12,+(?x_8,?y_8)),*(?x_12,?z_8)), *(?x_12,+(?y_9,?x_9)) = +(*(?x_12,?x_9),*(?x_12,?y_9)), *(?x,?z_13) = +(*(?x,?z_13),*(0,?z_13)), *(s(+(?x_1,?y_1)),?z_13) = +(*(?x_1,?z_13),*(s(?y_1),?z_13)), *(?y_2,?z_13) = +(*(0,?z_13),*(?y_2,?z_13)), *(s(+(?x_3,?y_3)),?z_13) = +(*(s(?x_3),?z_13),*(?y_3,?z_13)), *(+(?x_8,+(?y_8,?z_8)),?z_13) = +(*(+(?x_8,?y_8),?z_13),*(?z_8,?z_13)), *(+(?y_9,?x_9),?z_13) = +(*(?x_9,?z_13),*(?y_9,?z_13)), +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)), *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)) ] Outer CPs: [ 0 = 0, s(?x_3) = s(+(?x_3,0)), +(?x_8,?y_8) = +(?x_8,+(?y_8,0)), ?x = +(0,?x), s(+(0,?y_1)) = s(?y_1), s(+(s(?x_3),?y_1)) = s(+(?x_3,s(?y_1))), s(+(+(?x_8,?y_8),?y_1)) = +(?x_8,+(?y_8,s(?y_1))), s(+(?x_1,?y_1)) = +(s(?y_1),?x_1), ?y_2 = +(?y_2,0), s(+(?x_3,?y_3)) = +(?y_3,s(?x_3)), 0 = 0, 0 = +(*(?x_7,0),0), 0 = *(?x_10,*(?y_10,0)), 0 = *(0,?x_4), 0 = +(*(?x_13,0),*(?y_13,0)), +(*(0,?y_5),0) = 0, +(*(s(?x_7),?y_5),s(?x_7)) = +(*(?x_7,s(?y_5)),s(?y_5)), +(*(*(?x_10,?y_10),?y_5),*(?x_10,?y_10)) = *(?x_10,*(?y_10,s(?y_5))), +(*(?x_5,?y_5),?x_5) = *(s(?y_5),?x_5), +(*(+(?x_13,?y_13),?y_5),+(?x_13,?y_13)) = +(*(?x_13,s(?y_5)),*(?y_13,s(?y_5))), 0 = *(?y_6,0), 0 = +(*(0,?y_12),*(0,?z_12)), +(*(?x_7,?y_7),?y_7) = *(?y_7,s(?x_7)), +(*(?x_7,+(?y_12,?z_12)),+(?y_12,?z_12)) = +(*(s(?x_7),?y_12),*(s(?x_7),?z_12)), +(?x_8,+(?y_8,?z_8)) = +(?z_8,+(?x_8,?y_8)), *(?x_10,*(?y_10,?z_10)) = *(?z_10,*(?x_10,?y_10)), *(?x_10,*(?y_10,+(?y_12,?z_12))) = +(*(*(?x_10,?y_10),?y_12),*(*(?x_10,?y_10),?z_12)), *(+(?y_12,?z_12),?x_11) = +(*(?x_11,?y_12),*(?x_11,?z_12)), *(?y_11,+(?x_13,?y_13)) = +(*(?x_13,?y_11),*(?y_13,?y_11)), +(*(+(?x_13,?y_13),?y_12),*(+(?x_13,?y_13),?z_12)) = +(*(?x_13,+(?y_12,?z_12)),*(?y_13,+(?y_12,?z_12))) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Left-Linear, not Right-Linear unknown Development Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ 0 = 0, s(+(?x_3,0)) = s(?x_3), +(?x_8,+(?y_8,0)) = +(?x_8,?y_8), +(0,?x) = ?x, +(?x,+(0,?z_9)) = +(?x,?z_9), +(*(?x_13,?x),*(?x_13,0)) = *(?x_13,?x), +(*(?x,?z_14),*(0,?z_14)) = *(?x,?z_14), s(?y) = s(+(0,?y)), s(+(?x_3,s(?y))) = s(+(s(?x_3),?y)), +(?x_8,+(?y_8,s(?y))) = s(+(+(?x_8,?y_8),?y)), +(s(?y),?x) = s(+(?x,?y)), +(?x,+(s(?y),?z_9)) = +(s(+(?x,?y)),?z_9), +(*(?x_13,?x),*(?x_13,s(?y))) = *(?x_13,s(+(?x,?y))), +(*(?x,?z_14),*(s(?y),?z_14)) = *(s(+(?x,?y)),?z_14), s(+(0,?y_2)) = s(?y_2), +(?y,0) = ?y, +(0,+(?y,?z_9)) = +(?y,?z_9), +(*(?x_13,0),*(?x_13,?y)) = *(?x_13,?y), +(*(0,?z_14),*(?y,?z_14)) = *(?y,?z_14), s(?x) = s(+(?x,0)), s(+(s(?x),?y_2)) = s(+(?x,s(?y_2))), +(?y,s(?x)) = s(+(?x,?y)), +(s(?x),+(?y,?z_9)) = +(s(+(?x,?y)),?z_9), +(*(?x_13,s(?x)),*(?x_13,?y)) = *(?x_13,s(+(?x,?y))), +(*(s(?x),?z_14),*(?y,?z_14)) = *(s(+(?x,?y)),?z_14), +(*(?x_7,0),0) = 0, *(?x_10,*(?y_10,0)) = 0, *(0,?x) = 0, +(*(?x_13,0),*(?y_13,0)) = 0, *(?x,*(0,?z_11)) = *(0,?z_11), 0 = +(*(0,?y),0), +(*(?x_7,s(?y)),s(?y)) = +(*(s(?x_7),?y),s(?x_7)), *(?x_10,*(?y_10,s(?y))) = +(*(*(?x_10,?y_10),?y),*(?x_10,?y_10)), *(s(?y),?x) = +(*(?x,?y),?x), +(*(?x_13,s(?y)),*(?y_13,s(?y))) = +(*(+(?x_13,?y_13),?y),+(?x_13,?y_13)), *(?x,*(s(?y),?z_11)) = *(+(*(?x,?y),?x),?z_11), +(*(0,?y_6),0) = 0, *(?y,0) = 0, +(*(0,?y_12),*(0,?z_12)) = 0, *(0,*(?y,?z_11)) = *(0,?z_11), 0 = +(*(?x,0),0), +(*(s(?x),?y_6),s(?x)) = +(*(?x,s(?y_6)),s(?y_6)), *(?y,s(?x)) = +(*(?x,?y),?y), +(*(s(?x),?y_12),*(s(?x),?z_12)) = +(*(?x,+(?y_12,?z_12)),+(?y_12,?z_12)), *(s(?x),*(?y,?z_11)) = *(+(*(?x,?y),?y),?z_11), +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)), ?x = +(?x,+(0,0)), s(+(?x,?y_3)) = +(?x,+(s(?y_3),0)), ?y = +(0,+(?y,0)), s(+(?x_5,?y)) = +(s(?x_5),+(?y,0)), +(?y,?x) = +(?x,+(?y,0)), s(+(+(?x_3,+(?y_3,?y)),?y_2)) = +(+(?x_3,?y_3),+(?y,s(?y_2))), s(+(?x,?y_2)) = +(?x,+(0,s(?y_2))), s(+(s(+(?x,?y_5)),?y_2)) = +(?x,+(s(?y_5),s(?y_2))), s(+(?y,?y_2)) = +(0,+(?y,s(?y_2))), s(+(s(+(?x_7,?y)),?y_2)) = +(s(?x_7),+(?y,s(?y_2))), s(+(+(?y,?x),?y_2)) = +(?x,+(?y,s(?y_2))), +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)), +(?z,?x) = +(?x,+(0,?z)), +(?z,s(+(?x,?y_3))) = +(?x,+(s(?y_3),?z)), +(?z,?y) = +(0,+(?y,?z)), +(?z,s(+(?x_5,?y))) = +(s(?x_5),+(?y,?z)), +(?z,+(?y,?x)) = +(?x,+(?y,?z)), +(?x,?y) = +(?x,+(?y,0)), s(+(+(?x,?y),?y_2)) = +(?x,+(?y,s(?y_2))), +(?z,+(?x,?y)) = +(?x,+(?y,?z)), +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)), +(?x,?z) = +(?x,+(0,?z)), +(s(+(?x,?y_3)),?z) = +(?x,+(s(?y_3),?z)), +(?y,?z) = +(0,+(?y,?z)), +(s(+(?x_5,?y)),?z) = +(s(?x_5),+(?y,?z)), +(+(?y,?x),?z) = +(?x,+(?y,?z)), +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1), +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1), +(s(+(?x,?y_4)),+(?z,?z_1)) = +(+(?x,+(s(?y_4),?z)),?z_1), +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1), +(s(+(?x_6,?y)),+(?z,?z_1)) = +(+(s(?x_6),+(?y,?z)),?z_1), +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), +(*(?x_13,+(?x_14,+(?y_14,?y))),*(?x_13,?z)) = *(?x_13,+(+(?x_14,?y_14),+(?y,?z))), +(*(?x_13,?x),*(?x_13,?z)) = *(?x_13,+(?x,+(0,?z))), +(*(?x_13,s(+(?x,?y_16))),*(?x_13,?z)) = *(?x_13,+(?x,+(s(?y_16),?z))), +(*(?x_13,?y),*(?x_13,?z)) = *(?x_13,+(0,+(?y,?z))), +(*(?x_13,s(+(?x_18,?y))),*(?x_13,?z)) = *(?x_13,+(s(?x_18),+(?y,?z))), +(*(?x_13,+(?y,?x)),*(?x_13,?z)) = *(?x_13,+(?x,+(?y,?z))), +(*(+(?x_15,+(?y_15,?y)),?z_14),*(?z,?z_14)) = *(+(+(?x_15,?y_15),+(?y,?z)),?z_14), +(*(?x,?z_14),*(?z,?z_14)) = *(+(?x,+(0,?z)),?z_14), +(*(s(+(?x,?y_17)),?z_14),*(?z,?z_14)) = *(+(?x,+(s(?y_17),?z)),?z_14), +(*(?y,?z_14),*(?z,?z_14)) = *(+(0,+(?y,?z)),?z_14), +(*(s(+(?x_19,?y)),?z_14),*(?z,?z_14)) = *(+(s(?x_19),+(?y,?z)),?z_14), +(*(+(?y,?x),?z_14),*(?z,?z_14)) = *(+(?x,+(?y,?z)),?z_14), +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), +(*(?x_13,+(?x,?y)),*(?x_13,?z)) = *(?x_13,+(?x,+(?y,?z))), +(*(+(?x,?y),?z_14),*(?z,?z_14)) = *(+(?x,+(?y,?z)),?z_14), ?x = +(0,?x), s(+(?x,?y_2)) = +(s(?y_2),?x), ?y = +(?y,0), s(+(?x_4,?y)) = +(?y,s(?x_4)), +(?x_9,+(?y_9,?y)) = +(?y,+(?x_9,?y_9)), +(?x,+(?y,?z_10)) = +(+(?y,?x),?z_10), +(*(?x_13,?x),*(?x_13,?y)) = *(?x_13,+(?y,?x)), +(*(?x,?z_14),*(?y,?z_14)) = *(+(?y,?x),?z_14), 0 = *(*(?x_1,?y_1),*(?y,0)), 0 = *(?x,*(0,0)), 0 = *(?x,*(s(?y_7),0)), 0 = *(0,*(?y,0)), 0 = *(s(?x_9),*(?y,0)), 0 = *(?x,*(?y,0)), 0 = *(?x,*(+(?y_13,?z_13),0)), 0 = *(+(?x_14,?y_14),*(?y,0)), +(*(*(?x_7,*(?y_7,?y)),?y_6),*(?x_7,*(?y_7,?y))) = *(*(?x_7,?y_7),*(?y,s(?y_6))), +(*(0,?y_6),0) = *(?x,*(0,s(?y_6))), +(*(+(*(?x,?y_13),?x),?y_6),+(*(?x,?y_13),?x)) = *(?x,*(s(?y_13),s(?y_6))), +(*(0,?y_6),0) = *(0,*(?y,s(?y_6))), +(*(+(*(?x_15,?y),?y),?y_6),+(*(?x_15,?y),?y)) = *(s(?x_15),*(?y,s(?y_6))), +(*(*(?y,?x),?y_6),*(?y,?x)) = *(?x,*(?y,s(?y_6))), +(*(+(*(?x,?y_19),*(?x,?z_19)),?y_6),+(*(?x,?y_19),*(?x,?z_19))) = *(?x,*(+(?y_19,?z_19),s(?y_6))), +(*(+(*(?x_20,?y),*(?y_20,?y)),?y_6),+(*(?x_20,?y),*(?y_20,?y))) = *(+(?x_20,?y_20),*(?y,s(?y_6))), *(?z,*(?x_1,*(?y_1,?y))) = *(*(?x_1,?y_1),*(?y,?z)), *(?z,0) = *(?x,*(0,?z)), *(?z,+(*(?x,?y_7),?x)) = *(?x,*(s(?y_7),?z)), *(?z,0) = *(0,*(?y,?z)), *(?z,+(*(?x_9,?y),?y)) = *(s(?x_9),*(?y,?z)), *(?z,*(?y,?x)) = *(?x,*(?y,?z)), *(?z,+(*(?x,?y_13),*(?x,?z_13))) = *(?x,*(+(?y_13,?z_13),?z)), *(?z,+(*(?x_14,?y),*(?y_14,?y))) = *(+(?x_14,?y_14),*(?y,?z)), +(*(*(?x_13,*(?y_13,?y)),?y_12),*(*(?x_13,*(?y_13,?y)),?z_12)) = *(*(?x_13,?y_13),*(?y,+(?y_12,?z_12))), +(*(0,?y_12),*(0,?z_12)) = *(?x,*(0,+(?y_12,?z_12))), +(*(+(*(?x,?y_19),?x),?y_12),*(+(*(?x,?y_19),?x),?z_12)) = *(?x,*(s(?y_19),+(?y_12,?z_12))), +(*(0,?y_12),*(0,?z_12)) = *(0,*(?y,+(?y_12,?z_12))), +(*(+(*(?x_21,?y),?y),?y_12),*(+(*(?x_21,?y),?y),?z_12)) = *(s(?x_21),*(?y,+(?y_12,?z_12))), +(*(*(?y,?x),?y_12),*(*(?y,?x),?z_12)) = *(?x,*(?y,+(?y_12,?z_12))), +(*(+(*(?x,?y_25),*(?x,?z_25)),?y_12),*(+(*(?x,?y_25),*(?x,?z_25)),?z_12)) = *(?x,*(+(?y_25,?z_25),+(?y_12,?z_12))), +(*(+(*(?x_26,?y),*(?y_26,?y)),?y_12),*(+(*(?x_26,?y),*(?y_26,?y)),?z_12)) = *(+(?x_26,?y_26),*(?y,+(?y_12,?z_12))), +(*(*(?x,?y),?y_6),*(?x,?y)) = *(?x,*(?y,s(?y_6))), *(?z,*(?x,?y)) = *(?x,*(?y,?z)), +(*(*(?x,?y),?y_12),*(*(?x,?y),?z_12)) = *(?x,*(?y,+(?y_12,?z_12))), *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)), *(0,?z) = *(?x,*(0,?z)), *(+(*(?x,?y_7),?x),?z) = *(?x,*(s(?y_7),?z)), *(0,?z) = *(0,*(?y,?z)), *(+(*(?x_9,?y),?y),?z) = *(s(?x_9),*(?y,?z)), *(*(?y,?x),?z) = *(?x,*(?y,?z)), *(+(*(?x,?y_13),*(?x,?z_13)),?z) = *(?x,*(+(?y_13,?z_13),?z)), *(+(*(?x_14,?y),*(?y_14,?y)),?z) = *(+(?x_14,?y_14),*(?y,?z)), *(*(?x_2,*(?y_2,?y)),*(?z,?z_1)) = *(*(*(?x_2,?y_2),*(?y,?z)),?z_1), *(0,*(?z,?z_1)) = *(*(?x,*(0,?z)),?z_1), *(+(*(?x,?y_8),?x),*(?z,?z_1)) = *(*(?x,*(s(?y_8),?z)),?z_1), *(0,*(?z,?z_1)) = *(*(0,*(?y,?z)),?z_1), *(+(*(?x_10,?y),?y),*(?z,?z_1)) = *(*(s(?x_10),*(?y,?z)),?z_1), *(*(?y,?x),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1), *(+(*(?x,?y_14),*(?x,?z_14)),*(?z,?z_1)) = *(*(?x,*(+(?y_14,?z_14),?z)),?z_1), *(+(*(?x_15,?y),*(?y_15,?y)),*(?z,?z_1)) = *(*(+(?x_15,?y_15),*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1), 0 = *(0,?x), +(*(?x,?y_6),?x) = *(s(?y_6),?x), 0 = *(?y,0), +(*(?x_8,?y),?y) = *(?y,s(?x_8)), *(?x_11,*(?y_11,?y)) = *(?y,*(?x_11,?y_11)), +(*(?x,?y_12),*(?x,?z_12)) = *(+(?y_12,?z_12),?x), +(*(?x_13,?y),*(?y_13,?y)) = *(?y,+(?x_13,?y_13)), *(?x,*(?y,?z_12)) = *(*(?y,?x),?z_12), 0 = +(*(0,?y),*(0,0)), 0 = +(*(0,?y),*(0,s(?y_3))), 0 = +(*(0,0),*(0,?z)), 0 = +(*(0,s(?x_5)),*(0,?z)), 0 = +(*(0,+(?x_10,?y_10)),*(0,?z)), 0 = +(*(0,?y),*(0,?z)), +(*(?x_8,?y),?y) = +(*(s(?x_8),?y),*(s(?x_8),0)), +(*(?x_8,s(+(?y,?y_11))),s(+(?y,?y_11))) = +(*(s(?x_8),?y),*(s(?x_8),s(?y_11))), +(*(?x_8,?z),?z) = +(*(s(?x_8),0),*(s(?x_8),?z)), +(*(?x_8,s(+(?x_13,?z))),s(+(?x_13,?z))) = +(*(s(?x_8),s(?x_13)),*(s(?x_8),?z)), +(*(?x_8,+(?x_18,+(?y_18,?z))),+(?x_18,+(?y_18,?z))) = +(*(s(?x_8),+(?x_18,?y_18)),*(s(?x_8),?z)), +(*(?x_8,+(?z,?y)),+(?z,?y)) = +(*(s(?x_8),?y),*(s(?x_8),?z)), *(?x_11,*(?y_11,?y)) = +(*(*(?x_11,?y_11),?y),*(*(?x_11,?y_11),0)), *(?x_11,*(?y_11,s(+(?y,?y_14)))) = +(*(*(?x_11,?y_11),?y),*(*(?x_11,?y_11),s(?y_14))), *(?x_11,*(?y_11,?z)) = +(*(*(?x_11,?y_11),0),*(*(?x_11,?y_11),?z)), *(?x_11,*(?y_11,s(+(?x_16,?z)))) = +(*(*(?x_11,?y_11),s(?x_16)),*(*(?x_11,?y_11),?z)), *(?x_11,*(?y_11,+(?x_21,+(?y_21,?z)))) = +(*(*(?x_11,?y_11),+(?x_21,?y_21)),*(*(?x_11,?y_11),?z)), *(?x_11,*(?y_11,+(?z,?y))) = +(*(*(?x_11,?y_11),?y),*(*(?x_11,?y_11),?z)), *(?y,?x) = +(*(?x,?y),*(?x,0)), *(s(+(?y,?y_3)),?x) = +(*(?x,?y),*(?x,s(?y_3))), *(?z,?x) = +(*(?x,0),*(?x,?z)), *(s(+(?x_5,?z)),?x) = +(*(?x,s(?x_5)),*(?x,?z)), *(+(?x_10,+(?y_10,?z)),?x) = +(*(?x,+(?x_10,?y_10)),*(?x,?z)), *(+(?z,?y),?x) = +(*(?x,?y),*(?x,?z)), +(*(?x_13,?y),*(?y_13,?y)) = +(*(+(?x_13,?y_13),?y),*(+(?x_13,?y_13),0)), +(*(?x_13,s(+(?y,?y_16))),*(?y_13,s(+(?y,?y_16)))) = +(*(+(?x_13,?y_13),?y),*(+(?x_13,?y_13),s(?y_16))), +(*(?x_13,?z),*(?y_13,?z)) = +(*(+(?x_13,?y_13),0),*(+(?x_13,?y_13),?z)), +(*(?x_13,s(+(?x_18,?z))),*(?y_13,s(+(?x_18,?z)))) = +(*(+(?x_13,?y_13),s(?x_18)),*(+(?x_13,?y_13),?z)), +(*(?x_13,+(?x_23,+(?y_23,?z))),*(?y_13,+(?x_23,+(?y_23,?z)))) = +(*(+(?x_13,?y_13),+(?x_23,?y_23)),*(+(?x_13,?y_13),?z)), +(*(?x_13,+(?z,?y)),*(?y_13,+(?z,?y))) = +(*(+(?x_13,?y_13),?y),*(+(?x_13,?y_13),?z)), +(*(?x_8,+(?y,?z)),+(?y,?z)) = +(*(s(?x_8),?y),*(s(?x_8),?z)), *(?x_11,*(?y_11,+(?y,?z))) = +(*(*(?x_11,?y_11),?y),*(*(?x_11,?y_11),?z)), *(+(?y,?z),?x) = +(*(?x,?y),*(?x,?z)), +(*(?x_13,+(?y,?z)),*(?y_13,+(?y,?z))) = +(*(+(?x_13,?y_13),?y),*(+(?x_13,?y_13),?z)), *(?x,?y) = +(*(?x,?y),*(?x,0)), *(?x,s(+(?y,?y_3))) = +(*(?x,?y),*(?x,s(?y_3))), *(?x,?z) = +(*(?x,0),*(?x,?z)), *(?x,s(+(?x_5,?z))) = +(*(?x,s(?x_5)),*(?x,?z)), *(?x,+(?x_10,+(?y_10,?z))) = +(*(?x,+(?x_10,?y_10)),*(?x,?z)), *(?x,+(?z,?y)) = +(*(?x,?y),*(?x,?z)), *(?x,*(?y,?z_12)) = *(+(*(?x,?y),*(?x,0)),?z_12), *(?x,*(s(+(?y,?y_15)),?z_12)) = *(+(*(?x,?y),*(?x,s(?y_15))),?z_12), *(?x,*(?z,?z_12)) = *(+(*(?x,0),*(?x,?z)),?z_12), *(?x,*(s(+(?x_17,?z)),?z_12)) = *(+(*(?x,s(?x_17)),*(?x,?z)),?z_12), *(?x,*(+(?x_22,+(?y_22,?z)),?z_12)) = *(+(*(?x,+(?x_22,?y_22)),*(?x,?z)),?z_12), *(?x,*(+(?z,?y),?z_12)) = *(+(*(?x,?y),*(?x,?z)),?z_12), *(?x,*(+(?y,?z),?z_12)) = *(+(*(?x,?y),*(?x,?z)),?z_12), 0 = +(*(?x,0),*(0,0)), 0 = +(*(?x,0),*(s(?y_3),0)), 0 = +(*(0,0),*(?y,0)), 0 = +(*(s(?x_5),0),*(?y,0)), 0 = +(*(+(?x_10,?y_10),0),*(?y,0)), 0 = +(*(?x,0),*(?y,0)), +(*(?x,?y_6),?x) = +(*(?x,s(?y_6)),*(0,s(?y_6))), +(*(s(+(?x,?y_9)),?y_6),s(+(?x,?y_9))) = +(*(?x,s(?y_6)),*(s(?y_9),s(?y_6))), +(*(?y,?y_6),?y) = +(*(0,s(?y_6)),*(?y,s(?y_6))), +(*(s(+(?x_11,?y)),?y_6),s(+(?x_11,?y))) = +(*(s(?x_11),s(?y_6)),*(?y,s(?y_6))), +(*(+(?x_16,+(?y_16,?y)),?y_6),+(?x_16,+(?y_16,?y))) = +(*(+(?x_16,?y_16),s(?y_6)),*(?y,s(?y_6))), +(*(+(?y,?x),?y_6),+(?y,?x)) = +(*(?x,s(?y_6)),*(?y,s(?y_6))), *(?z,?x) = +(*(?x,?z),*(0,?z)), *(?z,s(+(?x,?y_3))) = +(*(?x,?z),*(s(?y_3),?z)), *(?z,?y) = +(*(0,?z),*(?y,?z)), *(?z,s(+(?x_5,?y))) = +(*(s(?x_5),?z),*(?y,?z)), *(?z,+(?x_10,+(?y_10,?y))) = +(*(+(?x_10,?y_10),?z),*(?y,?z)), *(?z,+(?y,?x)) = +(*(?x,?z),*(?y,?z)), +(*(?x,?y_13),*(?x,?z_13)) = +(*(?x,+(?y_13,?z_13)),*(0,+(?y_13,?z_13))), +(*(s(+(?x,?y_16)),?y_13),*(s(+(?x,?y_16)),?z_13)) = +(*(?x,+(?y_13,?z_13)),*(s(?y_16),+(?y_13,?z_13))), +(*(?y,?y_13),*(?y,?z_13)) = +(*(0,+(?y_13,?z_13)),*(?y,+(?y_13,?z_13))), +(*(s(+(?x_18,?y)),?y_13),*(s(+(?x_18,?y)),?z_13)) = +(*(s(?x_18),+(?y_13,?z_13)),*(?y,+(?y_13,?z_13))), +(*(+(?x_23,+(?y_23,?y)),?y_13),*(+(?x_23,+(?y_23,?y)),?z_13)) = +(*(+(?x_23,?y_23),+(?y_13,?z_13)),*(?y,+(?y_13,?z_13))), +(*(+(?y,?x),?y_13),*(+(?y,?x),?z_13)) = +(*(?x,+(?y_13,?z_13)),*(?y,+(?y_13,?z_13))), +(*(+(?x,?y),?y_6),+(?x,?y)) = +(*(?x,s(?y_6)),*(?y,s(?y_6))), *(?z,+(?x,?y)) = +(*(?x,?z),*(?y,?z)), +(*(+(?x,?y),?y_13),*(+(?x,?y),?z_13)) = +(*(?x,+(?y_13,?z_13)),*(?y,+(?y_13,?z_13))), *(?x,?z) = +(*(?x,?z),*(0,?z)), *(s(+(?x,?y_3)),?z) = +(*(?x,?z),*(s(?y_3),?z)), *(?y,?z) = +(*(0,?z),*(?y,?z)), *(s(+(?x_5,?y)),?z) = +(*(s(?x_5),?z),*(?y,?z)), *(+(?x_10,+(?y_10,?y)),?z) = +(*(+(?x_10,?y_10),?z),*(?y,?z)), *(+(?y,?x),?z) = +(*(?x,?z),*(?y,?z)), *(?x,*(?z,?z_12)) = *(+(*(?x,?z),*(0,?z)),?z_12), *(s(+(?x,?y_15)),*(?z,?z_12)) = *(+(*(?x,?z),*(s(?y_15),?z)),?z_12), *(?y,*(?z,?z_12)) = *(+(*(0,?z),*(?y,?z)),?z_12), *(s(+(?x_17,?y)),*(?z,?z_12)) = *(+(*(s(?x_17),?z),*(?y,?z)),?z_12), *(+(?x_22,+(?y_22,?y)),*(?z,?z_12)) = *(+(*(+(?x_22,?y_22),?z),*(?y,?z)),?z_12), *(+(?y,?x),*(?z,?z_12)) = *(+(*(?x,?z),*(?y,?z)),?z_12), *(+(?x,?y),*(?z,?z_12)) = *(+(*(?x,?z),*(?y,?z)),?z_12) ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair <+(?x,?z_8), +(?x,+(0,?z_8))> by Rules <0, 8> preceded by [(+,1)] joinable by a reduction of rules <[], [([(+,2)],2)]> Critical Pair <+(s(+(?x_1,?y_1)),?z_8), +(?x_1,+(s(?y_1),?z_8))> by Rules <1, 8> preceded by [(+,1)] joinable by a reduction of rules <[([],3),([(s,1)],8)], [([(+,2)],3),([],1)]> Critical Pair <+(?y_2,?z_8), +(0,+(?y_2,?z_8))> by Rules <2, 8> preceded by [(+,1)] joinable by a reduction of rules <[], [([],2)]> Critical Pair <+(s(+(?x_3,?y_3)),?z_8), +(s(?x_3),+(?y_3,?z_8))> by Rules <3, 8> preceded by [(+,1)] joinable by a reduction of rules <[([],3),([(s,1)],8)], [([],3)]> Critical Pair <+(+(?y_9,?x_9),?z_8), +(?x_9,+(?y_9,?z_8))> by Rules <9, 8> preceded by [(+,1)] joinable by a reduction of rules <[([(+,1)],9),([],8)], []> joinable by a reduction of rules <[([],8),([(+,2)],9)], [([],9),([],8)]> Critical Pair <*(0,?z_10), *(?x_4,*(0,?z_10))> by Rules <4, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],6)], [([(*,2)],6),([],4)]> joinable by a reduction of rules <[([],11),([],4)], [([(*,2)],6),([],4)]> Critical Pair <*(+(*(?x_5,?y_5),?x_5),?z_10), *(?x_5,*(s(?y_5),?z_10))> by Rules <5, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],13),([(+,1)],10)], [([(*,2)],7),([],12)]> Critical Pair <*(0,?z_10), *(0,*(?y_6,?z_10))> by Rules <6, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],6)], [([],6)]> Critical Pair <*(+(*(?x_7,?y_7),?y_7),?z_10), *(s(?x_7),*(?y_7,?z_10))> by Rules <7, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],13),([(+,1)],10)], [([],7)]> Critical Pair <*(*(?y_11,?x_11),?z_10), *(?x_11,*(?y_11,?z_10))> by Rules <11, 10> preceded by [(*,1)] joinable by a reduction of rules <[([(*,1)],11),([],10)], []> joinable by a reduction of rules <[([],10),([(*,2)],11)], [([],11),([],10)]> Critical Pair <*(+(*(?x_12,?y_12),*(?x_12,?z_12)),?z_10), *(?x_12,*(+(?y_12,?z_12),?z_10))> by Rules <12, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],13),([(+,2)],10),([(+,1)],10)], [([(*,2)],13),([],12)]> joinable by a reduction of rules <[([],13),([(+,1)],10),([(+,2)],10)], [([(*,2)],13),([],12)]> Critical Pair <*(+(*(?x_13,?z_13),*(?y_13,?z_13)),?z_10), *(+(?x_13,?y_13),*(?z_13,?z_10))> by Rules <13, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],13),([(+,2)],10),([(+,1)],10)], [([],13)]> joinable by a reduction of rules <[([],13),([(+,1)],10),([(+,2)],10)], [([],13)]> joinable by a reduction of rules <[([],13),([(+,2)],10),([(+,1)],10)], [([(*,1)],9),([],13),([],9)]> joinable by a reduction of rules <[([],13),([(+,1)],10),([(+,2)],10)], [([(*,1)],9),([],13),([],9)]> Critical Pair <*(?x_12,?x), +(*(?x_12,?x),*(?x_12,0))> by Rules <0, 12> preceded by [(*,2)] joinable by a reduction of rules <[], [([(+,2)],4),([],0)]> Critical Pair <*(?x_12,s(+(?x_1,?y_1))), +(*(?x_12,?x_1),*(?x_12,s(?y_1)))> by Rules <1, 12> preceded by [(*,2)] joinable by a reduction of rules <[([],5),([(+,1)],12),([],8)], [([(+,2)],5)]> joinable by a reduction of rules <[([],5),([(+,1)],12),([],8)], [([(+,2)],11),([(+,2)],7),([(+,2),(+,1)],11)]> joinable by a reduction of rules <[([],5),([(+,1)],12),([],8)], [([(+,1)],11),([(+,2)],5),([(+,1)],11)]> joinable by a reduction of rules <[([],5),([(+,1)],12),([],8)], [([],9),([(+,1)],5),([],9)]> Critical Pair <*(?x_12,?y_2), +(*(?x_12,0),*(?x_12,?y_2))> by Rules <2, 12> preceded by [(*,2)] joinable by a reduction of rules <[], [([(+,1)],4),([],2)]> Critical Pair <*(?x_12,s(+(?x_3,?y_3))), +(*(?x_12,s(?x_3)),*(?x_12,?y_3))> by Rules <3, 12> preceded by [(*,2)] joinable by a reduction of rules <[([],5),([(+,1)],12),([],9)], [([(+,1)],5),([(+,1)],9),([],8)]> joinable by a reduction of rules <[([],5),([(+,1)],12),([],8)], [([(+,1)],5),([],8),([(+,2)],9)]> joinable by a reduction of rules <[([],5),([],9),([(+,2)],12)], [([(+,1)],5),([(+,1)],9),([],8)]> Critical Pair <*(?x_12,+(?x_8,+(?y_8,?z_8))), +(*(?x_12,+(?x_8,?y_8)),*(?x_12,?z_8))> by Rules <8, 12> preceded by [(*,2)] joinable by a reduction of rules <[([],12),([(+,2)],12)], [([(+,1)],12),([],8)]> Critical Pair <*(?x_12,+(?y_9,?x_9)), +(*(?x_12,?x_9),*(?x_12,?y_9))> by Rules <9, 12> preceded by [(*,2)] joinable by a reduction of rules <[([],12)], [([],9)]> Critical Pair <*(?x,?z_13), +(*(?x,?z_13),*(0,?z_13))> by Rules <0, 13> preceded by [(*,1)] joinable by a reduction of rules <[], [([(+,2)],6),([],0)]> Critical Pair <*(s(+(?x_1,?y_1)),?z_13), +(*(?x_1,?z_13),*(s(?y_1),?z_13))> by Rules <1, 13> preceded by [(*,1)] joinable by a reduction of rules <[([],7),([(+,1)],13),([],8)], [([(+,2)],7)]> joinable by a reduction of rules <[([],7),([(+,1)],13),([],8)], [([(+,2)],11),([(+,2)],5),([(+,2),(+,1)],11)]> joinable by a reduction of rules <[([],7),([(+,1)],13),([],8)], [([(+,1)],11),([(+,2)],7),([(+,1)],11)]> joinable by a reduction of rules <[([],7),([(+,1)],13),([],8)], [([],9),([(+,1)],7),([],9)]> Critical Pair <*(?y_2,?z_13), +(*(0,?z_13),*(?y_2,?z_13))> by Rules <2, 13> preceded by [(*,1)] joinable by a reduction of rules <[], [([(+,1)],6),([],2)]> Critical Pair <*(s(+(?x_3,?y_3)),?z_13), +(*(s(?x_3),?z_13),*(?y_3,?z_13))> by Rules <3, 13> preceded by [(*,1)] joinable by a reduction of rules <[([],7),([(+,1)],13),([],9)], [([(+,1)],7),([(+,1)],9),([],8)]> joinable by a reduction of rules <[([],7),([(+,1)],13),([],8)], [([(+,1)],7),([],8),([(+,2)],9)]> joinable by a reduction of rules <[([],7),([],9),([(+,2)],13)], [([(+,1)],7),([(+,1)],9),([],8)]> Critical Pair <*(+(?x_8,+(?y_8,?z_8)),?z_13), +(*(+(?x_8,?y_8),?z_13),*(?z_8,?z_13))> by Rules <8, 13> preceded by [(*,1)] joinable by a reduction of rules <[([],13),([(+,2)],13)], [([(+,1)],13),([],8)]> Critical Pair <*(+(?y_9,?x_9),?z_13), +(*(?x_9,?z_13),*(?y_9,?z_13))> by Rules <9, 13> preceded by [(*,1)] joinable by a reduction of rules <[([],13)], [([],9)]> Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <8, 8> preceded by [(+,1)] joinable by a reduction of rules <[([],8),([(+,2)],8)], [([],8)]> Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <10, 10> preceded by [(*,1)] joinable by a reduction of rules <[([],10),([(*,2)],10)], [([],10)]> Critical Pair <0, 0> by Rules <2, 0> preceded by [] joinable by a reduction of rules <[], []> Critical Pair by Rules <3, 0> preceded by [] joinable by a reduction of rules <[([(s,1)],0)], []> Critical Pair <+(?x_8,+(?y_8,0)), +(?x_8,?y_8)> by Rules <8, 0> preceded by [] joinable by a reduction of rules <[([(+,2)],0)], []> Critical Pair <+(0,?x_9), ?x_9> by Rules <9, 0> preceded by [] joinable by a reduction of rules <[([],2)], []> Critical Pair by Rules <2, 1> preceded by [] joinable by a reduction of rules <[], [([(s,1)],2)]> Critical Pair by Rules <3, 1> preceded by [] joinable by a reduction of rules <[([(s,1)],1)], [([(s,1)],3)]> Critical Pair <+(?x_8,+(?y_8,s(?y_1))), s(+(+(?x_8,?y_8),?y_1))> by Rules <8, 1> preceded by [] joinable by a reduction of rules <[([(+,2)],1),([],1)], [([(s,1)],8)]> Critical Pair <+(s(?y_1),?x_9), s(+(?x_9,?y_1))> by Rules <9, 1> preceded by [] joinable by a reduction of rules <[([],3)], [([(s,1)],9)]> Critical Pair <+(?y_9,0), ?y_9> by Rules <9, 2> preceded by [] joinable by a reduction of rules <[([],0)], []> Critical Pair <+(?y_9,s(?x_3)), s(+(?x_3,?y_9))> by Rules <9, 3> preceded by [] joinable by a reduction of rules <[([],1)], [([(s,1)],9)]> Critical Pair <0, 0> by Rules <6, 4> preceded by [] joinable by a reduction of rules <[], []> Critical Pair <+(*(?x_7,0),0), 0> by Rules <7, 4> preceded by [] joinable by a reduction of rules <[([(+,1)],4),([],2)], []> joinable by a reduction of rules <[([(+,1)],4),([],0)], []> joinable by a reduction of rules <[([],0),([],4)], []> Critical Pair <*(?x_10,*(?y_10,0)), 0> by Rules <10, 4> preceded by [] joinable by a reduction of rules <[([(*,2)],4),([],4)], []> Critical Pair <*(0,?x_11), 0> by Rules <11, 4> preceded by [] joinable by a reduction of rules <[([],6)], []> Critical Pair <+(*(?x_13,0),*(?y_13,0)), 0> by Rules <13, 4> preceded by [] joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],2)], []> joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0)], []> joinable by a reduction of rules <[([(+,2)],4),([],0),([],4)], []> joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],2)], []> joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0)], []> joinable by a reduction of rules <[([(+,1)],4),([],2),([],4)], []> Critical Pair <0, +(*(0,?y_5),0)> by Rules <6, 5> preceded by [] joinable by a reduction of rules <[], [([(+,1)],6),([],2)]> joinable by a reduction of rules <[], [([(+,1)],6),([],0)]> joinable by a reduction of rules <[], [([],0),([],6)]> Critical Pair <+(*(?x_7,s(?y_5)),s(?y_5)), +(*(s(?x_7),?y_5),s(?x_7))> by Rules <7, 5> preceded by [] joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([(+,1)],7),([],9),([],3)]> joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([(+,1)],7),([],1),([(s,1)],9)]> joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([],9),([(+,2)],7),([],3)]> joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([],9),([],3),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([],1),([(s,1),(+,1)],7),([(s,1)],9)]> joinable by a reduction of rules <[([(+,1)],5),([(+,1)],9),([],1),([(s,1)],8)], [([],1),([(s,1)],9),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],9),([(+,2)],3)], [([(+,1)],7),([],8),([(+,2)],1)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],1),([(+,2),(s,1)],9)], [([(+,1)],7),([],8),([(+,2)],1)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([(+,1)],7),([],9),([],3)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([(+,1)],7),([],1),([(s,1)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([],9),([(+,2)],7),([],3)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([],9),([],3),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([],1),([(s,1),(+,1)],7),([(s,1)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1),(+,1)],9),([(s,1)],8)], [([],1),([(s,1)],9),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],8),([(s,1),(+,2)],9)], [([(+,1)],7),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],8),([(s,1),(+,2)],9)], [([],1),([(s,1),(+,1)],7),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([(+,1)],7),([],9),([],3)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([(+,1)],7),([],1),([(s,1)],9)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([],9),([(+,2)],7),([],3)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([],9),([],3),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([],1),([(s,1),(+,1)],7),([(s,1)],9)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1),(+,1)],9),([(s,1)],8)], [([],1),([(s,1)],9),([(s,1),(+,2)],7)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],8),([(s,1),(+,2)],9)], [([(+,1)],7),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],8),([(s,1),(+,2)],9)], [([],1),([(s,1),(+,1)],7),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],9),([],3)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],9),([],3)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],9),([],3)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],1)], [([(+,1)],7),([],8),([(+,2)],9),([(+,2)],3)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],1)], [([(+,1)],7),([],8),([(+,2)],1),([(+,2),(s,1)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],9)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],9)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],9)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],8)], [([(+,1)],7),([],1),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],8)], [([],1),([(s,1),(+,1)],7),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([],9),([(+,2)],5),([],3)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([],9),([(+,2)],5),([],3)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],9),([(+,2)],5),([],3)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],9),([],3),([(s,1),(+,2)],5)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([],9),([],3),([(s,1),(+,2)],5)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],9),([],3),([(s,1),(+,2)],5)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],9)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],9)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],9)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],8)], [([(+,1)],7),([],1),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],8)], [([],1),([(s,1),(+,1)],7),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([],1),([(s,1)],9),([(s,1),(+,2)],5)], [([(+,1)],7),([(+,1)],9),([],1),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1)],9),([(s,1),(+,2)],5)], [([(+,1)],7),([],1),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([],1),([(s,1)],9),([(s,1),(+,2)],5)], [([],1),([(s,1),(+,1)],7),([(s,1),(+,1)],9),([(s,1)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],1),([],1)], [([(+,1)],7),([],1),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2)],1),([],1)], [([],1),([(s,1),(+,1)],7),([(s,1)],8),([(s,1),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],5),([],1),([(s,1)],8),([(s,1),(+,2)],9)], [([(+,1)],7),([],8),([(+,2)],1),([],1)]> joinable by a reduction of rules <[([],1),([(s,1),(+,1)],5),([(s,1)],8),([(s,1),(+,2)],9)], [([(+,1)],7),([],8),([(+,2)],1),([],1)]> Critical Pair <*(?x_10,*(?y_10,s(?y_5))), +(*(*(?x_10,?y_10),?y_5),*(?x_10,?y_10))> by Rules <10, 5> preceded by [] joinable by a reduction of rules <[([(*,2)],5),([],12)], [([(+,1)],10)]> Critical Pair <*(s(?y_5),?x_11), +(*(?x_11,?y_5),?x_11)> by Rules <11, 5> preceded by [] joinable by a reduction of rules <[([],7)], [([(+,1)],11)]> Critical Pair <+(*(?x_13,s(?y_5)),*(?y_13,s(?y_5))), +(*(+(?x_13,?y_13),?y_5),+(?x_13,?y_13))> by Rules <13, 5> preceded by [] joinable by a reduction of rules <[([(+,2)],5),([(+,2)],9),([(+,1)],5),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],5),([(+,1)],5),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],5),([(+,1)],5),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],5),([(+,2)],5),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],5),([(+,2)],5),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],5),([],8),([(+,2),(+,2)],5),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> Critical Pair <*(?y_11,0), 0> by Rules <11, 6> preceded by [] joinable by a reduction of rules <[([],4)], []> Critical Pair <+(*(0,?y_12),*(0,?z_12)), 0> by Rules <12, 6> preceded by [] joinable by a reduction of rules <[([(+,2)],6),([(+,1)],6),([],2)], []> joinable by a reduction of rules <[([(+,2)],6),([(+,1)],6),([],0)], []> joinable by a reduction of rules <[([(+,2)],6),([],0),([],6)], []> joinable by a reduction of rules <[([(+,1)],6),([(+,2)],6),([],2)], []> joinable by a reduction of rules <[([(+,1)],6),([(+,2)],6),([],0)], []> joinable by a reduction of rules <[([(+,1)],6),([],2),([],6)], []> Critical Pair <*(?y_11,s(?x_7)), +(*(?x_7,?y_11),?y_11)> by Rules <11, 7> preceded by [] joinable by a reduction of rules <[([],5)], [([(+,1)],11)]> Critical Pair <+(*(s(?x_7),?y_12),*(s(?x_7),?z_12)), +(*(?x_7,+(?y_12,?z_12)),+(?y_12,?z_12))> by Rules <12, 7> preceded by [] joinable by a reduction of rules <[([(+,2)],7),([(+,2)],9),([(+,1)],7),([],8)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],7),([(+,1)],7),([(+,2)],9),([],8)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],7),([(+,1)],7),([],8),([(+,2),(+,2)],9)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],7),([(+,2)],7),([(+,2)],9),([],8)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],7),([(+,2)],7),([],8),([(+,2),(+,2)],9)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],7),([],8),([(+,2),(+,2)],7),([(+,2),(+,2)],9)], [([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)]> Critical Pair <+(?y_9,+(?x_8,?y_8)), +(?x_8,+(?y_8,?y_9))> by Rules <9, 8> preceded by [] joinable by a reduction of rules <[([],9),([],8)], []> Critical Pair <*(?y_11,*(?x_10,?y_10)), *(?x_10,*(?y_10,?y_11))> by Rules <11, 10> preceded by [] joinable by a reduction of rules <[([],11),([],10)], []> Critical Pair <+(*(*(?x_10,?y_10),?y_12),*(*(?x_10,?y_10),?z_12)), *(?x_10,*(?y_10,+(?y_12,?z_12)))> by Rules <12, 10> preceded by [] joinable by a reduction of rules <[([(+,2)],10),([(+,1)],10)], [([(*,2)],12),([],12)]> joinable by a reduction of rules <[([(+,1)],10),([(+,2)],10)], [([(*,2)],12),([],12)]> Critical Pair <+(*(?x_12,?y_12),*(?x_12,?z_12)), *(+(?y_12,?z_12),?x_12)> by Rules <12, 11> preceded by [] joinable by a reduction of rules <[([(+,2)],11),([(+,1)],11)], [([],13)]> joinable by a reduction of rules <[([(+,1)],11),([(+,2)],11)], [([],13)]> joinable by a reduction of rules <[], [([],11),([],12)]> joinable by a reduction of rules <[([(+,2)],11)], [([],13),([(+,1)],11)]> joinable by a reduction of rules <[([(+,1)],11)], [([],13),([(+,2)],11)]> Critical Pair <+(*(?x_13,?z_13),*(?y_13,?z_13)), *(?z_13,+(?x_13,?y_13))> by Rules <13, 11> preceded by [] joinable by a reduction of rules <[([(+,2)],11),([(+,1)],11)], [([],12)]> joinable by a reduction of rules <[([(+,1)],11),([(+,2)],11)], [([],12)]> joinable by a reduction of rules <[], [([],11),([],13)]> joinable by a reduction of rules <[([(+,2)],11)], [([],12),([(+,1)],11)]> joinable by a reduction of rules <[([(+,1)],11)], [([],12),([(+,2)],11)]> Critical Pair <+(*(?x_13,+(?y_12,?z_12)),*(?y_13,+(?y_12,?z_12))), +(*(+(?x_13,?y_13),?y_12),*(+(?x_13,?y_13),?z_12))> by Rules <13, 12> preceded by [] joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,2)],13),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,2)],9),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2),(*,1)],9),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,2)],13),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,2)],9),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2),(*,1)],9),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,2)],13),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,2)],9),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2),(*,1)],9),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2)],9),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,2)],13),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2),(*,1)],9),([(+,1)],13),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2)],13),([(+,2)],9),([(+,1)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([(+,2)],13),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([(+,2),(*,1)],9),([],8),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([(+,2)],9),([],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2),(*,1)],9),([(+,2),(+,2)],13)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2)],9),([(+,2),(+,1)],12),([(+,2)],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2),(+,2)],9)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,2)],12),([(+,1)],12),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,2)],12),([(+,1)],12),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,2)],12),([(+,1)],12),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,2)],12),([(+,1)],12),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([(+,2)],12),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([(+,2)],12),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([(+,2)],12),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([(+,2)],12),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([],8),([(+,2),(+,2)],12)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2),(*,2)],9),([(+,1)],12),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,2)],9),([(+,1)],12),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,2)],9),([(+,1)],12),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,2)],9),([(+,1)],12),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,2)],9),([(+,1)],12),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([(+,2)],9),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([(+,2)],9),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2),(+,2)],9)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,2)],12),([(+,1)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([(+,2)],12),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([(+,2)],12),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([(+,2)],12),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([(+,2)],12),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([],8),([(+,2),(+,2)],12)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2),(*,2)],9),([],8),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([(+,2)],9),([],8)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([(+,2)],9),([],8)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([(+,2)],9),([],8)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2),(+,2)],9)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([(+,2)],12),([],8),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2),(*,2)],9),([(+,2),(+,2)],12)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2),(*,2)],9),([(+,2),(+,2)],12)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2),(*,2)],9),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2),(*,2)],9),([(+,2),(+,2)],12)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2),(+,2)],9)], [([(+,2)],13),([(+,1)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2),(+,2)],9)], [([(+,1)],13),([(+,2)],13),([],8),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2),(+,2)],13),([(+,2)],9),([(+,2)],8)]> joinable by a reduction of rules <[([(+,1)],12),([],8),([(+,2),(+,2)],12),([(+,2),(+,2)],9)], [([(+,1)],13),([],8),([(+,2)],9),([(+,2),(+,1)],13),([(+,2)],8)]> unknown Diagram Decreasing [ +(?x,0) -> ?x, +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)), +(0,?y_2) -> ?y_2, +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)), *(?x_4,0) -> 0, *(?x_5,s(?y_5)) -> +(*(?x_5,?y_5),?x_5), *(0,?y_6) -> 0, *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7), +(+(?x_8,?y_8),?z_8) -> +(?x_8,+(?y_8,?z_8)), +(?x_9,?y_9) -> +(?y_9,?x_9), *(*(?x_10,?y_10),?z_10) -> *(?x_10,*(?y_10,?z_10)), *(?x_11,?y_11) -> *(?y_11,?x_11), *(?x_12,+(?y_12,?z_12)) -> +(*(?x_12,?y_12),*(?x_12,?z_12)), *(+(?x_13,?y_13),?z_13) -> +(*(?x_13,?z_13),*(?y_13,?z_13)) ] Sort Assignment: * : 38*38=>38 + : 38*38=>38 0 : =>38 s : 38=>38 non-linear variables: {?x_5,?y_7,?x_12,?z_13} non-linear types: {38} types leq non-linear types: {38} rules applicable to terms of non-linear types: [ +(?x,0) -> ?x, +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)), +(0,?y_2) -> ?y_2, +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)), *(?x_4,0) -> 0, *(?x_5,s(?y_5)) -> +(*(?x_5,?y_5),?x_5), *(0,?y_6) -> 0, *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7), +(+(?x_8,?y_8),?z_8) -> +(?x_8,+(?y_8,?z_8)), +(?x_9,?y_9) -> +(?y_9,?x_9), *(*(?x_10,?y_10),?z_10) -> *(?x_10,*(?y_10,?z_10)), *(?x_11,?y_11) -> *(?y_11,?x_11), *(?x_12,+(?y_12,?z_12)) -> +(*(?x_12,?y_12),*(?x_12,?z_12)), *(+(?x_13,?y_13),?z_13) -> +(*(?x_13,?z_13),*(?y_13,?z_13)) ] NLR: 0: {} 1: {} 2: {} 3: {} 4: {} 5: {0,1,2,3,4,5,6,7,8,9,10,11,12,13} 6: {} 7: {0,1,2,3,4,5,6,7,8,9,10,11,12,13} 8: {} 9: {} 10: {} 11: {} 12: {0,1,2,3,4,5,6,7,8,9,10,11,12,13} 13: {0,1,2,3,4,5,6,7,8,9,10,11,12,13} unknown innermost-termination for terms of non-linear types unknown Quasi-Linear & Linearized-Decreasing [ +(?x,0) -> ?x, +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)), +(0,?y_2) -> ?y_2, +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)), *(?x_4,0) -> 0, *(?x_5,s(?y_5)) -> +(*(?x_5,?y_5),?x_5), *(0,?y_6) -> 0, *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7), +(+(?x_8,?y_8),?z_8) -> +(?x_8,+(?y_8,?z_8)), +(?x_9,?y_9) -> +(?y_9,?x_9), *(*(?x_10,?y_10),?z_10) -> *(?x_10,*(?y_10,?z_10)), *(?x_11,?y_11) -> *(?y_11,?x_11), *(?x_12,+(?y_12,?z_12)) -> +(*(?x_12,?y_12),*(?x_12,?z_12)), *(+(?x_13,?y_13),?z_13) -> +(*(?x_13,?z_13),*(?y_13,?z_13)) ] Sort Assignment: * : 38*38=>38 + : 38*38=>38 0 : =>38 s : 38=>38 non-linear variables: {?x_5,?y_7,?x_12,?z_13} non-linear types: {38} types leq non-linear types: {38} rules applicable to terms of non-linear types: [ +(?x,0) -> ?x, +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)), +(0,?y_2) -> ?y_2, +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)), *(?x_4,0) -> 0, *(?x_5,s(?y_5)) -> +(*(?x_5,?y_5),?x_5), *(0,?y_6) -> 0, *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7), +(+(?x_8,?y_8),?z_8) -> +(?x_8,+(?y_8,?z_8)), +(?x_9,?y_9) -> +(?y_9,?x_9), *(*(?x_10,?y_10),?z_10) -> *(?x_10,*(?y_10,?z_10)), *(?x_11,?y_11) -> *(?y_11,?x_11), *(?x_12,+(?y_12,?z_12)) -> +(*(?x_12,?y_12),*(?x_12,?z_12)), *(+(?x_13,?y_13),?z_13) -> +(*(?x_13,?z_13),*(?y_13,?z_13)) ] unknown innermost-termination for terms of non-linear types unknown Strongly Quasi-Linear & Hierarchically Decreasing check Non-Confluence... obtain 24 rules by 3 steps unfolding strenghten *(?x_16,0) and 0 strenghten *(0,?x_11) and 0 strenghten +(?x_20,0) and ?x_20 strenghten +(0,?x_9) and ?x_9 strenghten *(?x_23,?y_23) and *(?y_23,?x_23) strenghten s(+(?x_3,0)) and s(?x_3) strenghten s(+(0,?y_1)) and s(?y_1) strenghten *(?x_10,*(?y_10,0)) and 0 strenghten +(*(?x_7,0),0) and 0 strenghten +(*(0,?y_5),0) and 0 strenghten s(+(?x_3,?y_9)) and +(?y_9,s(?x_3)) strenghten s(+(?x_9,?y_1)) and +(s(?y_1),?x_9) strenghten *(?x_4,*(0,?z_10)) and *(0,?z_10) strenghten *(0,*(?x_16,?z_10)) and *(0,?z_10) strenghten +(?x,+(0,?z_8)) and +(?x,?z_8) strenghten +(?x_8,+(?y_8,0)) and +(?x_8,?y_8) strenghten +(0,+(?x_20,?z_8)) and +(?x_20,?z_8) strenghten +(*(?x_13,0),*(?y_13,0)) and 0 strenghten +(*(0,?y_12),*(0,?z_12)) and 0 strenghten +(*(?x_7,?y_11),?y_11) and *(?y_11,s(?x_7)) strenghten +(*(?x_7,?y_22),?y_22) and *(s(?x_7),?y_22) strenghten +(*(?x_11,?y_5),?x_11) and *(s(?y_5),?x_11) strenghten +(*(?x_22,?y_5),?x_22) and *(?x_22,s(?y_5)) strenghten *(?x_10,*(?y_10,?y_11)) and *(?y_11,*(?x_10,?y_10)) strenghten *(?x_10,*(?y_10,?y_22)) and *(*(?x_10,?y_10),?y_22) strenghten *(?x_11,*(?y_11,?z_10)) and *(*(?y_11,?x_11),?z_10) strenghten +(?x_8,+(?y_8,?y_9)) and +(?y_9,+(?x_8,?y_8)) strenghten +(?x_9,+(?y_9,?z_8)) and +(+(?y_9,?x_9),?z_8) strenghten s(+(s(?x_3),?y_1)) and s(+(?x_3,s(?y_1))) strenghten +(*(?x,?z_13),*(0,?z_13)) and *(?x,?z_13) strenghten +(*(?x_12,?x),*(?x_12,0)) and *(?x_12,?x) strenghten +(*(?x_12,0),*(?x_12,?x_20)) and *(?x_12,?x_20) strenghten +(*(0,?z_13),*(?x_20,?z_13)) and *(?x_20,?z_13) strenghten +(?x_1,+(s(?y_1),?z_8)) and +(s(+(?x_1,?y_1)),?z_8) obtain 100 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Root-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) unknown Non-Confluence Check relative termination: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)), *(?x,0) -> 0, *(?x,s(?y)) -> +(*(?x,?y),?x), *(0,?y) -> 0, *(s(?x),?y) -> +(*(?x,?y),?y), *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)), *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) ] [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), +(?x,?y) -> +(?y,?x), *(*(?x,?y),?z) -> *(?x,*(?y,?z)), *(?x,?y) -> *(?y,?x) ] Polynomial Interpretation: *:= (1)*x1+(1)*x1*x2+(1)*x2 +:= (1)+(1)*x1+(1)*x2 0:= 0 s:= (3)+(1)*x1 retract +(?x,0) -> ?x retract +(0,?y) -> ?y retract *(?x,s(?y)) -> +(*(?x,?y),?x) retract *(s(?x),?y) -> +(*(?x,?y),?y) Polynomial Interpretation: *:= (2)+(2)*x1+(1)*x1*x2+(2)*x2 +:= (2)+(1)*x1+(1)*x2 0:= (2) s:= (1)*x1 retract +(?x,0) -> ?x retract +(0,?y) -> ?y retract *(?x,0) -> 0 retract *(?x,s(?y)) -> +(*(?x,?y),?x) retract *(0,?y) -> 0 retract *(s(?x),?y) -> +(*(?x,?y),?y) Polynomial Interpretation: *:= (2)+(2)*x1+(1)*x1*x2+(2)*x2 +:= (3)+(1)*x1+(1)*x2 0:= (2) s:= (1)*x1 retract +(?x,0) -> ?x retract +(0,?y) -> ?y retract *(?x,0) -> 0 retract *(?x,s(?y)) -> +(*(?x,?y),?x) retract *(0,?y) -> 0 retract *(s(?x),?y) -> +(*(?x,?y),?y) retract *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) retract *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) Polynomial Interpretation: *:= (1)*x1+(1)*x2 +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2 0:= (1) s:= (4)+(1)*x1 relatively terminating Huet (modulo AC) Direct Methods: CR Final result: CR 208.trs: Success(CR) (39748 msec.)