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



↳ PROLOG
  ↳ PrologToPiTRSProof

dis1(or2(B1, B2)) :- con1(B1), dis1(B2).
dis1(B) :- con1(B).
con1(and2(B1, B2)) :- dis1(B1), con1(B2).
con1(B) :- bool1(B).
bool1(00).
bool1(10).


With regard to the inferred argument filtering the predicates were used in the following modes:
dis1: (b)
con1: (b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g3(B1, B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g3(B1, B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g2(B, con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g2(B, bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g1(0_0)
bool_1_in_g1(1_0) -> bool_1_out_g1(1_0)
if_con_1_in_3_g2(B, bool_1_out_g1(B)) -> con_1_out_g1(B)
if_dis_1_in_3_g2(B, con_1_out_g1(B)) -> dis_1_out_g1(B)
if_con_1_in_1_g3(B1, B2, dis_1_out_g1(B1)) -> if_con_1_in_2_g3(B1, B2, con_1_in_g1(B2))
if_con_1_in_2_g3(B1, B2, con_1_out_g1(B2)) -> con_1_out_g1(and_22(B1, B2))
if_dis_1_in_1_g3(B1, B2, con_1_out_g1(B1)) -> if_dis_1_in_2_g3(B1, B2, dis_1_in_g1(B2))
if_dis_1_in_2_g3(B1, B2, dis_1_out_g1(B2)) -> dis_1_out_g1(or_22(B1, B2))

The argument filtering Pi contains the following mapping:
dis_1_in_g1(x1)  =  dis_1_in_g1(x1)
or_22(x1, x2)  =  or_22(x1, x2)
and_22(x1, x2)  =  and_22(x1, x2)
0_0  =  0_0
1_0  =  1_0
if_dis_1_in_1_g3(x1, x2, x3)  =  if_dis_1_in_1_g2(x2, x3)
con_1_in_g1(x1)  =  con_1_in_g1(x1)
if_con_1_in_1_g3(x1, x2, x3)  =  if_con_1_in_1_g2(x2, x3)
if_dis_1_in_3_g2(x1, x2)  =  if_dis_1_in_3_g1(x2)
if_con_1_in_3_g2(x1, x2)  =  if_con_1_in_3_g1(x2)
bool_1_in_g1(x1)  =  bool_1_in_g1(x1)
bool_1_out_g1(x1)  =  bool_1_out_g
con_1_out_g1(x1)  =  con_1_out_g
dis_1_out_g1(x1)  =  dis_1_out_g
if_con_1_in_2_g3(x1, x2, x3)  =  if_con_1_in_2_g1(x3)
if_dis_1_in_2_g3(x1, x2, x3)  =  if_dis_1_in_2_g1(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g3(B1, B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g3(B1, B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g2(B, con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g2(B, bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g1(0_0)
bool_1_in_g1(1_0) -> bool_1_out_g1(1_0)
if_con_1_in_3_g2(B, bool_1_out_g1(B)) -> con_1_out_g1(B)
if_dis_1_in_3_g2(B, con_1_out_g1(B)) -> dis_1_out_g1(B)
if_con_1_in_1_g3(B1, B2, dis_1_out_g1(B1)) -> if_con_1_in_2_g3(B1, B2, con_1_in_g1(B2))
if_con_1_in_2_g3(B1, B2, con_1_out_g1(B2)) -> con_1_out_g1(and_22(B1, B2))
if_dis_1_in_1_g3(B1, B2, con_1_out_g1(B1)) -> if_dis_1_in_2_g3(B1, B2, dis_1_in_g1(B2))
if_dis_1_in_2_g3(B1, B2, dis_1_out_g1(B2)) -> dis_1_out_g1(or_22(B1, B2))

The argument filtering Pi contains the following mapping:
dis_1_in_g1(x1)  =  dis_1_in_g1(x1)
or_22(x1, x2)  =  or_22(x1, x2)
and_22(x1, x2)  =  and_22(x1, x2)
0_0  =  0_0
1_0  =  1_0
if_dis_1_in_1_g3(x1, x2, x3)  =  if_dis_1_in_1_g2(x2, x3)
con_1_in_g1(x1)  =  con_1_in_g1(x1)
if_con_1_in_1_g3(x1, x2, x3)  =  if_con_1_in_1_g2(x2, x3)
if_dis_1_in_3_g2(x1, x2)  =  if_dis_1_in_3_g1(x2)
if_con_1_in_3_g2(x1, x2)  =  if_con_1_in_3_g1(x2)
bool_1_in_g1(x1)  =  bool_1_in_g1(x1)
bool_1_out_g1(x1)  =  bool_1_out_g
con_1_out_g1(x1)  =  con_1_out_g
dis_1_out_g1(x1)  =  dis_1_out_g
if_con_1_in_2_g3(x1, x2, x3)  =  if_con_1_in_2_g1(x3)
if_dis_1_in_2_g3(x1, x2, x3)  =  if_dis_1_in_2_g1(x3)


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

DIS_1_IN_G1(or_22(B1, B2)) -> IF_DIS_1_IN_1_G3(B1, B2, con_1_in_g1(B1))
DIS_1_IN_G1(or_22(B1, B2)) -> CON_1_IN_G1(B1)
CON_1_IN_G1(and_22(B1, B2)) -> IF_CON_1_IN_1_G3(B1, B2, dis_1_in_g1(B1))
CON_1_IN_G1(and_22(B1, B2)) -> DIS_1_IN_G1(B1)
DIS_1_IN_G1(B) -> IF_DIS_1_IN_3_G2(B, con_1_in_g1(B))
DIS_1_IN_G1(B) -> CON_1_IN_G1(B)
CON_1_IN_G1(B) -> IF_CON_1_IN_3_G2(B, bool_1_in_g1(B))
CON_1_IN_G1(B) -> BOOL_1_IN_G1(B)
IF_CON_1_IN_1_G3(B1, B2, dis_1_out_g1(B1)) -> IF_CON_1_IN_2_G3(B1, B2, con_1_in_g1(B2))
IF_CON_1_IN_1_G3(B1, B2, dis_1_out_g1(B1)) -> CON_1_IN_G1(B2)
IF_DIS_1_IN_1_G3(B1, B2, con_1_out_g1(B1)) -> IF_DIS_1_IN_2_G3(B1, B2, dis_1_in_g1(B2))
IF_DIS_1_IN_1_G3(B1, B2, con_1_out_g1(B1)) -> DIS_1_IN_G1(B2)

The TRS R consists of the following rules:

dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g3(B1, B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g3(B1, B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g2(B, con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g2(B, bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g1(0_0)
bool_1_in_g1(1_0) -> bool_1_out_g1(1_0)
if_con_1_in_3_g2(B, bool_1_out_g1(B)) -> con_1_out_g1(B)
if_dis_1_in_3_g2(B, con_1_out_g1(B)) -> dis_1_out_g1(B)
if_con_1_in_1_g3(B1, B2, dis_1_out_g1(B1)) -> if_con_1_in_2_g3(B1, B2, con_1_in_g1(B2))
if_con_1_in_2_g3(B1, B2, con_1_out_g1(B2)) -> con_1_out_g1(and_22(B1, B2))
if_dis_1_in_1_g3(B1, B2, con_1_out_g1(B1)) -> if_dis_1_in_2_g3(B1, B2, dis_1_in_g1(B2))
if_dis_1_in_2_g3(B1, B2, dis_1_out_g1(B2)) -> dis_1_out_g1(or_22(B1, B2))

The argument filtering Pi contains the following mapping:
dis_1_in_g1(x1)  =  dis_1_in_g1(x1)
or_22(x1, x2)  =  or_22(x1, x2)
and_22(x1, x2)  =  and_22(x1, x2)
0_0  =  0_0
1_0  =  1_0
if_dis_1_in_1_g3(x1, x2, x3)  =  if_dis_1_in_1_g2(x2, x3)
con_1_in_g1(x1)  =  con_1_in_g1(x1)
if_con_1_in_1_g3(x1, x2, x3)  =  if_con_1_in_1_g2(x2, x3)
if_dis_1_in_3_g2(x1, x2)  =  if_dis_1_in_3_g1(x2)
if_con_1_in_3_g2(x1, x2)  =  if_con_1_in_3_g1(x2)
bool_1_in_g1(x1)  =  bool_1_in_g1(x1)
bool_1_out_g1(x1)  =  bool_1_out_g
con_1_out_g1(x1)  =  con_1_out_g
dis_1_out_g1(x1)  =  dis_1_out_g
if_con_1_in_2_g3(x1, x2, x3)  =  if_con_1_in_2_g1(x3)
if_dis_1_in_2_g3(x1, x2, x3)  =  if_dis_1_in_2_g1(x3)
IF_CON_1_IN_3_G2(x1, x2)  =  IF_CON_1_IN_3_G1(x2)
IF_DIS_1_IN_1_G3(x1, x2, x3)  =  IF_DIS_1_IN_1_G2(x2, x3)
DIS_1_IN_G1(x1)  =  DIS_1_IN_G1(x1)
BOOL_1_IN_G1(x1)  =  BOOL_1_IN_G1(x1)
IF_DIS_1_IN_2_G3(x1, x2, x3)  =  IF_DIS_1_IN_2_G1(x3)
IF_DIS_1_IN_3_G2(x1, x2)  =  IF_DIS_1_IN_3_G1(x2)
IF_CON_1_IN_1_G3(x1, x2, x3)  =  IF_CON_1_IN_1_G2(x2, x3)
CON_1_IN_G1(x1)  =  CON_1_IN_G1(x1)
IF_CON_1_IN_2_G3(x1, x2, x3)  =  IF_CON_1_IN_2_G1(x3)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

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

DIS_1_IN_G1(or_22(B1, B2)) -> IF_DIS_1_IN_1_G3(B1, B2, con_1_in_g1(B1))
DIS_1_IN_G1(or_22(B1, B2)) -> CON_1_IN_G1(B1)
CON_1_IN_G1(and_22(B1, B2)) -> IF_CON_1_IN_1_G3(B1, B2, dis_1_in_g1(B1))
CON_1_IN_G1(and_22(B1, B2)) -> DIS_1_IN_G1(B1)
DIS_1_IN_G1(B) -> IF_DIS_1_IN_3_G2(B, con_1_in_g1(B))
DIS_1_IN_G1(B) -> CON_1_IN_G1(B)
CON_1_IN_G1(B) -> IF_CON_1_IN_3_G2(B, bool_1_in_g1(B))
CON_1_IN_G1(B) -> BOOL_1_IN_G1(B)
IF_CON_1_IN_1_G3(B1, B2, dis_1_out_g1(B1)) -> IF_CON_1_IN_2_G3(B1, B2, con_1_in_g1(B2))
IF_CON_1_IN_1_G3(B1, B2, dis_1_out_g1(B1)) -> CON_1_IN_G1(B2)
IF_DIS_1_IN_1_G3(B1, B2, con_1_out_g1(B1)) -> IF_DIS_1_IN_2_G3(B1, B2, dis_1_in_g1(B2))
IF_DIS_1_IN_1_G3(B1, B2, con_1_out_g1(B1)) -> DIS_1_IN_G1(B2)

The TRS R consists of the following rules:

dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g3(B1, B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g3(B1, B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g2(B, con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g2(B, bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g1(0_0)
bool_1_in_g1(1_0) -> bool_1_out_g1(1_0)
if_con_1_in_3_g2(B, bool_1_out_g1(B)) -> con_1_out_g1(B)
if_dis_1_in_3_g2(B, con_1_out_g1(B)) -> dis_1_out_g1(B)
if_con_1_in_1_g3(B1, B2, dis_1_out_g1(B1)) -> if_con_1_in_2_g3(B1, B2, con_1_in_g1(B2))
if_con_1_in_2_g3(B1, B2, con_1_out_g1(B2)) -> con_1_out_g1(and_22(B1, B2))
if_dis_1_in_1_g3(B1, B2, con_1_out_g1(B1)) -> if_dis_1_in_2_g3(B1, B2, dis_1_in_g1(B2))
if_dis_1_in_2_g3(B1, B2, dis_1_out_g1(B2)) -> dis_1_out_g1(or_22(B1, B2))

The argument filtering Pi contains the following mapping:
dis_1_in_g1(x1)  =  dis_1_in_g1(x1)
or_22(x1, x2)  =  or_22(x1, x2)
and_22(x1, x2)  =  and_22(x1, x2)
0_0  =  0_0
1_0  =  1_0
if_dis_1_in_1_g3(x1, x2, x3)  =  if_dis_1_in_1_g2(x2, x3)
con_1_in_g1(x1)  =  con_1_in_g1(x1)
if_con_1_in_1_g3(x1, x2, x3)  =  if_con_1_in_1_g2(x2, x3)
if_dis_1_in_3_g2(x1, x2)  =  if_dis_1_in_3_g1(x2)
if_con_1_in_3_g2(x1, x2)  =  if_con_1_in_3_g1(x2)
bool_1_in_g1(x1)  =  bool_1_in_g1(x1)
bool_1_out_g1(x1)  =  bool_1_out_g
con_1_out_g1(x1)  =  con_1_out_g
dis_1_out_g1(x1)  =  dis_1_out_g
if_con_1_in_2_g3(x1, x2, x3)  =  if_con_1_in_2_g1(x3)
if_dis_1_in_2_g3(x1, x2, x3)  =  if_dis_1_in_2_g1(x3)
IF_CON_1_IN_3_G2(x1, x2)  =  IF_CON_1_IN_3_G1(x2)
IF_DIS_1_IN_1_G3(x1, x2, x3)  =  IF_DIS_1_IN_1_G2(x2, x3)
DIS_1_IN_G1(x1)  =  DIS_1_IN_G1(x1)
BOOL_1_IN_G1(x1)  =  BOOL_1_IN_G1(x1)
IF_DIS_1_IN_2_G3(x1, x2, x3)  =  IF_DIS_1_IN_2_G1(x3)
IF_DIS_1_IN_3_G2(x1, x2)  =  IF_DIS_1_IN_3_G1(x2)
IF_CON_1_IN_1_G3(x1, x2, x3)  =  IF_CON_1_IN_1_G2(x2, x3)
CON_1_IN_G1(x1)  =  CON_1_IN_G1(x1)
IF_CON_1_IN_2_G3(x1, x2, x3)  =  IF_CON_1_IN_2_G1(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 5 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

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

IF_DIS_1_IN_1_G3(B1, B2, con_1_out_g1(B1)) -> DIS_1_IN_G1(B2)
IF_CON_1_IN_1_G3(B1, B2, dis_1_out_g1(B1)) -> CON_1_IN_G1(B2)
DIS_1_IN_G1(B) -> CON_1_IN_G1(B)
CON_1_IN_G1(and_22(B1, B2)) -> IF_CON_1_IN_1_G3(B1, B2, dis_1_in_g1(B1))
DIS_1_IN_G1(or_22(B1, B2)) -> CON_1_IN_G1(B1)
CON_1_IN_G1(and_22(B1, B2)) -> DIS_1_IN_G1(B1)
DIS_1_IN_G1(or_22(B1, B2)) -> IF_DIS_1_IN_1_G3(B1, B2, con_1_in_g1(B1))

The TRS R consists of the following rules:

dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g3(B1, B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g3(B1, B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g2(B, con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g2(B, bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g1(0_0)
bool_1_in_g1(1_0) -> bool_1_out_g1(1_0)
if_con_1_in_3_g2(B, bool_1_out_g1(B)) -> con_1_out_g1(B)
if_dis_1_in_3_g2(B, con_1_out_g1(B)) -> dis_1_out_g1(B)
if_con_1_in_1_g3(B1, B2, dis_1_out_g1(B1)) -> if_con_1_in_2_g3(B1, B2, con_1_in_g1(B2))
if_con_1_in_2_g3(B1, B2, con_1_out_g1(B2)) -> con_1_out_g1(and_22(B1, B2))
if_dis_1_in_1_g3(B1, B2, con_1_out_g1(B1)) -> if_dis_1_in_2_g3(B1, B2, dis_1_in_g1(B2))
if_dis_1_in_2_g3(B1, B2, dis_1_out_g1(B2)) -> dis_1_out_g1(or_22(B1, B2))

The argument filtering Pi contains the following mapping:
dis_1_in_g1(x1)  =  dis_1_in_g1(x1)
or_22(x1, x2)  =  or_22(x1, x2)
and_22(x1, x2)  =  and_22(x1, x2)
0_0  =  0_0
1_0  =  1_0
if_dis_1_in_1_g3(x1, x2, x3)  =  if_dis_1_in_1_g2(x2, x3)
con_1_in_g1(x1)  =  con_1_in_g1(x1)
if_con_1_in_1_g3(x1, x2, x3)  =  if_con_1_in_1_g2(x2, x3)
if_dis_1_in_3_g2(x1, x2)  =  if_dis_1_in_3_g1(x2)
if_con_1_in_3_g2(x1, x2)  =  if_con_1_in_3_g1(x2)
bool_1_in_g1(x1)  =  bool_1_in_g1(x1)
bool_1_out_g1(x1)  =  bool_1_out_g
con_1_out_g1(x1)  =  con_1_out_g
dis_1_out_g1(x1)  =  dis_1_out_g
if_con_1_in_2_g3(x1, x2, x3)  =  if_con_1_in_2_g1(x3)
if_dis_1_in_2_g3(x1, x2, x3)  =  if_dis_1_in_2_g1(x3)
IF_DIS_1_IN_1_G3(x1, x2, x3)  =  IF_DIS_1_IN_1_G2(x2, x3)
DIS_1_IN_G1(x1)  =  DIS_1_IN_G1(x1)
IF_CON_1_IN_1_G3(x1, x2, x3)  =  IF_CON_1_IN_1_G2(x2, x3)
CON_1_IN_G1(x1)  =  CON_1_IN_G1(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPSizeChangeProof

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

IF_DIS_1_IN_1_G2(B2, con_1_out_g) -> DIS_1_IN_G1(B2)
IF_CON_1_IN_1_G2(B2, dis_1_out_g) -> CON_1_IN_G1(B2)
DIS_1_IN_G1(B) -> CON_1_IN_G1(B)
CON_1_IN_G1(and_22(B1, B2)) -> IF_CON_1_IN_1_G2(B2, dis_1_in_g1(B1))
DIS_1_IN_G1(or_22(B1, B2)) -> CON_1_IN_G1(B1)
CON_1_IN_G1(and_22(B1, B2)) -> DIS_1_IN_G1(B1)
DIS_1_IN_G1(or_22(B1, B2)) -> IF_DIS_1_IN_1_G2(B2, con_1_in_g1(B1))

The TRS R consists of the following rules:

dis_1_in_g1(or_22(B1, B2)) -> if_dis_1_in_1_g2(B2, con_1_in_g1(B1))
con_1_in_g1(and_22(B1, B2)) -> if_con_1_in_1_g2(B2, dis_1_in_g1(B1))
dis_1_in_g1(B) -> if_dis_1_in_3_g1(con_1_in_g1(B))
con_1_in_g1(B) -> if_con_1_in_3_g1(bool_1_in_g1(B))
bool_1_in_g1(0_0) -> bool_1_out_g
bool_1_in_g1(1_0) -> bool_1_out_g
if_con_1_in_3_g1(bool_1_out_g) -> con_1_out_g
if_dis_1_in_3_g1(con_1_out_g) -> dis_1_out_g
if_con_1_in_1_g2(B2, dis_1_out_g) -> if_con_1_in_2_g1(con_1_in_g1(B2))
if_con_1_in_2_g1(con_1_out_g) -> con_1_out_g
if_dis_1_in_1_g2(B2, con_1_out_g) -> if_dis_1_in_2_g1(dis_1_in_g1(B2))
if_dis_1_in_2_g1(dis_1_out_g) -> dis_1_out_g

The set Q consists of the following terms:

dis_1_in_g1(x0)
con_1_in_g1(x0)
bool_1_in_g1(x0)
if_con_1_in_3_g1(x0)
if_dis_1_in_3_g1(x0)
if_con_1_in_1_g2(x0, x1)
if_con_1_in_2_g1(x0)
if_dis_1_in_1_g2(x0, x1)
if_dis_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DIS_1_IN_G1, IF_DIS_1_IN_1_G2, CON_1_IN_G1, IF_CON_1_IN_1_G2}.
By using the subterm criterion together with the size-change analysis 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: