YES

We show the termination of the TRS R:

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

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: |intersect'ii'in|#(Xs,cons(X0,Ys)) -> |u'1'1|#(|intersect'ii'in|(Xs,Ys))
p2: |intersect'ii'in|#(Xs,cons(X0,Ys)) -> |intersect'ii'in|#(Xs,Ys)
p3: |intersect'ii'in|#(cons(X0,Xs),Ys) -> |u'2'1|#(|intersect'ii'in|(Xs,Ys))
p4: |intersect'ii'in|#(cons(X0,Xs),Ys) -> |intersect'ii'in|#(Xs,Ys)
p5: |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))
p6: |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)
p7: |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))
p8: |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)
p9: |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))
p10: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)
p11: |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)
p12: |reduce'ii'in|#(sequent(cons(|x'2b|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,Fs),Gs),NF)
p13: |u'6'1|#(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|#(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
p14: |u'6'1|#(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |reduce'ii'in|#(sequent(cons(F2,Fs),Gs),NF)
p15: |reduce'ii'in|#(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|#(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
p16: |reduce'ii'in|#(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(Fs,cons(F1,Gs)),NF)
p17: |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))
p18: |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)
p19: |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))
p20: |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)
p21: |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)))
p22: |reduce'ii'in|#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> |reduce'ii'in|#(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))
p23: |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))
p24: |reduce'ii'in|#(sequent(Fs,cons(|x'2b|(G1,G2),Gs)),NF) -> |reduce'ii'in|#(sequent(Fs,cons(G1,cons(G2,Gs))),NF)
p25: |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)
p26: |reduce'ii'in|#(sequent(Fs,cons(|x'2a|(G1,G2),Gs)),NF) -> |reduce'ii'in|#(sequent(Fs,cons(G1,Gs)),NF)
p27: |u'12'1|#(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|#(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
p28: |u'12'1|#(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |reduce'ii'in|#(sequent(Fs,cons(G2,Gs)),NF)
p29: |reduce'ii'in|#(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|#(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
p30: |reduce'ii'in|#(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |reduce'ii'in|#(sequent(cons(G1,Fs),Gs),NF)
p31: |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))))
p32: |reduce'ii'in|#(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> |reduce'ii'in|#(sequent(nil(),Gs),sequent(Left,cons(p(V),Right)))
p33: |reduce'ii'in|#(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|#(|intersect'ii'in|(F1,F2))
p34: |reduce'ii'in|#(sequent(nil(),nil()),sequent(F1,F2)) -> |intersect'ii'in|#(F1,F2)
p35: |tautology'i'in|#(F) -> |u'16'1|#(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
p36: |tautology'i'in|#(F) -> |reduce'ii'in|#(sequent(nil(),cons(F,nil())),sequent(nil(),nil()))

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The estimated dependency graph contains the following SCCs:

  {p6, p8, p10, p11, p12, p14, p16, p18, p20, p22, p24, p25, p26, p28, p30, p32}
  {p2, p4}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: |reduce'ii'in|#(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> |reduce'ii'in|#(sequent(nil(),Gs),sequent(Left,cons(p(V),Right)))
