NO
Rewrite Rules:
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y,?ys)) -> false,
     subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)),
     member(?x,nil) -> false,
     member(?x,cons(?y,?ys)) -> or(eq(?x,?y),member(?x,?ys)),
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     or(?x,true) -> true,
     or(true,?y) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x,false) -> false,
     and(false,?y) -> false,
     seteq(?xs,?xs) -> true,
     seteq(?xs,?ys) -> seteq(?ys,?xs) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ and(subseteq(?ys,?ys),subseteq(?ys,?ys)) = true,
     and(subseteq(?xs,?ys),subseteq(?ys,?xs)) = seteq(?ys,?xs),
     true = true,
     false = false,
     true = seteq(?xs_12,?xs_12) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
not Left-Linear, not Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y_1,?ys_1)) -> false,
     subseteq(cons(?x_2,?xs_2),?ys_2) -> and(member(?x_2,?ys_2),subseteq(?xs_2,?ys_2)),
     member(?x_3,nil) -> false,
     member(?x_4,cons(?y_4,?ys_4)) -> or(eq(?x_4,?y_4),member(?x_4,?ys_4)),
     eq(0,0) -> true,
     eq(0,s(?y_5)) -> false,
     eq(s(?x_6),0) -> false,
     eq(s(?x_7),s(?y_7)) -> eq(?x_7,?y_7),
     or(?x_8,true) -> true,
     or(true,?y_9) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x_10,false) -> false,
     and(false,?y_11) -> false,
     seteq(?xs_12,?xs_12) -> true,
     seteq(?xs_13,?ys_13) -> seteq(?ys_13,?xs_13) ]
Sort Assignment:
 0 : =>27
 s : 27=>27
 eq : 27*27=>50
 or : 50*50=>50
 and : 50*50=>50
 nil : =>45
 cons : 27*45=>45
 true : =>50
 false : =>50
 seteq : 45*45=>50
 member : 27*45=>50
 subseteq : 45*45=>50
non-linear variables: {?xs_12}
non-linear types: {45}
types leq non-linear types: {45}
rules applicable to terms of non-linear types:
   [ ]
terms of non-linear types are innermost terminating
outer CP <p,q> = <and(subseteq(?ys:45,?ys:45),subseteq(?ys:45,?ys:45)), true>
parallel reducts of p: {and(subseteq(?ys:45,?ys:45),subseteq(?ys:45,?ys:45))}
parallel reducts of q: {true}
unknown Quasi-Left-Linear & Parallel-Closed
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y_1,?ys_1)) -> false,
     subseteq(cons(?x_2,?xs_2),?ys_2) -> and(member(?x_2,?ys_2),subseteq(?xs_2,?ys_2)),
     member(?x_3,nil) -> false,
     member(?x_4,cons(?y_4,?ys_4)) -> or(eq(?x_4,?y_4),member(?x_4,?ys_4)),
     eq(0,0) -> true,
     eq(0,s(?y_5)) -> false,
     eq(s(?x_6),0) -> false,
     eq(s(?x_7),s(?y_7)) -> eq(?x_7,?y_7),
     or(?x_8,true) -> true,
     or(true,?y_9) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x_10,false) -> false,
     and(false,?y_11) -> false,
     seteq(?xs_12,?xs_12) -> true,
     seteq(?xs_13,?ys_13) -> seteq(?ys_13,?xs_13) ]
Sort Assignment:
 0 : =>27
 s : 27=>27
 eq : 27*27=>50
 or : 50*50=>50
 and : 50*50=>50
 nil : =>45
 cons : 27*45=>45
 true : =>50
 false : =>50
 seteq : 45*45=>50
 member : 27*45=>50
 subseteq : 45*45=>50
non-linear variables: {?xs,?ys,?ys_2,?x_4,?xs_12}
non-linear types: {45,27}
types leq non-linear types: {45,27}
rules applicable to terms of non-linear types:
   [ ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {}
9: {}
10: {}
11: {}
12: {}
13: {}
14: {}
15: {}
16: {}
17: {}
terms of non-linear types are innermost terminating
Critical Pair <true, and(subseteq(?xs_12,?xs_12),subseteq(?xs_12,?xs_12))> by Rules <16, 0>
no joinable sequence for some critical pairs
unknown Quasi-Linear & Linearized-Decreasing
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y_1,?ys_1)) -> false,
     subseteq(cons(?x_2,?xs_2),?ys_2) -> and(member(?x_2,?ys_2),subseteq(?xs_2,?ys_2)),
     member(?x_3,nil) -> false,
     member(?x_4,cons(?y_4,?ys_4)) -> or(eq(?x_4,?y_4),member(?x_4,?ys_4)),
     eq(0,0) -> true,
     eq(0,s(?y_5)) -> false,
     eq(s(?x_6),0) -> false,
     eq(s(?x_7),s(?y_7)) -> eq(?x_7,?y_7),
     or(?x_8,true) -> true,
     or(true,?y_9) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x_10,false) -> false,
     and(false,?y_11) -> false,
     seteq(?xs_12,?xs_12) -> true,
     seteq(?xs_13,?ys_13) -> seteq(?ys_13,?xs_13) ]
