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

(0) Obligation:

Clauses:

overlap(Xs, Ys) :- ','(member(X, Xs), member(X, Ys)).
member(X, Y) :- ','(no(empty(Y)), head(Y, X)).
member(X, Y) :- ','(no(empty(Y)), ','(tail(Y, T), member(X, T))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: overlap(g,g)

(1) 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: overlap(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: overlap(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(member(X9, T5), member(X9, T6))\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 1 | ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(','(no(empty(T10)), head(T10, X21)), member(X21, T6)) | ','(member(X9, T10), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT10 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(','(no(empty(T10)), head(T10, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 8 | ','(','(no(empty(T10)), head(T10, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T10), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT10 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(','(call(empty(T14)), ','(!_3, failure(a))), ','(head(T14, X21), member(X21, T6))) | ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(empty(T14), ','(','(!_3, failure(a)), ','(head(T14, X21), member(X21, T6)))) | ?_4 | ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(empty(T14), ','(','(!_3, failure(a)), ','(head(T14, X21), member(X21, T6)))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(','(!_3, failure(a)), ','(head([], X21), member(X21, T6))) | ?_5 | ?_4 | ','(','(no(empty([])), head([], X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, []), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ?_5 | ?_4 | ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free\nempty(T14) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(failure(a), ','(head([], X21), member(X21, T6))) | ','(member(X9, []), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(failure(a), ','(head([], X21), member(X21, T6))), SCOPE: 6, CLAUSE: 10 | ?_6 | ','(member(X9, []), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX9 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ?_6 | ','(member(X9, []), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(member(X9, []), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6))\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 8 | ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 9\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(call(empty([])), ','(!_7, failure(a))), ','(','(tail([], X44), member(X45, X44)), member(X45, T6))) | ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 9\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(empty([]), ','(','(!_7, failure(a)), ','(','(tail([], X44), member(X45, X44)), member(X45, T6)))) | ?_8 | ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 9\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(empty([]), ','(','(!_7, failure(a)), ','(','(tail([], X44), member(X45, X44)), member(X45, T6)))), SCOPE: 9, CLAUSE: 7 | ?_9 | ?_8 | ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 9\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(','(!_7, failure(a)), ','(','(tail([], X44), member(X45, X44)), member(X45, T6))) | ?_9 | ?_8 | ','(','(no(empty([])), ','(tail([], X44), member(X45, X44))), member(X45, T6)), SCOPE: 7, CLAUSE: 9\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(failure(a), ','(','(tail([], X44), member(X45, X44)), member(X45, T6)))\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(failure(a), ','(','(tail([], X44), member(X45, X44)), member(X45, T6))), SCOPE: 10, CLAUSE: 10\n\nT6 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ?_4 | ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free\nempty(T14) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(','(no(empty(T14)), head(T14, X21)), member(X21, T6)), SCOPE: 3, CLAUSE: 9 | ?_3 | ','(member(X9, T14), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT14 is ground\nX9 is free\nX21 is free\nempty(T14) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(head(T19, X21), member(X21, T6)) | ?_3 | ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(head(T19, X21), member(X21, T6)), SCOPE: 11, CLAUSE: 3 | ','(head(T19, X21), member(X21, T6)), SCOPE: 11, CLAUSE: 4 | ?_11 | ?_3 | ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(head(T19, X21), member(X21, T6)), SCOPE: 11, CLAUSE: 4 | ?_11 | ?_3 | ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nempty(T19) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: member(T25, T6) | ?_11 | ?_3 | ','(member(X9, .(T25, T26)), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT25 is ground\nT26 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_11 | ?_3 | ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nX72 is free\nX73 is free\nempty(T19) !=? empty([])\nhead(T19, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: member(T25, T6)\n\nT6 is ground\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ?_11 | ?_3 | ','(member(X9, .(T25, T26)), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT25 is ground\nT26 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: member(T25, T6), SCOPE: 12, CLAUSE: 1 | member(T25, T6), SCOPE: 12, CLAUSE: 2\n\nT6 is ground\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(no(empty(T36)), head(T36, T35)) | member(T35, T36), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(empty(T36)), head(T36, T35)), SCOPE: 13, CLAUSE: 8 | ','(no(empty(T36)), head(T36, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T36), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(','(call(empty(T39)), ','(!_13, failure(a))), head(T39, T35)) | ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(empty(T39), ','(','(!_13, failure(a)), head(T39, T35))) | ?_14 | ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(empty(T39), ','(','(!_13, failure(a)), head(T39, T35))), SCOPE: 15, CLAUSE: 7 | ?_15 | ?_14 | ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(','(!_13, failure(a)), head([], T35)) | ?_15 | ?_14 | ','(no(empty([])), head([], T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, []), SCOPE: 12, CLAUSE: 2\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ?_15 | ?_14 | ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground\nempty(T39) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(failure(a), head([], T35)) | member(T35, []), SCOPE: 12, CLAUSE: 2\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(failure(a), head([], T35)), SCOPE: 16, CLAUSE: 10 | ?_16 | member(T35, []), SCOPE: 12, CLAUSE: 2\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_16 | member(T35, []), SCOPE: 12, CLAUSE: 2\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: member(T35, []), SCOPE: 12, CLAUSE: 2\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(no(empty([])), ','(tail([], X97), member(T43, X97)))\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 8 | ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 9\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(','(call(empty([])), ','(!_17, failure(a))), ','(tail([], X97), member(T43, X97))) | ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 9\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(empty([]), ','(','(!_17, failure(a)), ','(tail([], X97), member(T43, X97)))) | ?_18 | ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 9\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(empty([]), ','(','(!_17, failure(a)), ','(tail([], X97), member(T43, X97)))), SCOPE: 19, CLAUSE: 7 | ?_19 | ?_18 | ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 9\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(','(!_17, failure(a)), ','(tail([], X97), member(T43, X97))) | ?_19 | ?_18 | ','(no(empty([])), ','(tail([], X97), member(T43, X97))), SCOPE: 17, CLAUSE: 9\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(failure(a), ','(tail([], X97), member(T43, X97)))\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(failure(a), ','(tail([], X97), member(T43, X97))), SCOPE: 20, CLAUSE: 10\n\nT43 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ?_14 | ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground\nempty(T39) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(no(empty(T39)), head(T39, T35)), SCOPE: 13, CLAUSE: 9 | ?_13 | member(T35, T39), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT39 is ground\nempty(T39) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: head(T48, T35) | ?_13 | member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nempty(T48) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: head(T48, T35), SCOPE: 21, CLAUSE: 3 | head(T48, T35), SCOPE: 21, CLAUSE: 4 | ?_21 | ?_13 | member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nempty(T48) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: head(T48, T35), SCOPE: 21, CLAUSE: 4 | ?_21 | ?_13 | member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nempty(T48) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: true | ?_21 | ?_13 | member(T54, .(T54, T55)), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_21 | ?_13 | member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nX115 is free\nX116 is free\nempty(T48) !=? empty([])\nhead(T48, T35) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ?_21 | ?_13 | member(T54, .(T54, T55)), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ?_13 | member(T54, .(T54, T55)), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: member(T54, .(T54, T55)), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(no(empty(.(T61, T62))), ','(tail(.(T61, T62), X127), member(T61, X127)))\n\nT61 is ground\nT62 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(no(empty(.(T61, T62))), ','(tail(.(T61, T62), X127), member(T61, X127))), SCOPE: 22, CLAUSE: 8 | ','(no(empty(.(T61, T62))), ','(tail(.(T61, T62), X127), member(T61, X127))), SCOPE: 22, CLAUSE: 9\n\nT61 is ground\nT62 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(','(call(empty(.(T68, T69))), ','(!_22, failure(a))), ','(tail(.(T68, T69), X127), member(T68, X127))) | ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(empty(.(T68, T69)), ','(','(!_22, failure(a)), ','(tail(.(T68, T69), X127), member(T68, X127)))) | ?_23 | ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(empty(.(T68, T69)), ','(','(!_22, failure(a)), ','(tail(.(T68, T69), X127), member(T68, X127)))), SCOPE: 24, CLAUSE: 7 | ?_24 | ?_23 | ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ?_24 | ?_23 | ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ?_23 | ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(no(empty(.(T68, T69))), ','(tail(.(T68, T69), X127), member(T68, X127))), SCOPE: 22, CLAUSE: 9\n\nT68 is ground\nT69 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(tail(.(T75, T76), X127), member(T75, X127))\n\nT75 is ground\nT76 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(tail(.(T75, T76), X127), member(T75, X127)), SCOPE: 25, CLAUSE: 5 | ','(tail(.(T75, T76), X127), member(T75, X127)), SCOPE: 25, CLAUSE: 6\n\nT75 is ground\nT76 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(tail(.(T75, T76), X127), member(T75, X127)), SCOPE: 25, CLAUSE: 6\n\nT75 is ground\nT76 is ground\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: member(T84, T85)\n\nT84 is ground\nT85 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ?_13 | member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nX115 is free\nX116 is free\nempty(T48) !=? empty([])\nhead(T48, T35) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: member(T35, T48), SCOPE: 12, CLAUSE: 2\n\nT35 is ground\nT48 is ground\nX115 is free\nX116 is free\nempty(T48) !=? empty([])\nhead(T48, T35) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(no(empty(T94)), ','(tail(T94, X163), member(T93, X163)))\n\nT93 is ground\nT94 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T94) !=? empty([])\nhead(T94, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(no(empty(T94)), ','(tail(T94, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 8 | ','(no(empty(T94)), ','(tail(T94, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT94 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T94) !=? empty([])\nhead(T94, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(','(call(empty(T98)), ','(!_26, failure(a))), ','(tail(T98, X163), member(T93, X163))) | ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(empty(T98), ','(','(!_26, failure(a)), ','(tail(T98, X163), member(T93, X163)))) | ?_27 | ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(empty(T98), ','(','(!_26, failure(a)), ','(tail(T98, X163), member(T93, X163)))), SCOPE: 28, CLAUSE: 7 | ?_28 | ?_27 | ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ?_28 | ?_27 | ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ?_27 | ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(no(empty(T98)), ','(tail(T98, X163), member(T93, X163))), SCOPE: 26, CLAUSE: 9\n\nT93 is ground\nT98 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T98) !=? empty([])\nhead(T98, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(tail(T102, X163), member(T93, X163))\n\nT93 is ground\nT102 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T102) !=? empty([])\nhead(T102, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(tail(T102, X163), member(T93, X163)), SCOPE: 29, CLAUSE: 5 | ','(tail(T102, X163), member(T93, X163)), SCOPE: 29, CLAUSE: 6\n\nT93 is ground\nT102 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T102) !=? empty([])\nhead(T102, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(tail(T102, X163), member(T93, X163)), SCOPE: 29, CLAUSE: 6\n\nT93 is ground\nT102 is ground\nX115 is free\nX116 is free\nX163 is free\nempty(T102) !=? empty([])\nhead(T102, T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: member(T93, T109)\n\nT93 is ground\nT108 is ground\nT109 is ground\nX115 is free\nX116 is free\nhead(.(T108, T109), T93) !=? head(.(X115, X116), X115)", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ?_3 | ','(member(X9, .(T25, T26)), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT25 is ground\nT26 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(member(X9, .(T25, T26)), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT25 is ground\nT26 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(','(no(empty(.(T116, T117))), ','(tail(.(T116, T117), X200), member(X201, X200))), member(X201, T6))\n\nT6 is ground\nT116 is ground\nT117 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(','(no(empty(.(T116, T117))), ','(tail(.(T116, T117), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 8 | ','(','(no(empty(.(T116, T117))), ','(tail(.(T116, T117), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT116 is ground\nT117 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(','(call(empty(.(T122, T123))), ','(!_30, failure(a))), ','(','(tail(.(T122, T123), X200), member(X201, X200)), member(X201, T6))) | ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(empty(.(T122, T123)), ','(','(!_30, failure(a)), ','(','(tail(.(T122, T123), X200), member(X201, X200)), member(X201, T6)))) | ?_31 | ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(empty(.(T122, T123)), ','(','(!_30, failure(a)), ','(','(tail(.(T122, T123), X200), member(X201, X200)), member(X201, T6)))), SCOPE: 32, CLAUSE: 7 | ?_32 | ?_31 | ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ?_32 | ?_31 | ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ?_31 | ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(','(no(empty(.(T122, T123))), ','(tail(.(T122, T123), X200), member(X201, X200))), member(X201, T6)), SCOPE: 30, CLAUSE: 9\n\nT6 is ground\nT122 is ground\nT123 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(','(tail(.(T128, T129), X200), member(X201, X200)), member(X201, T6))\n\nT6 is ground\nT128 is ground\nT129 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(','(tail(.(T128, T129), X200), member(X201, X200)), member(X201, T6)), SCOPE: 33, CLAUSE: 5 | ','(','(tail(.(T128, T129), X200), member(X201, X200)), member(X201, T6)), SCOPE: 33, CLAUSE: 6\n\nT6 is ground\nT128 is ground\nT129 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(','(tail(.(T128, T129), X200), member(X201, X200)), member(X201, T6)), SCOPE: 33, CLAUSE: 6\n\nT6 is ground\nT128 is ground\nT129 is ground\nX201 is free\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(member(X201, T136), member(X201, T6))\n\nT6 is ground\nT136 is ground\nX201 is free", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ?_3 | ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nX72 is free\nX73 is free\nempty(T19) !=? empty([])\nhead(T19, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(member(X9, T19), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT19 is ground\nX9 is free\nX21 is free\nX72 is free\nX73 is free\nempty(T19) !=? empty([])\nhead(T19, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(','(no(empty(T140)), ','(tail(T140, X245), member(X246, X245))), member(X246, T6))\n\nT6 is ground\nT140 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T140) !=? empty([])\nhead(T140, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(','(no(empty(T140)), ','(tail(T140, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 8 | ','(','(no(empty(T140)), ','(tail(T140, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT140 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T140) !=? empty([])\nhead(T140, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(','(call(empty(T143)), ','(!_34, failure(a))), ','(','(tail(T143, X245), member(X246, X245)), member(X246, T6))) | ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(empty(T143), ','(','(!_34, failure(a)), ','(','(tail(T143, X245), member(X246, X245)), member(X246, T6)))) | ?_35 | ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ','(empty(T143), ','(','(!_34, failure(a)), ','(','(tail(T143, X245), member(X246, X245)), member(X246, T6)))), SCOPE: 36, CLAUSE: 7 | ?_36 | ?_35 | ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ?_36 | ?_35 | ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ?_35 | ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(','(no(empty(T143)), ','(tail(T143, X245), member(X246, X245))), member(X246, T6)), SCOPE: 34, CLAUSE: 9\n\nT6 is ground\nT143 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T143) !=? empty([])\nhead(T143, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(','(tail(T146, X245), member(X246, X245)), member(X246, T6))\n\nT6 is ground\nT146 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T146) !=? empty([])\nhead(T146, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ','(','(tail(T146, X245), member(X246, X245)), member(X246, T6)), SCOPE: 37, CLAUSE: 5 | ','(','(tail(T146, X245), member(X246, X245)), member(X246, T6)), SCOPE: 37, CLAUSE: 6\n\nT6 is ground\nT146 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T146) !=? empty([])\nhead(T146, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(','(tail(T146, X245), member(X246, X245)), member(X246, T6)), SCOPE: 37, CLAUSE: 6\n\nT6 is ground\nT146 is ground\nX21 is free\nX72 is free\nX73 is free\nX246 is free\nX245 is free\nempty(T146) !=? empty([])\nhead(T146, X21) !=? head(.(X72, X73), X72)", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 238 [arrowhead = none ];
238 -> 4;

239 [label="ONLY EVAL with clause\noverlap(X7, X8) :- ','(member(X9, X7), member(X9, X8)).\nand substitutionT1 -> T5,\nX7 -> T5,\nT2 -> T6,\nX8 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 239 [arrowhead = none ];
239 -> 5;

240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 240 [arrowhead = none ];
240 -> 7;

241 [label="ONLY EVAL with clause\nmember(X19, X20) :- ','(no(empty(X20)), head(X20, X19)).\nand substitutionX9 -> X21,\nX19 -> X21,\nT5 -> T10,\nX20 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 241 [arrowhead = none ];
241 -> 8;

242 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 242 [arrowhead = none ];
242 -> 9;

243 [label="ONLY EVAL with clause\nno(X27) :- ','(call(X27), ','(!_3, failure(a))).\nand substitutionT10 -> T14,\nX27 -> empty(T14)", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 243 [arrowhead = none ];
243 -> 10;

244 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 244 [arrowhead = none ];
244 -> 13;

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 245 [arrowhead = none ];
245 -> 14;

246 [label="EVAL with clause\nempty([]).\nand substitutionT14 -> []", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 246 [arrowhead = none ];
246 -> 15;

247 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 247 [arrowhead = none ];
247 -> 17;

248 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 248 [arrowhead = none ];
248 -> 18;

249 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 249 [arrowhead = none ];
249 -> 49;

250 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
18 -> 250 [arrowhead = none ];
250 -> 21;

251 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 251 [arrowhead = none ];
251 -> 22;

252 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 252 [arrowhead = none ];
252 -> 24;

253 [label="ONLY EVAL with clause\nmember(X42, X43) :- ','(no(empty(X43)), ','(tail(X43, X44), member(X42, X44))).\nand substitutionX9 -> X45,\nX42 -> X45,\nX43 -> []", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 253 [arrowhead = none ];
253 -> 33;

254 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 254 [arrowhead = none ];
254 -> 34;

255 [label="ONLY EVAL with clause\nno(X52) :- ','(call(X52), ','(!_7, failure(a))).\nand substitutionX52 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 255 [arrowhead = none ];
255 -> 37;

256 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 256 [arrowhead = none ];
256 -> 38;

257 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 257 [arrowhead = none ];
257 -> 39;

258 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 258 [arrowhead = none ];
258 -> 42;

259 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 259 [arrowhead = none ];
259 -> 43;

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 260 [arrowhead = none ];
260 -> 47;

261 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 261 [arrowhead = none ];
261 -> 48;

262 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 262 [arrowhead = none ];
262 -> 50;

263 [label="ONLY EVAL with clause\nno(X62).\nand substitutionT14 -> T19,\nX62 -> empty(T19)", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 263 [arrowhead = none ];
263 -> 55;

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 264 [arrowhead = none ];
264 -> 59;

265 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T19), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 265 [arrowhead = none ];
265 -> 60;

266 [label="EVAL with clause\nhead(.(X72, X73), X72).\nand substitutionX72 -> T25,\nX73 -> T26,\nT19 -> .(T25, T26),\nX21 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 266 [arrowhead = none ];
266 -> 64;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 267 [arrowhead = none ];
267 -> 65;

268 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 268 [arrowhead = none ];
268 -> 68;

269 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 269 [arrowhead = none ];
269 -> 69;

270 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 270 [arrowhead = none ];
270 -> 213;

271 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 271 [arrowhead = none ];
271 -> 70;

272 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 272 [arrowhead = none ];
272 -> 185;

273 [label="ONLY EVAL with clause\nmember(X82, X83) :- ','(no(empty(X83)), head(X83, X82)).\nand substitutionT25 -> T35,\nX82 -> T35,\nT6 -> T36,\nX83 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 273 [arrowhead = none ];
273 -> 72;

274 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 274 [arrowhead = none ];
274 -> 74;

275 [label="ONLY EVAL with clause\nno(X86) :- ','(call(X86), ','(!_13, failure(a))).\nand substitutionT36 -> T39,\nX86 -> empty(T39)", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 275 [arrowhead = none ];
275 -> 75;

276 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 276 [arrowhead = none ];
276 -> 76;

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
76 -> 277 [arrowhead = none ];
277 -> 78;

278 [label="EVAL with clause\nempty([]).\nand substitutionT39 -> []", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 278 [arrowhead = none ];
278 -> 80;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 279 [arrowhead = none ];
279 -> 82;

280 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 280 [arrowhead = none ];
280 -> 84;

281 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 281 [arrowhead = none ];
281 -> 103;

282 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 282 [arrowhead = none ];
282 -> 87;

283 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 283 [arrowhead = none ];
283 -> 88;

284 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 284 [arrowhead = none ];
284 -> 89;

285 [label="ONLY EVAL with clause\nmember(X95, X96) :- ','(no(empty(X96)), ','(tail(X96, X97), member(X95, X97))).\nand substitutionT35 -> T43,\nX95 -> T43,\nX96 -> []", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 285 [arrowhead = none ];
285 -> 91;

286 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 286 [arrowhead = none ];
286 -> 94;

287 [label="ONLY EVAL with clause\nno(X103) :- ','(call(X103), ','(!_17, failure(a))).\nand substitutionX103 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 287 [arrowhead = none ];
287 -> 95;

288 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 288 [arrowhead = none ];
288 -> 96;

289 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 289 [arrowhead = none ];
289 -> 97;

290 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 290 [arrowhead = none ];
290 -> 99;

291 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 291 [arrowhead = none ];
291 -> 100;

292 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
100 -> 292 [arrowhead = none ];
292 -> 101;

293 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 293 [arrowhead = none ];
293 -> 102;

294 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 294 [arrowhead = none ];
294 -> 104;

295 [label="ONLY EVAL with clause\nno(X109).\nand substitutionT39 -> T48,\nX109 -> empty(T48)", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 295 [arrowhead = none ];
295 -> 105;

296 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 296 [arrowhead = none ];
296 -> 106;

297 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T48), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 297 [arrowhead = none ];
297 -> 108;

298 [label="EVAL with clause\nhead(.(X115, X116), X115).\nand substitutionX115 -> T54,\nX116 -> T55,\nT48 -> .(T54, T55),\nT35 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 298 [arrowhead = none ];
298 -> 110;

299 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 299 [arrowhead = none ];
299 -> 111;

300 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 300 [arrowhead = none ];
300 -> 112;

301 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 301 [arrowhead = none ];
301 -> 140;

302 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 302 [arrowhead = none ];
302 -> 113;

303 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 303 [arrowhead = none ];
303 -> 114;

304 [label="ONLY EVAL with clause\nmember(X125, X126) :- ','(no(empty(X126)), ','(tail(X126, X127), member(X125, X127))).\nand substitutionT54 -> T61,\nX125 -> T61,\nT55 -> T62,\nX126 -> .(T61, T62)", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 304 [arrowhead = none ];
304 -> 117;

305 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 305 [arrowhead = none ];
305 -> 118;

306 [label="ONLY EVAL with clause\nno(X133) :- ','(call(X133), ','(!_22, failure(a))).\nand substitutionT61 -> T68,\nT62 -> T69,\nX133 -> empty(.(T68, T69))", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 306 [arrowhead = none ];
306 -> 121;

307 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 307 [arrowhead = none ];
307 -> 123;

308 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
123 -> 308 [arrowhead = none ];
308 -> 125;

309 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 309 [arrowhead = none ];
309 -> 127;

310 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 310 [arrowhead = none ];
310 -> 128;

311 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 311 [arrowhead = none ];
311 -> 130;

312 [label="ONLY EVAL with clause\nno(X139).\nand substitutionT68 -> T75,\nT69 -> T76,\nX139 -> empty(.(T75, T76))", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 312 [arrowhead = none ];
312 -> 131;

313 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
131 -> 313 [arrowhead = none ];
313 -> 133;

314 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 314 [arrowhead = none ];
314 -> 134;

315 [label="ONLY EVAL with clause\ntail(.(X149, X150), X150).\nand substitutionT75 -> T84,\nX149 -> T84,\nT76 -> T85,\nX150 -> T85,\nX127 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 315 [arrowhead = none ];
315 -> 138;

316 [label="INSTANCE with matching:\nT25 -> T84\nT6 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 316 [arrowhead = none , style=dashed];
316 -> 68[style=dashed];

317 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 317 [arrowhead = none ];
317 -> 141;

318 [label="ONLY EVAL with clause\nmember(X161, X162) :- ','(no(empty(X162)), ','(tail(X162, X163), member(X161, X163))).\nand substitutionT35 -> T93,\nX161 -> T93,\nT48 -> T94,\nX162 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 318 [arrowhead = none ];
318 -> 144;

319 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 319 [arrowhead = none ];
319 -> 150;

320 [label="ONLY EVAL with clause\nno(X169) :- ','(call(X169), ','(!_26, failure(a))).\nand substitutionT94 -> T98,\nX169 -> empty(T98)", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 320 [arrowhead = none ];
320 -> 155;

321 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
155 -> 321 [arrowhead = none ];
321 -> 156;

322 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
156 -> 322 [arrowhead = none ];
322 -> 157;

323 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T98), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 323 [arrowhead = none ];
323 -> 158;

324 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 324 [arrowhead = none ];
324 -> 160;

325 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 325 [arrowhead = none ];
325 -> 161;

326 [label="ONLY EVAL with clause\nno(X175).\nand substitutionT98 -> T102,\nX175 -> empty(T102)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 326 [arrowhead = none ];
326 -> 166;

327 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
166 -> 327 [arrowhead = none ];
327 -> 169;

328 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T102), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 328 [arrowhead = none ];
328 -> 172;

329 [label="EVAL with clause\ntail(.(X183, X184), X184).\nand substitutionX183 -> T108,\nX184 -> T109,\nT102 -> .(T108, T109),\nX163 -> T109", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 329 [arrowhead = none ];
329 -> 178;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 330 [arrowhead = none ];
330 -> 179;

331 [label="INSTANCE with matching:\nT25 -> T93\nT6 -> T109", fontsize=14, style = filled, fillcolor = lightgrey];
178 -> 331 [arrowhead = none , style=dashed];
331 -> 68[style=dashed];

332 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 332 [arrowhead = none ];
332 -> 186;

333 [label="ONLY EVAL with clause\nmember(X198, X199) :- ','(no(empty(X199)), ','(tail(X199, X200), member(X198, X200))).\nand substitutionX9 -> X201,\nX198 -> X201,\nT25 -> T116,\nT26 -> T117,\nX199 -> .(T116, T117)", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 333 [arrowhead = none ];
333 -> 188;

334 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
188 -> 334 [arrowhead = none ];
334 -> 190;

335 [label="ONLY EVAL with clause\nno(X208) :- ','(call(X208), ','(!_30, failure(a))).\nand substitutionT116 -> T122,\nT117 -> T123,\nX208 -> empty(.(T122, T123))", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 335 [arrowhead = none ];
335 -> 193;

336 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 336 [arrowhead = none ];
336 -> 196;

337 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
196 -> 337 [arrowhead = none ];
337 -> 199;

338 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
199 -> 338 [arrowhead = none ];
338 -> 200;

339 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 339 [arrowhead = none ];
339 -> 201;

340 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 340 [arrowhead = none ];
340 -> 202;

341 [label="ONLY EVAL with clause\nno(X215).\nand substitutionT122 -> T128,\nT123 -> T129,\nX215 -> empty(.(T128, T129))", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 341 [arrowhead = none ];
341 -> 205;

342 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
205 -> 342 [arrowhead = none ];
342 -> 207;

343 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
207 -> 343 [arrowhead = none ];
343 -> 208;

344 [label="ONLY EVAL with clause\ntail(.(X227, X228), X228).\nand substitutionT128 -> T135,\nX227 -> T135,\nT129 -> T136,\nX228 -> T136,\nX200 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
208 -> 344 [arrowhead = none ];
344 -> 210;

345 [label="INSTANCE with matching:\nX9 -> X201\nT5 -> T136", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 345 [arrowhead = none , style=dashed];
345 -> 5[style=dashed];

346 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
213 -> 346 [arrowhead = none ];
346 -> 214;

347 [label="ONLY EVAL with clause\nmember(X243, X244) :- ','(no(empty(X244)), ','(tail(X244, X245), member(X243, X245))).\nand substitutionX9 -> X246,\nX243 -> X246,\nT19 -> T140,\nX244 -> T140", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 347 [arrowhead = none ];
347 -> 216;

348 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
216 -> 348 [arrowhead = none ];
348 -> 218;

349 [label="ONLY EVAL with clause\nno(X253) :- ','(call(X253), ','(!_34, failure(a))).\nand substitutionT140 -> T143,\nX253 -> empty(T143)", fontsize=14, style = filled, fillcolor = lightblue];
218 -> 349 [arrowhead = none ];
349 -> 222;

350 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
222 -> 350 [arrowhead = none ];
350 -> 224;

351 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
224 -> 351 [arrowhead = none ];
351 -> 227;

352 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T143), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
227 -> 352 [arrowhead = none ];
352 -> 228;

353 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
228 -> 353 [arrowhead = none ];
353 -> 229;

354 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 354 [arrowhead = none ];
354 -> 230;

355 [label="ONLY EVAL with clause\nno(X260).\nand substitutionT143 -> T146,\nX260 -> empty(T146)", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 355 [arrowhead = none ];
355 -> 233;

356 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
233 -> 356 [arrowhead = none ];
356 -> 235;

357 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T146), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 357 [arrowhead = none ];
357 -> 236;

358 [label="BACKTRACK\nfor clause: tail(.(X3, T), T)\nwith clash: (head(T146, X21), head(.(X72, X73), X72))", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 358 [arrowhead = none ];
358 -> 237;

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c(U1'(f5_in(z0, z1), z0, z1), F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(U2'(f64_in(z0, z2, z1), .(z0, z1), z2), F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(U3'(f68_in(z0, z1), z0, .(z0, z1)), F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(U4'(f68_in(z0, z2), z0, .(z1, z2)), F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(U5'(f5_in(z1, z2), z0, z1, z2), F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(U6'(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2), F68_IN(z0, z1), F69_IN(z0, z2, z1))

S tuples:

F2_IN(z0, z1) → c(U1'(f5_in(z0, z1), z0, z1), F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(U2'(f64_in(z0, z2, z1), .(z0, z1), z2), F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(U3'(f68_in(z0, z1), z0, .(z0, z1)), F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(U4'(f68_in(z0, z2), z0, .(z1, z2)), F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(U5'(f5_in(z1, z2), z0, z1, z2), F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(U6'(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2), F68_IN(z0, z1), F69_IN(z0, z2, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c, c2, c6, c7, c10, c12

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F5_IN(.(z0, z1), z2) → c2(U2'(f64_in(z0, z2, z1), .(z0, z1), z2), F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(U3'(f68_in(z0, z1), z0, .(z0, z1)), F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(U4'(f68_in(z0, z2), z0, .(z1, z2)), F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(U5'(f5_in(z1, z2), z0, z1, z2), F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(U6'(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2), F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1(U1'(f5_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c1(F5_IN(z0, z1))

S tuples:

F5_IN(.(z0, z1), z2) → c2(U2'(f64_in(z0, z2, z1), .(z0, z1), z2), F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(U3'(f68_in(z0, z1), z0, .(z0, z1)), F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(U4'(f68_in(z0, z2), z0, .(z1, z2)), F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(U5'(f5_in(z1, z2), z0, z1, z2), F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(U6'(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2), F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1(U1'(f5_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c1(F5_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F5_IN, F68_IN, F69_IN, F64_IN, F2_IN

Compound Symbols:

c2, c6, c7, c10, c12, c1

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

Removed 6 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

S tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c1, c2, c6, c7, c10, c12, c1

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

S tuples:

F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))

K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c1, c2, c6, c7, c10, c12, c1

(9) 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.

F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))

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

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

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

POL(.(x₁, x₂)) = [2] + x₁ + x₂   
POL(F2_IN(x₁, x₂)) = [3]x₁ + [3]x₂   
POL(F5_IN(x₁, x₂)) = [2]x₁   
POL(F64_IN(x₁, x₂, x₃)) = x₁ + [2]x₃   
POL(F68_IN(x₁, x₂)) = 0   
POL(F69_IN(x₁, x₂, x₃)) = x₁ + [2]x₂   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c2(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

S tuples:

F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))

K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c1, c2, c6, c7, c10, c12, c1

(11) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

S tuples:

F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))

K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c1, c2, c6, c7, c10, c12, c1

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))

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

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

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

POL(.(x₁, x₂)) = [1] + x₂   
POL(F2_IN(x₁, x₂)) = x₁·x₂   
POL(F5_IN(x₁, x₂)) = x₁·x₂   
POL(F64_IN(x₁, x₂, x₃)) = x₂ + x₂·x₃   
POL(F68_IN(x₁, x₂)) = x₂   
POL(F69_IN(x₁, x₂, x₃)) = x₂·x₃   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c2(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1, z0, z1) → f2_out1
f5_in(.(z0, z1), z2) → U2(f64_in(z0, z2, z1), .(z0, z1), z2)
U2(f64_out1, .(z0, z1), z2) → f5_out1
U2(f64_out4, .(z0, z1), z2) → f5_out1
f68_in(z0, .(z0, z1)) → f68_out1
f68_in(z0, .(z0, z1)) → U3(f68_in(z0, z1), z0, .(z0, z1))
f68_in(z0, .(z1, z2)) → U4(f68_in(z0, z2), z0, .(z1, z2))
U3(f68_out1, z0, .(z0, z1)) → f68_out1
U4(f68_out1, z0, .(z1, z2)) → f68_out1
f69_in(z0, z1, z2) → U5(f5_in(z1, z2), z0, z1, z2)
U5(f5_out1, z0, z1, z2) → f69_out3
f64_in(z0, z1, z2) → U6(f68_in(z0, z1), f69_in(z0, z2, z1), z0, z1, z2)
U6(f68_out1, z0, z1, z2, z3) → f64_out1
U6(z0, f69_out3, z1, z2, z3) → f64_out4

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F2_IN(z0, z1) → c1

S tuples:none
K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1
F5_IN(.(z0, z1), z2) → c2(F64_IN(z0, z2, z1))
F64_IN(z0, z1, z2) → c12(F68_IN(z0, z1), F69_IN(z0, z2, z1))
F69_IN(z0, z1, z2) → c10(F5_IN(z1, z2))
F68_IN(z0, .(z0, z1)) → c6(F68_IN(z0, z1))
F68_IN(z0, .(z1, z2)) → c7(F68_IN(z0, z2))

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f68_in, U3, U4, f69_in, U5, f64_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F68_IN, F69_IN, F64_IN

Compound Symbols:

c1, c2, c6, c7, c10, c12, c1

(15) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(16) BOUNDS(O(1), O(1))

(17) 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: overlap(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: overlap(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(member(X15, T8), member(X15, T9))\n\nT8 is ground\nT9 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: member(X15, T8)\n\nT8 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: member(T11, T9)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: member(X15, T8), SCOPE: 2, CLAUSE: 1 | member(X15, T8), SCOPE: 2, CLAUSE: 2\n\nT8 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(no(empty(T15)), head(T15, X30)) | member(X15, T15), SCOPE: 2, CLAUSE: 2\n\nT15 is ground\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(no(empty(T15)), head(T15, X30)), SCOPE: 3, CLAUSE: 8 | ','(no(empty(T15)), head(T15, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T15), SCOPE: 2, CLAUSE: 2\n\nT15 is ground\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(','(call(empty(T18)), ','(!_3, failure(a))), head(T18, X30)) | ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(empty(T18), ','(','(!_3, failure(a)), head(T18, X30))) | ?_4 | ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(empty(T18), ','(','(!_3, failure(a)), head(T18, X30))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(','(!_3, failure(a)), head([], X30)) | ?_5 | ?_4 | ','(no(empty([])), head([], X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, []), SCOPE: 2, CLAUSE: 2\n\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ?_5 | ?_4 | ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free\nempty(T18) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(failure(a), head([], X30)) | member(X15, []), SCOPE: 2, CLAUSE: 2\n\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(failure(a), head([], X30)), SCOPE: 6, CLAUSE: 10 | ?_6 | member(X15, []), SCOPE: 2, CLAUSE: 2\n\nX15 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ?_6 | member(X15, []), SCOPE: 2, CLAUSE: 2\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: member(X15, []), SCOPE: 2, CLAUSE: 2\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(empty([])), ','(tail([], X47), member(X48, X47)))\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 8 | ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 9\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(','(call(empty([])), ','(!_7, failure(a))), ','(tail([], X47), member(X48, X47))) | ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 9\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(empty([]), ','(','(!_7, failure(a)), ','(tail([], X47), member(X48, X47)))) | ?_8 | ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 9\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(empty([]), ','(','(!_7, failure(a)), ','(tail([], X47), member(X48, X47)))), SCOPE: 9, CLAUSE: 7 | ?_9 | ?_8 | ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 9\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(','(!_7, failure(a)), ','(tail([], X47), member(X48, X47))) | ?_9 | ?_8 | ','(no(empty([])), ','(tail([], X47), member(X48, X47))), SCOPE: 7, CLAUSE: 9\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(failure(a), ','(tail([], X47), member(X48, X47)))\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(failure(a), ','(tail([], X47), member(X48, X47))), SCOPE: 10, CLAUSE: 10\n\nX48 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ?_4 | ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free\nempty(T18) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(no(empty(T18)), head(T18, X30)), SCOPE: 3, CLAUSE: 9 | ?_3 | member(X15, T18), SCOPE: 2, CLAUSE: 2\n\nT18 is ground\nX15 is free\nX30 is free\nempty(T18) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: head(T21, X30) | ?_3 | member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: head(T21, X30), SCOPE: 11, CLAUSE: 3 | head(T21, X30), SCOPE: 11, CLAUSE: 4 | ?_11 | ?_3 | member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: head(T21, X30), SCOPE: 11, CLAUSE: 4 | ?_11 | ?_3 | member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true | ?_11 | ?_3 | member(X15, .(T26, T27)), SCOPE: 2, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_11 | ?_3 | member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nX69 is free\nX70 is free\nempty(T21) !=? empty([])\nhead(T21, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ?_11 | ?_3 | member(X15, .(T26, T27)), SCOPE: 2, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ?_3 | member(X15, .(T26, T27)), SCOPE: 2, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: member(X15, .(T26, T27)), SCOPE: 2, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(no(empty(.(T32, T33))), ','(tail(.(T32, T33), X84), member(X85, X84)))\n\nT32 is ground\nT33 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(no(empty(.(T32, T33))), ','(tail(.(T32, T33), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 8 | ','(no(empty(.(T32, T33))), ','(tail(.(T32, T33), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT32 is ground\nT33 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(','(call(empty(.(T38, T39))), ','(!_12, failure(a))), ','(tail(.(T38, T39), X84), member(X85, X84))) | ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(empty(.(T38, T39)), ','(','(!_12, failure(a)), ','(tail(.(T38, T39), X84), member(X85, X84)))) | ?_13 | ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(empty(.(T38, T39)), ','(','(!_12, failure(a)), ','(tail(.(T38, T39), X84), member(X85, X84)))), SCOPE: 14, CLAUSE: 7 | ?_14 | ?_13 | ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ?_14 | ?_13 | ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ?_13 | ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(no(empty(.(T38, T39))), ','(tail(.(T38, T39), X84), member(X85, X84))), SCOPE: 12, CLAUSE: 9\n\nT38 is ground\nT39 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail(.(T44, T45), X84), member(X85, X84))\n\nT44 is ground\nT45 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(tail(.(T44, T45), X84), member(X85, X84)), SCOPE: 15, CLAUSE: 5 | ','(tail(.(T44, T45), X84), member(X85, X84)), SCOPE: 15, CLAUSE: 6\n\nT44 is ground\nT45 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(tail(.(T44, T45), X84), member(X85, X84)), SCOPE: 15, CLAUSE: 6\n\nT44 is ground\nT45 is ground\nX85 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: member(X85, T52)\n\nT52 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ?_3 | member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nX69 is free\nX70 is free\nempty(T21) !=? empty([])\nhead(T21, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: member(X15, T21), SCOPE: 2, CLAUSE: 2\n\nT21 is ground\nX15 is free\nX30 is free\nX69 is free\nX70 is free\nempty(T21) !=? empty([])\nhead(T21, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(no(empty(T56)), ','(tail(T56, X129), member(X130, X129)))\n\nT56 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T56) !=? empty([])\nhead(T56, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(no(empty(T56)), ','(tail(T56, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 8 | ','(no(empty(T56)), ','(tail(T56, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT56 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T56) !=? empty([])\nhead(T56, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(','(call(empty(T59)), ','(!_16, failure(a))), ','(tail(T59, X129), member(X130, X129))) | ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(empty(T59), ','(','(!_16, failure(a)), ','(tail(T59, X129), member(X130, X129)))) | ?_17 | ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(empty(T59), ','(','(!_16, failure(a)), ','(tail(T59, X129), member(X130, X129)))), SCOPE: 18, CLAUSE: 7 | ?_18 | ?_17 | ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ?_18 | ?_17 | ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ?_17 | ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(no(empty(T59)), ','(tail(T59, X129), member(X130, X129))), SCOPE: 16, CLAUSE: 9\n\nT59 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T59) !=? empty([])\nhead(T59, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(tail(T62, X129), member(X130, X129))\n\nT62 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T62) !=? empty([])\nhead(T62, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(tail(T62, X129), member(X130, X129)), SCOPE: 19, CLAUSE: 5 | ','(tail(T62, X129), member(X130, X129)), SCOPE: 19, CLAUSE: 6\n\nT62 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T62) !=? empty([])\nhead(T62, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(tail(T62, X129), member(X130, X129)), SCOPE: 19, CLAUSE: 6\n\nT62 is ground\nX30 is free\nX69 is free\nX70 is free\nX130 is free\nX129 is free\nempty(T62) !=? empty([])\nhead(T62, X30) !=? head(.(X69, X70), X69)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: member(T11, T9), SCOPE: 20, CLAUSE: 1 | member(T11, T9), SCOPE: 20, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(no(empty(T73)), head(T73, T74)) | member(T11, T73), SCOPE: 20, CLAUSE: 2\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(no(empty(T73)), head(T73, T74)), SCOPE: 21, CLAUSE: 8 | ','(no(empty(T73)), head(T73, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T73), SCOPE: 20, CLAUSE: 2\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(','(call(empty(T77)), ','(!_21, failure(a))), head(T77, T74)) | ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(empty(T77), ','(','(!_21, failure(a)), head(T77, T74))) | ?_22 | ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(empty(T77), ','(','(!_21, failure(a)), head(T77, T74))), SCOPE: 23, CLAUSE: 7 | ?_23 | ?_22 | ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(','(!_21, failure(a)), head([], T74)) | ?_23 | ?_22 | ','(no(empty([])), head([], T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, []), SCOPE: 20, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ?_23 | ?_22 | ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground\nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(failure(a), head([], T74)) | member(T11, []), SCOPE: 20, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(failure(a), head([], T74)), SCOPE: 24, CLAUSE: 10 | ?_24 | member(T11, []), SCOPE: 20, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ?_24 | member(T11, []), SCOPE: 20, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: member(T11, []), SCOPE: 20, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(no(empty([])), ','(tail([], X172), member(T83, X172)))\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 8 | ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 9\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(','(call(empty([])), ','(!_25, failure(a))), ','(tail([], X172), member(T83, X172))) | ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 9\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(empty([]), ','(','(!_25, failure(a)), ','(tail([], X172), member(T83, X172)))) | ?_26 | ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 9\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(empty([]), ','(','(!_25, failure(a)), ','(tail([], X172), member(T83, X172)))), SCOPE: 27, CLAUSE: 7 | ?_27 | ?_26 | ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 9\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(','(!_25, failure(a)), ','(tail([], X172), member(T83, X172))) | ?_27 | ?_26 | ','(no(empty([])), ','(tail([], X172), member(T83, X172))), SCOPE: 25, CLAUSE: 9\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(failure(a), ','(tail([], X172), member(T83, X172)))\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(failure(a), ','(tail([], X172), member(T83, X172))), SCOPE: 28, CLAUSE: 10\n\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ?_22 | ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground\nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(no(empty(T77)), head(T77, T74)), SCOPE: 21, CLAUSE: 9 | ?_21 | member(T11, T77), SCOPE: 20, CLAUSE: 2\n\nT77 is ground\nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: head(T88, T74) | ?_21 | member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: head(T88, T74), SCOPE: 29, CLAUSE: 3 | head(T88, T74), SCOPE: 29, CLAUSE: 4 | ?_29 | ?_21 | member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: head(T88, T74), SCOPE: 29, CLAUSE: 4 | ?_29 | ?_21 | member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: true | ?_29 | ?_21 | member(T11, .(T94, T95)), SCOPE: 20, CLAUSE: 2\n\nT94 is ground\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ?_29 | ?_21 | member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nX190 is free\nX191 is free\nempty(T88) !=? empty([])\nhead(T88, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ?_29 | ?_21 | member(T11, .(T94, T95)), SCOPE: 20, CLAUSE: 2\n\nT94 is ground\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ?_21 | member(T11, .(T94, T95)), SCOPE: 20, CLAUSE: 2\n\nT94 is ground\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: member(T11, .(T94, T95)), SCOPE: 20, CLAUSE: 2\n\nT94 is ground\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(no(empty(.(T105, T106))), ','(tail(.(T105, T106), X202), member(T107, X202)))\n\nT105 is ground\nT106 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(no(empty(.(T105, T106))), ','(tail(.(T105, T106), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 8 | ','(no(empty(.(T105, T106))), ','(tail(.(T105, T106), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT105 is ground\nT106 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(','(call(empty(.(T113, T114))), ','(!_30, failure(a))), ','(tail(.(T113, T114), X202), member(T107, X202))) | ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(empty(.(T113, T114)), ','(','(!_30, failure(a)), ','(tail(.(T113, T114), X202), member(T107, X202)))) | ?_31 | ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(empty(.(T113, T114)), ','(','(!_30, failure(a)), ','(tail(.(T113, T114), X202), member(T107, X202)))), SCOPE: 32, CLAUSE: 7 | ?_32 | ?_31 | ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ?_32 | ?_31 | ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ?_31 | ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(no(empty(.(T113, T114))), ','(tail(.(T113, T114), X202), member(T107, X202))), SCOPE: 30, CLAUSE: 9\n\nT113 is ground\nT114 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(tail(.(T120, T121), X202), member(T107, X202))\n\nT120 is ground\nT121 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(tail(.(T120, T121), X202), member(T107, X202)), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T120, T121), X202), member(T107, X202)), SCOPE: 33, CLAUSE: 6\n\nT120 is ground\nT121 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(tail(.(T120, T121), X202), member(T107, X202)), SCOPE: 33, CLAUSE: 6\n\nT120 is ground\nT121 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: member(T107, T130)\n\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ?_21 | member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nX190 is free\nX191 is free\nempty(T88) !=? empty([])\nhead(T88, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: member(T11, T88), SCOPE: 20, CLAUSE: 2\n\nT88 is ground\nX190 is free\nX191 is free\nempty(T88) !=? empty([])\nhead(T88, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(no(empty(T140)), ','(tail(T140, X238), member(T141, X238)))\n\nT140 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T140) !=? empty([])\nhead(T140, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(no(empty(T140)), ','(tail(T140, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 8 | ','(no(empty(T140)), ','(tail(T140, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT140 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T140) !=? empty([])\nhead(T140, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(','(call(empty(T145)), ','(!_34, failure(a))), ','(tail(T145, X238), member(T141, X238))) | ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ','(empty(T145), ','(','(!_34, failure(a)), ','(tail(T145, X238), member(T141, X238)))) | ?_35 | ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(empty(T145), ','(','(!_34, failure(a)), ','(tail(T145, X238), member(T141, X238)))), SCOPE: 36, CLAUSE: 7 | ?_36 | ?_35 | ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ?_36 | ?_35 | ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ?_35 | ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(no(empty(T145)), ','(tail(T145, X238), member(T141, X238))), SCOPE: 34, CLAUSE: 9\n\nT145 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T145) !=? empty([])\nhead(T145, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(tail(T149, X238), member(T141, X238))\n\nT149 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T149) !=? empty([])\nhead(T149, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(tail(T149, X238), member(T141, X238)), SCOPE: 37, CLAUSE: 5 | ','(tail(T149, X238), member(T141, X238)), SCOPE: 37, CLAUSE: 6\n\nT149 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T149) !=? empty([])\nhead(T149, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(tail(T149, X238), member(T141, X238)), SCOPE: 37, CLAUSE: 6\n\nT149 is ground\nX190 is free\nX191 is free\nX238 is free\nempty(T149) !=? empty([])\nhead(T149, T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: member(T141, T156)\n\nT155 is ground\nT156 is ground\nX190 is free\nX191 is free\nhead(.(T155, T156), T74) !=? head(.(X190, X191), X190)", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 240 [arrowhead = none ];
240 -> 3;

241 [label="ONLY EVAL with clause\noverlap(X13, X14) :- ','(member(X15, X13), member(X15, X14)).\nand substitutionT1 -> T8,\nX13 -> T8,\nT2 -> T9,\nX14 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 241 [arrowhead = none ];
241 -> 6;

242 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
6 -> 242 [arrowhead = none ];
242 -> 11;

243 [label="SPLIT 2\nnew knowledge:\nT8 is ground\nreplacements:X15 -> T11", fontsize=14, style = filled, fillcolor = violet];
6 -> 243 [arrowhead = none ];
243 -> 12;

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

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

246 [label="ONLY EVAL with clause\nmember(X28, X29) :- ','(no(empty(X29)), head(X29, X28)).\nand substitutionX15 -> X30,\nX28 -> X30,\nT8 -> T15,\nX29 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 246 [arrowhead = none ];
246 -> 19;

247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 247 [arrowhead = none ];
247 -> 20;

248 [label="ONLY EVAL with clause\nno(X33) :- ','(call(X33), ','(!_3, failure(a))).\nand substitutionT15 -> T18,\nX33 -> empty(T18)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 248 [arrowhead = none ];
248 -> 23;

249 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 249 [arrowhead = none ];
249 -> 25;

250 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 250 [arrowhead = none ];
250 -> 26;

251 [label="EVAL with clause\nempty([]).\nand substitutionT18 -> []", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 251 [arrowhead = none ];
251 -> 27;

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

253 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 253 [arrowhead = none ];
253 -> 29;

254 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 254 [arrowhead = none ];
254 -> 53;

255 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 255 [arrowhead = none ];
255 -> 30;

256 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 256 [arrowhead = none ];
256 -> 31;

257 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 257 [arrowhead = none ];
257 -> 32;

258 [label="ONLY EVAL with clause\nmember(X45, X46) :- ','(no(empty(X46)), ','(tail(X46, X47), member(X45, X47))).\nand substitutionX15 -> X48,\nX45 -> X48,\nX46 -> []", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 258 [arrowhead = none ];
258 -> 35;

259 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 259 [arrowhead = none ];
259 -> 36;

260 [label="ONLY EVAL with clause\nno(X55) :- ','(call(X55), ','(!_7, failure(a))).\nand substitutionX55 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 260 [arrowhead = none ];
260 -> 40;

261 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 261 [arrowhead = none ];
261 -> 41;

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
41 -> 262 [arrowhead = none ];
262 -> 44;

263 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 263 [arrowhead = none ];
263 -> 45;

264 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 264 [arrowhead = none ];
264 -> 46;

265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 265 [arrowhead = none ];
265 -> 51;

266 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 266 [arrowhead = none ];
266 -> 52;

267 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 267 [arrowhead = none ];
267 -> 54;

268 [label="ONLY EVAL with clause\nno(X62).\nand substitutionT18 -> T21,\nX62 -> empty(T21)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 268 [arrowhead = none ];
268 -> 56;

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 269 [arrowhead = none ];
269 -> 57;

270 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T21), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 270 [arrowhead = none ];
270 -> 58;

271 [label="EVAL with clause\nhead(.(X69, X70), X69).\nand substitutionX69 -> T26,\nX70 -> T27,\nT21 -> .(T26, T27),\nX30 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 271 [arrowhead = none ];
271 -> 61;

272 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 272 [arrowhead = none ];
272 -> 62;

273 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 273 [arrowhead = none ];
273 -> 63;

274 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 274 [arrowhead = none ];
274 -> 107;

275 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 275 [arrowhead = none ];
275 -> 66;

276 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 276 [arrowhead = none ];
276 -> 67;

277 [label="ONLY EVAL with clause\nmember(X82, X83) :- ','(no(empty(X83)), ','(tail(X83, X84), member(X82, X84))).\nand substitutionX15 -> X85,\nX82 -> X85,\nT26 -> T32,\nT27 -> T33,\nX83 -> .(T32, T33)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 277 [arrowhead = none ];
277 -> 71;

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
71 -> 278 [arrowhead = none ];
278 -> 73;

279 [label="ONLY EVAL with clause\nno(X92) :- ','(call(X92), ','(!_12, failure(a))).\nand substitutionT32 -> T38,\nT33 -> T39,\nX92 -> empty(.(T38, T39))", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 279 [arrowhead = none ];
279 -> 77;

280 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
77 -> 280 [arrowhead = none ];
280 -> 79;

281 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 281 [arrowhead = none ];
281 -> 81;

282 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 282 [arrowhead = none ];
282 -> 83;

283 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 283 [arrowhead = none ];
283 -> 85;

284 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 284 [arrowhead = none ];
284 -> 86;

285 [label="ONLY EVAL with clause\nno(X99).\nand substitutionT38 -> T44,\nT39 -> T45,\nX99 -> empty(.(T44, T45))", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 285 [arrowhead = none ];
285 -> 90;

286 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
90 -> 286 [arrowhead = none ];
286 -> 92;

287 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 287 [arrowhead = none ];
287 -> 93;

288 [label="ONLY EVAL with clause\ntail(.(X111, X112), X112).\nand substitutionT44 -> T51,\nX111 -> T51,\nT45 -> T52,\nX112 -> T52,\nX84 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 288 [arrowhead = none ];
288 -> 98;

289 [label="INSTANCE with matching:\nX15 -> X85\nT8 -> T52", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 289 [arrowhead = none , style=dashed];
289 -> 11[style=dashed];

290 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 290 [arrowhead = none ];
290 -> 109;

291 [label="ONLY EVAL with clause\nmember(X127, X128) :- ','(no(empty(X128)), ','(tail(X128, X129), member(X127, X129))).\nand substitutionX15 -> X130,\nX127 -> X130,\nT21 -> T56,\nX128 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 291 [arrowhead = none ];
291 -> 115;

292 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
115 -> 292 [arrowhead = none ];
292 -> 116;

293 [label="ONLY EVAL with clause\nno(X137) :- ','(call(X137), ','(!_16, failure(a))).\nand substitutionT56 -> T59,\nX137 -> empty(T59)", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 293 [arrowhead = none ];
293 -> 119;

294 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 294 [arrowhead = none ];
294 -> 120;

295 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 295 [arrowhead = none ];
295 -> 122;

296 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T59), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 296 [arrowhead = none ];
296 -> 124;

297 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 297 [arrowhead = none ];
297 -> 126;

298 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 298 [arrowhead = none ];
298 -> 129;

299 [label="ONLY EVAL with clause\nno(X144).\nand substitutionT59 -> T62,\nX144 -> empty(T62)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 299 [arrowhead = none ];
299 -> 132;

300 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
132 -> 300 [arrowhead = none ];
300 -> 135;

301 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T62), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 301 [arrowhead = none ];
301 -> 136;

302 [label="BACKTRACK\nfor clause: tail(.(X3, T), T)\nwith clash: (head(T62, X30), head(.(X69, X70), X69))", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 302 [arrowhead = none ];
302 -> 137;

303 [label="ONLY EVAL with clause\nmember(X157, X158) :- ','(no(empty(X158)), head(X158, X157)).\nand substitutionT11 -> T74,\nX157 -> T74,\nT9 -> T73,\nX158 -> T73,\nT72 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 303 [arrowhead = none ];
303 -> 142;

304 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
142 -> 304 [arrowhead = none ];
304 -> 143;

305 [label="ONLY EVAL with clause\nno(X161) :- ','(call(X161), ','(!_21, failure(a))).\nand substitutionT73 -> T77,\nX161 -> empty(T77)", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 305 [arrowhead = none ];
305 -> 145;

306 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
145 -> 306 [arrowhead = none ];
306 -> 146;

307 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
146 -> 307 [arrowhead = none ];
307 -> 147;

308 [label="EVAL with clause\nempty([]).\nand substitutionT77 -> []", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 308 [arrowhead = none ];
308 -> 148;

309 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 309 [arrowhead = none ];
309 -> 149;

310 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 310 [arrowhead = none ];
310 -> 151;

311 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 311 [arrowhead = none ];
311 -> 173;

312 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
151 -> 312 [arrowhead = none ];
312 -> 152;

313 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 313 [arrowhead = none ];
313 -> 153;

314 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 314 [arrowhead = none ];
314 -> 154;

315 [label="ONLY EVAL with clause\nmember(X170, X171) :- ','(no(empty(X171)), ','(tail(X171, X172), member(X170, X172))).\nand substitutionT11 -> T83,\nX170 -> T83,\nX171 -> [],\nT82 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 315 [arrowhead = none ];
315 -> 159;

316 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
159 -> 316 [arrowhead = none ];
316 -> 162;

317 [label="ONLY EVAL with clause\nno(X178) :- ','(call(X178), ','(!_25, failure(a))).\nand substitutionX178 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 317 [arrowhead = none ];
317 -> 163;

318 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
163 -> 318 [arrowhead = none ];
318 -> 164;

319 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 319 [arrowhead = none ];
319 -> 165;

320 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 320 [arrowhead = none ];
320 -> 167;

321 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 321 [arrowhead = none ];
321 -> 168;

322 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
168 -> 322 [arrowhead = none ];
322 -> 170;

323 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
170 -> 323 [arrowhead = none ];
323 -> 171;

324 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 324 [arrowhead = none ];
324 -> 174;

325 [label="ONLY EVAL with clause\nno(X184).\nand substitutionT77 -> T88,\nX184 -> empty(T88)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 325 [arrowhead = none ];
325 -> 175;

326 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
175 -> 326 [arrowhead = none ];
326 -> 176;

327 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T88), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 327 [arrowhead = none ];
327 -> 177;

328 [label="EVAL with clause\nhead(.(X190, X191), X190).\nand substitutionX190 -> T94,\nX191 -> T95,\nT88 -> .(T94, T95),\nT74 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 328 [arrowhead = none ];
328 -> 180;

329 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 329 [arrowhead = none ];
329 -> 181;

330 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 330 [arrowhead = none ];
330 -> 182;

331 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 331 [arrowhead = none ];
331 -> 211;

332 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 332 [arrowhead = none ];
332 -> 183;

333 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
183 -> 333 [arrowhead = none ];
333 -> 184;

334 [label="ONLY EVAL with clause\nmember(X200, X201) :- ','(no(empty(X201)), ','(tail(X201, X202), member(X200, X202))).\nand substitutionT11 -> T107,\nX200 -> T107,\nT94 -> T105,\nT95 -> T106,\nX201 -> .(T105, T106),\nT104 -> T107", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 334 [arrowhead = none ];
334 -> 187;

335 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
187 -> 335 [arrowhead = none ];
335 -> 189;

336 [label="ONLY EVAL with clause\nno(X208) :- ','(call(X208), ','(!_30, failure(a))).\nand substitutionT105 -> T113,\nT106 -> T114,\nX208 -> empty(.(T113, T114))", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 336 [arrowhead = none ];
336 -> 191;

337 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
191 -> 337 [arrowhead = none ];
337 -> 192;

338 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
192 -> 338 [arrowhead = none ];
338 -> 194;

339 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
194 -> 339 [arrowhead = none ];
339 -> 195;

340 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 340 [arrowhead = none ];
340 -> 197;

341 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 341 [arrowhead = none ];
341 -> 198;

342 [label="ONLY EVAL with clause\nno(X214).\nand substitutionT113 -> T120,\nT114 -> T121,\nX214 -> empty(.(T120, T121))", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 342 [arrowhead = none ];
342 -> 203;

343 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
203 -> 343 [arrowhead = none ];
343 -> 204;

344 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 344 [arrowhead = none ];
344 -> 206;

345 [label="ONLY EVAL with clause\ntail(.(X224, X225), X225).\nand substitutionT120 -> T129,\nX224 -> T129,\nT121 -> T130,\nX225 -> T130,\nX202 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 345 [arrowhead = none ];
345 -> 209;

346 [label="INSTANCE with matching:\nT11 -> T107\nT9 -> T130", fontsize=14, style = filled, fillcolor = lightgrey];
209 -> 346 [arrowhead = none , style=dashed];
346 -> 12[style=dashed];

347 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 347 [arrowhead = none ];
347 -> 212;

348 [label="ONLY EVAL with clause\nmember(X236, X237) :- ','(no(empty(X237)), ','(tail(X237, X238), member(X236, X238))).\nand substitutionT11 -> T141,\nX236 -> T141,\nT88 -> T140,\nX237 -> T140,\nT139 -> T141", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 348 [arrowhead = none ];
348 -> 215;

349 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
215 -> 349 [arrowhead = none ];
349 -> 217;

350 [label="ONLY EVAL with clause\nno(X244) :- ','(call(X244), ','(!_34, failure(a))).\nand substitutionT140 -> T145,\nX244 -> empty(T145)", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 350 [arrowhead = none ];
350 -> 219;

351 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
219 -> 351 [arrowhead = none ];
351 -> 220;

352 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
220 -> 352 [arrowhead = none ];
352 -> 221;

353 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T145), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 353 [arrowhead = none ];
353 -> 223;

354 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 354 [arrowhead = none ];
354 -> 225;

355 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
225 -> 355 [arrowhead = none ];
355 -> 226;

356 [label="ONLY EVAL with clause\nno(X250).\nand substitutionT145 -> T149,\nX250 -> empty(T149)", fontsize=14, style = filled, fillcolor = lightblue];
226 -> 356 [arrowhead = none ];
356 -> 231;

357 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
231 -> 357 [arrowhead = none ];
357 -> 232;

358 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T149), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 358 [arrowhead = none ];
358 -> 234;

359 [label="EVAL with clause\ntail(.(X258, X259), X259).\nand substitutionX258 -> T155,\nX259 -> T156,\nT149 -> .(T155, T156),\nX238 -> T156", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 359 [arrowhead = none ];
359 -> 238;

360 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 360 [arrowhead = none ];
360 -> 239;

361 [label="INSTANCE with matching:\nT11 -> T141\nT9 -> T156", fontsize=14, style = filled, fillcolor = lightgrey];
238 -> 361 [arrowhead = none , style=dashed];
361 -> 12[style=dashed];

}

(18) Obligation:

Complex Complexity Dependency Tuples Problem
MAX

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(19) MaxProof (BOTH BOUNDS(ID, ID) transformation)

Took the maximum complexity of the problems.

(20) Complex Obligation (MAX)

(21) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(22) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(23) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(U1'(f6_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(U10'(f12_in(z1), z0, z1))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))

S tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F1_IN(z0, z1) → c7(U1'(f6_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, U2', F11_IN, U5', F12_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

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

Removed 7 trailing tuple parts

(25) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

S tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
U2'(f11_out1, z0, z1) → c3
F1_IN(z0, z1) → c7

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, F1_IN, U9', U2', F11_IN, U5', F12_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(26) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F1_IN(z0, z1) → c7
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U2'(f11_out1, z0, z1) → c3
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U9'(f11_out1, z0, z1) → c7
U5'(f11_out1, z0, z1) → c4

Now S is empty

(27) BOUNDS(O(1), O(1))

(28) Obligation:

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(29) MultiplicationProof (BOTH BOUNDS(ID, ID) transformation)

Multiplied the complexity of the problems.

(30) Complex Obligation (MULT)

(31) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(32) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(33) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(U1'(f6_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(U10'(f12_in(z1), z0, z1))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, U2', F11_IN, U5', F12_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

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

Removed 7 trailing tuple parts

(35) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

S tuples:

F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, F1_IN, U9', U2', F11_IN, U5', F12_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(36) 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.

F6_IN(z0, z1) → c7(F11_IN(z0))
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4

We considered the (Usable) Rules:

f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1

And the Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

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

POL(.(x₁, x₂)) = [2] + x₂   
POL(F11_IN(x₁)) = x₁   
POL(F12_IN(x₁)) = 0   
POL(F1_IN(x₁, x₂)) = [2] + [3]x₁ + [3]x₂   
POL(F6_IN(x₁, x₂)) = [1] + [2]x₁ + [3]x₂   
POL(U2'(x₁, x₂, x₃)) = x₂   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂, x₃)) = [1] + x₂   
POL(U9'(x₁, x₂, x₃)) = x₂ + x₃   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = 0   
POL(f11_out1) = 0   

(37) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

S tuples:

F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))

K tuples:

F6_IN(z0, z1) → c7(F11_IN(z0))
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4

Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, F1_IN, U9', U2', F11_IN, U5', F12_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(38) 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.

F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))

We considered the (Usable) Rules:

f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1

And the Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

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

POL(.(x₁, x₂)) = 0   
POL(F11_IN(x₁)) = [1]   
POL(F12_IN(x₁)) = 0   
POL(F1_IN(x₁, x₂)) = [2] + [3]x₁ + [3]x₂   
POL(F6_IN(x₁, x₂)) = [1] + [2]x₁ + [2]x₂   
POL(U2'(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂, x₃)) = [2]x₃   
POL(U9'(x₁, x₂, x₃)) = [2]x₂ + [2]x₃   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = 0   
POL(f11_out1) = 0   

(39) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

S tuples:none
K tuples:

F6_IN(z0, z1) → c7(F11_IN(z0))
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))

Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, F1_IN, U9', U2', F11_IN, U5', F12_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(40) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(41) BOUNDS(O(1), O(1))

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f6_in(z0, z1), z0, z1), F6_IN(z0, z1))
F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F6_IN(z0, z1) → c3(U5'(f11_in(z0), z0, z1), F11_IN(z0))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

S tuples:

F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c6(U10'(f12_in(z1), z0, z1), F12_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F6_IN, U2', F11_IN, U5', F12_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(43) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
U2'(f11_out1, z0, z1) → c3(U3'(f12_in(z1), z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1, z0, z1) → c4(U6'(f12_in(z1), z0, z1))
F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(U1'(f6_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(U10'(f12_in(z1), z0, z1))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))

S tuples:

F12_IN(.(z0, z1)) → c1(U7'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F12_IN(.(z0, z1)) → c2(U8'(f12_in(z1), .(z0, z1)), F12_IN(z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c7(U10'(f12_in(z1), z0, z1))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, U2', F11_IN, U5', F12_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

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

Removed 7 trailing tuple parts

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f6_in(z0, z1), z0, z1)
U1(f6_out1, z0, z1) → f1_out1
f6_in(z0, z1) → U2(f11_in(z0), z0, z1)
f6_in(z0, z1) → U5(f11_in(z0), z0, z1)
f6_in(z0, z1) → U9(f11_in(z0), z0, z1)
U2(f11_out1, z0, z1) → U3(f12_in(z1), z0, z1)
U3(f12_out1, z0, z1) → f6_out1
f11_in(.(z0, z1)) → f11_out1
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1, .(z0, z1)) → f11_out1
U5(f11_out1, z0, z1) → U6(f12_in(z1), z0, z1)
U6(f12_out1, z0, z1) → f6_out1
f12_in(.(z0, z1)) → f12_out1
f12_in(.(z0, z1)) → U7(f12_in(z1), .(z0, z1))
f12_in(.(z0, z1)) → U8(f12_in(z1), .(z0, z1))
U7(f12_out1, .(z0, z1)) → f12_out1
U8(f12_out1, .(z0, z1)) → f12_out1
U9(f11_out1, z0, z1) → U10(f12_in(z1), z0, z1)
U10(f12_out1, z0, z1) → f6_out1

Tuples:

F6_IN(z0, z1) → c2(U2'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
F1_IN(z0, z1) → c7(F6_IN(z0, z1))
F6_IN(z0, z1) → c7(U5'(f11_in(z0), z0, z1))
F6_IN(z0, z1) → c7(F11_IN(z0))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
U2'(f11_out1, z0, z1) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1, z0, z1) → c4
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
F1_IN(z0, z1) → c7
U9'(f11_out1, z0, z1) → c7

S tuples:

F6_IN(z0, z1) → c5(U9'(f11_in(z0), z0, z1))
U9'(f11_out1, z0, z1) → c7(F12_IN(z1))
F12_IN(.(z0, z1)) → c1(F12_IN(z1))
F12_IN(.(z0, z1)) → c2(F12_IN(z1))
U9'(f11_out1, z0, z1) → c7

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, U3, f11_in, U4, U5, U6, f12_in, U7, U8, U9, U10

Defined Pair Symbols:

F6_IN, F1_IN, U9', U2', F11_IN, U5', F12_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7