Left Termination proof of /tmp/tmp52OQDQ/cnfequiv.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 379 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 661 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 12 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 22 ms)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔, 1177 ms)

        ↳20 QDP

        ↳21 DependencyGraphProof (⇔, 0 ms)

        ↳22 TRUE

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔, 0 ms)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇒, 36 ms)

        ↳27 QDP

        ↳28 QDPOrderProof (⇔, 1021 ms)

        ↳29 QDP

        ↳30 DependencyGraphProof (⇔, 0 ms)

        ↳31 TRUE

    ↳32 PiDP

        ↳33 UsableRulesProof (⇔, 0 ms)

        ↳34 PiDP

        ↳35 PiDPToQDPProof (⇒, 0 ms)

        ↳36 QDP

        ↳37 QDPOrderProof (⇔, 174 ms)

        ↳38 QDP

        ↳39 QDPOrderProof (⇔, 1108 ms)

        ↳40 QDP

        ↳41 DependencyGraphProof (⇔, 0 ms)

        ↳42 TRUE

(0) Obligation:

Clauses:

cnfequiv(X, Y) :- ','(transform(X, Z), cnfequiv(Z, Y)).
cnfequiv(X, X).
transform(n(n(X)), X).
transform(n(a(X, Y)), o(n(X), n(Y))).
transform(n(o(X, Y)), a(n(X), n(Y))).
transform(o(X, a(Y, Z)), a(o(X, Y), o(X, Z))).
transform(o(a(X, Y), Z), a(o(X, Z), o(Y, Z))).
transform(o(X1, Y), o(X2, Y)) :- transform(X1, X2).
transform(o(X, Y1), o(X, Y2)) :- transform(Y1, Y2).
transform(a(X1, Y), a(X2, Y)) :- transform(X1, X2).
transform(a(X, Y1), a(X, Y2)) :- transform(Y1, Y2).
transform(n(X1), n(X2)) :- transform(X1, X2).

