MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,?ys) -> true,
     subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     member(?x,?ys) -> if(eq(?x,?y),false,member(?x,?ys)),
     or(?x,?y) -> if(?x,true,?y),
     and(?x,?y) -> if(?x,?y,false),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     seteq(app(?xs,?ys),app(?ys,?xs)) -> true ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,nil,cons,true,false}
Defined function symbols: {eq,if,or,and,app,seteq,member,subseteq}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,?ys) -> true,
     subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     or(?x,?y) -> if(?x,true,?y),
     and(?x,?y) -> if(?x,?y,false),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     member(?x,?ys) -> if(eq(?x,?y),false,member(?x,?ys)) ]
   [ seteq(app(?xs,?ys),app(?ys,?xs)) -> true ]
Trying with:
R:
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,?ys) -> true,
     subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     or(?x,?y) -> if(?x,true,?y),
     and(?x,?y) -> if(?x,?y,false),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     member(?x,?ys) -> if(eq(?x,?y),false,member(?x,?ys)) ]
E:
   [ seteq(app(?xs,?ys),app(?ys,?xs)) = true ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool,List}
Signature:
   [ seteq : List,List -> Bool,
     subseteq : List,List -> Bool,
     member : Nat,List -> Bool,
     if : Bool,Bool,Bool -> Bool,
     eq : Nat,Nat -> Bool,
     or : Bool,Bool -> Bool,
     and : Bool,Bool -> Bool,
     app : List,List -> List,
     cons : Nat,List -> List,
     true : Bool,
     false : Bool,
     nil : List,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ seteq(?xs,?ys) -> and(subseteq(?xs,?ys),subseteq(?ys,?xs)),
     subseteq(nil,?ys) -> true,
     subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     or(?x,?y) -> if(?x,true,?y),
     and(?x,?y) -> if(?x,?y,false),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     member(?x,?ys) -> if(eq(?x,?y),false,member(?x,?ys)) ]
Conjecture Part:
   [ seteq(app(?xs,?ys),app(?ys,?xs)) = true ]
Termination proof failed.
new/seteq3.trs: Failure(unknown)
(1764 msec.)