/* C version of the example: represents list traversal
int main(int n0, int n1) {
  int i0 = 0;
  int k = 0;

  tmpl("2");
  while( i0 < n0 ) {
    i0++;
    k++;
  }
  int i1 = 0;
  while( i1 < n1 ) {
    i1++;
    k++;
  }
  int j1 = 0;
  while( j1 < n1 ) {
    assert(k > 0);
    j1++;
    k--;
  }
  int j0 = 0;
  while( j0 < n0 ) {
    assert( k > 0);
    j0++;
    k--;
  }
  return 0;
}*/
:- multifile r/5,implicit_updates/0,var2names/2,preds/2,trans_preds/3,cube_size/1,start/1,error/1,refinement/1,cutpoint/1,invgen_template/2,invgen_template/1,cfg_exit_relation/1,stmtsrc/2,strengthening/2.
refinement(inter).
cube_size(1).
preds(p(_, data(V5, V3, V2, V6, V7, V4, V1)), []).
trans_preds(p(_, data(V5, V3, V2, V6, V7, V4, V1)), p(_, data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), []).
var2names(p(pc(_), data(V5, V3, V2, V6, V7, V4, V1)), [(V5, 'n1'), (V3, 'n0'), (V2, 'k'), (V6, 'j1'), (V7, 'j0'), (V4, 'i1'), (V1, 'i0')]).
% start location
start(pc(main-0-3)).
% error location
error(pc(main-err-0)).
% cutpoint locations
cutpoint(pc(main-26-22)). % line 22
cutpoint(pc(main-17-16)). % line 16
cutpoint(pc(main-10-11)). % line 11
cutpoint(pc(main-1-6)). % line 6
% invariant templates
invgen_template(2). 
% cfg loop exit relation
cfg_exit_relation([(pc(main-17-16), pc(main-26-22)), (pc(main-10-11), pc(main-17-16)), (pc(main-1-6), pc(main-10-11))]).
% 41 transitions
r(p(pc(main-8-6), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-5-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 1). % 
stmtsrc(1, 'skip;').
r(p(pc(main-15-11), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-12-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 2). % 
stmtsrc(2, 'skip;').
r(p(pc(main-22-16), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-19-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 3). % 
stmtsrc(3, 'skip;').
r(p(pc(main-31-22), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-28-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 4). % 
stmtsrc(4, 'skip;').
r(p(pc(main-27-27), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-ret-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 5). % 
stmtsrc(5, 'skip;').
r(p(pc(main-28-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-27-27), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 6). % 
stmtsrc(6, 'skip;').
r(p(pc(main-34-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-26-22), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = (V2 - 1), V6p = V6, V7p = V7, V4p = V4, V1p = V1], 7). % k := k - 1
stmtsrc(7, 'k = k - 1;').
r(p(pc(main-32-25), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-34-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = (V7 + 1), V4p = V4, V1p = V1], 8). % j0 := j0 + 1
stmtsrc(8, 'j0 = j0 + 1;').
r(p(pc(main-30-23), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-32-25), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V2 >= 1+ 0)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 9). % k > 0
stmtsrc(9, 'assume(k > 0);').
r(p(pc(main-33-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-err-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 10). % 
stmtsrc(10, 'skip;').
r(p(pc(main-30-23), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-33-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V2 =< 0)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 11). % k <= 0
stmtsrc(11, 'assume(k <= 0);').
r(p(pc(main-29-22), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-31-22), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V7 >= V3)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 12). % j0 >= n0
stmtsrc(12, 'assume(j0 >= n0);').
r(p(pc(main-29-22), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-30-23), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V7 +1 =< V3)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 13). % j0 < n0
stmtsrc(13, 'assume(j0 < n0);').
r(p(pc(main-26-22), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-29-22), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 14). % 
stmtsrc(14, 'skip;').
r(p(pc(main-18-21), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-26-22), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = 0, V4p = V4, V1p = V1], 15). % j0 := 0
stmtsrc(15, 'j0 = 0;').
r(p(pc(main-19-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-18-21), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 16). % 
stmtsrc(16, 'skip;').
r(p(pc(main-25-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-17-16), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = (V2 - 1), V6p = V6, V7p = V7, V4p = V4, V1p = V1], 17). % k := k - 1
stmtsrc(17, 'k = k - 1;').
r(p(pc(main-23-19), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-25-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = (V6 + 1), V7p = V7, V4p = V4, V1p = V1], 18). % j1 := j1 + 1
stmtsrc(18, 'j1 = j1 + 1;').
r(p(pc(main-21-17), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-23-19), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V2 >= 1+ 0)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 19). % k > 0
stmtsrc(19, 'assume(k > 0);').
r(p(pc(main-24-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-err-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 20). % 
stmtsrc(20, 'skip;').
r(p(pc(main-21-17), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-24-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V2 =< 0)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 21). % k <= 0
stmtsrc(21, 'assume(k <= 0);').
r(p(pc(main-20-16), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-22-16), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V6 >= V5)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 22). % j1 >= n1
stmtsrc(22, 'assume(j1 >= n1);').
r(p(pc(main-20-16), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-21-17), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V6 +1 =< V5)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 23). % j1 < n1
stmtsrc(23, 'assume(j1 < n1);').
r(p(pc(main-17-16), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-20-16), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 24). % 
stmtsrc(24, 'skip;').
r(p(pc(main-11-15), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-17-16), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = 0, V7p = V7, V4p = V4, V1p = V1], 25). % j1 := 0
stmtsrc(25, 'j1 = 0;').
r(p(pc(main-12-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-11-15), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 26). % 
stmtsrc(26, 'skip;').
r(p(pc(main-16-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-10-11), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = (V2 + 1), V6p = V6, V7p = V7, V4p = V4, V1p = V1], 27). % k := k + 1
stmtsrc(27, 'k = k + 1;').
r(p(pc(main-14-13), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-16-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = (V4 + 1), V1p = V1], 28). % i1 := i1 + 1
stmtsrc(28, 'i1 = i1 + 1;').
r(p(pc(main-13-11), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-15-11), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V4 >= V5)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 29). % i1 >= n1
stmtsrc(29, 'assume(i1 >= n1);').
r(p(pc(main-13-11), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-14-13), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V4 +1 =< V5)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 30). % i1 < n1
stmtsrc(30, 'assume(i1 < n1);').
r(p(pc(main-10-11), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-13-11), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 31). % 
stmtsrc(31, 'skip;').
r(p(pc(main-4-10), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-10-11), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = 0, V1p = V1], 32). % i1 := 0
stmtsrc(32, 'i1 = 0;').
r(p(pc(main-5-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-4-10), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 33). % 
stmtsrc(33, 'skip;').
r(p(pc(main-9-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-1-6), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = (V2 + 1), V6p = V6, V7p = V7, V4p = V4, V1p = V1], 34). % k := k + 1
stmtsrc(34, 'k = k + 1;').
r(p(pc(main-7-8), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-9-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = (V1 + 1)], 35). % i0 := i0 + 1
stmtsrc(35, 'i0 = i0 + 1;').
r(p(pc(main-6-6), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-8-6), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V1 >= V3)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 36). % i0 >= n0
stmtsrc(36, 'assume(i0 >= n0);').
r(p(pc(main-6-6), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-7-8), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [(V1 +1 =< V3)], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 37). % i0 < n0
stmtsrc(37, 'assume(i0 < n0);').
r(p(pc(main-1-6), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-6-6), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 38). % 
stmtsrc(38, 'skip;').
r(p(pc(main-3-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-1-6), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 39). % 
stmtsrc(39, 'skip;').
r(p(pc(main-2-0), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-3-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = 0, V6p = V6, V7p = V7, V4p = V4, V1p = V1], 40). % k := 0
stmtsrc(40, 'k = 0;').
r(p(pc(main-0-3), data(V5, V3, V2, V6, V7, V4, V1)), p(pc(main-2-0), data(V5p, V3p, V2p, V6p, V7p, V4p, V1p)), [], [V5p = V5, V3p = V3, V2p = V2, V6p = V6, V7p = V7, V4p = V4, V1p = 0], 41). % i0 := 0
stmtsrc(41, 'i0 = 0;').
strengthening(p(pc(main-26-22), data(V5, V3, V2, V6, V7, V4, V1)), [( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V7 +( 0) >= 0, ( 1)*V6 +( 0) >= 0, ( 1)*V2 +( 0) >= 0,( 1)*V1 +( 0) >= 0, ( 1)*V4+( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V7+( 1)*V1 +( 0) >= 0, ( 1)*V7+( 1)*V4 +( 0) >= 0, ( 1)*V7 +( 0) >= 0, ( -1)*V7+( 1)*V1 +( 1) >= 0, ( 1)*V6+( 1)*V1 +( 0) >= 0, ( 1)*V6+( 1)*V4 +( 0) >= 0, ( 1)*V6+( 1)*V7 +( 0) >= 0, ( 1)*V6 +( 0) >= 0, ( 1)*V2+( 1)*V1 +( 0) >= 0, ( 1)*V2+( 1)*V4 +( 0) >= 0, ( 1)*V2+( 1)*V7 +( 0) >= 0, ( 1)*V2+( 1)*V6 +( 0) >= 0, ( 1)*V2 +( 0) >= 0, ( -1)*V3+( 1)*V1 +( 0) >= 0, ( -1)*V5+( 1)*V4 +( 0) >= 0, ( -1)*V5+( 1)*V6 +( 0) >= 0,( 0)*V5+( 0)*V3+( -1)*V2+( -1)*V6+( -1)*V7+( 1)*V4+( 1)*V1 +( 0) = 0, ( 0)*V5+( 0)*V3+( 1)*V2+( 0)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0, ( -1)*V5+( 0)*V3+( 0)*V2+( 1)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 1)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0, ( -1)*V5+( 0)*V3+( 1)*V2+( 1)*V6+( 1)*V7+( 0)*V4+( -1)*V1 +( 0) >= 0, ( 0)*V5+( -1)*V3+( 0)*V2+( 0)*V6+( 0)*V7+( 0)*V4+( 1)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 0)*V6+( 1)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 0)*V6+( -1)*V7+( 0)*V4+( 1)*V1 +( 1) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 0)*V6+( -1)*V7+( 0)*V4+( 2)*V1 +( 0) >= 0]).
strengthening(p(pc(main-17-16), data(V5, V3, V2, V6, V7, V4, V1)), [( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V6 +( 0) >= 0, ( 1)*V2 +( 0) >= 0,( 1)*V1 +( 0) >= 0, ( 1)*V4+( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V6+( 1)*V1 +( 0) >= 0, ( 1)*V6+( 1)*V4 +( 0) >= 0, ( 1)*V6 +( 0) >= 0, ( -1)*V6+( 1)*V4 +( 1) >= 0, ( 1)*V2+( 1)*V1 +( 0) >= 0, ( 1)*V2+( 1)*V4 +( 0) >= 0, ( 1)*V2+( 1)*V6 +( 0) >= 0, ( 1)*V2 +( 0) >= 0, ( -1)*V3+( 1)*V1 +( 0) >= 0, ( -1)*V5+( 1)*V4 +( 0) >= 0,( 0)*V5+( 0)*V3+( -1)*V2+( -1)*V6+( 0)*V7+( 1)*V4+( 1)*V1 +( 0) = 0, ( 0)*V5+( -1)*V3+( 1)*V2+( 1)*V6+( 0)*V7+( -1)*V4+( 0)*V1 +( 0) >= 0, ( -1)*V5+( 0)*V3+( 0)*V2+( 0)*V6+( 0)*V7+( 1)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 1)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 1)*V2+( 1)*V6+( 0)*V7+( -1)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( -1)*V6+( 0)*V7+( 1)*V4+( 0)*V1 +( 1) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( -1)*V6+( 0)*V7+( 2)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 1)*V2+( 0)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0]).
strengthening(p(pc(main-10-11), data(V5, V3, V2, V6, V7, V4, V1)), [( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V2 +( 0) >= 0,( 1)*V1 +( 0) >= 0, ( 1)*V4+( 1)*V1 +( 0) >= 0, ( 1)*V4 +( 0) >= 0, ( 1)*V2+( -1)*V1 +( 0) >= 0, ( 1)*V2+( 1)*V1 +( 0) >= 0, ( 1)*V2+( -1)*V4 +( 0) >= 0, ( 1)*V2+( 1)*V4 +( 0) >= 0, ( 1)*V2 +( 0) >= 0, ( -1)*V3+( 1)*V1 +( 0) >= 0, ( -1)*V3+( 1)*V2 +( 0) >= 0,( 0)*V5+( 0)*V3+( -1)*V2+( 0)*V6+( 0)*V7+( 1)*V4+( 1)*V1 +( 0) = 0, ( 0)*V5+( 0)*V3+( 1)*V2+( 0)*V6+( 0)*V7+( -1)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( -1)*V3+( 1)*V2+( 0)*V6+( 0)*V7+( -1)*V4+( 0)*V1 +( 0) >= 0, ( 0)*V5+( 0)*V3+( 0)*V2+( 0)*V6+( 0)*V7+( 1)*V4+( 0)*V1 +( 0) >= 0]).
strengthening(p(pc(main-1-6), data(V5, V3, V2, V6, V7, V4, V1)), [( 1)*V1 +( 0) >= 0, ( 1)*V2 +( 0) >= 0,( 1)*V1 +( 0) >= 0, ( 1)*V2+( -1)*V1 +( 0) >= 0, ( 1)*V2+( 1)*V1 +( 0) >= 0, ( 1)*V2 +( 0) >= 0, ( -1)*V2+( 1)*V1 +( 0) >= 0,( 0)*V5+( 0)*V3+( -1)*V2+( 0)*V6+( 0)*V7+( 0)*V4+( 1)*V1 +( 0) = 0, ( 0)*V5+( 0)*V3+( 1)*V2+( 0)*V6+( 0)*V7+( 0)*V4+( 0)*V1 +( 0) >= 0]).