Runtime Complexity of the query pattern
member(a,g)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Clauses:

member(X, .(Y, Xs)) :- member(X, Xs).
member(X, .(X, Xs)).

Query: member(a,g)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

member(X, .(X, Xs)).
member(X, .(Y, Xs)) :- member(X, Xs).

Query: member(a,g)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: member(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: member(T1, T2), SCOPE: 1, CLAUSE: 0 | member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | member(T1, .(T7, T8)), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX5 is free\nX6 is free\nmember(T1, T2) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: member(T1, .(T7, T8)), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: member(T23, T22)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: member(T37, T36)\n\nT35 is ground\nT36 is ground\nX5 is free\nX6 is free\nmember(T1, .(T35, T36)) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 20 [arrowhead = none ];
20 -> 3;

21 [label="EVAL with clause\nmember(X5, .(X5, X6)).\nand substitutionT1 -> T7,\nX5 -> T7,\nX6 -> T8,\nT2 -> .(T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 21 [arrowhead = none ];
21 -> 6;

22 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 22 [arrowhead = none ];
22 -> 7;

23 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 23 [arrowhead = none ];
23 -> 10;

24 [label="EVAL with clause\nmember(X30, .(X31, X32)) :- member(X30, X32).\nand substitutionT1 -> T37,\nX30 -> T37,\nX31 -> T35,\nX32 -> T36,\nT2 -> .(T35, T36),\nT34 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 24 [arrowhead = none ];
24 -> 18;

25 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 25 [arrowhead = none ];
25 -> 19;

26 [label="ONLY EVAL with clause\nmember(X17, .(X18, X19)) :- member(X17, X19).\nand substitutionT1 -> T23,\nX17 -> T23,\nT7 -> T21,\nX18 -> T21,\nT8 -> T22,\nX19 -> T22,\nT20 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 26 [arrowhead = none ];
26 -> 13;

27 [label="INSTANCE with matching:\nT1 -> T23\nT2 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
13 -> 27 [arrowhead = none , style=dashed];
27 -> 2[style=dashed];

28 [label="INSTANCE with matching:\nT1 -> T37\nT2 -> T36", fontsize=14, style = filled, fillcolor = lightgrey];
18 -> 28 [arrowhead = none , style=dashed];
28 -> 2[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(.(z0, z1)) → f2_out1(z0)
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1(z0), .(z1, z2)) → f2_out1(z0)
U2(f2_out1(z0), .(z1, z2)) → f2_out1(z0)

Tuples:

F2_IN(.(z0, z1)) → c1(U1'(f2_in(z1), .(z0, z1)), F2_IN(z1))
F2_IN(.(z0, z1)) → c2(U2'(f2_in(z1), .(z0, z1)), F2_IN(z1))

S tuples:

F2_IN(.(z0, z1)) → c1(U1'(f2_in(z1), .(z0, z1)), F2_IN(z1))
F2_IN(.(z0, z1)) → c2(U2'(f2_in(z1), .(z0, z1)), F2_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(.(z0, z1)) → f2_out1(z0)
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1(z0), .(z1, z2)) → f2_out1(z0)
U2(f2_out1(z0), .(z1, z2)) → f2_out1(z0)

Tuples:

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

S tuples:

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [2] + x₂   
POL(F2_IN(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(.(z0, z1)) → f2_out1(z0)
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1(z0), .(z1, z2)) → f2_out1(z0)
U2(f2_out1(z0), .(z1, z2)) → f2_out1(z0)

Tuples:

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

S tuples:none
K tuples:

F2_IN(.(z0, z1)) → c1(F2_IN(z1))
F2_IN(.(z0, z1)) → c2(F2_IN(z1))

Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

(9) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(10) BOUNDS(O(1), O(1))

(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: member(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: member(T1, T2), SCOPE: 1, CLAUSE: 0 | member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | member(T1, .(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX3 is free\nX4 is free\nmember(T1, T2) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: member(T1, .(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: member(T13, T12)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: member(T13, T12), SCOPE: 2, CLAUSE: 0 | member(T13, T12), SCOPE: 2, CLAUSE: 1\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | member(T13, .(T18, T19)), SCOPE: 2, CLAUSE: 1\n\nT18 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: member(T13, T12), SCOPE: 2, CLAUSE: 1\n\nT12 is ground\nX15 is free\nX16 is free\nmember(T13, T12) !=? member(X15, .(X15, X16))", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: member(T13, .(T18, T19)), SCOPE: 2, CLAUSE: 1\n\nT18 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: member(T34, T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: member(T48, T47)\n\nT46 is ground\nT47 is ground\nX15 is free\nX16 is free\nmember(T13, .(T46, T47)) !=? member(X15, .(X15, X16))", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: member(T59, T58)\n\nT57 is ground\nT58 is ground\nX3 is free\nX4 is free\nmember(T1, .(T57, T58)) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: member(T59, T58), SCOPE: 3, CLAUSE: 0 | member(T59, T58), SCOPE: 3, CLAUSE: 1\n\nT57 is ground\nT58 is ground\nX3 is free\nX4 is free\nmember(T1, .(T57, T58)) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true | member(T59, .(T64, T65)), SCOPE: 3, CLAUSE: 1\n\nT57 is ground\nT64 is ground\nT65 is ground\nX3 is free\nX4 is free\nmember(T1, .(T57, .(T64, T65))) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: member(T59, T58), SCOPE: 3, CLAUSE: 1\n\nT57 is ground\nT58 is ground\nX3 is free\nX4 is free\nX57 is free\nX58 is free\nmember(T1, .(T57, T58)) !=? member(X3, .(X3, X4))\nmember(T59, T58) !=? member(X57, .(X57, X58))", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: member(T59, .(T64, T65)), SCOPE: 3, CLAUSE: 1\n\nT57 is ground\nT64 is ground\nT65 is ground\nX3 is free\nX4 is free\nmember(T1, .(T57, .(T64, T65))) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: member(T80, T79)\n\nT57 is ground\nT78 is ground\nT79 is ground\nX3 is free\nX4 is free\nmember(T1, .(T57, .(T78, T79))) !=? member(X3, .(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: member(T94, T93)\n\nT57 is ground\nT92 is ground\nT93 is ground\nX3 is free\nX4 is free\nX57 is free\nX58 is free\nmember(T1, .(T57, .(T92, T93))) !=? member(X3, .(X3, X4))\nmember(T59, .(T92, T93)) !=? member(X57, .(X57, X58))", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 33 [arrowhead = none ];
33 -> 4;

34 [label="EVAL with clause\nmember(X3, .(X3, X4)).\nand substitutionT1 -> T5,\nX3 -> T5,\nX4 -> T6,\nT2 -> .(T5, T6)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 34 [arrowhead = none ];
34 -> 5;

35 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 35 [arrowhead = none ];
35 -> 8;

36 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 36 [arrowhead = none ];
36 -> 9;

37 [label="EVAL with clause\nmember(X50, .(X51, X52)) :- member(X50, X52).\nand substitutionT1 -> T59,\nX50 -> T59,\nX51 -> T57,\nX52 -> T58,\nT2 -> .(T57, T58),\nT56 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 37 [arrowhead = none ];
37 -> 22;

38 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 38 [arrowhead = none ];
38 -> 23;

39 [label="ONLY EVAL with clause\nmember(X8, .(X9, X10)) :- member(X8, X10).\nand substitutionT1 -> T13,\nX8 -> T13,\nT5 -> T11,\nX9 -> T11,\nT6 -> T12,\nX10 -> T12,\nT10 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 39 [arrowhead = none ];
39 -> 11;

40 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
11 -> 40 [arrowhead = none ];
40 -> 12;

41 [label="EVAL with clause\nmember(X15, .(X15, X16)).\nand substitutionT13 -> T18,\nX15 -> T18,\nX16 -> T19,\nT12 -> .(T18, T19)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 41 [arrowhead = none ];
41 -> 14;

42 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 42 [arrowhead = none ];
42 -> 15;

43 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 43 [arrowhead = none ];
43 -> 16;

44 [label="EVAL with clause\nmember(X40, .(X41, X42)) :- member(X40, X42).\nand substitutionT13 -> T48,\nX40 -> T48,\nX41 -> T46,\nX42 -> T47,\nT12 -> .(T46, T47),\nT45 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 44 [arrowhead = none ];
44 -> 20;

45 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 45 [arrowhead = none ];
45 -> 21;

46 [label="ONLY EVAL with clause\nmember(X27, .(X28, X29)) :- member(X27, X29).\nand substitutionT13 -> T34,\nX27 -> T34,\nT18 -> T32,\nX28 -> T32,\nT19 -> T33,\nX29 -> T33,\nT31 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 46 [arrowhead = none ];
46 -> 17;

47 [label="INSTANCE with matching:\nT1 -> T34\nT2 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
17 -> 47 [arrowhead = none , style=dashed];
47 -> 1[style=dashed];

48 [label="INSTANCE with matching:\nT1 -> T48\nT2 -> T47", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 48 [arrowhead = none , style=dashed];
48 -> 1[style=dashed];

49 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 49 [arrowhead = none ];
49 -> 24;

50 [label="EVAL with clause\nmember(X57, .(X57, X58)).\nand substitutionT59 -> T64,\nX57 -> T64,\nX58 -> T65,\nT58 -> .(T64, T65)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 50 [arrowhead = none ];
50 -> 25;

51 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 51 [arrowhead = none ];
51 -> 26;

52 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 52 [arrowhead = none ];
52 -> 27;

53 [label="EVAL with clause\nmember(X82, .(X83, X84)) :- member(X82, X84).\nand substitutionT59 -> T94,\nX82 -> T94,\nX83 -> T92,\nX84 -> T93,\nT58 -> .(T92, T93),\nT91 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 53 [arrowhead = none ];
53 -> 31;

54 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 54 [arrowhead = none ];
54 -> 32;

55 [label="ONLY EVAL with clause\nmember(X69, .(X70, X71)) :- member(X69, X71).\nand substitutionT59 -> T80,\nX69 -> T80,\nT64 -> T78,\nX70 -> T78,\nT65 -> T79,\nX71 -> T79,\nT77 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 55 [arrowhead = none ];
55 -> 28;

56 [label="INSTANCE with matching:\nT1 -> T80\nT2 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 56 [arrowhead = none , style=dashed];
56 -> 1[style=dashed];

57 [label="INSTANCE with matching:\nT1 -> T94\nT2 -> T93", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 57 [arrowhead = none , style=dashed];
57 -> 1[style=dashed];

}

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(.(z0, z1)) → f1_out1(z0)
f1_in(.(z0, .(z1, z2))) → f1_out1(z1)
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U2(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U3(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U4(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(U2'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(U3'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(U4'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(U2'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(U3'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(U4'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4

Defined Pair Symbols:

F1_IN

Compound Symbols:

c2, c3, c4, c5

(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(.(z0, z1)) → f1_out1(z0)
f1_in(.(z0, .(z1, z2))) → f1_out1(z1)
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U2(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U3(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U4(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4

Defined Pair Symbols:

F1_IN

Compound Symbols:

c2, c3, c4, c5

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂   
POL(F1_IN(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(.(z0, z1)) → f1_out1(z0)
f1_in(.(z0, .(z1, z2))) → f1_out1(z1)
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U2(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U3(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)
U4(f1_out1(z0), .(z1, .(z2, z3))) → f1_out1(z0)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

S tuples:none
K tuples:

F1_IN(.(z0, .(z1, z2))) → c2(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c3(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))

Defined Rule Symbols:

f1_in, U1, U2, U3, U4

Defined Pair Symbols:

F1_IN

Compound Symbols:

c2, c3, c4, c5