/home/nowonder/forschung/aprove/TPDB05/TRS/currying/D33/12.trs

The program

(VAR x y z)
(RULES
  app(not, app(not, x)) -> x
  app(not, app(app(or, x), y)) -> app(app(and, app(not, x)), app(not, y))
  app(not, app(app(and, x), y)) -> app(app(or, app(not, x)), app(not, y))
  app(app(and, x), app(app(or, y), z)) -> app(app(or, app(app(and, x), y)), app(app(and, x), z))
  app(app(and, app(app(or, y), z)), x) -> app(app(or, app(app(and, x), y)), app(app(and, x), z))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend