unionemptyXXmaxsinglxxmaxunionsinglxsingl0xmaxunionsinglsxsinglsysmaxunionsinglxsinglymaxunionsinglxunionYZmaxunionsinglxsinglmaxunionYZunionunion2.11union21211empty01max111singl111000s111unionemptyXX1union21211max111singl111003s111maxunionsinglxsingl0x2union222221112max111singl111s1111maxunionsinglsxsinglsysmaxunionsinglxsinglyunionxyunionyxunionunionxyzunionxunionyzmaxunionsinglxunionYZmaxunionsinglxsinglmaxunionYZmaxunionsinglxunionYZmaxunionYZ1union221112max111singl111max121maxunionsinglxunionYZmaxunionYZmaxsinglxxmaxunionsinglxunionYZmaxunionsinglxsinglmaxunionYZunionxyunionyxunionunionxyzunionxunionyz1max111union211112singl10max10maxunionsinglxunionYZmaxunionsinglxsinglmaxunionYZunionunionxyzunionxunionyzunionxyunionyxAProVEAProVE Commit ID: f0658065a3d9bb0113f6aab7d64dab3d35253877 ffrohn 20160816 unpublished Statistics for single proof: 100.00 % (7 real / 0 unknown / 0 assumptions / 7 total proof steps)http://aprove.informatik.rwth-aachen.deJohnDoe