Query: cnfequiv(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: cnfequiv(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: cnfequiv(T1, T2), SCOPE: 1, CLAUSE: 0 | cnfequiv(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(transform(T5, X7), cnfequiv(X7, T7)) | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 2 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 3 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 4 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 3 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 4 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: cnfequiv(T12, T7)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 4 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: cnfequiv(o(n(T23), n(T24)), T7)\n\nT23 is ground\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: cnfequiv(a(n(T36), n(T37)), T7)\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: cnfequiv(a(o(T53, T54), o(T53, T55)), T7)\n\nT53 is ground\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: cnfequiv(a(o(T72, T74), o(T73, T74)), T7)\n\nT72 is ground\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="B: ','(transform(T87, X97), cnfequiv(o(X97, T88), T7))\n\nT87 is ground\nT88 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="G: transform(T87, X97)\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: cnfequiv(o(T91, T88), T7)\n\nT88 is ground\nT91 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: transform(T87, X97), SCOPE: 3, CLAUSE: 2 | transform(T87, X97), SCOPE: 3, CLAUSE: 3 | transform(T87, X97), SCOPE: 3, CLAUSE: 4 | transform(T87, X97), SCOPE: 3, CLAUSE: 5 | transform(T87, X97), SCOPE: 3, CLAUSE: 6 | transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: transform(T87, X97), SCOPE: 3, CLAUSE: 2\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: transform(T87, X97), SCOPE: 3, CLAUSE: 3 | transform(T87, X97), SCOPE: 3, CLAUSE: 4 | transform(T87, X97), SCOPE: 3, CLAUSE: 5 | transform(T87, X97), SCOPE: 3, CLAUSE: 6 | transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: transform(T87, X97), SCOPE: 3, CLAUSE: 3\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: transform(T87, X97), SCOPE: 3, CLAUSE: 4 | transform(T87, X97), SCOPE: 3, CLAUSE: 5 | transform(T87, X97), SCOPE: 3, CLAUSE: 6 | transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: transform(T87, X97), SCOPE: 3, CLAUSE: 4\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: transform(T87, X97), SCOPE: 3, CLAUSE: 5 | transform(T87, X97), SCOPE: 3, CLAUSE: 6 | transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: transform(T87, X97), SCOPE: 3, CLAUSE: 5\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: transform(T87, X97), SCOPE: 3, CLAUSE: 6 | transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: transform(T87, X97), SCOPE: 3, CLAUSE: 6\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: transform(T87, X97), SCOPE: 3, CLAUSE: 7 | transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: transform(T87, X97), SCOPE: 3, CLAUSE: 7\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: transform(T87, X97), SCOPE: 3, CLAUSE: 8 | transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: transform(T157, X176)\n\nT157 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: transform(T87, X97), SCOPE: 3, CLAUSE: 8\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: transform(T87, X97), SCOPE: 3, CLAUSE: 9 | transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: transform(T170, X198)\n\nT170 is ground\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: transform(T87, X97), SCOPE: 3, CLAUSE: 9\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: transform(T87, X97), SCOPE: 3, CLAUSE: 10 | transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: transform(T181, X220)\n\nT181 is ground\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: transform(T87, X97), SCOPE: 3, CLAUSE: 10\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: transform(T87, X97), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: transform(T194, X242)\n\nT194 is ground\nX242 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: transform(T199, X253)\n\nT199 is ground\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="C: ','(transform(T214, X278), cnfequiv(o(T213, X278), T7))\n\nT213 is ground\nT214 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: transform(T214, X278)\n\nT214 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: cnfequiv(o(T213, T217), T7)\n\nT213 is ground\nT217 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10 | ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="D: ','(transform(T231, X305), cnfequiv(a(X305, T232), T7))\n\nT231 is ground\nT232 is ground\nX305 is free", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: transform(T231, X305)\n\nT231 is ground\nX305 is free", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: cnfequiv(a(T235, T232), T7)\n\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11 | ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="E: ','(transform(T250, X332), cnfequiv(a(T249, X332), T7))\n\nT249 is ground\nT250 is ground\nX332 is free", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: transform(T250, X332)\n\nT250 is ground\nX332 is free", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: cnfequiv(a(T249, T253), T7)\n\nT249 is ground\nT253 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11\n\nT5 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="F: ','(transform(T263, X354), cnfequiv(n(X354), T7))\n\nT263 is ground\nX354 is free", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: transform(T263, X354)\n\nT263 is ground\nX354 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: cnfequiv(n(T266), T7)\n\nT266 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 259 [arrowhead = none ];
259 -> 5;

260 [label="ONLY EVAL with clause\ncnfequiv(X5, X6) :- ','(transform(X5, X7), cnfequiv(X7, X6)).\nand substitutionT1 -> T5,\nX5 -> T5,\nT2 -> T7,\nX6 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 260 [arrowhead = none ];
260 -> 8;

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

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

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 263 [arrowhead = none ];
263 -> 16;

264 [label="EVAL with clause\ntransform(n(n(X12)), X12).\nand substitutionX12 -> T12,\nT5 -> n(n(T12)),\nX7 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 264 [arrowhead = none ];
264 -> 19;

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

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 266 [arrowhead = none ];
266 -> 25;

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

268 [label="INSTANCE with matching:\nT1 -> T12\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
19 -> 268 [arrowhead = none , style=dashed];
268 -> 2[style=dashed];

269 [label="EVAL with clause\ntransform(n(a(X24, X25)), o(n(X24), n(X25))).\nand substitutionX24 -> T23,\nX25 -> T24,\nT5 -> n(a(T23, T24)),\nX7 -> o(n(T23), n(T24))", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 269 [arrowhead = none ];
269 -> 29;

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

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

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

273 [label="INSTANCE with matching:\nT1 -> o(n(T23), n(T24))\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
29 -> 273 [arrowhead = none , style=dashed];
273 -> 2[style=dashed];

274 [label="EVAL with clause\ntransform(n(o(X37, X38)), a(n(X37), n(X38))).\nand substitutionX37 -> T36,\nX38 -> T37,\nT5 -> n(o(T36, T37)),\nX7 -> a(n(T36), n(T37))", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 274 [arrowhead = none ];
274 -> 42;

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

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 276 [arrowhead = none ];
276 -> 49;

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

278 [label="INSTANCE with matching:\nT1 -> a(n(T36), n(T37))\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 278 [arrowhead = none , style=dashed];
278 -> 2[style=dashed];

279 [label="EVAL with clause\ntransform(o(X54, a(X55, X56)), a(o(X54, X55), o(X54, X56))).\nand substitutionX54 -> T53,\nX55 -> T54,\nX56 -> T55,\nT5 -> o(T53, a(T54, T55)),\nX7 -> a(o(T53, T54), o(T53, T55))", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 279 [arrowhead = none ];
279 -> 54;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 280 [arrowhead = none ];
280 -> 55;

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

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

283 [label="INSTANCE with matching:\nT1 -> a(o(T53, T54), o(T53, T55))\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
54 -> 283 [arrowhead = none , style=dashed];
283 -> 2[style=dashed];

284 [label="EVAL with clause\ntransform(o(a(X72, X73), X74), a(o(X72, X74), o(X73, X74))).\nand substitutionX72 -> T72,\nX73 -> T73,\nX74 -> T74,\nT5 -> o(a(T72, T73), T74),\nX7 -> a(o(T72, T74), o(T73, T74))", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 284 [arrowhead = none ];
284 -> 67;

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

286 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 286 [arrowhead = none ];
286 -> 71;

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

288 [label="INSTANCE with matching:\nT1 -> a(o(T72, T74), o(T73, T74))\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 288 [arrowhead = none , style=dashed];
288 -> 2[style=dashed];

289 [label="EVAL with clause\ntransform(o(X94, X95), o(X96, X95)) :- transform(X94, X96).\nand substitutionX94 -> T87,\nX95 -> T88,\nT5 -> o(T87, T88),\nX96 -> X97,\nX7 -> o(X97, T88)", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 289 [arrowhead = none ];
289 -> 75;

290 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 290 [arrowhead = none ];
290 -> 77;

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

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

293 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
75 -> 293 [arrowhead = none ];
293 -> 85;

294 [label="SPLIT 2\nnew knowledge:\nT87 is ground\nT91 is ground\nreplacements:X97 -> T91", fontsize=14, style = filled, fillcolor = violet];
75 -> 294 [arrowhead = none ];
294 -> 86;

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

296 [label="INSTANCE with matching:\nT1 -> o(T91, T88)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 296 [arrowhead = none , style=dashed];
296 -> 2[style=dashed];

297 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
89 -> 297 [arrowhead = none ];
297 -> 94;

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
89 -> 298 [arrowhead = none ];
298 -> 95;

299 [label="EVAL with clause\ntransform(n(n(X106)), X106).\nand substitutionX106 -> T98,\nT87 -> n(n(T98)),\nX97 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 299 [arrowhead = none ];
299 -> 100;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 300 [arrowhead = none ];
300 -> 101;

301 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
95 -> 301 [arrowhead = none ];
301 -> 103;

302 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
95 -> 302 [arrowhead = none ];
302 -> 105;

303 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 303 [arrowhead = none ];
303 -> 102;

304 [label="EVAL with clause\ntransform(n(a(X115, X116)), o(n(X115), n(X116))).\nand substitutionX115 -> T107,\nX116 -> T108,\nT87 -> n(a(T107, T108)),\nX97 -> o(n(T107), n(T108))", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 304 [arrowhead = none ];
304 -> 110;

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

306 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
105 -> 306 [arrowhead = none ];
306 -> 114;

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

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

309 [label="EVAL with clause\ntransform(n(o(X125, X126)), a(n(X125), n(X126))).\nand substitutionX125 -> T117,\nX126 -> T118,\nT87 -> n(o(T117, T118)),\nX97 -> a(n(T117), n(T118))", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 309 [arrowhead = none ];
309 -> 118;

310 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 310 [arrowhead = none ];
310 -> 121;

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

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

313 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 313 [arrowhead = none ];
313 -> 122;

314 [label="EVAL with clause\ntransform(o(X139, a(X140, X141)), a(o(X139, X140), o(X139, X141))).\nand substitutionX139 -> T131,\nX140 -> T132,\nX141 -> T133,\nT87 -> o(T131, a(T132, T133)),\nX97 -> a(o(T131, T132), o(T131, T133))", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 314 [arrowhead = none ];
314 -> 135;

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

316 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 316 [arrowhead = none ];
316 -> 140;

317 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 317 [arrowhead = none ];
317 -> 141;

318 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 318 [arrowhead = none ];
318 -> 139;

319 [label="EVAL with clause\ntransform(o(a(X154, X155), X156), a(o(X154, X156), o(X155, X156))).\nand substitutionX154 -> T146,\nX155 -> T147,\nX156 -> T148,\nT87 -> o(a(T146, T147), T148),\nX97 -> a(o(T146, T148), o(T147, T148))", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 319 [arrowhead = none ];
319 -> 147;

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

321 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 321 [arrowhead = none ];
321 -> 150;

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 322 [arrowhead = none ];
322 -> 151;

323 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 323 [arrowhead = none ];
323 -> 149;

324 [label="EVAL with clause\ntransform(o(X173, X174), o(X175, X174)) :- transform(X173, X175).\nand substitutionX173 -> T157,\nX174 -> T158,\nT87 -> o(T157, T158),\nX175 -> X176,\nX97 -> o(X176, T158)", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 324 [arrowhead = none ];
324 -> 156;

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

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

327 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
151 -> 327 [arrowhead = none ];
327 -> 164;

328 [label="INSTANCE with matching:\nT87 -> T157\nX97 -> X176", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 328 [arrowhead = none , style=dashed];
328 -> 85[style=dashed];

329 [label="EVAL with clause\ntransform(o(X195, X196), o(X195, X197)) :- transform(X196, X197).\nand substitutionX195 -> T169,\nX196 -> T170,\nT87 -> o(T169, T170),\nX197 -> X198,\nX97 -> o(T169, X198)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 329 [arrowhead = none ];
329 -> 168;

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

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

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

333 [label="INSTANCE with matching:\nT87 -> T170\nX97 -> X198", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 333 [arrowhead = none , style=dashed];
333 -> 85[style=dashed];

334 [label="EVAL with clause\ntransform(a(X217, X218), a(X219, X218)) :- transform(X217, X219).\nand substitutionX217 -> T181,\nX218 -> T182,\nT87 -> a(T181, T182),\nX219 -> X220,\nX97 -> a(X220, T182)", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 334 [arrowhead = none ];
334 -> 182;

335 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 335 [arrowhead = none ];
335 -> 183;

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

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

338 [label="INSTANCE with matching:\nT87 -> T181\nX97 -> X220", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 338 [arrowhead = none , style=dashed];
338 -> 85[style=dashed];

339 [label="EVAL with clause\ntransform(a(X239, X240), a(X239, X241)) :- transform(X240, X241).\nand substitutionX239 -> T193,\nX240 -> T194,\nT87 -> a(T193, T194),\nX241 -> X242,\nX97 -> a(T193, X242)", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 339 [arrowhead = none ];
339 -> 194;

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

341 [label="EVAL with clause\ntransform(n(X251), n(X252)) :- transform(X251, X252).\nand substitutionX251 -> T199,\nT87 -> n(T199),\nX252 -> X253,\nX97 -> n(X253)", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 341 [arrowhead = none ];
341 -> 201;

342 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 342 [arrowhead = none ];
342 -> 202;

343 [label="INSTANCE with matching:\nT87 -> T194\nX97 -> X242", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 343 [arrowhead = none , style=dashed];
343 -> 85[style=dashed];

344 [label="INSTANCE with matching:\nT87 -> T199\nX97 -> X253", fontsize=14, style = filled, fillcolor = lightgrey];
201 -> 344 [arrowhead = none , style=dashed];
344 -> 85[style=dashed];

345 [label="EVAL with clause\ntransform(o(X275, X276), o(X275, X277)) :- transform(X276, X277).\nand substitutionX275 -> T213,\nX276 -> T214,\nT5 -> o(T213, T214),\nX277 -> X278,\nX7 -> o(T213, X278)", fontsize=14, style = filled, fillcolor = lightblue];
205 -> 345 [arrowhead = none ];
345 -> 209;

346 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 346 [arrowhead = none ];
346 -> 210;

347 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 347 [arrowhead = none ];
347 -> 217;

348 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 348 [arrowhead = none ];
348 -> 218;

349 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
209 -> 349 [arrowhead = none ];
349 -> 213;

350 [label="SPLIT 2\nnew knowledge:\nT214 is ground\nT217 is ground\nreplacements:X278 -> T217", fontsize=14, style = filled, fillcolor = violet];
209 -> 350 [arrowhead = none ];
350 -> 214;

351 [label="INSTANCE with matching:\nT87 -> T214\nX97 -> X278", fontsize=14, style = filled, fillcolor = lightgrey];
213 -> 351 [arrowhead = none , style=dashed];
351 -> 85[style=dashed];

352 [label="INSTANCE with matching:\nT1 -> o(T213, T217)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
214 -> 352 [arrowhead = none , style=dashed];
352 -> 2[style=dashed];

353 [label="EVAL with clause\ntransform(a(X302, X303), a(X304, X303)) :- transform(X302, X304).\nand substitutionX302 -> T231,\nX303 -> T232,\nT5 -> a(T231, T232),\nX304 -> X305,\nX7 -> a(X305, T232)", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 353 [arrowhead = none ];
353 -> 223;

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

355 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
218 -> 355 [arrowhead = none ];
355 -> 231;

356 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
218 -> 356 [arrowhead = none ];
356 -> 232;

357 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
223 -> 357 [arrowhead = none ];
357 -> 225;

358 [label="SPLIT 2\nnew knowledge:\nT231 is ground\nT235 is ground\nreplacements:X305 -> T235", fontsize=14, style = filled, fillcolor = violet];
223 -> 358 [arrowhead = none ];
358 -> 226;

359 [label="INSTANCE with matching:\nT87 -> T231\nX97 -> X305", fontsize=14, style = filled, fillcolor = lightgrey];
225 -> 359 [arrowhead = none , style=dashed];
359 -> 85[style=dashed];

360 [label="INSTANCE with matching:\nT1 -> a(T235, T232)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
226 -> 360 [arrowhead = none , style=dashed];
360 -> 2[style=dashed];

361 [label="EVAL with clause\ntransform(a(X329, X330), a(X329, X331)) :- transform(X330, X331).\nand substitutionX329 -> T249,\nX330 -> T250,\nT5 -> a(T249, T250),\nX331 -> X332,\nX7 -> a(T249, X332)", fontsize=14, style = filled, fillcolor = lightblue];
231 -> 361 [arrowhead = none ];
361 -> 245;

362 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
231 -> 362 [arrowhead = none ];
362 -> 246;

363 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
232 -> 363 [arrowhead = none ];
363 -> 249;

364 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
232 -> 364 [arrowhead = none ];
364 -> 250;

365 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
245 -> 365 [arrowhead = none ];
365 -> 247;

366 [label="SPLIT 2\nnew knowledge:\nT250 is ground\nT253 is ground\nreplacements:X332 -> T253", fontsize=14, style = filled, fillcolor = violet];
245 -> 366 [arrowhead = none ];
366 -> 248;

367 [label="INSTANCE with matching:\nT87 -> T250\nX97 -> X332", fontsize=14, style = filled, fillcolor = lightgrey];
247 -> 367 [arrowhead = none , style=dashed];
367 -> 85[style=dashed];

368 [label="INSTANCE with matching:\nT1 -> a(T249, T253)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
248 -> 368 [arrowhead = none , style=dashed];
368 -> 2[style=dashed];

369 [label="EVAL with clause\ntransform(n(X352), n(X353)) :- transform(X352, X353).\nand substitutionX352 -> T263,\nT5 -> n(T263),\nX353 -> X354,\nX7 -> n(X354)", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 369 [arrowhead = none ];
369 -> 251;

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

371 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
250 -> 371 [arrowhead = none ];
371 -> 255;

372 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
251 -> 372 [arrowhead = none ];
372 -> 253;

373 [label="SPLIT 2\nnew knowledge:\nT263 is ground\nT266 is ground\nreplacements:X354 -> T266", fontsize=14, style = filled, fillcolor = violet];
251 -> 373 [arrowhead = none ];
373 -> 254;

374 [label="INSTANCE with matching:\nT87 -> T263\nX97 -> X354", fontsize=14, style = filled, fillcolor = lightgrey];
253 -> 374 [arrowhead = none , style=dashed];
374 -> 85[style=dashed];

375 [label="INSTANCE with matching:\nT1 -> n(T266)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
254 -> 375 [arrowhead = none , style=dashed];
375 -> 2[style=dashed];

376 [label="EVAL with clause\ncnfequiv(X364, X364).\nand substitutionT5 -> T273,\nX364 -> T273,\nT2 -> T273", fontsize=14, style = filled, fillcolor = lightblue];
255 -> 376 [arrowhead = none ];
376 -> 256;

377 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
255 -> 377 [arrowhead = none ];
377 -> 257;

378 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
256 -> 378 [arrowhead = none ];
378 -> 258;

}

(2) Obligation:

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

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

CNFEQUIVA_IN_GA(n(n(T12)), T7) → U1_GA(T12, T7, cnfequivA_in_ga(T12, T7))
CNFEQUIVA_IN_GA(n(n(T12)), T7) → CNFEQUIVA_IN_GA(T12, T7)
CNFEQUIVA_IN_GA(n(a(T23, T24)), T7) → U2_GA(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIVA_IN_GA(n(a(T23, T24)), T7) → CNFEQUIVA_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIVA_IN_GA(n(o(T36, T37)), T7) → U3_GA(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIVA_IN_GA(n(o(T36, T37)), T7) → CNFEQUIVA_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIVA_IN_GA(o(T53, a(T54, T55)), T7) → U4_GA(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIVA_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIVA_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIVA_IN_GA(o(a(T72, T73), T74), T7) → U5_GA(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIVA_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIVA_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIVA_IN_GA(o(T87, T88), T7) → U6_GA(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
CNFEQUIVA_IN_GA(o(T87, T88), T7) → PB_IN_GAGA(T87, X97, T88, T7)
PB_IN_GAGA(T87, T91, T88, T7) → U16_GAGA(T87, T91, T88, T7, transformG_in_ga(T87, T91))
PB_IN_GAGA(T87, T91, T88, T7) → TRANSFORMG_IN_GA(T87, T91)
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → U11_GA(T157, T158, X176, transformG_in_ga(T157, X176))
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMG_IN_GA(T157, X176)
TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → U12_GA(T169, T170, X198, transformG_in_ga(T170, X198))
TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMG_IN_GA(T170, X198)
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → U13_GA(T181, T182, X220, transformG_in_ga(T181, X220))
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMG_IN_GA(T181, X220)
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → U14_GA(T193, T194, X242, transformG_in_ga(T194, X242))
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMG_IN_GA(T194, X242)
TRANSFORMG_IN_GA(n(T199), n(X253)) → U15_GA(T199, X253, transformG_in_ga(T199, X253))
TRANSFORMG_IN_GA(n(T199), n(X253)) → TRANSFORMG_IN_GA(T199, X253)
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_GAGA(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88), T7)
CNFEQUIVA_IN_GA(o(T213, T214), T7) → U7_GA(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
CNFEQUIVA_IN_GA(o(T213, T214), T7) → PC_IN_GAGA(T214, X278, T213, T7)
PC_IN_GAGA(T214, T217, T213, T7) → U18_GAGA(T214, T217, T213, T7, transformG_in_ga(T214, T217))
PC_IN_GAGA(T214, T217, T213, T7) → TRANSFORMG_IN_GA(T214, T217)
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_GAGA(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217), T7)
CNFEQUIVA_IN_GA(a(T231, T232), T7) → U8_GA(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
CNFEQUIVA_IN_GA(a(T231, T232), T7) → PD_IN_GAGA(T231, X305, T232, T7)
PD_IN_GAGA(T231, T235, T232, T7) → U20_GAGA(T231, T235, T232, T7, transformG_in_ga(T231, T235))
PD_IN_GAGA(T231, T235, T232, T7) → TRANSFORMG_IN_GA(T231, T235)
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_GAGA(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232), T7)
CNFEQUIVA_IN_GA(a(T249, T250), T7) → U9_GA(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
CNFEQUIVA_IN_GA(a(T249, T250), T7) → PE_IN_GAGA(T250, X332, T249, T7)
PE_IN_GAGA(T250, T253, T249, T7) → U22_GAGA(T250, T253, T249, T7, transformG_in_ga(T250, T253))
PE_IN_GAGA(T250, T253, T249, T7) → TRANSFORMG_IN_GA(T250, T253)
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_GAGA(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253), T7)
CNFEQUIVA_IN_GA(n(T263), T7) → U10_GA(T263, T7, pF_in_gaa(T263, X354, T7))
CNFEQUIVA_IN_GA(n(T263), T7) → PF_IN_GAA(T263, X354, T7)
PF_IN_GAA(T263, T266, T7) → U24_GAA(T263, T266, T7, transformG_in_ga(T263, T266))
PF_IN_GAA(T263, T266, T7) → TRANSFORMG_IN_GA(T263, T266)
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_GAA(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266), T7)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

The argument filtering Pi contains the following mapping:
cnfequivA_in_ga(x1, x2) = cnfequivA_in_ga(x1)
n(x1) = n(x1)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
a(x1, x2) = a(x1, x2)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
o(x1, x2) = o(x1, x2)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x2, x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x3, x5)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4) = pB_in_gaga(x1, x3)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x3, x5)
transformG_in_ga(x1, x2) = transformG_in_ga(x1)
transformG_out_ga(x1, x2) = transformG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4) = U11_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4) = U12_ga(x1, x2, x4)
U13_ga(x1, x2, x3, x4) = U13_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4) = U14_ga(x1, x2, x4)
U15_ga(x1, x2, x3) = U15_ga(x1, x3)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x2, x3, x5)
U7_ga(x1, x2, x3, x4) = U7_ga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4) = pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5) = U18_gaga(x1, x3, x5)
U19_gaga(x1, x2, x3, x4, x5) = U19_gaga(x1, x2, x3, x5)
U8_ga(x1, x2, x3, x4) = U8_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4) = pD_in_gaga(x1, x3)
U20_gaga(x1, x2, x3, x4, x5) = U20_gaga(x1, x3, x5)
U21_gaga(x1, x2, x3, x4, x5) = U21_gaga(x1, x2, x3, x5)
U9_ga(x1, x2, x3, x4) = U9_ga(x1, x2, x4)
pE_in_gaga(x1, x2, x3, x4) = pE_in_gaga(x1, x3)
U22_gaga(x1, x2, x3, x4, x5) = U22_gaga(x1, x3, x5)
U23_gaga(x1, x2, x3, x4, x5) = U23_gaga(x1, x2, x3, x5)
U10_ga(x1, x2, x3) = U10_ga(x1, x3)
pF_in_gaa(x1, x2, x3) = pF_in_gaa(x1)
U24_gaa(x1, x2, x3, x4) = U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4) = U25_gaa(x1, x2, x4)
cnfequivA_out_ga(x1, x2) = cnfequivA_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3) = pF_out_gaa(x1, x2, x3)
pE_out_gaga(x1, x2, x3, x4) = pE_out_gaga(x1, x2, x3, x4)
pD_out_gaga(x1, x2, x3, x4) = pD_out_gaga(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4) = pC_out_gaga(x1, x2, x3, x4)
pB_out_gaga(x1, x2, x3, x4) = pB_out_gaga(x1, x2, x3, x4)
CNFEQUIVA_IN_GA(x1, x2) = CNFEQUIVA_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x3, x5)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x2, x3, x5)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x2, x4)
PB_IN_GAGA(x1, x2, x3, x4) = PB_IN_GAGA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5) = U16_GAGA(x1, x3, x5)
TRANSFORMG_IN_GA(x1, x2) = TRANSFORMG_IN_GA(x1)
U11_GA(x1, x2, x3, x4) = U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4) = U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4) = U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4) = U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3) = U15_GA(x1, x3)
U17_GAGA(x1, x2, x3, x4, x5) = U17_GAGA(x1, x2, x3, x5)
U7_GA(x1, x2, x3, x4) = U7_GA(x1, x2, x4)
PC_IN_GAGA(x1, x2, x3, x4) = PC_IN_GAGA(x1, x3)
U18_GAGA(x1, x2, x3, x4, x5) = U18_GAGA(x1, x3, x5)
U19_GAGA(x1, x2, x3, x4, x5) = U19_GAGA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4) = U8_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4) = PD_IN_GAGA(x1, x3)
U20_GAGA(x1, x2, x3, x4, x5) = U20_GAGA(x1, x3, x5)
U21_GAGA(x1, x2, x3, x4, x5) = U21_GAGA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4) = U9_GA(x1, x2, x4)
PE_IN_GAGA(x1, x2, x3, x4) = PE_IN_GAGA(x1, x3)
U22_GAGA(x1, x2, x3, x4, x5) = U22_GAGA(x1, x3, x5)
U23_GAGA(x1, x2, x3, x4, x5) = U23_GAGA(x1, x2, x3, x5)
U10_GA(x1, x2, x3) = U10_GA(x1, x3)
PF_IN_GAA(x1, x2, x3) = PF_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4) = U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4) = U25_GAA(x1, x2, x4)

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

(4) Obligation:

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

CNFEQUIVA_IN_GA(n(n(T12)), T7) → U1_GA(T12, T7, cnfequivA_in_ga(T12, T7))
CNFEQUIVA_IN_GA(n(n(T12)), T7) → CNFEQUIVA_IN_GA(T12, T7)
CNFEQUIVA_IN_GA(n(a(T23, T24)), T7) → U2_GA(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIVA_IN_GA(n(a(T23, T24)), T7) → CNFEQUIVA_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIVA_IN_GA(n(o(T36, T37)), T7) → U3_GA(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIVA_IN_GA(n(o(T36, T37)), T7) → CNFEQUIVA_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIVA_IN_GA(o(T53, a(T54, T55)), T7) → U4_GA(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIVA_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIVA_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIVA_IN_GA(o(a(T72, T73), T74), T7) → U5_GA(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIVA_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIVA_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIVA_IN_GA(o(T87, T88), T7) → U6_GA(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
CNFEQUIVA_IN_GA(o(T87, T88), T7) → PB_IN_GAGA(T87, X97, T88, T7)
PB_IN_GAGA(T87, T91, T88, T7) → U16_GAGA(T87, T91, T88, T7, transformG_in_ga(T87, T91))
PB_IN_GAGA(T87, T91, T88, T7) → TRANSFORMG_IN_GA(T87, T91)
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → U11_GA(T157, T158, X176, transformG_in_ga(T157, X176))
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMG_IN_GA(T157, X176)
TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → U12_GA(T169, T170, X198, transformG_in_ga(T170, X198))
TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMG_IN_GA(T170, X198)
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → U13_GA(T181, T182, X220, transformG_in_ga(T181, X220))
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMG_IN_GA(T181, X220)
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → U14_GA(T193, T194, X242, transformG_in_ga(T194, X242))
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMG_IN_GA(T194, X242)
TRANSFORMG_IN_GA(n(T199), n(X253)) → U15_GA(T199, X253, transformG_in_ga(T199, X253))
TRANSFORMG_IN_GA(n(T199), n(X253)) → TRANSFORMG_IN_GA(T199, X253)
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_GAGA(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88), T7)
CNFEQUIVA_IN_GA(o(T213, T214), T7) → U7_GA(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
CNFEQUIVA_IN_GA(o(T213, T214), T7) → PC_IN_GAGA(T214, X278, T213, T7)
PC_IN_GAGA(T214, T217, T213, T7) → U18_GAGA(T214, T217, T213, T7, transformG_in_ga(T214, T217))
PC_IN_GAGA(T214, T217, T213, T7) → TRANSFORMG_IN_GA(T214, T217)
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_GAGA(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217), T7)
CNFEQUIVA_IN_GA(a(T231, T232), T7) → U8_GA(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
CNFEQUIVA_IN_GA(a(T231, T232), T7) → PD_IN_GAGA(T231, X305, T232, T7)
PD_IN_GAGA(T231, T235, T232, T7) → U20_GAGA(T231, T235, T232, T7, transformG_in_ga(T231, T235))
PD_IN_GAGA(T231, T235, T232, T7) → TRANSFORMG_IN_GA(T231, T235)
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_GAGA(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232), T7)
CNFEQUIVA_IN_GA(a(T249, T250), T7) → U9_GA(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
CNFEQUIVA_IN_GA(a(T249, T250), T7) → PE_IN_GAGA(T250, X332, T249, T7)
PE_IN_GAGA(T250, T253, T249, T7) → U22_GAGA(T250, T253, T249, T7, transformG_in_ga(T250, T253))
PE_IN_GAGA(T250, T253, T249, T7) → TRANSFORMG_IN_GA(T250, T253)
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_GAGA(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253), T7)
CNFEQUIVA_IN_GA(n(T263), T7) → U10_GA(T263, T7, pF_in_gaa(T263, X354, T7))
CNFEQUIVA_IN_GA(n(T263), T7) → PF_IN_GAA(T263, X354, T7)
PF_IN_GAA(T263, T266, T7) → U24_GAA(T263, T266, T7, transformG_in_ga(T263, T266))
PF_IN_GAA(T263, T266, T7) → TRANSFORMG_IN_GA(T263, T266)
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_GAA(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266), T7)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 29 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMG_IN_GA(T170, X198)
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMG_IN_GA(T157, X176)
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMG_IN_GA(T181, X220)
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMG_IN_GA(T194, X242)
TRANSFORMG_IN_GA(n(T199), n(X253)) → TRANSFORMG_IN_GA(T199, X253)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

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

TRANSFORMG_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMG_IN_GA(T170, X198)
TRANSFORMG_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMG_IN_GA(T157, X176)
TRANSFORMG_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMG_IN_GA(T181, X220)
TRANSFORMG_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMG_IN_GA(T194, X242)
TRANSFORMG_IN_GA(n(T199), n(X253)) → TRANSFORMG_IN_GA(T199, X253)

R is empty.
The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
TRANSFORMG_IN_GA(x1, x2) = TRANSFORMG_IN_GA(x1)

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

TRANSFORMG_IN_GA(o(T169, T170)) → TRANSFORMG_IN_GA(T170)
TRANSFORMG_IN_GA(o(T157, T158)) → TRANSFORMG_IN_GA(T157)
TRANSFORMG_IN_GA(a(T181, T182)) → TRANSFORMG_IN_GA(T181)
TRANSFORMG_IN_GA(a(T193, T194)) → TRANSFORMG_IN_GA(T194)
TRANSFORMG_IN_GA(n(T199)) → TRANSFORMG_IN_GA(T199)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

TRANSFORMG_IN_GA(o(T169, T170)) → TRANSFORMG_IN_GA(T170)
The graph contains the following edges 1 > 1
TRANSFORMG_IN_GA(o(T157, T158)) → TRANSFORMG_IN_GA(T157)
The graph contains the following edges 1 > 1
TRANSFORMG_IN_GA(a(T181, T182)) → TRANSFORMG_IN_GA(T181)
The graph contains the following edges 1 > 1
TRANSFORMG_IN_GA(a(T193, T194)) → TRANSFORMG_IN_GA(T194)
The graph contains the following edges 1 > 1
TRANSFORMG_IN_GA(n(T199)) → TRANSFORMG_IN_GA(T199)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

PD_IN_GAGA(T231, T235, T232, T7) → U20_GAGA(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232), T7)
CNFEQUIVA_IN_GA(a(T231, T232), T7) → PD_IN_GAGA(T231, X305, T232, T7)
CNFEQUIVA_IN_GA(a(T249, T250), T7) → PE_IN_GAGA(T250, X332, T249, T7)
PE_IN_GAGA(T250, T253, T249, T7) → U22_GAGA(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253), T7)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

PD_IN_GAGA(T231, T235, T232, T7) → U20_GAGA(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_GAGA(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232), T7)
CNFEQUIVA_IN_GA(a(T231, T232), T7) → PD_IN_GAGA(T231, X305, T232, T7)
CNFEQUIVA_IN_GA(a(T249, T250), T7) → PE_IN_GAGA(T250, X332, T249, T7)
PE_IN_GAGA(T250, T253, T249, T7) → U22_GAGA(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_GAGA(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253), T7)

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transformG_in_ga(x1, x2) = transformG_in_ga(x1)
transformG_out_ga(x1, x2) = transformG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4) = U11_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4) = U12_ga(x1, x2, x4)
U13_ga(x1, x2, x3, x4) = U13_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4) = U14_ga(x1, x2, x4)
U15_ga(x1, x2, x3) = U15_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2) = CNFEQUIVA_IN_GA(x1)
PD_IN_GAGA(x1, x2, x3, x4) = PD_IN_GAGA(x1, x3)
U20_GAGA(x1, x2, x3, x4, x5) = U20_GAGA(x1, x3, x5)
PE_IN_GAGA(x1, x2, x3, x4) = PE_IN_GAGA(x1, x3)
U22_GAGA(x1, x2, x3, x4, x5) = U22_GAGA(x1, x3, x5)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

PD_IN_GAGA(T231, T232) → U20_GAGA(T231, T232, transformG_in_ga(T231))
U20_GAGA(T231, T232, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232))
CNFEQUIVA_IN_GA(a(T231, T232)) → PD_IN_GAGA(T231, T232)
CNFEQUIVA_IN_GA(a(T249, T250)) → PE_IN_GAGA(T250, T249)
PE_IN_GAGA(T250, T249) → U22_GAGA(T250, T249, transformG_in_ga(T250))
U22_GAGA(T250, T249, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U20_GAGA(T231, T232, transformG_out_ga(T231, T235)) → CNFEQUIVA_IN_GA(a(T235, T232))
U22_GAGA(T250, T249, transformG_out_ga(T250, T253)) → CNFEQUIVA_IN_GA(a(T249, T253))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PD_IN_GAGA(x1, x2) = PD_IN_GAGA(x1, x2)
U20_GAGA(x1, x2, x3) = U20_GAGA(x2, x3)
transformG_in_ga(x1) = x1
transformG_out_ga(x1, x2) = transformG_out_ga(x2)
CNFEQUIVA_IN_GA(x1) = x1
a(x1, x2) = a(x1, x2)
PE_IN_GAGA(x1, x2) = PE_IN_GAGA(x1, x2)
U22_GAGA(x1, x2, x3) = U22_GAGA(x2, x3)
n(x1) = n(x1)
o(x1, x2) = o(x1, x2)
U11_ga(x1, x2, x3) = U11_ga(x2, x3)
U12_ga(x1, x2, x3) = U12_ga(x1, x3)
U13_ga(x1, x2, x3) = U13_ga(x2, x3)
U14_ga(x1, x2, x3) = U14_ga(x1, x3)
U15_ga(x1, x2) = U15_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:

[n₁, U15_ga₁] > [o₂, U11_ga₂, U12_ga₂] > [PD_{IN_GAGA₂}, U20_GAGA₂, a₂, PE_{IN_GAGA₂}, U22_GAGA₂, U13_ga₂, U14_ga₂] > transformG_{out_ga₁}

Status:

PD_{IN_GAGA₂}: multiset
U20_GAGA₂: multiset
transformG_{out_ga₁}: multiset
a₂: multiset
PE_{IN_GAGA₂}: multiset
U22_GAGA₂: multiset
n₁: [1]
o₂: multiset
U11_ga₂: multiset
U12_ga₂: multiset
U13_ga₂: multiset
U14_ga₂: multiset
U15_ga₁: [1]

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

(20) Obligation:

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

PD_IN_GAGA(T231, T232) → U20_GAGA(T231, T232, transformG_in_ga(T231))
CNFEQUIVA_IN_GA(a(T231, T232)) → PD_IN_GAGA(T231, T232)
CNFEQUIVA_IN_GA(a(T249, T250)) → PE_IN_GAGA(T250, T249)
PE_IN_GAGA(T250, T249) → U22_GAGA(T250, T249, transformG_in_ga(T250))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE

(23) Obligation:

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

CNFEQUIVA_IN_GA(o(T87, T88), T7) → PB_IN_GAGA(T87, X97, T88, T7)
PB_IN_GAGA(T87, T91, T88, T7) → U16_GAGA(T87, T91, T88, T7, transformG_in_ga(T87, T91))
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88), T7)
CNFEQUIVA_IN_GA(o(T213, T214), T7) → PC_IN_GAGA(T214, X278, T213, T7)
PC_IN_GAGA(T214, T217, T213, T7) → U18_GAGA(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217), T7)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

CNFEQUIVA_IN_GA(o(T87, T88), T7) → PB_IN_GAGA(T87, X97, T88, T7)
PB_IN_GAGA(T87, T91, T88, T7) → U16_GAGA(T87, T91, T88, T7, transformG_in_ga(T87, T91))
U16_GAGA(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88), T7)
CNFEQUIVA_IN_GA(o(T213, T214), T7) → PC_IN_GAGA(T214, X278, T213, T7)
PC_IN_GAGA(T214, T217, T213, T7) → U18_GAGA(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_GAGA(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217), T7)

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transformG_in_ga(x1, x2) = transformG_in_ga(x1)
transformG_out_ga(x1, x2) = transformG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4) = U11_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4) = U12_ga(x1, x2, x4)
U13_ga(x1, x2, x3, x4) = U13_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4) = U14_ga(x1, x2, x4)
U15_ga(x1, x2, x3) = U15_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2) = CNFEQUIVA_IN_GA(x1)
PB_IN_GAGA(x1, x2, x3, x4) = PB_IN_GAGA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5) = U16_GAGA(x1, x3, x5)
PC_IN_GAGA(x1, x2, x3, x4) = PC_IN_GAGA(x1, x3)
U18_GAGA(x1, x2, x3, x4, x5) = U18_GAGA(x1, x3, x5)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

CNFEQUIVA_IN_GA(o(T87, T88)) → PB_IN_GAGA(T87, T88)
PB_IN_GAGA(T87, T88) → U16_GAGA(T87, T88, transformG_in_ga(T87))
U16_GAGA(T87, T88, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88))
CNFEQUIVA_IN_GA(o(T213, T214)) → PC_IN_GAGA(T214, T213)
PC_IN_GAGA(T214, T213) → U18_GAGA(T214, T213, transformG_in_ga(T214))
U18_GAGA(T214, T213, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U16_GAGA(T87, T88, transformG_out_ga(T87, T91)) → CNFEQUIVA_IN_GA(o(T91, T88))
U18_GAGA(T214, T213, transformG_out_ga(T214, T217)) → CNFEQUIVA_IN_GA(o(T213, T217))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIVA_IN_GA(x1) = x1
o(x1, x2) = o(x1, x2)
PB_IN_GAGA(x1, x2) = PB_IN_GAGA(x1, x2)
U16_GAGA(x1, x2, x3) = U16_GAGA(x2, x3)
transformG_in_ga(x1) = x1
transformG_out_ga(x1, x2) = transformG_out_ga(x2)
PC_IN_GAGA(x1, x2) = PC_IN_GAGA(x1, x2)
U18_GAGA(x1, x2, x3) = U18_GAGA(x2, x3)
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
U11_ga(x1, x2, x3) = U11_ga(x2, x3)
U12_ga(x1, x2, x3) = U12_ga(x1, x3)
U13_ga(x1, x2, x3) = U13_ga(x2, x3)
U14_ga(x1, x2, x3) = U14_ga(x1, x3)
U15_ga(x1, x2) = U15_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:

[n₁, U15_ga₁] > [o₂, PB_{IN_GAGA₂}, U16_GAGA₂, PC_{IN_GAGA₂}, U18_GAGA₂, U11_ga₂, U12_ga₂] > [a₂, U13_ga₂, U14_ga₂] > transformG_{out_ga₁}

Status:

o₂: [1,2]
PB_{IN_GAGA₂}: [1,2]
U16_GAGA₂: [2,1]
transformG_{out_ga₁}: multiset
PC_{IN_GAGA₂}: [2,1]
U18_GAGA₂: [1,2]
n₁: [1]
a₂: multiset
U11_ga₂: [2,1]
U12_ga₂: [1,2]
U13_ga₂: multiset
U14_ga₂: multiset
U15_ga₁: [1]

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

(29) Obligation:

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

CNFEQUIVA_IN_GA(o(T87, T88)) → PB_IN_GAGA(T87, T88)
PB_IN_GAGA(T87, T88) → U16_GAGA(T87, T88, transformG_in_ga(T87))
CNFEQUIVA_IN_GA(o(T213, T214)) → PC_IN_GAGA(T214, T213)
PC_IN_GAGA(T214, T213) → U18_GAGA(T214, T213, transformG_in_ga(T214))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(30) DependencyGraphProof (EQUIVALENT transformation)

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

(31) TRUE

(32) Obligation:

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

CNFEQUIVA_IN_GA(n(T263), T7) → PF_IN_GAA(T263, X354, T7)
PF_IN_GAA(T263, T266, T7) → U24_GAA(T263, T266, T7, transformG_in_ga(T263, T266))
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266), T7)
CNFEQUIVA_IN_GA(n(n(T12)), T7) → CNFEQUIVA_IN_GA(T12, T7)

