Problem:
 -(+(x,-(x))) -> 0()
 +(x,-(x)) -> 0()
 -(+(0(),0())) -> 0()
 +(0(),0()) -> 0()
 -(0()) -> 0()

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 8
   -(+(+(x29,-(x29)),0())) <-0|0,1[]- -(+(+(x29,-(x29)),-(+(x29,-(x29))))) -0|[]-> 0()
   +(+(x30,-(x30)),0()) <-0|1[]- +(+(x30,-(x30)),-(+(x30,-(x30)))) -1|[]-> 0()
   -(0()) <-1|0[]- -(+(x,-(x))) -0|[]-> 0()
   -(+(+(0(),0()),0())) <-2|0,1[]- -(+(+(0(),0()),-(+(0(),0())))) -0|[]-> 0()
   +(+(0(),0()),0()) <-2|1[]- +(+(0(),0()),-(+(0(),0()))) -1|[]-> 0()
   -(0()) <-3|0[]- -(+(0(),0())) -2|[]-> 0()
   -(+(0(),0())) <-4|0,1[]- -(+(0(),-(0()))) -0|[]-> 0()
   +(0(),0()) <-4|1[]- +(0(),-(0())) -1|[]-> 0()
  Redundant Rules Transformation:
   +(x,-(x)) -> 0()
   +(0(),0()) -> 0()
   -(0()) -> 0()
   Church Rosser Transformation Processor (kb):
    +(x,-(x)) -> 0()
    +(0(),0()) -> 0()
    -(0()) -> 0()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [0] = 5,
      
      [+](x0, x1) = x0 + x1 + 4,
      
      [-](x0) = x0 + 4
     orientation:
      +(x,-(x)) = 2x + 8 >= 5 = 0()
      
      +(0(),0()) = 14 >= 5 = 0()
      
      -(0()) = 9 >= 5 = 0()
     problem:
      
     Qed