MAYBE
Time: 6.552

Problem:
 Equations:
  virgAC(virgAC(x9,x10),x11) -> virgAC(x9,virgAC(x10,x11))
  virgAC(x9,x10) -> virgAC(x10,x9)
  *AC(*AC(x9,x10),x11) -> *AC(x9,*AC(x10,x11))
  *AC(x9,x10) -> *AC(x10,x9)
  virgAC(x9,virgAC(x10,x11)) -> virgAC(virgAC(x9,x10),x11)
  virgAC(x10,x9) -> virgAC(x9,x10)
  *AC(x9,*AC(x10,x11)) -> *AC(*AC(x9,x10),x11)
  *AC(x10,x9) -> *AC(x9,x10)
 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:
 DP Processor:
  Equations#:
   virg{AC,#}(virgAC(x9,x10),x11) -> virg{AC,#}(x9,virgAC(x10,x11))
   virg{AC,#}(x9,x10) -> virg{AC,#}(x10,x9)
   *{AC,#}(*AC(x9,x10),x11) -> *{AC,#}(x9,*AC(x10,x11))
   *{AC,#}(x9,x10) -> *{AC,#}(x10,x9)
   virg{AC,#}(x9,virgAC(x10,x11)) -> virg{AC,#}(virgAC(x9,x10),x11)
   virg{AC,#}(x10,x9) -> virg{AC,#}(x9,x10)
   *{AC,#}(x9,*AC(x10,x11)) -> *{AC,#}(*AC(x9,x10),x11)
   *{AC,#}(x10,x9) -> *{AC,#}(x9,x10)
  DPs:
   substt#(ef(x),y) -> substt#(x,y)
   substf#(Pe(x),y) -> substt#(x,y)
   substf#(neg(f),s) -> substf#(f,s)
   substf#(neg(f),s) -> neg#(substf(f,s))
   substf#(and(f,g),s) -> substf#(g,s)
   substf#(and(f,g),s) -> substf#(f,s)
   substf#(and(f,g),s) -> and#(substf(f,s),substf(g,s))
   substf#(or(f,g),s) -> substf#(g,s)
   substf#(or(f,g),s) -> substf#(f,s)
   substf#(or(f,g),s) -> or#(substf(f,s),substf(g,s))
   substf#(imp(f,g),s) -> substf#(g,s)
   substf#(imp(f,g),s) -> substf#(f,s)
   substf#(imp(f,g),s) -> imp#(substf(f,s),substf(g,s))
   substf#(forall(f),s) -> ron#(s,shift())
   substf#(forall(f),s) -> .#(1(),ron(s,shift()))
   substf#(forall(f),s) -> substf#(f,.(1(),ron(s,shift())))
   substf#(exists(f),s) -> ron#(s,shift())
   substf#(exists(f),s) -> .#(1(),ron(s,shift()))
   substf#(exists(f),s) -> substf#(f,.(1(),ron(s,shift())))
   substf#(exists(f),s) -> exists#(substf(f,.(1(),ron(s,shift()))))
   substt#(substt(x,s),t) -> ron#(s,t)
   substt#(substt(x,s),t) -> substt#(x,ron(s,t))
   substf#(substf(f,s),t) -> ron#(s,t)
   substf#(substf(f,s),t) -> substf#(f,ron(s,t))
   ron#(ron(s,t),u) -> ron#(t,u)
   ron#(ron(s,t),u) -> ron#(s,ron(t,u))
   ron#(.(x,s),t) -> ron#(s,t)
   ron#(.(x,s),t) -> substt#(x,t)
   ron#(.(x,s),t) -> .#(substt(x,t),ron(s,t))
   imp#(f,g) -> neg#(f)
   imp#(f,g) -> or#(neg(f),g)
   exists#(f) -> neg#(f)
   exists#(f) -> neg#(forall(neg(f)))
   sequent#(virgAC(convf(neg(f)),a),b) -> virg{AC,#}(convf(f),b)
   sequent#(virgAC(convf(neg(f)),a),b) -> sequent#(a,virgAC(convf(f),b))
   sequent#(convf(neg(f)),b) -> virg{AC,#}(convf(f),b)
   sequent#(convf(neg(f)),b) -> sequent#(emptyfset(),virgAC(convf(f),b))
   sequent#(a,virgAC(convf(neg(f)),b)) -> virg{AC,#}(convf(f),a)
   sequent#(a,virgAC(convf(neg(f)),b)) -> sequent#(virgAC(convf(f),a),b)
   sequent#(a,convf(neg(f))) -> virg{AC,#}(convf(f),a)
   sequent#(a,convf(neg(f))) -> sequent#(virgAC(convf(f),a),emptyfset())
   sequent#(virgAC(convf(and(f,g)),a),b) -> virg{AC,#}(convf(f),a)
   sequent#(virgAC(convf(and(f,g)),a),b) -> virg{AC,#}(convf(g),virgAC(convf(f),a))
   sequent#(virgAC(convf(and(f,g)),a),b) -> sequent#(virgAC(convf(g),virgAC(convf(f),a)),b)
   sequent#(convf(and(f,g)),b) -> virg{AC,#}(convf(f),convf(g))
   sequent#(convf(and(f,g)),b) -> sequent#(virgAC(convf(f),convf(g)),b)
   sequent#(a,virgAC(convf(or(f,g)),b)) -> virg{AC,#}(convf(f),convf(g))
   sequent#(a,virgAC(convf(or(f,g)),b)) -> virg{AC,#}(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))) -> virg{AC,#}(convf(f),convf(g))
   sequent#(a,convf(or(f,g))) -> sequent#(a,virgAC(convf(f),convf(g)))
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> virg{AC,#}(convf(g),b)
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> sequent#(a,virgAC(convf(g),b))
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> convs#(sequent(a,virgAC(convf(g),b)))
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> virg{AC,#}(convf(f),b)
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> sequent#(a,virgAC(convf(f),b))
   convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> convs#(sequent(a,virgAC(convf(f),b)))
   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)))) -> sequent#(a,convf(g))
   convs#(sequent(a,convf(and(f,g)))) -> convs#(sequent(a,convf(g)))
   convs#(sequent(a,convf(and(f,g)))) -> sequent#(a,convf(f))
   convs#(sequent(a,convf(and(f,g)))) -> convs#(sequent(a,convf(f)))
   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)) -> virg{AC,#}(convf(g),a)
   convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> sequent#(virgAC(convf(g),a),b)
   convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> convs#(sequent(virgAC(convf(g),a),b))
   convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> virg{AC,#}(convf(f),a)
   convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> sequent#(virgAC(convf(f),a),b)
   convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> convs#(sequent(virgAC(convf(f),a),b))
   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)) -> sequent#(convf(g),b)
   convs#(sequent(convf(or(f,g)),b)) -> convs#(sequent(convf(g),b))
   convs#(sequent(convf(or(f,g)),b)) -> sequent#(convf(f),b)
   convs#(sequent(convf(or(f,g)),b)) -> convs#(sequent(convf(f),b))
   convs#(sequent(convf(or(f,g)),b)) ->
   *{AC,#}(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))
   virg{AC,#}(x12,virgAC(emptyfset(),a)) -> virg{AC,#}(x12,a)
   virg{AC,#}(x13,virgAC(a,a)) -> virg{AC,#}(x13,a)
   *{AC,#}(x14,*AC(emptysset(),a)) -> *{AC,#}(x14,a)
   *{AC,#}(x15,*AC(a,a)) -> *{AC,#}(x15,a)
   *{AC,#}(x16,*AC(convs(sequent(virgAC(f,a),virgAC(g,b))),convs(sequent(a,b)))) ->
   *{AC,#}(x16,convs(sequent(a,b)))
   *{AC,#}(x17,*AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,b)))) ->
   *{AC,#}(x17,convs(sequent(a,b)))
   *{AC,#}(x18,*AC(convs(sequent(a,virgAC(f,b))),convs(sequent(a,b)))) ->
   *{AC,#}(x18,convs(sequent(a,b)))
   *{AC,#}(x19,*AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,emptyfset())))) ->
   *{AC,#}(x19,convs(sequent(a,emptyfset())))
   *{AC,#}(x20,*AC(convs(sequent(emptyfset(),b)),convs(sequent(a,virgAC(f,b))))) ->
   *{AC,#}(x20,convs(sequent(emptyfset(),b)))
   *{AC,#}(x21,*AC(convs(sequent(emptyfset(),b)),convs(sequent(a,b)))) ->
   *{AC,#}(x21,convs(sequent(emptyfset(),b)))
   *{AC,#}(x22,*AC(convs(sequent(a,emptyfset())),convs(sequent(a,b)))) ->
   *{AC,#}(x22,convs(sequent(a,emptyfset())))
   *{AC,#}(x23,*AC(convs(sequent(emptyfset(),emptyfset())),convs(sequent(a,b)))) ->
   *{AC,#}(x23,convs(sequent(emptyfset(),emptyfset())))
  Equations:
   virgAC(virgAC(x9,x10),x11) -> virgAC(x9,virgAC(x10,x11))
   virgAC(x9,x10) -> virgAC(x10,x9)
   *AC(*AC(x9,x10),x11) -> *AC(x9,*AC(x10,x11))
   *AC(x9,x10) -> *AC(x10,x9)
   virgAC(x9,virgAC(x10,x11)) -> virgAC(virgAC(x9,x10),x11)
   virgAC(x10,x9) -> virgAC(x9,x10)
   *AC(x9,*AC(x10,x11)) -> *AC(*AC(x9,x10),x11)
   *AC(x10,x9) -> *AC(x9,x10)
  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()))
  S:
   virg{AC,#}(virgAC(x24,x25),x26) -> virg{AC,#}(x24,x25)
   virg{AC,#}(x24,virgAC(x25,x26)) -> virg{AC,#}(x25,x26)
   *{AC,#}(*AC(x24,x25),x26) -> *{AC,#}(x24,x25)
   *{AC,#}(x24,*AC(x25,x26)) -> *{AC,#}(x25,x26)
  AC-EDG Processor:
   Equations#:
    virg{AC,#}(virgAC(x9,x10),x11) -> virg{AC,#}(x9,virgAC(x10,x11))
    virg{AC,#}(x9,x10) -> virg{AC,#}(x10,x9)
    *{AC,#}(*AC(x9,x10),x11) -> *{AC,#}(x9,*AC(x10,x11))
    *{AC,#}(x9,x10) -> *{AC,#}(x10,x9)
    virg{AC,#}(x9,virgAC(x10,x11)) -> virg{AC,#}(virgAC(x9,x10),x11)
    virg{AC,#}(x10,x9) -> virg{AC,#}(x9,x10)
    *{AC,#}(x9,*AC(x10,x11)) -> *{AC,#}(*AC(x9,x10),x11)
    *{AC,#}(x10,x9) -> *{AC,#}(x9,x10)
   DPs:
    substt#(ef(x),y) -> substt#(x,y)
    substf#(Pe(x),y) -> substt#(x,y)
    substf#(neg(f),s) -> substf#(f,s)
    substf#(neg(f),s) -> neg#(substf(f,s))
    substf#(and(f,g),s) -> substf#(g,s)
    substf#(and(f,g),s) -> substf#(f,s)
    substf#(and(f,g),s) -> and#(substf(f,s),substf(g,s))
    substf#(or(f,g),s) -> substf#(g,s)
    substf#(or(f,g),s) -> substf#(f,s)
    substf#(or(f,g),s) -> or#(substf(f,s),substf(g,s))
    substf#(imp(f,g),s) -> substf#(g,s)
    substf#(imp(f,g),s) -> substf#(f,s)
    substf#(imp(f,g),s) -> imp#(substf(f,s),substf(g,s))
    substf#(forall(f),s) -> ron#(s,shift())
    substf#(forall(f),s) -> .#(1(),ron(s,shift()))
    substf#(forall(f),s) -> substf#(f,.(1(),ron(s,shift())))
    substf#(exists(f),s) -> ron#(s,shift())
    substf#(exists(f),s) -> .#(1(),ron(s,shift()))
    substf#(exists(f),s) -> substf#(f,.(1(),ron(s,shift())))
    substf#(exists(f),s) -> exists#(substf(f,.(1(),ron(s,shift()))))
    substt#(substt(x,s),t) -> ron#(s,t)
    substt#(substt(x,s),t) -> substt#(x,ron(s,t))
    substf#(substf(f,s),t) -> ron#(s,t)
    substf#(substf(f,s),t) -> substf#(f,ron(s,t))
    ron#(ron(s,t),u) -> ron#(t,u)
    ron#(ron(s,t),u) -> ron#(s,ron(t,u))
    ron#(.(x,s),t) -> ron#(s,t)
    ron#(.(x,s),t) -> substt#(x,t)
    ron#(.(x,s),t) -> .#(substt(x,t),ron(s,t))
    imp#(f,g) -> neg#(f)
    imp#(f,g) -> or#(neg(f),g)
    exists#(f) -> neg#(f)
    exists#(f) -> neg#(forall(neg(f)))
    sequent#(virgAC(convf(neg(f)),a),b) -> virg{AC,#}(convf(f),b)
    sequent#(virgAC(convf(neg(f)),a),b) -> sequent#(a,virgAC(convf(f),b))
    sequent#(convf(neg(f)),b) -> virg{AC,#}(convf(f),b)
    sequent#(convf(neg(f)),b) -> sequent#(emptyfset(),virgAC(convf(f),b))
    sequent#(a,virgAC(convf(neg(f)),b)) -> virg{AC,#}(convf(f),a)
    sequent#(a,virgAC(convf(neg(f)),b)) -> sequent#(virgAC(convf(f),a),b)
    sequent#(a,convf(neg(f))) -> virg{AC,#}(convf(f),a)
    sequent#(a,convf(neg(f))) -> sequent#(virgAC(convf(f),a),emptyfset())
    sequent#(virgAC(convf(and(f,g)),a),b) -> virg{AC,#}(convf(f),a)
    sequent#(virgAC(convf(and(f,g)),a),b) -> virg{AC,#}(convf(g),virgAC(convf(f),a))
    sequent#(virgAC(convf(and(f,g)),a),b) -> sequent#(virgAC(convf(g),virgAC(convf(f),a)),b)
    sequent#(convf(and(f,g)),b) -> virg{AC,#}(convf(f),convf(g))
    sequent#(convf(and(f,g)),b) -> sequent#(virgAC(convf(f),convf(g)),b)
    sequent#(a,virgAC(convf(or(f,g)),b)) -> virg{AC,#}(convf(f),convf(g))
    sequent#(a,virgAC(convf(or(f,g)),b)) -> virg{AC,#}(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))) -> virg{AC,#}(convf(f),convf(g))
    sequent#(a,convf(or(f,g))) -> sequent#(a,virgAC(convf(f),convf(g)))
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> virg{AC,#}(convf(g),b)
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> sequent#(a,virgAC(convf(g),b))
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> convs#(sequent(a,virgAC(convf(g),b)))
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> virg{AC,#}(convf(f),b)
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> sequent#(a,virgAC(convf(f),b))
    convs#(sequent(a,virgAC(convf(and(f,g)),b))) -> convs#(sequent(a,virgAC(convf(f),b)))
    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)))) -> sequent#(a,convf(g))
    convs#(sequent(a,convf(and(f,g)))) -> convs#(sequent(a,convf(g)))
    convs#(sequent(a,convf(and(f,g)))) -> sequent#(a,convf(f))
    convs#(sequent(a,convf(and(f,g)))) -> convs#(sequent(a,convf(f)))
    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)) -> virg{AC,#}(convf(g),a)
    convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> sequent#(virgAC(convf(g),a),b)
    convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> convs#(sequent(virgAC(convf(g),a),b))
    convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> virg{AC,#}(convf(f),a)
    convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> sequent#(virgAC(convf(f),a),b)
    convs#(sequent(virgAC(convf(or(f,g)),a),b)) -> convs#(sequent(virgAC(convf(f),a),b))
    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)) -> sequent#(convf(g),b)
    convs#(sequent(convf(or(f,g)),b)) -> convs#(sequent(convf(g),b))
    convs#(sequent(convf(or(f,g)),b)) -> sequent#(convf(f),b)
    convs#(sequent(convf(or(f,g)),b)) -> convs#(sequent(convf(f),b))
    convs#(sequent(convf(or(f,g)),b)) ->
    *{AC,#}(convs(sequent(convf(f),b)),convs(sequent(convf(g),b)))
    virg{AC,#}(x12,virgAC(emptyfset(),a)) -> virg{AC,#}(x12,a)
    virg{AC,#}(x13,virgAC(a,a)) -> virg{AC,#}(x13,a)
    *{AC,#}(x14,*AC(emptysset(),a)) -> *{AC,#}(x14,a)
    *{AC,#}(x15,*AC(a,a)) -> *{AC,#}(x15,a)
    *{AC,#}(x16,*AC(convs(sequent(virgAC(f,a),virgAC(g,b))),convs(sequent(a,b)))) ->
    *{AC,#}(x16,convs(sequent(a,b)))
    *{AC,#}(x17,*AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,b)))) ->
    *{AC,#}(x17,convs(sequent(a,b)))
    *{AC,#}(x18,*AC(convs(sequent(a,virgAC(f,b))),convs(sequent(a,b)))) ->
    *{AC,#}(x18,convs(sequent(a,b)))
    *{AC,#}(x19,*AC(convs(sequent(virgAC(f,a),b)),convs(sequent(a,emptyfset())))) ->
    *{AC,#}(x19,convs(sequent(a,emptyfset())))
    *{AC,#}(x20,*AC(convs(sequent(emptyfset(),b)),convs(sequent(a,virgAC(f,b))))) ->
    *{AC,#}(x20,convs(sequent(emptyfset(),b)))
    *{AC,#}(x21,*AC(convs(sequent(emptyfset(),b)),convs(sequent(a,b)))) ->
    *{AC,#}(x21,convs(sequent(emptyfset(),b)))
    *{AC,#}(x22,*AC(convs(sequent(a,emptyfset())),convs(sequent(a,b)))) ->
    *{AC,#}(x22,convs(sequent(a,emptyfset())))
    *{AC,#}(x23,*AC(convs(sequent(emptyfset(),emptyfset())),convs(sequent(a,b)))) ->
    *{AC,#}(x23,convs(sequent(emptyfset(),emptyfset())))
   Equations:
    virgAC(virgAC(x9,x10),x11) -> virgAC(x9,virgAC(x10,x11))
    virgAC(x9,x10) -> virgAC(x10,x9)
    *AC(*AC(x9,x10),x11) -> *AC(x9,*AC(x10,x11))
    *AC(x9,x10) -> *AC(x10,x9)
    virgAC(x9,virgAC(x10,x11)) -> virgAC(virgAC(x9,x10),x11)
    virgAC(x10,x9) -> virgAC(x9,x10)
    *AC(x9,*AC(x10,x11)) -> *AC(*AC(x9,x10),x11)
    *AC(x10,x9) -> *AC(x9,x10)
   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()))
   S:
    virg{AC,#}(virgAC(x24,x25),x26) -> virg{AC,#}(x24,x25)
    virg{AC,#}(x24,virgAC(x25,x26)) -> virg{AC,#}(x25,x26)
    *{AC,#}(*AC(x24,x25),x26) -> *{AC,#}(x24,x25)
    *{AC,#}(x24,*AC(x25,x26)) -> *{AC,#}(x25,x26)
   Open