The TRS R consists of the following rules:

cnfequivA_in_ga(n(n(T12)), T7) → U1_ga(T12, T7, cnfequivA_in_ga(T12, T7))
cnfequivA_in_ga(n(a(T23, T24)), T7) → U2_ga(T23, T24, T7, cnfequivA_in_ga(o(n(T23), n(T24)), T7))
cnfequivA_in_ga(n(o(T36, T37)), T7) → U3_ga(T36, T37, T7, cnfequivA_in_ga(a(n(T36), n(T37)), T7))
cnfequivA_in_ga(o(T53, a(T54, T55)), T7) → U4_ga(T53, T54, T55, T7, cnfequivA_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivA_in_ga(o(a(T72, T73), T74), T7) → U5_ga(T72, T73, T74, T7, cnfequivA_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivA_in_ga(o(T87, T88), T7) → U6_ga(T87, T88, T7, pB_in_gaga(T87, X97, T88, T7))
pB_in_gaga(T87, T91, T88, T7) → U16_gaga(T87, T91, T88, T7, transformG_in_ga(T87, T91))
transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U16_gaga(T87, T91, T88, T7, transformG_out_ga(T87, T91)) → U17_gaga(T87, T91, T88, T7, cnfequivA_in_ga(o(T91, T88), T7))
cnfequivA_in_ga(o(T213, T214), T7) → U7_ga(T213, T214, T7, pC_in_gaga(T214, X278, T213, T7))
pC_in_gaga(T214, T217, T213, T7) → U18_gaga(T214, T217, T213, T7, transformG_in_ga(T214, T217))
U18_gaga(T214, T217, T213, T7, transformG_out_ga(T214, T217)) → U19_gaga(T214, T217, T213, T7, cnfequivA_in_ga(o(T213, T217), T7))
cnfequivA_in_ga(a(T231, T232), T7) → U8_ga(T231, T232, T7, pD_in_gaga(T231, X305, T232, T7))
pD_in_gaga(T231, T235, T232, T7) → U20_gaga(T231, T235, T232, T7, transformG_in_ga(T231, T235))
U20_gaga(T231, T235, T232, T7, transformG_out_ga(T231, T235)) → U21_gaga(T231, T235, T232, T7, cnfequivA_in_ga(a(T235, T232), T7))
cnfequivA_in_ga(a(T249, T250), T7) → U9_ga(T249, T250, T7, pE_in_gaga(T250, X332, T249, T7))
pE_in_gaga(T250, T253, T249, T7) → U22_gaga(T250, T253, T249, T7, transformG_in_ga(T250, T253))
U22_gaga(T250, T253, T249, T7, transformG_out_ga(T250, T253)) → U23_gaga(T250, T253, T249, T7, cnfequivA_in_ga(a(T249, T253), T7))
cnfequivA_in_ga(n(T263), T7) → U10_ga(T263, T7, pF_in_gaa(T263, X354, T7))
pF_in_gaa(T263, T266, T7) → U24_gaa(T263, T266, T7, transformG_in_ga(T263, T266))
U24_gaa(T263, T266, T7, transformG_out_ga(T263, T266)) → U25_gaa(T263, T266, T7, cnfequivA_in_ga(n(T266), T7))
cnfequivA_in_ga(T273, T273) → cnfequivA_out_ga(T273, T273)
U25_gaa(T263, T266, T7, cnfequivA_out_ga(n(T266), T7)) → pF_out_gaa(T263, T266, T7)
U10_ga(T263, T7, pF_out_gaa(T263, X354, T7)) → cnfequivA_out_ga(n(T263), T7)
U23_gaga(T250, T253, T249, T7, cnfequivA_out_ga(a(T249, T253), T7)) → pE_out_gaga(T250, T253, T249, T7)
U9_ga(T249, T250, T7, pE_out_gaga(T250, X332, T249, T7)) → cnfequivA_out_ga(a(T249, T250), T7)
U21_gaga(T231, T235, T232, T7, cnfequivA_out_ga(a(T235, T232), T7)) → pD_out_gaga(T231, T235, T232, T7)
U8_ga(T231, T232, T7, pD_out_gaga(T231, X305, T232, T7)) → cnfequivA_out_ga(a(T231, T232), T7)
U19_gaga(T214, T217, T213, T7, cnfequivA_out_ga(o(T213, T217), T7)) → pC_out_gaga(T214, T217, T213, T7)
U7_ga(T213, T214, T7, pC_out_gaga(T214, X278, T213, T7)) → cnfequivA_out_ga(o(T213, T214), T7)
U17_gaga(T87, T91, T88, T7, cnfequivA_out_ga(o(T91, T88), T7)) → pB_out_gaga(T87, T91, T88, T7)
U6_ga(T87, T88, T7, pB_out_gaga(T87, X97, T88, T7)) → cnfequivA_out_ga(o(T87, T88), T7)
U5_ga(T72, T73, T74, T7, cnfequivA_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivA_out_ga(o(a(T72, T73), T74), T7)
U4_ga(T53, T54, T55, T7, cnfequivA_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivA_out_ga(o(T53, a(T54, T55)), T7)
U3_ga(T36, T37, T7, cnfequivA_out_ga(a(n(T36), n(T37)), T7)) → cnfequivA_out_ga(n(o(T36, T37)), T7)
U2_ga(T23, T24, T7, cnfequivA_out_ga(o(n(T23), n(T24)), T7)) → cnfequivA_out_ga(n(a(T23, T24)), T7)
U1_ga(T12, T7, cnfequivA_out_ga(T12, T7)) → cnfequivA_out_ga(n(n(T12)), T7)

(33) UsableRulesProof (EQUIVALENT transformation)

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

(34) Obligation:

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

CNFEQUIVA_IN_GA(n(T263), T7) → PF_IN_GAA(T263, X354, T7)
PF_IN_GAA(T263, T266, T7) → U24_GAA(T263, T266, T7, transformG_in_ga(T263, T266))
U24_GAA(T263, T266, T7, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266), T7)
CNFEQUIVA_IN_GA(n(n(T12)), T7) → CNFEQUIVA_IN_GA(T12, T7)

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98)), T98) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158), o(X176, T158)) → U11_ga(T157, T158, X176, transformG_in_ga(T157, X176))
transformG_in_ga(o(T169, T170), o(T169, X198)) → U12_ga(T169, T170, X198, transformG_in_ga(T170, X198))
transformG_in_ga(a(T181, T182), a(X220, T182)) → U13_ga(T181, T182, X220, transformG_in_ga(T181, X220))
transformG_in_ga(a(T193, T194), a(T193, X242)) → U14_ga(T193, T194, X242, transformG_in_ga(T194, X242))
transformG_in_ga(n(T199), n(X253)) → U15_ga(T199, X253, transformG_in_ga(T199, X253))
U11_ga(T157, T158, X176, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, X198, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, X220, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, X242, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, X253, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transformG_in_ga(x1, x2) = transformG_in_ga(x1)
transformG_out_ga(x1, x2) = transformG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4) = U11_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4) = U12_ga(x1, x2, x4)
U13_ga(x1, x2, x3, x4) = U13_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4) = U14_ga(x1, x2, x4)
U15_ga(x1, x2, x3) = U15_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2) = CNFEQUIVA_IN_GA(x1)
PF_IN_GAA(x1, x2, x3) = PF_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4) = U24_GAA(x1, x4)

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

