YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  even(0) -> true
  ?1(true, x) -> true
  even(s(x)) -> ?1(odd(x), x)
  ?2(true, x) -> true
  odd(s(x)) -> ?2(even(x), x)

 DP Processor:
  DPs:
   even#(s(x)) -> odd#(x)
   even#(s(x)) -> ?1#(odd(x),x)
   odd#(s(x)) -> even#(x)
   odd#(s(x)) -> ?2#(even(x),x)
  TRS:
   even(0()) -> true()
   ?1(true(),x) -> true()
   even(s(x)) -> ?1(odd(x),x)
   ?2(true(),x) -> true()
   odd(s(x)) -> ?2(even(x),x)
  TDG Processor:
   DPs:
    even#(s(x)) -> odd#(x)
    even#(s(x)) -> ?1#(odd(x),x)
    odd#(s(x)) -> even#(x)
    odd#(s(x)) -> ?2#(even(x),x)
   TRS:
    even(0()) -> true()
    ?1(true(),x) -> true()
    even(s(x)) -> ?1(odd(x),x)
    ?2(true(),x) -> true()
    odd(s(x)) -> ?2(even(x),x)
   graph:
    odd#(s(x)) -> even#(x) -> even#(s(x)) -> ?1#(odd(x),x)
    odd#(s(x)) -> even#(x) -> even#(s(x)) -> odd#(x)
    even#(s(x)) -> odd#(x) -> odd#(s(x)) -> ?2#(even(x),x)
    even#(s(x)) -> odd#(x) -> odd#(s(x)) -> even#(x)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 4/16
    DPs:
     odd#(s(x)) -> even#(x)
     even#(s(x)) -> odd#(x)
    TRS:
     even(0()) -> true()
     ?1(true(),x) -> true()
     even(s(x)) -> ?1(odd(x),x)
     ?2(true(),x) -> true()
     odd(s(x)) -> ?2(even(x),x)
    Subterm Criterion Processor:
     simple projection:
      pi(even#) = 0
      pi(odd#) = 0
     problem:
      DPs:
       
      TRS:
       even(0()) -> true()
       ?1(true(),x) -> true()
       even(s(x)) -> ?1(odd(x),x)
       ?2(true(),x) -> true()
       odd(s(x)) -> ?2(even(x),x)
     Qed