Input TRS:
    1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
    2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
    3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
    4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
    5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
    6: |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))
    7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    8: |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))
    9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    10: |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))
    11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    12: |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)
    13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|(sequent(cons(F2,Fs),Gs),NF))
    14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
    15: |reduce'ii'in|(sequent(cons(|x'2d|(F1),Fs),Gs),NF) -> |u'7'1|(|reduce'ii'in|(sequent(Fs,cons(F1,Gs)),NF))
    16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    17: |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))
    18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    19: |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))
    20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    21: |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)))
    22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    23: |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))
    24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    25: |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)
    26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|(sequent(Fs,cons(G2,Gs)),NF))
    27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
    28: |reduce'ii'in|(sequent(Fs,cons(|x'2d|(G1),Gs)),NF) -> |u'13'1|(|reduce'ii'in|(sequent(cons(G1,Fs),Gs),NF))
    29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    30: |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))))
    31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
    32: |reduce'ii'in|(sequent(nil(),nil()),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
    33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
    34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
    35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()
Number of strict rules: 35
Direct Order(PosReal,>,Poly) ... failed.
Freezing |reduce'ii'in|
1: |intersect'ii'in|(cons(X,X0),cons(X,X1)) -> |intersect'ii'out|()
2: |intersect'ii'in|(Xs,cons(X0,Ys)) -> |u'1'1|(|intersect'ii'in|(Xs,Ys))
3: |u'1'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
4: |intersect'ii'in|(cons(X0,Xs),Ys) -> |u'2'1|(|intersect'ii'in|(Xs,Ys))
5: |u'2'1|(|intersect'ii'out|()) -> |intersect'ii'out|()
6: |reduce'ii'in|❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> |u'3'1|(|reduce'ii'in|❆1_sequent(cons(|x'2b|(|x'2d|(B),A),Fs),Gs,NF))
7: |u'3'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
8: |reduce'ii'in|❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> |u'4'1|(|reduce'ii'in|❆1_sequent(cons(|x'2a|(if(A,B),if(B,A)),Fs),Gs,NF))
9: |u'4'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
10: |reduce'ii'in|❆1_sequent(cons(|x'2a|(F1,F2),Fs),Gs,NF) -> |u'5'1|(|reduce'ii'in|❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF))
11: |u'5'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
12: |reduce'ii'in|❆1_sequent(cons(|x'2b|(F1,F2),Fs),Gs,NF) -> |u'6'1|(|reduce'ii'in|❆1_sequent(cons(F1,Fs),Gs,NF),F2,Fs,Gs,NF)
13: |u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> |u'6'2|(|reduce'ii'in|❆1_sequent(cons(F2,Fs),Gs,NF))
14: |u'6'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
15: |reduce'ii'in|❆1_sequent(cons(|x'2d|(F1),Fs),Gs,NF) -> |u'7'1|(|reduce'ii'in|❆1_sequent(Fs,cons(F1,Gs),NF))
16: |u'7'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
17: |reduce'ii'in|❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> |u'8'1|(|reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(|x'2d|(B),A),Gs),NF))
18: |u'8'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
19: |reduce'ii'in|❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> |u'9'1|(|reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(if(A,B),if(B,A)),Gs),NF))
20: |u'9'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
21: |reduce'ii'in|❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> |u'10'1|(|reduce'ii'in|❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right)))
22: |u'10'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
23: |reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(G1,G2),Gs),NF) -> |u'11'1|(|reduce'ii'in|❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF))
24: |u'11'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
25: |reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(G1,G2),Gs),NF) -> |u'12'1|(|reduce'ii'in|❆1_sequent(Fs,cons(G1,Gs),NF),Fs,G2,Gs,NF)
26: |u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> |u'12'2|(|reduce'ii'in|❆1_sequent(Fs,cons(G2,Gs),NF))
27: |u'12'2|(|reduce'ii'out|()) -> |reduce'ii'out|()
28: |reduce'ii'in|❆1_sequent(Fs,cons(|x'2d|(G1),Gs),NF) -> |u'13'1|(|reduce'ii'in|❆1_sequent(cons(G1,Fs),Gs,NF))
29: |u'13'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
30: |reduce'ii'in|❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> |u'14'1|(|reduce'ii'in|❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right))))
31: |u'14'1|(|reduce'ii'out|()) -> |reduce'ii'out|()
32: |reduce'ii'in|❆1_sequent(nil(),nil(),sequent(F1,F2)) -> |u'15'1|(|intersect'ii'in|(F1,F2))
33: |u'15'1|(|intersect'ii'out|()) -> |reduce'ii'out|()
34: |tautology'i'in|(F) -> |u'16'1|(|reduce'ii'in|❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil())))
35: |u'16'1|(|reduce'ii'out|()) -> |tautology'i'out|()
36: |reduce'ii'in|(sequent(_1,_2),_3) ->= |reduce'ii'in|❆1_sequent(_1,_2,_3)
Number of strict rules: 35
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #|intersect'ii'in|(Xs,cons(X0,Ys)) -> #|u'1'1|(|intersect'ii'in|(Xs,Ys))
   #2: #|intersect'ii'in|(Xs,cons(X0,Ys)) -> #|intersect'ii'in|(Xs,Ys)
   #3: #|reduce'ii'in|❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> #|u'3'1|(|reduce'ii'in|❆1_sequent(cons(|x'2b|(|x'2d|(B),A),Fs),Gs,NF))
   #4: #|reduce'ii'in|❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> #|reduce'ii'in|❆1_sequent(cons(|x'2b|(|x'2d|(B),A),Fs),Gs,NF)
   #5: #|u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> #|u'6'2|(|reduce'ii'in|❆1_sequent(cons(F2,Fs),Gs,NF))
   #6: #|u'6'1|(|reduce'ii'out|(),F2,Fs,Gs,NF) -> #|reduce'ii'in|❆1_sequent(cons(F2,Fs),Gs,NF)
   #7: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(G1,G2),Gs),NF) -> #|u'11'1|(|reduce'ii'in|❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF))
   #8: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(G1,G2),Gs),NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF)
   #9: #|reduce'ii'in|❆1_sequent(cons(|x'2b|(F1,F2),Fs),Gs,NF) -> #|u'6'1|(|reduce'ii'in|❆1_sequent(cons(F1,Fs),Gs,NF),F2,Fs,Gs,NF)
   #10: #|reduce'ii'in|❆1_sequent(cons(|x'2b|(F1,F2),Fs),Gs,NF) -> #|reduce'ii'in|❆1_sequent(cons(F1,Fs),Gs,NF)
   #11: #|reduce'ii'in|❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> #|u'14'1|(|reduce'ii'in|❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right))))
   #12: #|reduce'ii'in|❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> #|reduce'ii'in|❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right)))
   #13: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(G1,G2),Gs),NF) -> #|u'12'1|(|reduce'ii'in|❆1_sequent(Fs,cons(G1,Gs),NF),Fs,G2,Gs,NF)
   #14: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(G1,G2),Gs),NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(G1,Gs),NF)
   #15: #|reduce'ii'in|❆1_sequent(cons(|x'2a|(F1,F2),Fs),Gs,NF) -> #|u'5'1|(|reduce'ii'in|❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF))
   #16: #|reduce'ii'in|❆1_sequent(cons(|x'2a|(F1,F2),Fs),Gs,NF) -> #|reduce'ii'in|❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF)
   #17: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2d|(G1),Gs),NF) -> #|u'13'1|(|reduce'ii'in|❆1_sequent(cons(G1,Fs),Gs,NF))
   #18: #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2d|(G1),Gs),NF) -> #|reduce'ii'in|❆1_sequent(cons(G1,Fs),Gs,NF)
   #19: #|tautology'i'in|(F) -> #|u'16'1|(|reduce'ii'in|❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil())))
   #20: #|tautology'i'in|(F) -> #|reduce'ii'in|❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil()))
   #21: #|reduce'ii'in|❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> #|u'8'1|(|reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(|x'2d|(B),A),Gs),NF))
   #22: #|reduce'ii'in|❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2b|(|x'2d|(B),A),Gs),NF)
   #23: #|reduce'ii'in|❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> #|u'9'1|(|reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(if(A,B),if(B,A)),Gs),NF))
   #24: #|reduce'ii'in|❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(|x'2a|(if(A,B),if(B,A)),Gs),NF)
   #25: #|reduce'ii'in|❆1_sequent(nil(),nil(),sequent(F1,F2)) -> #|u'15'1|(|intersect'ii'in|(F1,F2))
   #26: #|reduce'ii'in|❆1_sequent(nil(),nil(),sequent(F1,F2)) -> #|intersect'ii'in|(F1,F2)
   #27: #|u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> #|u'12'2|(|reduce'ii'in|❆1_sequent(Fs,cons(G2,Gs),NF))
   #28: #|u'12'1|(|reduce'ii'out|(),Fs,G2,Gs,NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(G2,Gs),NF)
   #29: #|reduce'ii'in|(sequent(_1,_2),_3) ->? #|reduce'ii'in|❆1_sequent(_1,_2,_3)
   #30: #|reduce'ii'in|❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> #|u'10'1|(|reduce'ii'in|❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right)))
   #31: #|reduce'ii'in|❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> #|reduce'ii'in|❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right))
   #32: #|reduce'ii'in|❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> #|u'4'1|(|reduce'ii'in|❆1_sequent(cons(|x'2a|(if(A,B),if(B,A)),Fs),Gs,NF))
   #33: #|reduce'ii'in|❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> #|reduce'ii'in|❆1_sequent(cons(|x'2a|(if(A,B),if(B,A)),Fs),Gs,NF)
   #34: #|reduce'ii'in|❆1_sequent(cons(|x'2d|(F1),Fs),Gs,NF) -> #|u'7'1|(|reduce'ii'in|❆1_sequent(Fs,cons(F1,Gs),NF))
   #35: #|reduce'ii'in|❆1_sequent(cons(|x'2d|(F1),Fs),Gs,NF) -> #|reduce'ii'in|❆1_sequent(Fs,cons(F1,Gs),NF)
   #36: #|intersect'ii'in|(cons(X0,Xs),Ys) -> #|u'2'1|(|intersect'ii'in|(Xs,Ys))
   #37: #|intersect'ii'in|(cons(X0,Xs),Ys) -> #|intersect'ii'in|(Xs,Ys)
