YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { @(Cons(x, xs), ys) -> Cons(x, @(xs, ys))
  , @(Nil(), ys) -> ys
  , game(p1, p2, Cons(Capture(), xs)) ->
    game[Ite][False][Ite][False][Ite](True(),
                                      p1,
                                      p2,
                                      Cons(Capture(), xs))
  , game(p1, p2, Cons(Swap(), xs)) -> game(p2, p1, xs)
  , game(p1, p2, Nil()) -> @(p1, p2)
  , equal(Capture(), Capture()) -> True()
  , equal(Capture(), Swap()) -> False()
  , equal(Swap(), Capture()) -> False()
  , equal(Swap(), Swap()) -> True()
  , goal(p1, p2, moves) -> game(p1, p2, moves) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 1. The enriched problem is
compatible with the following automaton.
{ @_0(2, 2) -> 1
, @_1(2, 2) -> 1
, @_1(2, 2) -> 3
, Cons_0(2, 2) -> 1
, Cons_0(2, 2) -> 2
, Cons_0(2, 2) -> 3
, Cons_1(2, 3) -> 1
, Cons_1(2, 3) -> 3
, Cons_1(6, 2) -> 5
, Nil_0() -> 1
, Nil_0() -> 2
, Nil_0() -> 3
, game_0(2, 2, 2) -> 1
, game_1(2, 2, 2) -> 1
, Capture_0() -> 1
, Capture_0() -> 2
, Capture_0() -> 3
, Capture_1() -> 6
, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 1
, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 2
, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 3
, game[Ite][False][Ite][False][Ite]_1(4, 2, 2, 5) -> 1
, True_0() -> 1
, True_0() -> 2
, True_0() -> 3
, True_1() -> 1
, True_1() -> 4
, Swap_0() -> 1
, Swap_0() -> 2
, Swap_0() -> 3
, equal_0(2, 2) -> 1
, False_0() -> 1
, False_0() -> 2
, False_0() -> 3
, False_1() -> 1
, goal_0(2, 2, 2) -> 1
, 2 -> 1
, 2 -> 3 }

Hurray, we answered YES(?,O(n^1))