% SZS status Success for multisets_binary.trs
57.48 (total time)

S-CONVERGENT TRS: 
false() -> eq(0(),1())
inter(empty(),x) -> empty()
true() -> eq(1(),1())
if(eq(0(),1()),x,y) -> y
inter(union(y,z),x) -> union(inter(x,y),inter(x,z))
if(eq(x,y),single(x),empty()) -> inter(single(x),single(y))
inter(single(0()),single(1())) -> empty()
if(eq(1(),1()),x,y) -> x
inter(single(1()),single(1())) -> single(1())

Total time: 57.497557