MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d) -> f10001(a, b, c, d)
		(?, 1)    f2(a, b, c, d) -> f2(a, b, c, d)
		(?, 1)    f2(a, b, c, d) -> f10001(a, b, c, d)
		(?, 1)    f2(a, b, c, d) -> f1200(b, b, c, d)
		(?, 1)    f2200(a, b, c, d) -> f10000(a, b, 0, d) [ c = 0 ]
		(?, 1)    f12(a, b, c, d) -> f12(a, b, c, d)
		(?, 1)    f100(a, b, c, d) -> f110(a, 1, c, d)
		(?, 1)    f110(a, b, c, d) -> f120(a, 2, c, d)
		(?, 1)    f120(a, b, c, d) -> f120(a, b, c, d)
		(?, 1)    f1200(a, b, c, d) -> f1200(a, b, c, d)
		(1, 1)    f0(a, b, c, d) -> f2(a, 2, c, d)
		(1, 1)    f0(a, b, c, d) -> f10001(a, 1, c, d)
		(1, 1)    f0(a, b, c, d) -> f110(1, 1, c, d)
		(1, 1)    f0(a, b, c, d) -> f12(b, 2, c, d)
		(?, 1)    f12(a, b, c, d) -> f10001(a, b, c, 1)
		(1, 1)    f0(a, b, c, d) -> f10001(b, b, c, 1)
		(1, 1)    f0(a, b, c, d) -> f10001(b, 1, c, 1)
		(?, 1)    f100(a, b, c, d) -> f10001(a, b, c, 1)
		(?, 1)    f110(a, b, c, d) -> f10001(a, b, c, 1)
		(?, 1)    f120(a, b, c, d) -> f10001(a, b, c, 1)
		(?, 1)    f1000(a, b, c, d) -> f1200(a, 2, c, d)
		(?, 1)    f1000(a, b, c, d) -> f10001(a, b, c, 1)
		(?, 1)    f1200(a, b, c, d) -> f10001(a, b, c, 1)
		(?, 1)    f1000(a, b, c, d) -> f10001(a, 1, c, 1)
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [c].
We thus obtain the following problem:
2:	T:
		(?, 1)    f1000(c) -> f10001(c)
		(?, 1)    f1200(c) -> f10001(c)
		(?, 1)    f1000(c) -> f10001(c)
		(?, 1)    f1000(c) -> f1200(c)
		(?, 1)    f120(c) -> f10001(c)
		(?, 1)    f110(c) -> f10001(c)
		(?, 1)    f100(c) -> f10001(c)
		(1, 1)    f0(c) -> f10001(c)
		(1, 1)    f0(c) -> f10001(c)
		(?, 1)    f12(c) -> f10001(c)
		(1, 1)    f0(c) -> f12(c)
		(1, 1)    f0(c) -> f110(c)
		(1, 1)    f0(c) -> f10001(c)
		(1, 1)    f0(c) -> f2(c)
		(?, 1)    f1200(c) -> f1200(c)
		(?, 1)    f120(c) -> f120(c)
		(?, 1)    f110(c) -> f120(c)
		(?, 1)    f100(c) -> f110(c)
		(?, 1)    f12(c) -> f12(c)
		(?, 1)    f2200(c) -> f10000(0) [ c = 0 ]
		(?, 1)    f2(c) -> f1200(c)
		(?, 1)    f2(c) -> f10001(c)
		(?, 1)    f2(c) -> f2(c)
		(1, 1)    f0(c) -> f10001(c)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f1000(c) -> f1200(c)
		(1, 1)    f0(c) -> f12(c)
		(1, 1)    f0(c) -> f110(c)
		(1, 1)    f0(c) -> f2(c)
		(?, 1)    f1200(c) -> f1200(c)
		(?, 1)    f120(c) -> f120(c)
		(?, 1)    f110(c) -> f120(c)
		(?, 1)    f100(c) -> f110(c)
		(?, 1)    f12(c) -> f12(c)
		(?, 1)    f2(c) -> f1200(c)
		(?, 1)    f2(c) -> f2(c)
	start location:	f0
	leaf cost:	13

Testing for reachability in the complexity graph removes the following transitions from problem 3:
	f1000(c) -> f1200(c)
	f100(c) -> f110(c)
We thus obtain the following problem:
4:	T:
		(?, 1)    f1200(c) -> f1200(c)
		(?, 1)    f120(c) -> f120(c)
		(?, 1)    f2(c) -> f2(c)
		(?, 1)    f2(c) -> f1200(c)
		(?, 1)    f110(c) -> f120(c)
		(?, 1)    f12(c) -> f12(c)
		(1, 1)    f0(c) -> f2(c)
		(1, 1)    f0(c) -> f110(c)
		(1, 1)    f0(c) -> f12(c)
	start location:	f0
	leaf cost:	13

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(?, 1)    f1200(c) -> f1200(c)
		(?, 1)    f120(c) -> f120(c)
		(?, 1)    f2(c) -> f2(c)
		(?, 1)    f2(c) -> f1200(c)
		(1, 1)    f110(c) -> f120(c)
		(?, 1)    f12(c) -> f12(c)
		(1, 1)    f0(c) -> f2(c)
		(1, 1)    f0(c) -> f110(c)
		(1, 1)    f0(c) -> f12(c)
	start location:	f0
	leaf cost:	13

A polynomial rank function with
	Pol(f1200) = 0
	Pol(f120) = 0
	Pol(f2) = 1
	Pol(f110) = 0
	Pol(f12) = 0
	Pol(f0) = 1
orients all transitions weakly and the transition
	f2(c) -> f1200(c)
strictly and produces the following problem:
6:	T:
		(?, 1)    f1200(c) -> f1200(c)
		(?, 1)    f120(c) -> f120(c)
		(?, 1)    f2(c) -> f2(c)
		(1, 1)    f2(c) -> f1200(c)
		(1, 1)    f110(c) -> f120(c)
		(?, 1)    f12(c) -> f12(c)
		(1, 1)    f0(c) -> f2(c)
		(1, 1)    f0(c) -> f110(c)
		(1, 1)    f0(c) -> f12(c)
	start location:	f0
	leaf cost:	13

Complexity upper bound ?

Time: 0.259 sec (SMT: 0.243 sec)