0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 106 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 119 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 13 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇔, 24 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 7 ms)
↳12 YES
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
U4_g(T64, T65, conC_out_g(or(T64, T65))) → disA_out_g(or(T64, T65))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
DISA_IN_G(or(and(T14, T15), T5)) → U1_G(T14, T15, T5, pB_in_ggg(T14, T15, T5))
DISA_IN_G(or(and(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U7_GGG(T14, T15, T5, disA_in_g(T14))
PB_IN_GGG(T14, T15, T5) → DISA_IN_G(T14)
DISA_IN_G(or(0, T5)) → U2_G(T5, disA_in_g(T5))
DISA_IN_G(or(0, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(1, T5)) → U3_G(T5, disA_in_g(T5))
DISA_IN_G(or(1, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(T64, T65)) → U4_G(T64, T65, conC_in_g(or(T64, T65)))
DISA_IN_G(or(T64, T65)) → CONC_IN_G(or(T64, T65))
CONC_IN_G(and(T32, T33)) → U6_G(T32, T33, pD_in_gg(T32, T33))
CONC_IN_G(and(T32, T33)) → PD_IN_GG(T32, T33)
PD_IN_GG(T32, T33) → U11_GG(T32, T33, disA_in_g(T32))
PD_IN_GG(T32, T33) → DISA_IN_G(T32)
DISA_IN_G(and(T76, T77)) → U5_G(T76, T77, pD_in_gg(T76, T77))
DISA_IN_G(and(T76, T77)) → PD_IN_GG(T76, T77)
U11_GG(T32, T33, disA_out_g(T32)) → U12_GG(T32, T33, conC_in_g(T33))
U11_GG(T32, T33, disA_out_g(T32)) → CONC_IN_G(T33)
U7_GGG(T14, T15, T5, disA_out_g(T14)) → U8_GGG(T14, T15, T5, pE_in_gg(T15, T5))
U7_GGG(T14, T15, T5, disA_out_g(T14)) → PE_IN_GG(T15, T5)
PE_IN_GG(T15, T5) → U9_GG(T15, T5, conC_in_g(T15))
PE_IN_GG(T15, T5) → CONC_IN_G(T15)
U9_GG(T15, T5, conC_out_g(T15)) → U10_GG(T15, T5, disA_in_g(T5))
U9_GG(T15, T5, conC_out_g(T15)) → DISA_IN_G(T5)
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
U4_g(T64, T65, conC_out_g(or(T64, T65))) → disA_out_g(or(T64, T65))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
DISA_IN_G(or(and(T14, T15), T5)) → U1_G(T14, T15, T5, pB_in_ggg(T14, T15, T5))
DISA_IN_G(or(and(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U7_GGG(T14, T15, T5, disA_in_g(T14))
PB_IN_GGG(T14, T15, T5) → DISA_IN_G(T14)
DISA_IN_G(or(0, T5)) → U2_G(T5, disA_in_g(T5))
DISA_IN_G(or(0, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(1, T5)) → U3_G(T5, disA_in_g(T5))
DISA_IN_G(or(1, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(T64, T65)) → U4_G(T64, T65, conC_in_g(or(T64, T65)))
DISA_IN_G(or(T64, T65)) → CONC_IN_G(or(T64, T65))
CONC_IN_G(and(T32, T33)) → U6_G(T32, T33, pD_in_gg(T32, T33))
CONC_IN_G(and(T32, T33)) → PD_IN_GG(T32, T33)
PD_IN_GG(T32, T33) → U11_GG(T32, T33, disA_in_g(T32))
PD_IN_GG(T32, T33) → DISA_IN_G(T32)
DISA_IN_G(and(T76, T77)) → U5_G(T76, T77, pD_in_gg(T76, T77))
DISA_IN_G(and(T76, T77)) → PD_IN_GG(T76, T77)
U11_GG(T32, T33, disA_out_g(T32)) → U12_GG(T32, T33, conC_in_g(T33))
U11_GG(T32, T33, disA_out_g(T32)) → CONC_IN_G(T33)
U7_GGG(T14, T15, T5, disA_out_g(T14)) → U8_GGG(T14, T15, T5, pE_in_gg(T15, T5))
U7_GGG(T14, T15, T5, disA_out_g(T14)) → PE_IN_GG(T15, T5)
PE_IN_GG(T15, T5) → U9_GG(T15, T5, conC_in_g(T15))
PE_IN_GG(T15, T5) → CONC_IN_G(T15)
U9_GG(T15, T5, conC_out_g(T15)) → U10_GG(T15, T5, disA_in_g(T5))
U9_GG(T15, T5, conC_out_g(T15)) → DISA_IN_G(T5)
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
U4_g(T64, T65, conC_out_g(or(T64, T65))) → disA_out_g(or(T64, T65))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
DISA_IN_G(or(and(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U7_GGG(T14, T15, T5, disA_in_g(T14))
U7_GGG(T14, T15, T5, disA_out_g(T14)) → PE_IN_GG(T15, T5)
PE_IN_GG(T15, T5) → U9_GG(T15, T5, conC_in_g(T15))
U9_GG(T15, T5, conC_out_g(T15)) → DISA_IN_G(T5)
DISA_IN_G(or(0, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(1, T5)) → DISA_IN_G(T5)
DISA_IN_G(and(T76, T77)) → PD_IN_GG(T76, T77)
PD_IN_GG(T32, T33) → U11_GG(T32, T33, disA_in_g(T32))
U11_GG(T32, T33, disA_out_g(T32)) → CONC_IN_G(T33)
CONC_IN_G(and(T32, T33)) → PD_IN_GG(T32, T33)
PD_IN_GG(T32, T33) → DISA_IN_G(T32)
PE_IN_GG(T15, T5) → CONC_IN_G(T15)
PB_IN_GGG(T14, T15, T5) → DISA_IN_G(T14)
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
U4_g(T64, T65, conC_out_g(or(T64, T65))) → disA_out_g(or(T64, T65))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
DISA_IN_G(or(and(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U7_GGG(T14, T15, T5, disA_in_g(T14))
U7_GGG(T14, T15, T5, disA_out_g(T14)) → PE_IN_GG(T15, T5)
PE_IN_GG(T15, T5) → U9_GG(T15, T5, conC_in_g(T15))
U9_GG(T15, T5, conC_out_g(T15)) → DISA_IN_G(T5)
DISA_IN_G(or(0, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(1, T5)) → DISA_IN_G(T5)
DISA_IN_G(and(T76, T77)) → PD_IN_GG(T76, T77)
PD_IN_GG(T32, T33) → U11_GG(T32, T33, disA_in_g(T32))
U11_GG(T32, T33, disA_out_g(T32)) → CONC_IN_G(T33)
CONC_IN_G(and(T32, T33)) → PD_IN_GG(T32, T33)
PD_IN_GG(T32, T33) → DISA_IN_G(T32)
PE_IN_GG(T15, T5) → CONC_IN_G(T15)
PB_IN_GGG(T14, T15, T5) → DISA_IN_G(T14)
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
DISA_IN_G(or(and(T14, T15), T5)) → PB_IN_GGG(T14, T15, T5)
PB_IN_GGG(T14, T15, T5) → U7_GGG(T14, T15, T5, disA_in_g(T14))
U7_GGG(T14, T15, T5, disA_out_g(T14)) → PE_IN_GG(T15, T5)
PE_IN_GG(T15, T5) → U9_GG(T15, T5, conC_in_g(T15))
U9_GG(T15, T5, conC_out_g(T15)) → DISA_IN_G(T5)
DISA_IN_G(or(0, T5)) → DISA_IN_G(T5)
DISA_IN_G(or(1, T5)) → DISA_IN_G(T5)
DISA_IN_G(and(T76, T77)) → PD_IN_GG(T76, T77)
PD_IN_GG(T32, T33) → U11_GG(T32, T33, disA_in_g(T32))
U11_GG(T32, T33, disA_out_g(T32)) → CONC_IN_G(T33)
CONC_IN_G(and(T32, T33)) → PD_IN_GG(T32, T33)
PD_IN_GG(T32, T33) → DISA_IN_G(T32)
PE_IN_GG(T15, T5) → CONC_IN_G(T15)
PB_IN_GGG(T14, T15, T5) → DISA_IN_G(T14)
disA_in_g(or(and(T14, T15), T5)) → U1_g(T14, T15, T5, pB_in_ggg(T14, T15, T5))
disA_in_g(or(0, T5)) → U2_g(T5, disA_in_g(T5))
disA_in_g(or(1, T5)) → U3_g(T5, disA_in_g(T5))
disA_in_g(or(T64, T65)) → U4_g(T64, T65, conC_in_g(or(T64, T65)))
disA_in_g(and(T76, T77)) → U5_g(T76, T77, pD_in_gg(T76, T77))
disA_in_g(0) → disA_out_g(0)
disA_in_g(1) → disA_out_g(1)
conC_in_g(and(T32, T33)) → U6_g(T32, T33, pD_in_gg(T32, T33))
conC_in_g(0) → conC_out_g(0)
conC_in_g(1) → conC_out_g(1)
U1_g(T14, T15, T5, pB_out_ggg(T14, T15, T5)) → disA_out_g(or(and(T14, T15), T5))
U2_g(T5, disA_out_g(T5)) → disA_out_g(or(0, T5))
U3_g(T5, disA_out_g(T5)) → disA_out_g(or(1, T5))
U5_g(T76, T77, pD_out_gg(T76, T77)) → disA_out_g(and(T76, T77))
U6_g(T32, T33, pD_out_gg(T32, T33)) → conC_out_g(and(T32, T33))
pB_in_ggg(T14, T15, T5) → U7_ggg(T14, T15, T5, disA_in_g(T14))
pD_in_gg(T32, T33) → U11_gg(T32, T33, disA_in_g(T32))
U7_ggg(T14, T15, T5, disA_out_g(T14)) → U8_ggg(T14, T15, T5, pE_in_gg(T15, T5))
U11_gg(T32, T33, disA_out_g(T32)) → U12_gg(T32, T33, conC_in_g(T33))
U8_ggg(T14, T15, T5, pE_out_gg(T15, T5)) → pB_out_ggg(T14, T15, T5)
U12_gg(T32, T33, conC_out_g(T33)) → pD_out_gg(T32, T33)
pE_in_gg(T15, T5) → U9_gg(T15, T5, conC_in_g(T15))
U9_gg(T15, T5, conC_out_g(T15)) → U10_gg(T15, T5, disA_in_g(T5))
U10_gg(T15, T5, disA_out_g(T5)) → pE_out_gg(T15, T5)
disA_in_g(x0)
conC_in_g(x0)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1)
U3_g(x0, x1)
U5_g(x0, x1, x2)
U6_g(x0, x1, x2)
pB_in_ggg(x0, x1, x2)
pD_in_gg(x0, x1)
U7_ggg(x0, x1, x2, x3)
U11_gg(x0, x1, x2)
U8_ggg(x0, x1, x2, x3)
U12_gg(x0, x1, x2)
pE_in_gg(x0, x1)
U9_gg(x0, x1, x2)
U10_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: