not(and(

not(or(

and(

R

↳Dependency Pair Analysis

NOT(and(x,y)) -> NOT(x)

NOT(and(x,y)) -> NOT(y)

NOT(or(x,y)) -> AND(not(x), not(y))

NOT(or(x,y)) -> NOT(x)

NOT(or(x,y)) -> NOT(y)

AND(x, or(y,z)) -> AND(x,y)

AND(x, or(y,z)) -> AND(x,z)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****AND(***x*, or(*y*,*z*)) -> AND(*x*,*z*)**AND(***x*, or(*y*,*z*)) -> AND(*x*,*y*)**Rules:**

not(and(*x*,*y*)) -> or(not(*x*), not(*y*))

not(or(*x*,*y*)) -> and(not(*x*), not(*y*))

and(*x*, or(*y*,*z*)) -> or(and(*x*,*y*), and(*x*,*z*))**Dependency Pairs:****NOT(or(***x*,*y*)) -> NOT(*y*)**NOT(or(***x*,*y*)) -> NOT(*x*)**NOT(and(***x*,*y*)) -> NOT(*y*)**NOT(and(***x*,*y*)) -> NOT(*x*)**Rules:**

not(and(*x*,*y*)) -> or(not(*x*), not(*y*))

not(or(*x*,*y*)) -> and(not(*x*), not(*y*))

and(*x*, or(*y*,*z*)) -> or(and(*x*,*y*), and(*x*,*z*))

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****AND(***x*, or(*y*,*z*)) -> AND(*x*,*z*)**AND(***x*, or(*y*,*z*)) -> AND(*x*,*y*)**Rules:**

not(and(*x*,*y*)) -> or(not(*x*), not(*y*))

not(or(*x*,*y*)) -> and(not(*x*), not(*y*))

and(*x*, or(*y*,*z*)) -> or(and(*x*,*y*), and(*x*,*z*))**Dependency Pairs:****NOT(or(***x*,*y*)) -> NOT(*y*)**NOT(or(***x*,*y*)) -> NOT(*x*)**NOT(and(***x*,*y*)) -> NOT(*y*)**NOT(and(***x*,*y*)) -> NOT(*x*)**Rules:**

not(and(*x*,*y*)) -> or(not(*x*), not(*y*))

not(or(*x*,*y*)) -> and(not(*x*), not(*y*))

and(*x*, or(*y*,*z*)) -> or(and(*x*,*y*), and(*x*,*z*))

Duration:

0:00 minutes