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

(0) Obligation:

Clauses:

dis(or(B1, B2)) :- ','(con(B1), dis(B2)).
dis(B) :- con(B).
con(and(B1, B2)) :- ','(dis(B1), con(B2)).
con(B) :- bool(B).
bool(0).
bool(1).

Query: con(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: con(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: con(T1), SCOPE: 1, CLAUSE: 2 | con(T1), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(dis(T4), con(T5)) | con(and(T4, T5)), SCOPE: 1, CLAUSE: 3\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: con(T1), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nX3 is free\nX4 is free\ncon(T1) !=? con(and(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(dis(T4), con(T5)), SCOPE: 2, CLAUSE: 0 | ','(dis(T4), con(T5)), SCOPE: 2, CLAUSE: 1 | ?_2 | con(and(T4, T5)), SCOPE: 1, CLAUSE: 3\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(dis(T4), con(T5)), SCOPE: 2, CLAUSE: 0\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(dis(T4), con(T5)), SCOPE: 2, CLAUSE: 1 | ?_2 | con(and(T4, T5)), SCOPE: 1, CLAUSE: 3\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="B: ','(','(con(T14), dis(T15)), con(T5))\n\nT5 is ground\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: con(T14)\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="F: ','(dis(T15), con(T5))\n\nT5 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="D: dis(T15)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: con(T5)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: dis(T15), SCOPE: 3, CLAUSE: 0 | dis(T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: dis(T15), SCOPE: 3, CLAUSE: 0\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: dis(T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="E: ','(con(T32), dis(T33))\n\nT32 is ground\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: con(T32)\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: dis(T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: con(T44)\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(dis(T4), con(T5)), SCOPE: 2, CLAUSE: 1\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ?_2 | con(and(T4, T5)), SCOPE: 1, CLAUSE: 3\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="C: ','(con(T57), con(T5))\n\nT5 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: con(T57)\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: con(T5)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: con(and(T4, T5)), SCOPE: 1, CLAUSE: 3\n\nT4 is ground\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: bool(and(T68, T69))\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: bool(and(T68, T69)), SCOPE: 4, CLAUSE: 4 | bool(and(T68, T69)), SCOPE: 4, CLAUSE: 5\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: bool(and(T68, T69)), SCOPE: 4, CLAUSE: 5\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: bool(T71)\n\nT71 is ground\nX3 is free\nX4 is free\ncon(T71) !=? con(and(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: bool(T71), SCOPE: 5, CLAUSE: 4 | bool(T71), SCOPE: 5, CLAUSE: 5\n\nT71 is ground\nX3 is free\nX4 is free\ncon(T71) !=? con(and(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: bool(T71), SCOPE: 5, CLAUSE: 4\n\nT71 is ground\nX3 is free\nX4 is free\ncon(T71) !=? con(and(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: bool(T71), SCOPE: 5, CLAUSE: 5\n\nT71 is ground\nX3 is free\nX4 is free\ncon(T71) !=? con(and(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 107 [arrowhead = none ];
107 -> 6;

108 [label="EVAL with clause\ncon(and(X3, X4)) :- ','(dis(X3), con(X4)).\nand substitutionX3 -> T4,\nX4 -> T5,\nT1 -> and(T4, T5)", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 108 [arrowhead = none ];
108 -> 10;

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

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

111 [label="ONLY EVAL with clause\ncon(X67) :- bool(X67).\nand substitutionT1 -> T71,\nX67 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 111 [arrowhead = none ];
111 -> 89;

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

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

114 [label="EVAL with clause\ndis(or(X13, X14)) :- ','(con(X13), dis(X14)).\nand substitutionX13 -> T14,\nX14 -> T15,\nT4 -> or(T14, T15)", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 114 [arrowhead = none ];
114 -> 21;

115 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 115 [arrowhead = none ];
115 -> 23;

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

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

118 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
21 -> 118 [arrowhead = none ];
118 -> 28;

119 [label="SPLIT 2\nnew knowledge:\nT14 is ground", fontsize=14, style = filled, fillcolor = violet];
21 -> 119 [arrowhead = none ];
119 -> 30;

120 [label="INSTANCE with matching:\nT1 -> T14", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 120 [arrowhead = none , style=dashed];
120 -> 3[style=dashed];

121 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 121 [arrowhead = none ];
121 -> 37;

122 [label="SPLIT 2\nnew knowledge:\nT15 is ground", fontsize=14, style = filled, fillcolor = violet];
30 -> 122 [arrowhead = none ];
122 -> 39;

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

124 [label="INSTANCE with matching:\nT1 -> T5", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 124 [arrowhead = none , style=dashed];
124 -> 3[style=dashed];

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

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

127 [label="EVAL with clause\ndis(or(X31, X32)) :- ','(con(X31), dis(X32)).\nand substitutionX31 -> T32,\nX32 -> T33,\nT15 -> or(T32, T33)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 127 [arrowhead = none ];
127 -> 48;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 128 [arrowhead = none ];
128 -> 50;

129 [label="ONLY EVAL with clause\ndis(X43) :- con(X43).\nand substitutionT15 -> T44,\nX43 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 129 [arrowhead = none ];
129 -> 57;

130 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
48 -> 130 [arrowhead = none ];
130 -> 52;

131 [label="SPLIT 2\nnew knowledge:\nT32 is ground", fontsize=14, style = filled, fillcolor = violet];
48 -> 131 [arrowhead = none ];
131 -> 53;

132 [label="INSTANCE with matching:\nT1 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 132 [arrowhead = none , style=dashed];
132 -> 3[style=dashed];

133 [label="INSTANCE with matching:\nT15 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 133 [arrowhead = none , style=dashed];
133 -> 37[style=dashed];

134 [label="INSTANCE with matching:\nT1 -> T44", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 134 [arrowhead = none , style=dashed];
134 -> 3[style=dashed];

135 [label="ONLY EVAL with clause\ndis(X56) :- con(X56).\nand substitutionT4 -> T57,\nX56 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 135 [arrowhead = none ];
135 -> 63;

136 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 136 [arrowhead = none ];
136 -> 77;

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

138 [label="SPLIT 2\nnew knowledge:\nT57 is ground", fontsize=14, style = filled, fillcolor = violet];
63 -> 138 [arrowhead = none ];
138 -> 66;

139 [label="INSTANCE with matching:\nT1 -> T57", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 139 [arrowhead = none , style=dashed];
139 -> 3[style=dashed];

140 [label="INSTANCE with matching:\nT1 -> T5", fontsize=14, style = filled, fillcolor = lightgrey];
66 -> 140 [arrowhead = none , style=dashed];
140 -> 3[style=dashed];

141 [label="ONLY EVAL with clause\ncon(X65) :- bool(X65).\nand substitutionT4 -> T68,\nT5 -> T69,\nX65 -> and(T68, T69)", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 141 [arrowhead = none ];
141 -> 81;

142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
81 -> 142 [arrowhead = none ];
142 -> 82;

143 [label="BACKTRACK\nfor clause: bool(0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 143 [arrowhead = none ];
143 -> 83;

144 [label="BACKTRACK\nfor clause: bool(1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 144 [arrowhead = none ];
144 -> 85;

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

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

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

148 [label="EVAL with clause\nbool(0).\nand substitutionT71 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 148 [arrowhead = none ];
148 -> 97;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 149 [arrowhead = none ];
149 -> 98;

150 [label="EVAL with clause\nbool(1).\nand substitutionT71 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 150 [arrowhead = none ];
150 -> 103;

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

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

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

}

(2) Obligation:

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

conA_in_g(and(or(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U5_ggg(T14, T15, T5, conA_in_g(T14))
conA_in_g(and(T57, T5)) → U2_g(T57, T5, pC_in_gg(T57, T5))
pC_in_gg(T57, T5) → U11_gg(T57, T5, conA_in_g(T57))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U11_gg(T57, T5, conA_out_g(T57)) → U12_gg(T57, T5, conA_in_g(T5))
U12_gg(T57, T5, conA_out_g(T5)) → pC_out_gg(T57, T5)
U2_g(T57, T5, pC_out_gg(T57, T5)) → conA_out_g(and(T57, T5))
U5_ggg(T14, T15, T5, conA_out_g(T14)) → U6_ggg(T14, T15, T5, pF_in_gg(T15, T5))
pF_in_gg(T15, T5) → U7_gg(T15, T5, disD_in_g(T15))
disD_in_g(or(T32, T33)) → U3_g(T32, T33, pE_in_gg(T32, T33))
pE_in_gg(T32, T33) → U9_gg(T32, T33, conA_in_g(T32))
U9_gg(T32, T33, conA_out_g(T32)) → U10_gg(T32, T33, disD_in_g(T33))
disD_in_g(T44) → U4_g(T44, conA_in_g(T44))
U4_g(T44, conA_out_g(T44)) → disD_out_g(T44)
U10_gg(T32, T33, disD_out_g(T33)) → pE_out_gg(T32, T33)
U3_g(T32, T33, pE_out_gg(T32, T33)) → disD_out_g(or(T32, T33))
U7_gg(T15, T5, disD_out_g(T15)) → U8_gg(T15, T5, conA_in_g(T5))
U8_gg(T15, T5, conA_out_g(T5)) → pF_out_gg(T15, T5)
U6_ggg(T14, T15, T5, pF_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → conA_out_g(and(or(T14, T15), T5))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

CONA_IN_G(and(or(T14, T15), T5)) → U1_G(T14, T15, T5, pB_in_ggg(T14, T15, T5))
CONA_IN_G(and(or(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U5_GGG(T14, T15, T5, conA_in_g(T14))
PB_IN_GGG(T14, T15, T5) → CONA_IN_G(T14)
CONA_IN_G(and(T57, T5)) → U2_G(T57, T5, pC_in_gg(T57, T5))
CONA_IN_G(and(T57, T5)) → PC_IN_GG(T57, T5)
PC_IN_GG(T57, T5) → U11_GG(T57, T5, conA_in_g(T57))
PC_IN_GG(T57, T5) → CONA_IN_G(T57)
U11_GG(T57, T5, conA_out_g(T57)) → U12_GG(T57, T5, conA_in_g(T5))
U11_GG(T57, T5, conA_out_g(T57)) → CONA_IN_G(T5)
U5_GGG(T14, T15, T5, conA_out_g(T14)) → U6_GGG(T14, T15, T5, pF_in_gg(T15, T5))
U5_GGG(T14, T15, T5, conA_out_g(T14)) → PF_IN_GG(T15, T5)
PF_IN_GG(T15, T5) → U7_GG(T15, T5, disD_in_g(T15))
PF_IN_GG(T15, T5) → DISD_IN_G(T15)
DISD_IN_G(or(T32, T33)) → U3_G(T32, T33, pE_in_gg(T32, T33))
DISD_IN_G(or(T32, T33)) → PE_IN_GG(T32, T33)
PE_IN_GG(T32, T33) → U9_GG(T32, T33, conA_in_g(T32))
PE_IN_GG(T32, T33) → CONA_IN_G(T32)
U9_GG(T32, T33, conA_out_g(T32)) → U10_GG(T32, T33, disD_in_g(T33))
U9_GG(T32, T33, conA_out_g(T32)) → DISD_IN_G(T33)
DISD_IN_G(T44) → U4_G(T44, conA_in_g(T44))
DISD_IN_G(T44) → CONA_IN_G(T44)
U7_GG(T15, T5, disD_out_g(T15)) → U8_GG(T15, T5, conA_in_g(T5))
U7_GG(T15, T5, disD_out_g(T15)) → CONA_IN_G(T5)

The TRS R consists of the following rules:

conA_in_g(and(or(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U5_ggg(T14, T15, T5, conA_in_g(T14))
conA_in_g(and(T57, T5)) → U2_g(T57, T5, pC_in_gg(T57, T5))
pC_in_gg(T57, T5) → U11_gg(T57, T5, conA_in_g(T57))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U11_gg(T57, T5, conA_out_g(T57)) → U12_gg(T57, T5, conA_in_g(T5))
U12_gg(T57, T5, conA_out_g(T5)) → pC_out_gg(T57, T5)
U2_g(T57, T5, pC_out_gg(T57, T5)) → conA_out_g(and(T57, T5))
U5_ggg(T14, T15, T5, conA_out_g(T14)) → U6_ggg(T14, T15, T5, pF_in_gg(T15, T5))
pF_in_gg(T15, T5) → U7_gg(T15, T5, disD_in_g(T15))
disD_in_g(or(T32, T33)) → U3_g(T32, T33, pE_in_gg(T32, T33))
pE_in_gg(T32, T33) → U9_gg(T32, T33, conA_in_g(T32))
U9_gg(T32, T33, conA_out_g(T32)) → U10_gg(T32, T33, disD_in_g(T33))
disD_in_g(T44) → U4_g(T44, conA_in_g(T44))
U4_g(T44, conA_out_g(T44)) → disD_out_g(T44)
U10_gg(T32, T33, disD_out_g(T33)) → pE_out_gg(T32, T33)
U3_g(T32, T33, pE_out_gg(T32, T33)) → disD_out_g(or(T32, T33))
U7_gg(T15, T5, disD_out_g(T15)) → U8_gg(T15, T5, conA_in_g(T5))
U8_gg(T15, T5, conA_out_g(T5)) → pF_out_gg(T15, T5)
U6_ggg(T14, T15, T5, pF_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → conA_out_g(and(or(T14, T15), T5))

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

(4) Obligation:

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

CONA_IN_G(and(or(T14, T15), T5)) → U1_G(T14, T15, T5, pB_in_ggg(T14, T15, T5))
CONA_IN_G(and(or(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U5_GGG(T14, T15, T5, conA_in_g(T14))
PB_IN_GGG(T14, T15, T5) → CONA_IN_G(T14)
CONA_IN_G(and(T57, T5)) → U2_G(T57, T5, pC_in_gg(T57, T5))
CONA_IN_G(and(T57, T5)) → PC_IN_GG(T57, T5)
PC_IN_GG(T57, T5) → U11_GG(T57, T5, conA_in_g(T57))
PC_IN_GG(T57, T5) → CONA_IN_G(T57)
U11_GG(T57, T5, conA_out_g(T57)) → U12_GG(T57, T5, conA_in_g(T5))
U11_GG(T57, T5, conA_out_g(T57)) → CONA_IN_G(T5)
U5_GGG(T14, T15, T5, conA_out_g(T14)) → U6_GGG(T14, T15, T5, pF_in_gg(T15, T5))
U5_GGG(T14, T15, T5, conA_out_g(T14)) → PF_IN_GG(T15, T5)
PF_IN_GG(T15, T5) → U7_GG(T15, T5, disD_in_g(T15))
PF_IN_GG(T15, T5) → DISD_IN_G(T15)
DISD_IN_G(or(T32, T33)) → U3_G(T32, T33, pE_in_gg(T32, T33))
DISD_IN_G(or(T32, T33)) → PE_IN_GG(T32, T33)
PE_IN_GG(T32, T33) → U9_GG(T32, T33, conA_in_g(T32))
PE_IN_GG(T32, T33) → CONA_IN_G(T32)
U9_GG(T32, T33, conA_out_g(T32)) → U10_GG(T32, T33, disD_in_g(T33))
U9_GG(T32, T33, conA_out_g(T32)) → DISD_IN_G(T33)
DISD_IN_G(T44) → U4_G(T44, conA_in_g(T44))
DISD_IN_G(T44) → CONA_IN_G(T44)
U7_GG(T15, T5, disD_out_g(T15)) → U8_GG(T15, T5, conA_in_g(T5))
U7_GG(T15, T5, disD_out_g(T15)) → CONA_IN_G(T5)

The TRS R consists of the following rules:

conA_in_g(and(or(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U5_ggg(T14, T15, T5, conA_in_g(T14))
conA_in_g(and(T57, T5)) → U2_g(T57, T5, pC_in_gg(T57, T5))
pC_in_gg(T57, T5) → U11_gg(T57, T5, conA_in_g(T57))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U11_gg(T57, T5, conA_out_g(T57)) → U12_gg(T57, T5, conA_in_g(T5))
U12_gg(T57, T5, conA_out_g(T5)) → pC_out_gg(T57, T5)
U2_g(T57, T5, pC_out_gg(T57, T5)) → conA_out_g(and(T57, T5))
U5_ggg(T14, T15, T5, conA_out_g(T14)) → U6_ggg(T14, T15, T5, pF_in_gg(T15, T5))
pF_in_gg(T15, T5) → U7_gg(T15, T5, disD_in_g(T15))
disD_in_g(or(T32, T33)) → U3_g(T32, T33, pE_in_gg(T32, T33))
pE_in_gg(T32, T33) → U9_gg(T32, T33, conA_in_g(T32))
U9_gg(T32, T33, conA_out_g(T32)) → U10_gg(T32, T33, disD_in_g(T33))
disD_in_g(T44) → U4_g(T44, conA_in_g(T44))
U4_g(T44, conA_out_g(T44)) → disD_out_g(T44)
U10_gg(T32, T33, disD_out_g(T33)) → pE_out_gg(T32, T33)
U3_g(T32, T33, pE_out_gg(T32, T33)) → disD_out_g(or(T32, T33))
U7_gg(T15, T5, disD_out_g(T15)) → U8_gg(T15, T5, conA_in_g(T5))
U8_gg(T15, T5, conA_out_g(T5)) → pF_out_gg(T15, T5)
U6_ggg(T14, T15, T5, pF_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → conA_out_g(and(or(T14, T15), T5))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 8 less nodes.

(6) Obligation:

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

CONA_IN_G(and(or(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U5_GGG(T14, T15, T5, conA_in_g(T14))
U5_GGG(T14, T15, T5, conA_out_g(T14)) → PF_IN_GG(T15, T5)
PF_IN_GG(T15, T5) → U7_GG(T15, T5, disD_in_g(T15))
U7_GG(T15, T5, disD_out_g(T15)) → CONA_IN_G(T5)
CONA_IN_G(and(T57, T5)) → PC_IN_GG(T57, T5)
PC_IN_GG(T57, T5) → U11_GG(T57, T5, conA_in_g(T57))
U11_GG(T57, T5, conA_out_g(T57)) → CONA_IN_G(T5)
PC_IN_GG(T57, T5) → CONA_IN_G(T57)
PF_IN_GG(T15, T5) → DISD_IN_G(T15)
DISD_IN_G(or(T32, T33)) → PE_IN_GG(T32, T33)
PE_IN_GG(T32, T33) → U9_GG(T32, T33, conA_in_g(T32))
U9_GG(T32, T33, conA_out_g(T32)) → DISD_IN_G(T33)
DISD_IN_G(T44) → CONA_IN_G(T44)
PE_IN_GG(T32, T33) → CONA_IN_G(T32)
PB_IN_GGG(T14, T15, T5) → CONA_IN_G(T14)

The TRS R consists of the following rules:

conA_in_g(and(or(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U5_ggg(T14, T15, T5, conA_in_g(T14))
conA_in_g(and(T57, T5)) → U2_g(T57, T5, pC_in_gg(T57, T5))
pC_in_gg(T57, T5) → U11_gg(T57, T5, conA_in_g(T57))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U11_gg(T57, T5, conA_out_g(T57)) → U12_gg(T57, T5, conA_in_g(T5))
U12_gg(T57, T5, conA_out_g(T5)) → pC_out_gg(T57, T5)
U2_g(T57, T5, pC_out_gg(T57, T5)) → conA_out_g(and(T57, T5))
U5_ggg(T14, T15, T5, conA_out_g(T14)) → U6_ggg(T14, T15, T5, pF_in_gg(T15, T5))
pF_in_gg(T15, T5) → U7_gg(T15, T5, disD_in_g(T15))
disD_in_g(or(T32, T33)) → U3_g(T32, T33, pE_in_gg(T32, T33))
pE_in_gg(T32, T33) → U9_gg(T32, T33, conA_in_g(T32))
U9_gg(T32, T33, conA_out_g(T32)) → U10_gg(T32, T33, disD_in_g(T33))
disD_in_g(T44) → U4_g(T44, conA_in_g(T44))
U4_g(T44, conA_out_g(T44)) → disD_out_g(T44)
U10_gg(T32, T33, disD_out_g(T33)) → pE_out_gg(T32, T33)
U3_g(T32, T33, pE_out_gg(T32, T33)) → disD_out_g(or(T32, T33))
U7_gg(T15, T5, disD_out_g(T15)) → U8_gg(T15, T5, conA_in_g(T5))
U8_gg(T15, T5, conA_out_g(T5)) → pF_out_gg(T15, T5)
U6_ggg(T14, T15, T5, pF_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → conA_out_g(and(or(T14, T15), T5))

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

(7) PiDPToQDPProof (EQUIVALENT transformation)

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

(8) Obligation:

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

CONA_IN_G(and(or(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U5_GGG(T14, T15, T5, conA_in_g(T14))
U5_GGG(T14, T15, T5, conA_out_g(T14)) → PF_IN_GG(T15, T5)
PF_IN_GG(T15, T5) → U7_GG(T15, T5, disD_in_g(T15))
U7_GG(T15, T5, disD_out_g(T15)) → CONA_IN_G(T5)
CONA_IN_G(and(T57, T5)) → PC_IN_GG(T57, T5)
PC_IN_GG(T57, T5) → U11_GG(T57, T5, conA_in_g(T57))
U11_GG(T57, T5, conA_out_g(T57)) → CONA_IN_G(T5)
PC_IN_GG(T57, T5) → CONA_IN_G(T57)
PF_IN_GG(T15, T5) → DISD_IN_G(T15)
DISD_IN_G(or(T32, T33)) → PE_IN_GG(T32, T33)
PE_IN_GG(T32, T33) → U9_GG(T32, T33, conA_in_g(T32))
U9_GG(T32, T33, conA_out_g(T32)) → DISD_IN_G(T33)
DISD_IN_G(T44) → CONA_IN_G(T44)
PE_IN_GG(T32, T33) → CONA_IN_G(T32)
PB_IN_GGG(T14, T15, T5) → CONA_IN_G(T14)

The TRS R consists of the following rules:

conA_in_g(and(or(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U5_ggg(T14, T15, T5, conA_in_g(T14))
conA_in_g(and(T57, T5)) → U2_g(T57, T5, pC_in_gg(T57, T5))
pC_in_gg(T57, T5) → U11_gg(T57, T5, conA_in_g(T57))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U11_gg(T57, T5, conA_out_g(T57)) → U12_gg(T57, T5, conA_in_g(T5))
U12_gg(T57, T5, conA_out_g(T5)) → pC_out_gg(T57, T5)
U2_g(T57, T5, pC_out_gg(T57, T5)) → conA_out_g(and(T57, T5))
U5_ggg(T14, T15, T5, conA_out_g(T14)) → U6_ggg(T14, T15, T5, pF_in_gg(T15, T5))
pF_in_gg(T15, T5) → U7_gg(T15, T5, disD_in_g(T15))
disD_in_g(or(T32, T33)) → U3_g(T32, T33, pE_in_gg(T32, T33))
pE_in_gg(T32, T33) → U9_gg(T32, T33, conA_in_g(T32))
U9_gg(T32, T33, conA_out_g(T32)) → U10_gg(T32, T33, disD_in_g(T33))
disD_in_g(T44) → U4_g(T44, conA_in_g(T44))
U4_g(T44, conA_out_g(T44)) → disD_out_g(T44)
U10_gg(T32, T33, disD_out_g(T33)) → pE_out_gg(T32, T33)
U3_g(T32, T33, pE_out_gg(T32, T33)) → disD_out_g(or(T32, T33))
U7_gg(T15, T5, disD_out_g(T15)) → U8_gg(T15, T5, conA_in_g(T5))
U8_gg(T15, T5, conA_out_g(T5)) → pF_out_gg(T15, T5)
U6_ggg(T14, T15, T5, pF_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → conA_out_g(and(or(T14, T15), T5))

The set Q consists of the following terms:

conA_in_g(x0)
pB_in_ggg(x0, x1, x2)
pC_in_gg(x0, x1)
U11_gg(x0, x1, x2)
U12_gg(x0, x1, x2)
U2_g(x0, x1, x2)
U5_ggg(x0, x1, x2, x3)
pF_in_gg(x0, x1)
disD_in_g(x0)
pE_in_gg(x0, x1)
U9_gg(x0, x1, x2)
U4_g(x0, x1)
U10_gg(x0, x1, x2)
U3_g(x0, x1, x2)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)
U6_ggg(x0, x1, x2, x3)
U1_g(x0, x1, x2, x3)

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

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

• PB_IN_GGG(T14, T15, T5) → CONA_IN_G(T14)
  The graph contains the following edges 1 >= 1

• PB_IN_GGG(T14, T15, T5) → U5_GGG(T14, T15, T5, conA_in_g(T14))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

• U5_GGG(T14, T15, T5, conA_out_g(T14)) → PF_IN_GG(T15, T5)
  The graph contains the following edges 2 >= 1, 3 >= 2

• CONA_IN_G(and(or(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• U7_GG(T15, T5, disD_out_g(T15)) → CONA_IN_G(T5)
  The graph contains the following edges 2 >= 1

• PF_IN_GG(T15, T5) → U7_GG(T15, T5, disD_in_g(T15))
  The graph contains the following edges 1 >= 1, 2 >= 2

• PF_IN_GG(T15, T5) → DISD_IN_G(T15)
  The graph contains the following edges 1 >= 1

• CONA_IN_G(and(T57, T5)) → PC_IN_GG(T57, T5)
  The graph contains the following edges 1 > 1, 1 > 2

• PC_IN_GG(T57, T5) → CONA_IN_G(T57)
  The graph contains the following edges 1 >= 1

• PC_IN_GG(T57, T5) → U11_GG(T57, T5, conA_in_g(T57))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U11_GG(T57, T5, conA_out_g(T57)) → CONA_IN_G(T5)
  The graph contains the following edges 2 >= 1

• DISD_IN_G(T44) → CONA_IN_G(T44)
  The graph contains the following edges 1 >= 1

• PE_IN_GG(T32, T33) → CONA_IN_G(T32)
  The graph contains the following edges 1 >= 1

• DISD_IN_G(or(T32, T33)) → PE_IN_GG(T32, T33)
  The graph contains the following edges 1 > 1, 1 > 2

• PE_IN_GG(T32, T33) → U9_GG(T32, T33, conA_in_g(T32))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U9_GG(T32, T33, conA_out_g(T32)) → DISD_IN_G(T33)
  The graph contains the following edges 2 >= 1

(10) YES