(ignored inputs)COMMENT doi:10.1145/322217.322230 [12] p. 819 submitted by: Aart Middeldorp
Rewrite Rules:
   [ E(+(?x,?y)) -> *(E(?x),E(?y)),
     E(0) -> 1,
     +(?x,0) -> ?x,
     +(0,?x) -> ?x,
     *(?x,1) -> ?x,
     *(1,?x) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?x,?y) -> *(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ E(?x_1) = *(E(?x_1),E(0)),
     E(?x_2) = *(E(0),E(?x_2)),
     E(+(?x_5,+(?y_5,?z_5))) = *(E(+(?x_5,?y_5)),E(?z_5)),
     E(+(+(?x_6,?y_6),?z_6)) = *(E(?x_6),E(+(?y_6,?z_6))),
     E(+(?y_7,?x_7)) = *(E(?x_7),E(?y_7)),
     +(?x_1,?z_5) = +(?x_1,+(0,?z_5)),
     +(?x_2,?z_5) = +(0,+(?x_2,?z_5)),
     +(+(+(?x_6,?y_6),?z_6),?z_5) = +(?x_6,+(+(?y_6,?z_6),?z_5)),
     +(+(?y_7,?x_7),?z_5) = +(?x_7,+(?y_7,?z_5)),
     +(?x_6,?x_1) = +(+(?x_6,?x_1),0),
     +(?x_6,?x_2) = +(+(?x_6,0),?x_2),
     +(?x_6,+(?x_5,+(?y_5,?z_5))) = +(+(?x_6,+(?x_5,?y_5)),?z_5),
     +(?x_6,+(?y_7,?x_7)) = +(+(?x_6,?x_7),?y_7),
     *(?x_3,?z_8) = *(?x_3,*(1,?z_8)),
     *(?x_4,?z_8) = *(1,*(?x_4,?z_8)),
     *(*(*(?x_9,?y_9),?z_9),?z_8) = *(?x_9,*(*(?y_9,?z_9),?z_8)),
     *(*(?y_10,?x_10),?z_8) = *(?x_10,*(?y_10,?z_8)),
     *(?x_9,?x_3) = *(*(?x_9,?x_3),1),
     *(?x_9,?x_4) = *(*(?x_9,1),?x_4),
     *(?x_9,*(?x_8,*(?y_8,?z_8))) = *(*(?x_9,*(?x_8,?y_8)),?z_8),
     *(?x_9,*(?y_10,?x_10)) = *(*(?x_9,?x_10),?y_10),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)),
     *(?x_1,*(*(?x,?y),?z)) = *(*(?x_1,?x),*(?y,?z)) ]