p2: |reduce'ii'in|#(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |reduce'ii'in|#(sequent(cons(G1,Fs),Gs),NF)
p3: |reduce'ii'in|#(sequent(Fs,cons(|x'2a|(G1,G2),Gs)),NF) -> |reduce'ii'in|#(sequent(Fs,cons(G1,Gs)),NF)
p4: |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)
p5: |u'12'1|#(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |reduce'ii'in|#(sequent(Fs,cons(G2,Gs)),NF)
p6: |reduce'ii'in|#(sequent(Fs,cons(|x'2b|(G1,G2),Gs)),NF) -> |reduce'ii'in|#(sequent(Fs,cons(G1,cons(G2,Gs))),NF)
p7: |reduce'ii'in|#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> |reduce'ii'in|#(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))
p8: |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)
p9: |reduce'ii'in|#(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(Fs,cons(F1,Gs)),NF)
p10: |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)
p11: |reduce'ii'in|#(sequent(cons(|x'2b|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,Fs),Gs),NF)
p12: |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)
p13: |u'6'1|#(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |reduce'ii'in|#(sequent(cons(F2,Fs),Gs),NF)
p14: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)
p15: |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)
p16: |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)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = ((0,1),(0,1)) x1 + x2
        sequent_A(x1,x2) = x1 + x2 + (1,0)
        nil_A() = (0,1)
        cons_A(x1,x2) = ((0,0),(1,1)) x1 + x2 + (1,2)
        p_A(x1) = ((0,0),(1,1)) x1 + (1,1)
        |x'2d|_A(x1) = ((0,0),(1,1)) x1 + (1,1)
        |x'2a|_A(x1,x2) = ((0,1),(1,0)) x1 + ((0,1),(1,0)) x2 + (1,1)
        |u'12'1|#_A(x1,x2,x3,x4,x5) = ((0,1),(0,1)) x2 + ((1,1),(1,1)) x3 + ((0,1),(0,1)) x4 + x5 + (3,2)
        |reduce'ii'in|_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (7,3)
        |reduce'ii'out|_A() = (1,1)
        |x'2b|_A(x1,x2) = ((1,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (0,3)
        iff_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (13,1)
        if_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (1,5)
        |u'6'1|#_A(x1,x2,x3,x4,x5) = ((1,1),(1,1)) x2 + ((0,1),(0,1)) x3 + ((0,1),(0,1)) x4 + x5 + (3,2)
        |u'1'1|_A(x1) = ((0,0),(1,0)) x1 + (2,0)
        |intersect'ii'out|_A() = (1,1)
        |u'2'1|_A(x1) = (3,1)
        |intersect'ii'in|_A(x1,x2) = ((0,0),(1,0)) x2 + (3,2)
        |u'6'2|_A(x1) = (2,1)
        |u'12'2|_A(x1) = ((0,1),(0,0)) x1 + (0,1)
        |u'15'1|_A(x1) = ((0,0),(1,1)) x1 + (2,0)
        |u'3'1|_A(x1) = (2,1)
        |u'4'1|_A(x1) = (7,1)
        |u'5'1|_A(x1) = x1 + (0,1)
        |u'6'1|_A(x1,x2,x3,x4,x5) = (3,4)
        |u'7'1|_A(x1) = x1 + (0,1)
        |u'8'1|_A(x1) = ((0,1),(0,0)) x1 + (1,1)
        |u'9'1|_A(x1) = (2,1)
        |u'10'1|_A(x1) = x1 + (0,1)
        |u'11'1|_A(x1) = x1
        |u'12'1|_A(x1,x2,x3,x4,x5) = x5 + (5,1)
        |u'13'1|_A(x1) = x1 + (0,1)
        |u'14'1|_A(x1) = (2,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = ((1,0),(1,0)) x2
        sequent_A(x1,x2) = ((1,1),(1,1)) x2 + (1,1)
        nil_A() = (1,1)
        cons_A(x1,x2) = (1,1)
        p_A(x1) = (0,0)
        |x'2d|_A(x1) = (1,0)
        |x'2a|_A(x1,x2) = (1,1)
        |u'12'1|#_A(x1,x2,x3,x4,x5) = x3 + x5
        |reduce'ii'in|_A(x1,x2) = (4,4)
        |reduce'ii'out|_A() = (1,1)
        |x'2b|_A(x1,x2) = (1,1)
        iff_A(x1,x2) = (1,1)
        if_A(x1,x2) = (1,1)
        |u'6'1|#_A(x1,x2,x3,x4,x5) = ((1,0),(1,0)) x5 + (1,1)
        |u'1'1|_A(x1) = (0,2)
        |intersect'ii'out|_A() = (2,3)
        |u'2'1|_A(x1) = (0,1)
        |intersect'ii'in|_A(x1,x2) = (1,1)
        |u'6'2|_A(x1) = (6,0)
        |u'12'2|_A(x1) = (2,1)
        |u'15'1|_A(x1) = (5,0)
        |u'3'1|_A(x1) = (5,0)
        |u'4'1|_A(x1) = (0,0)
        |u'5'1|_A(x1) = (2,1)
        |u'6'1|_A(x1,x2,x3,x4,x5) = (5,5)
        |u'7'1|_A(x1) = ((1,0),(1,0)) x1
        |u'8'1|_A(x1) = (0,0)
        |u'9'1|_A(x1) = (0,5)
        |u'10'1|_A(x1) = ((0,1),(0,0)) x1 + (0,4)
        |u'11'1|_A(x1) = x1 + (2,0)
        |u'12'1|_A(x1,x2,x3,x4,x5) = ((1,1),(1,0)) x5 + (3,5)
        |u'13'1|_A(x1) = (1,4)
        |u'14'1|_A(x1) = (5,5)
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p9, p11, p12, p13

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: |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)
p2: |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)
p3: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)
p4: |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)
p5: |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)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: |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)
p2: |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)
p3: |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)
p4: |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)
p5: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = ((0,1),(0,0)) x1 + x2
        sequent_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(1,0)) x2
        cons_A(x1,x2) = x1 + (1,1)
        iff_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,1)
        |x'2a|_A(x1,x2) = x1 + (0,1)
        if_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (2,1)
        |x'2b|_A(x1,x2) = ((1,1),(0,1)) x2 + (1,0)
        |x'2d|_A(x1) = ((0,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = x2
        sequent_A(x1,x2) = (1,1)
        cons_A(x1,x2) = ((0,0),(1,1)) x1 + (1,1)
        iff_A(x1,x2) = ((0,1),(1,0)) x1 + ((1,1),(1,0)) x2 + (1,1)
        |x'2a|_A(x1,x2) = ((0,0),(1,1)) x1 + (1,1)
        if_A(x1,x2) = ((1,1),(1,1)) x1 + (1,1)
        |x'2b|_A(x1,x2) = ((1,1),(1,0)) x2 + (1,1)
        |x'2d|_A(x1) = (1,1)
    

