Left Termination of the query pattern
goal(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

goal(Name, Code) :- ','(eq(Name, .(First, Others)), ','(reduce(Others, s(0), First, Reduced), eq(Code, Reduced))).
reduce(X1, s(s(s(s(0)))), X2, []) :- !.
reduce([], X3, X4, []) :- !.
reduce(.(Current, Others), Count, Current, Code) :- ','(vowel_h_w_y(Current), ','(!, reduce(Others, Count, Current, Code))).
reduce(.(Letter, Others), Count, Letter, Code) :- ','(!, reduce(Others, Count, Letter, Code)).
reduce(.(Current, Others), Count, X5, .(Current, Code)) :- reduce(Others, s(Count), Current, Code).
vowel_h_w_y(97).
vowel_h_w_y(101).
vowel_h_w_y(105).
vowel_h_w_y(111).
vowel_h_w_y(117).
vowel_h_w_y(104).
vowel_h_w_y(119).
vowel_h_w_y(121).
eq(X, X).

Query: goal(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: goal(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: goal(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(eq(T5, .(X10, X11)), ','(reduce(X11, s(0), X10, X12), eq(T7, X12)))\n\nT5 is ground\nX10 is free\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(eq(T5, .(X10, X11)), ','(reduce(X11, s(0), X10, X12), eq(T7, X12))), SCOPE: 2, CLAUSE: 14\n\nT5 is ground\nX10 is free\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="B: ','(reduce(T16, s(0), T15, X12), eq(T7, X12))\n\nT15 is ground\nT16 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="C: reduce(T16, s(0), T15, X12)\n\nT15 is ground\nT16 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="F: eq(T7, T18)\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 1 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 2 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 3 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 4 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 2 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 3 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 4 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: !_3 | reduce([], s(0), T23, X12), SCOPE: 3, CLAUSE: 3 | reduce([], s(0), T23, X12), SCOPE: 3, CLAUSE: 4 | reduce([], s(0), T23, X12), SCOPE: 3, CLAUSE: 5\n\nT23 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 3 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 4 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX12 is free\nX26 is free\nX27 is free\nreduce(T16, s(0), T15, X12) !=? reduce([], X26, X27, [])", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 3\n\nT15 is ground\nT16 is ground\nX12 is free\nX26 is free\nX27 is free\nreduce(T16, s(0), T15, X12) !=? reduce([], X26, X27, [])", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 4 | reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX12 is free\nX26 is free\nX27 is free\nreduce(T16, s(0), T15, X12) !=? reduce([], X26, X27, [])", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52)))\n\nT32 is ground\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 6 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 7 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 8 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(!_3, reduce(T33, s(0), 97, X52)) | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 7 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 8 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(97), ','(!_3, reduce(T33, s(0), 97, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 7 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 8 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: reduce(T33, s(0), 97, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(!_3, reduce(T33, s(0), 101, X52)) | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 8 | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(101), ','(!_3, reduce(T33, s(0), 101, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 8 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: reduce(T33, s(0), 101, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(!_3, reduce(T33, s(0), 105, X52)) | ','(vowel_h_w_y(105), ','(!_3, reduce(T33, s(0), 105, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(105), ','(!_3, reduce(T33, s(0), 105, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(105), ','(!_3, reduce(T33, s(0), 105, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(105), ','(!_3, reduce(T33, s(0), 105, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(105), ','(!_3, reduce(T33, s(0), 105, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 9 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)\nvowel_h_w_y(T32) !=? vowel_h_w_y(105)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: reduce(T33, s(0), 105, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(!_3, reduce(T33, s(0), 111, X52)) | ','(vowel_h_w_y(111), ','(!_3, reduce(T33, s(0), 111, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(111), ','(!_3, reduce(T33, s(0), 111, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(111), ','(!_3, reduce(T33, s(0), 111, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(111), ','(!_3, reduce(T33, s(0), 111, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 10 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)\nvowel_h_w_y(T32) !=? vowel_h_w_y(105)\nvowel_h_w_y(T32) !=? vowel_h_w_y(111)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: reduce(T33, s(0), 111, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(!_3, reduce(T33, s(0), 117, X52)) | ','(vowel_h_w_y(117), ','(!_3, reduce(T33, s(0), 117, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(117), ','(!_3, reduce(T33, s(0), 117, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(117), ','(!_3, reduce(T33, s(0), 117, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 11 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)\nvowel_h_w_y(T32) !=? vowel_h_w_y(105)\nvowel_h_w_y(T32) !=? vowel_h_w_y(111)\nvowel_h_w_y(T32) !=? vowel_h_w_y(117)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: reduce(T33, s(0), 117, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(!_3, reduce(T33, s(0), 104, X52)) | ','(vowel_h_w_y(104), ','(!_3, reduce(T33, s(0), 104, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(104), ','(!_3, reduce(T33, s(0), 104, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 12 | ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)\nvowel_h_w_y(T32) !=? vowel_h_w_y(105)\nvowel_h_w_y(T32) !=? vowel_h_w_y(111)\nvowel_h_w_y(T32) !=? vowel_h_w_y(117)\nvowel_h_w_y(T32) !=? vowel_h_w_y(104)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: reduce(T33, s(0), 104, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(!_3, reduce(T33, s(0), 119, X52)) | ','(vowel_h_w_y(119), ','(!_3, reduce(T33, s(0), 119, X52))), SCOPE: 4, CLAUSE: 13\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(vowel_h_w_y(T32), ','(!_3, reduce(T33, s(0), T32, X52))), SCOPE: 4, CLAUSE: 13\n\nT32 is ground\nT33 is ground\nX52 is free\nvowel_h_w_y(T32) !=? vowel_h_w_y(97)\nvowel_h_w_y(T32) !=? vowel_h_w_y(101)\nvowel_h_w_y(T32) !=? vowel_h_w_y(105)\nvowel_h_w_y(T32) !=? vowel_h_w_y(111)\nvowel_h_w_y(T32) !=? vowel_h_w_y(117)\nvowel_h_w_y(T32) !=? vowel_h_w_y(104)\nvowel_h_w_y(T32) !=? vowel_h_w_y(119)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: reduce(T33, s(0), 119, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(!_3, reduce(T33, s(0), 121, X52))\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: reduce(T33, s(0), 121, X52)\n\nT33 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 4\n\nT15 is ground\nT16 is ground\nX12 is free\nX26 is free\nX27 is free\nreduce(T16, s(0), T15, X12) !=? reduce([], X26, X27, [])", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: reduce(T16, s(0), T15, X12), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX12 is free\nX26 is free\nX27 is free\nreduce(T16, s(0), T15, X12) !=? reduce([], X26, X27, [])", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(!_3, reduce(T51, s(0), T50, X93))\n\nT50 is ground\nT51 is ground\nX93 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: reduce(T51, s(0), T50, X93)\n\nT50 is ground\nT51 is ground\nX93 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="D: reduce(T60, s(s(0)), T59, X113)\n\nT59 is ground\nT60 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 1 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 2 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 3 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 4 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 5\n\nT59 is ground\nT60 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 2 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 3 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 4 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 5\n\nT59 is ground\nT60 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: !_5 | reduce([], s(s(0)), T66, X113), SCOPE: 5, CLAUSE: 3 | reduce([], s(s(0)), T66, X113), SCOPE: 5, CLAUSE: 4 | reduce([], s(s(0)), T66, X113), SCOPE: 5, CLAUSE: 5\n\nT66 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 3 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 4 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 5\n\nT59 is ground\nT60 is ground\nX113 is free\nX122 is free\nX123 is free\nreduce(T60, s(s(0)), T59, X113) !=? reduce([], X122, X123, [])", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 3\n\nT59 is ground\nT60 is ground\nX113 is free\nX122 is free\nX123 is free\nreduce(T60, s(s(0)), T59, X113) !=? reduce([], X122, X123, [])", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 4 | reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 5\n\nT59 is ground\nT60 is ground\nX113 is free\nX122 is free\nX123 is free\nreduce(T60, s(s(0)), T59, X113) !=? reduce([], X122, X123, [])", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148)))\n\nT75 is ground\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 6 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 7 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 8 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(!_5, reduce(T76, s(s(0)), 97, X148)) | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 7 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 8 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(97), ','(!_5, reduce(T76, s(s(0)), 97, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 7 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 8 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: reduce(T76, s(s(0)), 97, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(!_5, reduce(T76, s(s(0)), 101, X148)) | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 8 | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(101), ','(!_5, reduce(T76, s(s(0)), 101, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 8 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: reduce(T76, s(s(0)), 101, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(!_5, reduce(T76, s(s(0)), 105, X148)) | ','(vowel_h_w_y(105), ','(!_5, reduce(T76, s(s(0)), 105, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(105), ','(!_5, reduce(T76, s(s(0)), 105, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(105), ','(!_5, reduce(T76, s(s(0)), 105, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(105), ','(!_5, reduce(T76, s(s(0)), 105, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(105), ','(!_5, reduce(T76, s(s(0)), 105, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 9 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)\nvowel_h_w_y(T75) !=? vowel_h_w_y(105)", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: reduce(T76, s(s(0)), 105, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(!_5, reduce(T76, s(s(0)), 111, X148)) | ','(vowel_h_w_y(111), ','(!_5, reduce(T76, s(s(0)), 111, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(111), ','(!_5, reduce(T76, s(s(0)), 111, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(111), ','(!_5, reduce(T76, s(s(0)), 111, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(111), ','(!_5, reduce(T76, s(s(0)), 111, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 10 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)\nvowel_h_w_y(T75) !=? vowel_h_w_y(105)\nvowel_h_w_y(T75) !=? vowel_h_w_y(111)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: reduce(T76, s(s(0)), 111, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ','(!_5, reduce(T76, s(s(0)), 117, X148)) | ','(vowel_h_w_y(117), ','(!_5, reduce(T76, s(s(0)), 117, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(117), ','(!_5, reduce(T76, s(s(0)), 117, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(117), ','(!_5, reduce(T76, s(s(0)), 117, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 11 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)\nvowel_h_w_y(T75) !=? vowel_h_w_y(105)\nvowel_h_w_y(T75) !=? vowel_h_w_y(111)\nvowel_h_w_y(T75) !=? vowel_h_w_y(117)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: reduce(T76, s(s(0)), 117, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(!_5, reduce(T76, s(s(0)), 104, X148)) | ','(vowel_h_w_y(104), ','(!_5, reduce(T76, s(s(0)), 104, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(104), ','(!_5, reduce(T76, s(s(0)), 104, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 12 | ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)\nvowel_h_w_y(T75) !=? vowel_h_w_y(105)\nvowel_h_w_y(T75) !=? vowel_h_w_y(111)\nvowel_h_w_y(T75) !=? vowel_h_w_y(117)\nvowel_h_w_y(T75) !=? vowel_h_w_y(104)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: reduce(T76, s(s(0)), 104, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: ','(!_5, reduce(T76, s(s(0)), 119, X148)) | ','(vowel_h_w_y(119), ','(!_5, reduce(T76, s(s(0)), 119, X148))), SCOPE: 6, CLAUSE: 13\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(vowel_h_w_y(T75), ','(!_5, reduce(T76, s(s(0)), T75, X148))), SCOPE: 6, CLAUSE: 13\n\nT75 is ground\nT76 is ground\nX148 is free\nvowel_h_w_y(T75) !=? vowel_h_w_y(97)\nvowel_h_w_y(T75) !=? vowel_h_w_y(101)\nvowel_h_w_y(T75) !=? vowel_h_w_y(105)\nvowel_h_w_y(T75) !=? vowel_h_w_y(111)\nvowel_h_w_y(T75) !=? vowel_h_w_y(117)\nvowel_h_w_y(T75) !=? vowel_h_w_y(104)\nvowel_h_w_y(T75) !=? vowel_h_w_y(119)", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: reduce(T76, s(s(0)), 119, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(!_5, reduce(T76, s(s(0)), 121, X148))\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: reduce(T76, s(s(0)), 121, X148)\n\nT76 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX113 is free\nX122 is free\nX123 is free\nreduce(T60, s(s(0)), T59, X113) !=? reduce([], X122, X123, [])", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: reduce(T60, s(s(0)), T59, X113), SCOPE: 5, CLAUSE: 5\n\nT59 is ground\nT60 is ground\nX113 is free\nX122 is free\nX123 is free\nreduce(T60, s(s(0)), T59, X113) !=? reduce([], X122, X123, [])", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(!_5, reduce(T94, s(s(0)), T93, X189))\n\nT93 is ground\nT94 is ground\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: reduce(T94, s(s(0)), T93, X189)\n\nT93 is ground\nT94 is ground\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="E: reduce(T103, s(s(s(0))), T102, X209)\n\nT102 is ground\nT103 is ground\nX209 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 1 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 2 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 3 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 4 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 5\n\nT102 is ground\nT103 is ground\nX209 is free", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 2 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 3 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 4 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 5\n\nT102 is ground\nT103 is ground\nX209 is free", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: !_7 | reduce([], s(s(s(0))), T109, X209), SCOPE: 7, CLAUSE: 3 | reduce([], s(s(s(0))), T109, X209), SCOPE: 7, CLAUSE: 4 | reduce([], s(s(s(0))), T109, X209), SCOPE: 7, CLAUSE: 5\n\nT109 is ground\nX209 is free", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 3 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 4 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 5\n\nT102 is ground\nT103 is ground\nX209 is free\nX218 is free\nX219 is free\nreduce(T103, s(s(s(0))), T102, X209) !=? reduce([], X218, X219, [])", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 3\n\nT102 is ground\nT103 is ground\nX209 is free\nX218 is free\nX219 is free\nreduce(T103, s(s(s(0))), T102, X209) !=? reduce([], X218, X219, [])", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 4 | reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 5\n\nT102 is ground\nT103 is ground\nX209 is free\nX218 is free\nX219 is free\nreduce(T103, s(s(s(0))), T102, X209) !=? reduce([], X218, X219, [])", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244)))\n\nT118 is ground\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 6 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 7 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 8 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: ','(!_7, reduce(T119, s(s(s(0))), 97, X244)) | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 7 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 8 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(97), ','(!_7, reduce(T119, s(s(s(0))), 97, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 7 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 8 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: reduce(T119, s(s(s(0))), 97, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: ','(!_7, reduce(T119, s(s(s(0))), 101, X244)) | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 8 | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(101), ','(!_7, reduce(T119, s(s(s(0))), 101, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 8 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: reduce(T119, s(s(s(0))), 101, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: ','(!_7, reduce(T119, s(s(s(0))), 105, X244)) | ','(vowel_h_w_y(105), ','(!_7, reduce(T119, s(s(s(0))), 105, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(105), ','(!_7, reduce(T119, s(s(s(0))), 105, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(105), ','(!_7, reduce(T119, s(s(s(0))), 105, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(105), ','(!_7, reduce(T119, s(s(s(0))), 105, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(105), ','(!_7, reduce(T119, s(s(s(0))), 105, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 9 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)\nvowel_h_w_y(T118) !=? vowel_h_w_y(105)", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: reduce(T119, s(s(s(0))), 105, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: ','(!_7, reduce(T119, s(s(s(0))), 111, X244)) | ','(vowel_h_w_y(111), ','(!_7, reduce(T119, s(s(s(0))), 111, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(111), ','(!_7, reduce(T119, s(s(s(0))), 111, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(111), ','(!_7, reduce(T119, s(s(s(0))), 111, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(111), ','(!_7, reduce(T119, s(s(s(0))), 111, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 10 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)\nvowel_h_w_y(T118) !=? vowel_h_w_y(105)\nvowel_h_w_y(T118) !=? vowel_h_w_y(111)", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: reduce(T119, s(s(s(0))), 111, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: ','(!_7, reduce(T119, s(s(s(0))), 117, X244)) | ','(vowel_h_w_y(117), ','(!_7, reduce(T119, s(s(s(0))), 117, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(117), ','(!_7, reduce(T119, s(s(s(0))), 117, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(117), ','(!_7, reduce(T119, s(s(s(0))), 117, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 11 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)\nvowel_h_w_y(T118) !=? vowel_h_w_y(105)\nvowel_h_w_y(T118) !=? vowel_h_w_y(111)\nvowel_h_w_y(T118) !=? vowel_h_w_y(117)", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: reduce(T119, s(s(s(0))), 117, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: ','(!_7, reduce(T119, s(s(s(0))), 104, X244)) | ','(vowel_h_w_y(104), ','(!_7, reduce(T119, s(s(s(0))), 104, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(104), ','(!_7, reduce(T119, s(s(s(0))), 104, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 12 | ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)\nvowel_h_w_y(T118) !=? vowel_h_w_y(105)\nvowel_h_w_y(T118) !=? vowel_h_w_y(111)\nvowel_h_w_y(T118) !=? vowel_h_w_y(117)\nvowel_h_w_y(T118) !=? vowel_h_w_y(104)", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: reduce(T119, s(s(s(0))), 104, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: ','(!_7, reduce(T119, s(s(s(0))), 119, X244)) | ','(vowel_h_w_y(119), ','(!_7, reduce(T119, s(s(s(0))), 119, X244))), SCOPE: 8, CLAUSE: 13\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: ','(vowel_h_w_y(T118), ','(!_7, reduce(T119, s(s(s(0))), T118, X244))), SCOPE: 8, CLAUSE: 13\n\nT118 is ground\nT119 is ground\nX244 is free\nvowel_h_w_y(T118) !=? vowel_h_w_y(97)\nvowel_h_w_y(T118) !=? vowel_h_w_y(101)\nvowel_h_w_y(T118) !=? vowel_h_w_y(105)\nvowel_h_w_y(T118) !=? vowel_h_w_y(111)\nvowel_h_w_y(T118) !=? vowel_h_w_y(117)\nvowel_h_w_y(T118) !=? vowel_h_w_y(104)\nvowel_h_w_y(T118) !=? vowel_h_w_y(119)", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: reduce(T119, s(s(s(0))), 119, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(!_7, reduce(T119, s(s(s(0))), 121, X244))\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: reduce(T119, s(s(s(0))), 121, X244)\n\nT119 is ground\nX244 is free", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 4\n\nT102 is ground\nT103 is ground\nX209 is free\nX218 is free\nX219 is free\nreduce(T103, s(s(s(0))), T102, X209) !=? reduce([], X218, X219, [])", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: reduce(T103, s(s(s(0))), T102, X209), SCOPE: 7, CLAUSE: 5\n\nT102 is ground\nT103 is ground\nX209 is free\nX218 is free\nX219 is free\nreduce(T103, s(s(s(0))), T102, X209) !=? reduce([], X218, X219, [])", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: ','(!_7, reduce(T137, s(s(s(0))), T136, X285))\n\nT136 is ground\nT137 is ground\nX285 is free", fontsize=16, style=filled, fillcolor=lightyellow];
395 [label="395: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
398 [label="398: reduce(T137, s(s(s(0))), T136, X285)\n\nT136 is ground\nT137 is ground\nX285 is free", fontsize=16, style=filled, fillcolor=lightyellow];
407 [label="407: reduce(T146, s(s(s(s(0)))), T145, X305)\n\nT145 is ground\nT146 is ground\nX305 is free", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: reduce(T146, s(s(s(s(0)))), T145, X305), SCOPE: 9, CLAUSE: 1 | reduce(T146, s(s(s(s(0)))), T145, X305), SCOPE: 9, CLAUSE: 2 | reduce(T146, s(s(s(s(0)))), T145, X305), SCOPE: 9, CLAUSE: 3 | reduce(T146, s(s(s(s(0)))), T145, X305), SCOPE: 9, CLAUSE: 4 | reduce(T146, s(s(s(s(0)))), T145, X305), SCOPE: 9, CLAUSE: 5\n\nT145 is ground\nT146 is ground\nX305 is free", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: !_9 | reduce(T154, s(s(s(s(0)))), T155, X305), SCOPE: 9, CLAUSE: 2 | reduce(T154, s(s(s(s(0)))), T155, X305), SCOPE: 9, CLAUSE: 3 | reduce(T154, s(s(s(s(0)))), T155, X305), SCOPE: 9, CLAUSE: 4 | reduce(T154, s(s(s(s(0)))), T155, X305), SCOPE: 9, CLAUSE: 5\n\nT154 is ground\nT155 is ground\nX305 is free", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: eq(T7, T18), SCOPE: 10, CLAUSE: 14\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
417 [label="417: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 419 [arrowhead = none ];
419 -> 6;

420 [label="ONLY EVAL with clause\ngoal(X8, X9) :- ','(eq(X8, .(X10, X11)), ','(reduce(X11, s(0), X10, X12), eq(X9, X12))).\nand substitutionT1 -> T5,\nX8 -> T5,\nT2 -> T7,\nX9 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 420 [arrowhead = none ];
420 -> 8;

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

422 [label="EVAL with clause\neq(X15, X15).\nand substitutionT5 -> .(T15, T16),\nX15 -> .(T15, T16),\nX10 -> T15,\nX11 -> T16,\nT14 -> .(T15, T16)", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 422 [arrowhead = none ];
422 -> 14;

423 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 423 [arrowhead = none ];
423 -> 16;

424 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 424 [arrowhead = none ];
424 -> 21;

425 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT15 is ground\nT18 is ground\nreplacements:X12 -> T18", fontsize=14, style = filled, fillcolor = violet];
14 -> 425 [arrowhead = none ];
425 -> 23;

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

427 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 427 [arrowhead = none ];
427 -> 415;

428 [label="BACKTRACK\nfor clause: reduce(X1, s(s(s(s(0)))), X2, []) :- !because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 428 [arrowhead = none ];
428 -> 30;

429 [label="EVAL with clause\nreduce([], X26, X27, []) :- !_3.\nand substitutionT16 -> [],\nX26 -> s(0),\nT15 -> T23,\nX27 -> T23,\nX12 -> []", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 429 [arrowhead = none ];
429 -> 32;

430 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 430 [arrowhead = none ];
430 -> 34;

431 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 431 [arrowhead = none ];
431 -> 36;

432 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 432 [arrowhead = none ];
432 -> 41;

433 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 433 [arrowhead = none ];
433 -> 44;

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

435 [label="EVAL with clause\nreduce(.(X48, X49), X50, X48, X51) :- ','(vowel_h_w_y(X48), ','(!_3, reduce(X49, X50, X48, X51))).\nand substitutionX48 -> T32,\nX49 -> T33,\nT16 -> .(T32, T33),\nX50 -> s(0),\nT15 -> T32,\nX12 -> X52,\nX51 -> X52", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 435 [arrowhead = none ];
435 -> 50;

436 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 436 [arrowhead = none ];
436 -> 52;

437 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 437 [arrowhead = none ];
437 -> 132;

438 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 438 [arrowhead = none ];
438 -> 133;

439 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 439 [arrowhead = none ];
439 -> 54;

440 [label="EVAL with clause\nvowel_h_w_y(97).\nand substitutionT32 -> 97", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 440 [arrowhead = none ];
440 -> 57;

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

442 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 442 [arrowhead = none ];
442 -> 62;

443 [label="EVAL with clause\nvowel_h_w_y(101).\nand substitutionT32 -> 101", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 443 [arrowhead = none ];
443 -> 68;

444 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 444 [arrowhead = none ];
444 -> 70;

445 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 97\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 445 [arrowhead = none , style=dashed];
445 -> 21[style=dashed];

446 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 446 [arrowhead = none ];
446 -> 72;

447 [label="EVAL with clause\nvowel_h_w_y(105).\nand substitutionT32 -> 105", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 447 [arrowhead = none ];
447 -> 77;

448 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 448 [arrowhead = none ];
448 -> 80;

449 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 101\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 449 [arrowhead = none , style=dashed];
449 -> 21[style=dashed];

450 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 450 [arrowhead = none ];
450 -> 82;

451 [label="EVAL with clause\nvowel_h_w_y(111).\nand substitutionT32 -> 111", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 451 [arrowhead = none ];
451 -> 86;

452 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 452 [arrowhead = none ];
452 -> 90;

453 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 105\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 453 [arrowhead = none , style=dashed];
453 -> 21[style=dashed];

454 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 454 [arrowhead = none ];
454 -> 91;

455 [label="EVAL with clause\nvowel_h_w_y(117).\nand substitutionT32 -> 117", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 455 [arrowhead = none ];
455 -> 95;

456 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 456 [arrowhead = none ];
456 -> 99;

457 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 111\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 457 [arrowhead = none , style=dashed];
457 -> 21[style=dashed];

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

459 [label="EVAL with clause\nvowel_h_w_y(104).\nand substitutionT32 -> 104", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 459 [arrowhead = none ];
459 -> 104;

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

461 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 117\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 461 [arrowhead = none , style=dashed];
461 -> 21[style=dashed];

462 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 462 [arrowhead = none ];
462 -> 110;

463 [label="EVAL with clause\nvowel_h_w_y(119).\nand substitutionT32 -> 119", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 463 [arrowhead = none ];
463 -> 113;

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

465 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 104\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 465 [arrowhead = none , style=dashed];
465 -> 21[style=dashed];

466 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 466 [arrowhead = none ];
466 -> 119;

467 [label="EVAL with clause\nvowel_h_w_y(121).\nand substitutionT32 -> 121", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 467 [arrowhead = none ];
467 -> 124;

468 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 468 [arrowhead = none ];
468 -> 126;

469 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 119\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 469 [arrowhead = none , style=dashed];
469 -> 21[style=dashed];

470 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 470 [arrowhead = none ];
470 -> 127;

471 [label="INSTANCE with matching:\nT16 -> T33\nT15 -> 121\nX12 -> X52", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 471 [arrowhead = none , style=dashed];
471 -> 21[style=dashed];

472 [label="EVAL with clause\nreduce(.(X89, X90), X91, X89, X92) :- ','(!_3, reduce(X90, X91, X89, X92)).\nand substitutionX89 -> T50,\nX90 -> T51,\nT16 -> .(T50, T51),\nX91 -> s(0),\nT15 -> T50,\nX12 -> X93,\nX92 -> X93", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 472 [arrowhead = none ];
472 -> 139;

473 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 473 [arrowhead = none ];
473 -> 140;

474 [label="EVAL with clause\nreduce(.(X108, X109), X110, X111, .(X108, X112)) :- reduce(X109, s(X110), X108, X112).\nand substitutionX108 -> T59,\nX109 -> T60,\nT16 -> .(T59, T60),\nX110 -> s(0),\nT15 -> T61,\nX111 -> T61,\nX112 -> X113,\nX12 -> .(T59, X113)", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 474 [arrowhead = none ];
474 -> 149;

475 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 475 [arrowhead = none ];
475 -> 150;

476 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 476 [arrowhead = none ];
476 -> 141;

477 [label="INSTANCE with matching:\nT16 -> T51\nT15 -> T50\nX12 -> X93", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 477 [arrowhead = none , style=dashed];
477 -> 21[style=dashed];

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

479 [label="BACKTRACK\nfor clause: reduce(X1, s(s(s(s(0)))), X2, []) :- !because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 479 [arrowhead = none ];
479 -> 155;

480 [label="EVAL with clause\nreduce([], X122, X123, []) :- !_5.\nand substitutionT60 -> [],\nX122 -> s(s(0)),\nT59 -> T66,\nX123 -> T66,\nX113 -> []", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 480 [arrowhead = none ];
480 -> 160;

481 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 481 [arrowhead = none ];
481 -> 161;

482 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 482 [arrowhead = none ];
482 -> 162;

483 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 483 [arrowhead = none ];
483 -> 171;

484 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 484 [arrowhead = none ];
484 -> 172;

485 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 485 [arrowhead = none ];
485 -> 164;

486 [label="EVAL with clause\nreduce(.(X144, X145), X146, X144, X147) :- ','(vowel_h_w_y(X144), ','(!_5, reduce(X145, X146, X144, X147))).\nand substitutionX144 -> T75,\nX145 -> T76,\nT60 -> .(T75, T76),\nX146 -> s(s(0)),\nT59 -> T75,\nX113 -> X148,\nX147 -> X148", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 486 [arrowhead = none ];
486 -> 181;

487 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 487 [arrowhead = none ];
487 -> 184;

488 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 488 [arrowhead = none ];
488 -> 262;

489 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 489 [arrowhead = none ];
489 -> 264;

490 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
181 -> 490 [arrowhead = none ];
490 -> 186;

491 [label="EVAL with clause\nvowel_h_w_y(97).\nand substitutionT75 -> 97", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 491 [arrowhead = none ];
491 -> 187;

492 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 492 [arrowhead = none ];
492 -> 188;

493 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
187 -> 493 [arrowhead = none ];
493 -> 189;

494 [label="EVAL with clause\nvowel_h_w_y(101).\nand substitutionT75 -> 101", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 494 [arrowhead = none ];
494 -> 196;

495 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
188 -> 495 [arrowhead = none ];
495 -> 197;

496 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 97\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
189 -> 496 [arrowhead = none , style=dashed];
496 -> 149[style=dashed];

497 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 497 [arrowhead = none ];
497 -> 198;

498 [label="EVAL with clause\nvowel_h_w_y(105).\nand substitutionT75 -> 105", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 498 [arrowhead = none ];
498 -> 205;

499 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 499 [arrowhead = none ];
499 -> 206;

500 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 101\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 500 [arrowhead = none , style=dashed];
500 -> 149[style=dashed];

501 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 501 [arrowhead = none ];
501 -> 208;

502 [label="EVAL with clause\nvowel_h_w_y(111).\nand substitutionT75 -> 111", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 502 [arrowhead = none ];
502 -> 214;

503 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 503 [arrowhead = none ];
503 -> 215;

504 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 105\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 504 [arrowhead = none , style=dashed];
504 -> 149[style=dashed];

505 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 505 [arrowhead = none ];
505 -> 217;

506 [label="EVAL with clause\nvowel_h_w_y(117).\nand substitutionT75 -> 117", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 506 [arrowhead = none ];
506 -> 223;

507 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
215 -> 507 [arrowhead = none ];
507 -> 224;

508 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 111\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
217 -> 508 [arrowhead = none , style=dashed];
508 -> 149[style=dashed];

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

510 [label="EVAL with clause\nvowel_h_w_y(104).\nand substitutionT75 -> 104", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 510 [arrowhead = none ];
510 -> 232;

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

512 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 117\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
225 -> 512 [arrowhead = none , style=dashed];
512 -> 149[style=dashed];

513 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 513 [arrowhead = none ];
513 -> 235;

514 [label="EVAL with clause\nvowel_h_w_y(119).\nand substitutionT75 -> 119", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 514 [arrowhead = none ];
514 -> 241;

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

516 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 104\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
235 -> 516 [arrowhead = none , style=dashed];
516 -> 149[style=dashed];

517 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
241 -> 517 [arrowhead = none ];
517 -> 244;

518 [label="EVAL with clause\nvowel_h_w_y(121).\nand substitutionT75 -> 121", fontsize=14, style = filled, fillcolor = lightblue];
243 -> 518 [arrowhead = none ];
518 -> 249;

519 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 519 [arrowhead = none ];
519 -> 251;

520 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 119\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
244 -> 520 [arrowhead = none , style=dashed];
520 -> 149[style=dashed];

521 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 521 [arrowhead = none ];
521 -> 252;

522 [label="INSTANCE with matching:\nT60 -> T76\nT59 -> 121\nX113 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
252 -> 522 [arrowhead = none , style=dashed];
522 -> 149[style=dashed];

523 [label="EVAL with clause\nreduce(.(X185, X186), X187, X185, X188) :- ','(!_5, reduce(X186, X187, X185, X188)).\nand substitutionX185 -> T93,\nX186 -> T94,\nT60 -> .(T93, T94),\nX187 -> s(s(0)),\nT59 -> T93,\nX113 -> X189,\nX188 -> X189", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 523 [arrowhead = none ];
523 -> 269;

524 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 524 [arrowhead = none ];
524 -> 270;

525 [label="EVAL with clause\nreduce(.(X204, X205), X206, X207, .(X204, X208)) :- reduce(X205, s(X206), X204, X208).\nand substitutionX204 -> T102,\nX205 -> T103,\nT60 -> .(T102, T103),\nX206 -> s(s(0)),\nT59 -> T104,\nX207 -> T104,\nX208 -> X209,\nX113 -> .(T102, X209)", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 525 [arrowhead = none ];
525 -> 281;

526 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
264 -> 526 [arrowhead = none ];
526 -> 282;

527 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 527 [arrowhead = none ];
527 -> 271;

528 [label="INSTANCE with matching:\nT60 -> T94\nT59 -> T93\nX113 -> X189", fontsize=14, style = filled, fillcolor = lightgrey];
271 -> 528 [arrowhead = none , style=dashed];
528 -> 149[style=dashed];

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

530 [label="BACKTRACK\nfor clause: reduce(X1, s(s(s(s(0)))), X2, []) :- !because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
284 -> 530 [arrowhead = none ];
530 -> 286;

531 [label="EVAL with clause\nreduce([], X218, X219, []) :- !_7.\nand substitutionT103 -> [],\nX218 -> s(s(s(0))),\nT102 -> T109,\nX219 -> T109,\nX209 -> []", fontsize=14, style = filled, fillcolor = lightblue];
286 -> 531 [arrowhead = none ];
531 -> 291;

532 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
286 -> 532 [arrowhead = none ];
532 -> 294;

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

534 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
294 -> 534 [arrowhead = none ];
534 -> 303;

535 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
294 -> 535 [arrowhead = none ];
535 -> 304;

536 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
295 -> 536 [arrowhead = none ];
536 -> 296;

537 [label="EVAL with clause\nreduce(.(X240, X241), X242, X240, X243) :- ','(vowel_h_w_y(X240), ','(!_7, reduce(X241, X242, X240, X243))).\nand substitutionX240 -> T118,\nX241 -> T119,\nT103 -> .(T118, T119),\nX242 -> s(s(s(0))),\nT102 -> T118,\nX209 -> X244,\nX243 -> X244", fontsize=14, style = filled, fillcolor = lightblue];
303 -> 537 [arrowhead = none ];
537 -> 311;

538 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
303 -> 538 [arrowhead = none ];
538 -> 314;

539 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
304 -> 539 [arrowhead = none ];
539 -> 389;

540 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
304 -> 540 [arrowhead = none ];
540 -> 390;

541 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
311 -> 541 [arrowhead = none ];
541 -> 315;

542 [label="EVAL with clause\nvowel_h_w_y(97).\nand substitutionT118 -> 97", fontsize=14, style = filled, fillcolor = lightblue];
315 -> 542 [arrowhead = none ];
542 -> 316;

543 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
315 -> 543 [arrowhead = none ];
543 -> 318;

544 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
316 -> 544 [arrowhead = none ];
544 -> 319;

545 [label="EVAL with clause\nvowel_h_w_y(101).\nand substitutionT118 -> 101", fontsize=14, style = filled, fillcolor = lightblue];
318 -> 545 [arrowhead = none ];
545 -> 328;

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

547 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 97\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
319 -> 547 [arrowhead = none , style=dashed];
547 -> 281[style=dashed];

548 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
328 -> 548 [arrowhead = none ];
548 -> 330;

549 [label="EVAL with clause\nvowel_h_w_y(105).\nand substitutionT118 -> 105", fontsize=14, style = filled, fillcolor = lightblue];
329 -> 549 [arrowhead = none ];
549 -> 336;

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

551 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 101\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
330 -> 551 [arrowhead = none , style=dashed];
551 -> 281[style=dashed];

552 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
336 -> 552 [arrowhead = none ];
552 -> 339;

553 [label="EVAL with clause\nvowel_h_w_y(111).\nand substitutionT118 -> 111", fontsize=14, style = filled, fillcolor = lightblue];
338 -> 553 [arrowhead = none ];
553 -> 345;

554 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
338 -> 554 [arrowhead = none ];
554 -> 347;

555 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 105\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
339 -> 555 [arrowhead = none , style=dashed];
555 -> 281[style=dashed];

556 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
345 -> 556 [arrowhead = none ];
556 -> 348;

557 [label="EVAL with clause\nvowel_h_w_y(117).\nand substitutionT118 -> 117", fontsize=14, style = filled, fillcolor = lightblue];
347 -> 557 [arrowhead = none ];
557 -> 351;

558 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
347 -> 558 [arrowhead = none ];
558 -> 356;

559 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 111\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
348 -> 559 [arrowhead = none , style=dashed];
559 -> 281[style=dashed];

560 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
351 -> 560 [arrowhead = none ];
560 -> 357;

561 [label="EVAL with clause\nvowel_h_w_y(104).\nand substitutionT118 -> 104", fontsize=14, style = filled, fillcolor = lightblue];
356 -> 561 [arrowhead = none ];
561 -> 362;

562 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
356 -> 562 [arrowhead = none ];
562 -> 365;

563 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 117\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
357 -> 563 [arrowhead = none , style=dashed];
563 -> 281[style=dashed];

564 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
362 -> 564 [arrowhead = none ];
564 -> 366;

565 [label="EVAL with clause\nvowel_h_w_y(119).\nand substitutionT118 -> 119", fontsize=14, style = filled, fillcolor = lightblue];
365 -> 565 [arrowhead = none ];
565 -> 370;

566 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
365 -> 566 [arrowhead = none ];
566 -> 373;

567 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 104\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
366 -> 567 [arrowhead = none , style=dashed];
567 -> 281[style=dashed];

568 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
370 -> 568 [arrowhead = none ];
568 -> 374;

569 [label="EVAL with clause\nvowel_h_w_y(121).\nand substitutionT118 -> 121", fontsize=14, style = filled, fillcolor = lightblue];
373 -> 569 [arrowhead = none ];
569 -> 381;

570 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
373 -> 570 [arrowhead = none ];
570 -> 382;

571 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 119\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
374 -> 571 [arrowhead = none , style=dashed];
571 -> 281[style=dashed];

572 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
381 -> 572 [arrowhead = none ];
572 -> 383;

573 [label="INSTANCE with matching:\nT103 -> T119\nT102 -> 121\nX209 -> X244", fontsize=14, style = filled, fillcolor = lightgrey];
383 -> 573 [arrowhead = none , style=dashed];
573 -> 281[style=dashed];

574 [label="EVAL with clause\nreduce(.(X281, X282), X283, X281, X284) :- ','(!_7, reduce(X282, X283, X281, X284)).\nand substitutionX281 -> T136,\nX282 -> T137,\nT103 -> .(T136, T137),\nX283 -> s(s(s(0))),\nT102 -> T136,\nX209 -> X285,\nX284 -> X285", fontsize=14, style = filled, fillcolor = lightblue];
389 -> 574 [arrowhead = none ];
574 -> 392;

575 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
389 -> 575 [arrowhead = none ];
575 -> 395;

576 [label="EVAL with clause\nreduce(.(X300, X301), X302, X303, .(X300, X304)) :- reduce(X301, s(X302), X300, X304).\nand substitutionX300 -> T145,\nX301 -> T146,\nT103 -> .(T145, T146),\nX302 -> s(s(s(0))),\nT102 -> T147,\nX303 -> T147,\nX304 -> X305,\nX209 -> .(T145, X305)", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 576 [arrowhead = none ];
576 -> 407;

577 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
390 -> 577 [arrowhead = none ];
577 -> 408;

578 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
392 -> 578 [arrowhead = none ];
578 -> 398;

579 [label="INSTANCE with matching:\nT103 -> T137\nT102 -> T136\nX209 -> X285", fontsize=14, style = filled, fillcolor = lightgrey];
398 -> 579 [arrowhead = none , style=dashed];
579 -> 281[style=dashed];

580 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
407 -> 580 [arrowhead = none ];
580 -> 409;

581 [label="ONLY EVAL with clause\nreduce(X312, s(s(s(s(0)))), X313, []) :- !_9.\nand substitutionT146 -> T154,\nX312 -> T154,\nT145 -> T155,\nX313 -> T155,\nX305 -> []", fontsize=14, style = filled, fillcolor = lightblue];
409 -> 581 [arrowhead = none ];
581 -> 412;

582 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
412 -> 582 [arrowhead = none ];
582 -> 413;

583 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
413 -> 583 [arrowhead = none ];
583 -> 414;

584 [label="EVAL with clause\neq(X316, X316).\nand substitutionT7 -> T158,\nX316 -> T158,\nT18 -> T158", fontsize=14, style = filled, fillcolor = lightblue];
415 -> 584 [arrowhead = none ];
584 -> 416;

585 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
415 -> 585 [arrowhead = none ];
585 -> 417;

586 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
416 -> 586 [arrowhead = none ];
586 -> 418;

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOALA_IN_GA(.(T15, T16), T7) → U1_GA(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
GOALA_IN_GA(.(T15, T16), T7) → PB_IN_GGAA(T16, T15, X12, T7)
PB_IN_GGAA(T16, T15, T18, T7) → U31_GGAA(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
PB_IN_GGAA(T16, T15, T18, T7) → REDUCEC_IN_GGA(T16, T15, T18)
REDUCEC_IN_GGA(.(97, T33), 97, X52) → U2_GGA(T33, X52, reduceC_in_gga(T33, 97, X52))
REDUCEC_IN_GGA(.(97, T33), 97, X52) → REDUCEC_IN_GGA(T33, 97, X52)
REDUCEC_IN_GGA(.(101, T33), 101, X52) → U3_GGA(T33, X52, reduceC_in_gga(T33, 101, X52))
REDUCEC_IN_GGA(.(101, T33), 101, X52) → REDUCEC_IN_GGA(T33, 101, X52)
REDUCEC_IN_GGA(.(105, T33), 105, X52) → U4_GGA(T33, X52, reduceC_in_gga(T33, 105, X52))
REDUCEC_IN_GGA(.(105, T33), 105, X52) → REDUCEC_IN_GGA(T33, 105, X52)
REDUCEC_IN_GGA(.(111, T33), 111, X52) → U5_GGA(T33, X52, reduceC_in_gga(T33, 111, X52))
REDUCEC_IN_GGA(.(111, T33), 111, X52) → REDUCEC_IN_GGA(T33, 111, X52)
REDUCEC_IN_GGA(.(117, T33), 117, X52) → U6_GGA(T33, X52, reduceC_in_gga(T33, 117, X52))
REDUCEC_IN_GGA(.(117, T33), 117, X52) → REDUCEC_IN_GGA(T33, 117, X52)
REDUCEC_IN_GGA(.(104, T33), 104, X52) → U7_GGA(T33, X52, reduceC_in_gga(T33, 104, X52))
REDUCEC_IN_GGA(.(104, T33), 104, X52) → REDUCEC_IN_GGA(T33, 104, X52)
REDUCEC_IN_GGA(.(119, T33), 119, X52) → U8_GGA(T33, X52, reduceC_in_gga(T33, 119, X52))
REDUCEC_IN_GGA(.(119, T33), 119, X52) → REDUCEC_IN_GGA(T33, 119, X52)
REDUCEC_IN_GGA(.(121, T33), 121, X52) → U9_GGA(T33, X52, reduceC_in_gga(T33, 121, X52))
REDUCEC_IN_GGA(.(121, T33), 121, X52) → REDUCEC_IN_GGA(T33, 121, X52)
REDUCEC_IN_GGA(.(T50, T51), T50, X93) → U10_GGA(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
REDUCEC_IN_GGA(.(T50, T51), T50, X93) → REDUCEC_IN_GGA(T51, T50, X93)
REDUCEC_IN_GGA(.(T59, T60), T61, .(T59, X113)) → U11_GGA(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
REDUCEC_IN_GGA(.(T59, T60), T61, .(T59, X113)) → REDUCED_IN_GGA(T60, T59, X113)
REDUCED_IN_GGA(.(97, T76), 97, X148) → U12_GGA(T76, X148, reduceD_in_gga(T76, 97, X148))
REDUCED_IN_GGA(.(97, T76), 97, X148) → REDUCED_IN_GGA(T76, 97, X148)
REDUCED_IN_GGA(.(101, T76), 101, X148) → U13_GGA(T76, X148, reduceD_in_gga(T76, 101, X148))
REDUCED_IN_GGA(.(101, T76), 101, X148) → REDUCED_IN_GGA(T76, 101, X148)
REDUCED_IN_GGA(.(105, T76), 105, X148) → U14_GGA(T76, X148, reduceD_in_gga(T76, 105, X148))
REDUCED_IN_GGA(.(105, T76), 105, X148) → REDUCED_IN_GGA(T76, 105, X148)
REDUCED_IN_GGA(.(111, T76), 111, X148) → U15_GGA(T76, X148, reduceD_in_gga(T76, 111, X148))
REDUCED_IN_GGA(.(111, T76), 111, X148) → REDUCED_IN_GGA(T76, 111, X148)
REDUCED_IN_GGA(.(117, T76), 117, X148) → U16_GGA(T76, X148, reduceD_in_gga(T76, 117, X148))
REDUCED_IN_GGA(.(117, T76), 117, X148) → REDUCED_IN_GGA(T76, 117, X148)
REDUCED_IN_GGA(.(104, T76), 104, X148) → U17_GGA(T76, X148, reduceD_in_gga(T76, 104, X148))
REDUCED_IN_GGA(.(104, T76), 104, X148) → REDUCED_IN_GGA(T76, 104, X148)
REDUCED_IN_GGA(.(119, T76), 119, X148) → U18_GGA(T76, X148, reduceD_in_gga(T76, 119, X148))
REDUCED_IN_GGA(.(119, T76), 119, X148) → REDUCED_IN_GGA(T76, 119, X148)
REDUCED_IN_GGA(.(121, T76), 121, X148) → U19_GGA(T76, X148, reduceD_in_gga(T76, 121, X148))
REDUCED_IN_GGA(.(121, T76), 121, X148) → REDUCED_IN_GGA(T76, 121, X148)
REDUCED_IN_GGA(.(T93, T94), T93, X189) → U20_GGA(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
REDUCED_IN_GGA(.(T93, T94), T93, X189) → REDUCED_IN_GGA(T94, T93, X189)
REDUCED_IN_GGA(.(T102, T103), T104, .(T102, X209)) → U21_GGA(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
REDUCED_IN_GGA(.(T102, T103), T104, .(T102, X209)) → REDUCEE_IN_GGA(T103, T102, X209)
REDUCEE_IN_GGA(.(97, T119), 97, X244) → U22_GGA(T119, X244, reduceE_in_gga(T119, 97, X244))
REDUCEE_IN_GGA(.(97, T119), 97, X244) → REDUCEE_IN_GGA(T119, 97, X244)
REDUCEE_IN_GGA(.(101, T119), 101, X244) → U23_GGA(T119, X244, reduceE_in_gga(T119, 101, X244))
REDUCEE_IN_GGA(.(101, T119), 101, X244) → REDUCEE_IN_GGA(T119, 101, X244)
REDUCEE_IN_GGA(.(105, T119), 105, X244) → U24_GGA(T119, X244, reduceE_in_gga(T119, 105, X244))
REDUCEE_IN_GGA(.(105, T119), 105, X244) → REDUCEE_IN_GGA(T119, 105, X244)
REDUCEE_IN_GGA(.(111, T119), 111, X244) → U25_GGA(T119, X244, reduceE_in_gga(T119, 111, X244))
REDUCEE_IN_GGA(.(111, T119), 111, X244) → REDUCEE_IN_GGA(T119, 111, X244)
REDUCEE_IN_GGA(.(117, T119), 117, X244) → U26_GGA(T119, X244, reduceE_in_gga(T119, 117, X244))
REDUCEE_IN_GGA(.(117, T119), 117, X244) → REDUCEE_IN_GGA(T119, 117, X244)
REDUCEE_IN_GGA(.(104, T119), 104, X244) → U27_GGA(T119, X244, reduceE_in_gga(T119, 104, X244))
REDUCEE_IN_GGA(.(104, T119), 104, X244) → REDUCEE_IN_GGA(T119, 104, X244)
REDUCEE_IN_GGA(.(119, T119), 119, X244) → U28_GGA(T119, X244, reduceE_in_gga(T119, 119, X244))
REDUCEE_IN_GGA(.(119, T119), 119, X244) → REDUCEE_IN_GGA(T119, 119, X244)
REDUCEE_IN_GGA(.(121, T119), 121, X244) → U29_GGA(T119, X244, reduceE_in_gga(T119, 121, X244))
REDUCEE_IN_GGA(.(121, T119), 121, X244) → REDUCEE_IN_GGA(T119, 121, X244)
REDUCEE_IN_GGA(.(T136, T137), T136, X285) → U30_GGA(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
REDUCEE_IN_GGA(.(T136, T137), T136, X285) → REDUCEE_IN_GGA(T137, T136, X285)
U31_GGAA(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_GGAA(T16, T15, T18, T7, eqF_in_ag(T7, T18))
U31_GGAA(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → EQF_IN_AG(T7, T18)

The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)
GOALA_IN_GA(x1, x2)  =  GOALA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U31_GGAA(x1, x2, x3, x4, x5)  =  U31_GGAA(x1, x2, x5)
REDUCEC_IN_GGA(x1, x2, x3)  =  REDUCEC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3)  =  U2_GGA(x1, x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
U4_GGA(x1, x2, x3)  =  U4_GGA(x1, x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4, x5)  =  U11_GGA(x1, x2, x3, x5)
REDUCED_IN_GGA(x1, x2, x3)  =  REDUCED_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4, x5)  =  U21_GGA(x1, x2, x3, x5)
REDUCEE_IN_GGA(x1, x2, x3)  =  REDUCEE_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3)  =  U22_GGA(x1, x3)
U23_GGA(x1, x2, x3)  =  U23_GGA(x1, x3)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
U25_GGA(x1, x2, x3)  =  U25_GGA(x1, x3)
U26_GGA(x1, x2, x3)  =  U26_GGA(x1, x3)
U27_GGA(x1, x2, x3)  =  U27_GGA(x1, x3)
U28_GGA(x1, x2, x3)  =  U28_GGA(x1, x3)
U29_GGA(x1, x2, x3)  =  U29_GGA(x1, x3)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U32_GGAA(x1, x2, x3, x4, x5)  =  U32_GGAA(x1, x2, x3, x5)
EQF_IN_AG(x1, x2)  =  EQF_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOALA_IN_GA(.(T15, T16), T7) → U1_GA(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
GOALA_IN_GA(.(T15, T16), T7) → PB_IN_GGAA(T16, T15, X12, T7)
PB_IN_GGAA(T16, T15, T18, T7) → U31_GGAA(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
PB_IN_GGAA(T16, T15, T18, T7) → REDUCEC_IN_GGA(T16, T15, T18)
REDUCEC_IN_GGA(.(97, T33), 97, X52) → U2_GGA(T33, X52, reduceC_in_gga(T33, 97, X52))
REDUCEC_IN_GGA(.(97, T33), 97, X52) → REDUCEC_IN_GGA(T33, 97, X52)
REDUCEC_IN_GGA(.(101, T33), 101, X52) → U3_GGA(T33, X52, reduceC_in_gga(T33, 101, X52))
REDUCEC_IN_GGA(.(101, T33), 101, X52) → REDUCEC_IN_GGA(T33, 101, X52)
REDUCEC_IN_GGA(.(105, T33), 105, X52) → U4_GGA(T33, X52, reduceC_in_gga(T33, 105, X52))
REDUCEC_IN_GGA(.(105, T33), 105, X52) → REDUCEC_IN_GGA(T33, 105, X52)
REDUCEC_IN_GGA(.(111, T33), 111, X52) → U5_GGA(T33, X52, reduceC_in_gga(T33, 111, X52))
REDUCEC_IN_GGA(.(111, T33), 111, X52) → REDUCEC_IN_GGA(T33, 111, X52)
REDUCEC_IN_GGA(.(117, T33), 117, X52) → U6_GGA(T33, X52, reduceC_in_gga(T33, 117, X52))
REDUCEC_IN_GGA(.(117, T33), 117, X52) → REDUCEC_IN_GGA(T33, 117, X52)
REDUCEC_IN_GGA(.(104, T33), 104, X52) → U7_GGA(T33, X52, reduceC_in_gga(T33, 104, X52))
REDUCEC_IN_GGA(.(104, T33), 104, X52) → REDUCEC_IN_GGA(T33, 104, X52)
REDUCEC_IN_GGA(.(119, T33), 119, X52) → U8_GGA(T33, X52, reduceC_in_gga(T33, 119, X52))
REDUCEC_IN_GGA(.(119, T33), 119, X52) → REDUCEC_IN_GGA(T33, 119, X52)
REDUCEC_IN_GGA(.(121, T33), 121, X52) → U9_GGA(T33, X52, reduceC_in_gga(T33, 121, X52))
REDUCEC_IN_GGA(.(121, T33), 121, X52) → REDUCEC_IN_GGA(T33, 121, X52)
REDUCEC_IN_GGA(.(T50, T51), T50, X93) → U10_GGA(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
REDUCEC_IN_GGA(.(T50, T51), T50, X93) → REDUCEC_IN_GGA(T51, T50, X93)
REDUCEC_IN_GGA(.(T59, T60), T61, .(T59, X113)) → U11_GGA(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
REDUCEC_IN_GGA(.(T59, T60), T61, .(T59, X113)) → REDUCED_IN_GGA(T60, T59, X113)
REDUCED_IN_GGA(.(97, T76), 97, X148) → U12_GGA(T76, X148, reduceD_in_gga(T76, 97, X148))
REDUCED_IN_GGA(.(97, T76), 97, X148) → REDUCED_IN_GGA(T76, 97, X148)
REDUCED_IN_GGA(.(101, T76), 101, X148) → U13_GGA(T76, X148, reduceD_in_gga(T76, 101, X148))
REDUCED_IN_GGA(.(101, T76), 101, X148) → REDUCED_IN_GGA(T76, 101, X148)
REDUCED_IN_GGA(.(105, T76), 105, X148) → U14_GGA(T76, X148, reduceD_in_gga(T76, 105, X148))
REDUCED_IN_GGA(.(105, T76), 105, X148) → REDUCED_IN_GGA(T76, 105, X148)
REDUCED_IN_GGA(.(111, T76), 111, X148) → U15_GGA(T76, X148, reduceD_in_gga(T76, 111, X148))
REDUCED_IN_GGA(.(111, T76), 111, X148) → REDUCED_IN_GGA(T76, 111, X148)
REDUCED_IN_GGA(.(117, T76), 117, X148) → U16_GGA(T76, X148, reduceD_in_gga(T76, 117, X148))
REDUCED_IN_GGA(.(117, T76), 117, X148) → REDUCED_IN_GGA(T76, 117, X148)
REDUCED_IN_GGA(.(104, T76), 104, X148) → U17_GGA(T76, X148, reduceD_in_gga(T76, 104, X148))
REDUCED_IN_GGA(.(104, T76), 104, X148) → REDUCED_IN_GGA(T76, 104, X148)
REDUCED_IN_GGA(.(119, T76), 119, X148) → U18_GGA(T76, X148, reduceD_in_gga(T76, 119, X148))
REDUCED_IN_GGA(.(119, T76), 119, X148) → REDUCED_IN_GGA(T76, 119, X148)
REDUCED_IN_GGA(.(121, T76), 121, X148) → U19_GGA(T76, X148, reduceD_in_gga(T76, 121, X148))
REDUCED_IN_GGA(.(121, T76), 121, X148) → REDUCED_IN_GGA(T76, 121, X148)
REDUCED_IN_GGA(.(T93, T94), T93, X189) → U20_GGA(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
REDUCED_IN_GGA(.(T93, T94), T93, X189) → REDUCED_IN_GGA(T94, T93, X189)
REDUCED_IN_GGA(.(T102, T103), T104, .(T102, X209)) → U21_GGA(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
REDUCED_IN_GGA(.(T102, T103), T104, .(T102, X209)) → REDUCEE_IN_GGA(T103, T102, X209)
REDUCEE_IN_GGA(.(97, T119), 97, X244) → U22_GGA(T119, X244, reduceE_in_gga(T119, 97, X244))
REDUCEE_IN_GGA(.(97, T119), 97, X244) → REDUCEE_IN_GGA(T119, 97, X244)
REDUCEE_IN_GGA(.(101, T119), 101, X244) → U23_GGA(T119, X244, reduceE_in_gga(T119, 101, X244))
REDUCEE_IN_GGA(.(101, T119), 101, X244) → REDUCEE_IN_GGA(T119, 101, X244)
REDUCEE_IN_GGA(.(105, T119), 105, X244) → U24_GGA(T119, X244, reduceE_in_gga(T119, 105, X244))
REDUCEE_IN_GGA(.(105, T119), 105, X244) → REDUCEE_IN_GGA(T119, 105, X244)
REDUCEE_IN_GGA(.(111, T119), 111, X244) → U25_GGA(T119, X244, reduceE_in_gga(T119, 111, X244))
REDUCEE_IN_GGA(.(111, T119), 111, X244) → REDUCEE_IN_GGA(T119, 111, X244)
REDUCEE_IN_GGA(.(117, T119), 117, X244) → U26_GGA(T119, X244, reduceE_in_gga(T119, 117, X244))
REDUCEE_IN_GGA(.(117, T119), 117, X244) → REDUCEE_IN_GGA(T119, 117, X244)
REDUCEE_IN_GGA(.(104, T119), 104, X244) → U27_GGA(T119, X244, reduceE_in_gga(T119, 104, X244))
REDUCEE_IN_GGA(.(104, T119), 104, X244) → REDUCEE_IN_GGA(T119, 104, X244)
REDUCEE_IN_GGA(.(119, T119), 119, X244) → U28_GGA(T119, X244, reduceE_in_gga(T119, 119, X244))
REDUCEE_IN_GGA(.(119, T119), 119, X244) → REDUCEE_IN_GGA(T119, 119, X244)
REDUCEE_IN_GGA(.(121, T119), 121, X244) → U29_GGA(T119, X244, reduceE_in_gga(T119, 121, X244))
REDUCEE_IN_GGA(.(121, T119), 121, X244) → REDUCEE_IN_GGA(T119, 121, X244)
REDUCEE_IN_GGA(.(T136, T137), T136, X285) → U30_GGA(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
REDUCEE_IN_GGA(.(T136, T137), T136, X285) → REDUCEE_IN_GGA(T137, T136, X285)
U31_GGAA(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_GGAA(T16, T15, T18, T7, eqF_in_ag(T7, T18))
U31_GGAA(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → EQF_IN_AG(T7, T18)

The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)
GOALA_IN_GA(x1, x2)  =  GOALA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U31_GGAA(x1, x2, x3, x4, x5)  =  U31_GGAA(x1, x2, x5)
REDUCEC_IN_GGA(x1, x2, x3)  =  REDUCEC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3)  =  U2_GGA(x1, x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
U4_GGA(x1, x2, x3)  =  U4_GGA(x1, x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4, x5)  =  U11_GGA(x1, x2, x3, x5)
REDUCED_IN_GGA(x1, x2, x3)  =  REDUCED_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4, x5)  =  U21_GGA(x1, x2, x3, x5)
REDUCEE_IN_GGA(x1, x2, x3)  =  REDUCEE_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3)  =  U22_GGA(x1, x3)
U23_GGA(x1, x2, x3)  =  U23_GGA(x1, x3)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
U25_GGA(x1, x2, x3)  =  U25_GGA(x1, x3)
U26_GGA(x1, x2, x3)  =  U26_GGA(x1, x3)
U27_GGA(x1, x2, x3)  =  U27_GGA(x1, x3)
U28_GGA(x1, x2, x3)  =  U28_GGA(x1, x3)
U29_GGA(x1, x2, x3)  =  U29_GGA(x1, x3)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U32_GGAA(x1, x2, x3, x4, x5)  =  U32_GGAA(x1, x2, x3, x5)
EQF_IN_AG(x1, x2)  =  EQF_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 37 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCEE_IN_GGA(.(T136, T137), T136, X285) → REDUCEE_IN_GGA(T137, T136, X285)
REDUCEE_IN_GGA(.(97, T119), 97, X244) → REDUCEE_IN_GGA(T119, 97, X244)
REDUCEE_IN_GGA(.(101, T119), 101, X244) → REDUCEE_IN_GGA(T119, 101, X244)
REDUCEE_IN_GGA(.(105, T119), 105, X244) → REDUCEE_IN_GGA(T119, 105, X244)
REDUCEE_IN_GGA(.(111, T119), 111, X244) → REDUCEE_IN_GGA(T119, 111, X244)
REDUCEE_IN_GGA(.(117, T119), 117, X244) → REDUCEE_IN_GGA(T119, 117, X244)
REDUCEE_IN_GGA(.(104, T119), 104, X244) → REDUCEE_IN_GGA(T119, 104, X244)
REDUCEE_IN_GGA(.(119, T119), 119, X244) → REDUCEE_IN_GGA(T119, 119, X244)
REDUCEE_IN_GGA(.(121, T119), 121, X244) → REDUCEE_IN_GGA(T119, 121, X244)

The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)
REDUCEE_IN_GGA(x1, x2, x3)  =  REDUCEE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCEE_IN_GGA(.(T136, T137), T136, X285) → REDUCEE_IN_GGA(T137, T136, X285)
REDUCEE_IN_GGA(.(97, T119), 97, X244) → REDUCEE_IN_GGA(T119, 97, X244)
REDUCEE_IN_GGA(.(101, T119), 101, X244) → REDUCEE_IN_GGA(T119, 101, X244)
REDUCEE_IN_GGA(.(105, T119), 105, X244) → REDUCEE_IN_GGA(T119, 105, X244)
REDUCEE_IN_GGA(.(111, T119), 111, X244) → REDUCEE_IN_GGA(T119, 111, X244)
REDUCEE_IN_GGA(.(117, T119), 117, X244) → REDUCEE_IN_GGA(T119, 117, X244)
REDUCEE_IN_GGA(.(104, T119), 104, X244) → REDUCEE_IN_GGA(T119, 104, X244)
REDUCEE_IN_GGA(.(119, T119), 119, X244) → REDUCEE_IN_GGA(T119, 119, X244)
REDUCEE_IN_GGA(.(121, T119), 121, X244) → REDUCEE_IN_GGA(T119, 121, X244)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCEE_IN_GGA(x1, x2, x3)  =  REDUCEE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REDUCEE_IN_GGA(.(T136, T137), T136) → REDUCEE_IN_GGA(T137, T136)
REDUCEE_IN_GGA(.(97, T119), 97) → REDUCEE_IN_GGA(T119, 97)
REDUCEE_IN_GGA(.(101, T119), 101) → REDUCEE_IN_GGA(T119, 101)
REDUCEE_IN_GGA(.(105, T119), 105) → REDUCEE_IN_GGA(T119, 105)
REDUCEE_IN_GGA(.(111, T119), 111) → REDUCEE_IN_GGA(T119, 111)
REDUCEE_IN_GGA(.(117, T119), 117) → REDUCEE_IN_GGA(T119, 117)
REDUCEE_IN_GGA(.(104, T119), 104) → REDUCEE_IN_GGA(T119, 104)
REDUCEE_IN_GGA(.(119, T119), 119) → REDUCEE_IN_GGA(T119, 119)
REDUCEE_IN_GGA(.(121, T119), 121) → REDUCEE_IN_GGA(T119, 121)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• REDUCEE_IN_GGA(.(T136, T137), T136) → REDUCEE_IN_GGA(T137, T136)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(97, T119), 97) → REDUCEE_IN_GGA(T119, 97)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(101, T119), 101) → REDUCEE_IN_GGA(T119, 101)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(105, T119), 105) → REDUCEE_IN_GGA(T119, 105)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(111, T119), 111) → REDUCEE_IN_GGA(T119, 111)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(117, T119), 117) → REDUCEE_IN_GGA(T119, 117)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(104, T119), 104) → REDUCEE_IN_GGA(T119, 104)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(119, T119), 119) → REDUCEE_IN_GGA(T119, 119)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEE_IN_GGA(.(121, T119), 121) → REDUCEE_IN_GGA(T119, 121)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCED_IN_GGA(.(T93, T94), T93, X189) → REDUCED_IN_GGA(T94, T93, X189)
REDUCED_IN_GGA(.(97, T76), 97, X148) → REDUCED_IN_GGA(T76, 97, X148)
REDUCED_IN_GGA(.(101, T76), 101, X148) → REDUCED_IN_GGA(T76, 101, X148)
REDUCED_IN_GGA(.(105, T76), 105, X148) → REDUCED_IN_GGA(T76, 105, X148)
REDUCED_IN_GGA(.(111, T76), 111, X148) → REDUCED_IN_GGA(T76, 111, X148)
REDUCED_IN_GGA(.(117, T76), 117, X148) → REDUCED_IN_GGA(T76, 117, X148)
REDUCED_IN_GGA(.(104, T76), 104, X148) → REDUCED_IN_GGA(T76, 104, X148)
REDUCED_IN_GGA(.(119, T76), 119, X148) → REDUCED_IN_GGA(T76, 119, X148)
REDUCED_IN_GGA(.(121, T76), 121, X148) → REDUCED_IN_GGA(T76, 121, X148)

The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)
REDUCED_IN_GGA(x1, x2, x3)  =  REDUCED_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCED_IN_GGA(.(T93, T94), T93, X189) → REDUCED_IN_GGA(T94, T93, X189)
REDUCED_IN_GGA(.(97, T76), 97, X148) → REDUCED_IN_GGA(T76, 97, X148)
REDUCED_IN_GGA(.(101, T76), 101, X148) → REDUCED_IN_GGA(T76, 101, X148)
REDUCED_IN_GGA(.(105, T76), 105, X148) → REDUCED_IN_GGA(T76, 105, X148)
REDUCED_IN_GGA(.(111, T76), 111, X148) → REDUCED_IN_GGA(T76, 111, X148)
REDUCED_IN_GGA(.(117, T76), 117, X148) → REDUCED_IN_GGA(T76, 117, X148)
REDUCED_IN_GGA(.(104, T76), 104, X148) → REDUCED_IN_GGA(T76, 104, X148)
REDUCED_IN_GGA(.(119, T76), 119, X148) → REDUCED_IN_GGA(T76, 119, X148)
REDUCED_IN_GGA(.(121, T76), 121, X148) → REDUCED_IN_GGA(T76, 121, X148)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCED_IN_GGA(x1, x2, x3)  =  REDUCED_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REDUCED_IN_GGA(.(T93, T94), T93) → REDUCED_IN_GGA(T94, T93)
REDUCED_IN_GGA(.(97, T76), 97) → REDUCED_IN_GGA(T76, 97)
REDUCED_IN_GGA(.(101, T76), 101) → REDUCED_IN_GGA(T76, 101)
REDUCED_IN_GGA(.(105, T76), 105) → REDUCED_IN_GGA(T76, 105)
REDUCED_IN_GGA(.(111, T76), 111) → REDUCED_IN_GGA(T76, 111)
REDUCED_IN_GGA(.(117, T76), 117) → REDUCED_IN_GGA(T76, 117)
REDUCED_IN_GGA(.(104, T76), 104) → REDUCED_IN_GGA(T76, 104)
REDUCED_IN_GGA(.(119, T76), 119) → REDUCED_IN_GGA(T76, 119)
REDUCED_IN_GGA(.(121, T76), 121) → REDUCED_IN_GGA(T76, 121)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• REDUCED_IN_GGA(.(T93, T94), T93) → REDUCED_IN_GGA(T94, T93)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(97, T76), 97) → REDUCED_IN_GGA(T76, 97)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(101, T76), 101) → REDUCED_IN_GGA(T76, 101)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(105, T76), 105) → REDUCED_IN_GGA(T76, 105)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(111, T76), 111) → REDUCED_IN_GGA(T76, 111)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(117, T76), 117) → REDUCED_IN_GGA(T76, 117)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(104, T76), 104) → REDUCED_IN_GGA(T76, 104)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(119, T76), 119) → REDUCED_IN_GGA(T76, 119)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCED_IN_GGA(.(121, T76), 121) → REDUCED_IN_GGA(T76, 121)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCEC_IN_GGA(.(T50, T51), T50, X93) → REDUCEC_IN_GGA(T51, T50, X93)
REDUCEC_IN_GGA(.(97, T33), 97, X52) → REDUCEC_IN_GGA(T33, 97, X52)
REDUCEC_IN_GGA(.(101, T33), 101, X52) → REDUCEC_IN_GGA(T33, 101, X52)
REDUCEC_IN_GGA(.(105, T33), 105, X52) → REDUCEC_IN_GGA(T33, 105, X52)
REDUCEC_IN_GGA(.(111, T33), 111, X52) → REDUCEC_IN_GGA(T33, 111, X52)
REDUCEC_IN_GGA(.(117, T33), 117, X52) → REDUCEC_IN_GGA(T33, 117, X52)
REDUCEC_IN_GGA(.(104, T33), 104, X52) → REDUCEC_IN_GGA(T33, 104, X52)
REDUCEC_IN_GGA(.(119, T33), 119, X52) → REDUCEC_IN_GGA(T33, 119, X52)
REDUCEC_IN_GGA(.(121, T33), 121, X52) → REDUCEC_IN_GGA(T33, 121, X52)

The TRS R consists of the following rules:

goalA_in_ga(.(T15, T16), T7) → U1_ga(T15, T16, T7, pB_in_ggaa(T16, T15, X12, T7))
pB_in_ggaa(T16, T15, T18, T7) → U31_ggaa(T16, T15, T18, T7, reduceC_in_gga(T16, T15, T18))
reduceC_in_gga([], T23, []) → reduceC_out_gga([], T23, [])
reduceC_in_gga(.(97, T33), 97, X52) → U2_gga(T33, X52, reduceC_in_gga(T33, 97, X52))
reduceC_in_gga(.(101, T33), 101, X52) → U3_gga(T33, X52, reduceC_in_gga(T33, 101, X52))
reduceC_in_gga(.(105, T33), 105, X52) → U4_gga(T33, X52, reduceC_in_gga(T33, 105, X52))
reduceC_in_gga(.(111, T33), 111, X52) → U5_gga(T33, X52, reduceC_in_gga(T33, 111, X52))
reduceC_in_gga(.(117, T33), 117, X52) → U6_gga(T33, X52, reduceC_in_gga(T33, 117, X52))
reduceC_in_gga(.(104, T33), 104, X52) → U7_gga(T33, X52, reduceC_in_gga(T33, 104, X52))
reduceC_in_gga(.(119, T33), 119, X52) → U8_gga(T33, X52, reduceC_in_gga(T33, 119, X52))
reduceC_in_gga(.(121, T33), 121, X52) → U9_gga(T33, X52, reduceC_in_gga(T33, 121, X52))
reduceC_in_gga(.(T50, T51), T50, X93) → U10_gga(T50, T51, X93, reduceC_in_gga(T51, T50, X93))
reduceC_in_gga(.(T59, T60), T61, .(T59, X113)) → U11_gga(T59, T60, T61, X113, reduceD_in_gga(T60, T59, X113))
reduceD_in_gga([], T66, []) → reduceD_out_gga([], T66, [])
reduceD_in_gga(.(97, T76), 97, X148) → U12_gga(T76, X148, reduceD_in_gga(T76, 97, X148))
reduceD_in_gga(.(101, T76), 101, X148) → U13_gga(T76, X148, reduceD_in_gga(T76, 101, X148))
reduceD_in_gga(.(105, T76), 105, X148) → U14_gga(T76, X148, reduceD_in_gga(T76, 105, X148))
reduceD_in_gga(.(111, T76), 111, X148) → U15_gga(T76, X148, reduceD_in_gga(T76, 111, X148))
reduceD_in_gga(.(117, T76), 117, X148) → U16_gga(T76, X148, reduceD_in_gga(T76, 117, X148))
reduceD_in_gga(.(104, T76), 104, X148) → U17_gga(T76, X148, reduceD_in_gga(T76, 104, X148))
reduceD_in_gga(.(119, T76), 119, X148) → U18_gga(T76, X148, reduceD_in_gga(T76, 119, X148))
reduceD_in_gga(.(121, T76), 121, X148) → U19_gga(T76, X148, reduceD_in_gga(T76, 121, X148))
reduceD_in_gga(.(T93, T94), T93, X189) → U20_gga(T93, T94, X189, reduceD_in_gga(T94, T93, X189))
reduceD_in_gga(.(T102, T103), T104, .(T102, X209)) → U21_gga(T102, T103, T104, X209, reduceE_in_gga(T103, T102, X209))
reduceE_in_gga([], T109, []) → reduceE_out_gga([], T109, [])
reduceE_in_gga(.(97, T119), 97, X244) → U22_gga(T119, X244, reduceE_in_gga(T119, 97, X244))
reduceE_in_gga(.(101, T119), 101, X244) → U23_gga(T119, X244, reduceE_in_gga(T119, 101, X244))
reduceE_in_gga(.(105, T119), 105, X244) → U24_gga(T119, X244, reduceE_in_gga(T119, 105, X244))
reduceE_in_gga(.(111, T119), 111, X244) → U25_gga(T119, X244, reduceE_in_gga(T119, 111, X244))
reduceE_in_gga(.(117, T119), 117, X244) → U26_gga(T119, X244, reduceE_in_gga(T119, 117, X244))
reduceE_in_gga(.(104, T119), 104, X244) → U27_gga(T119, X244, reduceE_in_gga(T119, 104, X244))
reduceE_in_gga(.(119, T119), 119, X244) → U28_gga(T119, X244, reduceE_in_gga(T119, 119, X244))
reduceE_in_gga(.(121, T119), 121, X244) → U29_gga(T119, X244, reduceE_in_gga(T119, 121, X244))
reduceE_in_gga(.(T136, T137), T136, X285) → U30_gga(T136, T137, X285, reduceE_in_gga(T137, T136, X285))
reduceE_in_gga(.(T155, T154), T147, .(T155, [])) → reduceE_out_gga(.(T155, T154), T147, .(T155, []))
U30_gga(T136, T137, X285, reduceE_out_gga(T137, T136, X285)) → reduceE_out_gga(.(T136, T137), T136, X285)
U29_gga(T119, X244, reduceE_out_gga(T119, 121, X244)) → reduceE_out_gga(.(121, T119), 121, X244)
U28_gga(T119, X244, reduceE_out_gga(T119, 119, X244)) → reduceE_out_gga(.(119, T119), 119, X244)
U27_gga(T119, X244, reduceE_out_gga(T119, 104, X244)) → reduceE_out_gga(.(104, T119), 104, X244)
U26_gga(T119, X244, reduceE_out_gga(T119, 117, X244)) → reduceE_out_gga(.(117, T119), 117, X244)
U25_gga(T119, X244, reduceE_out_gga(T119, 111, X244)) → reduceE_out_gga(.(111, T119), 111, X244)
U24_gga(T119, X244, reduceE_out_gga(T119, 105, X244)) → reduceE_out_gga(.(105, T119), 105, X244)
U23_gga(T119, X244, reduceE_out_gga(T119, 101, X244)) → reduceE_out_gga(.(101, T119), 101, X244)
U22_gga(T119, X244, reduceE_out_gga(T119, 97, X244)) → reduceE_out_gga(.(97, T119), 97, X244)
U21_gga(T102, T103, T104, X209, reduceE_out_gga(T103, T102, X209)) → reduceD_out_gga(.(T102, T103), T104, .(T102, X209))
U20_gga(T93, T94, X189, reduceD_out_gga(T94, T93, X189)) → reduceD_out_gga(.(T93, T94), T93, X189)
U19_gga(T76, X148, reduceD_out_gga(T76, 121, X148)) → reduceD_out_gga(.(121, T76), 121, X148)
U18_gga(T76, X148, reduceD_out_gga(T76, 119, X148)) → reduceD_out_gga(.(119, T76), 119, X148)
U17_gga(T76, X148, reduceD_out_gga(T76, 104, X148)) → reduceD_out_gga(.(104, T76), 104, X148)
U16_gga(T76, X148, reduceD_out_gga(T76, 117, X148)) → reduceD_out_gga(.(117, T76), 117, X148)
U15_gga(T76, X148, reduceD_out_gga(T76, 111, X148)) → reduceD_out_gga(.(111, T76), 111, X148)
U14_gga(T76, X148, reduceD_out_gga(T76, 105, X148)) → reduceD_out_gga(.(105, T76), 105, X148)
U13_gga(T76, X148, reduceD_out_gga(T76, 101, X148)) → reduceD_out_gga(.(101, T76), 101, X148)
U12_gga(T76, X148, reduceD_out_gga(T76, 97, X148)) → reduceD_out_gga(.(97, T76), 97, X148)
U11_gga(T59, T60, T61, X113, reduceD_out_gga(T60, T59, X113)) → reduceC_out_gga(.(T59, T60), T61, .(T59, X113))
U10_gga(T50, T51, X93, reduceC_out_gga(T51, T50, X93)) → reduceC_out_gga(.(T50, T51), T50, X93)
U9_gga(T33, X52, reduceC_out_gga(T33, 121, X52)) → reduceC_out_gga(.(121, T33), 121, X52)
U8_gga(T33, X52, reduceC_out_gga(T33, 119, X52)) → reduceC_out_gga(.(119, T33), 119, X52)
U7_gga(T33, X52, reduceC_out_gga(T33, 104, X52)) → reduceC_out_gga(.(104, T33), 104, X52)
U6_gga(T33, X52, reduceC_out_gga(T33, 117, X52)) → reduceC_out_gga(.(117, T33), 117, X52)
U5_gga(T33, X52, reduceC_out_gga(T33, 111, X52)) → reduceC_out_gga(.(111, T33), 111, X52)
U4_gga(T33, X52, reduceC_out_gga(T33, 105, X52)) → reduceC_out_gga(.(105, T33), 105, X52)
U3_gga(T33, X52, reduceC_out_gga(T33, 101, X52)) → reduceC_out_gga(.(101, T33), 101, X52)
U2_gga(T33, X52, reduceC_out_gga(T33, 97, X52)) → reduceC_out_gga(.(97, T33), 97, X52)
U31_ggaa(T16, T15, T18, T7, reduceC_out_gga(T16, T15, T18)) → U32_ggaa(T16, T15, T18, T7, eqF_in_ag(T7, T18))
eqF_in_ag(T158, T158) → eqF_out_ag(T158, T158)
U32_ggaa(T16, T15, T18, T7, eqF_out_ag(T7, T18)) → pB_out_ggaa(T16, T15, T18, T7)
U1_ga(T15, T16, T7, pB_out_ggaa(T16, T15, X12, T7)) → goalA_out_ga(.(T15, T16), T7)

The argument filtering Pi contains the following mapping:
goalA_in_ga(x1, x2)  =  goalA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
reduceC_in_gga(x1, x2, x3)  =  reduceC_in_gga(x1, x2)
[]  =  []
reduceC_out_gga(x1, x2, x3)  =  reduceC_out_gga(x1, x2, x3)
97  =  97
U2_gga(x1, x2, x3)  =  U2_gga(x1, x3)
101  =  101
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
105  =  105
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
111  =  111
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
117  =  117
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
104  =  104
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
119  =  119
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
121  =  121
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4, x5)  =  U11_gga(x1, x2, x3, x5)
reduceD_in_gga(x1, x2, x3)  =  reduceD_in_gga(x1, x2)
reduceD_out_gga(x1, x2, x3)  =  reduceD_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
reduceE_in_gga(x1, x2, x3)  =  reduceE_in_gga(x1, x2)
reduceE_out_gga(x1, x2, x3)  =  reduceE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3)  =  U22_gga(x1, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x3)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3)  =  U26_gga(x1, x3)
U27_gga(x1, x2, x3)  =  U27_gga(x1, x3)
U28_gga(x1, x2, x3)  =  U28_gga(x1, x3)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x3)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x1, x2, x4)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x3, x5)
eqF_in_ag(x1, x2)  =  eqF_in_ag(x2)
eqF_out_ag(x1, x2)  =  eqF_out_ag(x1, x2)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
goalA_out_ga(x1, x2)  =  goalA_out_ga(x1, x2)
REDUCEC_IN_GGA(x1, x2, x3)  =  REDUCEC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REDUCEC_IN_GGA(.(T50, T51), T50, X93) → REDUCEC_IN_GGA(T51, T50, X93)
REDUCEC_IN_GGA(.(97, T33), 97, X52) → REDUCEC_IN_GGA(T33, 97, X52)
REDUCEC_IN_GGA(.(101, T33), 101, X52) → REDUCEC_IN_GGA(T33, 101, X52)
REDUCEC_IN_GGA(.(105, T33), 105, X52) → REDUCEC_IN_GGA(T33, 105, X52)
REDUCEC_IN_GGA(.(111, T33), 111, X52) → REDUCEC_IN_GGA(T33, 111, X52)
REDUCEC_IN_GGA(.(117, T33), 117, X52) → REDUCEC_IN_GGA(T33, 117, X52)
REDUCEC_IN_GGA(.(104, T33), 104, X52) → REDUCEC_IN_GGA(T33, 104, X52)
REDUCEC_IN_GGA(.(119, T33), 119, X52) → REDUCEC_IN_GGA(T33, 119, X52)
REDUCEC_IN_GGA(.(121, T33), 121, X52) → REDUCEC_IN_GGA(T33, 121, X52)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCEC_IN_GGA(x1, x2, x3)  =  REDUCEC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REDUCEC_IN_GGA(.(T50, T51), T50) → REDUCEC_IN_GGA(T51, T50)
REDUCEC_IN_GGA(.(97, T33), 97) → REDUCEC_IN_GGA(T33, 97)
REDUCEC_IN_GGA(.(101, T33), 101) → REDUCEC_IN_GGA(T33, 101)
REDUCEC_IN_GGA(.(105, T33), 105) → REDUCEC_IN_GGA(T33, 105)
REDUCEC_IN_GGA(.(111, T33), 111) → REDUCEC_IN_GGA(T33, 111)
REDUCEC_IN_GGA(.(117, T33), 117) → REDUCEC_IN_GGA(T33, 117)
REDUCEC_IN_GGA(.(104, T33), 104) → REDUCEC_IN_GGA(T33, 104)
REDUCEC_IN_GGA(.(119, T33), 119) → REDUCEC_IN_GGA(T33, 119)
REDUCEC_IN_GGA(.(121, T33), 121) → REDUCEC_IN_GGA(T33, 121)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• REDUCEC_IN_GGA(.(T50, T51), T50) → REDUCEC_IN_GGA(T51, T50)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(97, T33), 97) → REDUCEC_IN_GGA(T33, 97)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(101, T33), 101) → REDUCEC_IN_GGA(T33, 101)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(105, T33), 105) → REDUCEC_IN_GGA(T33, 105)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(111, T33), 111) → REDUCEC_IN_GGA(T33, 111)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(117, T33), 117) → REDUCEC_IN_GGA(T33, 117)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(104, T33), 104) → REDUCEC_IN_GGA(T33, 104)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(119, T33), 119) → REDUCEC_IN_GGA(T33, 119)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

• REDUCEC_IN_GGA(.(121, T33), 121) → REDUCEC_IN_GGA(T33, 121)
  The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(27) YES