Left Termination proof of /tmp/tmpF1SAC0/der-bf.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 QDPOrderProof (⇔)

        ↳13 QDP

        ↳14 DependencyGraphProof (⇔)

        ↳15 TRUE

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇐)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔)

        ↳22 YES

(0) Obligation:

Clauses:

p(d(e(t)), const(1)).
p(d(e(const(A))), const(0)).
p(d(e(+(X, Y))), +(DX, DY)) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY)).
p(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY)).
p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX)).

Queries:

p(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: p(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: p(T1, T2), SCOPE: 1, CLAUSE: 0 | p(T1, T2), SCOPE: 1, CLAUSE: 1 | p(T1, T2), SCOPE: 1, CLAUSE: 2 | p(T1, T2), SCOPE: 1, CLAUSE: 3 | p(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 1 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: p(T1, T2), SCOPE: 1, CLAUSE: 1 | p(T1, T2), SCOPE: 1, CLAUSE: 2 | p(T1, T2), SCOPE: 1, CLAUSE: 3 | p(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\np(T1, T2) !=? p(d(e(t)), const(1))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: p(d(e(t)), T2), SCOPE: 1, CLAUSE: 1 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: p(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: p(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: p(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 2 | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: p(T1, T2), SCOPE: 1, CLAUSE: 2 | p(T1, T2), SCOPE: 1, CLAUSE: 3 | p(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\np(T1, T2) !=? p(d(e(t)), const(1))\np(T1, T2) !=? p(d(e(const(X13))), const(0))", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 2 | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: p(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)) | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: p(T1, T2), SCOPE: 1, CLAUSE: 3 | p(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\np(T1, T2) !=? p(d(e(t)), const(1))\np(T1, T2) !=? p(d(e(const(X13))), const(0))\np(T1, T2) !=? p(d(e(+(X29, X30))), +(X31, X32))", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 0 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 0\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: p(d(e(T10)), T15)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: p(d(e(T10)), T21)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(p(d(e(T38)), T42), ','(p(d(e(T39)), T43), p(d(e(T10)), T44)))\n\nT10 is ground\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: p(d(e(T38)), T42)\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(p(d(e(T39)), T45), p(d(e(T10)), T46))\n\nT10 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: p(d(e(T39)), T45)\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: p(d(e(T10)), T47)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(d(e(T9)), T13), p(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(p(d(e(T64)), T68), ','(p(d(e(T65)), T69), p(d(e(T10)), T70)))\n\nT10 is ground\nT64 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_2 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: p(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)) | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: p(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\np(T1, T2) !=? p(d(e(t)), const(1))\np(T1, T2) !=? p(d(e(const(X13))), const(0))\np(T1, T2) !=? p(d(e(+(X29, X30))), +(X31, X32))\np(T1, T2) !=? p(d(e(*(X103, X104))), +(*(X103, X105), *(X104, X106)))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 0 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 0\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: p(d(e(T76)), T81)\n\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: p(d(e(T76)), T87)\n\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(p(d(e(T104)), T108), ','(p(d(e(T105)), T109), p(d(e(T76)), T110)))\n\nT76 is ground\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(p(d(e(T75)), T79), p(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(d(e(T127)), T131), ','(p(d(e(T128)), T132), p(d(e(T76)), T133)))\n\nT76 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_3 | p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: p(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(p(d(T136), X173), p(d(e(X173)), T138))\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 0 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 1 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 2 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 3 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 0\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 1 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 2 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 3 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: p(d(e(const(1))), T138)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 1\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 2 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 3 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: p(d(e(const(0))), T138)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 2\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 3 | ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(p(d(e(T152)), X214), ','(p(d(e(T153)), X215), p(d(e(+(X214, X215))), T138)))\n\nT152 is ground\nT153 is ground\nX214 is free; \nX215 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: p(d(e(T152)), X214)\n\nT152 is ground\nX214 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(p(d(e(T153)), X215), p(d(e(+(T154, X215))), T138))\n\nT153 is ground\nT154 is ground\nX215 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: p(d(e(T153)), X215)\n\nT153 is ground\nX215 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: p(d(e(+(T154, T155))), T138)\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 3\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(d(T136), X173), p(d(e(X173)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(p(d(e(T168)), X255), ','(p(d(e(T169)), X254), p(d(e(+(*(T168, X254), *(T169, X255)))), T138)))\n\nT168 is ground\nT169 is ground\nX254 is free; \nX255 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: p(d(e(T168)), X255)\n\nT168 is ground\nX255 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(p(d(e(T169)), X254), p(d(e(+(*(T168, X254), *(T169, T170)))), T138))\n\nT168 is ground\nT169 is ground\nT170 is ground\nX254 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: p(d(e(T169)), X254)\n\nT169 is ground\nX254 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: p(d(e(+(*(T168, T171), *(T169, T170)))), T138)\n\nT168 is ground\nT169 is ground\nT170 is ground\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(p(d(T180), X275), ','(p(d(e(X275)), X276), p(d(e(X276)), T138)))\n\nT180 is ground\nX276 is free; \nX275 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: p(d(T180), X275)\n\nT180 is ground\nX275 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(d(e(T181)), X276), p(d(e(X276)), T138))\n\nT181 is ground\nX276 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 96 [arrowhead = none ];
96 -> 2;

97 [label="EVAL with clause\np(d(e(t)), const(1)).\nand substitution\nT1 -> d(e(t))\nT2 -> const(1)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 97 [arrowhead = none ];
97 -> 3;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 98 [arrowhead = none ];
98 -> 4;

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

100 [label="EVAL with clause\np(d(e(const(X13))), const(0)).\nand substitution\nX13 -> T4\nT1 -> d(e(const(T4)))\nT2 -> const(0)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 100 [arrowhead = none ];
100 -> 10;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 101 [arrowhead = none ];
101 -> 11;

102 [label="BACKTRACK\nfor clause: p(d(e(const(A))), const(0))because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 102 [arrowhead = none ];
102 -> 6;

103 [label="BACKTRACK\nfor clause: p(d(e(+(X, Y))), +(DX, DY)) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = white];
6 -> 103 [arrowhead = none ];
103 -> 7;

104 [label="BACKTRACK\nfor clause: p(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = white];
7 -> 104 [arrowhead = none ];
104 -> 8;

105 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
8 -> 105 [arrowhead = none ];
105 -> 9;

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

107 [label="EVAL with clause\np(d(e(+(X29, X30))), +(X31, X32)) :- ','(p(d(e(X29)), X31), p(d(e(X30)), X32)).\nand substitution\nX29 -> T9\nX30 -> T10\nT1 -> d(e(+(T9, T10)))\nX31 -> T13\nX32 -> T14\nT2 -> +(T13, T14)\nT11 -> T13\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 107 [arrowhead = none ];
107 -> 16;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 108 [arrowhead = none ];
108 -> 17;

109 [label="BACKTRACK\nfor clause: p(d(e(+(X, Y))), +(DX, DY)) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = white];
12 -> 109 [arrowhead = none ];
109 -> 13;

110 [label="BACKTRACK\nfor clause: p(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = white];
13 -> 110 [arrowhead = none ];
110 -> 14;

111 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
14 -> 111 [arrowhead = none ];
111 -> 15;

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

113 [label="EVAL with clause\np(d(e(*(X103, X104))), +(*(X103, X105), *(X104, X106))) :- ','(p(d(e(X103)), X106), p(d(e(X104)), X105)).\nand substitution\nX103 -> T75\nX104 -> T76\nT1 -> d(e(*(T75, T76)))\nX105 -> T80\nX106 -> T79\nT2 -> +(*(T75, T80), *(T76, T79))\nT78 -> T79\nT77 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 113 [arrowhead = none ];
113 -> 43;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 114 [arrowhead = none ];
114 -> 44;

115 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 115 [arrowhead = none ];
115 -> 19;

116 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 116 [arrowhead = none ];
116 -> 20;

117 [label="EVAL with clause\np(d(e(t)), const(1)).\nand substitution\nT9 -> t\nT13 -> const(1)\nT14 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 117 [arrowhead = none ];
117 -> 21;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 118 [arrowhead = none ];
118 -> 22;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 119 [arrowhead = none ];
119 -> 23;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 120 [arrowhead = none ];
120 -> 24;

121 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T15", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 121 [arrowhead = none , style=dashed];
121 -> 1[style=dashed];

122 [label="EVAL with clause\np(d(e(const(X41))), const(0)).\nand substitution\nX41 -> T20\nT9 -> const(T20)\nT13 -> const(0)\nT14 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 122 [arrowhead = none ];
122 -> 25;

123 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 123 [arrowhead = none ];
123 -> 26;

124 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 124 [arrowhead = none ];
124 -> 27;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 125 [arrowhead = none ];
125 -> 28;

126 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 126 [arrowhead = none , style=dashed];
126 -> 1[style=dashed];

127 [label="EVAL with clause\np(d(e(+(X59, X60))), +(X61, X62)) :- ','(p(d(e(X59)), X61), p(d(e(X60)), X62)).\nand substitution\nX59 -> T38\nX60 -> T39\nT9 -> +(T38, T39)\nX61 -> T42\nX62 -> T43\nT13 -> +(T42, T43)\nT40 -> T42\nT41 -> T43\nT14 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 127 [arrowhead = none ];
127 -> 29;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 128 [arrowhead = none ];
128 -> 30;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 129 [arrowhead = none ];
129 -> 35;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 130 [arrowhead = none ];
130 -> 36;

131 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
29 -> 131 [arrowhead = none ];
131 -> 31;

132 [label="SPLIT 2\nnew knowledge:\nT42 is ground\nreplacements:\nT43 -> T45\nT44 -> T46", fontsize=14, style = filled, fillcolor = violet];
29 -> 132 [arrowhead = none ];
132 -> 32;

133 [label="INSTANCE with matching:\nT1 -> d(e(T38))\nT2 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 133 [arrowhead = none , style=dashed];
133 -> 1[style=dashed];

134 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 134 [arrowhead = none ];
134 -> 33;

135 [label="SPLIT 2\nnew knowledge:\nT45 is ground\nreplacements:\nT46 -> T47", fontsize=14, style = filled, fillcolor = violet];
32 -> 135 [arrowhead = none ];
135 -> 34;

136 [label="INSTANCE with matching:\nT1 -> d(e(T39))\nT2 -> T45", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 136 [arrowhead = none , style=dashed];
136 -> 1[style=dashed];

137 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T47", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 137 [arrowhead = none , style=dashed];
137 -> 1[style=dashed];

138 [label="EVAL with clause\np(d(e(*(X83, X84))), +(*(X83, X85), *(X84, X86))) :- ','(p(d(e(X83)), X86), p(d(e(X84)), X85)).\nand substitution\nX83 -> T64\nX84 -> T65\nT9 -> *(T64, T65)\nX85 -> T69\nX86 -> T68\nT13 -> +(*(T64, T69), *(T65, T68))\nT67 -> T68\nT66 -> T69\nT14 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 138 [arrowhead = none ];
138 -> 37;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 139 [arrowhead = none ];
139 -> 38;

140 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
36 -> 140 [arrowhead = none ];
140 -> 39;

141 [label="INSTANCE with matching:\nT38 -> T64\nT42 -> T68\nT39 -> T65\nT43 -> T69\nT44 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 141 [arrowhead = none , style=dashed];
141 -> 29[style=dashed];

142 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 142 [arrowhead = none ];
142 -> 40;

143 [label="BACKTRACK\nfor clause: p(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(p(d(e(X)), DX), p(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = white];
40 -> 143 [arrowhead = none ];
143 -> 41;

144 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
41 -> 144 [arrowhead = none ];
144 -> 42;

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

146 [label="EVAL with clause\np(d(d(X171)), X172) :- ','(p(d(X171), X173), p(d(e(X173)), X172)).\nand substitution\nX171 -> T136\nT1 -> d(d(T136))\nT2 -> T138\nX172 -> T138\nT137 -> T138", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 146 [arrowhead = none ];
146 -> 65;

147 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 147 [arrowhead = none ];
147 -> 66;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 148 [arrowhead = none ];
148 -> 46;

149 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 149 [arrowhead = none ];
149 -> 47;

150 [label="EVAL with clause\np(d(e(t)), const(1)).\nand substitution\nT75 -> t\nT79 -> const(1)\nT80 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 150 [arrowhead = none ];
150 -> 48;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 151 [arrowhead = none ];
151 -> 49;

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 152 [arrowhead = none ];
152 -> 50;

153 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 153 [arrowhead = none ];
153 -> 51;

154 [label="INSTANCE with matching:\nT1 -> d(e(T76))\nT2 -> T81", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 154 [arrowhead = none , style=dashed];
154 -> 1[style=dashed];

155 [label="EVAL with clause\np(d(e(const(X115))), const(0)).\nand substitution\nX115 -> T86\nT75 -> const(T86)\nT79 -> const(0)\nT80 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 155 [arrowhead = none ];
155 -> 52;

156 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 156 [arrowhead = none ];
156 -> 53;

157 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 157 [arrowhead = none ];
157 -> 54;

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 158 [arrowhead = none ];
158 -> 55;

159 [label="INSTANCE with matching:\nT1 -> d(e(T76))\nT2 -> T87", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 159 [arrowhead = none , style=dashed];
159 -> 1[style=dashed];

160 [label="EVAL with clause\np(d(e(+(X133, X134))), +(X135, X136)) :- ','(p(d(e(X133)), X135), p(d(e(X134)), X136)).\nand substitution\nX133 -> T104\nX134 -> T105\nT75 -> +(T104, T105)\nX135 -> T108\nX136 -> T109\nT79 -> +(T108, T109)\nT106 -> T108\nT107 -> T109\nT80 -> T110", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 160 [arrowhead = none ];
160 -> 56;

161 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 161 [arrowhead = none ];
161 -> 57;

162 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 162 [arrowhead = none ];
162 -> 58;

163 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 163 [arrowhead = none ];
163 -> 59;

164 [label="INSTANCE with matching:\nT38 -> T104\nT42 -> T108\nT39 -> T105\nT43 -> T109\nT10 -> T76\nT44 -> T110", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 164 [arrowhead = none , style=dashed];
164 -> 29[style=dashed];

165 [label="EVAL with clause\np(d(e(*(X157, X158))), +(*(X157, X159), *(X158, X160))) :- ','(p(d(e(X157)), X160), p(d(e(X158)), X159)).\nand substitution\nX157 -> T127\nX158 -> T128\nT75 -> *(T127, T128)\nX159 -> T132\nX160 -> T131\nT79 -> +(*(T127, T132), *(T128, T131))\nT130 -> T131\nT129 -> T132\nT80 -> T133", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 165 [arrowhead = none ];
165 -> 60;

166 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 166 [arrowhead = none ];
166 -> 61;

167 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
59 -> 167 [arrowhead = none ];
167 -> 62;

168 [label="INSTANCE with matching:\nT38 -> T127\nT42 -> T131\nT39 -> T128\nT43 -> T132\nT10 -> T76\nT44 -> T133", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 168 [arrowhead = none , style=dashed];
168 -> 29[style=dashed];

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

170 [label="BACKTRACK\nfor clause: p(d(d(X)), DDX) :- ','(p(d(X), DX), p(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = white];
63 -> 170 [arrowhead = none ];
170 -> 64;

171 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 171 [arrowhead = none ];
171 -> 67;

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

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

174 [label="EVAL with clause\np(d(e(t)), const(1)).\nand substitution\nT136 -> e(t)\nX173 -> const(1)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 174 [arrowhead = none ];
174 -> 70;

175 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 175 [arrowhead = none ];
175 -> 71;

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

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

178 [label="INSTANCE with matching:\nT1 -> d(e(const(1)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 178 [arrowhead = none , style=dashed];
178 -> 1[style=dashed];

179 [label="EVAL with clause\np(d(e(const(X182))), const(0)).\nand substitution\nX182 -> T143\nT136 -> e(const(T143))\nX173 -> const(0)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 179 [arrowhead = none ];
179 -> 74;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 180 [arrowhead = none ];
180 -> 75;

181 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 181 [arrowhead = none ];
181 -> 76;

182 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 182 [arrowhead = none ];
182 -> 77;

183 [label="INSTANCE with matching:\nT1 -> d(e(const(0)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 183 [arrowhead = none , style=dashed];
183 -> 1[style=dashed];

184 [label="EVAL with clause\np(d(e(+(X210, X211))), +(X212, X213)) :- ','(p(d(e(X210)), X212), p(d(e(X211)), X213)).\nand substitution\nX210 -> T152\nX211 -> T153\nT136 -> e(+(T152, T153))\nX212 -> X214\nX213 -> X215\nX173 -> +(X214, X215)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 184 [arrowhead = none ];
184 -> 78;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 185 [arrowhead = none ];
185 -> 79;

186 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 186 [arrowhead = none ];
186 -> 84;

187 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 187 [arrowhead = none ];
187 -> 85;

188 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
78 -> 188 [arrowhead = none ];
188 -> 80;

189 [label="SPLIT 2\nnew knowledge:\nT154 is ground\nreplacements:\nX214 -> T154", fontsize=14, style = filled, fillcolor = violet];
78 -> 189 [arrowhead = none ];
189 -> 81;

190 [label="INSTANCE with matching:\nT1 -> d(e(T152))\nT2 -> X214", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 190 [arrowhead = none , style=dashed];
190 -> 1[style=dashed];

191 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 191 [arrowhead = none ];
191 -> 82;

192 [label="SPLIT 2\nnew knowledge:\nT155 is ground\nreplacements:\nX215 -> T155", fontsize=14, style = filled, fillcolor = violet];
81 -> 192 [arrowhead = none ];
192 -> 83;

193 [label="INSTANCE with matching:\nT1 -> d(e(T153))\nT2 -> X215", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 193 [arrowhead = none , style=dashed];
193 -> 1[style=dashed];

194 [label="INSTANCE with matching:\nT1 -> d(e(+(T154, T155)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 194 [arrowhead = none , style=dashed];
194 -> 1[style=dashed];

195 [label="EVAL with clause\np(d(e(*(X250, X251))), +(*(X250, X252), *(X251, X253))) :- ','(p(d(e(X250)), X253), p(d(e(X251)), X252)).\nand substitution\nX250 -> T168\nX251 -> T169\nT136 -> e(*(T168, T169))\nX252 -> X254\nX253 -> X255\nX173 -> +(*(T168, X254), *(T169, X255))", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 195 [arrowhead = none ];
195 -> 86;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 196 [arrowhead = none ];
196 -> 87;

197 [label="EVAL with clause\np(d(d(X273)), X274) :- ','(p(d(X273), X275), p(d(e(X275)), X274)).\nand substitution\nX273 -> T180\nT136 -> d(T180)\nX173 -> X276\nX274 -> X276", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 197 [arrowhead = none ];
197 -> 92;

198 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 198 [arrowhead = none ];
198 -> 93;

199 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
86 -> 199 [arrowhead = none ];
199 -> 88;

200 [label="SPLIT 2\nnew knowledge:\nT170 is ground\nreplacements:\nX255 -> T170", fontsize=14, style = filled, fillcolor = violet];
86 -> 200 [arrowhead = none ];
200 -> 89;

201 [label="INSTANCE with matching:\nT1 -> d(e(T168))\nT2 -> X255", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 201 [arrowhead = none , style=dashed];
201 -> 1[style=dashed];

202 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
89 -> 202 [arrowhead = none ];
202 -> 90;

203 [label="SPLIT 2\nnew knowledge:\nT171 is ground\nreplacements:\nX254 -> T171", fontsize=14, style = filled, fillcolor = violet];
89 -> 203 [arrowhead = none ];
203 -> 91;

204 [label="INSTANCE with matching:\nT1 -> d(e(T169))\nT2 -> X254", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 204 [arrowhead = none , style=dashed];
204 -> 1[style=dashed];

205 [label="INSTANCE with matching:\nT1 -> d(e(+(*(T168, T171), *(T169, T170))))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 205 [arrowhead = none , style=dashed];
205 -> 1[style=dashed];

206 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
92 -> 206 [arrowhead = none ];
206 -> 94;

207 [label="SPLIT 2\nnew knowledge:\nT181 is ground\nreplacements:\nX275 -> T181", fontsize=14, style = filled, fillcolor = violet];
92 -> 207 [arrowhead = none ];
207 -> 95;

208 [label="INSTANCE with matching:\nT1 -> d(T180)\nT2 -> X275", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 208 [arrowhead = none , style=dashed];
208 -> 1[style=dashed];

209 [label="INSTANCE with matching:\nT136 -> e(T181)\nX173 -> X276", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 209 [arrowhead = none , style=dashed];
209 -> 65[style=dashed];

}

(2) Obligation:

Triples:

p29(T38, T42, T39, T43, T10, T44) :- p1(d(e(T38)), T42).
p29(T38, T42, T39, T45, T10, T46) :- ','(pc1(d(e(T38)), T42), p1(d(e(T39)), T45)).
p29(T38, T42, T39, T45, T10, T47) :- ','(pc1(d(e(T38)), T42), ','(pc1(d(e(T39)), T45), p1(d(e(T10)), T47))).
p65(e(t), const(1), T138) :- p1(d(e(const(1))), T138).
p65(e(const(T143)), const(0), T138) :- p1(d(e(const(0))), T138).
p65(e(+(T152, T153)), +(X214, X215), T138) :- p1(d(e(T152)), X214).
p65(e(+(T152, T153)), +(T154, X215), T138) :- ','(pc1(d(e(T152)), T154), p1(d(e(T153)), X215)).
p65(e(+(T152, T153)), +(T154, T155), T138) :- ','(pc1(d(e(T152)), T154), ','(pc1(d(e(T153)), T155), p1(d(e(+(T154, T155))), T138))).
p65(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) :- p1(d(e(T168)), X255).
p65(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), p1(d(e(T169)), X254)).
p65(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), ','(pc1(d(e(T169)), T171), p1(d(e(+(*(T168, T171), *(T169, T170)))), T138))).
p65(d(T180), X276, T138) :- p1(d(T180), X275).
p65(d(T180), X276, T138) :- ','(pc1(d(T180), T181), p65(e(T181), X276, T138)).
p1(d(e(+(t, T10))), +(const(1), T15)) :- p1(d(e(T10)), T15).
p1(d(e(+(const(T20), T10))), +(const(0), T21)) :- p1(d(e(T10)), T21).
p1(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) :- p29(T38, T42, T39, T43, T10, T44).
p1(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) :- p29(T64, T68, T65, T69, T10, T70).
p1(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) :- p1(d(e(T76)), T81).
p1(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) :- p1(d(e(T76)), T87).
p1(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) :- p29(T104, T108, T105, T109, T76, T110).
p1(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) :- p29(T127, T131, T128, T132, T76, T133).
p1(d(d(T136)), T138) :- p65(T136, X173, T138).

Clauses:

pc1(d(e(t)), const(1)).
pc1(d(e(const(T4))), const(0)).
pc1(d(e(+(t, T10))), +(const(1), T15)) :- pc1(d(e(T10)), T15).
pc1(d(e(+(const(T20), T10))), +(const(0), T21)) :- pc1(d(e(T10)), T21).
pc1(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) :- qc29(T38, T42, T39, T43, T10, T44).
pc1(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) :- qc29(T64, T68, T65, T69, T10, T70).
pc1(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) :- pc1(d(e(T76)), T81).
pc1(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) :- pc1(d(e(T76)), T87).
pc1(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) :- qc29(T104, T108, T105, T109, T76, T110).
pc1(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) :- qc29(T127, T131, T128, T132, T76, T133).
pc1(d(d(T136)), T138) :- qc65(T136, X173, T138).
qc29(T38, T42, T39, T45, T10, T47) :- ','(pc1(d(e(T38)), T42), ','(pc1(d(e(T39)), T45), pc1(d(e(T10)), T47))).
qc65(e(t), const(1), T138) :- pc1(d(e(const(1))), T138).
qc65(e(const(T143)), const(0), T138) :- pc1(d(e(const(0))), T138).
qc65(e(+(T152, T153)), +(T154, T155), T138) :- ','(pc1(d(e(T152)), T154), ','(pc1(d(e(T153)), T155), pc1(d(e(+(T154, T155))), T138))).
qc65(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) :- ','(pc1(d(e(T168)), T170), ','(pc1(d(e(T169)), T171), pc1(d(e(+(*(T168, T171), *(T169, T170)))), T138))).
qc65(d(T180), X276, T138) :- ','(pc1(d(T180), T181), qc65(e(T181), X276, T138)).

Afs:

p1(x1, x2) = p1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
p1_in: (b,f)
p29_in: (b,f,b,f,b,f)
pc1_in: (b,f)
qc29_in: (b,f,b,f,b,f)
qc65_in: (b,f,f)
p65_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → U24_GA(T10, T15, p1_in_ga(d(e(T10)), T15))
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → U25_GA(T20, T10, T21, p1_in_ga(d(e(T10)), T21))
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U26_GA(T38, T39, T10, T42, T43, T44, p29_in_gagaga(T38, T42, T39, T43, T10, T44))
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → U1_GAGAGA(T38, T42, T39, T43, T10, T44, p1_in_ga(d(e(T38)), T42))
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U27_GA(T64, T65, T10, T69, T68, T70, p29_in_gagaga(T64, T68, T65, T69, T10, T70))
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → U3_GAGAGA(T38, T42, T39, T45, T10, T46, p1_in_ga(d(e(T39)), T45))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U28_GA(T76, T81, p1_in_ga(d(e(T76)), T81))
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U29_GA(T86, T76, T87, p1_in_ga(d(e(T76)), T87))
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U30_GA(T104, T105, T76, T110, T108, T109, p29_in_gagaga(T104, T108, T105, T109, T76, T110))
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U6_GAGAGA(T38, T42, T39, T45, T10, T47, p1_in_ga(d(e(T10)), T47))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U31_GA(T127, T128, T76, T133, T132, T131, p29_in_gagaga(T127, T131, T128, T132, T76, T133))
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)
P1_IN_GA(d(d(T136)), T138) → U32_GA(T136, T138, p65_in_gaa(T136, X173, T138))
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)
P65_IN_GAA(e(t), const(1), T138) → U7_GAA(T138, p1_in_ga(d(e(const(1))), T138))
P65_IN_GAA(e(t), const(1), T138) → P1_IN_GA(d(e(const(1))), T138)
P65_IN_GAA(e(const(T143)), const(0), T138) → U8_GAA(T143, T138, p1_in_ga(d(e(const(0))), T138))
P65_IN_GAA(e(const(T143)), const(0), T138) → P1_IN_GA(d(e(const(0))), T138)
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → U9_GAA(T152, T153, X214, X215, T138, p1_in_ga(d(e(T152)), X214))
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → P1_IN_GA(d(e(T152)), X214)
P65_IN_GAA(e(+(T152, T153)), +(T154, X215), T138) → U10_GAA(T152, T153, T154, X215, T138, pc1_in_ga(d(e(T152)), T154))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → U11_GAA(T152, T153, T154, X215, T138, p1_in_ga(d(e(T153)), X215))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → P1_IN_GA(d(e(T153)), X215)
P65_IN_GAA(e(+(T152, T153)), +(T154, T155), T138) → U12_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U12_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U13_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U14_GAA(T152, T153, T154, T155, T138, p1_in_ga(d(e(+(T154, T155))), T138))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → P1_IN_GA(d(e(+(T154, T155))), T138)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → U15_GAA(T168, T169, X254, X255, T138, p1_in_ga(d(e(T168)), X255))
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → P1_IN_GA(d(e(T168)), X255)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) → U16_GAA(T168, T169, X254, T170, T138, pc1_in_ga(d(e(T168)), T170))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U17_GAA(T168, T169, X254, T170, T138, p1_in_ga(d(e(T169)), X254))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → P1_IN_GA(d(e(T169)), X254)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U18_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U18_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U19_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U20_GAA(T168, T169, T171, T170, T138, p1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → P1_IN_GA(d(e(+(*(T168, T171), *(T169, T170)))), T138)
P65_IN_GAA(d(T180), X276, T138) → U21_GAA(T180, X276, T138, p1_in_ga(d(T180), X275))
P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P65_IN_GAA(d(T180), X276, T138) → U22_GAA(T180, X276, T138, pc1_in_ga(d(T180), T181))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U23_GAA(T180, X276, T138, p65_in_gaa(e(T181), X276, T138))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → P65_IN_GAA(e(T181), X276, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
p1_in_ga(x1, x2) = p1_in_ga(x1)
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
p29_in_gagaga(x1, x2, x3, x4, x5, x6) = p29_in_gagaga(x1, x3, x5)
*(x1, x2) = *(x1, x2)
pc1_in_ga(x1, x2) = pc1_in_ga(x1)
pc1_out_ga(x1, x2) = pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3) = U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7) = U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6) = qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7) = U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6) = qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3) = U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4) = U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7) = U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7) = U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3) = U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3) = qc65_in_gaa(x1)
U46_gaa(x1, x2) = U46_gaa(x2)
1 = 1
qc65_out_gaa(x1, x2, x3) = qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3) = U47_gaa(x1, x3)
0 = 0
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6) = U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6) = U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6) = U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4) = U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4) = U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7) = U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7) = U45_gagaga(x1, x2, x3, x4, x5, x7)
p65_in_gaa(x1, x2, x3) = p65_in_gaa(x1)
P1_IN_GA(x1, x2) = P1_IN_GA(x1)
U24_GA(x1, x2, x3) = U24_GA(x1, x3)
U25_GA(x1, x2, x3, x4) = U25_GA(x1, x2, x4)
U26_GA(x1, x2, x3, x4, x5, x6, x7) = U26_GA(x1, x2, x3, x7)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6) = P29_IN_GAGAGA(x1, x3, x5)
U1_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U1_GAGAGA(x1, x3, x5, x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7) = U27_GA(x1, x2, x3, x7)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U2_GAGAGA(x1, x3, x5, x7)
U3_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U3_GAGAGA(x1, x3, x5, x7)
U28_GA(x1, x2, x3) = U28_GA(x1, x3)
U29_GA(x1, x2, x3, x4) = U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4, x5, x6, x7) = U30_GA(x1, x2, x3, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GAGAGA(x1, x3, x5, x7)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U6_GAGAGA(x1, x3, x5, x7)
U31_GA(x1, x2, x3, x4, x5, x6, x7) = U31_GA(x1, x2, x3, x7)
U32_GA(x1, x2, x3) = U32_GA(x1, x3)
P65_IN_GAA(x1, x2, x3) = P65_IN_GAA(x1)
U7_GAA(x1, x2) = U7_GAA(x2)
U8_GAA(x1, x2, x3) = U8_GAA(x1, x3)
U9_GAA(x1, x2, x3, x4, x5, x6) = U9_GAA(x1, x2, x6)
U10_GAA(x1, x2, x3, x4, x5, x6) = U10_GAA(x1, x2, x6)
U11_GAA(x1, x2, x3, x4, x5, x6) = U11_GAA(x1, x2, x6)
U12_GAA(x1, x2, x3, x4, x5, x6) = U12_GAA(x1, x2, x6)
U13_GAA(x1, x2, x3, x4, x5, x6) = U13_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6) = U14_GAA(x1, x2, x6)
U15_GAA(x1, x2, x3, x4, x5, x6) = U15_GAA(x1, x2, x6)
U16_GAA(x1, x2, x3, x4, x5, x6) = U16_GAA(x1, x2, x6)
U17_GAA(x1, x2, x3, x4, x5, x6) = U17_GAA(x1, x2, x6)
U18_GAA(x1, x2, x3, x4, x5, x6) = U18_GAA(x1, x2, x6)
U19_GAA(x1, x2, x3, x4, x5, x6) = U19_GAA(x1, x2, x4, x6)
U20_GAA(x1, x2, x3, x4, x5, x6) = U20_GAA(x1, x2, x6)
U21_GAA(x1, x2, x3, x4) = U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4) = U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4) = U23_GAA(x1, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → U24_GA(T10, T15, p1_in_ga(d(e(T10)), T15))
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → U25_GA(T20, T10, T21, p1_in_ga(d(e(T10)), T21))
P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U26_GA(T38, T39, T10, T42, T43, T44, p29_in_gagaga(T38, T42, T39, T43, T10, T44))
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → U1_GAGAGA(T38, T42, T39, T43, T10, T44, p1_in_ga(d(e(T38)), T42))
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U27_GA(T64, T65, T10, T69, T68, T70, p29_in_gagaga(T64, T68, T65, T69, T10, T70))
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → U3_GAGAGA(T38, T42, T39, T45, T10, T46, p1_in_ga(d(e(T39)), T45))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U28_GA(T76, T81, p1_in_ga(d(e(T76)), T81))
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U29_GA(T86, T76, T87, p1_in_ga(d(e(T76)), T87))
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U30_GA(T104, T105, T76, T110, T108, T109, p29_in_gagaga(T104, T108, T105, T109, T76, T110))
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U6_GAGAGA(T38, T42, T39, T45, T10, T47, p1_in_ga(d(e(T10)), T47))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U31_GA(T127, T128, T76, T133, T132, T131, p29_in_gagaga(T127, T131, T128, T132, T76, T133))
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)
P1_IN_GA(d(d(T136)), T138) → U32_GA(T136, T138, p65_in_gaa(T136, X173, T138))
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)
P65_IN_GAA(e(t), const(1), T138) → U7_GAA(T138, p1_in_ga(d(e(const(1))), T138))
P65_IN_GAA(e(t), const(1), T138) → P1_IN_GA(d(e(const(1))), T138)
P65_IN_GAA(e(const(T143)), const(0), T138) → U8_GAA(T143, T138, p1_in_ga(d(e(const(0))), T138))
P65_IN_GAA(e(const(T143)), const(0), T138) → P1_IN_GA(d(e(const(0))), T138)
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → U9_GAA(T152, T153, X214, X215, T138, p1_in_ga(d(e(T152)), X214))
P65_IN_GAA(e(+(T152, T153)), +(X214, X215), T138) → P1_IN_GA(d(e(T152)), X214)
P65_IN_GAA(e(+(T152, T153)), +(T154, X215), T138) → U10_GAA(T152, T153, T154, X215, T138, pc1_in_ga(d(e(T152)), T154))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → U11_GAA(T152, T153, T154, X215, T138, p1_in_ga(d(e(T153)), X215))
U10_GAA(T152, T153, T154, X215, T138, pc1_out_ga(d(e(T152)), T154)) → P1_IN_GA(d(e(T153)), X215)
P65_IN_GAA(e(+(T152, T153)), +(T154, T155), T138) → U12_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U12_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U13_GAA(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U14_GAA(T152, T153, T154, T155, T138, p1_in_ga(d(e(+(T154, T155))), T138))
U13_GAA(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → P1_IN_GA(d(e(+(T154, T155))), T138)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → U15_GAA(T168, T169, X254, X255, T138, p1_in_ga(d(e(T168)), X255))
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, X255)), T138) → P1_IN_GA(d(e(T168)), X255)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, X254), *(T169, T170)), T138) → U16_GAA(T168, T169, X254, T170, T138, pc1_in_ga(d(e(T168)), T170))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U17_GAA(T168, T169, X254, T170, T138, p1_in_ga(d(e(T169)), X254))
U16_GAA(T168, T169, X254, T170, T138, pc1_out_ga(d(e(T168)), T170)) → P1_IN_GA(d(e(T169)), X254)
P65_IN_GAA(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U18_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U18_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U19_GAA(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U20_GAA(T168, T169, T171, T170, T138, p1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U19_GAA(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → P1_IN_GA(d(e(+(*(T168, T171), *(T169, T170)))), T138)
P65_IN_GAA(d(T180), X276, T138) → U21_GAA(T180, X276, T138, p1_in_ga(d(T180), X275))
P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P65_IN_GAA(d(T180), X276, T138) → U22_GAA(T180, X276, T138, pc1_in_ga(d(T180), T181))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U23_GAA(T180, X276, T138, p65_in_gaa(e(T181), X276, T138))
U22_GAA(T180, X276, T138, pc1_out_ga(d(T180), T181)) → P65_IN_GAA(e(T181), X276, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 38 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
*(x1, x2) = *(x1, x2)
pc1_in_ga(x1, x2) = pc1_in_ga(x1)
pc1_out_ga(x1, x2) = pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3) = U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7) = U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6) = qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7) = U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6) = qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3) = U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4) = U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7) = U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7) = U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3) = U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3) = qc65_in_gaa(x1)
U46_gaa(x1, x2) = U46_gaa(x2)
1 = 1
qc65_out_gaa(x1, x2, x3) = qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3) = U47_gaa(x1, x3)
0 = 0
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6) = U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6) = U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6) = U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4) = U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4) = U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7) = U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7) = U45_gagaga(x1, x2, x3, x4, x5, x7)
P1_IN_GA(x1, x2) = P1_IN_GA(x1)
P29_IN_GAGAGA(x1, x2, x3, x4, x5, x6) = P29_IN_GAGAGA(x1, x3, x5)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U2_GAGAGA(x1, x3, x5, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GAGAGA(x1, x3, x5, x7)

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:

P1_IN_GA(d(e(+(const(T20), T10))), +(const(0), T21)) → P1_IN_GA(d(e(T10)), T21)
P1_IN_GA(d(e(+(t, T10))), +(const(1), T15)) → P1_IN_GA(d(e(T10)), T15)
P1_IN_GA(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44)
P29_IN_GAGAGA(T38, T42, T39, T43, T10, T44) → P1_IN_GA(d(e(T38)), T42)
P1_IN_GA(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → P29_IN_GAGAGA(T64, T68, T65, T69, T10, T70)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T46) → U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_in_ga(d(e(T38)), T42))
U2_GAGAGA(T38, T42, T39, T45, T10, T46, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)), T45)
P1_IN_GA(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → P1_IN_GA(d(e(T76)), T81)
P1_IN_GA(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → P1_IN_GA(d(e(T76)), T87)
P1_IN_GA(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → P29_IN_GAGAGA(T104, T108, T105, T109, T76, T110)
P29_IN_GAGAGA(T38, T42, T39, T45, T10, T47) → U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U4_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U5_GAGAGA(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)), T47)
P1_IN_GA(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → P29_IN_GAGAGA(T127, T131, T128, T132, T76, T133)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

(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:

P1_IN_GA(d(e(+(const(T20), T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(t, T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(+(T38, T39), T10)))) → P29_IN_GAGAGA(T38, T39, T10)
P29_IN_GAGAGA(T38, T39, T10) → P1_IN_GA(d(e(T38)))
P1_IN_GA(d(e(+(*(T64, T65), T10)))) → P29_IN_GAGAGA(T64, T65, T10)
P29_IN_GAGAGA(T38, T39, T10) → U2_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U2_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)))
P1_IN_GA(d(e(*(t, T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(const(T86), T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(+(T104, T105), T76)))) → P29_IN_GAGAGA(T104, T105, T76)
P29_IN_GAGAGA(T38, T39, T10) → U4_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U4_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T39))))
U5_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(*(*(T127, T128), T76)))) → P29_IN_GAGAGA(T127, T128, T76)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t))) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4)))) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10)))) → U34_ga(T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(const(T20), T10)))) → U35_ga(T20, T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(+(T38, T39), T10)))) → U36_ga(T38, T39, T10, qc29_in_gagaga(T38, T39, T10))
pc1_in_ga(d(e(+(*(T64, T65), T10)))) → U37_ga(T64, T65, T10, qc29_in_gagaga(T64, T65, T10))
pc1_in_ga(d(e(*(t, T76)))) → U38_ga(T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(const(T86), T76)))) → U39_ga(T86, T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(+(T104, T105), T76)))) → U40_ga(T104, T105, T76, qc29_in_gagaga(T104, T105, T76))
pc1_in_ga(d(e(*(*(T127, T128), T76)))) → U41_ga(T127, T128, T76, qc29_in_gagaga(T127, T128, T76))
U34_ga(T10, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T39, T10) → U43_gagaga(T38, T39, T10, pc1_in_ga(d(e(T38))))
U43_gagaga(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T10, pc1_in_ga(d(e(T39))))
U44_gagaga(T38, T42, T39, T10, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, pc1_in_ga(d(e(T10))))
U45_gagaga(T38, T42, T39, T45, T10, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

The set Q consists of the following terms:

pc1_in_ga(x0)
U34_ga(x0, x1)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2, x3)
U41_ga(x0, x1, x2, x3)
qc29_in_gagaga(x0, x1, x2)
U43_gagaga(x0, x1, x2, x3)
U44_gagaga(x0, x1, x2, x3, x4)
U45_gagaga(x0, x1, x2, x3, x4, x5)

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

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P1_IN_GA(d(e(+(const(T20), T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(t, T10)))) → P1_IN_GA(d(e(T10)))
P1_IN_GA(d(e(+(+(T38, T39), T10)))) → P29_IN_GAGAGA(T38, T39, T10)
P29_IN_GAGAGA(T38, T39, T10) → P1_IN_GA(d(e(T38)))
P1_IN_GA(d(e(+(*(T64, T65), T10)))) → P29_IN_GAGAGA(T64, T65, T10)
U2_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → P1_IN_GA(d(e(T39)))
P1_IN_GA(d(e(*(t, T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(const(T86), T76)))) → P1_IN_GA(d(e(T76)))
P1_IN_GA(d(e(*(+(T104, T105), T76)))) → P29_IN_GAGAGA(T104, T105, T76)
P29_IN_GAGAGA(T38, T39, T10) → U4_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
P1_IN_GA(d(e(*(*(T127, T128), T76)))) → P29_IN_GAGAGA(T127, T128, T76)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = 1 + x₁ + x₂
POL(+(x₁, x₂)) = 1 + x₁ + x₂
POL(0) = 0
POL(1) = 0
POL(P1_IN_GA(x₁)) = x₁
POL(P29_IN_GAGAGA(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U2_GAGAGA(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃
POL(U34_ga(x₁, x₂)) = 0
POL(U35_ga(x₁, x₂, x₃)) = 0
POL(U36_ga(x₁, x₂, x₃, x₄)) = 0
POL(U37_ga(x₁, x₂, x₃, x₄)) = 0
POL(U38_ga(x₁, x₂)) = 0
POL(U39_ga(x₁, x₂, x₃)) = 0
POL(U40_ga(x₁, x₂, x₃, x₄)) = 0
POL(U41_ga(x₁, x₂, x₃, x₄)) = 0
POL(U43_gagaga(x₁, x₂, x₃, x₄)) = 0
POL(U44_gagaga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U45_gagaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U4_GAGAGA(x₁, x₂, x₃, x₄)) = x₂ + x₃
POL(U5_GAGAGA(x₁, x₂, x₃, x₄)) = x₂ + x₃
POL(const(x₁)) = 1
POL(d(x₁)) = x₁
POL(e(x₁)) = x₁
POL(pc1_in_ga(x₁)) = 0
POL(pc1_out_ga(x₁, x₂)) = 0
POL(qc29_in_gagaga(x₁, x₂, x₃)) = 0
POL(qc29_out_gagaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(t) = 1

The following usable rules [FROCOS05] were oriented: none

(13) Obligation:

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

P29_IN_GAGAGA(T38, T39, T10) → U2_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T38))))
U4_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U5_GAGAGA(T38, T39, T10, pc1_in_ga(d(e(T39))))
U5_GAGAGA(T38, T39, T10, pc1_out_ga(d(e(T39)), T45)) → P1_IN_GA(d(e(T10)))

The TRS R consists of the following rules:

pc1_in_ga(d(e(t))) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4)))) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10)))) → U34_ga(T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(const(T20), T10)))) → U35_ga(T20, T10, pc1_in_ga(d(e(T10))))
pc1_in_ga(d(e(+(+(T38, T39), T10)))) → U36_ga(T38, T39, T10, qc29_in_gagaga(T38, T39, T10))
pc1_in_ga(d(e(+(*(T64, T65), T10)))) → U37_ga(T64, T65, T10, qc29_in_gagaga(T64, T65, T10))
pc1_in_ga(d(e(*(t, T76)))) → U38_ga(T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(const(T86), T76)))) → U39_ga(T86, T76, pc1_in_ga(d(e(T76))))
pc1_in_ga(d(e(*(+(T104, T105), T76)))) → U40_ga(T104, T105, T76, qc29_in_gagaga(T104, T105, T76))
pc1_in_ga(d(e(*(*(T127, T128), T76)))) → U41_ga(T127, T128, T76, qc29_in_gagaga(T127, T128, T76))
U34_ga(T10, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))
U35_ga(T20, T10, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U36_ga(T38, T39, T10, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U37_ga(T64, T65, T10, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
U38_ga(T76, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U39_ga(T86, T76, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U40_ga(T104, T105, T76, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
U41_ga(T127, T128, T76, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
qc29_in_gagaga(T38, T39, T10) → U43_gagaga(T38, T39, T10, pc1_in_ga(d(e(T38))))
U43_gagaga(T38, T39, T10, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T10, pc1_in_ga(d(e(T39))))
U44_gagaga(T38, T42, T39, T10, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, pc1_in_ga(d(e(T10))))
U45_gagaga(T38, T42, T39, T45, T10, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)

The set Q consists of the following terms:

pc1_in_ga(x0)
U34_ga(x0, x1)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2, x3)
U41_ga(x0, x1, x2, x3)
qc29_in_gagaga(x0, x1, x2)
U43_gagaga(x0, x1, x2, x3)
U44_gagaga(x0, x1, x2, x3, x4)
U45_gagaga(x0, x1, x2, x3, x4, x5)

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

(14) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(15) TRUE

(16) Obligation:

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

P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)

The TRS R consists of the following rules:

pc1_in_ga(d(e(t)), const(1)) → pc1_out_ga(d(e(t)), const(1))
pc1_in_ga(d(e(const(T4))), const(0)) → pc1_out_ga(d(e(const(T4))), const(0))
pc1_in_ga(d(e(+(t, T10))), +(const(1), T15)) → U34_ga(T10, T15, pc1_in_ga(d(e(T10)), T15))
pc1_in_ga(d(e(+(const(T20), T10))), +(const(0), T21)) → U35_ga(T20, T10, T21, pc1_in_ga(d(e(T10)), T21))
pc1_in_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44)) → U36_ga(T38, T39, T10, T42, T43, T44, qc29_in_gagaga(T38, T42, T39, T43, T10, T44))
qc29_in_gagaga(T38, T42, T39, T45, T10, T47) → U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T38)), T42))
pc1_in_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70)) → U37_ga(T64, T65, T10, T69, T68, T70, qc29_in_gagaga(T64, T68, T65, T69, T10, T70))
U37_ga(T64, T65, T10, T69, T68, T70, qc29_out_gagaga(T64, T68, T65, T69, T10, T70)) → pc1_out_ga(d(e(+(*(T64, T65), T10))), +(+(*(T64, T69), *(T65, T68)), T70))
pc1_in_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1)))) → U38_ga(T76, T81, pc1_in_ga(d(e(T76)), T81))
pc1_in_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0)))) → U39_ga(T86, T76, T87, pc1_in_ga(d(e(T76)), T87))
pc1_in_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109)))) → U40_ga(T104, T105, T76, T110, T108, T109, qc29_in_gagaga(T104, T108, T105, T109, T76, T110))
U40_ga(T104, T105, T76, T110, T108, T109, qc29_out_gagaga(T104, T108, T105, T109, T76, T110)) → pc1_out_ga(d(e(*(+(T104, T105), T76))), +(*(+(T104, T105), T110), *(T76, +(T108, T109))))
pc1_in_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131))))) → U41_ga(T127, T128, T76, T133, T132, T131, qc29_in_gagaga(T127, T131, T128, T132, T76, T133))
U41_ga(T127, T128, T76, T133, T132, T131, qc29_out_gagaga(T127, T131, T128, T132, T76, T133)) → pc1_out_ga(d(e(*(*(T127, T128), T76))), +(*(*(T127, T128), T133), *(T76, +(*(T127, T132), *(T128, T131)))))
pc1_in_ga(d(d(T136)), T138) → U42_ga(T136, T138, qc65_in_gaa(T136, X173, T138))
qc65_in_gaa(e(t), const(1), T138) → U46_gaa(T138, pc1_in_ga(d(e(const(1))), T138))
U46_gaa(T138, pc1_out_ga(d(e(const(1))), T138)) → qc65_out_gaa(e(t), const(1), T138)
qc65_in_gaa(e(const(T143)), const(0), T138) → U47_gaa(T143, T138, pc1_in_ga(d(e(const(0))), T138))
U47_gaa(T143, T138, pc1_out_ga(d(e(const(0))), T138)) → qc65_out_gaa(e(const(T143)), const(0), T138)
qc65_in_gaa(e(+(T152, T153)), +(T154, T155), T138) → U48_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T152)), T154))
U48_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T152)), T154)) → U49_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(T153)), T155))
U49_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(T153)), T155)) → U50_gaa(T152, T153, T154, T155, T138, pc1_in_ga(d(e(+(T154, T155))), T138))
U50_gaa(T152, T153, T154, T155, T138, pc1_out_ga(d(e(+(T154, T155))), T138)) → qc65_out_gaa(e(+(T152, T153)), +(T154, T155), T138)
qc65_in_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138) → U51_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T168)), T170))
U51_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T168)), T170)) → U52_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(T169)), T171))
U52_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(T169)), T171)) → U53_gaa(T168, T169, T171, T170, T138, pc1_in_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138))
U53_gaa(T168, T169, T171, T170, T138, pc1_out_ga(d(e(+(*(T168, T171), *(T169, T170)))), T138)) → qc65_out_gaa(e(*(T168, T169)), +(*(T168, T171), *(T169, T170)), T138)
qc65_in_gaa(d(T180), X276, T138) → U54_gaa(T180, X276, T138, pc1_in_ga(d(T180), T181))
U54_gaa(T180, X276, T138, pc1_out_ga(d(T180), T181)) → U55_gaa(T180, X276, T138, qc65_in_gaa(e(T181), X276, T138))
U55_gaa(T180, X276, T138, qc65_out_gaa(e(T181), X276, T138)) → qc65_out_gaa(d(T180), X276, T138)
U42_ga(T136, T138, qc65_out_gaa(T136, X173, T138)) → pc1_out_ga(d(d(T136)), T138)
U39_ga(T86, T76, T87, pc1_out_ga(d(e(T76)), T87)) → pc1_out_ga(d(e(*(const(T86), T76))), +(*(const(T86), T87), *(T76, const(0))))
U38_ga(T76, T81, pc1_out_ga(d(e(T76)), T81)) → pc1_out_ga(d(e(*(t, T76))), +(*(t, T81), *(T76, const(1))))
U43_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T38)), T42)) → U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T39)), T45))
U44_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T39)), T45)) → U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_in_ga(d(e(T10)), T47))
U45_gagaga(T38, T42, T39, T45, T10, T47, pc1_out_ga(d(e(T10)), T47)) → qc29_out_gagaga(T38, T42, T39, T45, T10, T47)
U36_ga(T38, T39, T10, T42, T43, T44, qc29_out_gagaga(T38, T42, T39, T43, T10, T44)) → pc1_out_ga(d(e(+(+(T38, T39), T10))), +(+(T42, T43), T44))
U35_ga(T20, T10, T21, pc1_out_ga(d(e(T10)), T21)) → pc1_out_ga(d(e(+(const(T20), T10))), +(const(0), T21))
U34_ga(T10, T15, pc1_out_ga(d(e(T10)), T15)) → pc1_out_ga(d(e(+(t, T10))), +(const(1), T15))