Outer CPs:
   [ 0 = 0,
     +(?x_5,?y_5) = +(?x_5,+(?y_5,0)),
     ?x_1 = +(0,?x_1),
     +(?y_6,?z_6) = +(+(0,?y_6),?z_6),
     ?x_2 = +(?x_2,0),
     1 = 1,
     *(?x_8,?y_8) = *(?x_8,*(?y_8,1)),
     ?x_3 = *(1,?x_3),
     *(?y_9,?z_9) = *(*(1,?y_9),?z_9),
     ?x_4 = *(?x_4,1),
     +(?x_5,+(?y_5,+(?y_6,?z_6))) = +(+(+(?x_5,?y_5),?y_6),?z_6),
     +(?x_5,+(?y_5,?z_5)) = +(?z_5,+(?x_5,?y_5)),
     +(+(?x_6,?y_6),?z_6) = +(+(?y_6,?z_6),?x_6),
     *(?x_8,*(?y_8,*(?y_9,?z_9))) = *(*(*(?x_8,?y_8),?y_9),?z_9),
     *(?x_8,*(?y_8,?z_8)) = *(?z_8,*(?x_8,?y_8)),
     *(*(?x_9,?y_9),?z_9) = *(*(?y_9,?z_9),?x_9) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ E(?x) = *(E(?x),E(0)),
     E(?y) = *(E(0),E(?y)),
     E(+(?x_6,+(?y_6,?y))) = *(E(+(?x_6,?y_6)),E(?y)),
     E(+(+(?x,?y_7),?z_7)) = *(E(?x),E(+(?y_7,?z_7))),
     E(+(?y,?x)) = *(E(?x),E(?y)),
     0 = 0,
     +(?x_5,+(?y_5,0)) = +(?x_5,?y_5),
     +(0,?x) = ?x,
     *(E(?x),E(0)) = E(?x),
     +(?x,+(0,?z_6)) = +(?x,?z_6),
     +(+(?x_7,?x),0) = +(?x_7,?x),
     +(+(0,?y_6),?z_6) = +(?y_6,?z_6),
     +(?x,0) = ?x,
     *(E(0),E(?x)) = E(?x),
     +(0,+(?x,?z_6)) = +(?x,?z_6),
     +(+(?x_7,0),?x) = +(?x_7,?x),
     1 = 1,
     *(?x_8,*(?y_8,1)) = *(?x_8,?y_8),
     *(1,?x) = ?x,
     *(?x,*(1,?z_9)) = *(?x,?z_9),
     *(*(?x_10,?x),1) = *(?x_10,?x),
     *(*(1,?y_9),?z_9) = *(?y_9,?z_9),
     *(?x,1) = ?x,
     *(1,*(?x,?z_9)) = *(?x,?z_9),
     *(*(?x_10,1),?x) = *(?x_10,?x),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
     ?x = +(?x,+(0,0)),
     ?y = +(0,+(?y,0)),
     +(+(?x,?y_7),?z_7) = +(?x,+(+(?y_7,?z_7),0)),
     +(?y,?x) = +(?x,+(?y,0)),
     +(+(+(?x_7,+(?y_7,?y)),?y_6),?z_6) = +(+(?x_7,?y_7),+(?y,+(?y_6,?z_6))),
     +(+(?x,?y_6),?z_6) = +(?x,+(0,+(?y_6,?z_6))),
     +(+(?y,?y_6),?z_6) = +(0,+(?y,+(?y_6,?z_6))),
     +(+(+(+(?x,?y_13),?z_13),?y_6),?z_6) = +(?x,+(+(?y_13,?z_13),+(?y_6,?z_6))),
     +(+(+(?y,?x),?y_6),?z_6) = +(?x,+(?y,+(?y_6,?z_6))),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?x) = +(?x,+(0,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,+(+(?x,?y_7),?z_7)) = +(?x,+(+(?y_7,?z_7),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?x,+(?y,0)),
     +(+(+(?x,?y),?y_6),?z_6) = +(?x,+(?y,+(?y_6,?z_6))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?x,?z) = +(?x,+(0,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(+(+(?x,?y_7),?z_7),?z) = +(?x,+(+(?y_7,?z_7),?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),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(+(+(?x,?y_8),?z_8),+(?z,?z_1)) = +(+(?x,+(+(?y_8,?z_8),?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     *(E(+(?x_1,+(?y_1,?y))),E(?z)) = E(+(+(?x_1,?y_1),+(?y,?z))),
     *(E(?x),E(?z)) = E(+(?x,+(0,?z))),
     *(E(?y),E(?z)) = E(+(0,+(?y,?z))),
     *(E(+(+(?x,?y_7),?z_7)),E(?z)) = E(+(?x,+(+(?y_7,?z_7),?z))),
     *(E(+(?y,?x)),E(?z)) = E(+(?x,+(?y,?z))),
     +(+(?x_7,+(?x_8,+(?y_8,?y))),?z) = +(?x_7,+(+(?x_8,?y_8),+(?y,?z))),
     +(+(?x_7,?x),?z) = +(?x_7,+(?x,+(0,?z))),
     +(+(?x_7,+(+(?x,?y_14),?z_14)),?z) = +(?x_7,+(?x,+(+(?y_14,?z_14),?z))),
     +(+(?x_7,+(?y,?x)),?z) = +(?x_7,+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     *(E(+(?x,?y)),E(?z)) = E(+(?x,+(?y,?z))),
     +(+(?x_7,+(?x,?y)),?z) = +(?x_7,+(?x,+(?y,?z))),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     ?y = +(+(0,?y),0),
     ?z = +(+(0,0),?z),
     +(?z,?y) = +(+(0,?y),?z),
     +(?x_6,+(?y_6,+(+(?y,?y_7),?z_7))) = +(+(+(?x_6,?y_6),?y),+(?y_7,?z_7)),
     +(?x_6,+(?y_6,?y)) = +(+(+(?x_6,?y_6),?y),0),
     +(?x_6,+(?y_6,?z)) = +(+(+(?x_6,?y_6),0),?z),
     +(?x_6,+(?y_6,+(?x_13,+(?y_13,?z)))) = +(+(+(?x_6,?y_6),+(?x_13,?y_13)),?z),
     +(?x_6,+(?y_6,+(?z,?y))) = +(+(+(?x_6,?y_6),?y),?z),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?y,?x) = +(+(?x,?y),0),
     +(?z,?x) = +(+(?x,0),?z),
     +(+(?x_7,+(?y_7,?z)),?x) = +(+(?x,+(?x_7,?y_7)),?z),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(?y,?z) = +(+(0,?y),?z),
     +(?x_6,+(?y_6,+(?y,?z))) = +(+(+(?x_6,?y_6),?y),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,?y) = +(+(?x,?y),0),
     +(?x,?z) = +(+(?x,0),?z),
     +(?x,+(?x_7,+(?y_7,?z))) = +(+(?x,+(?x_7,?y_7)),?z),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)),
     +(+(?x_1,?x),+(?x_8,+(?y_8,?z))) = +(?x_1,+(+(?x,+(?x_8,?y_8)),?z)),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     *(E(?x),E(+(+(?y,?y_1),?z_1))) = E(+(+(?x,?y),+(?y_1,?z_1))),
     *(E(?x),E(?y)) = E(+(+(?x,?y),0)),
     *(E(?x),E(?z)) = E(+(+(?x,0),?z)),
     *(E(?x),E(+(?x_7,+(?y_7,?z)))) = E(+(+(?x,+(?x_7,?y_7)),?z)),
     *(E(?x),E(+(?z,?y))) = E(+(+(?x,?y),?z)),
     +(?x,+(+(+(?y,?y_8),?z_8),?z_7)) = +(+(+(?x,?y),+(?y_8,?z_8)),?z_7),
     +(?x,+(?z,?z_7)) = +(+(+(?x,0),?z),?z_7),
     +(?x,+(+(?x_14,+(?y_14,?z)),?z_7)) = +(+(+(?x,+(?x_14,?y_14)),?z),?z_7),
     +(?x,+(+(?z,?y),?z_7)) = +(+(+(?x,?y),?z),?z_7),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     *(E(?x),E(+(?y,?z))) = E(+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_7)) = +(+(+(?x,?y),?z),?z_7),
     ?x = +(0,?x),
     ?y = +(?y,0),
     +(?x_6,+(?y_6,?y)) = +(?y,+(?x_6,?y_6)),
     +(+(?x,?y_7),?z_7) = +(+(?y_7,?z_7),?x),
     *(E(?x),E(?y)) = E(+(?y,?x)),
     +(?x,+(?y,?z_7)) = +(+(?y,?x),?z_7),
     +(+(?x_8,?x),?y) = +(?x_8,+(?y,?x)),
     *(?x_1,*(?y_1,?y)) = *(*(?x_1,?y_1),*(?y,1)),
     ?x = *(?x,*(1,1)),
     ?y = *(1,*(?y,1)),
     *(*(?x,?y_10),?z_10) = *(?x,*(*(?y_10,?z_10),1)),
     *(?y,?x) = *(?x,*(?y,1)),
     *(*(*(?x_10,*(?y_10,?y)),?y_9),?z_9) = *(*(?x_10,?y_10),*(?y,*(?y_9,?z_9))),
     *(*(?x,?y_9),?z_9) = *(?x,*(1,*(?y_9,?z_9))),
     *(*(?y,?y_9),?z_9) = *(1,*(?y,*(?y_9,?z_9))),
     *(*(*(*(?x,?y_19),?z_19),?y_9),?z_9) = *(?x,*(*(?y_19,?z_19),*(?y_9,?z_9))),
     *(*(*(?y,?x),?y_9),?z_9) = *(?x,*(?y,*(?y_9,?z_9))),
     *(?z,*(?x_1,*(?y_1,?y))) = *(*(?x_1,?y_1),*(?y,?z)),
     *(?z,?x) = *(?x,*(1,?z)),
     *(?z,?y) = *(1,*(?y,?z)),
     *(?z,*(*(?x,?y_10),?z_10)) = *(?x,*(*(?y_10,?z_10),?z)),
     *(?z,*(?y,?x)) = *(?x,*(?y,?z)),
     *(?x,?y) = *(?x,*(?y,1)),
     *(*(*(?x,?y),?y_9),?z_9) = *(?x,*(?y,*(?y_9,?z_9))),
     *(?z,*(?x,?y)) = *(?x,*(?y,?z)),
     *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)),
     *(?x,?z) = *(?x,*(1,?z)),
     *(?y,?z) = *(1,*(?y,?z)),
     *(*(*(?x,?y_10),?z_10),?z) = *(?x,*(*(?y_10,?z_10),?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,*(1,?z)),?z_1),
     *(?y,*(?z,?z_1)) = *(*(1,*(?y,?z)),?z_1),
     *(*(*(?x,?y_11),?z_11),*(?z,?z_1)) = *(*(?x,*(*(?y_11,?z_11),?z)),?z_1),
     *(*(?y,?x),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(*(?x_10,*(?x_11,*(?y_11,?y))),?z) = *(?x_10,*(*(?x_11,?y_11),*(?y,?z))),
     *(*(?x_10,?x),?z) = *(?x_10,*(?x,*(1,?z))),
     *(*(?x_10,*(*(?x,?y_20),?z_20)),?z) = *(?x_10,*(?x,*(*(?y_20,?z_20),?z))),
     *(*(?x_10,*(?y,?x)),?z) = *(?x_10,*(?x,*(?y,?z))),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(*(?x_10,*(?x,?y)),?z) = *(?x_10,*(?x,*(?y,?z))),
     *(*(?y,?y_1),?z_1) = *(*(1,?y),*(?y_1,?z_1)),
     ?y = *(*(1,?y),1),
     ?z = *(*(1,1),?z),
     *(?z,?y) = *(*(1,?y),?z),
     *(?x_9,*(?y_9,*(*(?y,?y_10),?z_10))) = *(*(*(?x_9,?y_9),?y),*(?y_10,?z_10)),
     *(?x_9,*(?y_9,?y)) = *(*(*(?x_9,?y_9),?y),1),
     *(?x_9,*(?y_9,?z)) = *(*(*(?x_9,?y_9),1),?z),
     *(?x_9,*(?y_9,*(?x_19,*(?y_19,?z)))) = *(*(*(?x_9,?y_9),*(?x_19,?y_19)),?z),
     *(?x_9,*(?y_9,*(?z,?y))) = *(*(*(?x_9,?y_9),?y),?z),
     *(*(*(?y,?y_1),?z_1),?x) = *(*(?x,?y),*(?y_1,?z_1)),
     *(?y,?x) = *(*(?x,?y),1),
     *(?z,?x) = *(*(?x,1),?z),
     *(*(?x_10,*(?y_10,?z)),?x) = *(*(?x,*(?x_10,?y_10)),?z),
     *(*(?z,?y),?x) = *(*(?x,?y),?z),
     *(?y,?z) = *(*(1,?y),?z),
     *(?x_9,*(?y_9,*(?y,?z))) = *(*(*(?x_9,?y_9),?y),?z),
     *(*(?y,?z),?x) = *(*(?x,?y),?z),
     *(?x,*(*(?y,?y_1),?z_1)) = *(*(?x,?y),*(?y_1,?z_1)),
     *(?x,?y) = *(*(?x,?y),1),
     *(?x,?z) = *(*(?x,1),?z),
     *(?x,*(?x_10,*(?y_10,?z))) = *(*(?x,*(?x_10,?y_10)),?z),
     *(?x,*(?z,?y)) = *(*(?x,?y),?z),
     *(*(?x_1,?x),*(*(?y,?y_2),?z_2)) = *(?x_1,*(*(?x,?y),*(?y_2,?z_2))),
     *(*(?x_1,?x),?z) = *(?x_1,*(*(?x,1),?z)),
     *(*(?x_1,?x),*(?x_11,*(?y_11,?z))) = *(?x_1,*(*(?x,*(?x_11,?y_11)),?z)),
     *(*(?x_1,?x),*(?z,?y)) = *(?x_1,*(*(?x,?y),?z)),
     *(?x,*(*(*(?y,?y_11),?z_11),?z_10)) = *(*(*(?x,?y),*(?y_11,?z_11)),?z_10),
     *(?x,*(?z,?z_10)) = *(*(*(?x,1),?z),?z_10),
     *(?x,*(*(?x_20,*(?y_20,?z)),?z_10)) = *(*(*(?x,*(?x_20,?y_20)),?z),?z_10),
     *(?x,*(*(?z,?y),?z_10)) = *(*(*(?x,?y),?z),?z_10),
     *(*(?x_1,?x),*(?y,?z)) = *(?x_1,*(*(?x,?y),?z)),
     *(?x,*(*(?y,?z),?z_10)) = *(*(*(?x,?y),?z),?z_10),
     ?x = *(1,?x),
     ?y = *(?y,1),
     *(?x_9,*(?y_9,?y)) = *(?y,*(?x_9,?y_9)),
     *(*(?x,?y_10),?z_10) = *(*(?y_10,?z_10),?x),
     *(?x,*(?y,?z_10)) = *(*(?y,?x),?z_10),
     *(*(?x_11,?x),?y) = *(?x_11,*(?y,?x)) ]
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 <E(?x_1), *(E(?x_1),E(0))> by Rules <2, 0> preceded by [(E,1)]
 joinable by a reduction of rules <[], [([(*,2)],1),([],4)]>
Critical Pair <E(?x_2), *(E(0),E(?x_2))> by Rules <3, 0> preceded by [(E,1)]
 joinable by a reduction of rules <[], [([(*,1)],1),([],5)]>
Critical Pair <E(+(?x_5,+(?y_5,?z_5))), *(E(+(?x_5,?y_5)),E(?z_5))> by Rules <6, 0> preceded by [(E,1)]
 joinable by a reduction of rules <[([(E,1)],7),([],0)], []>
 joinable by a reduction of rules <[([],0),([(*,2)],0)], [([(*,1)],0),([],9)]>
Critical Pair <E(+(+(?x_6,?y_6),?z_6)), *(E(?x_6),E(+(?y_6,?z_6)))> by Rules <7, 0> preceded by [(E,1)]
 joinable by a reduction of rules <[([(E,1)],6),([],0)], []>
 joinable by a reduction of rules <[([],0),([(*,1)],0)], [([(*,2)],0),([],10)]>
Critical Pair <E(+(?y_7,?x_7)), *(E(?x_7),E(?y_7))> by Rules <8, 0> preceded by [(E,1)]
 joinable by a reduction of rules <[([],0)], [([],11)]>
Critical Pair <+(?x_1,?z_5), +(?x_1,+(0,?z_5))> by Rules <2, 6> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([(+,2)],3)]>
Critical Pair <+(?x_2,?z_5), +(0,+(?x_2,?z_5))> by Rules <3, 6> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <+(+(+(?x_6,?y_6),?z_6),?z_5), +(?x_6,+(+(?y_6,?z_6),?z_5))> by Rules <7, 6> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],6)], [([],7)]>
Critical Pair <+(+(?y_7,?x_7),?z_5), +(?x_7,+(?y_7,?z_5))> by Rules <8, 6> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],8)], [([],7)]>
Critical Pair <+(?x_6,?x_1), +(+(?x_6,?x_1),0)> by Rules <2, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <+(?x_6,?x_2), +(+(?x_6,0),?x_2)> by Rules <3, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],2)]>
Critical Pair <+(?x_6,+(?x_5,+(?y_5,?z_5))), +(+(?x_6,+(?x_5,?y_5)),?z_5)> by Rules <6, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],7)], [([],6)]>
Critical Pair <+(?x_6,+(?y_7,?x_7)), +(+(?x_6,?x_7),?y_7)> by Rules <8, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],8)], [([],6)]>
Critical Pair <*(?x_3,?z_8), *(?x_3,*(1,?z_8))> by Rules <4, 9> preceded by [(*,1)]
 joinable by a reduction of rules <[], [([(*,2)],5)]>