The next rules are strictly ordered:

  p1, p3

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: |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)
p2: |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)
p3: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The estimated dependency graph contains the following SCCs:

  {p2, p3}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: |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)
p2: |reduce'ii'in|#(sequent(cons(|x'2a|(F1,F2),Fs),Gs),NF) -> |reduce'ii'in|#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = x1 + x2
        sequent_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (0,1)
        cons_A(x1,x2) = x1 + (1,1)
        iff_A(x1,x2) = ((0,1),(1,1)) x1 + ((1,1),(1,0)) x2 + (1,3)
        |x'2a|_A(x1,x2) = x1 + (1,1)
        if_A(x1,x2) = ((0,1),(1,1)) x1 + ((0,1),(1,0)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |reduce'ii'in|#_A(x1,x2) = x2
        sequent_A(x1,x2) = x2 + (1,1)
        cons_A(x1,x2) = (1,1)
        iff_A(x1,x2) = x2 + (1,0)
        |x'2a|_A(x1,x2) = (1,0)
        if_A(x1,x2) = (1,1)
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: |intersect'ii'in|#(Xs,cons(X0,Ys)) -> |intersect'ii'in|#(Xs,Ys)
p2: |intersect'ii'in|#(cons(X0,Xs),Ys) -> |intersect'ii'in|#(Xs,Ys)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |intersect'ii'in|#_A(x1,x2) = ((1,1),(0,1)) x2
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |intersect'ii'in|#_A(x1,x2) = ((0,0),(1,1)) x2
        cons_A(x1,x2) = ((1,0),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: |intersect'ii'in|#(cons(X0,Xs),Ys) -> |intersect'ii'in|#(Xs,Ys)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: |intersect'ii'in|#(cons(X0,Xs),Ys) -> |intersect'ii'in|#(Xs,Ys)

and R consists of:

r1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
r2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
r3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
r5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
r6: |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))
r7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r8: |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))
r9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r10: |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))
r11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r12: |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)
r13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
r14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
r16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r17: |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))
r18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r19: |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))
r20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r21: |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)))
r22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r23: |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))
r24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r25: |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)
r26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
r27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
r28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
r29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r30: |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))))
r31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
r32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
r33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
r34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
r35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |intersect'ii'in|#_A(x1,x2) = ((1,1),(1,1)) x1 + x2
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        |intersect'ii'in|#_A(x1,x2) = ((0,1),(1,0)) x1 + x2
        cons_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,0),(1,0)) x2 + (1,1)
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.