(35) PiDPToQDPProof (SOUND transformation)

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

(36) Obligation:

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

CNFEQUIVA_IN_GA(n(T263)) → PF_IN_GAA(T263)
PF_IN_GAA(T263) → U24_GAA(T263, transformG_in_ga(T263))
U24_GAA(T263, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266))
CNFEQUIVA_IN_GA(n(n(T12))) → CNFEQUIVA_IN_GA(T12)

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

CNFEQUIVA_IN_GA(n(n(T12))) → CNFEQUIVA_IN_GA(T12)

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

POL(CNFEQUIVA_IN_GA(x₁)) = x₁
POL(PF_IN_GAA(x₁)) = 1 + x₁
POL(U11_ga(x₁, x₂, x₃)) = 0
POL(U12_ga(x₁, x₂, x₃)) = 0
POL(U13_ga(x₁, x₂, x₃)) = 0
POL(U14_ga(x₁, x₂, x₃)) = 0
POL(U15_ga(x₁, x₂)) = 1 + x₂
POL(U24_GAA(x₁, x₂)) = 1 + x₂
POL(a(x₁, x₂)) = 0
POL(n(x₁)) = 1 + x₁
POL(o(x₁, x₂)) = 0
POL(transformG_in_ga(x₁)) = x₁
POL(transformG_out_ga(x₁, x₂)) = x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

