[runlim] version: 1.7 [runlim] time limit: 3600 seconds [runlim] real time limit: 311040000 seconds [runlim] space limit: 4294967069 MB [runlim] argv[0]: /home/zhouyan/BACH/armc [runlim] argv[1]: live [runlim] argv[2]: /home/zhouyan/BACH/tmpFile20141130191833.armc [runlim] argv[3]: -straight [runlim] start: Sun Nov 30 19:22:44 2014 [runlim] main pid: 1189 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [live,/home/zhouyan/BACH/tmpFile20141130191833.armc,-straight] reading input from /home/zhouyan/BACH/tmpFile20141130191833.armc...done. creating straight line code between cutpoints...done. meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [31]). meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [30]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v8),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [29]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [28]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [27]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v7),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [26]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [25]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [24]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v6),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [23]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v5),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [22]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [21]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [20]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [19]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [18]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], [17]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [16]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v2),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [15]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [14]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v3),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [13]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], [12]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,_)), p(pc(v4),data(I,J,K,L,M,N,O,P,Q)), [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D<4,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5,Q>0,O-P<10,O-P>0,N-O<10,N-O>0,M-N<10,M-N>0,L-M<10,L-M>0,K-L<10,K-L>0,J-K<10,J-K>0,I-J<10,I-J>0], [11]). meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I)), p(pc(v8),data(J,K,L,M,N,O,P,Q,R)), [], [Q=H+10*I,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [9]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I)), p(pc(v7),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P=G+10*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [8]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I)), p(pc(v6),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O=F+10*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [7]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I)), p(pc(v5),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O==F+8*I,N=E+10*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [6]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I)), p(pc(v3),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L=C+10*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [5]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K==B+8*I,J==A+8*I,R>0,I>0,P-Q<10,G-H<10,P-Q>5,G-H>5,O-P<10,F-G<10,O-P>5,F-G>5,N-O<10,E-F<10,N-O>5,E-F>5,M-N<10,D-E<10,M-N>5,D-E>5,L-M<10,C-D<10,L-M>5,C-D>5,K-L<10,B-C<10,K-L>5,B-C>5,J-K<10,A-B<10,J-K>5,A-B>5], [4]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I)), p(pc(v4),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M=D+10*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [3]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I)), p(pc(v2),data(J,K,L,M,N,O,P,Q,R)), [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K=B+10*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], [2]). meta_transition(p(pc(err),data(A,B,C,D,E,F,G,H,I)), p(pc(err),data(J,K,L,M,N,O,P,Q,R)), [], [Q=H,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0], [1]). meta_transition(p(pc(v0),data(_,_,_,_,_,_,_,_,_)), p(pc(v1),data(A,B,C,D,E,F,G,H,I)), [], [H=25.0,G=30.0,F=35.0,E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,I>0,G-H<10,G-H>5,F-G<10,F-G>5,E-F<10,E-F>5,D-E<10,D-E>5,C-D<10,C-D>5,B-C<10,B-C>5,A-B<10,A-B>5], [10]). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([31])). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,G-H>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([30])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([28])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,F-G>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([27])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([25])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,E-F>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([24])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([21])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,D-E>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([20])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([19])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([18])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,_)), p(pc(err),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B<1,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0], tid([17])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,A-B>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([16])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,B-C>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([14])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,_)), p(pc(v1),data(I,J,K,L,M,N,O,P,Q)), {P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5}, [], [P=H,O=G,N=F,M=E,L=D,K=C,J=B,I=A,C-D>4,G-H<10,G-H>0,F-G<10,F-G>0,E-F<10,E-F>0,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,Q>0,O-P<10,O-P>5,N-O<10,N-O>5,M-N<10,M-N>5,L-M<10,L-M>5,K-L<10,K-L>5,J-K<10,J-K>5,I-J<10,I-J>5], tid([12])). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I)), p(pc(v8),data(J,K,L,M,N,O,P,Q,R)), {Q=H+10*I,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q=H+10*I,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([9])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I)), p(pc(v7),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P=G+10*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P=G+10*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([8])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I)), p(pc(v6),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O=F+10*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P==G+8*I,O=F+10*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([7])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I)), p(pc(v5),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O==F+8*I,N=E+10*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P==G+8*I,O==F+8*I,N=E+10*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([6])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I)), p(pc(v3),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L=C+10*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L=C+10*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([5])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K==B+8*I,J==A+8*I,R>0,I>0,P-Q<10,G-H<10,P-Q>5,G-H>5,O-P<10,F-G<10,O-P>5,F-G>5,N-O<10,E-F<10,N-O>5,E-F>5,M-N<10,D-E<10,M-N>5,D-E>5,L-M<10,C-D<10,L-M>5,C-D>5,K-L<10,B-C<10,K-L>5,B-C>5,J-K<10,A-B<10,J-K>5,A-B>5}, [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K==B+8*I,J==A+8*I,R>0,I>0,P-Q<10,G-H<10,P-Q>5,G-H>5,O-P<10,F-G<10,O-P>5,F-G>5,N-O<10,E-F<10,N-O>5,E-F>5,M-N<10,D-E<10,M-N>5,D-E>5,L-M<10,C-D<10,L-M>5,C-D>5,K-L<10,B-C<10,K-L>5,B-C>5,J-K<10,A-B<10,J-K>5,A-B>5], tid([4])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I)), p(pc(v4),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M=D+10*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M=D+10*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([3])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I)), p(pc(v2),data(J,K,L,M,N,O,P,Q,R)), {Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K=B+10*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0}, [], [Q==H+8*I,P==G+8*I,O==F+8*I,N==E+8*I,M==D+8*I,L==C+8*I,K=B+10*I,J=A+12*I,R>0,I>0,P-Q<10,G-H<10,P-Q>0,G-H>0,O-P<10,F-G<10,O-P>0,F-G>0,N-O<10,E-F<10,N-O>0,E-F>0,M-N<10,D-E<10,M-N>0,D-E>0,L-M<10,C-D<10,L-M>0,C-D>0,K-L<10,B-C<10,K-L>0,B-C>0,J-K<10,A-B<10,J-K>0,A-B>0], tid([2])). transition(p(pc(err),data(A,B,C,D,E,F,G,H,I)), p(pc(err),data(J,K,L,M,N,O,P,Q,R)), {Q=H,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0}, [], [Q=H,P=G+12*I,O=F+12*I,N=E+12*I,M=D+12*I,L=C+12*I,K=B+12*I,J=A+12*I,R>0,I>0], tid([1])). tid([31]): pc(v8) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([30]): pc(v8) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([28]): pc(v7) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([27]): pc(v7) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([25]): pc(v6) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([24]): pc(v6) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([21]): pc(v5) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([20]): pc(v5) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([19]): pc(v4) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([18]): pc(v3) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([17]): pc(v2) pc(err) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0] tid([16]): pc(v2) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([14]): pc(v3) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([12]): pc(v4) pc(v1) {x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5} [] [x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x7-x8<10,x7-x8>0,x6-x7<10,x6-x7>0,x5-x6<10,x5-x6>0,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x7'-x8'<10,x7'-x8'>5,x6'-x7'<10,x6'-x7'>5,x5'-x6'<10,x5'-x6'>5,x4'-x5'<10,x4'-x5'>5,x3'-x4'<10,x3'-x4'>5,x2'-x3'<10,x2'-x3'>5,x1'-x2'<10,x1'-x2'>5] tid([9]): pc(v8) pc(v8) {x8'=x8+10*t,x7'=x7+12*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'=x8+10*t,x7'=x7+12*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([8]): pc(v7) pc(v7) {x8'==x8+8*t,x7'=x7+10*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'=x7+10*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([7]): pc(v6) pc(v6) {x8'==x8+8*t,x7'==x7+8*t,x6'=x6+10*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'==x7+8*t,x6'=x6+10*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([6]): pc(v5) pc(v5) {x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'=x5+10*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'=x5+10*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([5]): pc(v3) pc(v3) {x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'=x3+10*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'=x3+10*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([4]): pc(v1) pc(v1) {x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'==x3+8*t,x2'==x2+8*t,x1'==x1+8*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>5,x7-x8>5,x6'-x7'<10,x6-x7<10,x6'-x7'>5,x6-x7>5,x5'-x6'<10,x5-x6<10,x5'-x6'>5,x5-x6>5,x4'-x5'<10,x4-x5<10,x4'-x5'>5,x4-x5>5,x3'-x4'<10,x3-x4<10,x3'-x4'>5,x3-x4>5,x2'-x3'<10,x2-x3<10,x2'-x3'>5,x2-x3>5,x1'-x2'<10,x1-x2<10,x1'-x2'>5,x1-x2>5} [] [x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'==x3+8*t,x2'==x2+8*t,x1'==x1+8*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>5,x7-x8>5,x6'-x7'<10,x6-x7<10,x6'-x7'>5,x6-x7>5,x5'-x6'<10,x5-x6<10,x5'-x6'>5,x5-x6>5,x4'-x5'<10,x4-x5<10,x4'-x5'>5,x4-x5>5,x3'-x4'<10,x3-x4<10,x3'-x4'>5,x3-x4>5,x2'-x3'<10,x2-x3<10,x2'-x3'>5,x2-x3>5,x1'-x2'<10,x1-x2<10,x1'-x2'>5,x1-x2>5] tid([3]): pc(v4) pc(v4) {x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'=x4+10*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'=x4+10*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([2]): pc(v2) pc(v2) {x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'==x3+8*t,x2'=x2+10*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0} [] [x8'==x8+8*t,x7'==x7+8*t,x6'==x6+8*t,x5'==x5+8*t,x4'==x4+8*t,x3'==x3+8*t,x2'=x2+10*t,x1'=x1+12*t,t'>0,t>0,x7'-x8'<10,x7-x8<10,x7'-x8'>0,x7-x8>0,x6'-x7'<10,x6-x7<10,x6'-x7'>0,x6-x7>0,x5'-x6'<10,x5-x6<10,x5'-x6'>0,x5-x6>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0] tid([1]): pc(err) pc(err) {x8'=x8,x7'=x7+12*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0} [] [x8'=x8,x7'=x7+12*t,x6'=x6+12*t,x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0] -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 ================================================== ARMC-LIVE: program is correct abstract trans fixpoint abstract_trans_state(0, pc(v0), pc(v0), [], stem, 1, (0,0)). frontier 0: stem 1 (pc(v0)->pc(v0)) from 0 by appying 0: T _30014->_30017: #0: Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.00, wall 0.00 s. Time on cli constraint preparation: run 0.00, wall 0.00 s. Time on cli matrix parsing: run 0.00, wall 0.00 s. Time on cli preprocessing: run 0.00, wall 0.00 s. Time on computing the subsumer subtree: run 0.00, wall 0.00 s. Time on finding the location of subsumer in queue: run 0.00, wall 0.00 s. Time on asserting thick transitions: run 0.00, wall 0.00 s. Time on path invariant generation: run 0.00, wall 0.00 s. Time on new predicate selection: run 0.00, wall 0.00 s. Time on refinement preprocessing cut: run 0.00, wall 0.00 s. Time on refinement cutting trace: run 0.00, wall 0.00 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.00 s. Time on refinement: run 0.00, wall 0.00 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 0.00, wall 0.00 s. Time on fixpoint test: run 0.00, wall 0.00 s. Time on abstract check: run 0.00, wall 0.00 s. Time on total including result checking: run 0.00, wall 0.00 s. Time on check result: run 0.00, wall 0.00 s. Time on total: run 0.00, wall 0.00 s. ================================================== ARMC-LIVE: program is correct [runlim] end: Sun Nov 30 19:22:44 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 0.98 seconds [runlim] time: 0.09 seconds [runlim] space: 5.6 MB [runlim] samples: 2