MAYBE
Time: 5.194

Problem:
 Equations:
  
 TRS:
  substt(ef(x),y) -> ef(substt(x,y))
  substf(Pe(x),y) -> Pe(substt(x,y))
  substf(neg(f),s) -> neg(substf(f,s))
  substf(and(f,g),s) -> and(substf(f,s),substf(g,s))
  substf(or(f,g),s) -> or(substf(f,s),substf(g,s))
  substf(imp(f,g),s) -> imp(substf(f,s),substf(g,s))
  substf(forall(f),s) -> forall(substf(f,.(1(),ron(s,shift()))))
  substf(exists(f),s) -> exists(substf(f,.(1(),ron(s,shift()))))
  substt(x,id()) -> x
  substf(f,id()) -> f
  substt(substt(x,s),t) -> substt(x,ron(s,t))
  substf(substf(f,s),t) -> substf(f,ron(s,t))
  substt(1(),.(x,s)) -> x
  ron(id(),s) -> s
  ron(shift(),.(x,s)) -> s
  ron(ron(s,t),u) -> ron(s,ron(t,u))
  ron(.(x,s),t) -> .(substt(x,t),ron(s,t))
  ron(s,id()) -> s
  .(1(),shift()) -> id()
  .(substt(1(),s),ron(shift(),s)) -> s
  virgAC(emptyfset(),a) -> a
  virgAC(a,a) -> a
  *AC(emptysset(),a) -> a
  *AC(a,a) -> a
  neg(neg(f)) -> f
  and(f,f) -> f
  or(f,f) -> f
  imp(f,g) -> or(neg(f),g)
  exists(f) -> neg(forall(neg(f)))
  sequent(virgAC(convf(neg(f)),a),b) -> sequent(a,virgAC(convf(f),b))
  sequent(convf(neg(f)),b) -> sequent(emptyfset(),virgAC(convf(f),b))
  sequent(a,virgAC(convf(neg(f)),b)) -> sequent(virgAC(convf(f),a),b)
  sequent(a,convf(neg(f))) -> sequent(virgAC(convf(f),a),emptyfset())
  sequent(virgAC(convf(and(f,g)),a),b) -> sequent(virgAC(convf(g),virgAC(convf(f),a)),b)
  sequent(convf(and(f,g)),b) -> sequent(virgAC(convf(f),convf(g)),b)
  sequent(a,virgAC(convf(or(f,g)),b)) -> sequent(a,virgAC(virgAC(convf(f),convf(g)),b))
  sequent(a,convf(or(f,g))) -> sequent(a,virgAC(convf(f),convf(g)))
  convs(sequent(a,virgAC(convf(and(f,g)),b))) ->
  *AC(convs(sequent(a,virgAC(convf(f),b))),convs(sequent(a,virgAC(convf(g),b))))
  convs(sequent(a,convf(and(f,g)))) -> *AC(convs(sequent(a,convf(f))),convs(sequent(a,convf(g))))
  convs(sequent(virgAC(convf(or(f,g)),a),b)) ->
  *AC(convs(sequent(virgAC(convf(f),a),b)),convs(sequent(virgAC(convf(g),a),b)))
  convs(sequent(convf(or(f,g)),b)) -> *AC(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))
  convs(sequent(virgAC(convf(f),a),virgAC(convf(f),b))) -> emptysset()
  convs(sequent(virgAC(convf(f),a),convf(f))) -> emptysset()
  convs(sequent(convf(f),virgAC(convf(f),b))) -> emptysset()
  convs(sequent(convf(f),convf(f))) -> emptysset()
  *AC(convs(sequent(virgAC(f,a),virgAC(g,b))),convs(sequent(a,b))) -> convs(sequent(a,b))
  *AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,b))) -> convs(sequent(a,b))
  *AC(convs(sequent(a,virgAC(f,b))),convs(sequent(a,b))) -> convs(sequent(a,b))
  *AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,emptyfset()))) -> convs(sequent(a,emptyfset()))
  *AC(convs(sequent(emptyfset(),b)),convs(sequent(a,virgAC(f,b)))) -> convs(sequent(emptyfset(),b))
  *AC(convs(sequent(emptyfset(),b)),convs(sequent(a,b))) -> convs(sequent(emptyfset(),b))
  *AC(convs(sequent(a,emptyfset())),convs(sequent(a,b))) -> convs(sequent(a,emptyfset()))
  *AC(convs(sequent(emptyfset(),emptyfset())),convs(sequent(a,b))) ->
  convs(sequent(emptyfset(),emptyfset()))

Proof:
 Open