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

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇐)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇐)

        ↳20 QDP

        ↳21 QDPOrderProof (⇔)

        ↳22 QDP

        ↳23 PisEmptyProof (⇔)

        ↳24 YES

    ↳25 PiDP

        ↳26 UsableRulesProof (⇔)

        ↳27 PiDP

        ↳28 PiDPToQDPProof (⇐)

        ↳29 QDP

        ↳30 QDPOrderProof (⇔)

        ↳31 QDP

        ↳32 DependencyGraphProof (⇔)

        ↳33 TRUE

    ↳34 PiDP

        ↳35 UsableRulesProof (⇔)

        ↳36 PiDP

        ↳37 PiDPToQDPProof (⇐)

        ↳38 QDP

        ↳39 QDPOrderProof (⇔)

        ↳40 QDP

        ↳41 QDPOrderProof (⇔)

        ↳42 QDP

        ↳43 PisEmptyProof (⇔)

        ↳44 YES

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

Queries:

cnfequiv(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: cnfequiv(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: cnfequiv(T1, T2), SCOPE: 1, CLAUSE: 0 | cnfequiv(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(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];
4 [label="4: ','(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];
5 [label="5: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(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];
7 [label="7: cnfequiv(T12, T7)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(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];
11 [label="11: cnfequiv(o(n(T23), n(T24)), T7)\n\nT23 is ground\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 4\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: 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];
15 [label="15: cnfequiv(a(n(T36), n(T37)), T7)\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(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(a(o(T53, T54), o(T53, T55)), T7)\n\nT53 is ground\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 6\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(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];
23 [label="23: 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];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 7\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(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];
27 [label="27: ','(transform(T87, X108), cnfequiv(o(X108, T88), T7))\n\nT87 is ground\nT88 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: transform(T87, X108)\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: cnfequiv(o(T91, T88), T7)\n\nT88 is ground\nT91 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: transform(T87, X108), SCOPE: 3, CLAUSE: 2 | transform(T87, X108), SCOPE: 3, CLAUSE: 3 | transform(T87, X108), SCOPE: 3, CLAUSE: 4 | transform(T87, X108), SCOPE: 3, CLAUSE: 5 | transform(T87, X108), SCOPE: 3, CLAUSE: 6 | transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: transform(T87, X108), SCOPE: 3, CLAUSE: 2\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: transform(T87, X108), SCOPE: 3, CLAUSE: 3 | transform(T87, X108), SCOPE: 3, CLAUSE: 4 | transform(T87, X108), SCOPE: 3, CLAUSE: 5 | transform(T87, X108), SCOPE: 3, CLAUSE: 6 | transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: transform(T87, X108), SCOPE: 3, CLAUSE: 3\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: transform(T87, X108), SCOPE: 3, CLAUSE: 4 | transform(T87, X108), SCOPE: 3, CLAUSE: 5 | transform(T87, X108), SCOPE: 3, CLAUSE: 6 | transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: transform(T87, X108), SCOPE: 3, CLAUSE: 4\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: transform(T87, X108), SCOPE: 3, CLAUSE: 5 | transform(T87, X108), SCOPE: 3, CLAUSE: 6 | transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: transform(T87, X108), SCOPE: 3, CLAUSE: 5\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: transform(T87, X108), SCOPE: 3, CLAUSE: 6 | transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: transform(T87, X108), SCOPE: 3, CLAUSE: 6\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: transform(T87, X108), SCOPE: 3, CLAUSE: 7 | transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: transform(T87, X108), SCOPE: 3, CLAUSE: 7\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: transform(T87, X108), SCOPE: 3, CLAUSE: 8 | transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: transform(T157, X201)\n\nT157 is ground\nX201 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: transform(T87, X108), SCOPE: 3, CLAUSE: 8\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: transform(T87, X108), SCOPE: 3, CLAUSE: 9 | transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: transform(T170, X226)\n\nT170 is ground\nX226 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: transform(T87, X108), SCOPE: 3, CLAUSE: 9\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: transform(T87, X108), SCOPE: 3, CLAUSE: 10 | transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: transform(T181, X251)\n\nT181 is ground\nX251 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: transform(T87, X108), SCOPE: 3, CLAUSE: 10\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: transform(T87, X108), SCOPE: 3, CLAUSE: 11\n\nT87 is ground\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: transform(T194, X276)\n\nT194 is ground\nX276 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: transform(T199, X290)\n\nT199 is ground\nX290 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 8\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(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];
77 [label="77: ','(transform(T214, X317), cnfequiv(o(T213, X317), T7))\n\nT213 is ground\nT214 is ground\nX317 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: transform(T214, X317)\n\nT214 is ground\nX317 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: cnfequiv(o(T213, T217), T7)\n\nT213 is ground\nT217 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 9\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(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];
83 [label="83: ','(transform(T231, X347), cnfequiv(a(X347, T232), T7))\n\nT231 is ground\nT232 is ground\nX347 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: transform(T231, X347)\n\nT231 is ground\nX347 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: cnfequiv(a(T235, T232), T7)\n\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 10\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(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];
89 [label="89: ','(transform(T250, X377), cnfequiv(a(T249, X377), T7))\n\nT249 is ground\nT250 is ground\nX377 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: transform(T250, X377)\n\nT250 is ground\nX377 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: cnfequiv(a(T249, T253), T7)\n\nT249 is ground\nT253 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(transform(T5, X7), cnfequiv(X7, T7)), SCOPE: 2, CLAUSE: 11\n\nT5 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ?_2 | cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(transform(T263, X402), cnfequiv(n(X402), T7))\n\nT263 is ground\nX402 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: transform(T263, X402)\n\nT263 is ground\nX402 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: cnfequiv(n(T266), T7)\n\nT266 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: cnfequiv(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", 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="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 103 [arrowhead = none ];
103 -> 2;

104 [label="ONLY EVAL with clause\ncnfequiv(X5, X6) :- ','(transform(X5, X7), cnfequiv(X7, X6)).\nand substitution\nT1 -> T5\nX5 -> T5\nT2 -> T7\nX6 -> T7\nT6 -> T7", fontsize=14, style = filled, fillcolor = white];
2 -> 104 [arrowhead = none ];
104 -> 3;

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

106 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 106 [arrowhead = none ];
106 -> 5;

107 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 107 [arrowhead = none ];
107 -> 6;

108 [label="EVAL with clause\ntransform(n(n(X12)), X12).\nand substitution\nX12 -> T12\nT5 -> n(n(T12))\nX7 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 108 [arrowhead = none ];
108 -> 7;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 109 [arrowhead = none ];
109 -> 8;

110 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 110 [arrowhead = none ];
110 -> 9;

111 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 111 [arrowhead = none ];
111 -> 10;

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

113 [label="EVAL with clause\ntransform(n(a(X25, X26)), o(n(X25), n(X26))).\nand substitution\nX25 -> T23\nX26 -> T24\nT5 -> n(a(T23, T24))\nX7 -> o(n(T23), n(T24))", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 113 [arrowhead = none ];
113 -> 11;

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

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

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

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

118 [label="EVAL with clause\ntransform(n(o(X40, X41)), a(n(X40), n(X41))).\nand substitution\nX40 -> T36\nX41 -> T37\nT5 -> n(o(T36, T37))\nX7 -> a(n(T36), n(T37))", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 118 [arrowhead = none ];
118 -> 15;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 119 [arrowhead = none ];
119 -> 16;

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

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

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

123 [label="EVAL with clause\ntransform(o(X59, a(X60, X61)), a(o(X59, X60), o(X59, X61))).\nand substitution\nX59 -> T53\nX60 -> T54\nX61 -> T55\nT5 -> o(T53, a(T54, T55))\nX7 -> a(o(T53, T54), o(T53, T55))", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 123 [arrowhead = none ];
123 -> 19;

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

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

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

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

128 [label="EVAL with clause\ntransform(o(a(X80, X81), X82), a(o(X80, X82), o(X81, X82))).\nand substitution\nX80 -> T72\nX81 -> T73\nX82 -> T74\nT5 -> o(a(T72, T73), T74)\nX7 -> a(o(T72, T74), o(T73, T74))", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 128 [arrowhead = none ];
128 -> 23;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 129 [arrowhead = none ];
129 -> 24;

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

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 131 [arrowhead = none ];
131 -> 26;

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

133 [label="EVAL with clause\ntransform(o(X105, X106), o(X107, X106)) :- transform(X105, X107).\nand substitution\nX105 -> T87\nX106 -> T88\nT5 -> o(T87, T88)\nX107 -> X108\nX7 -> o(X108, T88)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 133 [arrowhead = none ];
133 -> 27;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 134 [arrowhead = none ];
134 -> 28;

135 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 135 [arrowhead = none ];
135 -> 75;

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

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

138 [label="SPLIT 2\nnew knowledge:\nT91 is ground\nreplacements:\nX108 -> T91", fontsize=14, style = filled, fillcolor = violet];
27 -> 138 [arrowhead = none ];
138 -> 30;

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

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

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

142 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 142 [arrowhead = none ];
142 -> 33;

143 [label="EVAL with clause\ntransform(n(n(X120)), X120).\nand substitution\nX120 -> T98\nT87 -> n(n(T98))\nX108 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 143 [arrowhead = none ];
143 -> 34;

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

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

146 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
33 -> 146 [arrowhead = none ];
146 -> 38;

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

148 [label="EVAL with clause\ntransform(n(a(X130, X131)), o(n(X130), n(X131))).\nand substitution\nX130 -> T107\nX131 -> T108\nT87 -> n(a(T107, T108))\nX108 -> o(n(T107), n(T108))", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 148 [arrowhead = none ];
148 -> 39;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 149 [arrowhead = none ];
149 -> 40;

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

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

152 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 152 [arrowhead = none ];
152 -> 41;

153 [label="EVAL with clause\ntransform(n(o(X142, X143)), a(n(X142), n(X143))).\nand substitution\nX142 -> T117\nX143 -> T118\nT87 -> n(o(T117, T118))\nX108 -> a(n(T117), n(T118))", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 153 [arrowhead = none ];
153 -> 44;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 154 [arrowhead = none ];
154 -> 45;

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

156 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 156 [arrowhead = none ];
156 -> 48;

157 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 157 [arrowhead = none ];
157 -> 46;

158 [label="EVAL with clause\ntransform(o(X158, a(X159, X160)), a(o(X158, X159), o(X158, X160))).\nand substitution\nX158 -> T131\nX159 -> T132\nX160 -> T133\nT87 -> o(T131, a(T132, T133))\nX108 -> a(o(T131, T132), o(T131, T133))", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 158 [arrowhead = none ];
158 -> 49;

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

160 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 160 [arrowhead = none ];
160 -> 52;

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

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

163 [label="EVAL with clause\ntransform(o(a(X176, X177), X178), a(o(X176, X178), o(X177, X178))).\nand substitution\nX176 -> T146\nX177 -> T147\nX178 -> T148\nT87 -> o(a(T146, T147), T148)\nX108 -> a(o(T146, T148), o(T147, T148))", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 163 [arrowhead = none ];
163 -> 54;

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 164 [arrowhead = none ];
164 -> 55;

165 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 165 [arrowhead = none ];
165 -> 57;

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

167 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 167 [arrowhead = none ];
167 -> 56;

168 [label="EVAL with clause\ntransform(o(X198, X199), o(X200, X199)) :- transform(X198, X200).\nand substitution\nX198 -> T157\nX199 -> T158\nT87 -> o(T157, T158)\nX200 -> X201\nX108 -> o(X201, T158)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 168 [arrowhead = none ];
168 -> 59;

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

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

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

172 [label="INSTANCE with matching:\nT87 -> T157\nX108 -> X201", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 172 [arrowhead = none , style=dashed];
172 -> 29[style=dashed];

173 [label="EVAL with clause\ntransform(o(X223, X224), o(X223, X225)) :- transform(X224, X225).\nand substitution\nX223 -> T169\nX224 -> T170\nT87 -> o(T169, T170)\nX225 -> X226\nX108 -> o(T169, X226)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 173 [arrowhead = none ];
173 -> 63;

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

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

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

177 [label="INSTANCE with matching:\nT87 -> T170\nX108 -> X226", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 177 [arrowhead = none , style=dashed];
177 -> 29[style=dashed];

178 [label="EVAL with clause\ntransform(a(X248, X249), a(X250, X249)) :- transform(X248, X250).\nand substitution\nX248 -> T181\nX249 -> T182\nT87 -> a(T181, T182)\nX250 -> X251\nX108 -> a(X251, T182)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 178 [arrowhead = none ];
178 -> 67;

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

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

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

182 [label="INSTANCE with matching:\nT87 -> T181\nX108 -> X251", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 182 [arrowhead = none , style=dashed];
182 -> 29[style=dashed];

183 [label="EVAL with clause\ntransform(a(X273, X274), a(X273, X275)) :- transform(X274, X275).\nand substitution\nX273 -> T193\nX274 -> T194\nT87 -> a(T193, T194)\nX275 -> X276\nX108 -> a(T193, X276)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 183 [arrowhead = none ];
183 -> 71;

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

185 [label="EVAL with clause\ntransform(n(X288), n(X289)) :- transform(X288, X289).\nand substitution\nX288 -> T199\nT87 -> n(T199)\nX289 -> X290\nX108 -> n(X290)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 185 [arrowhead = none ];
185 -> 73;

186 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 186 [arrowhead = none ];
186 -> 74;

187 [label="INSTANCE with matching:\nT87 -> T194\nX108 -> X276", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 187 [arrowhead = none , style=dashed];
187 -> 29[style=dashed];

188 [label="INSTANCE with matching:\nT87 -> T199\nX108 -> X290", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 188 [arrowhead = none , style=dashed];
188 -> 29[style=dashed];

189 [label="EVAL with clause\ntransform(o(X314, X315), o(X314, X316)) :- transform(X315, X316).\nand substitution\nX314 -> T213\nX315 -> T214\nT5 -> o(T213, T214)\nX316 -> X317\nX7 -> o(T213, X317)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 189 [arrowhead = none ];
189 -> 77;

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

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

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

193 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
77 -> 193 [arrowhead = none ];
193 -> 79;

194 [label="SPLIT 2\nnew knowledge:\nT217 is ground\nreplacements:\nX317 -> T217", fontsize=14, style = filled, fillcolor = violet];
77 -> 194 [arrowhead = none ];
194 -> 80;

195 [label="INSTANCE with matching:\nT87 -> T214\nX108 -> X317", fontsize=14, style = filled, fillcolor = lightgrey];
79 -> 195 [arrowhead = none , style=dashed];
195 -> 29[style=dashed];

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

197 [label="EVAL with clause\ntransform(a(X344, X345), a(X346, X345)) :- transform(X344, X346).\nand substitution\nX344 -> T231\nX345 -> T232\nT5 -> a(T231, T232)\nX346 -> X347\nX7 -> a(X347, T232)", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 197 [arrowhead = none ];
197 -> 83;

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

199 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 199 [arrowhead = none ];
199 -> 87;

200 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 200 [arrowhead = none ];
200 -> 88;

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

202 [label="SPLIT 2\nnew knowledge:\nT235 is ground\nreplacements:\nX347 -> T235", fontsize=14, style = filled, fillcolor = violet];
83 -> 202 [arrowhead = none ];
202 -> 86;

203 [label="INSTANCE with matching:\nT87 -> T231\nX108 -> X347", fontsize=14, style = filled, fillcolor = lightgrey];
85 -> 203 [arrowhead = none , style=dashed];
203 -> 29[style=dashed];

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

205 [label="EVAL with clause\ntransform(a(X374, X375), a(X374, X376)) :- transform(X375, X376).\nand substitution\nX374 -> T249\nX375 -> T250\nT5 -> a(T249, T250)\nX376 -> X377\nX7 -> a(T249, X377)", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 205 [arrowhead = none ];
205 -> 89;

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

207 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 207 [arrowhead = none ];
207 -> 93;

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

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

210 [label="SPLIT 2\nnew knowledge:\nT253 is ground\nreplacements:\nX377 -> T253", fontsize=14, style = filled, fillcolor = violet];
89 -> 210 [arrowhead = none ];
210 -> 92;

211 [label="INSTANCE with matching:\nT87 -> T250\nX108 -> X377", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 211 [arrowhead = none , style=dashed];
211 -> 29[style=dashed];

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

213 [label="EVAL with clause\ntransform(n(X400), n(X401)) :- transform(X400, X401).\nand substitution\nX400 -> T263\nT5 -> n(T263)\nX401 -> X402\nX7 -> n(X402)", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 213 [arrowhead = none ];
213 -> 95;

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

215 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 215 [arrowhead = none ];
215 -> 99;

216 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
95 -> 216 [arrowhead = none ];
216 -> 97;

217 [label="SPLIT 2\nnew knowledge:\nT266 is ground\nreplacements:\nX402 -> T266", fontsize=14, style = filled, fillcolor = violet];
95 -> 217 [arrowhead = none ];
217 -> 98;

218 [label="INSTANCE with matching:\nT87 -> T263\nX108 -> X402", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 218 [arrowhead = none , style=dashed];
218 -> 29[style=dashed];

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

220 [label="EVAL with clause\ncnfequiv(X414, X414).\nand substitution\nT5 -> T273\nX414 -> T273\nT2 -> T273", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 220 [arrowhead = none ];
220 -> 100;

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

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

}

(2) Obligation:

Clauses:

transform29(n(n(T98)), T98).
transform29(n(a(T107, T108)), o(n(T107), n(T108))).
transform29(n(o(T117, T118)), a(n(T117), n(T118))).
transform29(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))).
transform29(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))).
transform29(o(T157, T158), o(X201, T158)) :- transform29(T157, X201).
transform29(o(T169, T170), o(T169, X226)) :- transform29(T170, X226).
transform29(a(T181, T182), a(X251, T182)) :- transform29(T181, X251).
transform29(a(T193, T194), a(T193, X276)) :- transform29(T194, X276).
transform29(n(T199), n(X290)) :- transform29(T199, X290).
cnfequiv1(n(n(T12)), T7) :- cnfequiv1(T12, T7).
cnfequiv1(n(a(T23, T24)), T7) :- cnfequiv1(o(n(T23), n(T24)), T7).
cnfequiv1(n(o(T36, T37)), T7) :- cnfequiv1(a(n(T36), n(T37)), T7).
cnfequiv1(o(T53, a(T54, T55)), T7) :- cnfequiv1(a(o(T53, T54), o(T53, T55)), T7).
cnfequiv1(o(a(T72, T73), T74), T7) :- cnfequiv1(a(o(T72, T74), o(T73, T74)), T7).
cnfequiv1(o(T87, T88), T7) :- transform29(T87, X108).
cnfequiv1(o(T87, T88), T7) :- ','(transform29(T87, T91), cnfequiv1(o(T91, T88), T7)).
cnfequiv1(o(T213, T214), T7) :- transform29(T214, X317).
cnfequiv1(o(T213, T214), T7) :- ','(transform29(T214, T217), cnfequiv1(o(T213, T217), T7)).
cnfequiv1(a(T231, T232), T7) :- transform29(T231, X347).
cnfequiv1(a(T231, T232), T7) :- ','(transform29(T231, T235), cnfequiv1(a(T235, T232), T7)).
cnfequiv1(a(T249, T250), T7) :- transform29(T250, X377).
cnfequiv1(a(T249, T250), T7) :- ','(transform29(T250, T253), cnfequiv1(a(T249, T253), T7)).
cnfequiv1(n(T263), T7) :- transform29(T263, X402).
cnfequiv1(n(T263), T7) :- ','(transform29(T263, T266), cnfequiv1(n(T266), T7)).
cnfequiv1(T273, T273).

Queries:

cnfequiv1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
cnfequiv1_in: (b,f)
transform29_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

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

CNFEQUIV1_IN_GA(n(n(T12)), T7) → U6_GA(T12, T7, cnfequiv1_in_ga(T12, T7))
CNFEQUIV1_IN_GA(n(n(T12)), T7) → CNFEQUIV1_IN_GA(T12, T7)
CNFEQUIV1_IN_GA(n(a(T23, T24)), T7) → U7_GA(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIV1_IN_GA(n(a(T23, T24)), T7) → CNFEQUIV1_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIV1_IN_GA(n(o(T36, T37)), T7) → U8_GA(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIV1_IN_GA(n(o(T36, T37)), T7) → CNFEQUIV1_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIV1_IN_GA(o(T53, a(T54, T55)), T7) → U9_GA(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIV1_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIV1_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIV1_IN_GA(o(a(T72, T73), T74), T7) → U10_GA(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIV1_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIV1_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIV1_IN_GA(o(T87, T88), T7) → U11_GA(T87, T88, T7, transform29_in_ga(T87, X108))
CNFEQUIV1_IN_GA(o(T87, T88), T7) → TRANSFORM29_IN_GA(T87, X108)
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → U1_GA(T157, T158, X201, transform29_in_ga(T157, X201))
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → TRANSFORM29_IN_GA(T157, X201)
TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → U2_GA(T169, T170, X226, transform29_in_ga(T170, X226))
TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → TRANSFORM29_IN_GA(T170, X226)
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → U3_GA(T181, T182, X251, transform29_in_ga(T181, X251))
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → TRANSFORM29_IN_GA(T181, X251)
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → U4_GA(T193, T194, X276, transform29_in_ga(T194, X276))
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → TRANSFORM29_IN_GA(T194, X276)
TRANSFORM29_IN_GA(n(T199), n(X290)) → U5_GA(T199, X290, transform29_in_ga(T199, X290))
TRANSFORM29_IN_GA(n(T199), n(X290)) → TRANSFORM29_IN_GA(T199, X290)
CNFEQUIV1_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transform29_in_ga(T87, T91))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_GA(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → CNFEQUIV1_IN_GA(o(T91, T88), T7)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U14_GA(T213, T214, T7, transform29_in_ga(T214, X317))
CNFEQUIV1_IN_GA(o(T213, T214), T7) → TRANSFORM29_IN_GA(T214, X317)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transform29_in_ga(T214, T217))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_GA(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → CNFEQUIV1_IN_GA(o(T213, T217), T7)
CNFEQUIV1_IN_GA(a(T231, T232), T7) → U17_GA(T231, T232, T7, transform29_in_ga(T231, X347))
CNFEQUIV1_IN_GA(a(T231, T232), T7) → TRANSFORM29_IN_GA(T231, X347)
CNFEQUIV1_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transform29_in_ga(T231, T235))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_GA(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → CNFEQUIV1_IN_GA(a(T235, T232), T7)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U20_GA(T249, T250, T7, transform29_in_ga(T250, X377))
CNFEQUIV1_IN_GA(a(T249, T250), T7) → TRANSFORM29_IN_GA(T250, X377)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transform29_in_ga(T250, T253))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_GA(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → CNFEQUIV1_IN_GA(a(T249, T253), T7)
CNFEQUIV1_IN_GA(n(T263), T7) → U23_GA(T263, T7, transform29_in_ga(T263, X402))
CNFEQUIV1_IN_GA(n(T263), T7) → TRANSFORM29_IN_GA(T263, X402)
CNFEQUIV1_IN_GA(n(T263), T7) → U24_GA(T263, T7, transform29_in_ga(T263, T266))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → U25_GA(T263, T7, cnfequiv1_in_ga(n(T266), T7))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → CNFEQUIV1_IN_GA(n(T266), T7)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

The argument filtering Pi contains the following mapping:
cnfequiv1_in_ga(x1, x2) = cnfequiv1_in_ga(x1)
n(x1) = n(x1)
U6_ga(x1, x2, x3) = U6_ga(x3)
a(x1, x2) = a(x1, x2)
U7_ga(x1, x2, x3, x4) = U7_ga(x4)
o(x1, x2) = o(x1, x2)
U8_ga(x1, x2, x3, x4) = U8_ga(x4)
U9_ga(x1, x2, x3, x4, x5) = U9_ga(x5)
U10_ga(x1, x2, x3, x4, x5) = U10_ga(x5)
U11_ga(x1, x2, x3, x4) = U11_ga(x4)
transform29_in_ga(x1, x2) = transform29_in_ga(x1)
transform29_out_ga(x1, x2) = transform29_out_ga(x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x2, x4)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x4)
U5_ga(x1, x2, x3) = U5_ga(x3)
cnfequiv1_out_ga(x1, x2) = cnfequiv1_out_ga
U12_ga(x1, x2, x3, x4) = U12_ga(x2, x4)
U13_ga(x1, x2, x3, x4) = U13_ga(x4)
U14_ga(x1, x2, x3, x4) = U14_ga(x4)
U15_ga(x1, x2, x3, x4) = U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4) = U16_ga(x4)
U17_ga(x1, x2, x3, x4) = U17_ga(x4)
U18_ga(x1, x2, x3, x4) = U18_ga(x2, x4)
U19_ga(x1, x2, x3, x4) = U19_ga(x4)
U20_ga(x1, x2, x3, x4) = U20_ga(x4)
U21_ga(x1, x2, x3, x4) = U21_ga(x1, x4)
U22_ga(x1, x2, x3, x4) = U22_ga(x4)
U23_ga(x1, x2, x3) = U23_ga(x3)
U24_ga(x1, x2, x3) = U24_ga(x3)
U25_ga(x1, x2, x3) = U25_ga(x3)
CNFEQUIV1_IN_GA(x1, x2) = CNFEQUIV1_IN_GA(x1)
U6_GA(x1, x2, x3) = U6_GA(x3)
U7_GA(x1, x2, x3, x4) = U7_GA(x4)
U8_GA(x1, x2, x3, x4) = U8_GA(x4)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x5)
U10_GA(x1, x2, x3, x4, x5) = U10_GA(x5)
U11_GA(x1, x2, x3, x4) = U11_GA(x4)
TRANSFORM29_IN_GA(x1, x2) = TRANSFORM29_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x2, x4)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x2, x4)
U4_GA(x1, x2, x3, x4) = U4_GA(x1, x4)
U5_GA(x1, x2, x3) = U5_GA(x3)
U12_GA(x1, x2, x3, x4) = U12_GA(x2, x4)
U13_GA(x1, x2, x3, x4) = U13_GA(x4)
U14_GA(x1, x2, x3, x4) = U14_GA(x4)
U15_GA(x1, x2, x3, x4) = U15_GA(x1, x4)
U16_GA(x1, x2, x3, x4) = U16_GA(x4)
U17_GA(x1, x2, x3, x4) = U17_GA(x4)
U18_GA(x1, x2, x3, x4) = U18_GA(x2, x4)
U19_GA(x1, x2, x3, x4) = U19_GA(x4)
U20_GA(x1, x2, x3, x4) = U20_GA(x4)
U21_GA(x1, x2, x3, x4) = U21_GA(x1, x4)
U22_GA(x1, x2, x3, x4) = U22_GA(x4)
U23_GA(x1, x2, x3) = U23_GA(x3)
U24_GA(x1, x2, x3) = U24_GA(x3)
U25_GA(x1, x2, x3) = U25_GA(x3)

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

(6) Obligation:

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

CNFEQUIV1_IN_GA(n(n(T12)), T7) → U6_GA(T12, T7, cnfequiv1_in_ga(T12, T7))
CNFEQUIV1_IN_GA(n(n(T12)), T7) → CNFEQUIV1_IN_GA(T12, T7)
CNFEQUIV1_IN_GA(n(a(T23, T24)), T7) → U7_GA(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIV1_IN_GA(n(a(T23, T24)), T7) → CNFEQUIV1_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIV1_IN_GA(n(o(T36, T37)), T7) → U8_GA(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIV1_IN_GA(n(o(T36, T37)), T7) → CNFEQUIV1_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIV1_IN_GA(o(T53, a(T54, T55)), T7) → U9_GA(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIV1_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIV1_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIV1_IN_GA(o(a(T72, T73), T74), T7) → U10_GA(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIV1_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIV1_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIV1_IN_GA(o(T87, T88), T7) → U11_GA(T87, T88, T7, transform29_in_ga(T87, X108))
CNFEQUIV1_IN_GA(o(T87, T88), T7) → TRANSFORM29_IN_GA(T87, X108)
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → U1_GA(T157, T158, X201, transform29_in_ga(T157, X201))
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → TRANSFORM29_IN_GA(T157, X201)
TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → U2_GA(T169, T170, X226, transform29_in_ga(T170, X226))
TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → TRANSFORM29_IN_GA(T170, X226)
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → U3_GA(T181, T182, X251, transform29_in_ga(T181, X251))
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → TRANSFORM29_IN_GA(T181, X251)
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → U4_GA(T193, T194, X276, transform29_in_ga(T194, X276))
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → TRANSFORM29_IN_GA(T194, X276)
TRANSFORM29_IN_GA(n(T199), n(X290)) → U5_GA(T199, X290, transform29_in_ga(T199, X290))
TRANSFORM29_IN_GA(n(T199), n(X290)) → TRANSFORM29_IN_GA(T199, X290)
CNFEQUIV1_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transform29_in_ga(T87, T91))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_GA(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → CNFEQUIV1_IN_GA(o(T91, T88), T7)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U14_GA(T213, T214, T7, transform29_in_ga(T214, X317))
CNFEQUIV1_IN_GA(o(T213, T214), T7) → TRANSFORM29_IN_GA(T214, X317)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transform29_in_ga(T214, T217))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_GA(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → CNFEQUIV1_IN_GA(o(T213, T217), T7)
CNFEQUIV1_IN_GA(a(T231, T232), T7) → U17_GA(T231, T232, T7, transform29_in_ga(T231, X347))
CNFEQUIV1_IN_GA(a(T231, T232), T7) → TRANSFORM29_IN_GA(T231, X347)
CNFEQUIV1_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transform29_in_ga(T231, T235))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_GA(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → CNFEQUIV1_IN_GA(a(T235, T232), T7)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U20_GA(T249, T250, T7, transform29_in_ga(T250, X377))
CNFEQUIV1_IN_GA(a(T249, T250), T7) → TRANSFORM29_IN_GA(T250, X377)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transform29_in_ga(T250, T253))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_GA(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → CNFEQUIV1_IN_GA(a(T249, T253), T7)
CNFEQUIV1_IN_GA(n(T263), T7) → U23_GA(T263, T7, transform29_in_ga(T263, X402))
CNFEQUIV1_IN_GA(n(T263), T7) → TRANSFORM29_IN_GA(T263, X402)
CNFEQUIV1_IN_GA(n(T263), T7) → U24_GA(T263, T7, transform29_in_ga(T263, T266))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → U25_GA(T263, T7, cnfequiv1_in_ga(n(T266), T7))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → CNFEQUIV1_IN_GA(n(T266), T7)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → TRANSFORM29_IN_GA(T170, X226)
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → TRANSFORM29_IN_GA(T157, X201)
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → TRANSFORM29_IN_GA(T181, X251)
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → TRANSFORM29_IN_GA(T194, X276)
TRANSFORM29_IN_GA(n(T199), n(X290)) → TRANSFORM29_IN_GA(T199, X290)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

TRANSFORM29_IN_GA(o(T169, T170), o(T169, X226)) → TRANSFORM29_IN_GA(T170, X226)
TRANSFORM29_IN_GA(o(T157, T158), o(X201, T158)) → TRANSFORM29_IN_GA(T157, X201)
TRANSFORM29_IN_GA(a(T181, T182), a(X251, T182)) → TRANSFORM29_IN_GA(T181, X251)
TRANSFORM29_IN_GA(a(T193, T194), a(T193, X276)) → TRANSFORM29_IN_GA(T194, X276)
TRANSFORM29_IN_GA(n(T199), n(X290)) → TRANSFORM29_IN_GA(T199, X290)

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)
TRANSFORM29_IN_GA(x1, x2) = TRANSFORM29_IN_GA(x1)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

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

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

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

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

(15) YES

(16) Obligation:

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

CNFEQUIV1_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transform29_in_ga(T231, T235))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → CNFEQUIV1_IN_GA(a(T235, T232), T7)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transform29_in_ga(T250, T253))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → CNFEQUIV1_IN_GA(a(T249, T253), T7)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

CNFEQUIV1_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transform29_in_ga(T231, T235))
U18_GA(T231, T232, T7, transform29_out_ga(T231, T235)) → CNFEQUIV1_IN_GA(a(T235, T232), T7)
CNFEQUIV1_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transform29_in_ga(T250, T253))
U21_GA(T249, T250, T7, transform29_out_ga(T250, T253)) → CNFEQUIV1_IN_GA(a(T249, T253), T7)

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transform29_in_ga(x1, x2) = transform29_in_ga(x1)
transform29_out_ga(x1, x2) = transform29_out_ga(x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x2, x4)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x4)
U5_ga(x1, x2, x3) = U5_ga(x3)
CNFEQUIV1_IN_GA(x1, x2) = CNFEQUIV1_IN_GA(x1)
U18_GA(x1, x2, x3, x4) = U18_GA(x2, x4)
U21_GA(x1, x2, x3, x4) = U21_GA(x1, x4)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

CNFEQUIV1_IN_GA(a(T231, T232)) → U18_GA(T232, transform29_in_ga(T231))
U18_GA(T232, transform29_out_ga(T235)) → CNFEQUIV1_IN_GA(a(T235, T232))
CNFEQUIV1_IN_GA(a(T249, T250)) → U21_GA(T249, transform29_in_ga(T250))
U21_GA(T249, transform29_out_ga(T253)) → CNFEQUIV1_IN_GA(a(T249, T253))

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

CNFEQUIV1_IN_GA(a(T231, T232)) → U18_GA(T232, transform29_in_ga(T231))
U18_GA(T232, transform29_out_ga(T235)) → CNFEQUIV1_IN_GA(a(T235, T232))
CNFEQUIV1_IN_GA(a(T249, T250)) → U21_GA(T249, transform29_in_ga(T250))
U21_GA(T249, transform29_out_ga(T253)) → CNFEQUIV1_IN_GA(a(T249, T253))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIV1_IN_GA(x1) = CNFEQUIV1_IN_GA(x1)
a(x1, x2) = a(x1, x2)
U18_GA(x1, x2) = U18_GA(x1, x2)
transform29_in_ga(x1) = x1
transform29_out_ga(x1) = transform29_out_ga(x1)
U21_GA(x1, x2) = U21_GA(x1, x2)
n(x1) = n(x1)
o(x1, x2) = o(x1, x2)
U1_ga(x1, x2) = U1_ga(x1, x2)
U2_ga(x1, x2) = U2_ga(x1, x2)
U3_ga(x1, x2) = U3_ga(x1, x2)
U4_ga(x1, x2) = U4_ga(x1, x2)
U5_ga(x1) = U5_ga(x1)

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

[n₁, U5_ga₁] > [o₂, U1_ga₂, U2_ga₂] > [a₂, U18_GA₂, U21_GA₂, U3_ga₂, U4_ga₂] > transform29_{out_ga₁} > CNFEQUIV1_{IN_GA₁}

Status:

CNFEQUIV1_{IN_GA₁}: multiset
a₂: multiset
U18_GA₂: multiset
transform29_{out_ga₁}: [1]
U21_GA₂: multiset
n₁: [1]
o₂: [2,1]
U1_ga₂: [1,2]
U2_ga₂: [2,1]
U3_ga₂: multiset
U4_ga₂: multiset
U5_ga₁: [1]

The following usable rules [FROCOS05] were oriented:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

(22) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(23) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(24) YES

(25) Obligation:

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

CNFEQUIV1_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transform29_in_ga(T87, T91))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → CNFEQUIV1_IN_GA(o(T91, T88), T7)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transform29_in_ga(T214, T217))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → CNFEQUIV1_IN_GA(o(T213, T217), T7)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

(26) UsableRulesProof (EQUIVALENT transformation)

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

(27) Obligation:

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

CNFEQUIV1_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transform29_in_ga(T87, T91))
U12_GA(T87, T88, T7, transform29_out_ga(T87, T91)) → CNFEQUIV1_IN_GA(o(T91, T88), T7)
CNFEQUIV1_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transform29_in_ga(T214, T217))
U15_GA(T213, T214, T7, transform29_out_ga(T214, T217)) → CNFEQUIV1_IN_GA(o(T213, T217), T7)

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transform29_in_ga(x1, x2) = transform29_in_ga(x1)
transform29_out_ga(x1, x2) = transform29_out_ga(x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x2, x4)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x4)
U5_ga(x1, x2, x3) = U5_ga(x3)
CNFEQUIV1_IN_GA(x1, x2) = CNFEQUIV1_IN_GA(x1)
U12_GA(x1, x2, x3, x4) = U12_GA(x2, x4)
U15_GA(x1, x2, x3, x4) = U15_GA(x1, x4)

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

(28) PiDPToQDPProof (SOUND transformation)

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

(29) Obligation:

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

CNFEQUIV1_IN_GA(o(T87, T88)) → U12_GA(T88, transform29_in_ga(T87))
U12_GA(T88, transform29_out_ga(T91)) → CNFEQUIV1_IN_GA(o(T91, T88))
CNFEQUIV1_IN_GA(o(T213, T214)) → U15_GA(T213, transform29_in_ga(T214))
U15_GA(T213, transform29_out_ga(T217)) → CNFEQUIV1_IN_GA(o(T213, T217))

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U12_GA(T88, transform29_out_ga(T91)) → CNFEQUIV1_IN_GA(o(T91, T88))
U15_GA(T213, transform29_out_ga(T217)) → CNFEQUIV1_IN_GA(o(T213, T217))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIV1_IN_GA(x1) = x1
o(x1, x2) = o(x1, x2)
U12_GA(x1, x2) = U12_GA(x1, x2)
transform29_in_ga(x1) = x1
transform29_out_ga(x1) = transform29_out_ga(x1)
U15_GA(x1, x2) = U15_GA(x1, x2)
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
U1_ga(x1, x2) = U1_ga(x1, x2)
U2_ga(x1, x2) = U2_ga(x1, x2)
U3_ga(x1, x2) = U3_ga(x1, x2)
U4_ga(x1, x2) = U4_ga(x1, x2)
U5_ga(x1) = U5_ga(x1)

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

[n₁, U5_ga₁] > [o₂, U12_GA₂, U15_GA₂, U1_ga₂, U2_ga₂] > [a₂, U3_ga₂, U4_ga₂] > transform29_{out_ga₁}

Status:

o₂: multiset
U12_GA₂: multiset
transform29_{out_ga₁}: multiset
U15_GA₂: multiset
n₁: [1]
a₂: multiset
U1_ga₂: multiset
U2_ga₂: multiset
U3_ga₂: multiset
U4_ga₂: multiset
U5_ga₁: [1]

The following usable rules [FROCOS05] were oriented:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

(31) Obligation:

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

CNFEQUIV1_IN_GA(o(T87, T88)) → U12_GA(T88, transform29_in_ga(T87))
CNFEQUIV1_IN_GA(o(T213, T214)) → U15_GA(T213, transform29_in_ga(T214))

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

(34) Obligation:

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

CNFEQUIV1_IN_GA(n(T263), T7) → U24_GA(T263, T7, transform29_in_ga(T263, T266))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → CNFEQUIV1_IN_GA(n(T266), T7)
CNFEQUIV1_IN_GA(n(n(T12)), T7) → CNFEQUIV1_IN_GA(T12, T7)

The TRS R consists of the following rules:

cnfequiv1_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequiv1_in_ga(T12, T7))
cnfequiv1_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequiv1_in_ga(o(n(T23), n(T24)), T7))
cnfequiv1_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequiv1_in_ga(a(n(T36), n(T37)), T7))
cnfequiv1_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequiv1_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequiv1_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequiv1_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequiv1_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transform29_in_ga(T87, X108))
transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U11_ga(T87, T88, T7, transform29_out_ga(T87, X108)) → cnfequiv1_out_ga(o(T87, T88), T7)
cnfequiv1_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transform29_in_ga(T87, T91))
U12_ga(T87, T88, T7, transform29_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequiv1_in_ga(o(T91, T88), T7))
cnfequiv1_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transform29_in_ga(T214, X317))
U14_ga(T213, T214, T7, transform29_out_ga(T214, X317)) → cnfequiv1_out_ga(o(T213, T214), T7)
cnfequiv1_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transform29_in_ga(T214, T217))
U15_ga(T213, T214, T7, transform29_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequiv1_in_ga(o(T213, T217), T7))
cnfequiv1_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transform29_in_ga(T231, X347))
U17_ga(T231, T232, T7, transform29_out_ga(T231, X347)) → cnfequiv1_out_ga(a(T231, T232), T7)
cnfequiv1_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transform29_in_ga(T231, T235))
U18_ga(T231, T232, T7, transform29_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequiv1_in_ga(a(T235, T232), T7))
cnfequiv1_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transform29_in_ga(T250, X377))
U20_ga(T249, T250, T7, transform29_out_ga(T250, X377)) → cnfequiv1_out_ga(a(T249, T250), T7)
cnfequiv1_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transform29_in_ga(T250, T253))
U21_ga(T249, T250, T7, transform29_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequiv1_in_ga(a(T249, T253), T7))
cnfequiv1_in_ga(n(T263), T7) → U23_ga(T263, T7, transform29_in_ga(T263, X402))
U23_ga(T263, T7, transform29_out_ga(T263, X402)) → cnfequiv1_out_ga(n(T263), T7)
cnfequiv1_in_ga(n(T263), T7) → U24_ga(T263, T7, transform29_in_ga(T263, T266))
U24_ga(T263, T7, transform29_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequiv1_in_ga(n(T266), T7))
cnfequiv1_in_ga(T273, T273) → cnfequiv1_out_ga(T273, T273)
U25_ga(T263, T7, cnfequiv1_out_ga(n(T266), T7)) → cnfequiv1_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequiv1_out_ga(a(T249, T253), T7)) → cnfequiv1_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequiv1_out_ga(a(T235, T232), T7)) → cnfequiv1_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequiv1_out_ga(o(T213, T217), T7)) → cnfequiv1_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequiv1_out_ga(o(T91, T88), T7)) → cnfequiv1_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequiv1_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequiv1_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequiv1_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequiv1_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequiv1_out_ga(a(n(T36), n(T37)), T7)) → cnfequiv1_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequiv1_out_ga(o(n(T23), n(T24)), T7)) → cnfequiv1_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequiv1_out_ga(T12, T7)) → cnfequiv1_out_ga(n(n(T12)), T7)

(35) UsableRulesProof (EQUIVALENT transformation)

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

(36) Obligation:

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

CNFEQUIV1_IN_GA(n(T263), T7) → U24_GA(T263, T7, transform29_in_ga(T263, T266))
U24_GA(T263, T7, transform29_out_ga(T263, T266)) → CNFEQUIV1_IN_GA(n(T266), T7)
CNFEQUIV1_IN_GA(n(n(T12)), T7) → CNFEQUIV1_IN_GA(T12, T7)

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98)), T98) → transform29_out_ga(n(n(T98)), T98)
transform29_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transform29_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transform29_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transform29_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transform29_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158), o(X201, T158)) → U1_ga(T157, T158, X201, transform29_in_ga(T157, X201))
transform29_in_ga(o(T169, T170), o(T169, X226)) → U2_ga(T169, T170, X226, transform29_in_ga(T170, X226))
transform29_in_ga(a(T181, T182), a(X251, T182)) → U3_ga(T181, T182, X251, transform29_in_ga(T181, X251))
transform29_in_ga(a(T193, T194), a(T193, X276)) → U4_ga(T193, T194, X276, transform29_in_ga(T194, X276))
transform29_in_ga(n(T199), n(X290)) → U5_ga(T199, X290, transform29_in_ga(T199, X290))
U1_ga(T157, T158, X201, transform29_out_ga(T157, X201)) → transform29_out_ga(o(T157, T158), o(X201, T158))
U2_ga(T169, T170, X226, transform29_out_ga(T170, X226)) → transform29_out_ga(o(T169, T170), o(T169, X226))
U3_ga(T181, T182, X251, transform29_out_ga(T181, X251)) → transform29_out_ga(a(T181, T182), a(X251, T182))
U4_ga(T193, T194, X276, transform29_out_ga(T194, X276)) → transform29_out_ga(a(T193, T194), a(T193, X276))
U5_ga(T199, X290, transform29_out_ga(T199, X290)) → transform29_out_ga(n(T199), n(X290))

The argument filtering Pi contains the following mapping:
n(x1) = n(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
transform29_in_ga(x1, x2) = transform29_in_ga(x1)
transform29_out_ga(x1, x2) = transform29_out_ga(x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x2, x4)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x4)
U5_ga(x1, x2, x3) = U5_ga(x3)
CNFEQUIV1_IN_GA(x1, x2) = CNFEQUIV1_IN_GA(x1)
U24_GA(x1, x2, x3) = U24_GA(x3)

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

(37) PiDPToQDPProof (SOUND transformation)

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

(38) Obligation:

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

CNFEQUIV1_IN_GA(n(T263)) → U24_GA(transform29_in_ga(T263))
U24_GA(transform29_out_ga(T266)) → CNFEQUIV1_IN_GA(n(T266))
CNFEQUIV1_IN_GA(n(n(T12))) → CNFEQUIV1_IN_GA(T12)

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(39) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

CNFEQUIV1_IN_GA(n(n(T12))) → CNFEQUIV1_IN_GA(T12)

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

POL(CNFEQUIV1_IN_GA(x₁)) = x₁
POL(U1_ga(x₁, x₂)) = 0
POL(U24_GA(x₁)) = 1 + x₁
POL(U2_ga(x₁, x₂)) = 0
POL(U3_ga(x₁, x₂)) = 0
POL(U4_ga(x₁, x₂)) = 0
POL(U5_ga(x₁)) = 1 + x₁
POL(a(x₁, x₂)) = 0
POL(n(x₁)) = 1 + x₁
POL(o(x₁, x₂)) = 0
POL(transform29_in_ga(x₁)) = x₁
POL(transform29_out_ga(x₁)) = x₁

The following usable rules [FROCOS05] were oriented:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

(40) Obligation:

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

CNFEQUIV1_IN_GA(n(T263)) → U24_GA(transform29_in_ga(T263))
U24_GA(transform29_out_ga(T266)) → CNFEQUIV1_IN_GA(n(T266))

The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(41) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

CNFEQUIV1_IN_GA(n(T263)) → U24_GA(transform29_in_ga(T263))
U24_GA(transform29_out_ga(T266)) → CNFEQUIV1_IN_GA(n(T266))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIV1_IN_GA(x1) = CNFEQUIV1_IN_GA(x1)
n(x1) = n(x1)
U24_GA(x1) = U24_GA(x1)
transform29_in_ga(x1) = x1
transform29_out_ga(x1) = transform29_out_ga(x1)
a(x1, x2) = a(x1, x2)
o(x1, x2) = o(x1, x2)
U1_ga(x1, x2) = U1_ga(x1, x2)
U2_ga(x1, x2) = U2_ga(x1, x2)
U3_ga(x1, x2) = U3_ga(x1, x2)
U4_ga(x1, x2) = U4_ga(x1, x2)
U5_ga(x1) = U5_ga(x1)

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

[n₁, U24_GA₁, U5_ga₁] > [o₂, U1_ga₂, U2_ga₂] > [a₂, U3_ga₂, U4_ga₂] > [CNFEQUIV1_{IN_GA₁}, transform29_{out_ga₁}]

Status:

CNFEQUIV1_{IN_GA₁}: multiset
n₁: [1]
U24_GA₁: [1]
transform29_{out_ga₁}: multiset
a₂: multiset
o₂: [2,1]
U1_ga₂: [1,2]
U2_ga₂: [2,1]
U3_ga₂: multiset
U4_ga₂: multiset
U5_ga₁: [1]

The following usable rules [FROCOS05] were oriented:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

(42) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

transform29_in_ga(n(n(T98))) → transform29_out_ga(T98)
transform29_in_ga(n(a(T107, T108))) → transform29_out_ga(o(n(T107), n(T108)))
transform29_in_ga(n(o(T117, T118))) → transform29_out_ga(a(n(T117), n(T118)))
transform29_in_ga(o(T131, a(T132, T133))) → transform29_out_ga(a(o(T131, T132), o(T131, T133)))
transform29_in_ga(o(a(T146, T147), T148)) → transform29_out_ga(a(o(T146, T148), o(T147, T148)))
transform29_in_ga(o(T157, T158)) → U1_ga(T158, transform29_in_ga(T157))
transform29_in_ga(o(T169, T170)) → U2_ga(T169, transform29_in_ga(T170))
transform29_in_ga(a(T181, T182)) → U3_ga(T182, transform29_in_ga(T181))
transform29_in_ga(a(T193, T194)) → U4_ga(T193, transform29_in_ga(T194))
transform29_in_ga(n(T199)) → U5_ga(transform29_in_ga(T199))
U1_ga(T158, transform29_out_ga(X201)) → transform29_out_ga(o(X201, T158))
U2_ga(T169, transform29_out_ga(X226)) → transform29_out_ga(o(T169, X226))
U3_ga(T182, transform29_out_ga(X251)) → transform29_out_ga(a(X251, T182))
U4_ga(T193, transform29_out_ga(X276)) → transform29_out_ga(a(T193, X276))
U5_ga(transform29_out_ga(X290)) → transform29_out_ga(n(X290))

The set Q consists of the following terms:

transform29_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)

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

(43) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) PisEmptyProof (EQUIVALENT transformation)

(24) YES

(25) Obligation:

(26) UsableRulesProof (EQUIVALENT transformation)

(27) Obligation:

(28) PiDPToQDPProof (SOUND transformation)

(29) Obligation:

(30) QDPOrderProof (EQUIVALENT transformation)

(31) Obligation:

(32) DependencyGraphProof (EQUIVALENT transformation)

(33) TRUE

(34) Obligation:

(35) UsableRulesProof (EQUIVALENT transformation)

(36) Obligation:

(37) PiDPToQDPProof (SOUND transformation)

(38) Obligation:

(39) QDPOrderProof (EQUIVALENT transformation)

(40) Obligation:

(41) QDPOrderProof (EQUIVALENT transformation)

(42) Obligation:

(43) PisEmptyProof (EQUIVALENT transformation)

(44) YES