Term Rewriting System R:
[X, X0, X1, Xs, Ys, A, B, Fs, Gs, NF, F1, F2, V, Left, Right, G1, G2, F]
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))
intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) -> intersect'ii'out
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))
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(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'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'2d(F1), Fs), Gs), NF) -> u'7'1(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(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(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(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'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'2d(G1), Gs)), NF) -> u'13'1(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, nil), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2))
u'3'1(reduce'ii'out) -> reduce'ii'out
u'4'1(reduce'ii'out) -> reduce'ii'out
u'5'1(reduce'ii'out) -> reduce'ii'out
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
u'7'1(reduce'ii'out) -> reduce'ii'out
u'8'1(reduce'ii'out) -> reduce'ii'out
u'9'1(reduce'ii'out) -> reduce'ii'out
u'10'1(reduce'ii'out) -> reduce'ii'out
u'11'1(reduce'ii'out) -> reduce'ii'out
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
u'13'1(reduce'ii'out) -> reduce'ii'out
u'14'1(reduce'ii'out) -> reduce'ii'out
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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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)
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)
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)
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)
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)
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))

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Polynomial Ordering
       →DP Problem 2
         ↳Remaining


Dependency Pairs:

INTERSECT'II'IN(cons(X0, Xs), Ys) -> INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(Xs, cons(X0, Ys)) -> INTERSECT'II'IN(Xs, Ys)


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))
intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) -> intersect'ii'out
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))
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(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'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'2d(F1), Fs), Gs), NF) -> u'7'1(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(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(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(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'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'2d(G1), Gs)), NF) -> u'13'1(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, nil), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2))
u'3'1(reduce'ii'out) -> reduce'ii'out
u'4'1(reduce'ii'out) -> reduce'ii'out
u'5'1(reduce'ii'out) -> reduce'ii'out
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
u'7'1(reduce'ii'out) -> reduce'ii'out
u'8'1(reduce'ii'out) -> reduce'ii'out
u'9'1(reduce'ii'out) -> reduce'ii'out
u'10'1(reduce'ii'out) -> reduce'ii'out
u'11'1(reduce'ii'out) -> reduce'ii'out
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
u'13'1(reduce'ii'out) -> reduce'ii'out
u'14'1(reduce'ii'out) -> reduce'ii'out
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





The following dependency pair can be strictly oriented:

INTERSECT'II'IN(cons(X0, Xs), Ys) -> INTERSECT'II'IN(Xs, Ys)


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(INTERSECT'II'IN(x1, x2))=  x1  
  POL(cons(x1, x2))=  1 + x2  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 3
             ↳Polynomial Ordering
       →DP Problem 2
         ↳Remaining


Dependency Pair:

INTERSECT'II'IN(Xs, cons(X0, Ys)) -> INTERSECT'II'IN(Xs, Ys)


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))
intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) -> intersect'ii'out
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))
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(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'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'2d(F1), Fs), Gs), NF) -> u'7'1(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(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(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(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'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'2d(G1), Gs)), NF) -> u'13'1(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, nil), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2))
u'3'1(reduce'ii'out) -> reduce'ii'out
u'4'1(reduce'ii'out) -> reduce'ii'out
u'5'1(reduce'ii'out) -> reduce'ii'out
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
u'7'1(reduce'ii'out) -> reduce'ii'out
u'8'1(reduce'ii'out) -> reduce'ii'out
u'9'1(reduce'ii'out) -> reduce'ii'out
u'10'1(reduce'ii'out) -> reduce'ii'out
u'11'1(reduce'ii'out) -> reduce'ii'out
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
u'13'1(reduce'ii'out) -> reduce'ii'out
u'14'1(reduce'ii'out) -> reduce'ii'out
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





The following dependency pair can be strictly oriented:

INTERSECT'II'IN(Xs, cons(X0, Ys)) -> INTERSECT'II'IN(Xs, Ys)


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(INTERSECT'II'IN(x1, x2))=  x2  
  POL(cons(x1, x2))=  1 + x2  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 3
             ↳Polo
             ...
               →DP Problem 4
                 ↳Dependency Graph
       →DP Problem 2
         ↳Remaining


Dependency Pair:


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))
intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) -> intersect'ii'out
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))
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(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'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'2d(F1), Fs), Gs), NF) -> u'7'1(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(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(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(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'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'2d(G1), Gs)), NF) -> u'13'1(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, nil), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2))
u'3'1(reduce'ii'out) -> reduce'ii'out
u'4'1(reduce'ii'out) -> reduce'ii'out
u'5'1(reduce'ii'out) -> reduce'ii'out
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
u'7'1(reduce'ii'out) -> reduce'ii'out
u'8'1(reduce'ii'out) -> reduce'ii'out
u'9'1(reduce'ii'out) -> reduce'ii'out
u'10'1(reduce'ii'out) -> reduce'ii'out
u'11'1(reduce'ii'out) -> reduce'ii'out
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
u'13'1(reduce'ii'out) -> reduce'ii'out
u'14'1(reduce'ii'out) -> reduce'ii'out
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





Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

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(Fs, cons(x'2d(G1), Gs)), NF) -> REDUCE'II'IN(sequent(cons(G1, Fs), 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'2b(G1, G2), Gs)), NF) -> REDUCE'II'IN(sequent(Fs, cons(G1, 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'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(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)) -> REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
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(x'2d(F1), Fs), Gs), NF) -> REDUCE'II'IN(sequent(Fs, cons(F1, 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(x'2a(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN(sequent(cons(F1, cons(F2, 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)
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'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(if(A, B), Fs), Gs), NF) -> REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)


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))
intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) -> intersect'ii'out
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))
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(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'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'2d(F1), Fs), Gs), NF) -> u'7'1(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(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(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(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'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'2d(G1), Gs)), NF) -> u'13'1(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, nil), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2))
u'3'1(reduce'ii'out) -> reduce'ii'out
u'4'1(reduce'ii'out) -> reduce'ii'out
u'5'1(reduce'ii'out) -> reduce'ii'out
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
u'7'1(reduce'ii'out) -> reduce'ii'out
u'8'1(reduce'ii'out) -> reduce'ii'out
u'9'1(reduce'ii'out) -> reduce'ii'out
u'10'1(reduce'ii'out) -> reduce'ii'out
u'11'1(reduce'ii'out) -> reduce'ii'out
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
u'13'1(reduce'ii'out) -> reduce'ii'out
u'14'1(reduce'ii'out) -> reduce'ii'out
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




Termination of R could not be shown.
Duration:
0:08 minutes