MAYBE
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/elimdup.trs
Input rules:
   [ delete(?x:Nat,nil) -> nil,
     delete(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(eq(?x:Nat,?y:Nat),cons(?y:Nat,delete(?x:Nat,?ys:List)),delete(?x:Nat,?ys:List)),
     elimdup(nil) -> nil,
     elimdup(cons(?x:Nat,?xs:List)) -> cons(?x:Nat,delete(?x:Nat,elimdup(?xs:List))),
     elimdup(cons(?x:Nat,?xs:List)) -> ifList(member(?x:Nat,?xs:List),elimdup(?xs:List),cons(?x:Nat,elimdup(?xs:List))),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> ifBool(eq(?x:Nat,?y:Nat),true,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),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?ys:List,?zs:List) -> ?ys:List,
     ifList(false,?ys:List,?zs:List) -> ?zs:List ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ delete(?x:Nat,nil) -> nil,
     delete(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(eq(?x:Nat,?y:Nat),cons(?y:Nat,delete(?x:Nat,?ys:List)),delete(?x:Nat,?ys:List)),
     elimdup(nil) -> nil,
     elimdup(cons(?x:Nat,?xs:List)) -> cons(?x:Nat,delete(?x:Nat,elimdup(?xs:List))),
     elimdup(cons(?x:Nat,?xs:List)) -> ifList(member(?x:Nat,?xs:List),elimdup(?xs:List),cons(?x:Nat,elimdup(?xs:List))),
     member(?x:Nat,nil) -> false,
     member(?x:Nat,cons(?y:Nat,?ys:List)) -> ifBool(eq(?x:Nat,?y:Nat),true,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),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?ys:List,?zs:List) -> ?ys:List,
     ifList(false,?ys:List,?zs:List) -> ?zs:List ]
Constructor pattern: [true,false,cons(?x_1,?x_2),nil,s(?x_1),0]
Defined pattern: [ifList(?x_3,?x_4,?x_5),ifBool(?x_3,?x_4,?x_5),eq(?x_2,?x_3),member(?x_2,?x_3),delete(?x_2,?x_3),elimdup(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for ifList(?x_3,?x_4,?x_5):
   [ ifList(true,?ys,?zs) -> ?ys,
     ifList(false,?ys,?zs) -> ?zs ]
candidate for ifBool(?x_3,?x_4,?x_5):
   [ ifBool(true,?y,?z) -> ?y,
     ifBool(false,?y,?z) -> ?z ]
candidate for eq(?x_2,?x_3):
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y) ]
candidate for member(?x_2,?x_3):
   [ member(?x,nil) -> false,
     member(?x,cons(?y,?ys)) -> ifBool(eq(?x,?y),true,member(?x,?ys)) ]
candidate for delete(?x_2,?x_3):
   [ delete(?x,nil) -> nil,
     delete(?x,cons(?y,?ys)) -> ifList(eq(?x,?y),cons(?y,delete(?x,?ys)),delete(?x,?ys)) ]
