YES(?,O(n^1))
0.00/0.63	YES(?,O(n^1))
0.00/0.63	
0.00/0.63	We are left with following problem, upon which TcT provides the
0.00/0.63	certificate YES(?,O(n^1)).
0.00/0.63	
0.00/0.63	Strict Trs:
0.00/0.63	  { @(Cons(x, xs), ys) -> Cons(x, @(xs, ys))
0.00/0.63	  , @(Nil(), ys) -> ys
0.00/0.63	  , game(p1, p2, Cons(Capture(), xs)) ->
0.00/0.63	    game[Ite][False][Ite][False][Ite](True(),
0.00/0.63	                                      p1,
0.00/0.63	                                      p2,
0.00/0.63	                                      Cons(Capture(), xs))
0.00/0.63	  , game(p1, p2, Cons(Swap(), xs)) -> game(p2, p1, xs)
0.00/0.63	  , game(p1, p2, Nil()) -> @(p1, p2)
0.00/0.63	  , equal(Capture(), Capture()) -> True()
0.00/0.63	  , equal(Capture(), Swap()) -> False()
0.00/0.63	  , equal(Swap(), Capture()) -> False()
0.00/0.63	  , equal(Swap(), Swap()) -> True()
0.00/0.63	  , goal(p1, p2, moves) -> game(p1, p2, moves) }
0.00/0.63	Obligation:
0.00/0.63	  innermost runtime complexity
0.00/0.63	Answer:
0.00/0.63	  YES(?,O(n^1))
0.00/0.63	
0.00/0.63	The problem is match-bounded by 1. The enriched problem is
0.00/0.63	compatible with the following automaton.
0.00/0.63	{ @_0(2, 2) -> 1
0.00/0.63	, @_1(2, 2) -> 1
0.00/0.63	, @_1(2, 2) -> 3
0.00/0.63	, Cons_0(2, 2) -> 1
0.00/0.63	, Cons_0(2, 2) -> 2
0.00/0.63	, Cons_0(2, 2) -> 3
0.00/0.63	, Cons_1(2, 3) -> 1
0.00/0.63	, Cons_1(2, 3) -> 3
0.00/0.63	, Cons_1(6, 2) -> 5
0.00/0.63	, Nil_0() -> 1
0.00/0.63	, Nil_0() -> 2
0.00/0.63	, Nil_0() -> 3
0.00/0.63	, game_0(2, 2, 2) -> 1
0.00/0.63	, game_1(2, 2, 2) -> 1
0.00/0.63	, Capture_0() -> 1
0.00/0.63	, Capture_0() -> 2
0.00/0.63	, Capture_0() -> 3
0.00/0.63	, Capture_1() -> 6
0.00/0.63	, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 1
0.00/0.63	, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 2
0.00/0.63	, game[Ite][False][Ite][False][Ite]_0(2, 2, 2, 2) -> 3
0.00/0.63	, game[Ite][False][Ite][False][Ite]_1(4, 2, 2, 5) -> 1
0.00/0.63	, True_0() -> 1
0.00/0.63	, True_0() -> 2
0.00/0.63	, True_0() -> 3
0.00/0.63	, True_1() -> 1
0.00/0.63	, True_1() -> 4
0.00/0.63	, Swap_0() -> 1
0.00/0.63	, Swap_0() -> 2
0.00/0.63	, Swap_0() -> 3
0.00/0.63	, equal_0(2, 2) -> 1
0.00/0.63	, False_0() -> 1
0.00/0.63	, False_0() -> 2
0.00/0.63	, False_0() -> 3
0.00/0.63	, False_1() -> 1
0.00/0.63	, goal_0(2, 2, 2) -> 1 }
0.00/0.63	
0.00/0.63	Hurray, we answered YES(?,O(n^1))
0.00/0.64	EOF