YES

Problem:
 not(tt()) -> ff()
 not(ff()) -> tt()
 or(tt(),x) -> tt()
 or(ff(),x) -> x
 eq(0(),0()) -> tt()
 eq(s(x),0()) -> ff()
 eq(0(),s(y)) -> ff()
 eq(s(x),s(y)) -> eq(x,y)
 main(phi) -> ver(phi,nil())
 in(x,nil()) -> ff()
 in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
 ver(Var(x),t()) -> in(x,t())
 ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
 ver(Not(phi),t()) -> not(ver(phi,t()))
 ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   main#(phi) -> ver#(phi,nil())
   in#(x,cons(a,l)) -> in#(x,l)
   in#(x,cons(a,l)) -> eq#(x,a)
   in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
   ver#(Var(x),t()) -> in#(x,t())
   ver#(Or(phi,psi),t()) -> ver#(psi,t())
   ver#(Or(phi,psi),t()) -> ver#(phi,t())
   ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
   ver#(Not(phi),t()) -> ver#(phi,t())
   ver#(Not(phi),t()) -> not#(ver(phi,t()))
   ver#(Exists(n,phi),t()) -> ver#(phi,t())
   ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
   ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
  TRS:
   not(tt()) -> ff()
   not(ff()) -> tt()
   or(tt(),x) -> tt()
   or(ff(),x) -> x
   eq(0(),0()) -> tt()
   eq(s(x),0()) -> ff()
   eq(0(),s(y)) -> ff()
   eq(s(x),s(y)) -> eq(x,y)
   main(phi) -> ver(phi,nil())
   in(x,nil()) -> ff()
   in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
   ver(Var(x),t()) -> in(x,t())
   ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
   ver(Not(phi),t()) -> not(ver(phi,t()))
   ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
  Usable Rule Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    main#(phi) -> ver#(phi,nil())
    in#(x,cons(a,l)) -> in#(x,l)
    in#(x,cons(a,l)) -> eq#(x,a)
    in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
    ver#(Var(x),t()) -> in#(x,t())
    ver#(Or(phi,psi),t()) -> ver#(psi,t())
    ver#(Or(phi,psi),t()) -> ver#(phi,t())
    ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
    ver#(Not(phi),t()) -> ver#(phi,t())
    ver#(Not(phi),t()) -> not#(ver(phi,t()))
    ver#(Exists(n,phi),t()) -> ver#(phi,t())
    ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
    ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
   TRS:
    f23(x,y) -> x
    f23(x,y) -> y
    in(x,nil()) -> ff()
    in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
    or(tt(),x) -> tt()
    or(ff(),x) -> x
    eq(0(),0()) -> tt()
    eq(s(x),0()) -> ff()
    eq(0(),s(y)) -> ff()
    eq(s(x),s(y)) -> eq(x,y)
    ver(Var(x),t()) -> in(x,t())
    ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
    ver(Not(phi),t()) -> not(ver(phi,t()))
    ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
    not(tt()) -> ff()
    not(ff()) -> tt()
   TDG Processor:
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
     main#(phi) -> ver#(phi,nil())
     in#(x,cons(a,l)) -> in#(x,l)
     in#(x,cons(a,l)) -> eq#(x,a)
     in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
    TRS:
     f23(x,y) -> x
     f23(x,y) -> y
     in(x,nil()) -> ff()
     in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
     or(tt(),x) -> tt()
     or(ff(),x) -> x
     eq(0(),0()) -> tt()
     eq(s(x),0()) -> ff()
     eq(0(),s(y)) -> ff()
     eq(s(x),s(y)) -> eq(x,y)
     ver(Var(x),t()) -> in(x,t())
     ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
     ver(Not(phi),t()) -> not(ver(phi,t()))
     ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
     not(tt()) -> ff()
     not(ff()) -> tt()
    graph:
     in#(x,cons(a,l)) -> in#(x,l) ->
     in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
     in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> eq#(x,a)
     in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> in#(x,l)
     in#(x,cons(a,l)) -> eq#(x,a) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,t()) ->
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ->
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Not(phi),t()) -> ver#(phi,t()) ->
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Or(phi,psi),t()) -> ver#(psi,t()) ->
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     ver#(Or(phi,psi),t()) -> ver#(phi,t()) ->
     ver#(Var(x),t()) -> in#(x,t())
     ver#(Var(x),t()) -> in#(x,t()) ->
     in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
     ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> eq#(x,a)
     ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> in#(x,l)
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Exists(n,phi),t()) -> ver#(phi,t())
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Not(phi),t()) -> not#(ver(phi,t()))
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Not(phi),t()) -> ver#(phi,t())
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Or(phi,psi),t()) -> ver#(phi,t())
     main#(phi) -> ver#(phi,nil()) ->
     ver#(Or(phi,psi),t()) -> ver#(psi,t())
     main#(phi) -> ver#(phi,nil()) -> ver#(Var(x),t()) -> in#(x,t())
     eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    Restore Modifier:
     DPs:
      eq#(s(x),s(y)) -> eq#(x,y)
      main#(phi) -> ver#(phi,nil())
      in#(x,cons(a,l)) -> in#(x,l)
      in#(x,cons(a,l)) -> eq#(x,a)
      in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l))
      ver#(Var(x),t()) -> in#(x,t())
      ver#(Or(phi,psi),t()) -> ver#(psi,t())
      ver#(Or(phi,psi),t()) -> ver#(phi,t())
      ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t()))
      ver#(Not(phi),t()) -> ver#(phi,t())
      ver#(Not(phi),t()) -> not#(ver(phi,t()))
      ver#(Exists(n,phi),t()) -> ver#(phi,t())
      ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
      ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t()))
     TRS:
      not(tt()) -> ff()
      not(ff()) -> tt()
      or(tt(),x) -> tt()
      or(ff(),x) -> x
      eq(0(),0()) -> tt()
      eq(s(x),0()) -> ff()
      eq(0(),s(y)) -> ff()
      eq(s(x),s(y)) -> eq(x,y)
      main(phi) -> ver(phi,nil())
      in(x,nil()) -> ff()
      in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
      ver(Var(x),t()) -> in(x,t())
      ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
      ver(Not(phi),t()) -> not(ver(phi,t()))
      ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
     SCC Processor:
      #sccs: 3
      #rules: 7
      #arcs: 62/196
      DPs:
       ver#(Exists(n,phi),t()) -> ver#(phi,t())
       ver#(Or(phi,psi),t()) -> ver#(psi,t())
       ver#(Or(phi,psi),t()) -> ver#(phi,t())
       ver#(Not(phi),t()) -> ver#(phi,t())
       ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t()))
      TRS:
       not(tt()) -> ff()
       not(ff()) -> tt()
       or(tt(),x) -> tt()
       or(ff(),x) -> x
       eq(0(),0()) -> tt()
       eq(s(x),0()) -> ff()
       eq(0(),s(y)) -> ff()
       eq(s(x),s(y)) -> eq(x,y)
       main(phi) -> ver(phi,nil())
       in(x,nil()) -> ff()
       in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
       ver(Var(x),t()) -> in(x,t())
       ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
       ver(Not(phi),t()) -> not(ver(phi,t()))
       ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [ver#](x0, x1) = x1,
        
        [Exists](x0, x1) = 0,
        
        [Not](x0) = 0,
        
        [Or](x0, x1) = 0,
        
        [t] = 1,
        
        [Var](x0) = 0,
        
        [cons](x0, x1) = 0,
        
        [in](x0, x1) = 0,
        
        [ver](x0, x1) = 0,
        
        [nil] = 0,
        
        [main](x0) = 0,
        
        [s](x0) = 0,
        
        [eq](x0, x1) = 0,
        
        [0] = 0,
        
        [or](x0, x1) = x1,
        
        [ff] = 0,
        
        [not](x0) = 0,
        
        [tt] = 0
       orientation:
        ver#(Exists(n,phi),t()) = 1 >= 1 = ver#(phi,t())
        
        ver#(Or(phi,psi),t()) = 1 >= 1 = ver#(psi,t())
        
        ver#(Or(phi,psi),t()) = 1 >= 1 = ver#(phi,t())
        
        ver#(Not(phi),t()) = 1 >= 1 = ver#(phi,t())
        
        ver#(Exists(n,phi),t()) = 1 >= 0 = ver#(phi,cons(n,t()))
        
        not(tt()) = 0 >= 0 = ff()
        
        not(ff()) = 0 >= 0 = tt()
        
        or(tt(),x) = x >= 0 = tt()
        
        or(ff(),x) = x >= x = x
        
        eq(0(),0()) = 0 >= 0 = tt()
        
        eq(s(x),0()) = 0 >= 0 = ff()
        
        eq(0(),s(y)) = 0 >= 0 = ff()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        main(phi) = 0 >= 0 = ver(phi,nil())
        
        in(x,nil()) = 0 >= 0 = ff()
        
        in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l))
        
        ver(Var(x),t()) = 0 >= 0 = in(x,t())
        
        ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t()))
        
        ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t()))
        
        ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t()))
       problem:
        DPs:
         ver#(Exists(n,phi),t()) -> ver#(phi,t())
         ver#(Or(phi,psi),t()) -> ver#(psi,t())
         ver#(Or(phi,psi),t()) -> ver#(phi,t())
         ver#(Not(phi),t()) -> ver#(phi,t())
        TRS:
         not(tt()) -> ff()
         not(ff()) -> tt()
         or(tt(),x) -> tt()
         or(ff(),x) -> x
         eq(0(),0()) -> tt()
         eq(s(x),0()) -> ff()
         eq(0(),s(y)) -> ff()
         eq(s(x),s(y)) -> eq(x,y)
         main(phi) -> ver(phi,nil())
         in(x,nil()) -> ff()
         in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
         ver(Var(x),t()) -> in(x,t())
         ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
         ver(Not(phi),t()) -> not(ver(phi,t()))
         ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [ver#](x0, x1) = x0,
         
         [Exists](x0, x1) = x1,
         
         [Not](x0) = x0 + 1,
         
         [Or](x0, x1) = x0 + x1,
         
         [t] = 1,
         
         [Var](x0) = 0,
         
         [cons](x0, x1) = x1,
         
         [in](x0, x1) = x1,
         
         [ver](x0, x1) = 1,
         
         [nil] = 0,
         
         [main](x0) = 1,
         
         [s](x0) = x0,
         
         [eq](x0, x1) = x0 + 1,
         
         [0] = 1,
         
         [or](x0, x1) = x1,
         
         [ff] = 0,
         
         [not](x0) = 0,
         
         [tt] = 0
        orientation:
         ver#(Exists(n,phi),t()) = phi >= phi = ver#(phi,t())
         
         ver#(Or(phi,psi),t()) = phi + psi >= psi = ver#(psi,t())
         
         ver#(Or(phi,psi),t()) = phi + psi >= phi = ver#(phi,t())
         
         ver#(Not(phi),t()) = phi + 1 >= phi = ver#(phi,t())
         
         not(tt()) = 0 >= 0 = ff()
         
         not(ff()) = 0 >= 0 = tt()
         
         or(tt(),x) = x >= 0 = tt()
         
         or(ff(),x) = x >= x = x
         
         eq(0(),0()) = 2 >= 0 = tt()
         
         eq(s(x),0()) = x + 1 >= 0 = ff()
         
         eq(0(),s(y)) = 2 >= 0 = ff()
         
         eq(s(x),s(y)) = x + 1 >= x + 1 = eq(x,y)
         
         main(phi) = 1 >= 1 = ver(phi,nil())
         
         in(x,nil()) = 0 >= 0 = ff()
         
         in(x,cons(a,l)) = l >= l = or(eq(x,a),in(x,l))
         
         ver(Var(x),t()) = 1 >= 1 = in(x,t())
         
         ver(Or(phi,psi),t()) = 1 >= 1 = or(ver(phi,t()),ver(psi,t()))
         
         ver(Not(phi),t()) = 1 >= 0 = not(ver(phi,t()))
         
         ver(Exists(n,phi),t()) = 1 >= 1 = or(ver(phi,cons(n,t())),ver(phi,t()))
        problem:
         DPs:
          ver#(Exists(n,phi),t()) -> ver#(phi,t())
          ver#(Or(phi,psi),t()) -> ver#(psi,t())
          ver#(Or(phi,psi),t()) -> ver#(phi,t())
         TRS:
          not(tt()) -> ff()
          not(ff()) -> tt()
          or(tt(),x) -> tt()
          or(ff(),x) -> x
          eq(0(),0()) -> tt()
          eq(s(x),0()) -> ff()
          eq(0(),s(y)) -> ff()
          eq(s(x),s(y)) -> eq(x,y)
          main(phi) -> ver(phi,nil())
          in(x,nil()) -> ff()
          in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
          ver(Var(x),t()) -> in(x,t())
          ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
          ver(Not(phi),t()) -> not(ver(phi,t()))
          ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [ver#](x0, x1) = x0 + 1,
          
          [Exists](x0, x1) = x1,
          
          [Not](x0) = 0,
          
          [Or](x0, x1) = x0 + x1 + 1,
          
          [t] = 0,
          
          [Var](x0) = 0,
          
          [cons](x0, x1) = 0,
          
          [in](x0, x1) = 1,
          
          [ver](x0, x1) = 1,
          
          [nil] = 0,
          
          [main](x0) = x0 + 1,
          
          [s](x0) = x0,
          
          [eq](x0, x1) = x0 + 1,
          
          [0] = 1,
          
          [or](x0, x1) = x1,
          
          [ff] = 1,
          
          [not](x0) = 1,
          
          [tt] = 0
         orientation:
          ver#(Exists(n,phi),t()) = phi + 1 >= phi + 1 = ver#(phi,t())
          
          ver#(Or(phi,psi),t()) = phi + psi + 2 >= psi + 1 = ver#(psi,t())
          
          ver#(Or(phi,psi),t()) = phi + psi + 2 >= phi + 1 = ver#(phi,t())
          
          not(tt()) = 1 >= 1 = ff()
          
          not(ff()) = 1 >= 0 = tt()
          
          or(tt(),x) = x >= 0 = tt()
          
          or(ff(),x) = x >= x = x
          
          eq(0(),0()) = 2 >= 0 = tt()
          
          eq(s(x),0()) = x + 1 >= 1 = ff()
          
          eq(0(),s(y)) = 2 >= 1 = ff()
          
          eq(s(x),s(y)) = x + 1 >= x + 1 = eq(x,y)
          
          main(phi) = phi + 1 >= 1 = ver(phi,nil())
          
          in(x,nil()) = 1 >= 1 = ff()
          
          in(x,cons(a,l)) = 1 >= 1 = or(eq(x,a),in(x,l))
          
          ver(Var(x),t()) = 1 >= 1 = in(x,t())
          
          ver(Or(phi,psi),t()) = 1 >= 1 = or(ver(phi,t()),ver(psi,t()))
          
          ver(Not(phi),t()) = 1 >= 1 = not(ver(phi,t()))
          
          ver(Exists(n,phi),t()) = 1 >= 1 = or(ver(phi,cons(n,t())),ver(phi,t()))
         problem:
          DPs:
           ver#(Exists(n,phi),t()) -> ver#(phi,t())
          TRS:
           not(tt()) -> ff()
           not(ff()) -> tt()
           or(tt(),x) -> tt()
           or(ff(),x) -> x
           eq(0(),0()) -> tt()
           eq(s(x),0()) -> ff()
           eq(0(),s(y)) -> ff()
           eq(s(x),s(y)) -> eq(x,y)
           main(phi) -> ver(phi,nil())
           in(x,nil()) -> ff()
           in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
           ver(Var(x),t()) -> in(x,t())
           ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
           ver(Not(phi),t()) -> not(ver(phi,t()))
           ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
         Matrix Interpretation Processor:
          dimension: 1
          interpretation:
           [ver#](x0, x1) = x0,
           
           [Exists](x0, x1) = x1 + 1,
           
           [Not](x0) = 0,
           
           [Or](x0, x1) = 0,
           
           [t] = 0,
           
           [Var](x0) = 0,
           
           [cons](x0, x1) = 0,
           
           [in](x0, x1) = 0,
           
           [ver](x0, x1) = 0,
           
           [nil] = 0,
           
           [main](x0) = 0,
           
           [s](x0) = 0,
           
           [eq](x0, x1) = 0,
           
           [0] = 0,
           
           [or](x0, x1) = x1,
           
           [ff] = 0,
           
           [not](x0) = 0,
           
           [tt] = 0
          orientation:
           ver#(Exists(n,phi),t()) = phi + 1 >= phi = ver#(phi,t())
           
           not(tt()) = 0 >= 0 = ff()
           
           not(ff()) = 0 >= 0 = tt()
           
           or(tt(),x) = x >= 0 = tt()
           
           or(ff(),x) = x >= x = x
           
           eq(0(),0()) = 0 >= 0 = tt()
           
           eq(s(x),0()) = 0 >= 0 = ff()
           
           eq(0(),s(y)) = 0 >= 0 = ff()
           
           eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
           
           main(phi) = 0 >= 0 = ver(phi,nil())
           
           in(x,nil()) = 0 >= 0 = ff()
           
           in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l))
           
           ver(Var(x),t()) = 0 >= 0 = in(x,t())
           
           ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t()))
           
           ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t()))
           
           ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t()))
          problem:
           DPs:
            
           TRS:
            not(tt()) -> ff()
            not(ff()) -> tt()
            or(tt(),x) -> tt()
            or(ff(),x) -> x
            eq(0(),0()) -> tt()
            eq(s(x),0()) -> ff()
            eq(0(),s(y)) -> ff()
            eq(s(x),s(y)) -> eq(x,y)
            main(phi) -> ver(phi,nil())
            in(x,nil()) -> ff()
            in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
            ver(Var(x),t()) -> in(x,t())
            ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
            ver(Not(phi),t()) -> not(ver(phi,t()))
            ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
          Qed
      
      DPs:
       in#(x,cons(a,l)) -> in#(x,l)
      TRS:
       not(tt()) -> ff()
       not(ff()) -> tt()
       or(tt(),x) -> tt()
       or(ff(),x) -> x
       eq(0(),0()) -> tt()
       eq(s(x),0()) -> ff()
       eq(0(),s(y)) -> ff()
       eq(s(x),s(y)) -> eq(x,y)
       main(phi) -> ver(phi,nil())
       in(x,nil()) -> ff()
       in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
       ver(Var(x),t()) -> in(x,t())
       ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
       ver(Not(phi),t()) -> not(ver(phi,t()))
       ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [in#](x0, x1) = x1 + 1,
        
        [Exists](x0, x1) = 0,
        
        [Not](x0) = 0,
        
        [Or](x0, x1) = 0,
        
        [t] = 0,
        
        [Var](x0) = 0,
        
        [cons](x0, x1) = x1 + 1,
        
        [in](x0, x1) = 0,
        
        [ver](x0, x1) = x1,
        
        [nil] = 0,
        
        [main](x0) = 0,
        
        [s](x0) = 0,
        
        [eq](x0, x1) = 0,
        
        [0] = 0,
        
        [or](x0, x1) = x1,
        
        [ff] = 0,
        
        [not](x0) = 0,
        
        [tt] = 0
       orientation:
        in#(x,cons(a,l)) = l + 2 >= l + 1 = in#(x,l)
        
        not(tt()) = 0 >= 0 = ff()
        
        not(ff()) = 0 >= 0 = tt()
        
        or(tt(),x) = x >= 0 = tt()
        
        or(ff(),x) = x >= x = x
        
        eq(0(),0()) = 0 >= 0 = tt()
        
        eq(s(x),0()) = 0 >= 0 = ff()
        
        eq(0(),s(y)) = 0 >= 0 = ff()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        main(phi) = 0 >= 0 = ver(phi,nil())
        
        in(x,nil()) = 0 >= 0 = ff()
        
        in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l))
        
        ver(Var(x),t()) = 0 >= 0 = in(x,t())
        
        ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t()))
        
        ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t()))
        
        ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t()))
       problem:
        DPs:
         
        TRS:
         not(tt()) -> ff()
         not(ff()) -> tt()
         or(tt(),x) -> tt()
         or(ff(),x) -> x
         eq(0(),0()) -> tt()
         eq(s(x),0()) -> ff()
         eq(0(),s(y)) -> ff()
         eq(s(x),s(y)) -> eq(x,y)
         main(phi) -> ver(phi,nil())
         in(x,nil()) -> ff()
         in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
         ver(Var(x),t()) -> in(x,t())
         ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
         ver(Not(phi),t()) -> not(ver(phi,t()))
         ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
       Qed
      
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      TRS:
       not(tt()) -> ff()
       not(ff()) -> tt()
       or(tt(),x) -> tt()
       or(ff(),x) -> x
       eq(0(),0()) -> tt()
       eq(s(x),0()) -> ff()
       eq(0(),s(y)) -> ff()
       eq(s(x),s(y)) -> eq(x,y)
       main(phi) -> ver(phi,nil())
       in(x,nil()) -> ff()
       in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
       ver(Var(x),t()) -> in(x,t())
       ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
       ver(Not(phi),t()) -> not(ver(phi,t()))
       ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [eq#](x0, x1) = x1 + 1,
        
        [Exists](x0, x1) = 0,
        
        [Not](x0) = 0,
        
        [Or](x0, x1) = 0,
        
        [t] = 0,
        
        [Var](x0) = 0,
        
        [cons](x0, x1) = 0,
        
        [in](x0, x1) = 0,
        
        [ver](x0, x1) = 0,
        
        [nil] = 0,
        
        [main](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [eq](x0, x1) = 0,
        
        [0] = 0,
        
        [or](x0, x1) = x1,
        
        [ff] = 0,
        
        [not](x0) = 0,
        
        [tt] = 0
       orientation:
        eq#(s(x),s(y)) = y + 2 >= y + 1 = eq#(x,y)
        
        not(tt()) = 0 >= 0 = ff()
        
        not(ff()) = 0 >= 0 = tt()
        
        or(tt(),x) = x >= 0 = tt()
        
        or(ff(),x) = x >= x = x
        
        eq(0(),0()) = 0 >= 0 = tt()
        
        eq(s(x),0()) = 0 >= 0 = ff()
        
        eq(0(),s(y)) = 0 >= 0 = ff()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        main(phi) = 0 >= 0 = ver(phi,nil())
        
        in(x,nil()) = 0 >= 0 = ff()
        
        in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l))
        
        ver(Var(x),t()) = 0 >= 0 = in(x,t())
        
        ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t()))
        
        ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t()))
        
        ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t()))
       problem:
        DPs:
         
        TRS:
         not(tt()) -> ff()
         not(ff()) -> tt()
         or(tt(),x) -> tt()
         or(ff(),x) -> x
         eq(0(),0()) -> tt()
         eq(s(x),0()) -> ff()
         eq(0(),s(y)) -> ff()
         eq(s(x),s(y)) -> eq(x,y)
         main(phi) -> ver(phi,nil())
         in(x,nil()) -> ff()
         in(x,cons(a,l)) -> or(eq(x,a),in(x,l))
         ver(Var(x),t()) -> in(x,t())
         ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t()))
         ver(Not(phi),t()) -> not(ver(phi,t()))
         ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t()))
       Qed