Goal:
    b : byte
  ============================
   (NoConfusion_byte b b)


DEBUG:Going to execute:
destruct b

Goals:
  
  ============================
   (NoConfusion_byte "000" "000")

  
  ============================
   (NoConfusion_byte "001" "001")

  
  ============================
   (NoConfusion_byte "002" "002")

  
  ============================
   (NoConfusion_byte "003" "003")

  
  ============================
   (NoConfusion_byte "004" "004")

  
  ============================
   (NoConfusion_byte "005" "005")

  
  ============================
   (NoConfusion_byte "006" "006")

  
  ============================
   (NoConfusion_byte "007" "007")

  
  ============================
   (NoConfusion_byte "008" "008")

  
  ============================
   (NoConfusion_byte "009" "009")

  
  ============================
   (NoConfusion_byte "010" "010")

  
  ============================
   (NoConfusion_byte "011" "011")

  
  ============================
   (NoConfusion_byte "012" "012")

  
  ============================
   (NoConfusion_byte "013" "013")

  
  ============================
   (NoConfusion_byte "014" "014")

  
  ============================
   (NoConfusion_byte "015" "015")

  
  ============================
   (NoConfusion_byte "016" "016")

  
  ============================
   (NoConfusion_byte "017" "017")

  
  ============================
   (NoConfusion_byte "018" "018")

  
  ============================
   (NoConfusion_byte "019" "019")

  
  ============================
   (NoConfusion_byte "020" "020")

  
  ============================
   (NoConfusion_byte "021" "021")

  
  ============================
   (NoConfusion_byte "022" "022")

  
  ============================
   (NoConfusion_byte "023" "023")

  
  ============================
   (NoConfusion_byte "024" "024")

  
  ============================
   (NoConfusion_byte "025" "025")

  
  ============================
   (NoConfusion_byte "026" "026")

  
  ============================
   (NoConfusion_byte "027" "027")

  
  ============================
   (NoConfusion_byte "028" "028")

  
  ============================
   (NoConfusion_byte "029" "029")

  
  ============================
   (NoConfusion_byte "030" "030")

  
  ============================
   (NoConfusion_byte "031" "031")

  
  ============================
   (NoConfusion_byte " " " ")

  
  ============================
   (NoConfusion_byte "!" "!")

  
  ============================
   (NoConfusion_byte """" """")

  
  ============================
   (NoConfusion_byte "#" "#")

  
  ============================
   (NoConfusion_byte "$" "$")

  
  ============================
   (NoConfusion_byte "%" "%")

  
  ============================
   (NoConfusion_byte "&" "&")

  
  ============================
   (NoConfusion_byte "'" "'")

  
  ============================
   (NoConfusion_byte "(" "(")

  
  ============================
   (NoConfusion_byte ")" ")")

  
  ============================
   (NoConfusion_byte "*" "*")

  
  ============================
   (NoConfusion_byte "+" "+")

  
  ============================
   (NoConfusion_byte "," ",")

  
  ============================
   (NoConfusion_byte "-" "-")

  
  ============================
   (NoConfusion_byte "." ".")

  
  ============================
   (NoConfusion_byte "/" "/")

  
  ============================
   (NoConfusion_byte "0" "0")

  
  ============================
   (NoConfusion_byte "1" "1")

  
  ============================
   (NoConfusion_byte "2" "2")

  
  ============================
   (NoConfusion_byte "3" "3")

  
  ============================
   (NoConfusion_byte "4" "4")

  
  ============================
   (NoConfusion_byte "5" "5")

  
  ============================
   (NoConfusion_byte "6" "6")

  
  ============================
   (NoConfusion_byte "7" "7")

  
  ============================
   (NoConfusion_byte "8" "8")

  
  ============================
   (NoConfusion_byte "9" "9")

  
  ============================
   (NoConfusion_byte ":" ":")

  
  ============================
   (NoConfusion_byte ";" ";")

  
  ============================
   (NoConfusion_byte "<" "<")

  
  ============================
   (NoConfusion_byte "=" "=")

  
  ============================
   (NoConfusion_byte ">" ">")

  
  ============================
   (NoConfusion_byte "?" "?")

  
  ============================
   (NoConfusion_byte "@" "@")

  
  ============================
   (NoConfusion_byte "A" "A")

  
  ============================
   (NoConfusion_byte "B" "B")

  
  ============================
   (NoConfusion_byte "C" "C")

  
  ============================
   (NoConfusion_byte "D" "D")

  
  ============================
   (NoConfusion_byte "E" "E")

  
  ============================
   (NoConfusion_byte "F" "F")

  
  ============================
   (NoConfusion_byte "G" "G")

  
  ============================
   (NoConfusion_byte "H" "H")

  
  ============================
   (NoConfusion_byte "I" "I")

  
  ============================
   (NoConfusion_byte "J" "J")

  
  ============================
   (NoConfusion_byte "K" "K")

  
  ============================
   (NoConfusion_byte "L" "L")

  
  ============================
   (NoConfusion_byte "M" "M")

  
  ============================
   (NoConfusion_byte "N" "N")

  
  ============================
   (NoConfusion_byte "O" "O")

  
  ============================
   (NoConfusion_byte "P" "P")

  
  ============================
   (NoConfusion_byte "Q" "Q")

  
  ============================
   (NoConfusion_byte "R" "R")

  
  ============================
   (NoConfusion_byte "S" "S")

  
  ============================
   (NoConfusion_byte "T" "T")

  
  ============================
   (NoConfusion_byte "U" "U")

  
  ============================
   (NoConfusion_byte "V" "V")

  
  ============================
   (NoConfusion_byte "W" "W")

  
  ============================
   (NoConfusion_byte "X" "X")

  
  ============================
   (NoConfusion_byte "Y" "Y")

  
  ============================
   (NoConfusion_byte "Z" "Z")

  
  ============================
   (NoConfusion_byte "[" "[")

  
  ============================
   (NoConfusion_byte "\" "\")

  
  ============================
   (NoConfusion_byte "]" "]")

  
  ============================
   (NoConfusion_byte "^" "^")

  
  ============================
   (NoConfusion_byte "_" "_")

  
  ============================
   (NoConfusion_byte "`" "`")

  
  ============================
   (NoConfusion_byte "a" "a")

  
  ============================
   (NoConfusion_byte "b" "b")

  
  ============================
   (NoConfusion_byte "c" "c")

  
  ============================
   (NoConfusion_byte "d" "d")

  
  ============================
   (NoConfusion_byte "e" "e")

  
  ============================
   (NoConfusion_byte "f" "f")

  
  ============================
   (NoConfusion_byte "g" "g")

  
  ============================
   (NoConfusion_byte "h" "h")

  
  ============================
   (NoConfusion_byte "i" "i")

  
  ============================
   (NoConfusion_byte "j" "j")

  
  ============================
   (NoConfusion_byte "k" "k")

  
  ============================
   (NoConfusion_byte "l" "l")

  
  ============================
   (NoConfusion_byte "m" "m")

  
  ============================
   (NoConfusion_byte "n" "n")

  
  ============================
   (NoConfusion_byte "o" "o")

  
  ============================
   (NoConfusion_byte "p" "p")

  
  ============================
   (NoConfusion_byte "q" "q")

  
  ============================
   (NoConfusion_byte "r" "r")

  
  ============================
   (NoConfusion_byte "s" "s")

  
  ============================
   (NoConfusion_byte "t" "t")

  
  ============================
   (NoConfusion_byte "u" "u")

  
  ============================
   (NoConfusion_byte "v" "v")

  
  ============================
   (NoConfusion_byte "w" "w")

  
  ============================
   (NoConfusion_byte "x" "x")

  
  ============================
   (NoConfusion_byte "y" "y")

  
  ============================
   (NoConfusion_byte "z" "z")

  
  ============================
   (NoConfusion_byte "{" "{")

  
  ============================
   (NoConfusion_byte "|" "|")

  
  ============================
   (NoConfusion_byte "}" "}")

  
  ============================
   (NoConfusion_byte "~" "~")

  
  ============================
   (NoConfusion_byte "127" "127")

  
  ============================
   (NoConfusion_byte "128" "128")

  
  ============================
   (NoConfusion_byte "129" "129")

  
  ============================
   (NoConfusion_byte "130" "130")

  
  ============================
   (NoConfusion_byte "131" "131")

  
  ============================
   (NoConfusion_byte "132" "132")

  
  ============================
   (NoConfusion_byte "133" "133")

  
  ============================
   (NoConfusion_byte "134" "134")

  
  ============================
   (NoConfusion_byte "135" "135")

  
  ============================
   (NoConfusion_byte "136" "136")

  
  ============================
   (NoConfusion_byte "137" "137")

  
  ============================
   (NoConfusion_byte "138" "138")

  
  ============================
   (NoConfusion_byte "139" "139")

  
  ============================
   (NoConfusion_byte "140" "140")

  
  ============================
   (NoConfusion_byte "141" "141")

  
  ============================
   (NoConfusion_byte "142" "142")

  
  ============================
   (NoConfusion_byte "143" "143")

  
  ============================
   (NoConfusion_byte "144" "144")

  
  ============================
   (NoConfusion_byte "145" "145")

  
  ============================
   (NoConfusion_byte "146" "146")

  
  ============================
   (NoConfusion_byte "147" "147")

  
  ============================
   (NoConfusion_byte "148" "148")

  
  ============================
   (NoConfusion_byte "149" "149")

  
  ============================
   (NoConfusion_byte "150" "150")

  
  ============================
   (NoConfusion_byte "151" "151")

  
  ============================
   (NoConfusion_byte "152" "152")

  
  ============================
   (NoConfusion_byte "153" "153")

  
  ============================
   (NoConfusion_byte "154" "154")

  
  ============================
   (NoConfusion_byte "155" "155")

  
  ============================
   (NoConfusion_byte "156" "156")

  
  ============================
   (NoConfusion_byte "157" "157")

  
  ============================
   (NoConfusion_byte "158" "158")

  
  ============================
   (NoConfusion_byte "159" "159")

  
  ============================
   (NoConfusion_byte "160" "160")

  
  ============================
   (NoConfusion_byte "161" "161")

  
  ============================
   (NoConfusion_byte "162" "162")

  
  ============================
   (NoConfusion_byte "163" "163")

  
  ============================
   (NoConfusion_byte "164" "164")

  
  ============================
   (NoConfusion_byte "165" "165")

  
  ============================
   (NoConfusion_byte "166" "166")

  
  ============================
   (NoConfusion_byte "167" "167")

  
  ============================
   (NoConfusion_byte "168" "168")

  
  ============================
   (NoConfusion_byte "169" "169")

  
  ============================
   (NoConfusion_byte "170" "170")

  
  ============================
   (NoConfusion_byte "171" "171")

  
  ============================
   (NoConfusion_byte "172" "172")

  
  ============================
   (NoConfusion_byte "173" "173")

  
  ============================
   (NoConfusion_byte "174" "174")

  
  ============================
   (NoConfusion_byte "175" "175")

  
  ============================
   (NoConfusion_byte "176" "176")

  
  ============================
   (NoConfusion_byte "177" "177")

  
  ============================
   (NoConfusion_byte "178" "178")

  
  ============================
   (NoConfusion_byte "179" "179")

  
  ============================
   (NoConfusion_byte "180" "180")

  
  ============================
   (NoConfusion_byte "181" "181")

  
  ============================
   (NoConfusion_byte "182" "182")

  
  ============================
   (NoConfusion_byte "183" "183")

  
  ============================
   (NoConfusion_byte "184" "184")

  
  ============================
   (NoConfusion_byte "185" "185")

  
  ============================
   (NoConfusion_byte "186" "186")

  
  ============================
   (NoConfusion_byte "187" "187")

  
  ============================
   (NoConfusion_byte "188" "188")

  
  ============================
   (NoConfusion_byte "189" "189")

  
  ============================
   (NoConfusion_byte "190" "190")

  
  ============================
   (NoConfusion_byte "191" "191")

  
  ============================
   (NoConfusion_byte "192" "192")

  
  ============================
   (NoConfusion_byte "193" "193")

  
  ============================
   (NoConfusion_byte "194" "194")

  
  ============================
   (NoConfusion_byte "195" "195")

  
  ============================
   (NoConfusion_byte "196" "196")

  
  ============================
   (NoConfusion_byte "197" "197")

  
  ============================
   (NoConfusion_byte "198" "198")

  
  ============================
   (NoConfusion_byte "199" "199")

  
  ============================
   (NoConfusion_byte "200" "200")

  
  ============================
   (NoConfusion_byte "201" "201")

  
  ============================
   (NoConfusion_byte "202" "202")

  
  ============================
   (NoConfusion_byte "203" "203")

  
  ============================
   (NoConfusion_byte "204" "204")

  
  ============================
   (NoConfusion_byte "205" "205")

  
  ============================
   (NoConfusion_byte "206" "206")

  
  ============================
   (NoConfusion_byte "207" "207")

  
  ============================
   (NoConfusion_byte "208" "208")

  
  ============================
   (NoConfusion_byte "209" "209")

  
  ============================
   (NoConfusion_byte "210" "210")

  
  ============================
   (NoConfusion_byte "211" "211")

  
  ============================
   (NoConfusion_byte "212" "212")

  
  ============================
   (NoConfusion_byte "213" "213")

  
  ============================
   (NoConfusion_byte "214" "214")

  
  ============================
   (NoConfusion_byte "215" "215")

  
  ============================
   (NoConfusion_byte "216" "216")

  
  ============================
   (NoConfusion_byte "217" "217")

  
  ============================
   (NoConfusion_byte "218" "218")

  
  ============================
   (NoConfusion_byte "219" "219")

  
  ============================
   (NoConfusion_byte "220" "220")

  
  ============================
   (NoConfusion_byte "221" "221")

  
  ============================
   (NoConfusion_byte "222" "222")

  
  ============================
   (NoConfusion_byte "223" "223")

  
  ============================
   (NoConfusion_byte "224" "224")

  
  ============================
   (NoConfusion_byte "225" "225")

  
  ============================
   (NoConfusion_byte "226" "226")

  
  ============================
   (NoConfusion_byte "227" "227")

  
  ============================
   (NoConfusion_byte "228" "228")

  
  ============================
   (NoConfusion_byte "229" "229")

  
  ============================
   (NoConfusion_byte "230" "230")

  
  ============================
   (NoConfusion_byte "231" "231")

  
  ============================
   (NoConfusion_byte "232" "232")

  
  ============================
   (NoConfusion_byte "233" "233")

  
  ============================
   (NoConfusion_byte "234" "234")

  
  ============================
   (NoConfusion_byte "235" "235")

  
  ============================
   (NoConfusion_byte "236" "236")

  
  ============================
   (NoConfusion_byte "237" "237")

  
  ============================
   (NoConfusion_byte "238" "238")

  
  ============================
   (NoConfusion_byte "239" "239")

  
  ============================
   (NoConfusion_byte "240" "240")

  
  ============================
   (NoConfusion_byte "241" "241")

  
  ============================
   (NoConfusion_byte "242" "242")

  
  ============================
   (NoConfusion_byte "243" "243")

  
  ============================
   (NoConfusion_byte "244" "244")

  
  ============================
   (NoConfusion_byte "245" "245")

  
  ============================
   (NoConfusion_byte "246" "246")

  
  ============================
   (NoConfusion_byte "247" "247")

  
  ============================
   (NoConfusion_byte "248" "248")

  
  ============================
   (NoConfusion_byte "249" "249")

  
  ============================
   (NoConfusion_byte "250" "250")

  
  ============================
   (NoConfusion_byte "251" "251")

  
  ============================
   (NoConfusion_byte "252" "252")

  
  ============================
   (NoConfusion_byte "253" "253")

  
  ============================
   (NoConfusion_byte "254" "254")

  
  ============================
   (NoConfusion_byte "255" "255")


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: b

Goals:
  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True

  
  ============================
   True


DEBUG:Going to execute:
exact I