YES

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

Proof:
 Church Rosser Transformation Processor (star):
  strict:
   *(1)(x330) -> +(0)(*(1)(x330))
   *(1)(x330) -> +(1)(x330)
   *(0)(x331) -> +(0)(x331)
   *(0)(x331) -> +(1)(*(0)(x331))
  weak:
   *(0)(s(0)(x329)) -> +(0)(*(0)(x329))
   *(1)(s(0)(x332)) -> +(1)(*(1)(x332))
   +(0)(x333) -> +(0)(+(0)(x333))
   +(1)(+(0)(x334)) -> +(0)(+(1)(x334))
   +(1)(+(1)(x335)) -> +(1)(x335)
   +(0)(+(0)(x336)) -> +(0)(x336)
   +(0)(+(1)(x337)) -> +(1)(+(0)(x337))
   +(1)(x338) -> +(1)(+(1)(x338))
   +(0)(x339) -> +(0)(s(0)(x339))
   +(1)(s(0)(x340)) -> +(1)(x340)
   +(0)(s(0)(x341)) -> +(0)(x341)
   +(1)(x342) -> +(1)(s(0)(x342))
   +(0)(x343) -> +(1)(x343)
   +(1)(x344) -> +(0)(x344)
   *(0)(x345) -> *(1)(x345)
   *(1)(x346) -> *(0)(x346)
  critical peaks: 32
   *(s(y),x) <-0|[]- *(x,s(y)) -6|[]-> +(x,*(x,y))
   *(y,s(x)) <-0|[]- *(s(x),y) -7|[]-> +(*(x,y),y)
   +(y,s(x)) <-1|[]- +(s(x),y) -2|[]-> +(x,s(y))
   +(s(y),x) <-1|[]- +(x,s(y)) -3|[]-> +(s(x),y)
   +(z,+(x,y)) <-1|[]- +(+(x,y),z) -4|[]-> +(x,+(y,z))
   +(+(y,x),z) <-1|0[]- +(+(x,y),z) -4|[]-> +(x,+(y,z))
   +(+(y,z),x) <-1|[]- +(x,+(y,z)) -5|[]-> +(+(x,y),z)
   +(x,+(z,y)) <-1|1[]- +(x,+(y,z)) -5|[]-> +(+(x,y),z)
   +(x271,s(y)) <-2|[]- +(s(x271),y) -1|[]-> +(y,s(x271))
   +(x273,s(s(y))) <-2|[]- +(s(x273),s(y)) -3|[]-> +(s(s(x273)),y)
   +(+(x275,s(y)),z) <-2|0[]- +(+(s(x275),y),z) -4|[]-> +(s(x275),+(y,z))
   +(x277,s(+(y,z))) <-2|[]- +(s(x277),+(y,z)) -5|[]-> +(+(s(x277),y),z)
   +(x,+(x279,s(z))) <-2|1[]- +(x,+(s(x279),z)) -5|[]-> +(+(x,s(x279)),z)
   +(s(x),x282) <-3|[]- +(x,s(x282)) -1|[]-> +(s(x282),x)
   +(s(s(x)),x284) <-3|[]- +(s(x),s(x284)) -2|[]-> +(x,s(s(x284)))
   +(s(+(x,y)),x286) <-3|[]- +(+(x,y),s(x286)) -4|[]-> +(x,+(y,s(x286)))
   +(+(s(x),x288),z) <-3|0[]- +(+(x,s(x288)),z) -4|[]-> +(x,+(s(x288),z))
   +(x,+(s(y),x290)) <-3|1[]- +(x,+(y,s(x290))) -5|[]-> +(+(x,y),s(x290))
   +(x291,+(x292,y)) <-4|[]- +(+(x291,x292),y) -1|[]-> +(y,+(x291,x292))
   +(x294,+(x295,s(y))) <-4|[]- +(+(x294,x295),s(y)) -3|[]-> +(s(+(x294,x295)),y)
   +(+(x297,+(x298,y)),z) <-4|0[]- +(+(+(x297,x298),y),z) -4|[]-> +(+(x297,x298),+(y,z))
   +(x300,+(x301,+(y,z))) <-4|[]- +(+(x300,x301),+(y,z)) -5|[]-> +(+(+(x300,x301),y),z)
   +(x,+(x303,+(x304,z))) <-4|1[]- +(x,+(+(x303,x304),z)) -5|[]-> +(+(x,+(x303,x304)),z)
   +(+(x,x307),x308) <-5|[]- +(x,+(x307,x308)) -1|[]-> +(+(x307,x308),x)
   +(+(s(x),x310),x311) <-5|[]- +(s(x),+(x310,x311)) -2|[]-> +(x,s(+(x310,x311)))
   +(+(+(x,y),x313),x314) <-5|[]- +(+(x,y),+(x313,x314)) -4|[]-> +(x,+(y,+(x313,x314)))
   +(+(+(x,x316),x317),z) <-5|0[]- +(+(x,+(x316,x317)),z) -4|[]-> +(x,+(+(x316,x317),z))
   +(x,+(+(y,x319),x320)) <-5|1[]- +(x,+(y,+(x319,x320))) -5|[]-> +(+(x,y),+(x319,x320))
   +(x,*(x,x322)) <-6|[]- *(x,s(x322)) -0|[]-> *(s(x322),x)
   +(s(x),*(s(x),x324)) <-6|[]- *(s(x),s(x324)) -7|[]-> +(*(x,s(x324)),s(x324))
   +(*(x325,y),y) <-7|[]- *(s(x325),y) -0|[]-> *(y,s(x325))
   +(*(x327,s(y)),s(y)) <-7|[]- *(s(x327),s(y)) -6|[]-> +(s(x327),*(s(x327),y))
  Matrix Interpretation Processor: dim=1, star lab=right 
   
   interpretation:
    [s(0)](x0) = x0,
    
    [*(0)](x0) = x0 + 1,
    
    [+(0)](x0) = x0,
    
    [+(1)](x0) = x0,
    
    [*(1)](x0) = x0 + 1
   orientation:
    *(1)(x330) = x330 + 1 >= x330 + 1 = +(0)(*(1)(x330))
    
    *(1)(x330) = x330 + 1 >= x330 = +(1)(x330)
    
    *(0)(x331) = x331 + 1 >= x331 = +(0)(x331)
    
    *(0)(x331) = x331 + 1 >= x331 + 1 = +(1)(*(0)(x331))
    
    *(0)(s(0)(x329)) = x329 + 1 >= x329 + 1 = +(0)(*(0)(x329))
    
    *(1)(s(0)(x332)) = x332 + 1 >= x332 + 1 = +(1)(*(1)(x332))
    
    +(0)(x333) = x333 >= x333 = +(0)(+(0)(x333))
    
    +(1)(+(0)(x334)) = x334 >= x334 = +(0)(+(1)(x334))
    
    +(1)(+(1)(x335)) = x335 >= x335 = +(1)(x335)
    
    +(0)(+(0)(x336)) = x336 >= x336 = +(0)(x336)
    
    +(0)(+(1)(x337)) = x337 >= x337 = +(1)(+(0)(x337))
    
    +(1)(x338) = x338 >= x338 = +(1)(+(1)(x338))
    
    +(0)(x339) = x339 >= x339 = +(0)(s(0)(x339))
    
    +(1)(s(0)(x340)) = x340 >= x340 = +(1)(x340)
    
    +(0)(s(0)(x341)) = x341 >= x341 = +(0)(x341)
    
    +(1)(x342) = x342 >= x342 = +(1)(s(0)(x342))
    
    +(0)(x343) = x343 >= x343 = +(1)(x343)
    
    +(1)(x344) = x344 >= x344 = +(0)(x344)
    
    *(0)(x345) = x345 + 1 >= x345 + 1 = *(1)(x345)
    
    *(1)(x346) = x346 + 1 >= x346 + 1 = *(0)(x346)
   problem:
    strict:
     *(1)(x330) -> +(0)(*(1)(x330))
     *(0)(x331) -> +(1)(*(0)(x331))
    weak:
     *(0)(s(0)(x329)) -> +(0)(*(0)(x329))
     *(1)(s(0)(x332)) -> +(1)(*(1)(x332))
     +(0)(x333) -> +(0)(+(0)(x333))
     +(1)(+(0)(x334)) -> +(0)(+(1)(x334))
     +(1)(+(1)(x335)) -> +(1)(x335)
     +(0)(+(0)(x336)) -> +(0)(x336)
     +(0)(+(1)(x337)) -> +(1)(+(0)(x337))
     +(1)(x338) -> +(1)(+(1)(x338))
     +(0)(x339) -> +(0)(s(0)(x339))
     +(1)(s(0)(x340)) -> +(1)(x340)
     +(0)(s(0)(x341)) -> +(0)(x341)
     +(1)(x342) -> +(1)(s(0)(x342))
     +(0)(x343) -> +(1)(x343)
     +(1)(x344) -> +(0)(x344)
     *(0)(x345) -> *(1)(x345)
     *(1)(x346) -> *(0)(x346)
   Matrix Interpretation Processor: dim=2, star lab=right 
    
    interpretation:
                       [0]
     [s(0)](x0) = x0 + [2],
     
                  [1 1]     [0]
     [*(0)](x0) = [0 0]x0 + [1],
     
                  [1 0]  
     [+(0)](x0) = [0 0]x0,
     
                  [1 0]  
     [+(1)](x0) = [0 0]x0,
     
                  [1 1]     [0]
     [*(1)](x0) = [0 0]x0 + [1]
    orientation:
                  [1 1]       [0]    [1 1]                       
     *(1)(x330) = [0 0]x330 + [1] >= [0 0]x330 = +(0)(*(1)(x330))
     
                  [1 1]       [0]    [1 1]                       
     *(0)(x331) = [0 0]x331 + [1] >= [0 0]x331 = +(1)(*(0)(x331))
     
                        [1 1]       [2]    [1 1]                       
     *(0)(s(0)(x329)) = [0 0]x329 + [1] >= [0 0]x329 = +(0)(*(0)(x329))
     
                        [1 1]       [2]    [1 1]                       
     *(1)(s(0)(x332)) = [0 0]x332 + [1] >= [0 0]x332 = +(1)(*(1)(x332))
     
                  [1 0]        [1 0]                       
     +(0)(x333) = [0 0]x333 >= [0 0]x333 = +(0)(+(0)(x333))
     
                        [1 0]        [1 0]                       
     +(1)(+(0)(x334)) = [0 0]x334 >= [0 0]x334 = +(0)(+(1)(x334))
     
                        [1 0]        [1 0]                 
     +(1)(+(1)(x335)) = [0 0]x335 >= [0 0]x335 = +(1)(x335)
     
                        [1 0]        [1 0]                 
     +(0)(+(0)(x336)) = [0 0]x336 >= [0 0]x336 = +(0)(x336)
     
                        [1 0]        [1 0]                       
     +(0)(+(1)(x337)) = [0 0]x337 >= [0 0]x337 = +(1)(+(0)(x337))
     
                  [1 0]        [1 0]                       
     +(1)(x338) = [0 0]x338 >= [0 0]x338 = +(1)(+(1)(x338))
     
                  [1 0]        [1 0]                       
     +(0)(x339) = [0 0]x339 >= [0 0]x339 = +(0)(s(0)(x339))
     
                        [1 0]        [1 0]                 
     +(1)(s(0)(x340)) = [0 0]x340 >= [0 0]x340 = +(1)(x340)
     
                        [1 0]        [1 0]                 
     +(0)(s(0)(x341)) = [0 0]x341 >= [0 0]x341 = +(0)(x341)
     
                  [1 0]        [1 0]                       
     +(1)(x342) = [0 0]x342 >= [0 0]x342 = +(1)(s(0)(x342))
     
                  [1 0]        [1 0]                 
     +(0)(x343) = [0 0]x343 >= [0 0]x343 = +(1)(x343)
     
                  [1 0]        [1 0]                 
     +(1)(x344) = [0 0]x344 >= [0 0]x344 = +(0)(x344)
     
                  [1 1]       [0]    [1 1]       [0]             
     *(0)(x345) = [0 0]x345 + [1] >= [0 0]x345 + [1] = *(1)(x345)
     
                  [1 1]       [0]    [1 1]       [0]             
     *(1)(x346) = [0 0]x346 + [1] >= [0 0]x346 + [1] = *(0)(x346)
    problem:
     strict:
      *(1)(x330) -> +(0)(*(1)(x330))
      *(0)(x331) -> +(1)(*(0)(x331))
     weak:
      +(0)(x333) -> +(0)(+(0)(x333))
      +(1)(+(0)(x334)) -> +(0)(+(1)(x334))
      +(1)(+(1)(x335)) -> +(1)(x335)
      +(0)(+(0)(x336)) -> +(0)(x336)
      +(0)(+(1)(x337)) -> +(1)(+(0)(x337))
      +(1)(x338) -> +(1)(+(1)(x338))
      +(0)(x339) -> +(0)(s(0)(x339))
      +(1)(s(0)(x340)) -> +(1)(x340)
      +(0)(s(0)(x341)) -> +(0)(x341)
      +(1)(x342) -> +(1)(s(0)(x342))
      +(0)(x343) -> +(1)(x343)
      +(1)(x344) -> +(0)(x344)
      *(0)(x345) -> *(1)(x345)
      *(1)(x346) -> *(0)(x346)
    Shift Processor (**) lab=left:
     strict:
      
     weak:
      
     Shift Processor lab=left (dd):
      strict:
       *(x,s(y)) -> *(s(y),x)
       *(x,s(y)) -> +(x,*(x,y))
       *(s(y),x) -> +(*(y,x),x)
       +(x,*(x,y)) -> +(x,*(y,x))
       +(x,*(y,x)) -> +(*(y,x),x)
       *(s(y),x) -> +(*(y,x),x)
       +(x,*(x,y)) -> +(*(x,y),x)
       +(*(x,y),x) -> +(*(y,x),x)
       *(s(y),x) -> *(x,s(y))
       *(x,s(y)) -> +(x,*(x,y))
       *(s(y),x) -> +(*(y,x),x)
       +(*(y,x),x) -> +(*(x,y),x)
       +(x,*(x,y)) -> +(*(x,y),x)
       *(s(y),x) -> +(*(y,x),x)
       +(*(y,x),x) -> +(x,*(y,x))
       +(x,*(x,y)) -> +(x,*(y,x))
       *(s(x),y) -> *(y,s(x))
       *(s(x),y) -> +(*(x,y),y)
       *(y,s(x)) -> +(y,*(y,x))
       +(*(x,y),y) -> +(*(y,x),y)
       +(*(y,x),y) -> +(y,*(y,x))
       *(y,s(x)) -> +(y,*(y,x))
       +(*(x,y),y) -> +(y,*(x,y))
       +(y,*(x,y)) -> +(y,*(y,x))
       *(y,s(x)) -> *(s(x),y)
       *(s(x),y) -> +(*(x,y),y)
       *(y,s(x)) -> +(y,*(y,x))
       +(y,*(y,x)) -> +(y,*(x,y))
       +(*(x,y),y) -> +(y,*(x,y))
       *(y,s(x)) -> +(y,*(y,x))
       +(y,*(y,x)) -> +(*(y,x),y)
       +(*(x,y),y) -> +(*(y,x),y)
       +(s(x),y) -> +(y,s(x))
       +(s(x),y) -> +(x,s(y))
       +(y,s(x)) -> +(s(x),y)
       +(x,s(y)) -> +(s(x),y)
       +(y,s(x)) -> +(s(y),x)
       +(x,s(y)) -> +(s(y),x)
       +(x,s(y)) -> +(s(y),x)
       +(x,s(y)) -> +(s(x),y)
       +(s(y),x) -> +(x,s(y))
       +(s(x),y) -> +(x,s(y))
       +(s(y),x) -> +(y,s(x))
       +(s(x),y) -> +(y,s(x))
       +(+(x,y),z) -> +(z,+(x,y))
       +(+(x,y),z) -> +(x,+(y,z))
       +(z,+(x,y)) -> +(+(x,y),z)
       +(x,+(y,z)) -> +(+(x,y),z)
       +(+(x,y),z) -> +(+(y,x),z)
       +(+(x,y),z) -> +(x,+(y,z))
       +(+(y,x),z) -> +(+(x,y),z)
       +(x,+(y,z)) -> +(+(x,y),z)
       +(x,+(y,z)) -> +(+(y,z),x)
       +(x,+(y,z)) -> +(+(x,y),z)
       +(+(y,z),x) -> +(x,+(y,z))
       +(+(x,y),z) -> +(x,+(y,z))
       +(x,+(y,z)) -> +(x,+(z,y))
       +(x,+(y,z)) -> +(+(x,y),z)
       +(x,+(z,y)) -> +(x,+(y,z))
       +(+(x,y),z) -> +(x,+(y,z))
       +(s(x271),y) -> +(x271,s(y))
       +(s(x271),y) -> +(y,s(x271))
       +(x271,s(y)) -> +(s(y),x271)
       +(y,s(x271)) -> +(s(y),x271)
       +(x271,s(y)) -> +(s(x271),y)
       +(y,s(x271)) -> +(s(x271),y)
       +(s(x273),s(y)) -> +(x273,s(s(y)))
       +(s(x273),s(y)) -> +(s(s(x273)),y)
       +(x273,s(s(y))) -> +(s(x273),s(y))
       +(s(s(x273)),y) -> +(s(x273),s(y))
       +(+(s(x275),y),z) -> +(+(x275,s(y)),z)
       +(+(s(x275),y),z) -> +(s(x275),+(y,z))
       +(+(x275,s(y)),z) -> +(+(s(x275),y),z)
       +(s(x275),+(y,z)) -> +(+(s(x275),y),z)
       +(s(x277),+(y,z)) -> +(x277,s(+(y,z)))
       +(s(x277),+(y,z)) -> +(+(s(x277),y),z)
       +(x277,s(+(y,z))) -> +(s(x277),+(y,z))
       +(+(s(x277),y),z) -> +(s(x277),+(y,z))
       +(x,+(s(x279),z)) -> +(x,+(x279,s(z)))
       +(x,+(s(x279),z)) -> +(+(x,s(x279)),z)
       +(x,+(x279,s(z))) -> +(x,+(s(x279),z))
       +(+(x,s(x279)),z) -> +(x,+(s(x279),z))
       +(x,s(x282)) -> +(s(x),x282)
       +(x,s(x282)) -> +(s(x282),x)
       +(s(x),x282) -> +(x282,s(x))
       +(s(x282),x) -> +(x282,s(x))
       +(s(x),x282) -> +(x,s(x282))
       +(s(x282),x) -> +(x,s(x282))
       +(s(x),s(x284)) -> +(s(s(x)),x284)
       +(s(x),s(x284)) -> +(x,s(s(x284)))
       +(s(s(x)),x284) -> +(s(x),s(x284))
       +(x,s(s(x284))) -> +(s(x),s(x284))
       +(+(x,y),s(x286)) -> +(s(+(x,y)),x286)
       +(+(x,y),s(x286)) -> +(x,+(y,s(x286)))
       +(s(+(x,y)),x286) -> +(+(x,y),s(x286))
       +(x,+(y,s(x286))) -> +(+(x,y),s(x286))
       +(+(x,s(x288)),z) -> +(+(s(x),x288),z)
       +(+(x,s(x288)),z) -> +(x,+(s(x288),z))
       +(+(s(x),x288),z) -> +(+(x,s(x288)),z)
       +(x,+(s(x288),z)) -> +(+(x,s(x288)),z)
       +(x,+(y,s(x290))) -> +(x,+(s(y),x290))
       +(x,+(y,s(x290))) -> +(+(x,y),s(x290))
       +(x,+(s(y),x290)) -> +(x,+(y,s(x290)))
       +(+(x,y),s(x290)) -> +(x,+(y,s(x290)))
       +(+(x291,x292),y) -> +(x291,+(x292,y))
       +(+(x291,x292),y) -> +(y,+(x291,x292))
       +(x291,+(x292,y)) -> +(+(x291,x292),y)
       +(y,+(x291,x292)) -> +(+(x291,x292),y)
       +(+(x294,x295),s(y)) -> +(x294,+(x295,s(y)))
       +(+(x294,x295),s(y)) -> +(s(+(x294,x295)),y)
       +(x294,+(x295,s(y))) -> +(+(x294,x295),s(y))
       +(s(+(x294,x295)),y) -> +(+(x294,x295),s(y))
       +(+(+(x297,x298),y),z) -> +(+(x297,+(x298,y)),z)
       +(+(+(x297,x298),y),z) -> +(+(x297,x298),+(y,z))
       +(+(x297,+(x298,y)),z) -> +(+(+(x297,x298),y),z)
       +(+(x297,x298),+(y,z)) -> +(+(+(x297,x298),y),z)
       +(+(x300,x301),+(y,z)) -> +(x300,+(x301,+(y,z)))
       +(+(x300,x301),+(y,z)) -> +(+(+(x300,x301),y),z)
       +(x300,+(x301,+(y,z))) -> +(+(x300,x301),+(y,z))
       +(+(+(x300,x301),y),z) -> +(+(x300,x301),+(y,z))
       +(x,+(+(x303,x304),z)) -> +(x,+(x303,+(x304,z)))
       +(x,+(+(x303,x304),z)) -> +(+(x,+(x303,x304)),z)
       +(x,+(x303,+(x304,z))) -> +(x,+(+(x303,x304),z))
       +(+(x,+(x303,x304)),z) -> +(x,+(+(x303,x304),z))
       +(x,+(x307,x308)) -> +(+(x,x307),x308)
       +(x,+(x307,x308)) -> +(+(x307,x308),x)
       +(+(x,x307),x308) -> +(x,+(x307,x308))
       +(+(x307,x308),x) -> +(x,+(x307,x308))
       +(s(x),+(x310,x311)) -> +(+(s(x),x310),x311)
       +(s(x),+(x310,x311)) -> +(x,s(+(x310,x311)))
       +(+(s(x),x310),x311) -> +(s(x),+(x310,x311))
       +(x,s(+(x310,x311))) -> +(s(x),+(x310,x311))
       +(+(x,y),+(x313,x314)) -> +(+(+(x,y),x313),x314)
       +(+(x,y),+(x313,x314)) -> +(x,+(y,+(x313,x314)))
       +(+(+(x,y),x313),x314) -> +(+(x,y),+(x313,x314))
       +(x,+(y,+(x313,x314))) -> +(+(x,y),+(x313,x314))
       +(+(x,+(x316,x317)),z) -> +(+(+(x,x316),x317),z)
       +(+(x,+(x316,x317)),z) -> +(x,+(+(x316,x317),z))
       +(+(+(x,x316),x317),z) -> +(+(x,+(x316,x317)),z)
       +(x,+(+(x316,x317),z)) -> +(+(x,+(x316,x317)),z)
       +(x,+(y,+(x319,x320))) -> +(x,+(+(y,x319),x320))
       +(x,+(y,+(x319,x320))) -> +(+(x,y),+(x319,x320))
       +(x,+(+(y,x319),x320)) -> +(x,+(y,+(x319,x320)))
       +(+(x,y),+(x319,x320)) -> +(x,+(y,+(x319,x320)))
       *(x,s(x322)) -> +(x,*(x,x322))
       *(x,s(x322)) -> *(s(x322),x)
       *(s(x322),x) -> *(x,s(x322))
       *(x,s(x322)) -> +(x,*(x,x322))
       +(x,*(x,x322)) -> +(x,*(x322,x))
       *(s(x322),x) -> +(*(x322,x),x)
       +(*(x322,x),x) -> +(x,*(x322,x))
       +(x,*(x,x322)) -> +(*(x,x322),x)
       *(s(x322),x) -> +(*(x322,x),x)
       +(*(x322,x),x) -> +(*(x,x322),x)
       +(x,*(x,x322)) -> +(x,*(x322,x))
       +(x,*(x322,x)) -> +(*(x322,x),x)
       *(s(x322),x) -> +(*(x322,x),x)
       +(x,*(x,x322)) -> +(*(x,x322),x)
       +(*(x,x322),x) -> +(*(x322,x),x)
       *(s(x322),x) -> +(*(x322,x),x)
       *(s(x),s(x324)) -> +(s(x),*(s(x),x324))
       *(s(x),s(x324)) -> +(*(x,s(x324)),s(x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
       +(+(s(x),*(x,x324)),x324) -> +(+(x,s(*(x,x324))),x324)
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
       +(x,+(*(x,x324),s(x324))) -> +(x,+(s(*(x,x324)),x324))
       +(x,+(s(*(x,x324)),x324)) -> +(+(x,s(*(x,x324))),x324)
       +(s(x),*(s(x),x324)) -> +(s(x),*(x324,s(x)))
       +(s(x),*(x324,s(x))) -> +(s(x),+(x324,*(x324,x)))
       +(s(x),+(x324,*(x324,x))) -> +(+(s(x),x324),*(x324,x))
       +(+(s(x),x324),*(x324,x)) -> +(*(x324,x),+(s(x),x324))
       +(*(x,s(x324)),s(x324)) -> +(*(s(x324),x),s(x324))
       +(*(s(x324),x),s(x324)) -> +(+(*(x324,x),x),s(x324))
       +(+(*(x324,x),x),s(x324)) -> +(*(x324,x),+(x,s(x324)))
       +(*(x324,x),+(x,s(x324))) -> +(*(x324,x),+(s(x),x324))
       +(s(x),*(s(x),x324)) -> +(s(x),*(x324,s(x)))
       +(s(x),*(x324,s(x))) -> +(s(x),+(x324,*(x324,x)))
       +(s(x),+(x324,*(x324,x))) -> +(+(s(x),x324),*(x324,x))
       +(+(s(x),x324),*(x324,x)) -> +(+(x,s(x324)),*(x324,x))
       +(*(x,s(x324)),s(x324)) -> +(*(s(x324),x),s(x324))
       +(*(s(x324),x),s(x324)) -> +(+(*(x324,x),x),s(x324))
       +(+(*(x324,x),x),s(x324)) -> +(*(x324,x),+(x,s(x324)))
       +(*(x324,x),+(x,s(x324))) -> +(+(x,s(x324)),*(x324,x))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x),x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x),x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(*(x,x324),+(s(x),x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
       +(+(s(x),*(x,x324)),x324) -> +(+(*(x,x324),s(x)),x324)
       +(+(*(x,x324),s(x)),x324) -> +(*(x,x324),+(s(x),x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
       +(+(s(x),*(x,x324)),x324) -> +(x324,+(s(x),*(x,x324)))
       +(x324,+(s(x),*(x,x324))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
       +(+(s(x),*(x,x324)),x324) -> +(x324,+(s(x),*(x,x324)))
       +(x324,+(s(x),*(x,x324))) -> +(+(x324,s(x)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
       +(*(s(x),x324),s(x)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
       +(x,+(*(x,x324),s(x324))) -> +(+(*(x,x324),s(x324)),x)
       +(+(*(x,x324),s(x324)),x) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
       +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
       +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
       +(x,+(*(x,x324),s(x324))) -> +(+(*(x,x324),s(x324)),x)
       +(+(*(x,x324),s(x324)),x) -> +(*(x,x324),+(s(x324),x))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
       +(s(x324),*(x,s(x324))) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
       +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
       +(+(s(x324),x),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
       +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
       +(*(x,x324),+(x,s(x324))) -> +(+(x,s(x324)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
       +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
       +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
       +(x,+(*(x,x324),s(x324))) -> +(x,+(s(x324),*(x,x324)))
       +(x,+(s(x324),*(x,x324))) -> +(+(x,s(x324)),*(x,x324))
       +(s(x),*(s(x),x324)) -> +(s(x),+(*(x,x324),x324))
       +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
       +(+(s(x),*(x,x324)),x324) -> +(+(x,s(*(x,x324))),x324)
       +(+(x,s(*(x,x324))),x324) -> +(x,+(s(*(x,x324)),x324))
       +(*(x,s(x324)),s(x324)) -> +(+(x,*(x,x324)),s(x324))
       +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
       +(x,+(*(x,x324),s(x324))) -> +(x,+(s(*(x,x324)),x324))
       *(s(x325),y) -> +(*(x325,y),y)
       *(s(x325),y) -> *(y,s(x325))
       *(y,s(x325)) -> *(s(x325),y)
       *(s(x325),y) -> +(*(x325,y),y)
       +(*(x325,y),y) -> +(*(y,x325),y)
       *(y,s(x325)) -> +(y,*(y,x325))
       +(y,*(y,x325)) -> +(*(y,x325),y)
       +(*(x325,y),y) -> +(y,*(x325,y))
       *(y,s(x325)) -> +(y,*(y,x325))
       +(y,*(y,x325)) -> +(y,*(x325,y))
       +(*(x325,y),y) -> +(*(y,x325),y)
       +(*(y,x325),y) -> +(y,*(y,x325))
       *(y,s(x325)) -> +(y,*(y,x325))
       +(*(x325,y),y) -> +(y,*(x325,y))
       +(y,*(x325,y)) -> +(y,*(y,x325))
       *(y,s(x325)) -> +(y,*(y,x325))
       *(s(x327),s(y)) -> +(*(x327,s(y)),s(y))
       *(s(x327),s(y)) -> +(s(x327),*(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
       +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(*(x327,y)),y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
       +(+(s(x327),*(x327,y)),y) -> +(+(x327,s(*(x327,y))),y)
       +(+(x327,s(*(x327,y))),y) -> +(x327,+(s(*(x327,y)),y))
       +(*(x327,s(y)),s(y)) -> +(*(s(y),x327),s(y))
       +(*(s(y),x327),s(y)) -> +(+(*(y,x327),x327),s(y))
       +(+(*(y,x327),x327),s(y)) -> +(*(y,x327),+(x327,s(y)))
       +(*(y,x327),+(x327,s(y))) -> +(+(x327,s(y)),*(y,x327))
       +(s(x327),*(s(x327),y)) -> +(s(x327),*(y,s(x327)))
       +(s(x327),*(y,s(x327))) -> +(s(x327),+(y,*(y,x327)))
       +(s(x327),+(y,*(y,x327))) -> +(+(s(x327),y),*(y,x327))
       +(+(s(x327),y),*(y,x327)) -> +(+(x327,s(y)),*(y,x327))
       +(*(x327,s(y)),s(y)) -> +(*(s(y),x327),s(y))
       +(*(s(y),x327),s(y)) -> +(+(*(y,x327),x327),s(y))
       +(+(*(y,x327),x327),s(y)) -> +(*(y,x327),+(x327,s(y)))
       +(*(y,x327),+(x327,s(y))) -> +(*(y,x327),+(s(x327),y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),*(y,s(x327)))
       +(s(x327),*(y,s(x327))) -> +(s(x327),+(y,*(y,x327)))
       +(s(x327),+(y,*(y,x327))) -> +(+(s(x327),y),*(y,x327))
       +(+(s(x327),y),*(y,x327)) -> +(*(y,x327),+(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(+(x327,s(y)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
       +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(y),*(x327,y)))
       +(x327,+(s(y),*(x327,y))) -> +(+(x327,s(y)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
       +(x327,+(*(x327,y),s(y))) -> +(+(*(x327,y),s(y)),x327)
       +(+(*(x327,y),s(y)),x327) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
       +(x327,+(*(x327,y),s(y))) -> +(+(*(x327,y),s(y)),x327)
       +(+(*(x327,y),s(y)),x327) -> +(*(x327,y),+(s(y),x327))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
       +(s(y),*(x327,s(y))) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
       +(+(s(x327),*(x327,y)),y) -> +(y,+(s(x327),*(x327,y)))
       +(y,+(s(x327),*(x327,y))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
       +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
       +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
       +(+(s(x327),*(x327,y)),y) -> +(y,+(s(x327),*(x327,y)))
       +(y,+(s(x327),*(x327,y))) -> +(+(y,s(x327)),*(x327,y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
       +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
       +(*(s(x327),y),s(x327)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
       +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
       +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
       +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
       +(+(s(x327),y),*(x327,y)) -> +(*(x327,y),+(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
       +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
       +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
       +(+(s(x327),*(x327,y)),y) -> +(+(*(x327,y),s(x327)),y)
       +(+(*(x327,y),s(x327)),y) -> +(*(x327,y),+(s(x327),y))
       +(*(x327,s(y)),s(y)) -> +(+(x327,*(x327,y)),s(y))
       +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
       +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(*(x327,y)),y))
       +(x327,+(s(*(x327,y)),y)) -> +(+(x327,s(*(x327,y))),y)
       +(s(x327),*(s(x327),y)) -> +(s(x327),+(*(x327,y),y))
       +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
       +(+(s(x327),*(x327,y)),y) -> +(+(x327,s(*(x327,y))),y)
      weak:
       *(x,y) -> *(y,x)
       +(x,y) -> +(y,x)
       +(s(x),y) -> +(x,s(y))
       +(x,s(y)) -> +(s(x),y)
       +(+(x,y),z) -> +(x,+(y,z))
       +(x,+(y,z)) -> +(+(x,y),z)
       *(x,s(y)) -> +(x,*(x,y))
       *(s(x),y) -> +(*(x,y),y)
      Polynomial Interpretation Processor:
       dimension: 1
       interpretation:
        [+](x0, x1) = x0 + x1,
        
        [*](x0, x1) = x0x0 + 3x0x1 + 2x1x0 + x1x1 + 1,
        
        [s](x0) = x0 + 1
       orientation:
        *(x,s(y)) = 5x + x*x + 5x*y + 2y + y*y + 2 >= 5x + x*x + 5x*y + 2y + y*y + 2 = *(s(y),x)
        
        *(x,s(y)) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(x,*(x,y))
        
        *(s(y),x) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        +(x,*(x,y)) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(x,*(y,x))
        
        +(x,*(y,x)) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        *(s(y),x) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        +(x,*(x,y)) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(*(x,y),x)
        
        +(*(x,y),x) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        *(s(y),x) = 5x + x*x + 5x*y + 2y + y*y + 2 >= 5x + x*x + 5x*y + 2y + y*y + 2 = *(x,s(y))
        
        *(x,s(y)) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(x,*(x,y))
        
        *(s(y),x) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        +(*(y,x),x) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(*(x,y),x)
        
        +(x,*(x,y)) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(*(x,y),x)
        
        *(s(y),x) = 5x + x*x + 5x*y + 2y + y*y + 2 >= x + x*x + 5x*y + y*y + 1 = +(*(y,x),x)
        
        +(*(y,x),x) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(x,*(y,x))
        
        +(x,*(x,y)) = x + x*x + 5x*y + y*y + 1 >= x + x*x + 5x*y + y*y + 1 = +(x,*(y,x))
        
        *(s(x),y) = 2x + x*x + 5x*y + 5y + y*y + 2 >= 2x + x*x + 5x*y + 5y + y*y + 2 = *(y,s(x))
        
        *(s(x),y) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(*(x,y),y)
        
        *(y,s(x)) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        +(*(x,y),y) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(*(y,x),y)
        
        +(*(y,x),y) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        *(y,s(x)) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        +(*(x,y),y) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(y,*(x,y))
        
        +(y,*(x,y)) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        *(y,s(x)) = 2x + x*x + 5x*y + 5y + y*y + 2 >= 2x + x*x + 5x*y + 5y + y*y + 2 = *(s(x),y)
        
        *(s(x),y) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(*(x,y),y)
        
        *(y,s(x)) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        +(y,*(y,x)) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(y,*(x,y))
        
        +(*(x,y),y) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(y,*(x,y))
        
        *(y,s(x)) = 2x + x*x + 5x*y + 5y + y*y + 2 >= x*x + 5x*y + y + y*y + 1 = +(y,*(y,x))
        
        +(y,*(y,x)) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(*(y,x),y)
        
        +(*(x,y),y) = x*x + 5x*y + y + y*y + 1 >= x*x + 5x*y + y + y*y + 1 = +(*(y,x),y)
        
        +(s(x),y) = x + y + 1 >= x + y + 1 = +(y,s(x))
        
        +(s(x),y) = x + y + 1 >= x + y + 1 = +(x,s(y))
        
        +(y,s(x)) = x + y + 1 >= x + y + 1 = +(s(x),y)
        
        +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(x),y)
        
        +(y,s(x)) = x + y + 1 >= x + y + 1 = +(s(y),x)
        
        +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(y),x)
        
        +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(y),x)
        
        +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(x),y)
        
        +(s(y),x) = x + y + 1 >= x + y + 1 = +(x,s(y))
        
        +(s(x),y) = x + y + 1 >= x + y + 1 = +(x,s(y))
        
        +(s(y),x) = x + y + 1 >= x + y + 1 = +(y,s(x))
        
        +(s(x),y) = x + y + 1 >= x + y + 1 = +(y,s(x))
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(z,+(x,y))
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(z,+(x,y)) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(+(y,x),z)
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(+(y,x),z) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(y,z),x)
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(+(y,z),x) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(x,+(z,y))
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
        
        +(x,+(z,y)) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
        
        +(s(x271),y) = x271 + y + 1 >= x271 + y + 1 = +(x271,s(y))
        
        +(s(x271),y) = x271 + y + 1 >= x271 + y + 1 = +(y,s(x271))
        
        +(x271,s(y)) = x271 + y + 1 >= x271 + y + 1 = +(s(y),x271)
        
        +(y,s(x271)) = x271 + y + 1 >= x271 + y + 1 = +(s(y),x271)
        
        +(x271,s(y)) = x271 + y + 1 >= x271 + y + 1 = +(s(x271),y)
        
        +(y,s(x271)) = x271 + y + 1 >= x271 + y + 1 = +(s(x271),y)
        
        +(s(x273),s(y)) = x273 + y + 2 >= x273 + y + 2 = +(x273,s(s(y)))
        
        +(s(x273),s(y)) = x273 + y + 2 >= x273 + y + 2 = +(s(s(x273)),y)
        
        +(x273,s(s(y))) = x273 + y + 2 >= x273 + y + 2 = +(s(x273),s(y))
        
        +(s(s(x273)),y) = x273 + y + 2 >= x273 + y + 2 = +(s(x273),s(y))
        
        +(+(s(x275),y),z) = x275 + y + z + 1 >= x275 + y + z + 1 = +(+(x275,s(y)),z)
        
        +(+(s(x275),y),z) = x275 + y + z + 1 >= x275 + y + z + 1 = +(s(x275),+(y,z))
        
        +(+(x275,s(y)),z) = x275 + y + z + 1 >= x275 + y + z + 1 = +(+(s(x275),y),z)
        
        +(s(x275),+(y,z)) = x275 + y + z + 1 >= x275 + y + z + 1 = +(+(s(x275),y),z)
        
        +(s(x277),+(y,z)) = x277 + y + z + 1 >= x277 + y + z + 1 = +(x277,s(+(y,z)))
        
        +(s(x277),+(y,z)) = x277 + y + z + 1 >= x277 + y + z + 1 = +(+(s(x277),y),z)
        
        +(x277,s(+(y,z))) = x277 + y + z + 1 >= x277 + y + z + 1 = +(s(x277),+(y,z))
        
        +(+(s(x277),y),z) = x277 + y + z + 1 >= x277 + y + z + 1 = +(s(x277),+(y,z))
        
        +(x,+(s(x279),z)) = x + x279 + z + 1 >= x + x279 + z + 1 = +(x,+(x279,s(z)))
        
        +(x,+(s(x279),z)) = x + x279 + z + 1 >= x + x279 + z + 1 = +(+(x,s(x279)),z)
        
        +(x,+(x279,s(z))) = x + x279 + z + 1 >= x + x279 + z + 1 = +(x,+(s(x279),z))
        
        +(+(x,s(x279)),z) = x + x279 + z + 1 >= x + x279 + z + 1 = +(x,+(s(x279),z))
        
        +(x,s(x282)) = x + x282 + 1 >= x + x282 + 1 = +(s(x),x282)
        
        +(x,s(x282)) = x + x282 + 1 >= x + x282 + 1 = +(s(x282),x)
        
        +(s(x),x282) = x + x282 + 1 >= x + x282 + 1 = +(x282,s(x))
        
        +(s(x282),x) = x + x282 + 1 >= x + x282 + 1 = +(x282,s(x))
        
        +(s(x),x282) = x + x282 + 1 >= x + x282 + 1 = +(x,s(x282))
        
        +(s(x282),x) = x + x282 + 1 >= x + x282 + 1 = +(x,s(x282))
        
        +(s(x),s(x284)) = x + x284 + 2 >= x + x284 + 2 = +(s(s(x)),x284)
        
        +(s(x),s(x284)) = x + x284 + 2 >= x + x284 + 2 = +(x,s(s(x284)))
        
        +(s(s(x)),x284) = x + x284 + 2 >= x + x284 + 2 = +(s(x),s(x284))
        
        +(x,s(s(x284))) = x + x284 + 2 >= x + x284 + 2 = +(s(x),s(x284))
        
        +(+(x,y),s(x286)) = x + x286 + y + 1 >= x + x286 + y + 1 = +(s(+(x,y)),x286)
        
        +(+(x,y),s(x286)) = x + x286 + y + 1 >= x + x286 + y + 1 = +(x,+(y,s(x286)))
        
        +(s(+(x,y)),x286) = x + x286 + y + 1 >= x + x286 + y + 1 = +(+(x,y),s(x286))
        
        +(x,+(y,s(x286))) = x + x286 + y + 1 >= x + x286 + y + 1 = +(+(x,y),s(x286))
        
        +(+(x,s(x288)),z) = x + x288 + z + 1 >= x + x288 + z + 1 = +(+(s(x),x288),z)
        
        +(+(x,s(x288)),z) = x + x288 + z + 1 >= x + x288 + z + 1 = +(x,+(s(x288),z))
        
        +(+(s(x),x288),z) = x + x288 + z + 1 >= x + x288 + z + 1 = +(+(x,s(x288)),z)
        
        +(x,+(s(x288),z)) = x + x288 + z + 1 >= x + x288 + z + 1 = +(+(x,s(x288)),z)
        
        +(x,+(y,s(x290))) = x + x290 + y + 1 >= x + x290 + y + 1 = +(x,+(s(y),x290))
        
        +(x,+(y,s(x290))) = x + x290 + y + 1 >= x + x290 + y + 1 = +(+(x,y),s(x290))
        
        +(x,+(s(y),x290)) = x + x290 + y + 1 >= x + x290 + y + 1 = +(x,+(y,s(x290)))
        
        +(+(x,y),s(x290)) = x + x290 + y + 1 >= x + x290 + y + 1 = +(x,+(y,s(x290)))
        
        +(+(x291,x292),y) = x291 + x292 + y >= x291 + x292 + y = +(x291,+(x292,y))
        
        +(+(x291,x292),y) = x291 + x292 + y >= x291 + x292 + y = +(y,+(x291,x292))
        
        +(x291,+(x292,y)) = x291 + x292 + y >= x291 + x292 + y = +(+(x291,x292),y)
        
        +(y,+(x291,x292)) = x291 + x292 + y >= x291 + x292 + y = +(+(x291,x292),y)
        
        +(+(x294,x295),s(y)) = x294 + x295 + y + 1 >= x294 + x295 + y + 1 = +(x294,+(x295,s(y)))
        
        +(+(x294,x295),s(y)) = x294 + x295 + y + 1 >= x294 + x295 + y + 1 = +(s(+(x294,x295)),y)
        
        +(x294,+(x295,s(y))) = x294 + x295 + y + 1 >= x294 + x295 + y + 1 = +(+(x294,x295),s(y))
        
        +(s(+(x294,x295)),y) = x294 + x295 + y + 1 >= x294 + x295 + y + 1 = +(+(x294,x295),s(y))
        
        +(+(+(x297,x298),y),z) = x297 + x298 + y + z >= x297 + x298 + y + z = +(+(x297,+(x298,y)),z)
        
        +(+(+(x297,x298),y),z) = x297 + x298 + y + z >= x297 + x298 + y + z = +(+(x297,x298),+(y,z))
        
        +(+(x297,+(x298,y)),z) = x297 + x298 + y + z >= x297 + x298 + y + z = +(+(+(x297,x298),y),z)
        
        +(+(x297,x298),+(y,z)) = x297 + x298 + y + z >= x297 + x298 + y + z = +(+(+(x297,x298),y),z)
        
        +(+(x300,x301),+(y,z)) = x300 + x301 + y + z >= x300 + x301 + y + z = +(x300,+(x301,+(y,z)))
        
        +(+(x300,x301),+(y,z)) = x300 + x301 + y + z >= x300 + x301 + y + z = +(+(+(x300,x301),y),z)
        
        +(x300,+(x301,+(y,z))) = x300 + x301 + y + z >= x300 + x301 + y + z = +(+(x300,x301),+(y,z))
        
        +(+(+(x300,x301),y),z) = x300 + x301 + y + z >= x300 + x301 + y + z = +(+(x300,x301),+(y,z))
        
        +(x,+(+(x303,x304),z)) = x + x303 + x304 + z >= x + x303 + x304 + z = +(x,+(x303,+(x304,z)))
        
        +(x,+(+(x303,x304),z)) = x + x303 + x304 + z >= x + x303 + x304 + z = +(+(x,+(x303,x304)),z)
        
        +(x,+(x303,+(x304,z))) = x + x303 + x304 + z >= x + x303 + x304 + z = +(x,+(+(x303,x304),z))
        
        +(+(x,+(x303,x304)),z) = x + x303 + x304 + z >= x + x303 + x304 + z = +(x,+(+(x303,x304),z))
        
        +(x,+(x307,x308)) = x + x307 + x308 >= x + x307 + x308 = +(+(x,x307),x308)
        
        +(x,+(x307,x308)) = x + x307 + x308 >= x + x307 + x308 = +(+(x307,x308),x)
        
        +(+(x,x307),x308) = x + x307 + x308 >= x + x307 + x308 = +(x,+(x307,x308))
        
        +(+(x307,x308),x) = x + x307 + x308 >= x + x307 + x308 = +(x,+(x307,x308))
        
        +(s(x),+(x310,x311)) = x + x310 + x311 + 1 >= x + x310 + x311 + 1 = +(+(s(x),x310),x311)
        
        +(s(x),+(x310,x311)) = x + x310 + x311 + 1 >= x + x310 + x311 + 1 = +(x,s(+(x310,x311)))
        
        +(+(s(x),x310),x311) = x + x310 + x311 + 1 >= x + x310 + x311 + 1 = +(s(x),+(x310,x311))
        
        +(x,s(+(x310,x311))) = x + x310 + x311 + 1 >= x + x310 + x311 + 1 = +(s(x),+(x310,x311))
        
        +(+(x,y),+(x313,x314)) = x + x313 + x314 + y >= x + x313 + x314 + y = +(+(+(x,y),x313),x314)
        
        +(+(x,y),+(x313,x314)) = x + x313 + x314 + y >= x + x313 + x314 + y = +(x,+(y,+(x313,x314)))
        
        +(+(+(x,y),x313),x314) = x + x313 + x314 + y >= x + x313 + x314 + y = +(+(x,y),+(x313,x314))
        
        +(x,+(y,+(x313,x314))) = x + x313 + x314 + y >= x + x313 + x314 + y = +(+(x,y),+(x313,x314))
        
        +(+(x,+(x316,x317)),z) = x + x316 + x317 + z >= x + x316 + x317 + z = +(+(+(x,x316),x317),z)
        
        +(+(x,+(x316,x317)),z) = x + x316 + x317 + z >= x + x316 + x317 + z = +(x,+(+(x316,x317),z))
        
        +(+(+(x,x316),x317),z) = x + x316 + x317 + z >= x + x316 + x317 + z = +(+(x,+(x316,x317)),z)
        
        +(x,+(+(x316,x317),z)) = x + x316 + x317 + z >= x + x316 + x317 + z = +(+(x,+(x316,x317)),z)
        
        +(x,+(y,+(x319,x320))) = x + x319 + x320 + y >= x + x319 + x320 + y = +(x,+(+(y,x319),x320))
        
        +(x,+(y,+(x319,x320))) = x + x319 + x320 + y >= x + x319 + x320 + y = +(+(x,y),+(x319,x320))
        
        +(x,+(+(y,x319),x320)) = x + x319 + x320 + y >= x + x319 + x320 + y = +(x,+(y,+(x319,x320)))
        
        +(+(x,y),+(x319,x320)) = x + x319 + x320 + y >= x + x319 + x320 + y = +(x,+(y,+(x319,x320)))
        
        *(x,s(x322)) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(x,*(x,x322))
        
        *(x,s(x322)) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 = *(s(x322),x)
        
        *(s(x322),x) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 = *(x,s(x322))
        
        *(x,s(x322)) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(x,*(x,x322))
        
        +(x,*(x,x322)) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(x,*(x322,x))
        
        *(s(x322),x) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        +(*(x322,x),x) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(x,*(x322,x))
        
        +(x,*(x,x322)) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x,x322),x)
        
        *(s(x322),x) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        +(*(x322,x),x) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x,x322),x)
        
        +(x,*(x,x322)) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(x,*(x322,x))
        
        +(x,*(x322,x)) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        *(s(x322),x) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        +(x,*(x,x322)) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x,x322),x)
        
        +(*(x,x322),x) = x + x*x + 5x*x322 + x322*x322 + 1 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        *(s(x322),x) = 5x + x*x + 5x*x322 + 2x322 + x322*x322 + 2 >= x + x*x + 5x*x322 + x322*x322 + 1 = +(*(x322,x),x)
        
        *(s(x),s(x324)) = 7x + x*x + 5x*x324 + 7x324 + x324*x324 + 8 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(s(x),*(s(x),x324))
        
        *(s(x),s(x324)) = 7x + x*x + 5x*x324 + 7x324 + x324*x324 + 8 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(*(x,s(x324)),s(x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),*(x,x324)),x324)
        
        +(+(s(x),*(x,x324)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(*(x,x324))),x324)
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(*(x,x324),s(x324)))
        
        +(x,+(*(x,x324),s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(s(*(x,x324)),x324))
        
        +(x,+(s(*(x,x324)),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(*(x,x324))),x324)
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(s(x),*(x324,s(x)))
        
        +(s(x),*(x324,s(x))) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x324,x)))
        
        +(s(x),+(x324,*(x324,x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x324,x))
        
        +(+(s(x),x324),*(x324,x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x324,x),+(s(x),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(*(s(x324),x),s(x324))
        
        +(*(s(x324),x),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x324,x),x),s(x324))
        
        +(+(*(x324,x),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x324,x),+(x,s(x324)))
        
        +(*(x324,x),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x324,x),+(s(x),x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(s(x),*(x324,s(x)))
        
        +(s(x),*(x324,s(x))) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x324,x)))
        
        +(s(x),+(x324,*(x324,x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x324,x))
        
        +(+(s(x),x324),*(x324,x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x324,x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(*(s(x324),x),s(x324))
        
        +(*(s(x324),x),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x324,x),x),s(x324))
        
        +(+(*(x324,x),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x324,x),+(x,s(x324)))
        
        +(*(x324,x),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x324,x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),*(x,x324)),x324)
        
        +(+(s(x),*(x,x324)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),s(x)),x324)
        
        +(+(*(x,x324),s(x)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x),x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),*(x,x324)),x324)
        
        +(+(s(x),*(x,x324)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x324,+(s(x),*(x,x324)))
        
        +(x324,+(s(x),*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),*(x,x324)),x324)
        
        +(+(s(x),*(x,x324)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x324,+(s(x),*(x,x324)))
        
        +(x324,+(s(x),*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x324,s(x)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 = +(*(s(x),x324),s(x))
        
        +(*(s(x),x324),s(x)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(*(x,x324),s(x324)))
        
        +(x,+(*(x,x324),s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),s(x324)),x)
        
        +(+(*(x,x324),s(x324)),x) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x324),s(x))
        
        +(+(*(x,x324),x324),s(x)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x324,s(x)))
        
        +(*(x,x324),+(x324,s(x))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(*(x,x324),s(x324)))
        
        +(x,+(*(x,x324),s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),s(x324)),x)
        
        +(+(*(x,x324),s(x324)),x) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(s(x324),x))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 = +(s(x324),*(x,s(x324)))
        
        +(s(x324),*(x,s(x324))) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x324),+(x,*(x,x324)))
        
        +(s(x324),+(x,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x324),x),*(x,x324))
        
        +(+(s(x324),x),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(*(x,x324),x),s(x324))
        
        +(+(*(x,x324),x),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(*(x,x324),+(x,s(x324)))
        
        +(*(x,x324),+(x,s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(x324,*(x,x324)))
        
        +(s(x),+(x324,*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),x324),*(x,x324))
        
        +(+(s(x),x324),*(x,x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(*(x,x324),s(x324)))
        
        +(x,+(*(x,x324),s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(s(x324),*(x,x324)))
        
        +(x,+(s(x324),*(x,x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(x324)),*(x,x324))
        
        +(s(x),*(s(x),x324)) = 3x + x*x + 5x*x324 + 5x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(s(x),+(*(x,x324),x324))
        
        +(s(x),+(*(x,x324),x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(s(x),*(x,x324)),x324)
        
        +(+(s(x),*(x,x324)),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,s(*(x,x324))),x324)
        
        +(+(x,s(*(x,x324))),x324) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(s(*(x,x324)),x324))
        
        +(*(x,s(x324)),s(x324)) = 5x + x*x + 5x*x324 + 3x324 + x324*x324 + 3 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(+(x,*(x,x324)),s(x324))
        
        +(+(x,*(x,x324)),s(x324)) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(*(x,x324),s(x324)))
        
        +(x,+(*(x,x324),s(x324))) = x + x*x + 5x*x324 + x324 + x324*x324 + 2 >= x + x*x + 5x*x324 + x324 + x324*x324 + 2 = +(x,+(s(*(x,x324)),x324))
        
        *(s(x325),y) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(*(x325,y),y)
        
        *(s(x325),y) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 = *(y,s(x325))
        
        *(y,s(x325)) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 = *(s(x325),y)
        
        *(s(x325),y) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(*(x325,y),y)
        
        +(*(x325,y),y) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(*(y,x325),y)
        
        *(y,s(x325)) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        +(y,*(y,x325)) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(*(y,x325),y)
        
        +(*(x325,y),y) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(x325,y))
        
        *(y,s(x325)) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        +(y,*(y,x325)) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(x325,y))
        
        +(*(x325,y),y) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(*(y,x325),y)
        
        +(*(y,x325),y) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        *(y,s(x325)) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        +(*(x325,y),y) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(x325,y))
        
        +(y,*(x325,y)) = x325*x325 + 5x325*y + y + y*y + 1 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        *(y,s(x325)) = 2x325 + x325*x325 + 5x325*y + 5y + y*y + 2 >= x325*x325 + 5x325*y + y + y*y + 1 = +(y,*(y,x325))
        
        *(s(x327),s(y)) = 7x327 + x327*x327 + 5x327*y + 7y + y*y + 8 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(*(x327,s(y)),s(y))
        
        *(s(x327),s(y)) = 7x327 + x327*x327 + 5x327*y + 7y + y*y + 8 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(s(x327),*(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(*(x327,y),s(y)))
        
        +(x327,+(*(x327,y),s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(s(*(x327,y)),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),*(x327,y)),y)
        
        +(+(s(x327),*(x327,y)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(*(x327,y))),y)
        
        +(+(x327,s(*(x327,y))),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(s(*(x327,y)),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(*(s(y),x327),s(y))
        
        +(*(s(y),x327),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(y,x327),x327),s(y))
        
        +(+(*(y,x327),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(y,x327),+(x327,s(y)))
        
        +(*(y,x327),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(y,x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(s(x327),*(y,s(x327)))
        
        +(s(x327),*(y,s(x327))) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(y,x327)))
        
        +(s(x327),+(y,*(y,x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(y,x327))
        
        +(+(s(x327),y),*(y,x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(y,x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(*(s(y),x327),s(y))
        
        +(*(s(y),x327),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(y,x327),x327),s(y))
        
        +(+(*(y,x327),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(y,x327),+(x327,s(y)))
        
        +(*(y,x327),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(y,x327),+(s(x327),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(s(x327),*(y,s(x327)))
        
        +(s(x327),*(y,s(x327))) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(y,x327)))
        
        +(s(x327),+(y,*(y,x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(y,x327))
        
        +(+(s(x327),y),*(y,x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(y,x327),+(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(*(x327,y),s(y)))
        
        +(x327,+(*(x327,y),s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(s(y),*(x327,y)))
        
        +(x327,+(s(y),*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(y)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(*(x327,y),s(y)))
        
        +(x327,+(*(x327,y),s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),s(y)),x327)
        
        +(+(*(x327,y),s(y)),x327) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(*(x327,y),s(y)))
        
        +(x327,+(*(x327,y),s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),s(y)),x327)
        
        +(+(*(x327,y),s(y)),x327) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(y),x327))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 = +(s(y),*(x327,s(y)))
        
        +(s(y),*(x327,s(y))) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),*(x327,y)),y)
        
        +(+(s(x327),*(x327,y)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(y,+(s(x327),*(x327,y)))
        
        +(y,+(s(x327),*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(y),+(x327,*(x327,y)))
        
        +(s(y),+(x327,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(y),x327),*(x327,y))
        
        +(+(s(y),x327),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),*(x327,y)),y)
        
        +(+(s(x327),*(x327,y)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(y,+(s(x327),*(x327,y)))
        
        +(y,+(s(x327),*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(y,s(x327)),*(x327,y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 = +(*(s(x327),y),s(x327))
        
        +(*(s(x327),y),s(x327)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),y),s(x327))
        
        +(+(*(x327,y),y),s(x327)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(y,s(x327)))
        
        +(*(x327,y),+(y,s(x327))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(y,*(x327,y)))
        
        +(s(x327),+(y,*(x327,y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),y),*(x327,y))
        
        +(+(s(x327),y),*(x327,y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),x327),s(y))
        
        +(+(*(x327,y),x327),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(x327,s(y)))
        
        +(*(x327,y),+(x327,s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),*(x327,y)),y)
        
        +(+(s(x327),*(x327,y)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(*(x327,y),s(x327)),y)
        
        +(+(*(x327,y),s(x327)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(*(x327,y),+(s(x327),y))
        
        +(*(x327,s(y)),s(y)) = 5x327 + x327*x327 + 5x327*y + 3y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,*(x327,y)),s(y))
        
        +(+(x327,*(x327,y)),s(y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(*(x327,y),s(y)))
        
        +(x327,+(*(x327,y),s(y))) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(x327,+(s(*(x327,y)),y))
        
        +(x327,+(s(*(x327,y)),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(*(x327,y))),y)
        
        +(s(x327),*(s(x327),y)) = 3x327 + x327*x327 + 5x327*y + 5y + y*y + 3 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(s(x327),+(*(x327,y),y))
        
        +(s(x327),+(*(x327,y),y)) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(s(x327),*(x327,y)),y)
        
        +(+(s(x327),*(x327,y)),y) = x327 + x327*x327 + 5x327*y + y + y*y + 2 >= x327 + x327*x327 + 5x327*y + y + y*y + 2 = +(+(x327,s(*(x327,y))),y)
        
        *(x,y) = x*x + 5x*y + y*y + 1 >= x*x + 5x*y + y*y + 1 = *(y,x)
        
        +(x,y) = x + y >= x + y = +(y,x)
       problem:
        strict:
         *(x,s(y)) -> *(s(y),x)
         +(x,*(x,y)) -> +(x,*(y,x))
         +(x,*(y,x)) -> +(*(y,x),x)
         +(x,*(x,y)) -> +(*(x,y),x)
         +(*(x,y),x) -> +(*(y,x),x)
         *(s(y),x) -> *(x,s(y))
         +(*(y,x),x) -> +(*(x,y),x)
         +(x,*(x,y)) -> +(*(x,y),x)
         +(*(y,x),x) -> +(x,*(y,x))
         +(x,*(x,y)) -> +(x,*(y,x))
         *(s(x),y) -> *(y,s(x))
         +(*(x,y),y) -> +(*(y,x),y)
         +(*(y,x),y) -> +(y,*(y,x))
         +(*(x,y),y) -> +(y,*(x,y))
         +(y,*(x,y)) -> +(y,*(y,x))
         *(y,s(x)) -> *(s(x),y)
         +(y,*(y,x)) -> +(y,*(x,y))
         +(*(x,y),y) -> +(y,*(x,y))
         +(y,*(y,x)) -> +(*(y,x),y)
         +(*(x,y),y) -> +(*(y,x),y)
         +(s(x),y) -> +(y,s(x))
         +(s(x),y) -> +(x,s(y))
         +(y,s(x)) -> +(s(x),y)
         +(x,s(y)) -> +(s(x),y)
         +(y,s(x)) -> +(s(y),x)
         +(x,s(y)) -> +(s(y),x)
         +(x,s(y)) -> +(s(y),x)
         +(x,s(y)) -> +(s(x),y)
         +(s(y),x) -> +(x,s(y))
         +(s(x),y) -> +(x,s(y))
         +(s(y),x) -> +(y,s(x))
         +(s(x),y) -> +(y,s(x))
         +(+(x,y),z) -> +(z,+(x,y))
         +(+(x,y),z) -> +(x,+(y,z))
         +(z,+(x,y)) -> +(+(x,y),z)
         +(x,+(y,z)) -> +(+(x,y),z)
         +(+(x,y),z) -> +(+(y,x),z)
         +(+(x,y),z) -> +(x,+(y,z))
         +(+(y,x),z) -> +(+(x,y),z)
         +(x,+(y,z)) -> +(+(x,y),z)
         +(x,+(y,z)) -> +(+(y,z),x)
         +(x,+(y,z)) -> +(+(x,y),z)
         +(+(y,z),x) -> +(x,+(y,z))
         +(+(x,y),z) -> +(x,+(y,z))
         +(x,+(y,z)) -> +(x,+(z,y))
         +(x,+(y,z)) -> +(+(x,y),z)
         +(x,+(z,y)) -> +(x,+(y,z))
         +(+(x,y),z) -> +(x,+(y,z))
         +(s(x271),y) -> +(x271,s(y))
         +(s(x271),y) -> +(y,s(x271))
         +(x271,s(y)) -> +(s(y),x271)
         +(y,s(x271)) -> +(s(y),x271)
         +(x271,s(y)) -> +(s(x271),y)
         +(y,s(x271)) -> +(s(x271),y)
         +(s(x273),s(y)) -> +(x273,s(s(y)))
         +(s(x273),s(y)) -> +(s(s(x273)),y)
         +(x273,s(s(y))) -> +(s(x273),s(y))
         +(s(s(x273)),y) -> +(s(x273),s(y))
         +(+(s(x275),y),z) -> +(+(x275,s(y)),z)
         +(+(s(x275),y),z) -> +(s(x275),+(y,z))
         +(+(x275,s(y)),z) -> +(+(s(x275),y),z)
         +(s(x275),+(y,z)) -> +(+(s(x275),y),z)
         +(s(x277),+(y,z)) -> +(x277,s(+(y,z)))
         +(s(x277),+(y,z)) -> +(+(s(x277),y),z)
         +(x277,s(+(y,z))) -> +(s(x277),+(y,z))
         +(+(s(x277),y),z) -> +(s(x277),+(y,z))
         +(x,+(s(x279),z)) -> +(x,+(x279,s(z)))
         +(x,+(s(x279),z)) -> +(+(x,s(x279)),z)
         +(x,+(x279,s(z))) -> +(x,+(s(x279),z))
         +(+(x,s(x279)),z) -> +(x,+(s(x279),z))
         +(x,s(x282)) -> +(s(x),x282)
         +(x,s(x282)) -> +(s(x282),x)
         +(s(x),x282) -> +(x282,s(x))
         +(s(x282),x) -> +(x282,s(x))
         +(s(x),x282) -> +(x,s(x282))
         +(s(x282),x) -> +(x,s(x282))
         +(s(x),s(x284)) -> +(s(s(x)),x284)
         +(s(x),s(x284)) -> +(x,s(s(x284)))
         +(s(s(x)),x284) -> +(s(x),s(x284))
         +(x,s(s(x284))) -> +(s(x),s(x284))
         +(+(x,y),s(x286)) -> +(s(+(x,y)),x286)
         +(+(x,y),s(x286)) -> +(x,+(y,s(x286)))
         +(s(+(x,y)),x286) -> +(+(x,y),s(x286))
         +(x,+(y,s(x286))) -> +(+(x,y),s(x286))
         +(+(x,s(x288)),z) -> +(+(s(x),x288),z)
         +(+(x,s(x288)),z) -> +(x,+(s(x288),z))
         +(+(s(x),x288),z) -> +(+(x,s(x288)),z)
         +(x,+(s(x288),z)) -> +(+(x,s(x288)),z)
         +(x,+(y,s(x290))) -> +(x,+(s(y),x290))
         +(x,+(y,s(x290))) -> +(+(x,y),s(x290))
         +(x,+(s(y),x290)) -> +(x,+(y,s(x290)))
         +(+(x,y),s(x290)) -> +(x,+(y,s(x290)))
         +(+(x291,x292),y) -> +(x291,+(x292,y))
         +(+(x291,x292),y) -> +(y,+(x291,x292))
         +(x291,+(x292,y)) -> +(+(x291,x292),y)
         +(y,+(x291,x292)) -> +(+(x291,x292),y)
         +(+(x294,x295),s(y)) -> +(x294,+(x295,s(y)))
         +(+(x294,x295),s(y)) -> +(s(+(x294,x295)),y)
         +(x294,+(x295,s(y))) -> +(+(x294,x295),s(y))
         +(s(+(x294,x295)),y) -> +(+(x294,x295),s(y))
         +(+(+(x297,x298),y),z) -> +(+(x297,+(x298,y)),z)
         +(+(+(x297,x298),y),z) -> +(+(x297,x298),+(y,z))
         +(+(x297,+(x298,y)),z) -> +(+(+(x297,x298),y),z)
         +(+(x297,x298),+(y,z)) -> +(+(+(x297,x298),y),z)
         +(+(x300,x301),+(y,z)) -> +(x300,+(x301,+(y,z)))
         +(+(x300,x301),+(y,z)) -> +(+(+(x300,x301),y),z)
         +(x300,+(x301,+(y,z))) -> +(+(x300,x301),+(y,z))
         +(+(+(x300,x301),y),z) -> +(+(x300,x301),+(y,z))
         +(x,+(+(x303,x304),z)) -> +(x,+(x303,+(x304,z)))
         +(x,+(+(x303,x304),z)) -> +(+(x,+(x303,x304)),z)
         +(x,+(x303,+(x304,z))) -> +(x,+(+(x303,x304),z))
         +(+(x,+(x303,x304)),z) -> +(x,+(+(x303,x304),z))
         +(x,+(x307,x308)) -> +(+(x,x307),x308)
         +(x,+(x307,x308)) -> +(+(x307,x308),x)
         +(+(x,x307),x308) -> +(x,+(x307,x308))
         +(+(x307,x308),x) -> +(x,+(x307,x308))
         +(s(x),+(x310,x311)) -> +(+(s(x),x310),x311)
         +(s(x),+(x310,x311)) -> +(x,s(+(x310,x311)))
         +(+(s(x),x310),x311) -> +(s(x),+(x310,x311))
         +(x,s(+(x310,x311))) -> +(s(x),+(x310,x311))
         +(+(x,y),+(x313,x314)) -> +(+(+(x,y),x313),x314)
         +(+(x,y),+(x313,x314)) -> +(x,+(y,+(x313,x314)))
         +(+(+(x,y),x313),x314) -> +(+(x,y),+(x313,x314))
         +(x,+(y,+(x313,x314))) -> +(+(x,y),+(x313,x314))
         +(+(x,+(x316,x317)),z) -> +(+(+(x,x316),x317),z)
         +(+(x,+(x316,x317)),z) -> +(x,+(+(x316,x317),z))
         +(+(+(x,x316),x317),z) -> +(+(x,+(x316,x317)),z)
         +(x,+(+(x316,x317),z)) -> +(+(x,+(x316,x317)),z)
         +(x,+(y,+(x319,x320))) -> +(x,+(+(y,x319),x320))
         +(x,+(y,+(x319,x320))) -> +(+(x,y),+(x319,x320))
         +(x,+(+(y,x319),x320)) -> +(x,+(y,+(x319,x320)))
         +(+(x,y),+(x319,x320)) -> +(x,+(y,+(x319,x320)))
         *(x,s(x322)) -> *(s(x322),x)
         *(s(x322),x) -> *(x,s(x322))
         +(x,*(x,x322)) -> +(x,*(x322,x))
         +(*(x322,x),x) -> +(x,*(x322,x))
         +(x,*(x,x322)) -> +(*(x,x322),x)
         +(*(x322,x),x) -> +(*(x,x322),x)
         +(x,*(x,x322)) -> +(x,*(x322,x))
         +(x,*(x322,x)) -> +(*(x322,x),x)
         +(x,*(x,x322)) -> +(*(x,x322),x)
         +(*(x,x322),x) -> +(*(x322,x),x)
         +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
         +(+(s(x),*(x,x324)),x324) -> +(+(x,s(*(x,x324))),x324)
         +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
         +(x,+(*(x,x324),s(x324))) -> +(x,+(s(*(x,x324)),x324))
         +(x,+(s(*(x,x324)),x324)) -> +(+(x,s(*(x,x324))),x324)
         +(s(x),*(s(x),x324)) -> +(s(x),*(x324,s(x)))
         +(s(x),+(x324,*(x324,x))) -> +(+(s(x),x324),*(x324,x))
         +(+(s(x),x324),*(x324,x)) -> +(*(x324,x),+(s(x),x324))
         +(*(x,s(x324)),s(x324)) -> +(*(s(x324),x),s(x324))
         +(+(*(x324,x),x),s(x324)) -> +(*(x324,x),+(x,s(x324)))
         +(*(x324,x),+(x,s(x324))) -> +(*(x324,x),+(s(x),x324))
         +(s(x),*(s(x),x324)) -> +(s(x),*(x324,s(x)))
         +(s(x),+(x324,*(x324,x))) -> +(+(s(x),x324),*(x324,x))
         +(+(s(x),x324),*(x324,x)) -> +(+(x,s(x324)),*(x324,x))
         +(*(x,s(x324)),s(x324)) -> +(*(s(x324),x),s(x324))
         +(+(*(x324,x),x),s(x324)) -> +(*(x324,x),+(x,s(x324)))
         +(*(x324,x),+(x,s(x324))) -> +(+(x,s(x324)),*(x324,x))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x),x324))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x),x324))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(*(x,x324),+(s(x),x324))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
         +(+(s(x),*(x,x324)),x324) -> +(+(*(x,x324),s(x)),x324)
         +(+(*(x,x324),s(x)),x324) -> +(*(x,x324),+(s(x),x324))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x),x324))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(+(x324,s(x)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
         +(+(s(x),*(x,x324)),x324) -> +(x324,+(s(x),*(x,x324)))
         +(x324,+(s(x),*(x,x324))) -> +(+(x324,s(x)),*(x,x324))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
         +(+(s(x),*(x,x324)),x324) -> +(x324,+(s(x),*(x,x324)))
         +(x324,+(s(x),*(x,x324))) -> +(+(x324,s(x)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x324,s(x)),*(x,x324))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x324),x))
         +(s(x),*(s(x),x324)) -> +(*(s(x),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
         +(x,+(*(x,x324),s(x324))) -> +(+(*(x,x324),s(x324)),x)
         +(+(*(x,x324),s(x324)),x) -> +(*(x,x324),+(s(x324),x))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(*(x,x324),+(s(x324),x))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(*(x,x324),+(s(x324),x))
         +(s(x),+(*(x,x324),x324)) -> +(+(*(x,x324),x324),s(x))
         +(+(*(x,x324),x324),s(x)) -> +(*(x,x324),+(x324,s(x)))
         +(*(x,x324),+(x324,s(x))) -> +(*(x,x324),+(s(x324),x))
         +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
         +(x,+(*(x,x324),s(x324))) -> +(+(*(x,x324),s(x324)),x)
         +(+(*(x,x324),s(x324)),x) -> +(*(x,x324),+(s(x324),x))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(*(x,s(x324)),s(x324)) -> +(s(x324),*(x,s(x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(s(x324),+(x,*(x,x324)))
         +(s(x324),+(x,*(x,x324))) -> +(+(s(x324),x),*(x,x324))
         +(+(s(x324),x),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(+(*(x,x324),x),s(x324))
         +(+(*(x,x324),x),s(x324)) -> +(*(x,x324),+(x,s(x324)))
         +(*(x,x324),+(x,s(x324))) -> +(+(x,s(x324)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(s(x),+(x324,*(x,x324)))
         +(s(x),+(x324,*(x,x324))) -> +(+(s(x),x324),*(x,x324))
         +(+(s(x),x324),*(x,x324)) -> +(+(x,s(x324)),*(x,x324))
         +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
         +(x,+(*(x,x324),s(x324))) -> +(x,+(s(x324),*(x,x324)))
         +(x,+(s(x324),*(x,x324))) -> +(+(x,s(x324)),*(x,x324))
         +(s(x),+(*(x,x324),x324)) -> +(+(s(x),*(x,x324)),x324)
         +(+(s(x),*(x,x324)),x324) -> +(+(x,s(*(x,x324))),x324)
         +(+(x,s(*(x,x324))),x324) -> +(x,+(s(*(x,x324)),x324))
         +(+(x,*(x,x324)),s(x324)) -> +(x,+(*(x,x324),s(x324)))
         +(x,+(*(x,x324),s(x324))) -> +(x,+(s(*(x,x324)),x324))
         *(s(x325),y) -> *(y,s(x325))
         *(y,s(x325)) -> *(s(x325),y)
         +(*(x325,y),y) -> +(*(y,x325),y)
         +(y,*(y,x325)) -> +(*(y,x325),y)
         +(*(x325,y),y) -> +(y,*(x325,y))
         +(y,*(y,x325)) -> +(y,*(x325,y))
         +(*(x325,y),y) -> +(*(y,x325),y)
         +(*(y,x325),y) -> +(y,*(y,x325))
         +(*(x325,y),y) -> +(y,*(x325,y))
         +(y,*(x325,y)) -> +(y,*(y,x325))
         +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
         +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(*(x327,y)),y))
         +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
         +(+(s(x327),*(x327,y)),y) -> +(+(x327,s(*(x327,y))),y)
         +(+(x327,s(*(x327,y))),y) -> +(x327,+(s(*(x327,y)),y))
         +(*(x327,s(y)),s(y)) -> +(*(s(y),x327),s(y))
         +(+(*(y,x327),x327),s(y)) -> +(*(y,x327),+(x327,s(y)))
         +(*(y,x327),+(x327,s(y))) -> +(+(x327,s(y)),*(y,x327))
         +(s(x327),*(s(x327),y)) -> +(s(x327),*(y,s(x327)))
         +(s(x327),+(y,*(y,x327))) -> +(+(s(x327),y),*(y,x327))
         +(+(s(x327),y),*(y,x327)) -> +(+(x327,s(y)),*(y,x327))
         +(*(x327,s(y)),s(y)) -> +(*(s(y),x327),s(y))
         +(+(*(y,x327),x327),s(y)) -> +(*(y,x327),+(x327,s(y)))
         +(*(y,x327),+(x327,s(y))) -> +(*(y,x327),+(s(x327),y))
         +(s(x327),*(s(x327),y)) -> +(s(x327),*(y,s(x327)))
         +(s(x327),+(y,*(y,x327))) -> +(+(s(x327),y),*(y,x327))
         +(+(s(x327),y),*(y,x327)) -> +(*(y,x327),+(s(x327),y))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(+(x327,s(y)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
         +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(y),*(x327,y)))
         +(x327,+(s(y),*(x327,y))) -> +(+(x327,s(y)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(x327,s(y)),*(x327,y))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
         +(x327,+(*(x327,y),s(y))) -> +(+(*(x327,y),s(y)),x327)
         +(+(*(x327,y),s(y)),x327) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
         +(x327,+(*(x327,y),s(y))) -> +(+(*(x327,y),s(y)),x327)
         +(+(*(x327,y),s(y)),x327) -> +(*(x327,y),+(s(y),x327))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(y),x327))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(*(x327,s(y)),s(y)) -> +(s(y),*(x327,s(y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
         +(+(s(x327),*(x327,y)),y) -> +(y,+(s(x327),*(x327,y)))
         +(y,+(s(x327),*(x327,y))) -> +(+(y,s(x327)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(+(y,s(x327)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(s(y),+(x327,*(x327,y)))
         +(s(y),+(x327,*(x327,y))) -> +(+(s(y),x327),*(x327,y))
         +(+(s(y),x327),*(x327,y)) -> +(+(y,s(x327)),*(x327,y))
         +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
         +(+(s(x327),*(x327,y)),y) -> +(y,+(s(x327),*(x327,y)))
         +(y,+(s(x327),*(x327,y))) -> +(+(y,s(x327)),*(x327,y))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
         +(s(x327),*(s(x327),y)) -> +(*(s(x327),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(x327),y))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
         +(s(x327),+(*(x327,y),y)) -> +(+(*(x327,y),y),s(x327))
         +(+(*(x327,y),y),s(x327)) -> +(*(x327,y),+(y,s(x327)))
         +(*(x327,y),+(y,s(x327))) -> +(*(x327,y),+(s(x327),y))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
         +(s(x327),+(*(x327,y),y)) -> +(s(x327),+(y,*(x327,y)))
         +(s(x327),+(y,*(x327,y))) -> +(+(s(x327),y),*(x327,y))
         +(+(s(x327),y),*(x327,y)) -> +(*(x327,y),+(s(x327),y))
         +(+(x327,*(x327,y)),s(y)) -> +(+(*(x327,y),x327),s(y))
         +(+(*(x327,y),x327),s(y)) -> +(*(x327,y),+(x327,s(y)))
         +(*(x327,y),+(x327,s(y))) -> +(*(x327,y),+(s(x327),y))
         +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
         +(+(s(x327),*(x327,y)),y) -> +(+(*(x327,y),s(x327)),y)
         +(+(*(x327,y),s(x327)),y) -> +(*(x327,y),+(s(x327),y))
         +(+(x327,*(x327,y)),s(y)) -> +(x327,+(*(x327,y),s(y)))
         +(x327,+(*(x327,y),s(y))) -> +(x327,+(s(*(x327,y)),y))
         +(x327,+(s(*(x327,y)),y)) -> +(+(x327,s(*(x327,y))),y)
         +(s(x327),+(*(x327,y),y)) -> +(+(s(x327),*(x327,y)),y)
         +(+(s(x327),*(x327,y)),y) -> +(+(x327,s(*(x327,y))),y)
        weak:
         *(x,y) -> *(y,x)
         +(x,y) -> +(y,x)
         +(s(x),y) -> +(x,s(y))
         +(x,s(y)) -> +(s(x),y)
         +(+(x,y),z) -> +(x,+(y,z))
         +(x,+(y,z)) -> +(+(x,y),z)
       Shift Processor (ldh) lab=left (force):
        strict:
         
        weak:
         
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          *(s(y),x) <-0|[==1,==0,==0]- *(x,s(y)) -6|[==1,==0,==0]-> +(x,*(x,y))
         joins (1):
          *(s(y),x) -7|[==1,==0,==0]-> +(*(y,x),x)
          +(x,*(x,y)) -0|1[>>0,==0,==0]-> +(x,*(y,x)) -1|[>>0,==0,==0]-> +(*(y,x),x)
         peak:
          *(y,s(x)) <-0|[==1,==0,==0]- *(s(x),y) -7|[==1,==0,==0]-> +(*(x,y),y)
         joins (1):
          *(y,s(x)) -6|[==1,==0,==0]-> +(y,*(y,x))
          +(*(x,y),y) -0|0[>>0,==0,==0]-> +(*(y,x),y) -1|[>>0,==0,==0]-> +(y,*(y,x))
         peak:
          +(y,s(x)) <-1|[==1,==0,==0]- +(s(x),y) -2|[==1,==0,==0]-> +(x,s(y))
         joins (1):
          +(y,s(x)) -1|[==1,==0,==0]-> +(s(x),y)
          +(x,s(y)) -3|[==1,==0,==0]-> +(s(x),y)
         peak:
          +(s(y),x) <-1|[==1,==0,==0]- +(x,s(y)) -3|[==1,==0,==0]-> +(s(x),y)
         joins (1):
          +(s(y),x) -1|[==1,==0,==0]-> +(x,s(y))
          +(s(x),y) -2|[==1,==0,==0]-> +(x,s(y))
         peak:
          +(z,+(x,y)) <-1|[==1,==0,==0]- +(+(x,y),z) -4|[==1,==0,==0]-> +(x,+(y,z))
         joins (1):
          +(z,+(x,y)) -1|[==1,==0,==0]-> +(+(x,y),z)
          +(x,+(y,z)) -5|[==1,==0,==0]-> +(+(x,y),z)
         peak:
          +(+(y,x),z) <-1|0[==1,==0,==0]- +(+(x,y),z) -4|[==1,==0,==0]-> +(x,+(y,z))
         joins (1):
          +(+(y,x),z) -1|0[==1,==0,==0]-> +(+(x,y),z)
          +(x,+(y,z)) -5|[==1,==0,==0]-> +(+(x,y),z)
         peak:
          +(+(y,z),x) <-1|[==1,==0,==0]- +(x,+(y,z)) -5|[==1,==0,==0]-> +(+(x,y),z)
         joins (1):
          +(+(y,z),x) -1|[==1,==0,==0]-> +(x,+(y,z))
          +(+(x,y),z) -4|[==1,==0,==0]-> +(x,+(y,z))
         peak:
          +(x,+(z,y)) <-1|1[==1,==0,==0]- +(x,+(y,z)) -5|[==1,==0,==0]-> +(+(x,y),z)
         joins (1):
          +(x,+(z,y)) -1|1[==1,==0,==0]-> +(x,+(y,z))
          +(+(x,y),z) -4|[==1,==0,==0]-> +(x,+(y,z))
         peak:
          +(x271,s(y)) <-2|[==1,==0,==0]- +(s(x271),y) -1|[==1,==0,==0]-> +(y,s(x271))
         joins (1):
          +(x271,s(y)) -1|[==1,==0,==0]-> +(s(y),x271)
          +(y,s(x271)) -3|[==1,==0,==0]-> +(s(y),x271)
         peak:
          +(x273,s(s(y))) <-2|[==1,==0,==0]- +(s(x273),s(y)) -3|[==1,==0,==0]-> +(s(s(x273)),y)
         joins (1):
          +(x273,s(s(y))) -3|[==1,==0,==0]-> +(s(x273),s(y))
          +(s(s(x273)),y) -2|[==1,==0,==0]-> +(s(x273),s(y))
         peak:
          +(+(x275,s(y)),z) <-2|0[==1,==0,==0]- +(+(s(x275),y),z) -4|
                                                [==1,==0,==0]-> +(s(x275),+(y,z))
         joins (1):
          +(+(x275,s(y)),z) -3|0[==1,==0,==0]-> +(+(s(x275),y),z)
          +(s(x275),+(y,z)) -5|[==1,==0,==0]-> +(+(s(x275),y),z)
         peak:
          +(x277,s(+(y,z))) <-2|[==1,==0,==0]- +(s(x277),+(y,z)) -5|[
                                               ==1,==0,==0]-> +(+(s(x277),y),z)
         joins (1):
          +(x277,s(+(y,z))) -3|[==1,==0,==0]-> +(s(x277),+(y,z))
          +(+(s(x277),y),z) -4|[==1,==0,==0]-> +(s(x277),+(y,z))
         peak:
          +(x,+(x279,s(z))) <-2|1[==1,==0,==0]- +(x,+(s(x279),z)) -5|
                                                [==1,==0,==0]-> +(+(x,s(x279)),z)
         joins (1):
          +(x,+(x279,s(z))) -3|1[==1,==0,==0]-> +(x,+(s(x279),z))
          +(+(x,s(x279)),z) -4|[==1,==0,==0]-> +(x,+(s(x279),z))
         peak:
          +(s(x),x282) <-3|[==1,==0,==0]- +(x,s(x282)) -1|[==1,==0,==0]-> +(s(x282),x)
         joins (1):
          +(s(x),x282) -1|[==1,==0,==0]-> +(x282,s(x))
          +(s(x282),x) -2|[==1,==0,==0]-> +(x282,s(x))
         peak:
          +(s(s(x)),x284) <-3|[==1,==0,==0]- +(s(x),s(x284)) -2|[==1,==0,==0]-> +(x,s(s(x284)))
         joins (1):
          +(s(s(x)),x284) -2|[==1,==0,==0]-> +(s(x),s(x284))
          +(x,s(s(x284))) -3|[==1,==0,==0]-> +(s(x),s(x284))
         peak:
          +(s(+(x,y)),x286) <-3|[==1,==0,==0]- +(+(x,y),s(x286)) -4|[
                                               ==1,==0,==0]-> +(x,+(y,s(x286)))
         joins (1):
          +(s(+(x,y)),x286) -2|[==1,==0,==0]-> +(+(x,y),s(x286))
          +(x,+(y,s(x286))) -5|[==1,==0,==0]-> +(+(x,y),s(x286))
         peak:
          +(+(s(x),x288),z) <-3|0[==1,==0,==0]- +(+(x,s(x288)),z) -4|
                                                [==1,==0,==0]-> +(x,+(s(x288),z))
         joins (1):
          +(+(s(x),x288),z) -2|0[==1,==0,==0]-> +(+(x,s(x288)),z)
          +(x,+(s(x288),z)) -5|[==1,==0,==0]-> +(+(x,s(x288)),z)
         peak:
          +(x,+(s(y),x290)) <-3|1[==1,==0,==0]- +(x,+(y,s(x290))) -5|
                                                [==1,==0,==0]-> +(+(x,y),s(x290))
         joins (1):
          +(x,+(s(y),x290)) -2|1[==1,==0,==0]-> +(x,+(y,s(x290)))
          +(+(x,y),s(x290)) -4|[==1,==0,==0]-> +(x,+(y,s(x290)))
         peak:
          +(x291,+(x292,y)) <-4|[==1,==0,==0]- +(+(x291,x292),y) -1|[
                                               ==1,==0,==0]-> +(y,+(x291,x292))
         joins (1):
          +(x291,+(x292,y)) -5|[==1,==0,==0]-> +(+(x291,x292),y)
          +(y,+(x291,x292)) -1|[==1,==0,==0]-> +(+(x291,x292),y)
         peak:
          +(x294,+(x295,s(y))) <-4|[==1,==0,==0]- +(+(x294,x295),s(y)) -3|
                                                  [==1,==0,==0]-> +(s(+(x294,x295)),y)
         joins (1):
          +(x294,+(x295,s(y))) -5|[==1,==0,==0]-> +(+(x294,x295),s(y))
          +(s(+(x294,x295)),y) -2|[==1,==0,==0]-> +(+(x294,x295),s(y))
         peak:
          +(+(x297,+(x298,y)),z) <-4|0[==1,==0,==0]- +(+(+(x297,x298),y),z) -4|
                                                     [==1,==0,==0]-> 
                                                     +(+(x297,x298),+(y,z))
         joins (1):
          +(+(x297,+(x298,y)),z) -5|0[==1,==0,==0]-> +(+(+(x297,x298),y),z)
          +(+(x297,x298),+(y,z)) -5|[==1,==0,==0]-> +(+(+(x297,x298),y),z)
         peak:
          +(x300,+(x301,+(y,z))) <-4|[==1,==0,==0]- +(+(x300,x301),+(y,z)) -5|
                                                    [==1,==0,==0]-> +(+(+(x300,x301),y),z)
         joins (1):
          +(x300,+(x301,+(y,z))) -5|[==1,==0,==0]-> +(+(x300,x301),+(y,z))
          +(+(+(x300,x301),y),z) -4|[==1,==0,==0]-> +(+(x300,x301),+(y,z))
         peak:
          +(x,+(x303,+(x304,z))) <-4|1[==1,==0,==0]- +(x,+(+(x303,x304),z)) -5|
                                                     [==1,==0,==0]-> 
                                                     +(+(x,+(x303,x304)),z)
         joins (1):
          +(x,+(x303,+(x304,z))) -5|1[==1,==0,==0]-> +(x,+(+(x303,x304),z))
          +(+(x,+(x303,x304)),z) -4|[==1,==0,==0]-> +(x,+(+(x303,x304),z))
         peak:
          +(+(x,x307),x308) <-5|[==1,==0,==0]- +(x,+(x307,x308)) -1|[
                                               ==1,==0,==0]-> +(+(x307,x308),x)
         joins (1):
          +(+(x,x307),x308) -4|[==1,==0,==0]-> +(x,+(x307,x308))
          +(+(x307,x308),x) -1|[==1,==0,==0]-> +(x,+(x307,x308))
         peak:
          +(+(s(x),x310),x311) <-5|[==1,==0,==0]- +(s(x),+(x310,x311)) -2|
                                                  [==1,==0,==0]-> +(x,s(+(x310,x311)))
         joins (1):
          +(+(s(x),x310),x311) -4|[==1,==0,==0]-> +(s(x),+(x310,x311))
          +(x,s(+(x310,x311))) -3|[==1,==0,==0]-> +(s(x),+(x310,x311))
         peak:
          +(+(+(x,y),x313),x314) <-5|[==1,==0,==0]- +(+(x,y),+(x313,x314)) -4|
                                                    [==1,==0,==0]-> +(x,+(y,+(x313,x314)))
         joins (1):
          +(+(+(x,y),x313),x314) -4|[==1,==0,==0]-> +(+(x,y),+(x313,x314))
          +(x,+(y,+(x313,x314))) -5|[==1,==0,==0]-> +(+(x,y),+(x313,x314))
         peak:
          +(+(+(x,x316),x317),z) <-5|0[==1,==0,==0]- +(+(x,+(x316,x317)),z) -4|
                                                     [==1,==0,==0]-> 
                                                     +(x,+(+(x316,x317),z))
         joins (1):
          +(+(+(x,x316),x317),z) -4|0[==1,==0,==0]-> +(+(x,+(x316,x317)),z)
          +(x,+(+(x316,x317),z)) -5|[==1,==0,==0]-> +(+(x,+(x316,x317)),z)
         peak:
          +(x,+(+(y,x319),x320)) <-5|1[==1,==0,==0]- +(x,+(y,+(x319,x320))) -5|
                                                     [==1,==0,==0]-> 
                                                     +(+(x,y),+(x319,x320))
         joins (1):
          +(x,+(+(y,x319),x320)) -4|1[==1,==0,==0]-> +(x,+(y,+(x319,x320)))
          +(+(x,y),+(x319,x320)) -4|[==1,==0,==0]-> +(x,+(y,+(x319,x320)))
         peak:
          +(x,*(x,x322)) <-6|[==1,==0,==0]- *(x,s(x322)) -0|[==1,==0,==0]-> *(s(x322),x)
         joins (1):
          +(x,*(x,x322)) -0|1[>>0,==0,==0]-> +(x,*(x322,x))
          *(s(x322),x) -7|[==1,==0,==0]-> +(*(x322,x),x) -1|[>>0,==0,==0]-> +(x,*(x322,x))
         peak:
          +(s(x),*(s(x),x324)) <-6|[==1,==0,==0]- *(s(x),s(x324)) -7|
                                                  [==1,==0,==0]-> +(*(x,s(x324)),s(x324))
         joins (1):
          +(s(x),*(s(x),x324)) -7|1[>>0,==0,==0]-> +(s(x),+(*(x,x324),x324)) -5|[>>0,==0,==0]-> 
           +(+(s(x),*(x,x324)),x324) -2|0[>>0,==0,==0]-> +(+(x,s(*(x,x324))),x324)
          +(*(x,s(x324)),s(x324)) -6|0[>>0,==0,==0]-> +(+(x,*(x,x324)),s(x324)) -4|[>>0,==0,==0]-> 
           +(x,+(*(x,x324),s(x324))) -3|1[>>0,==0,==0]-> +(x,+(s(*(x,x324)),x324)) -5|
                                                         [>>0,==0,==0]-> 
                                                         +(+(x,s(*(x,x324))),x324)
         peak:
          +(*(x325,y),y) <-7|[==1,==0,==0]- *(s(x325),y) -0|[==1,==0,==0]-> *(y,s(x325))
         joins (1):
          +(*(x325,y),y) -0|0[>>0,==0,==0]-> +(*(y,x325),y)
          *(y,s(x325)) -6|[==1,==0,==0]-> +(y,*(y,x325)) -1|[>>0,==0,==0]-> +(*(y,x325),y)
         peak:
          +(*(x327,s(y)),s(y)) <-7|[==1,==0,==0]- *(s(x327),s(y)) -6|
                                                  [==1,==0,==0]-> +(s(x327),*(s(x327),y))
         joins (1):
          +(*(x327,s(y)),s(y)) -6|0[>>0,==0,==0]-> +(+(x327,*(x327,y)),s(y)) -4|[>>0,==0,==0]-> 
           +(x327,+(*(x327,y),s(y))) -3|1[>>0,==0,==0]-> +(x327,+(s(*(x327,y)),y))
          +(s(x327),*(s(x327),y)) -7|1[>>0,==0,==0]-> +(s(x327),+(*(x327,y),y)) -5|[>>0,==0,==0]-> 
           +(+(s(x327),*(x327,y)),y) -2|0[>>0,==0,==0]-> +(+(x327,s(*(x327,y))),y) -4|
                                                         [>>0,==0,==0]-> 
                                                         +(x327,+(s(*(x327,y)),y))
         Qed