(set-logic LIA)
(set-info :status unsat)
(declare-fun W_S2_V6 () Bool)
(declare-fun W_S2_V4 () Bool)
(declare-fun W_S2_V2 () Bool)
(declare-fun W_S2_V3 () Bool)
(declare-fun W_S2_V1 () Bool)
(declare-fun W_S1_V6 () Bool)
(declare-fun W_S1_V5 () Bool)
(declare-fun W_S1_V2 () Bool)
(declare-fun W_S1_V3 () Bool)
(declare-fun W_S1_V1 () Bool)
(declare-fun R_S1_V1 () Bool)
(declare-fun R_S2_V6 () Bool)
(declare-fun R_S2_V4 () Bool)
(declare-fun R_S2_V5 () Bool)
(declare-fun R_S2_V2 () Bool)
(declare-fun R_S2_V3 () Bool)
(declare-fun R_S2_V1 () Bool)
(declare-fun R_E1_V6 () Bool)
(declare-fun R_E1_V4 () Bool)
(declare-fun R_E1_V5 () Bool)
(declare-fun R_E1_V2 () Bool)
(declare-fun R_E1_V3 () Bool)
(declare-fun R_E1_V1 () Bool)
(declare-fun DISJ_W_S2_R_E1 () Bool)
(declare-fun DISJ_W_S2_R_S2 () Bool)
(declare-fun R_S1_V6 () Bool)
(declare-fun R_S1_V4 () Bool)
(declare-fun R_S1_V5 () Bool)
(declare-fun R_S1_V2 () Bool)
(declare-fun R_S1_V3 () Bool)
(declare-fun DISJ_W_S2_R_S1 () Bool)
(declare-fun DISJ_W_S1_W_S2 () Bool)
(declare-fun DISJ_W_S1_R_E1 () Bool)
(declare-fun DISJ_W_S1_R_S2 () Bool)
(declare-fun DISJ_W_S1_R_S1 () Bool)
(declare-fun W_S2_V5 () Bool)
(declare-fun W_S1_V4 () Bool)
(assert
 (let
 (($x1615
   (forall
    ((V1_0 Int) (V3_0 Int) 
     (V2_0 Int) (V5_0 Int) 
     (V4_0 Int) (V6_0 Int) 
     (MW_S1_V1 Bool) (MW_S1_V3 Bool) 
     (MW_S1_V2 Bool) (MW_S1_V5 Bool) 
     (MW_S1_V4 Bool) (MW_S1_V6 Bool) 
     (MW_S2_V1 Bool) (MW_S2_V3 Bool) 
     (MW_S2_V2 Bool) (MW_S2_V5 Bool) 
     (MW_S2_V4 Bool) (MW_S2_V6 Bool) 
     (S1_V1_!158 Int) (S1_V1_!171 Int) 
     (S2_V5_!167 Int) (S2_V5_!180 Int) 
     (S1_V3_!159 Int) (S1_V3_!172 Int) 
     (S1_V2_!160 Int) (S1_V2_!173 Int) 
     (E1_!157 Int) (E1_!170 Int) 
     (E1_!183 Int) (S2_V4_!168 Int) 
     (S2_V4_!181 Int) (S2_V6_!169 Int) 
     (S2_V6_!182 Int) (S1_V5_!161 Int) 
     (S1_V5_!174 Int) (S2_V1_!164 Int) 
     (S2_V1_!177 Int) (S1_V4_!162 Int) 
     (S1_V4_!175 Int) (S2_V3_!165 Int) 
     (S2_V3_!178 Int) (S2_V2_!166 Int) 
     (S2_V2_!179 Int) (S1_V6_!163 Int) 
     (S1_V6_!176 Int))
    (let ((?x1431 (ite MW_S1_V6 S1_V6_!176 V6_0)))
    (let ((?x1432 (ite MW_S2_V6 S2_V6_!182 ?x1431)))
    (let ((?x1433 (ite MW_S1_V6 S1_V6_!163 V6_0)))
    (let ((?x1434 (ite MW_S2_V6 S2_V6_!169 ?x1433)))
    (let (($x1435 (= ?x1434 ?x1432)))
    (let ((?x1436 (ite MW_S1_V4 S1_V4_!175 V4_0)))
    (let ((?x1437 (ite MW_S2_V4 S2_V4_!181 ?x1436)))
    (let ((?x1438 (ite MW_S1_V4 S1_V4_!162 V4_0)))
    (let ((?x1439 (ite MW_S2_V4 S2_V4_!168 ?x1438)))
    (let (($x1440 (= ?x1439 ?x1437)))
    (let ((?x1441 (ite MW_S1_V5 S1_V5_!174 V5_0)))
    (let ((?x1442 (ite MW_S2_V5 S2_V5_!180 ?x1441)))
    (let ((?x1444 (ite MW_S1_V5 S1_V5_!161 V5_0)))
    (let ((?x1445 (ite MW_S2_V5 S2_V5_!167 ?x1444)))
    (let (($x1446 (= ?x1445 ?x1442)))
    (let ((?x1447 (ite MW_S1_V2 S1_V2_!173 V2_0)))
    (let ((?x1448 (ite MW_S2_V2 S2_V2_!179 ?x1447)))
    (let ((?x1449 (ite MW_S1_V2 S1_V2_!160 V2_0)))
    (let ((?x1450 (ite MW_S2_V2 S2_V2_!166 ?x1449)))
    (let (($x1451 (= ?x1450 ?x1448)))
    (let ((?x1467 (ite MW_S1_V3 S1_V3_!159 V3_0)))
    (let ((?x1468 (+ 1 ?x1467)))
    (let ((?x1458 (ite MW_S2_V3 S2_V3_!165 ?x1468)))
    (let
    (($x1459
      (= ?x1458
      (+ (ite MW_S2_V3 S2_V3_!178 (ite MW_S1_V3 S1_V3_!172 V3_0)) ?x1448
      (* (- 1) E1_!183)))))
    (let ((?x1460 (ite MW_S1_V1 S1_V1_!171 E1_!170)))
    (let ((?x1487 (ite MW_S2_V1 S2_V1_!177 ?x1460)))
    (let ((?x1453 (ite MW_S1_V1 S1_V1_!158 E1_!157)))
    (let ((?x1489 (ite MW_S2_V1 S2_V1_!164 ?x1453)))
    (let (($x1289 (= ?x1489 ?x1487)))
    (let ((?x1455 (+ (- 1) ?x1448)))
    (let (($x1376 (>= ?x1487 ?x1455)))
    (let (($x1377 (<= V2_0 E1_!170)))
    (let (($x1379 (not $x1377)))
    (let ((?x1380 (+ (- 1) ?x1450)))
    (let (($x1381 (>= ?x1489 ?x1380)))
    (let (($x1479 (<= V2_0 E1_!157)))
    (let (($x1456 (not $x1479)))
    (let (($x1499 (and $x1456 $x1381 $x1379 $x1376)))
    (let (($x1500 (not $x1499)))
    (let (($x1502 (not MW_S2_V6)))
    (let (($x1503 (or $x1502 W_S2_V6)))
    (let (($x1504 (not MW_S2_V4)))
    (let (($x1505 (or $x1504 W_S2_V4)))
    (let (($x1508 (not MW_S2_V2)))
    (let (($x1509 (or $x1508 W_S2_V2)))
    (let (($x1510 (not MW_S2_V3)))
    (let (($x1511 (or $x1510 W_S2_V3)))
    (let (($x1512 (not MW_S2_V1)))
    (let (($x1513 (or $x1512 W_S2_V1)))
    (let (($x1514 (not MW_S1_V6)))
    (let (($x1515 (or $x1514 W_S1_V6)))
    (let (($x1518 (not MW_S1_V5)))
    (let (($x1519 (or $x1518 W_S1_V5)))
    (let (($x1520 (not MW_S1_V2)))
    (let (($x1521 (or $x1520 W_S1_V2)))
    (let (($x1522 (not MW_S1_V3)))
    (let (($x1523 (or $x1522 W_S1_V3)))
    (let (($x1524 (not MW_S1_V1)))
    (let (($x1525 (or $x1524 W_S1_V1)))
    (let (($x1527 (= S1_V6_!176 S1_V6_!163)))
    (let (($x1528 (= E1_!170 E1_!157)))
    (let (($x228 (not R_S1_V1)))
    (let (($x1529 (or $x228 $x1528)))
    (let (($x1530 (not $x1529)))
    (let (($x1531 (or $x1530 $x1527)))
    (let (($x1532 (= S2_V2_!179 S2_V2_!166)))
    (let (($x1533 (= ?x1431 ?x1433)))
    (let (($x253 (not R_S2_V6)))
    (let (($x1534 (or $x253 $x1533)))
    (let (($x1535 (= ?x1436 ?x1438)))
    (let (($x251 (not R_S2_V4)))
    (let (($x1536 (or $x251 $x1535)))
    (let (($x1537 (= ?x1441 ?x1444)))
    (let (($x249 (not R_S2_V5)))
    (let (($x1538 (or $x249 $x1537)))
    (let (($x1539 (= ?x1447 ?x1449)))
    (let (($x247 (not R_S2_V2)))
    (let (($x1540 (or $x247 $x1539)))
    (let ((?x1462 (ite MW_S1_V3 S1_V3_!172 V3_0)))
    (let (($x1541 (= ?x1462 ?x1468)))
    (let (($x245 (not R_S2_V3)))
    (let (($x1542 (or $x245 $x1541)))
    (let (($x1543 (= ?x1460 ?x1453)))
    (let (($x243 (not R_S2_V1)))
    (let (($x1544 (or $x243 $x1543)))
    (let (($x1545 (and $x1544 $x1542 $x1540 $x1538 $x1536 $x1534)))
    (let (($x1546 (not $x1545)))
    (let (($x1547 (or $x1546 $x1532)))
    (let (($x1548 (= S2_V3_!165 S2_V3_!178)))
    (let (($x1549 (= ?x1433 ?x1431)))
    (let (($x1550 (or $x253 $x1549)))
    (let (($x1551 (= ?x1438 ?x1436)))
    (let (($x1552 (or $x251 $x1551)))
    (let (($x1553 (= ?x1444 ?x1441)))
    (let (($x1554 (or $x249 $x1553)))
    (let (($x1555 (= ?x1449 ?x1447)))
    (let (($x1556 (or $x247 $x1555)))
    (let ((?x1557 (+ (- 1) ?x1462)))
    (let (($x1558 (= ?x1467 ?x1557)))
    (let (($x1559 (or $x245 $x1558)))
    (let (($x1560 (= ?x1453 ?x1460)))
    (let (($x1561 (or $x243 $x1560)))
    (let (($x1562 (and $x1561 $x1559 $x1556 $x1554 $x1552 $x1550)))
    (let (($x1563 (not $x1562)))
    (let (($x1564 (or $x1563 $x1548)))
    (let (($x1565 (= S1_V4_!175 S1_V4_!162)))
    (let (($x1566 (or $x1530 $x1565)))
    (let (($x1567 (= S2_V1_!177 S2_V1_!164)))
    (let (($x1568 (or $x1546 $x1567)))
    (let (($x1569 (= S1_V5_!174 S1_V5_!161)))
    (let (($x1570 (or $x1530 $x1569)))
    (let (($x1571 (= S2_V6_!182 S2_V6_!169)))
    (let (($x1572 (or $x1546 $x1571)))
    (let (($x1573 (= S2_V4_!168 S2_V4_!181)))
    (let (($x1574 (or $x1563 $x1573)))
    (let (($x1575 (= E1_!170 E1_!183)))
    (let (($x1576 (= V6_0 ?x1432)))
    (let (($x177 (not R_E1_V6)))
    (let (($x1577 (or $x177 $x1576)))
    (let (($x1578 (= V4_0 ?x1437)))
    (let (($x175 (not R_E1_V4)))
    (let (($x1579 (or $x175 $x1578)))
    (let (($x1580 (= V5_0 ?x1442)))
    (let (($x173 (not R_E1_V5)))
    (let (($x1581 (or $x173 $x1580)))
    (let (($x1582 (= V2_0 ?x1448)))
    (let (($x171 (not R_E1_V2)))
    (let (($x1583 (or $x171 $x1582)))
    (let ((?x1463 (ite MW_S2_V3 S2_V3_!178 ?x1462)))
    (let (($x1584 (= V3_0 ?x1463)))
    (let (($x169 (not R_E1_V3)))
    (let (($x1585 (or $x169 $x1584)))
    (let ((?x1586 (+ 1 ?x1487)))
    (let (($x1587 (= V1_0 ?x1586)))
    (let (($x167 (not R_E1_V1)))
    (let (($x1588 (or $x167 $x1587)))
    (let (($x1589 (and $x1588 $x1585 $x1583 $x1581 $x1579 $x1577)))
    (let (($x1590 (not $x1589)))
    (let (($x1591 (or $x1590 $x1575)))
    (let (($x1592 (= E1_!157 E1_!183)))
    (let (($x1593 (or $x1590 $x1592)))
    (let (($x1594 (= E1_!157 E1_!170)))
    (let (($x1595 (= S1_V2_!173 S1_V2_!160)))
    (let (($x1596 (or $x1530 $x1595)))
    (let (($x1597 (= S1_V3_!159 S1_V3_!172)))
    (let (($x1598 (or $x228 $x1594)))
    (let (($x1599 (not $x1598)))
    (let (($x1600 (or $x1599 $x1597)))
    (let (($x1601 (= S2_V5_!180 S2_V5_!167)))
    (let (($x1602 (or $x1546 $x1601)))
    (let (($x1603 (= S1_V1_!158 S1_V1_!171)))
    (let (($x1604 (or $x1599 $x1603)))
    (let
    (($x1612
      (and $x1604 $x1602 $x1600 $x1596 $x1594 $x1593 $x1591 $x1574 $x1572
      $x1570 $x1568 $x1566 $x1564 $x1547 $x1531 $x1525 $x1523 $x1521 $x1519
      $x1515 $x1513 $x1511 $x1509 $x1505 $x1503)))
    (let (($x1613 (not $x1612)))
    (or $x1613 $x1500 (and $x1289 $x1459 $x1451 $x1446 $x1440 $x1435)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 (let (($x103 (and W_S2_V6 R_E1_V6)))
 (let (($x102 (and W_S2_V4 R_E1_V4)))
 (let (($x100 (and W_S2_V2 R_E1_V2)))
 (let (($x99 (and W_S2_V3 R_E1_V3)))
 (let (($x98 (and W_S2_V1 R_E1_V1)))
 (let (($x128 (or $x98 $x99 $x100 R_E1_V5 $x102 $x103)))
 (let (($x129 (not $x128)))
 (let (($x130 (= DISJ_W_S2_R_E1 $x129)))
 (let (($x93 (and W_S2_V6 R_S2_V6)))
 (let (($x92 (and W_S2_V4 R_S2_V4)))
 (let (($x90 (and W_S2_V2 R_S2_V2)))
 (let (($x89 (and W_S2_V3 R_S2_V3)))
 (let (($x88 (and W_S2_V1 R_S2_V1)))
 (let (($x125 (or $x88 $x89 $x90 R_S2_V5 $x92 $x93)))
 (let (($x126 (not $x125)))
 (let (($x127 (= DISJ_W_S2_R_S2 $x126)))
 (let (($x83 (and W_S2_V6 R_S1_V6)))
 (let (($x82 (and W_S2_V4 R_S1_V4)))
 (let (($x80 (and W_S2_V2 R_S1_V2)))
 (let (($x79 (and W_S2_V3 R_S1_V3)))
 (let (($x78 (and W_S2_V1 R_S1_V1)))
 (let (($x122 (or $x78 $x79 $x80 R_S1_V5 $x82 $x83)))
 (let (($x123 (not $x122)))
 (let (($x124 (= DISJ_W_S2_R_S1 $x123)))
 (let (($x73 (and W_S1_V6 W_S2_V6)))
 (let (($x68 (and W_S1_V2 W_S2_V2)))
 (let (($x66 (and W_S1_V3 W_S2_V3)))
 (let (($x64 (and W_S1_V1 W_S2_V1)))
 (let (($x119 (or $x64 $x66 $x68 W_S1_V5 W_S2_V4 $x73)))
 (let (($x120 (not $x119)))
 (let (($x121 (= DISJ_W_S1_W_S2 $x120)))
 (let (($x58 (and W_S1_V6 R_E1_V6)))
 (let (($x54 (and W_S1_V5 R_E1_V5)))
 (let (($x52 (and W_S1_V2 R_E1_V2)))
 (let (($x50 (and W_S1_V3 R_E1_V3)))
 (let (($x48 (and W_S1_V1 R_E1_V1)))
 (let (($x116 (or $x48 $x50 $x52 $x54 R_E1_V4 $x58)))
 (let (($x117 (not $x116)))
 (let (($x118 (= DISJ_W_S1_R_E1 $x117)))
 (let (($x42 (and W_S1_V6 R_S2_V6)))
 (let (($x38 (and W_S1_V5 R_S2_V5)))
 (let (($x36 (and W_S1_V2 R_S2_V2)))
 (let (($x34 (and W_S1_V3 R_S2_V3)))
 (let (($x32 (and W_S1_V1 R_S2_V1)))
 (let (($x113 (or $x32 $x34 $x36 $x38 R_S2_V4 $x42)))
 (let (($x114 (not $x113)))
 (let (($x115 (= DISJ_W_S1_R_S2 $x114)))
 (let (($x26 (and W_S1_V6 R_S1_V6)))
 (let (($x21 (and W_S1_V5 R_S1_V5)))
 (let (($x18 (and W_S1_V2 R_S1_V2)))
 (let (($x15 (and W_S1_V3 R_S1_V3)))
 (let (($x12 (and W_S1_V1 R_S1_V1)))
 (let (($x110 (or $x12 $x15 $x18 $x21 R_S1_V4 $x26)))
 (let (($x111 (not $x110)))
 (let (($x112 (= DISJ_W_S1_R_S1 $x111)))
 (and W_S1_V4 W_S2_V5 $x112 $x115 $x118 $x121 $x124 $x127 $x130 $x1615))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x1192 (not W_S2_V2)))
 (let (($x1189 (not W_S2_V3)))
 (let (($x1186 (not W_S2_V1)))
 (let (($x1091 (not W_S1_V2)))
 (let (($x1078 (not W_S1_V1)))
 (let (($x245 (not R_S2_V3)))
 (let (($x167 (not R_E1_V1)))
 (let
 (($x1647
   (and $x167 $x245 $x1078 $x1091 $x1186 $x1189 $x1192 DISJ_W_S1_R_E1
   DISJ_W_S2_R_E1))) (not $x1647))))))))))
(check-sat)