The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
*(x1, x2) = *(x1, x2)
pc1_in_ga(x1, x2) = pc1_in_ga(x1)
pc1_out_ga(x1, x2) = pc1_out_ga(x1, x2)
U34_ga(x1, x2, x3) = U34_ga(x1, x3)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U36_ga(x1, x2, x3, x4, x5, x6, x7) = U36_ga(x1, x2, x3, x7)
qc29_in_gagaga(x1, x2, x3, x4, x5, x6) = qc29_in_gagaga(x1, x3, x5)
U43_gagaga(x1, x2, x3, x4, x5, x6, x7) = U43_gagaga(x1, x3, x5, x7)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
qc29_out_gagaga(x1, x2, x3, x4, x5, x6) = qc29_out_gagaga(x1, x2, x3, x4, x5, x6)
U38_ga(x1, x2, x3) = U38_ga(x1, x3)
U39_ga(x1, x2, x3, x4) = U39_ga(x1, x2, x4)
U40_ga(x1, x2, x3, x4, x5, x6, x7) = U40_ga(x1, x2, x3, x7)
U41_ga(x1, x2, x3, x4, x5, x6, x7) = U41_ga(x1, x2, x3, x7)
U42_ga(x1, x2, x3) = U42_ga(x1, x3)
qc65_in_gaa(x1, x2, x3) = qc65_in_gaa(x1)
U46_gaa(x1, x2) = U46_gaa(x2)
1 = 1
qc65_out_gaa(x1, x2, x3) = qc65_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3) = U47_gaa(x1, x3)
0 = 0
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x3, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4, x5, x6) = U51_gaa(x1, x2, x6)
U52_gaa(x1, x2, x3, x4, x5, x6) = U52_gaa(x1, x2, x4, x6)
U53_gaa(x1, x2, x3, x4, x5, x6) = U53_gaa(x1, x2, x3, x4, x6)
U54_gaa(x1, x2, x3, x4) = U54_gaa(x1, x4)
U55_gaa(x1, x2, x3, x4) = U55_gaa(x1, x4)
U44_gagaga(x1, x2, x3, x4, x5, x6, x7) = U44_gagaga(x1, x2, x3, x5, x7)
U45_gagaga(x1, x2, x3, x4, x5, x6, x7) = U45_gagaga(x1, x2, x3, x4, x5, x7)
P1_IN_GA(x1, x2) = P1_IN_GA(x1)
P65_IN_GAA(x1, x2, x3) = P65_IN_GAA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

P65_IN_GAA(d(T180), X276, T138) → P1_IN_GA(d(T180), X275)
P1_IN_GA(d(d(T136)), T138) → P65_IN_GAA(T136, X173, T138)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
P1_IN_GA(x1, x2) = P1_IN_GA(x1)
P65_IN_GAA(x1, x2, x3) = P65_IN_GAA(x1)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

P65_IN_GAA(d(T180)) → P1_IN_GA(d(T180))
P1_IN_GA(d(d(T136))) → P65_IN_GAA(T136)

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

(21) 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:

P1_IN_GA(d(d(T136))) → P65_IN_GAA(T136)
The graph contains the following edges 1 > 1
P65_IN_GAA(d(T180)) → P1_IN_GA(d(T180))
The graph contains the following edges 1 >= 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPOrderProof (EQUIVALENT transformation)

(13) Obligation:

(14) DependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES