Problem:
 +(+(x,y),z) -> +(x,+(y,z))
 +(x,y) -> +(y,x)
 *(*(x,y),z) -> *(x,*(y,z))
 *(x,y) -> *(y,x)
 *(+(x,y),z) -> +(*(x,z),*(y,z))
 *(x,+(y,z)) -> +(*(x,y),*(x,z))

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 22
   +(+(x163,+(x164,y)),z) <-0|0[]- +(+(+(x163,x164),y),z) -0|[]-> +(+(x163,x164),+(y,z))
   +(x166,+(x167,y)) <-0|[]- +(+(x166,x167),y) -1|[]-> +(y,+(x166,x167))
   *(+(x169,+(x170,y)),z) <-0|0[]- *(+(+(x169,x170),y),z) -4|[]-> +(*(+(x169,x170),z),*(y,z))
   *(x,+(x172,+(x173,z))) <-0|1[]- *(x,+(+(x172,x173),z)) -5|[]-> +(*(x,+(x172,x173)),*(x,z))
   +(z,+(x,y)) <-1|[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
   +(+(y,x),z) <-1|0[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
   *(+(y,x),z) <-1|0[]- *(+(x,y),z) -4|[]-> +(*(x,z),*(y,z))
   *(x,+(z,y)) <-1|1[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z))
   *(*(x183,*(x184,y)),z) <-2|0[]- *(*(*(x183,x184),y),z) -2|[]-> *(*(x183,x184),*(y,z))
   *(x186,*(x187,y)) <-2|[]- *(*(x186,x187),y) -3|[]-> *(y,*(x186,x187))
   *(x189,*(x190,+(y,z))) <-2|[]- *(*(x189,x190),+(y,z)) -5|[]-> +(*(*(x189,x190),y),
                                                                   *(*(x189,x190),z))
   *(z,*(x,y)) <-3|[]- *(*(x,y),z) -2|[]-> *(x,*(y,z))
   *(*(y,x),z) <-3|0[]- *(*(x,y),z) -2|[]-> *(x,*(y,z))
   *(z,+(x,y)) <-3|[]- *(+(x,y),z) -4|[]-> +(*(x,z),*(y,z))
   *(+(y,z),x) <-3|[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z))
   *(+(*(x200,y),*(x201,y)),z) <-4|0[]- *(*(+(x200,x201),y),z) -2|[]-> *(+(x200,x201),*(y,z))
   +(*(x203,y),*(x204,y)) <-4|[]- *(+(x203,x204),y) -3|[]-> *(y,+(x203,x204))
   +(*(x206,+(y,z)),*(x207,+(y,z))) <-4|[]- *(+(x206,x207),+(y,z)) -5|
                                            []-> +(*(+(x206,x207),y),*(+(x206,x207),z))
   +(*(*(x,y),x210),*(*(x,y),x211)) <-5|[]- *(*(x,y),+(x210,x211)) -2|[]-> *(x,*(y,+(x210,x211)))
   *(+(*(x,x213),*(x,x214)),z) <-5|0[]- *(*(x,+(x213,x214)),z) -2|[]-> *(x,*(+(x213,x214),z))
   +(*(x,x216),*(x,x217)) <-5|[]- *(x,+(x216,x217)) -3|[]-> *(+(x216,x217),x)
   +(*(+(x,y),x219),*(+(x,y),x220)) <-5|[]- *(+(x,y),+(x219,x220)) -4|
                                            []-> +(*(x,+(x219,x220)),*(y,+(x219,x220)))
  Redundant Rules Transformation:
   +(+(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))
   Church Rosser Transformation Processor (ac):
    f5_AC(x,f3_AC(y,z)) -> f3_AC(f5_AC(x,y),f5_AC(x,z))
    AC critical peaks: joinable
    AC-RPO Processor:
     precedence:
      f5_AC > f3_AC
     status:
      
     problem:
      
     Qed