Sort Assignment:
 0 : =>27
 s : 27=>27
 eq : 27*27=>50
 or : 50*50=>50
 and : 50*50=>50
 nil : =>45
 cons : 27*45=>45
 true : =>50
 false : =>50
 seteq : 45*45=>50
 member : 27*45=>50
 subseteq : 45*45=>50
non-linear variables: {?xs,?ys,?ys_2,?x_4,?xs_12}
non-linear types: {45,27}
types leq non-linear types: {45,27}
rules applicable to terms of non-linear types:
   [ ]
terms of non-linear types are terminating
Check Joinablility of CP from NLR:
done.
Critical Pair <true, and(subseteq(?xs_12,?xs_12),subseteq(?xs_12,?xs_12))> by Rules <16, 0>
no joinable sequence for some critical pairs
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 18 rules by 3 steps unfolding
obtain 5 candidates for checking non-joinability
check by TCAP-Approximation   [ seteq(?xs:List,?ys:List) -> and(subseteq(?xs:List,?ys:List),subseteq(?ys:List,?xs:List)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y:Nat,?ys:List)) -> false,
     subseteq(cons(?x:Nat,?xs:List),?ys:List) -> and(member(?x:Nat,?ys:List),subseteq(?xs:List,?ys:List)),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> or(eq(?x:Nat,?y:Nat),member(?x:Nat,?ys:List)),
     eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     or(?x:Bool,true) -> true,
     or(true,?y:Bool) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,false) -> false,
     and(false,?y:Bool) -> false,
     seteq(?xs:List,?xs:List) -> true,
     seteq(?xs:List,?ys:List) -> seteq(?ys:List,?xs:List) ]
   [ seteq(?xs:List,?ys:List) -> and(subseteq(?xs:List,?ys:List),subseteq(?ys:List,?xs:List)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y:Nat,?ys:List)) -> false,
     subseteq(cons(?x:Nat,?xs:List),?ys:List) -> and(member(?x:Nat,?ys:List),subseteq(?xs:List,?ys:List)),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> or(eq(?x:Nat,?y:Nat),member(?x:Nat,?ys:List)),
     eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     or(?x:Bool,true) -> true,
     or(true,?y:Bool) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,false) -> false,
     and(false,?y:Bool) -> false,
     seteq(?xs:List,?xs:List) -> true,
     seteq(?xs:List,?ys:List) -> seteq(?ys:List,?xs:List) ]
   [ seteq(?xs:List,?ys:List) -> and(subseteq(?xs:List,?ys:List),subseteq(?ys:List,?xs:List)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y:Nat,?ys:List)) -> false,
     subseteq(cons(?x:Nat,?xs:List),?ys:List) -> and(member(?x:Nat,?ys:List),subseteq(?xs:List,?ys:List)),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> or(eq(?x:Nat,?y:Nat),member(?x:Nat,?ys:List)),
     eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     or(?x:Bool,true) -> true,
     or(true,?y:Bool) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,false) -> false,
     and(false,?y:Bool) -> false,
     seteq(?xs:List,?xs:List) -> true,
     seteq(?xs:List,?ys:List) -> seteq(?ys:List,?xs:List) ]
   [ seteq(?xs:List,?ys:List) -> and(subseteq(?xs:List,?ys:List),subseteq(?ys:List,?xs:List)),
     subseteq(nil,nil) -> true,
     subseteq(nil,cons(?y:Nat,?ys:List)) -> false,
     subseteq(cons(?x:Nat,?xs:List),?ys:List) -> and(member(?x:Nat,?ys:List),subseteq(?xs:List,?ys:List)),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> or(eq(?x:Nat,?y:Nat),member(?x:Nat,?ys:List)),
     eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     or(?x:Bool,true) -> true,
     or(true,?y:Bool) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,false) -> false,
     and(false,?y:Bool) -> false,
     seteq(?xs:List,?xs:List) -> true,
     seteq(?xs:List,?ys:List) -> seteq(?ys:List,?xs:List) ]
 (success)
Witness for Non-Confluence: <and(subseteq(c_1,c_1),subseteq(c_1,c_1)) <- seteq(c_1,c_1) -> true>
Direct Methods: not CR

Final result: not CR
new/seteq.trs: Success(not CR)
(18 msec.)