Number of SCCs: 2, DPs: 18, edges: 167
	SCC { #2 #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
|intersect'ii'out|()	weight: 0
|u'14'1|(x1)	weight: 0
   iff(x1,x2)	weight: 0
|u'1'1|(x1)	weight: 0
#|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'13'1|(x1)	weight: 0
|u'6'2|(x1)	weight: 0
|u'9'1|(x1)	weight: 0
#|u'4'1|(x1)	weight: 0
#|intersect'ii'in|(x1,x2)	weight: x2
|u'6'1|(x1,x2,x3,x4,x5)	weight: 0
#|reduce'ii'in|(x1,x2)	weight: 0
|u'3'1|(x1)	weight: 0
|tautology'i'in|(x1)	weight: 0
|u'12'2|(x1)	weight: 0
|u'11'1|(x1)	weight: 0
|x'2d|(x1)	weight: 0
#|u'12'2|(x1)	weight: 0
#|u'2'1|(x1)	weight: 0
#|u'14'1|(x1)	weight: 0
#|u'1'1|(x1)	weight: 0
|u'8'1|(x1)	weight: 0
#|u'16'1|(x1)	weight: 0
|u'4'1|(x1)	weight: 0
#|u'11'1|(x1)	weight: 0
#|u'9'1|(x1)	weight: 0
|intersect'ii'in|(x1,x2)	weight: 0
#|tautology'i'in|(x1)	weight: 0
#|u'7'1|(x1)	weight: 0
#|u'6'2|(x1)	weight: 0
     p(x1)	weight: 0
#|u'15'1|(x1)	weight: 0
    if(x1,x2)	weight: 0
#|u'10'1|(x1)	weight: 0
   nil()	weight: 0
|tautology'i'out|()	weight: 0
#|u'6'1|(x1,x2,x3,x4,x5)	weight: 0
|reduce'ii'in|(x1,x2)	weight: 0
|u'7'1|(x1)	weight: 0
#|u'8'1|(x1)	weight: 0
|u'15'1|(x1)	weight: 0
|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'5'1|(x1)	weight: 0
|u'13'1|(x1)	weight: 0
#|u'3'1|(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: 0
|u'5'1|(x1)	weight: 0
|u'2'1|(x1)	weight: 0
|reduce'ii'out|()	weight: 0
|x'2b|(x1,x2)	weight: 0
|x'2a|(x1,x2)	weight: 0
#|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: 0
|u'10'1|(x1)	weight: 0
sequent(x1,x2)	weight: 0
|u'16'1|(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 2, DPs: 17, edges: 164
	SCC { #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
|intersect'ii'out|()	weight: 0
|u'14'1|(x1)	weight: 0
   iff(x1,x2)	weight: 0
|u'1'1|(x1)	weight: 0
#|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'13'1|(x1)	weight: 0
|u'6'2|(x1)	weight: 0
|u'9'1|(x1)	weight: 0
#|u'4'1|(x1)	weight: 0
#|intersect'ii'in|(x1,x2)	weight: x1
|u'6'1|(x1,x2,x3,x4,x5)	weight: 0
#|reduce'ii'in|(x1,x2)	weight: 0
|u'3'1|(x1)	weight: 0
|tautology'i'in|(x1)	weight: 0
|u'12'2|(x1)	weight: 0
|u'11'1|(x1)	weight: 0
|x'2d|(x1)	weight: 0
#|u'12'2|(x1)	weight: 0
#|u'2'1|(x1)	weight: 0
#|u'14'1|(x1)	weight: 0
#|u'1'1|(x1)	weight: 0
|u'8'1|(x1)	weight: 0
#|u'16'1|(x1)	weight: 0
|u'4'1|(x1)	weight: 0
#|u'11'1|(x1)	weight: 0
#|u'9'1|(x1)	weight: 0
|intersect'ii'in|(x1,x2)	weight: 0
#|tautology'i'in|(x1)	weight: 0
#|u'7'1|(x1)	weight: 0
#|u'6'2|(x1)	weight: 0
     p(x1)	weight: 0
#|u'15'1|(x1)	weight: 0
    if(x1,x2)	weight: 0
#|u'10'1|(x1)	weight: 0
   nil()	weight: 0
|tautology'i'out|()	weight: 0
#|u'6'1|(x1,x2,x3,x4,x5)	weight: 0
|reduce'ii'in|(x1,x2)	weight: 0
|u'7'1|(x1)	weight: 0
#|u'8'1|(x1)	weight: 0
|u'15'1|(x1)	weight: 0
|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'5'1|(x1)	weight: 0
|u'13'1|(x1)	weight: 0
#|u'3'1|(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: 0
|u'5'1|(x1)	weight: 0
|u'2'1|(x1)	weight: 0
|reduce'ii'out|()	weight: 0
|x'2b|(x1,x2)	weight: 0
|x'2a|(x1,x2)	weight: 0
#|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: 0
|u'10'1|(x1)	weight: 0
sequent(x1,x2)	weight: 0
|u'16'1|(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #37
Number of SCCs: 1, DPs: 16, edges: 163
	SCC { #4 #6 #8..10 #12..14 #16 #18 #22 #24 #28 #31 #33 #35 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded.
|intersect'ii'out|()	weight: (/ 1 2); (/ 3 8)
|u'14'1|(x1)	weight: (/ 1 8); (/ 1 8)
   iff(x1,x2)	weight: (/ 1 8) + x2_1 + x2_2 + x1_1 + x1_2; (/ 181313 2) + x2_1 + x2_2 + x1_1 + x1_2
|u'1'1|(x1)	weight: (/ 1 8) + x1_1 + x1_2; (/ 1 4)
#|u'12'1|(x1,x2,x3,x4,x5)	weight: (/ 95145 8) + x5_1 + x5_2 + x4_2 + x3_1 + x3_2 + x2_1 + x2_2; (/ 1 8) + x4_1 + x4_2 + x3_1 + x3_2 + x2_1 + x2_2
#|u'13'1|(x1)	weight: 0; 0
|u'6'2|(x1)	weight: (/ 1 8); (/ 1 8)
|u'9'1|(x1)	weight: x1_1; (/ 1 8)
#|u'4'1|(x1)	weight: 0; 0
#|intersect'ii'in|(x1,x2)	weight: 0; 0
|u'6'1|(x1,x2,x3,x4,x5)	weight: (/ 1 8); (/ 1 8)
#|reduce'ii'in|(x1,x2)	weight: 0; 0
|u'3'1|(x1)	weight: x1_2; x1_1
|tautology'i'in|(x1)	weight: 0; 0
|u'12'2|(x1)	weight: (/ 1 8); x1_2
|u'11'1|(x1)	weight: (/ 1 8); (/ 1 8)
|x'2d|(x1)	weight: (/ 1 8) + x1_2; (/ 236089 8) + x1_1
#|u'12'2|(x1)	weight: 0; 0
#|u'2'1|(x1)	weight: 0; 0
#|u'14'1|(x1)	weight: 0; 0
#|u'1'1|(x1)	weight: 0; 0
|u'8'1|(x1)	weight: (/ 1 8); x1_1
#|u'16'1|(x1)	weight: 0; 0
|u'4'1|(x1)	weight: x1_2; x1_1
#|u'11'1|(x1)	weight: 0; 0
#|u'9'1|(x1)	weight: 0; 0
|intersect'ii'in|(x1,x2)	weight: (/ 1 8) + x2_1 + x1_1; (/ 1 8) + x2_2 + x1_2
#|tautology'i'in|(x1)	weight: 0; 0
#|u'7'1|(x1)	weight: 0; 0
#|u'6'2|(x1)	weight: 0; 0
     p(x1)	weight: x1_1; x1_2
#|u'15'1|(x1)	weight: 0; 0
    if(x1,x2)	weight: (/ 106465 8) + x2_1 + x2_2 + x1_1 + x1_2; (/ 52147 2)
#|u'10'1|(x1)	weight: 0; 0
   nil()	weight: 0; 0
|tautology'i'out|()	weight: 0; 0
#|u'6'1|(x1,x2,x3,x4,x5)	weight: x5_1 + x5_2 + x4_2 + x3_1 + x3_2 + x2_1 + x2_2 + x1_1 + x1_2; (/ 1 8) + x4_1 + x4_2 + x3_1 + x3_2 + x2_1 + x2_2
|reduce'ii'in|(x1,x2)	weight: 0; 0
|u'7'1|(x1)	weight: (/ 1 8); x1_1
#|u'8'1|(x1)	weight: 0; 0
|u'15'1|(x1)	weight: x1_1 + x1_2; (/ 1 8) + x1_1
|u'12'1|(x1,x2,x3,x4,x5)	weight: x1_2; x1_2
#|u'5'1|(x1)	weight: 0; 0
|u'13'1|(x1)	weight: (/ 1 8); x1_1
#|u'3'1|(x1)	weight: 0; 0
  cons(x1,x2)	weight: (/ 1 8) + x2_1; x2_2 + x1_1 + x1_2
|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: (/ 1 8); (/ 1 8)
|u'5'1|(x1)	weight: x1_2; x1_1
|u'2'1|(x1)	weight: (/ 3 8); x1_1 + x1_2
|reduce'ii'out|()	weight: (/ 1 8); (/ 1 8)
|x'2b|(x1,x2)	weight: (/ 20105 8) + x2_1 + x1_2; (/ 58857 8) + x2_2 + x1_1
|x'2a|(x1,x2)	weight: (/ 71689 8) + x2_2 + x1_1; (/ 23457 8) + x2_1 + x1_2
#|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: x3_1 + x3_2 + x2_2 + x1_1 + x1_2; x2_1 + x2_2 + x1_1 + x1_2
|u'10'1|(x1)	weight: (/ 1 8); (/ 1 8)
sequent(x1,x2)	weight: (/ 1 8); (/ 1 8)
|u'16'1|(x1)	weight: 0; 0
    Usable rules: { 6..31 }
    Removed DPs: #4 #6 #8..10 #13 #14 #16 #18 #22 #24 #28 #31 #33 #35
Number of SCCs: 2, DPs: 1, edges: 1
	SCC { #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
|intersect'ii'out|()	weight: 0
|u'14'1|(x1)	weight: (/ 1 2)
   iff(x1,x2)	weight: (/ 1 4)
|u'1'1|(x1)	weight: (/ 1 2)
#|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'13'1|(x1)	weight: 0
|u'6'2|(x1)	weight: (/ 1 4) + x1
|u'9'1|(x1)	weight: 0
#|u'4'1|(x1)	weight: 0
#|intersect'ii'in|(x1,x2)	weight: 0
|u'6'1|(x1,x2,x3,x4,x5)	weight: (/ 1 4) + x1
#|reduce'ii'in|(x1,x2)	weight: 0
|u'3'1|(x1)	weight: (/ 1 4) + x1
|tautology'i'in|(x1)	weight: 0
|u'12'2|(x1)	weight: 0
|u'11'1|(x1)	weight: (/ 1 4)
|x'2d|(x1)	weight: (/ 1 4)
#|u'12'2|(x1)	weight: 0
#|u'2'1|(x1)	weight: 0
#|u'14'1|(x1)	weight: 0
#|u'1'1|(x1)	weight: 0
|u'8'1|(x1)	weight: 0
#|u'16'1|(x1)	weight: 0
|u'4'1|(x1)	weight: (/ 1 2)
#|u'11'1|(x1)	weight: 0
#|u'9'1|(x1)	weight: 0
|intersect'ii'in|(x1,x2)	weight: (/ 1 4)
#|tautology'i'in|(x1)	weight: 0
#|u'7'1|(x1)	weight: 0
#|u'6'2|(x1)	weight: 0
     p(x1)	weight: (/ 1 4)
#|u'15'1|(x1)	weight: 0
    if(x1,x2)	weight: (/ 1 4)
#|u'10'1|(x1)	weight: 0
   nil()	weight: 0
|tautology'i'out|()	weight: 0
#|u'6'1|(x1,x2,x3,x4,x5)	weight: 0
|reduce'ii'in|(x1,x2)	weight: 0
|u'7'1|(x1)	weight: (/ 1 4) + x1
#|u'8'1|(x1)	weight: 0
|u'15'1|(x1)	weight: 0
|u'12'1|(x1,x2,x3,x4,x5)	weight: 0
#|u'5'1|(x1)	weight: 0
|u'13'1|(x1)	weight: (/ 1 4)
#|u'3'1|(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: (/ 1 4)
|u'5'1|(x1)	weight: (/ 1 2)
|u'2'1|(x1)	weight: (/ 1 4) + x1
|reduce'ii'out|()	weight: 0
|x'2b|(x1,x2)	weight: (/ 1 4)
|x'2a|(x1,x2)	weight: (/ 1 4)
#|reduce'ii'in|❆1_sequent(x1,x2,x3)	weight: x2
|u'10'1|(x1)	weight: (/ 1 2)
sequent(x1,x2)	weight: (/ 1 4)
|u'16'1|(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12
Number of SCCs: 1, DPs: 0, edges: 0
YES