Critical Pair <*(?x_4,?z_8), *(1,*(?x_4,?z_8))> by Rules <5, 9> preceded by [(*,1)]
 joinable by a reduction of rules <[], [([],5)]>
Critical Pair <*(*(*(?x_9,?y_9),?z_9),?z_8), *(?x_9,*(*(?y_9,?z_9),?z_8))> by Rules <10, 9> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],9)], [([],10)]>
Critical Pair <*(*(?y_10,?x_10),?z_8), *(?x_10,*(?y_10,?z_8))> by Rules <11, 9> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],11)], [([],10)]>
Critical Pair <*(?x_9,?x_3), *(*(?x_9,?x_3),1)> by Rules <4, 10> preceded by [(*,2)]
 joinable by a reduction of rules <[], [([],4)]>
Critical Pair <*(?x_9,?x_4), *(*(?x_9,1),?x_4)> by Rules <5, 10> preceded by [(*,2)]
 joinable by a reduction of rules <[], [([(*,1)],4)]>
Critical Pair <*(?x_9,*(?x_8,*(?y_8,?z_8))), *(*(?x_9,*(?x_8,?y_8)),?z_8)> by Rules <9, 10> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],10)], [([],9)]>
Critical Pair <*(?x_9,*(?y_10,?x_10)), *(*(?x_9,?x_10),?y_10)> by Rules <11, 10> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],11)], [([],9)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <6, 6> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],7)], [([],7)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <7, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],6)], [([],6)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <9, 9> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],10)], [([],10)]>
Critical Pair <*(?x_1,*(*(?x,?y),?z)), *(*(?x_1,?x),*(?y,?z))> by Rules <10, 10> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],9)], [([],9)]>
Critical Pair <0, 0> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <+(?x_5,+(?y_5,0)), +(?x_5,?y_5)> by Rules <6, 2> preceded by []
 joinable by a reduction of rules <[([(+,2)],2)], []>
