Reduce-svn5758-src/xmpl/ibalp.rlg

33 1 or var106 = 1) and (var107 = 1 or var108 = 1) and (var109 = 1 or var110 = 1)
56 not(var105 = 1) or not(var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (
75  = 1) or not(var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114
113 (var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var113 = 1) or not(
151 var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114 = 1) or not(
246 (var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114 = 1) or not(
265 var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114 = 1) or not(
303 var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var113 = 1) or not(
341 var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114 = 1) or not(
379 (var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var113 = 1) or not(
417 var108 = 1) or not(var109 = 1) or not(var112 = 1)) and (not(var114 = 1) or not(
466 (var167 = 1)) and (var108 = 1 or not(var167 = 1)) and (var109 = 1 or not(var167
502  (var108 = 1 or not(var177 = 1)) and (var110 = 1 or not(var177 = 1)) and (var112
573 var197 = 1)) and (var106 = 1 or not(var197 = 1)) and (var108 = 1 or not(var197 =
609 var105 = 1 or not(var207 = 1)) and (var108 = 1 or not(var207 = 1)) and (var110 =
681  (var108 = 1 or not(var227 = 1)) and (var110 = 1 or not(var227 = 1)) and (var112
752 var247 = 1)) and (var106 = 1 or not(var247 = 1)) and (var108 = 1 or not(var247 =
860 (var108 = 1 or not(var277 = 1)) and (var110 = 1 or not(var277 = 1)) and (var111
931 var297 = 1)) and (var106 = 1 or not(var297 = 1)) and (var108 = 1 or not(var297 =
1110  1)) and (var105 = 1 or not(var347 = 1)) and (var108 = 1 or not(var347 = 1)) and
1146  1 or not(var357 = 1)) and (var108 = 1 or not(var357 = 1)) and (var110 = 1 or
1182  1)) and (var108 = 1 or not(var367 = 1)) and (var109 = 1 or not(var367 = 1)) and
1217 1 or not(var377 = 1)) and (var105 = 1 or not(var377 = 1)) and (var108 = 1 or not
1253 var387 = 1)) and (var106 = 1 or not(var387 = 1)) and (var108 = 1 or not(var387 =
1468 var106 = 1 or not(var447 = 1)) and (var108 = 1 or not(var447 = 1)) and (var109 =
1504 var457 = 1)) and (var108 = 1 or not(var457 = 1)) and (var110 = 1 or not(var457 =
1540  (var108 = 1 or not(var467 = 1)) and (var109 = 1 or not(var467 = 1)) and (var112
1575  1 or not(var477 = 1)) and (var106 = 1 or not(var477 = 1)) and (var108 = 1 or
1611 var487 = 1)) and (var106 = 1 or not(var487 = 1)) and (var108 = 1 or not(var487 =
1683 var507 = 1)) and (var108 = 1 or not(var507 = 1)) and (var110 = 1 or not(var507 =
1754 1 or not(var527 = 1)) and (var106 = 1 or not(var527 = 1)) and (var108 = 1 or not
1862 (var557 = 1)) and (var108 = 1 or not(var557 = 1)) and (var110 = 1 or not(var557
1933  1 or not(var577 = 1)) and (var105 = 1 or not(var577 = 1)) and (var108 = 1 or
2005 var106 = 1 or not(var597 = 1)) and (var108 = 1 or not(var597 = 1)) and (var109 =
2041 (var607 = 1)) and (var108 = 1 or not(var607 = 1)) and (var110 = 1 or not(var607
2112 1 or not(var627 = 1)) and (var105 = 1 or not(var627 = 1)) and (var108 = 1 or not
2148 var637 = 1)) and (var106 = 1 or not(var637 = 1)) and (var108 = 1 or not(var637 =
2184 var105 = 1 or not(var647 = 1)) and (var108 = 1 or not(var647 = 1)) and (var110 =
2256 (var108 = 1 or not(var667 = 1)) and (var110 = 1 or not(var667 = 1)) and (var112
2291 1 or not(var677 = 1)) and (var106 = 1 or not(var677 = 1)) and (var108 = 1 or not
2327 var687 = 1)) and (var106 = 1 or not(var687 = 1)) and (var108 = 1 or not(var687 =
2363 var106 = 1 or not(var697 = 1)) and (var108 = 1 or not(var697 = 1)) and (var110 =
2399 (var707 = 1)) and (var108 = 1 or not(var707 = 1)) and (var110 = 1 or not(var707
2506 var737 = 1)) and (var106 = 1 or not(var737 = 1)) and (var108 = 1 or not(var737 =
2685  1)) and (var105 = 1 or not(var787 = 1)) and (var108 = 1 or not(var787 = 1)) and
2721  1 or not(var797 = 1)) and (var108 = 1 or not(var797 = 1)) and (var109 = 1 or
2828  1)) and (var105 = 1 or not(var827 = 1)) and (var108 = 1 or not(var827 = 1)) and
2864  1 or not(var837 = 1)) and (var108 = 1 or not(var837 = 1)) and (var110 = 1 or
2900  1)) and (var108 = 1 or not(var847 = 1)) and (var109 = 1 or not(var847 = 1)) and
2971 var867 = 1)) and (var106 = 1 or not(var867 = 1)) and (var108 = 1 or not(var867 =
3007 (var105 = 1 or not(var877 = 1)) and (var108 = 1 or not(var877 = 1)) and (var110
3043 var887 = 1)) and (var108 = 1 or not(var887 = 1)) and (var110 = 1 or not(var887 =
3079  (var108 = 1 or not(var897 = 1)) and (var109 = 1 or not(var897 = 1)) and (var112
3114 1 or not(var907 = 1)) and (var106 = 1 or not(var907 = 1)) and (var108 = 1 or not
3150 var917 = 1)) and (var106 = 1 or not(var917 = 1)) and (var108 = 1 or not(var917 =
3186 (var106 = 1 or not(var927 = 1)) and (var108 = 1 or not(var927 = 1)) and (var109