(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN(Xs, cons(X0, Ys)) → U'1'1(intersect'ii'in(Xs, Ys))
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(cons(X0, Xs), Ys) → U'2'1(intersect'ii'in(Xs, Ys))
INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → U'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → U'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → U'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → U'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → U'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → U'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → U'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → U'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → U'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → U'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → U'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → U'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → REDUCE'II'IN(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))
REDUCE'II'IN(sequent(nil, nil), sequent(F1, F2)) → U'15'1(intersect'ii'in(F1, F2))
REDUCE'II'IN(sequent(nil, nil), sequent(F1, F2)) → INTERSECT'II'IN(F1, F2)
TAUTOLOGY'I'IN(F) → U'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
TAUTOLOGY'I'IN(F) → REDUCE'II'IN(sequent(nil, cons(F, nil)), sequent(nil, nil))

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 18 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
INTERSECT'II'IN(x1, x2)  =  x2
cons(x1, x2)  =  cons(x2)
intersect'ii'in(x1, x2)  =  intersect'ii'in
intersect'ii'out  =  intersect'ii'out
u'1'1(x1)  =  x1
u'2'1(x1)  =  x1
reduce'ii'in(x1, x2)  =  reduce'ii'in(x1)
sequent(x1, x2)  =  sequent
if(x1, x2)  =  if(x1, x2)
u'3'1(x1)  =  x1
x'2b(x1, x2)  =  x'2b
x'2d(x1)  =  x'2d
reduce'ii'out  =  reduce'ii'out
iff(x1, x2)  =  x1
u'4'1(x1)  =  x1
x'2a(x1, x2)  =  x'2a(x1)
u'5'1(x1)  =  x1
u'6'1(x1, x2, x3, x4, x5)  =  u'6'1
u'6'2(x1)  =  u'6'2
u'7'1(x1)  =  u'7'1
u'8'1(x1)  =  u'8'1
u'9'1(x1)  =  x1
p(x1)  =  x1
u'10'1(x1)  =  x1
u'11'1(x1)  =  x1
u'12'1(x1, x2, x3, x4, x5)  =  u'12'1
u'12'2(x1)  =  u'12'2
u'13'1(x1)  =  x1
nil  =  nil
u'14'1(x1)  =  u'14'1
u'15'1(x1)  =  u'15'1(x1)
tautology'i'in(x1)  =  tautology'i'in(x1)
u'16'1(x1)  =  u'16'1(x1)
tautology'i'out  =  tautology'i'out

Recursive path order with status [RPO].
Precedence:
x'2a1 > cons1 > intersect'ii'out > reduce'ii'out > sequent
x'2a1 > cons1 > if2 > sequent
x'2a1 > cons1 > x'2d > sequent
x'2a1 > cons1 > u'8'1 > reduce'ii'out > sequent
x'2a1 > u'12'1 > u'12'2 > reduce'ii'out > sequent
nil > reduce'ii'in1 > cons1 > intersect'ii'out > reduce'ii'out > sequent
nil > reduce'ii'in1 > cons1 > if2 > sequent
nil > reduce'ii'in1 > cons1 > x'2d > sequent
nil > reduce'ii'in1 > cons1 > u'8'1 > reduce'ii'out > sequent
nil > reduce'ii'in1 > intersect'ii'in > intersect'ii'out > reduce'ii'out > sequent
nil > reduce'ii'in1 > x'2b > sequent
nil > reduce'ii'in1 > u'6'1 > u'6'2 > reduce'ii'out > sequent
nil > reduce'ii'in1 > u'7'1 > reduce'ii'out > sequent
nil > reduce'ii'in1 > u'12'1 > u'12'2 > reduce'ii'out > sequent
nil > reduce'ii'in1 > u'14'1 > reduce'ii'out > sequent
nil > reduce'ii'in1 > u'15'11 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > cons1 > intersect'ii'out > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > cons1 > if2 > sequent
tautology'i'in1 > reduce'ii'in1 > cons1 > x'2d > sequent
tautology'i'in1 > reduce'ii'in1 > cons1 > u'8'1 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > intersect'ii'in > intersect'ii'out > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > x'2b > sequent
tautology'i'in1 > reduce'ii'in1 > u'6'1 > u'6'2 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > u'7'1 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > u'12'1 > u'12'2 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > u'14'1 > reduce'ii'out > sequent
tautology'i'in1 > reduce'ii'in1 > u'15'11 > reduce'ii'out > sequent
tautology'i'in1 > u'16'11 > tautology'i'out > sequent

