MAYBE Rewrite Rules: [ join(?x,meet(?x,?y)) -> ?x, meet(?x,join(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)), meet(?x,?x) -> ?x, join(?x,?x) -> ?x, meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)), meet(?x,?y) -> meet(?y,?x), join(join(?x,?y),?z) -> join(?x,join(?y,?z)), join(?x,?y) -> join(?y,?x) ] Apply Direct Methods... Inner CPs: [ join(?x_1,join(meet(?x_1,?y_1),meet(?x_1,?z_1))) = ?x_1, join(?x_2,?x_2) = ?x_2, join(meet(?x_4,?y_4),meet(?x_4,meet(?y_4,?z_4))) = meet(?x_4,?y_4), join(?x_5,meet(?y_5,?x_5)) = ?x_5, meet(?x_1,?x) = join(meet(?x_1,?x),meet(?x_1,meet(?x,?y))), meet(?x_1,?x_3) = join(meet(?x_1,?x_3),meet(?x_1,?x_3)), meet(?x_1,join(?x_6,join(?y_6,?z_6))) = join(meet(?x_1,join(?x_6,?y_6)),meet(?x_1,?z_6)), meet(?x_1,join(?y_7,?x_7)) = join(meet(?x_1,?x_7),meet(?x_1,?y_7)), meet(join(meet(?x_1,?y_1),meet(?x_1,?z_1)),?z_4) = meet(?x_1,meet(join(?y_1,?z_1),?z_4)), meet(?x_2,?z_4) = meet(?x_2,meet(?x_2,?z_4)), meet(meet(?y_5,?x_5),?z_4) = meet(?x_5,meet(?y_5,?z_4)), join(?x,?z_6) = join(?x,join(meet(?x,?y),?z_6)), join(?x_3,?z_6) = join(?x_3,join(?x_3,?z_6)), join(join(?y_7,?x_7),?z_6) = join(?x_7,join(?y_7,?z_6)), meet(meet(?x,meet(?y,?z)),?z_1) = meet(meet(?x,?y),meet(?z,?z_1)), join(join(?x,join(?y,?z)),?z_1) = join(join(?x,?y),join(?z,?z_1)) ] Outer CPs: [ join(?x_6,?y_6) = join(?x_6,join(?y_6,meet(join(?x_6,?y_6),?y))), ?x = join(meet(?x,?y),?x), join(meet(join(?y_1,?z_1),?y_1),meet(join(?y_1,?z_1),?z_1)) = join(?y_1,?z_1), join(meet(meet(?x_4,?y_4),?y_1),meet(meet(?x_4,?y_4),?z_1)) = meet(?x_4,meet(?y_4,join(?y_1,?z_1))), join(meet(?x_1,?y_1),meet(?x_1,?z_1)) = meet(join(?y_1,?z_1),?x_1), meet(?x_4,?y_4) = meet(?x_4,meet(?y_4,meet(?x_4,?y_4))), ?x_2 = meet(?x_2,?x_2), join(?x_6,?y_6) = join(?x_6,join(?y_6,join(?x_6,?y_6))), ?x_3 = join(?x_3,?x_3), meet(?x_4,meet(?y_4,?z_4)) = meet(?z_4,meet(?x_4,?y_4)), join(?x_6,join(?y_6,?z_6)) = join(?z_6,join(?x_6,?y_6)) ] unknown Terminating not Left-Linear, not Right-Linear unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ join(?x,meet(?x,?y)) -> ?x, meet(?x,join(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)), meet(?x,?x) -> ?x, join(?x,?x) -> ?x, meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)), meet(?x,?y) -> meet(?y,?x), join(join(?x,?y),?z) -> join(?x,join(?y,?z)), join(?x,?y) -> join(?y,?x) ] Sort Assignment: join : 24*24=>24 meet : 24*24=>24 maximal types: {24} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ join(?x,meet(?x,?y)) -> ?x, meet(?x,join(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)), meet(?x,?x) -> ?x, join(?x,?x) -> ?x, meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)), meet(?x,?y) -> meet(?y,?x), join(join(?x,?y),?z) -> join(?x,join(?y,?z)), join(?x,?y) -> join(?y,?x) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ join(?x,meet(?x,?y)) -> ?x, meet(?x,join(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)), meet(?x,?x) -> ?x, join(?x,?x) -> ?x, meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)), meet(?x,?y) -> meet(?y,?x), join(join(?x,?y),?z) -> join(?x,join(?y,?z)), join(?x,?y) -> join(?y,?x) ] Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge 109.trs: MAYBE (356 msec.)