candidate for elimdup(?x_1):
   [ elimdup(nil) -> nil,
     elimdup(cons(?x,?xs)) -> cons(?x,delete(?x,elimdup(?xs))) ]
   [ elimdup(nil) -> nil,
     elimdup(cons(?x,?xs)) -> ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 elimdup : Mul;
 member : Mul,  delete : Mul;
 ifList : Mul,  ifBool : Mul;
 eq : Mul;
 s : Mul;
 false : Mul;
 cons : Mul;
 nil : Mul,  0 : Mul;
 true : Mul;
Rules:
   [ ifList(true,?ys,?zs) -> ?ys,
     ifList(false,?ys,?zs) -> ?zs,
     ifBool(true,?y,?z) -> ?y,
     ifBool(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,nil) -> false,
     member(?x,cons(?y,?ys)) -> ifBool(eq(?x,?y),true,member(?x,?ys)),
     delete(?x,nil) -> nil,
     delete(?x,cons(?y,?ys)) -> ifList(eq(?x,?y),cons(?y,delete(?x,?ys)),delete(?x,?ys)),
     elimdup(nil) -> nil,
     elimdup(cons(?x,?xs)) -> cons(?x,delete(?x,elimdup(?xs))) ]
Conjectures:
   [ elimdup(cons(?x,?xs)) = ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
STEP 0
ES:
   [ elimdup(cons(?x,?xs)) = ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
HS:
   [ ]
ES0:
   [ cons(?x,delete(?x,elimdup(?xs))) = ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
HS0:
   [ ]
ES1:
   [ cons(?x,delete(?x,elimdup(?xs))) = ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
HS1:
   [ ]
Expand cons(?x,delete(?x,elimdup(?xs))) = ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs)))
   [ cons(?x,delete(?x,nil)) = ifList(member(?x,nil),elimdup(nil),cons(?x,elimdup(nil))),
     cons(?x,delete(?x,cons(?x_12,delete(?x_12,elimdup(?xs_12))))) = ifList(member(?x,cons(?x_12,?xs_12)),elimdup(cons(?x_12,?xs_12)),cons(?x,elimdup(cons(?x_12,?xs_12)))) ]
ES2:
   [ cons(?x,nil) = ifList(member(?x,nil),elimdup(nil),cons(?x,elimdup(nil))),
     cons(?x,ifList(eq(?x,?x_12),cons(?x_12,delete(?x,delete(?x_12,elimdup(?xs_12)))),delete(?x,delete(?x_12,elimdup(?xs_12))))) = ifList(member(?x,cons(?x_12,?xs_12)),elimdup(cons(?x_12,?xs_12)),cons(?x,elimdup(cons(?x_12,?xs_12)))) ]
HS2:
   [ cons(?x,delete(?x,elimdup(?xs))) -> ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
STEP 1
ES:
   [ cons(?x,nil) = ifList(member(?x,nil),elimdup(nil),cons(?x,elimdup(nil))),
     cons(?x,ifList(eq(?x,?x_12),cons(?x_12,delete(?x,delete(?x_12,elimdup(?xs_12)))),delete(?x,delete(?x_12,elimdup(?xs_12))))) = ifList(member(?x,cons(?x_12,?xs_12)),elimdup(cons(?x_12,?xs_12)),cons(?x,elimdup(cons(?x_12,?xs_12)))) ]
HS:
   [ cons(?x,delete(?x,elimdup(?xs))) -> ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
ES0:
   [ cons(?x,nil) = cons(?x,nil),
     cons(?x,ifList(eq(?x,?x_12),cons(?x_12,delete(?x,delete(?x_12,elimdup(?xs_12)))),delete(?x,delete(?x_12,elimdup(?xs_12))))) = ifList(ifBool(eq(?x,?x_12),true,member(?x,?xs_12)),ifList(member(?x_12,?xs_12),elimdup(?xs_12),cons(?x_12,elimdup(?xs_12))),cons(?x,ifList(member(?x_12,?xs_12),elimdup(?xs_12),cons(?x_12,elimdup(?xs_12))))) ]
HS0:
   [ cons(?x,delete(?x,elimdup(?xs))) -> ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
ES1:
   [ cons(?x,ifList(eq(?x,?x_12),cons(?x_12,delete(?x,delete(?x_12,elimdup(?xs_12)))),delete(?x,delete(?x_12,elimdup(?xs_12))))) = ifList(ifBool(eq(?x,?x_12),true,member(?x,?xs_12)),ifList(member(?x_12,?xs_12),elimdup(?xs_12),cons(?x_12,elimdup(?xs_12))),cons(?x,ifList(member(?x_12,?xs_12),elimdup(?xs_12),cons(?x_12,elimdup(?xs_12))))) ]
HS1:
   [ cons(?x,delete(?x,elimdup(?xs))) -> ifList(member(?x,?xs),elimdup(?xs),cons(?x,elimdup(?xs))) ]
Stopped: the smallest size of equations exceeeds the limit.
Try to select different rules for member ...
check Non-Ground-Confluence...
ground constructor terms for instantiation: {true,false,nil,0,cons(0,nil),s(0)}
ground terms for instantiation: {true:Bool,false:Bool,nil:List,0:Nat,cons(0,nil):List,s(0):Nat}
obtain 19 rules by 3 steps unfolding
obtain 32 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
: Failure(unknown)
(17174 msec.)