[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/tmpFile20141130191851.armc [runlim] argv[3]: -straight [runlim] start: Sun Nov 30 19:22:44 2014 [runlim] main pid: 1917 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [live,/home/zhouyan/BACH/tmpFile20141130191851.armc,-straight] reading input from /home/zhouyan/BACH/tmpFile20141130191851.armc...done. creating straight line code between cutpoints...done. meta_transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<1,H-I<10,H-I>0,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,S>0], [35]). meta_transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [34]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v9),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [33]). meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<1,H-I<10,H-I>0,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,S>0], [32]). meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [31]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v8),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [30]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<1,H-I<10,H-I>0,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,S>0], [29]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [28]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v7),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [27]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<1,H-I<10,H-I>0,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,S>0], [26]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [25]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v6),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [24]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v5),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [23]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<1,H-I<10,H-I>0,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,S>0], [22]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [21]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<1,H-I<10,H-I>0,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,S>0], [20]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<1,H-I<10,H-I>0,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,S>0], [19]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<1,H-I<10,H-I>0,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,S>0], [18]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [17]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v2),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [16]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [15]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v3),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [14]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], [13]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v4),data(J,K,L,M,N,O,P,Q,R,S)), [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], [12]). meta_transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v9),data(K,L,M,N,O,P,Q,R,S,T)), [], [S=I+10*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [10]). meta_transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v8),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R=H+10*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [9]). meta_transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v7),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q=G+10*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [8]). meta_transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v6),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P=F+10*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [7]). meta_transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v5),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O=E+10*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [6]). meta_transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v3),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M=C+10*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [5]). meta_transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v1),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L==B+8*J,K==A+8*J,T>0,J>0,R-S<10,H-I<10,R-S>2,H-I>2,Q-R<10,G-H<10,Q-R>2,G-H>2,P-Q<10,F-G<10,P-Q>2,F-G>2,O-P<10,E-F<10,O-P>2,E-F>2,N-O<10,D-E<10,N-O>2,D-E>2,M-N<10,C-D<10,M-N>2,C-D>2,L-M<10,B-C<10,L-M>2,B-C>2,K-L<10,A-B<10,K-L>2,A-B>2], [4]). meta_transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v4),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N=D+10*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [3]). meta_transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v2),data(K,L,M,N,O,P,Q,R,S,T)), [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L=B+10*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], [2]). meta_transition(p(pc(err),data(A,B,C,D,E,F,G,H,I,J)), p(pc(err),data(K,L,M,N,O,P,Q,R,S,T)), [], [S=I+12*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0], [1]). meta_transition(p(pc(v0),data(_,_,_,_,_,_,_,_,_,_)), p(pc(v1),data(A,B,C,D,E,F,G,H,I,J)), [], [I=20.0,H=25.0,G=30.0,F=35.0,E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,J>0,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2], [11]). transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<1,H-I<10,H-I>0,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,S>0], tid([35])). transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([34])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v9),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,H-I<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([33])). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<1,H-I<10,H-I>0,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,S>0], tid([32])). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([31])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v8),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,G-H<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([30])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<1,H-I<10,H-I>0,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,S>0], tid([29])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([28])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v7),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,F-G<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([27])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<1,H-I<10,H-I>0,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,S>0], tid([26])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([25])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v6),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,E-F<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([24])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v5),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([23])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E<1,H-I<10,H-I>0,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,S>0], tid([22])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,D-E>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([21])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<1,H-I<10,H-I>0,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,S>0], tid([20])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<1,H-I<10,H-I>0,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,S>0], tid([19])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,_)), p(pc(err),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<1,H-I<10,H-I>0,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,S>0}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<1,H-I<10,H-I>0,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,S>0], tid([18])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([17])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v2),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,A-B<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([16])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([15])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v3),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,B-C<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([14])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v1),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D>4,H-I<10,H-I>0,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,S>0,Q-R<10,Q-R>2,P-Q<10,P-Q>2,O-P<10,O-P>2,N-O<10,N-O>2,M-N<10,M-N>2,L-M<10,L-M>2,K-L<10,K-L>2,J-K<10,J-K>2], tid([13])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,_)), p(pc(v4),data(J,K,L,M,N,O,P,Q,R,S)), {R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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}, [], [R=I,Q=H,P=G,O=F,N=E,M=D,L=C,K=B,J=A,C-D<4,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,S>0,Q-R<10,Q-R>0,P-Q<10,P-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], tid([12])). transition(p(pc(v9),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v9),data(K,L,M,N,O,P,Q,R,S,T)), {S=I+10*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S=I+10*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([10])). transition(p(pc(v8),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v8),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R=H+10*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R=H+10*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([9])). transition(p(pc(v7),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v7),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q=G+10*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q=G+10*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([8])). transition(p(pc(v6),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v6),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P=F+10*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P=F+10*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([7])). transition(p(pc(v5),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v5),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O=E+10*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O=E+10*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([6])). transition(p(pc(v3),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v3),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M=C+10*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M=C+10*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([5])). transition(p(pc(v1),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v1),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L==B+8*J,K==A+8*J,T>0,J>0,R-S<10,H-I<10,R-S>2,H-I>2,Q-R<10,G-H<10,Q-R>2,G-H>2,P-Q<10,F-G<10,P-Q>2,F-G>2,O-P<10,E-F<10,O-P>2,E-F>2,N-O<10,D-E<10,N-O>2,D-E>2,M-N<10,C-D<10,M-N>2,C-D>2,L-M<10,B-C<10,L-M>2,B-C>2,K-L<10,A-B<10,K-L>2,A-B>2}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L==B+8*J,K==A+8*J,T>0,J>0,R-S<10,H-I<10,R-S>2,H-I>2,Q-R<10,G-H<10,Q-R>2,G-H>2,P-Q<10,F-G<10,P-Q>2,F-G>2,O-P<10,E-F<10,O-P>2,E-F>2,N-O<10,D-E<10,N-O>2,D-E>2,M-N<10,C-D<10,M-N>2,C-D>2,L-M<10,B-C<10,L-M>2,B-C>2,K-L<10,A-B<10,K-L>2,A-B>2], tid([4])). transition(p(pc(v4),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v4),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N=D+10*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N=D+10*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([3])). transition(p(pc(v2),data(A,B,C,D,E,F,G,H,I,J)), p(pc(v2),data(K,L,M,N,O,P,Q,R,S,T)), {S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L=B+10*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0}, [], [S==I+8*J,R==H+8*J,Q==G+8*J,P==F+8*J,O==E+8*J,N==D+8*J,M==C+8*J,L=B+10*J,K=A+12*J,T>0,J>0,R-S<10,H-I<10,R-S>0,H-I>0,Q-R<10,G-H<10,Q-R>0,G-H>0,P-Q<10,F-G<10,P-Q>0,F-G>0,O-P<10,E-F<10,O-P>0,E-F>0,N-O<10,D-E<10,N-O>0,D-E>0,M-N<10,C-D<10,M-N>0,C-D>0,L-M<10,B-C<10,L-M>0,B-C>0,K-L<10,A-B<10,K-L>0,A-B>0], tid([2])). transition(p(pc(err),data(A,B,C,D,E,F,G,H,I,J)), p(pc(err),data(K,L,M,N,O,P,Q,R,S,T)), {S=I+12*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0}, [], [S=I+12*J,R=H+12*J,Q=G+12*J,P=F+12*J,O=E+12*J,N=D+12*J,M=C+12*J,L=B+12*J,K=A+12*J,T>0,J>0], tid([1])). transition(p(pc(v0),data(_,_,_,_,_,_,_,_,_,_)), p(pc(v1),data(A,B,C,D,E,F,G,H,I,J)), {I=20.0,H=25.0,G=30.0,F=35.0,E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,J>0,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2}, [], [I=20.0,H=25.0,G=30.0,F=35.0,E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,J>0,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2,E-F<10,E-F>2,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2], tid([11])). tid([35]): pc(v9) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9<1,x8-x9<10,x8-x9>0,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([34]): pc(v9) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([33]): pc(v1) pc(v9) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x8-x9<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([32]): pc(v8) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<1,x8-x9<10,x8-x9>0,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([31]): pc(v8) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([30]): pc(v1) pc(v8) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x7-x8<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([29]): pc(v7) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<1,x8-x9<10,x8-x9>0,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([28]): pc(v7) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([27]): pc(v1) pc(v7) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x6-x7<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([26]): pc(v6) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<1,x8-x9<10,x8-x9>0,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([25]): pc(v6) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([24]): pc(v1) pc(v6) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x5-x6<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([23]): pc(v1) pc(v5) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([22]): pc(v5) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x8-x9<10,x8-x9>0,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([21]): pc(v5) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([20]): pc(v4) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x8-x9<10,x8-x9>0,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([19]): pc(v3) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x8-x9<10,x8-x9>0,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(v2) pc(err) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x8-x9<10,x8-x9>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x8-x9<10,x8-x9>0,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(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([16]): pc(v1) pc(v2) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([15]): pc(v3) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([14]): pc(v1) pc(v3) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([13]): pc(v4) pc(v1) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x8-x9<10,x8-x9>0,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'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] tid([12]): pc(v1) pc(v4) {x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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} [] [x9'=x9,x8'=x8,x7'=x7,x6'=x6,x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<4,x8-x9<10,x8-x9>2,x7-x8<10,x7-x8>2,x6-x7<10,x6-x7>2,x5-x6<10,x5-x6>2,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x8'-x9'<10,x8'-x9'>0,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] tid([10]): pc(v9) pc(v9) {x9'=x9+10*t,x8'=x8+12*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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'=x9+10*t,x8'=x8+12*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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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([9]): pc(v8) pc(v8) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>2,x8-x9>2,x7'-x8'<10,x7-x8<10,x7'-x8'>2,x7-x8>2,x6'-x7'<10,x6-x7<10,x6'-x7'>2,x6-x7>2,x5'-x6'<10,x5-x6<10,x5'-x6'>2,x5-x6>2,x4'-x5'<10,x4-x5<10,x4'-x5'>2,x4-x5>2,x3'-x4'<10,x3-x4<10,x3'-x4'>2,x3-x4>2,x2'-x3'<10,x2-x3<10,x2'-x3'>2,x2-x3>2,x1'-x2'<10,x1-x2<10,x1'-x2'>2,x1-x2>2} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>2,x8-x9>2,x7'-x8'<10,x7-x8<10,x7'-x8'>2,x7-x8>2,x6'-x7'<10,x6-x7<10,x6'-x7'>2,x6-x7>2,x5'-x6'<10,x5-x6<10,x5'-x6'>2,x5-x6>2,x4'-x5'<10,x4-x5<10,x4'-x5'>2,x4-x5>2,x3'-x4'<10,x3-x4<10,x3'-x4'>2,x3-x4>2,x2'-x3'<10,x2-x3<10,x2'-x3'>2,x2-x3>2,x1'-x2'<10,x1-x2<10,x1'-x2'>2,x1-x2>2] tid([3]): pc(v4) pc(v4) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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} [] [x9'==x9+8*t,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,x8'-x9'<10,x8-x9<10,x8'-x9'>0,x8-x9>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) {x9'=x9+12*t,x8'=x8+12*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} [] [x9'=x9+12*t,x8'=x8+12*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] tid([11]): pc(v0) pc(v1) {x9'=20.0,x8'=25.0,x7'=30.0,x6'=35.0,x5'=40.0,x4'=45.0,x3'=50.0,x2'=55.0,x1'=60.0,t'>0,x8'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2} [] [x9'=20.0,x8'=25.0,x7'=30.0,x6'=35.0,x5'=40.0,x4'=45.0,x3'=50.0,x2'=55.0,x1'=60.0,t'>0,x8'-x9'<10,x8'-x9'>2,x7'-x8'<10,x7'-x8'>2,x6'-x7'<10,x6'-x7'>2,x5'-x6'<10,x5'-x6'>2,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2] -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _42815->_42818: #0: projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([30])], loop [] trans preds: _19875->_19878: #0: projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x7'-x8'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x7'-x8'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _592514->_592517: #1: x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([27])], loop [] trans preds: _19716->_19719: #1: x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x6'-x7'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x6'-x7'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _589424->_589427: #2: x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([24])], loop [] trans preds: _19407->_19410: #2: x6'-x7'>=5, x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x5'-x6'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x5'-x6'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _595628->_595631: #3: x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([23])], loop [] trans preds: _18770->_18773: #3: x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x4'-x5'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x4'-x5'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _596034->_596037: #4: x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([16])], loop [] trans preds: _18310->_18313: #4: x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x1'-x2'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x1'-x2'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _625589->_625592: #5: x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([14])], loop [] trans preds: _17850->_17853: #5: x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x2'-x3'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x2'-x3'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _610482->_610485: #6: x2'-x3'>=5, x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([12])], loop [] trans preds: _17390->_17393: #6: x2'-x3'>=5, x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop infeasible: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): x3'-x4'>=5 refining stem cutting step 1 at pc(v1) LI at pc(v1): x3'-x4'>=5 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 abstract counterexample: stem [0,tid([11])], loop [tid([4])] trans preds: _605443->_605446: #7: x3'-x4'>=5, x2'-x3'>=5, x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1=60, x2=55, x3=50, x4=45, x5=40, x6=35, x7=30, x8=25, x9=20, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, x5'-x6'>2, x5'-x6'<10, x6'-x7'>2, x6'-x7'<10, x7'-x8'>2, x7'-x8'<10, x8'-x9'>2, x8'-x9'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t-1/8*x6'=< -35/8, t-1/8*x7'=< -15/4, t-1/8*x8'=< -25/8, t-1/8*x9'=< -5/2, t>0, t-1/10*x9'>= -2, t-1/10*x8'>= -5/2, t-1/10*x7'>= -3, t-1/10*x6'>= -7/2, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0 x1>=61 x1-x1'>= -7 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([11]),tid([4])], loop [] trans preds: _17097->_17100: #7: x3'-x4'>=5, x2'-x3'>=5, x1'-x2'>=5, x4'-x5'>=5, x5'-x6'>=5, x6'-x7'>=5, x7'-x8'>=5 projected loop: x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x9=<35, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x9=<30, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x9=<25, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-5/4*x9=<20, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-5/4*x9=<15, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-5/4*x9=<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-5/4*x9=<5, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x8-5/4*x9=<0, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x8=<115/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x8=<95/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x8=<75/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-5/4*x8=<55/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-5/4*x8=<35/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-5/4*x8=<15/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-5/4*x8=< -5/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x8-4/5*x9>=9, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x7=<45/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x7=<35/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x7=<25/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-5/4*x7=<15/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-5/4*x7=<5/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-5/4*x7=< -5/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-4/5*x8>=10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-4/5*x9>=14, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x6=<65/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x6=<45/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x6=<25/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-5/4*x6=<5/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-5/4*x6=< -15/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-4/5*x7>=11, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-4/5*x8>=15, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-4/5*x9>=19, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x5=<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x5=<5, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x5=<0, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-5/4*x5=< -5, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-4/5*x6>=12, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-4/5*x7>=16, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-4/5*x8>=20, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-4/5*x9>=24, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x4=<15/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x4=< -5/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-5/4*x4=< -25/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-4/5*x5>=13, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-4/5*x6>=17, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-4/5*x7>=21, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-4/5*x8>=25, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-4/5*x9>=29, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x3=< -5/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-5/4*x3=< -15/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x4>=14, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x5>=18, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x6>=22, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x7>=26, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x8>=30, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-4/5*x9>=34, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-5/4*x2=< -35/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x3>=15, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x4>=19, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x5>=23, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x6>=27, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x7>=31, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x8>=35, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-4/5*x9>=39, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x2>=16, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x3>=20, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x4>=24, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x5>=28, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x6>=32, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x7>=36, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x8>=40, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-4/5*x9>=44, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1>60, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-x2>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x1-x2<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-x3>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x2-x3<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-x4>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x3-x4<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-x5>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x4-x5<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-x6>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x5-x6<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-x7>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x6-x7<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-x8>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x7-x8<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x8-x9>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, x8-x9<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, x6'=x6, x7'=x7, x8'=x8, x9'=x9, t'=t, t>0 ================================================== ARMC-Live: feasible counterexample: stem [0,tid([11]),tid([4])] loop [] Stem: 0: unknown 11: unknown 4: unknown Loop: halt Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.41, wall 0.44 s. Time on cli constraint preparation: run 0.01, wall 0.04 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.51, wall 0.54 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.00 s. Time on refinement: run 0.53, wall 0.67 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. [runlim] end: Sun Nov 30 19:22:53 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 9.54 seconds [runlim] time: 8.05 seconds [runlim] space: 14.1 MB [runlim] samples: 85