Critical Pair <+(0,?x_7), ?x_7> by Rules <8, 2> preceded by []
 joinable by a reduction of rules <[([],3)], []>
Critical Pair <+(+(0,?y_6),?z_6), +(?y_6,?z_6)> by Rules <7, 3> preceded by []
 joinable by a reduction of rules <[([(+,1)],3)], []>
Critical Pair <+(?y_7,0), ?y_7> by Rules <8, 3> preceded by []
 joinable by a reduction of rules <[([],2)], []>
Critical Pair <1, 1> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <*(?x_8,*(?y_8,1)), *(?x_8,?y_8)> by Rules <9, 4> preceded by []
 joinable by a reduction of rules <[([(*,2)],4)], []>
Critical Pair <*(1,?x_10), ?x_10> by Rules <11, 4> preceded by []
 joinable by a reduction of rules <[([],5)], []>
Critical Pair <*(*(1,?y_9),?z_9), *(?y_9,?z_9)> by Rules <10, 5> preceded by []
 joinable by a reduction of rules <[([(*,1)],5)], []>
Critical Pair <*(?y_10,1), ?y_10> by Rules <11, 5> preceded by []
 joinable by a reduction of rules <[([],4)], []>
Critical Pair <+(+(+(?x_5,?y_5),?y_6),?z_6), +(?x_5,+(?y_5,+(?y_6,?z_6)))> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([],6)], [([],7)]>
Critical Pair <+(?y_7,+(?x_5,?y_5)), +(?x_5,+(?y_5,?y_7))> by Rules <8, 6> preceded by []
 joinable by a reduction of rules <[([],8)], [([],7)]>
Critical Pair <+(+(?y_6,?z_6),?x_7), +(+(?x_7,?y_6),?z_6)> by Rules <8, 7> preceded by []
 joinable by a reduction of rules <[([],8)], [([],6)]>
Critical Pair <*(*(*(?x_8,?y_8),?y_9),?z_9), *(?x_8,*(?y_8,*(?y_9,?z_9)))> by Rules <10, 9> preceded by []
 joinable by a reduction of rules <[([],9)], [([],10)]>
Critical Pair <*(?y_10,*(?x_8,?y_8)), *(?x_8,*(?y_8,?y_10))> by Rules <11, 9> preceded by []
 joinable by a reduction of rules <[([],11)], [([],10)]>
Critical Pair <*(*(?y_9,?z_9),?x_10), *(*(?x_10,?y_9),?z_9)> by Rules <11, 10> preceded by []
 joinable by a reduction of rules <[([],11)], [([],9)]>
Satisfiable by 9,8,7>3>4,2>1>12,11,10>6>5; *(0,0)+(0,0)E(0); 1>9,8,7>12,11,10,4>2>3>5>6
Diagram Decreasing
Direct Methods: CR

Combined result: CR
530.trs: Success(CR)
YES
(22 msec.)