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

(0) Obligation:

Clauses:

p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).

Query: p(a,a,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

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

(2) Obligation:

Clauses:

p(X, Y, Z) :- ','(user_defined_=(X, Y), ','(user_defined_=(Z, 1), !)).
p(X, Y, Z) :- ','(user_defined_=(Z, 1), ','(user_defined_=(Y, X), p(X, Y, Z))).
user_defined_=(X, X).

Query: p(a,a,a)

(3) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: p(T1, T2, T3)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: p(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(user_defined_=(T16, T17), ','(user_defined_=(T18, 1), !_1)) | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(user_defined_=(T16, T17), ','(user_defined_=(T18, 1), !_1)), SCOPE: 2, CLAUSE: 2 | ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(user_defined_=(T22, 1), !_1) | ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(user_defined_=(T22, 1), !_1), SCOPE: 3, CLAUSE: 2 | ?_3 | ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: !_1 | ?_3 | ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ?_3 | ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ?_2 | p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(user_defined_=(T41, 1), ','(user_defined_=(T42, T43), p(T43, T42, T41)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(user_defined_=(T41, 1), ','(user_defined_=(T42, T43), p(T43, T42, T41))), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(user_defined_=(T50, T51), p(T51, T50, 1))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(user_defined_=(T50, T51), p(T51, T50, 1)), SCOPE: 5, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: p(T57, T57, 1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: p(T57, T57, 1), SCOPE: 6, CLAUSE: 0 | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(user_defined_=(T63, T63), ','(user_defined_=(1, 1), !_6)) | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(user_defined_=(T63, T63), ','(user_defined_=(1, 1), !_6)), SCOPE: 7, CLAUSE: 2 | ?_7 | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(user_defined_=(1, 1), !_6) | ?_7 | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(user_defined_=(1, 1), !_6), SCOPE: 8, CLAUSE: 2 | ?_8 | ?_7 | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: !_6 | ?_8 | ?_7 | p(T57, T57, 1), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: p(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(user_defined_=(T82, 1), ','(user_defined_=(T83, T84), p(T84, T83, T82)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(user_defined_=(T82, 1), ','(user_defined_=(T83, T84), p(T84, T83, T82))), SCOPE: 9, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(user_defined_=(T91, T92), p(T92, T91, 1))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(user_defined_=(T91, T92), p(T92, T91, 1)), SCOPE: 10, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: p(T98, T98, 1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 93 [arrowhead = none ];
93 -> 6;

94 [label="ONLY EVAL with clause\np(X7, X8, X9) :- ','(user_defined_=(X7, X8), ','(user_defined_=(X9, 1), !_1)).\nand substitutionT1 -> T16,\nX7 -> T16,\nT2 -> T17,\nX8 -> T17,\nT3 -> T18,\nX9 -> T18,\nT13 -> T16,\nT14 -> T17,\nT15 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 94 [arrowhead = none ];
94 -> 9;

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

96 [label="EVAL with clause\nuser_defined_=(X12, X12).\nand substitutionT16 -> T21,\nX12 -> T21,\nT17 -> T21,\nT18 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 96 [arrowhead = none ];
96 -> 15;

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

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

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

100 [label="EVAL with clause\nuser_defined_=(X15, X15).\nand substitutionT22 -> 1,\nX15 -> 1,\nT25 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 100 [arrowhead = none ];
100 -> 24;

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

102 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 102 [arrowhead = none ];
102 -> 29;

103 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 103 [arrowhead = none ];
103 -> 35;

104 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 104 [arrowhead = none ];
104 -> 32;

105 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 105 [arrowhead = none ];
105 -> 38;

106 [label="ONLY EVAL with clause\np(X25, X26, X27) :- ','(user_defined_=(X27, 1), ','(user_defined_=(X26, X25), p(X25, X26, X27))).\nand substitutionT1 -> T43,\nX25 -> T43,\nT2 -> T42,\nX26 -> T42,\nT3 -> T41,\nX27 -> T41,\nT40 -> T41,\nT39 -> T42,\nT38 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 106 [arrowhead = none ];
106 -> 41;

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

108 [label="EVAL with clause\nuser_defined_=(X33, X33).\nand substitutionT41 -> 1,\nX33 -> 1,\nT49 -> 1,\nT42 -> T50,\nT43 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 108 [arrowhead = none ];
108 -> 47;

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

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

111 [label="EVAL with clause\nuser_defined_=(X39, X39).\nand substitutionT50 -> T57,\nX39 -> T57,\nT51 -> T57,\nT56 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 111 [arrowhead = none ];
111 -> 56;

112 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 112 [arrowhead = none ];
112 -> 57;

113 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 113 [arrowhead = none ];
113 -> 60;

114 [label="ONLY EVAL with clause\np(X49, X50, X51) :- ','(user_defined_=(X49, X50), ','(user_defined_=(X51, 1), !_6)).\nand substitutionT57 -> T63,\nX49 -> T63,\nX50 -> T63,\nX51 -> 1,\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 114 [arrowhead = none ];
114 -> 64;

115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
64 -> 115 [arrowhead = none ];
115 -> 66;

116 [label="ONLY EVAL with clause\nuser_defined_=(X54, X54).\nand substitutionT63 -> T66,\nX54 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 116 [arrowhead = none ];
116 -> 68;

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

118 [label="ONLY EVAL with clause\nuser_defined_=(X57, X57).\nand substitutionX57 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 118 [arrowhead = none ];
118 -> 70;

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

120 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 120 [arrowhead = none ];
120 -> 72;

121 [label="ONLY EVAL with clause\np(X67, X68, X69) :- ','(user_defined_=(X69, 1), ','(user_defined_=(X68, X67), p(X67, X68, X69))).\nand substitutionT1 -> T84,\nX67 -> T84,\nT2 -> T83,\nX68 -> T83,\nT3 -> T82,\nX69 -> T82,\nT81 -> T82,\nT80 -> T83,\nT79 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 121 [arrowhead = none ];
121 -> 80;

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

123 [label="EVAL with clause\nuser_defined_=(X75, X75).\nand substitutionT82 -> 1,\nX75 -> 1,\nT90 -> 1,\nT83 -> T91,\nT84 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 123 [arrowhead = none ];
123 -> 86;

124 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 124 [arrowhead = none ];
124 -> 87;

125 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
86 -> 125 [arrowhead = none ];
125 -> 88;

126 [label="EVAL with clause\nuser_defined_=(X81, X81).\nand substitutionT91 -> T98,\nX81 -> T98,\nT92 -> T98,\nT97 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 126 [arrowhead = none ];
126 -> 91;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 127 [arrowhead = none ];
127 -> 92;

128 [label="INSTANCE with matching:\nT57 -> T98", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 128 [arrowhead = none , style=dashed];
128 -> 56[style=dashed];

}

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f3_in → f3_out1(1)
f3_in → U1(f56_in)
U1(f56_out1) → f3_out1(1)
f3_in → U2(f56_in)
U2(f56_out1) → f3_out1(1)
f56_in → f56_out1

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:

f3_in > U2₁ > f56_in > f56_out1 > U1₁ > 1 > f3_out11

and weight map:

f3_in=3
1=2
f56_in=1
f56_out1=1
f3_out1_1=1
U1_1=2
U2_1=2

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f3_in → f3_out1(1)
f3_in → U1(f56_in)
U1(f56_out1) → f3_out1(1)
f3_in → U2(f56_in)
U2(f56_out1) → f3_out1(1)
f56_in → f56_out1

(6) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) YES