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

(0) Obligation:

Clauses:

p(X) :- ','(q(X), r(X)).
p(X) :- =(X, 2).
q(X) :- ','(=(X, 1), !).
q(X) :- =(X, 3).
r(X) :- ','(=(X, 1), !).
r(X) :- =(X, 4).
=(X, X).

Query: p(a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

p(X) :- ','(q(X), r(X)).
p(X) :- user_defined_=(X, 2).
q(X) :- ','(user_defined_=(X, 1), !).
q(X) :- user_defined_=(X, 3).
r(X) :- ','(user_defined_=(X, 1), !).
r(X) :- user_defined_=(X, 4).
user_defined_=(X, X).

Query: p(a)

(3) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: p(T1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: p(T1), SCOPE: 1, CLAUSE: 0 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(q(T4), r(T4)) | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 2 | ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(','(user_defined_=(T9, 1), !_2), r(T9)) | ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(','(user_defined_=(T9, 1), !_2), r(T9)), SCOPE: 3, CLAUSE: 6 | ?_3 | ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(!_2, r(1)) | ?_3 | ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_3 | ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: r(1) | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: r(1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: r(1), SCOPE: 4, CLAUSE: 4 | r(1), SCOPE: 4, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(user_defined_=(1, 1), !_4) | r(1), SCOPE: 4, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(user_defined_=(1, 1), !_4), SCOPE: 5, CLAUSE: 6 | ?_5 | r(1), SCOPE: 4, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: !_4 | ?_5 | r(1), SCOPE: 4, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: user_defined_=(T17, 2)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: user_defined_=(T17, 2), SCOPE: 6, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3 | ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(q(T4), r(T4)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_2 | p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(user_defined_=(T28, 3), r(T28))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(user_defined_=(T28, 3), r(T28)), SCOPE: 7, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: r(3)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: r(3), SCOPE: 8, CLAUSE: 4 | r(3), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(user_defined_=(3, 1), !_8) | r(3), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(user_defined_=(3, 1), !_8), SCOPE: 9, CLAUSE: 6 | ?_9 | r(3), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ?_9 | r(3), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: r(3), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: user_defined_=(3, 4)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: user_defined_=(3, 4), SCOPE: 10, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: p(T1), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: user_defined_=(T36, 2)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: user_defined_=(T36, 2), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 119 [arrowhead = none ];
119 -> 6;

120 [label="ONLY EVAL with clause\np(X2) :- ','(q(X2), r(X2)).\nand substitutionT1 -> T4,\nX2 -> T4,\nT3 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 120 [arrowhead = none ];
120 -> 7;

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

122 [label="ONLY EVAL with clause\nq(X5) :- ','(user_defined_=(X5, 1), !_2).\nand substitutionT4 -> T9,\nX5 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 122 [arrowhead = none ];
122 -> 13;

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

124 [label="EVAL with clause\nuser_defined_=(X8, X8).\nand substitutionT9 -> 1,\nX8 -> 1,\nT12 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 124 [arrowhead = none ];
124 -> 17;

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

126 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 126 [arrowhead = none ];
126 -> 21;

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

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

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

130 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 130 [arrowhead = none ];
130 -> 28;

131 [label="ONLY EVAL with clause\np(X17) :- user_defined_=(X17, 2).\nand substitutionT1 -> T17,\nX17 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 131 [arrowhead = none ];
131 -> 46;

132 [label="ONLY EVAL with clause\nr(X11) :- ','(user_defined_=(X11, 1), !_4).\nand substitutionX11 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 132 [arrowhead = none ];
132 -> 30;

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

134 [label="ONLY EVAL with clause\nuser_defined_=(X14, X14).\nand substitutionX14 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 134 [arrowhead = none ];
134 -> 34;

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

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

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

138 [label="EVAL with clause\nuser_defined_=(X20, X20).\nand substitutionT17 -> 2,\nX20 -> 2,\nT20 -> 2", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 138 [arrowhead = none ];
138 -> 51;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 139 [arrowhead = none ];
139 -> 53;

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

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

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

143 [label="ONLY EVAL with clause\nq(X25) :- user_defined_=(X25, 3).\nand substitutionT4 -> T28,\nX25 -> T28,\nT27 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 143 [arrowhead = none ];
143 -> 68;

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

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

146 [label="EVAL with clause\nuser_defined_=(X28, X28).\nand substitutionT28 -> 3,\nX28 -> 3,\nT31 -> 3", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 146 [arrowhead = none ];
146 -> 74;

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

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

149 [label="ONLY EVAL with clause\nr(X31) :- ','(user_defined_=(X31, 1), !_8).\nand substitutionX31 -> 3", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 149 [arrowhead = none ];
149 -> 79;

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

151 [label="BACKTRACK\nfor clause: user_defined_=(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 151 [arrowhead = none ];
151 -> 82;

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

153 [label="ONLY EVAL with clause\nr(X35) :- user_defined_=(X35, 4).\nand substitutionX35 -> 3", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 153 [arrowhead = none ];
153 -> 92;

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

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

156 [label="ONLY EVAL with clause\np(X39) :- user_defined_=(X39, 2).\nand substitutionT1 -> T36,\nX39 -> T36,\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 156 [arrowhead = none ];
156 -> 109;

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

158 [label="EVAL with clause\nuser_defined_=(X42, X42).\nand substitutionT36 -> 2,\nX42 -> 2,\nT39 -> 2", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 158 [arrowhead = none ];
158 -> 116;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 159 [arrowhead = none ];
159 -> 117;

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

}

(4) Obligation:

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

pA_in_a(1) → pA_out_a(1)
pA_in_a(2) → pA_out_a(2)

The argument filtering Pi contains the following mapping:
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a(x1)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

pA_in_a(1) → pA_out_a(1)
pA_in_a(2) → pA_out_a(2)

The argument filtering Pi contains the following mapping:
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a(x1)

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

(6) Obligation:

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

pA_in_a(1) → pA_out_a(1)
pA_in_a(2) → pA_out_a(2)

The argument filtering Pi contains the following mapping:
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a(x1)

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

(7) PisEmptyProof (EQUIVALENT transformation)

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

(8) YES