# MC: formula failed --- AG((((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))))
# MC: Calling debugger for trace 1
--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails AG((((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))))

since (((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))) is false at this state
--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes (((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes (((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes (((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes (((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes (decoder.state<9>=0 * decoder.state<8>=0).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<9>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<8>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<7>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<6>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<5>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<4>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<3>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<2>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<1>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes decoder.state<0>=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))

 --Counter example begins
--State 0:
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:0
character<1>:0
character<2>:0
character<3>:0
character<4>:0
character<5>:0
character<6>:0
character<7>:0
ci:0
decoder.state<0>:0
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0

--Goes to state 1:
character<0>:1
character<3>:1
character<6>:1
decoder.state<0>:1
encoder.shiftreg<0>:1
encoder.shiftreg<4>:1
start:1

 --Counter example ends


--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:1
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:1
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:1
fails (ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))).

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:1
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:1
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:1
passes ci=0.

--State
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:1
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:1
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:1
fails AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))

 --Counter example begins
--State 0:
ch<0>:0
ch<1>:0
ch<2>:0
ch<3>:0
ch<4>:0
ch<5>:0
ch<6>:0
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:1
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:0
encoder.shiftreg<4>:1
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:1

--Goes to state 1:
ch<0>:1
ch<3>:1
ch<6>:1
ci:1
decoder.state<0>:0
decoder.state<1>:1
encoder.shiftreg<0>:0
encoder.shiftreg<3>:1
encoder.shiftreg<4>:0
start:0

 --Counter example ends


--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:1
decoder.state<0>:0
decoder.state<1>:1
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:1
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:1
decoder.state<0>:0
decoder.state<1>:1
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:1
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ci=1.

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:1
decoder.state<0>:0
decoder.state<1>:1
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:1
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))

 --Counter example begins
--State 0:
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:1
decoder.state<0>:0
decoder.state<1>:1
decoder.state<2>:0
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:0
encoder.shiftreg<3>:1
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0

--Goes to state 1:
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0

 --Counter example ends


--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes ci=0.

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails ((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails ((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails ((plain<7>=0 * plain<6>=1) * plain<5>=0).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails (plain<7>=0 * plain<6>=1).

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
passes plain<7>=0.

--State
ch<0>:1
ch<1>:0
ch<2>:0
ch<3>:1
ch<4>:0
ch<5>:0
ch<6>:1
ch<7>:0
character<0>:1
character<1>:0
character<2>:0
character<3>:1
character<4>:0
character<5>:0
character<6>:1
character<7>:0
ci:0
decoder.state<0>:1
decoder.state<1>:0
decoder.state<2>:1
decoder.state<3>:0
decoder.state<4>:0
decoder.state<5>:0
decoder.state<6>:0
decoder.state<7>:0
decoder.state<8>:0
decoder.state<9>:0
encoder.shiftreg<0>:0
encoder.shiftreg<1>:0
encoder.shiftreg<2>:1
encoder.shiftreg<3>:0
encoder.shiftreg<4>:0
encoder.shiftreg<5>:0
encoder.shiftreg<6>:0
encoder.shiftreg<7>:0
encoder.shiftreg<8>:0
encoder.shiftreg<9>:0
start:0
fails plain<6>=1.