(38) Obligation:

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

CNFEQUIVA_IN_GA(n(T263)) → PF_IN_GAA(T263)
PF_IN_GAA(T263) → U24_GAA(T263, transformG_in_ga(T263))
U24_GAA(T263, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(39) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

CNFEQUIVA_IN_GA(n(T263)) → PF_IN_GAA(T263)
U24_GAA(T263, transformG_out_ga(T263, T266)) → CNFEQUIVA_IN_GA(n(T266))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIVA_IN_GA(x1) = CNFEQUIVA_IN_GA(x1)
n(x1) = n(x1)
PF_IN_GAA(x1) = PF_IN_GAA(x1)
U24_GAA(x1, x2) = U24_GAA(x2)
transformG_in_ga(x1) = x1
transformG_out_ga(x1, x2) = transformG_out_ga(x2)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
U11_ga(x1, x2, x3) = U11_ga(x2, x3)
U12_ga(x1, x2, x3) = U12_ga(x1, x3)
U13_ga(x1, x2, x3) = U13_ga(x2, x3)
U14_ga(x1, x2, x3) = U14_ga(x1, x3)
U15_ga(x1, x2) = U15_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:

[n₁, PF_{IN_GAA₁}, U24_GAA₁, U15_ga₁] > CNFEQUIVA_{IN_GA₁} > transformG_{out_ga₁}
[n₁, PF_{IN_GAA₁}, U24_GAA₁, U15_ga₁] > [o₂, U11_ga₂, U12_ga₂] > [a₂, U13_ga₂, U14_ga₂] > transformG_{out_ga₁}

Status:

CNFEQUIVA_{IN_GA₁}: multiset
n₁: multiset
PF_{IN_GAA₁}: multiset
U24_GAA₁: multiset
transformG_{out_ga₁}: [1]
a₂: multiset
o₂: multiset
U11_ga₂: multiset
U12_ga₂: multiset
U13_ga₂: multiset
U14_ga₂: multiset
U15_ga₁: multiset

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

(40) Obligation:

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

PF_IN_GAA(T263) → U24_GAA(T263, transformG_in_ga(T263))

The TRS R consists of the following rules:

transformG_in_ga(n(n(T98))) → transformG_out_ga(n(n(T98)), T98)
transformG_in_ga(n(a(T107, T108))) → transformG_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformG_in_ga(n(o(T117, T118))) → transformG_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformG_in_ga(o(T131, a(T132, T133))) → transformG_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformG_in_ga(o(a(T146, T147), T148)) → transformG_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformG_in_ga(o(T157, T158)) → U11_ga(T157, T158, transformG_in_ga(T157))
transformG_in_ga(o(T169, T170)) → U12_ga(T169, T170, transformG_in_ga(T170))
transformG_in_ga(a(T181, T182)) → U13_ga(T181, T182, transformG_in_ga(T181))
transformG_in_ga(a(T193, T194)) → U14_ga(T193, T194, transformG_in_ga(T194))
transformG_in_ga(n(T199)) → U15_ga(T199, transformG_in_ga(T199))
U11_ga(T157, T158, transformG_out_ga(T157, X176)) → transformG_out_ga(o(T157, T158), o(X176, T158))
U12_ga(T169, T170, transformG_out_ga(T170, X198)) → transformG_out_ga(o(T169, T170), o(T169, X198))
U13_ga(T181, T182, transformG_out_ga(T181, X220)) → transformG_out_ga(a(T181, T182), a(X220, T182))
U14_ga(T193, T194, transformG_out_ga(T194, X242)) → transformG_out_ga(a(T193, T194), a(T193, X242))
U15_ga(T199, transformG_out_ga(T199, X253)) → transformG_out_ga(n(T199), n(X253))

The set Q consists of the following terms:

transformG_in_ga(x0)
U11_ga(x0, x1, x2)
U12_ga(x0, x1, x2)
U13_ga(x0, x1, x2)
U14_ga(x0, x1, x2)
U15_ga(x0, x1)

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

(41) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT 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) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) DependencyGraphProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPOrderProof (EQUIVALENT transformation)

(29) Obligation:

(30) DependencyGraphProof (EQUIVALENT transformation)

(31) TRUE

(32) Obligation:

(33) UsableRulesProof (EQUIVALENT transformation)

(34) Obligation:

(35) PiDPToQDPProof (SOUND transformation)

(36) Obligation:

(37) QDPOrderProof (EQUIVALENT transformation)

(38) Obligation:

(39) QDPOrderProof (EQUIVALENT transformation)

(40) Obligation:

(41) DependencyGraphProof (EQUIVALENT transformation)

(42) TRUE