Status:
cons1: multiset
intersect'ii'in: []
intersect'ii'out: multiset
reduce'ii'in1: [1]
sequent: multiset
if2: multiset
x'2b: multiset
x'2d: multiset
reduce'ii'out: multiset
x'2a1: multiset
u'6'1: multiset
u'6'2: multiset
u'7'1: multiset
u'8'1: multiset
u'12'1: multiset
u'12'2: multiset
nil: multiset
u'14'1: multiset
u'15'11: multiset
tautology'i'in1: multiset
u'16'11: multiset
tautology'i'out: multiset

The following usable rules [FROCOS05] were oriented:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
INTERSECT'II'IN(x1, x2)  =  INTERSECT'II'IN(x1)
cons(x1, x2)  =  cons(x1, x2)
intersect'ii'in(x1, x2)  =  intersect'ii'in
intersect'ii'out  =  intersect'ii'out
u'1'1(x1)  =  x1
u'2'1(x1)  =  x1
reduce'ii'in(x1, x2)  =  reduce'ii'in(x1, x2)
sequent(x1, x2)  =  sequent(x1, x2)
if(x1, x2)  =  x1
u'3'1(x1)  =  x1
x'2b(x1, x2)  =  x2
x'2d(x1)  =  x'2d(x1)
reduce'ii'out  =  reduce'ii'out
iff(x1, x2)  =  iff(x2)
u'4'1(x1)  =  u'4'1
x'2a(x1, x2)  =  x2
u'5'1(x1)  =  u'5'1
u'6'1(x1, x2, x3, x4, x5)  =  u'6'1(x2, x3, x4)
u'6'2(x1)  =  u'6'2
u'7'1(x1)  =  u'7'1
u'8'1(x1)  =  x1
u'9'1(x1)  =  u'9'1
p(x1)  =  p
u'10'1(x1)  =  u'10'1
u'11'1(x1)  =  u'11'1
u'12'1(x1, x2, x3, x4, x5)  =  u'12'1(x2, x3, x4, x5)
u'12'2(x1)  =  u'12'2
u'13'1(x1)  =  x1
nil  =  nil
u'14'1(x1)  =  u'14'1
u'15'1(x1)  =  x1
tautology'i'in(x1)  =  tautology'i'in(x1)
u'16'1(x1)  =  u'16'1
tautology'i'out  =  tautology'i'out

Recursive path order with status [RPO].
Precedence:
reduce'ii'in2 > intersect'ii'in > intersect'ii'out > reduce'ii'out
reduce'ii'in2 > u'4'1 > reduce'ii'out
reduce'ii'in2 > u'5'1 > reduce'ii'out
reduce'ii'in2 > u'6'13 > sequent2 > p > cons2 > INTERSECT'II'IN1
reduce'ii'in2 > u'6'13 > sequent2 > nil > cons2 > INTERSECT'II'IN1
reduce'ii'in2 > u'6'13 > u'6'2 > reduce'ii'out
reduce'ii'in2 > u'7'1 > reduce'ii'out
reduce'ii'in2 > u'9'1 > reduce'ii'out
reduce'ii'in2 > u'10'1 > reduce'ii'out
reduce'ii'in2 > u'11'1 > reduce'ii'out
reduce'ii'in2 > u'12'14 > sequent2 > p > cons2 > INTERSECT'II'IN1
reduce'ii'in2 > u'12'14 > sequent2 > nil > cons2 > INTERSECT'II'IN1
reduce'ii'in2 > u'12'14 > u'12'2 > reduce'ii'out
reduce'ii'in2 > u'14'1 > reduce'ii'out
x'2d1 > sequent2 > p > cons2 > INTERSECT'II'IN1
x'2d1 > sequent2 > nil > cons2 > INTERSECT'II'IN1
x'2d1 > u'7'1 > reduce'ii'out
iff1 > sequent2 > p > cons2 > INTERSECT'II'IN1
iff1 > sequent2 > nil > cons2 > INTERSECT'II'IN1
iff1 > u'4'1 > reduce'ii'out
iff1 > u'9'1 > reduce'ii'out
tautology'i'in1 > nil > cons2 > INTERSECT'II'IN1
tautology'i'in1 > u'16'1 > tautology'i'out

Status:
INTERSECT'II'IN1: multiset
cons2: multiset
intersect'ii'in: []
intersect'ii'out: multiset
reduce'ii'in2: multiset
sequent2: [2,1]
x'2d1: multiset
reduce'ii'out: multiset
iff1: multiset
u'4'1: multiset
u'5'1: multiset
u'6'13: multiset
u'6'2: multiset
u'7'1: multiset
u'9'1: multiset
p: multiset
u'10'1: multiset
u'11'1: multiset
u'12'14: multiset
u'12'2: multiset
nil: multiset
u'14'1: multiset
tautology'i'in1: multiset
u'16'1: multiset
tautology'i'out: multiset

The following usable rules [FROCOS05] were oriented:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) TRUE

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → REDUCE'II'IN(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.