path: root/test/regress/regress1/boolean.cvc

% EXPECT: entailed
p : BOOLEAN;
q : BOOLEAN;
r : BOOLEAN;
s : BOOLEAN;
t : BOOLEAN;
u : BOOLEAN;
v : BOOLEAN;
P1 : BOOLEAN;
P2 : BOOLEAN;
P3 : BOOLEAN;
P4 : BOOLEAN;
P6 : BOOLEAN;
P5 : BOOLEAN;
a41 : BOOLEAN = 
        IF p THEN FALSE
        ELSE TRUE
        ENDIF;
a42 : BOOLEAN = 
        IF a41 THEN FALSE
        ELSE TRUE
        ENDIF;
a45 : BOOLEAN = 
        IF p THEN p
        ELSE a41
        ENDIF;
a46 : BOOLEAN = 
        IF q THEN FALSE
        ELSE TRUE
        ENDIF;
a49 : BOOLEAN = 
        IF s THEN t
        ELSE FALSE
        ENDIF;
a58 : BOOLEAN = 
        IF q THEN q
        ELSE a46
        ENDIF;
a59 : BOOLEAN = 
        IF r THEN FALSE
        ELSE TRUE
        ENDIF;
a61 : BOOLEAN = 
        IF s THEN FALSE
        ELSE TRUE
        ENDIF;
a62 : BOOLEAN = 
        IF s THEN s
        ELSE a61
        ENDIF;
a65 : BOOLEAN = 
        IF t THEN FALSE
        ELSE TRUE
        ENDIF;
a67 : BOOLEAN = 
        IF u THEN FALSE
        ELSE TRUE
        ENDIF;
a73 : BOOLEAN = 
        IF p THEN q
        ELSE FALSE
        ENDIF;
a74 : BOOLEAN = 
        IF q THEN p
        ELSE FALSE
        ENDIF;
a77 : BOOLEAN = 
        IF r THEN TRUE
        ELSE s
        ENDIF;
a78 : BOOLEAN = 
        IF s THEN TRUE
        ELSE r
        ENDIF;
a81 : BOOLEAN = 
        IF t THEN u
        ELSE a67
        ENDIF;
a82 : BOOLEAN = 
        IF u THEN t
        ELSE a65
        ENDIF;
a88 : BOOLEAN = 
        IF q THEN r
        ELSE FALSE
        ENDIF;
a89 : BOOLEAN = 
        IF p THEN a88
        ELSE FALSE
        ENDIF;
a92 : BOOLEAN = 
        IF s THEN TRUE
        ELSE t
        ENDIF;
a94 : BOOLEAN = 
        IF t THEN TRUE
        ELSE u
        ENDIF;
a95 : BOOLEAN = 
        IF s THEN TRUE
        ELSE a94
        ENDIF;
a105 : BOOLEAN = 
        IF t THEN u
        ELSE FALSE
        ENDIF;
a111 : BOOLEAN = 
        IF p THEN q
        ELSE TRUE
        ENDIF;
a112 : BOOLEAN = 
        IF q THEN r
        ELSE TRUE
        ENDIF;
a114 : BOOLEAN = 
        IF p THEN r
        ELSE TRUE
        ENDIF;
a116 : BOOLEAN = 
        IF s THEN t
        ELSE a65
        ENDIF;
a121 : BOOLEAN = 
        IF a46 THEN a41
        ELSE TRUE
        ENDIF;
a126 : BOOLEAN = 
        IF a59 THEN a61
        ELSE 
          IF a61 THEN FALSE
          ELSE TRUE
          ENDIF
        ENDIF;
a130 : BOOLEAN = 
        IF q THEN TRUE
        ELSE r
        ENDIF;
a132 : BOOLEAN = 
        IF p THEN r
        ELSE FALSE
        ENDIF;
a133 : BOOLEAN = 
        IF a73 THEN TRUE
        ELSE a132
        ENDIF;
a138 : BOOLEAN = 
        IF a92 THEN 
          IF s THEN TRUE
          ELSE u
          ENDIF
        ELSE FALSE
        ENDIF;
a143 : BOOLEAN = 
        IF a114 THEN a112
        ELSE FALSE
        ENDIF;
a145 : BOOLEAN = 
        IF 
          IF 
            IF p THEN TRUE
            ELSE q
            ENDIF THEN r
          ELSE TRUE
          ENDIF THEN a143
        ELSE 
          IF a143 THEN FALSE
          ELSE TRUE
          ENDIF
        ENDIF;
a147 : BOOLEAN = 
        IF s THEN t
        ELSE TRUE
        ENDIF;
a148 : BOOLEAN = 
        IF s THEN u
        ELSE TRUE
        ENDIF;
a149 : BOOLEAN = 
        IF a147 THEN TRUE
        ELSE a148
        ENDIF;
a153 : BOOLEAN = 
        IF a73 THEN r
        ELSE TRUE
        ENDIF;
a154 : BOOLEAN = 
        IF a114 THEN TRUE
        ELSE a112
        ENDIF;
a158 : BOOLEAN = 
        IF a147 THEN a148
        ELSE FALSE
        ENDIF;
a162 : BOOLEAN = 
        IF p THEN a112
        ELSE TRUE
        ENDIF;
a167 : BOOLEAN = 
        IF a46 THEN TRUE
        ELSE a59
        ENDIF;
a171 : BOOLEAN = 
        IF a61 THEN a65
        ELSE FALSE
        ENDIF;
a176 : BOOLEAN = 
        IF p THEN q
        ELSE r
        ENDIF;
a178 : BOOLEAN = 
        IF p THEN a46
        ELSE a59
        ENDIF;
a183 : BOOLEAN = 
        IF s THEN a65
        ELSE 
          IF a65 THEN FALSE
          ELSE TRUE
          ENDIF
        ENDIF;
a187 : BOOLEAN = 
        IF a41 THEN TRUE
        ELSE q
        ENDIF;
a192 : BOOLEAN = 
        IF 
          IF r THEN s
          ELSE FALSE
          ENDIF THEN TRUE
        ELSE 
          IF a59 THEN t
          ELSE FALSE
          ENDIF
        ENDIF;
a197 : BOOLEAN = 
        IF a111 THEN 
          IF a41 THEN r
          ELSE TRUE
          ENDIF
        ELSE FALSE
        ENDIF;
a200 : BOOLEAN = 
        IF a49 THEN TRUE
        ELSE a171
        ENDIF;
a204 : BOOLEAN = 
        IF p THEN q
        ELSE a46
        ENDIF;
a205 : BOOLEAN = 
        IF q THEN p
        ELSE TRUE
        ENDIF;
a206 : BOOLEAN = 
        IF a111 THEN a205
        ELSE FALSE
        ENDIF;
a210 : BOOLEAN = 
        IF p THEN a46
        ELSE TRUE
        ENDIF;
a214 : BOOLEAN = 
        IF a73 THEN FALSE
        ELSE TRUE
        ENDIF;
a221 : BOOLEAN = 
        IF 
          IF p THEN a46
          ELSE FALSE
          ENDIF THEN r
        ELSE TRUE
        ENDIF;
a225 : BOOLEAN = 
        IF a187 THEN a132
        ELSE TRUE
        ENDIF;
a228 : BOOLEAN = 
        IF q THEN r
        ELSE a59
        ENDIF;
a231 : BOOLEAN = 
        IF a204 THEN r
        ELSE a59
        ENDIF;
a237 : BOOLEAN = 
        IF q THEN a132
        ELSE 
          IF a41 THEN s
          ELSE FALSE
          ENDIF
        ENDIF;
a288 : BOOLEAN = 
        IF 
          IF 
            IF p THEN a41
            ELSE a42
            ENDIF THEN FALSE
          ELSE TRUE
          ENDIF THEN 
          IF 
            IF a45 THEN 
              IF 
                IF q THEN TRUE
                ELSE a46
                ENDIF THEN 
                IF 
                  IF r THEN r
                  ELSE TRUE
                  ENDIF THEN 
                  IF 
                    IF a49 THEN s
                    ELSE TRUE
                    ENDIF THEN 
                    IF u THEN 
                      IF u THEN TRUE
                      ELSE v
                      ENDIF
                    ELSE TRUE
                    ENDIF
                  ELSE FALSE
                  ENDIF
                ELSE FALSE
                ENDIF
              ELSE FALSE
              ENDIF
            ELSE FALSE
            ENDIF THEN 
            IF 
              IF a58 THEN 
                IF 
                  IF r THEN r
                  ELSE a59
                  ENDIF THEN a62
                ELSE FALSE
                ENDIF
              ELSE FALSE
              ENDIF THEN 
              IF 
                IF a45 THEN 
                  IF a62 THEN 
                    IF 
                      IF t THEN t
                      ELSE a65
                      ENDIF THEN 
                      IF a67 THEN a67
                      ELSE 
                        IF a67 THEN FALSE
                        ELSE TRUE
                        ENDIF
                      ENDIF
                    ELSE FALSE
                    ENDIF
                  ELSE FALSE
                  ENDIF
                ELSE FALSE
                ENDIF THEN 
                IF 
                  IF 
                    IF a73 THEN a74
                    ELSE 
                      IF a74 THEN FALSE
                      ELSE TRUE
                      ENDIF
                    ENDIF THEN 
                    IF 
                      IF a77 THEN a78
                      ELSE 
                        IF a78 THEN FALSE
                        ELSE TRUE
                        ENDIF
                      ENDIF THEN 
                      IF a81 THEN a82
                      ELSE 
                        IF a82 THEN FALSE
                        ELSE TRUE
                        ENDIF
                      ENDIF
                    ELSE FALSE
                    ENDIF
                  ELSE FALSE
                  ENDIF THEN 
                  IF 
                    IF 
                      IF 
                        IF a73 THEN r
                        ELSE FALSE
                        ENDIF THEN a89
                      ELSE 
                        IF a89 THEN FALSE
                        ELSE TRUE
                        ENDIF
                      ENDIF THEN 
                      IF 
                        IF a92 THEN TRUE
                        ELSE u
                        ENDIF THEN a95
                      ELSE 
                        IF a95 THEN FALSE
                        ELSE TRUE
                        ENDIF
                      ENDIF
                    ELSE FALSE
                    ENDIF THEN 
                    IF 
                      IF 
                        IF 
                          IF p THEN p
                          ELSE FALSE
                          ENDIF THEN p
                        ELSE a41
                        ENDIF THEN 
                        IF 
                          IF 
                            IF q THEN TRUE
                            ELSE q
                            ENDIF THEN q
                          ELSE a46
                          ENDIF THEN 
                          IF 
                            IF 
                              IF r THEN a77
                              ELSE FALSE
                              ENDIF THEN r
                            ELSE a59
                            ENDIF THEN 
                            IF 
                              IF t THEN TRUE
                              ELSE a105
                              ENDIF THEN t
                            ELSE a65
                            ENDIF
                          ELSE FALSE
                          ENDIF
                        ELSE FALSE
                        ENDIF
                      ELSE FALSE
                      ENDIF THEN 
                      IF a58 THEN 
                        IF 
                          IF 
                            IF 
                              IF a111 THEN a112
                              ELSE FALSE
                              ENDIF THEN a114
                            ELSE TRUE
                            ENDIF THEN 
                            IF 
                              IF a116 THEN a81
                              ELSE FALSE
                              ENDIF THEN 
                              IF s THEN u
                              ELSE a67
                              ENDIF
                            ELSE TRUE
                            ENDIF
                          ELSE FALSE
                          ENDIF THEN 
                          IF 
                            IF 
                              IF a111 THEN a121
                              ELSE 
                                IF a121 THEN FALSE
                                ELSE TRUE
                                ENDIF
                              ENDIF THEN 
                              IF 
                                IF r THEN s
                                ELSE a61
                                ENDIF THEN a126
                              ELSE 
                                IF a126 THEN FALSE
                                ELSE TRUE
                                ENDIF
                              ENDIF
                            ELSE FALSE
                            ENDIF THEN 
                            IF 
                              IF 
                                IF 
                                  IF p THEN a130
                                  ELSE FALSE
                                  ENDIF THEN a133
                                ELSE 
                                  IF a133 THEN FALSE
                                  ELSE TRUE
                                  ENDIF
                                ENDIF THEN 
                                IF 
                                  IF s THEN TRUE
                                  ELSE a105
                                  ENDIF THEN a138
                                ELSE 
                                  IF a138 THEN FALSE
                                  ELSE TRUE
                                  ENDIF
                                ENDIF
                              ELSE FALSE
                              ENDIF THEN 
                              IF 
                                IF a145 THEN 
                                  IF 
                                    IF s THEN a94
                                    ELSE TRUE
                                    ENDIF THEN a149
                                  ELSE 
                                    IF a149 THEN FALSE
                                    ELSE TRUE
                                    ENDIF
                                  ENDIF
                                ELSE FALSE
                                ENDIF THEN 
                                IF 
                                  IF 
                                    IF a153 THEN a154
                                    ELSE 
                                      IF a154 THEN FALSE
                                      ELSE TRUE
                                      ENDIF
                                    ENDIF THEN 
                                    IF 
                                      IF s THEN a105
                                      ELSE TRUE
                                      ENDIF THEN a158
                                    ELSE 
                                      IF a158 THEN FALSE
                                      ELSE TRUE
                                      ENDIF
                                    ENDIF
                                  ELSE FALSE
                                  ENDIF THEN 
                                  IF 
                                    IF a153 THEN a162
                                    ELSE 
                                      IF a162 THEN FALSE
                                      ELSE TRUE
                                      ENDIF
                                    ENDIF THEN 
                                    IF 
                                      IF 
                                        IF a42 THEN p
                                        ELSE a41
                                        ENDIF THEN 
                                        IF 
                                          IF 
                                            IF a88 THEN FALSE
                                            ELSE TRUE
                                            ENDIF THEN a167
                                          ELSE 
                                            IF a167 THEN FALSE
                                            ELSE TRUE
                                            ENDIF
                                          ENDIF THEN 
                                          IF 
                                            IF a92 THEN FALSE
                                            ELSE TRUE
                                            ENDIF THEN a171
                                          ELSE 
                                            IF a171 THEN FALSE
                                            ELSE TRUE
                                            ENDIF
                                          ENDIF
                                        ELSE FALSE
                                        ENDIF
                                      ELSE FALSE
                                      ENDIF THEN 
                                      IF 
                                        IF 
                                          IF 
                                            IF a176 THEN FALSE
                                            ELSE TRUE
                                            ENDIF THEN a178
                                          ELSE 
                                            IF a178 THEN FALSE
                                            ELSE TRUE
                                            ENDIF
                                          ENDIF THEN 
                                          IF 
                                            IF a116 THEN FALSE
                                            ELSE TRUE
                                            ENDIF THEN a183
                                          ELSE 
                                            IF a183 THEN FALSE
                                            ELSE TRUE
                                            ENDIF
                                          ENDIF
                                        ELSE FALSE
                                        ENDIF THEN 
                                        IF 
                                          IF 
                                            IF a111 THEN a187
                                            ELSE 
                                              IF a187 THEN FALSE
                                              ELSE TRUE
                                              ENDIF
                                            ENDIF THEN 
                                            IF 
                                              IF r THEN s
                                              ELSE t
                                              ENDIF THEN a192
                                            ELSE 
                                              IF a192 THEN FALSE
                                              ELSE TRUE
                                              ENDIF
                                            ENDIF
                                          ELSE FALSE
                                          ENDIF THEN 
                                          IF 
                                            IF 
                                              IF a176 THEN a197
                                              ELSE 
                                                IF a197 THEN FALSE
                                                ELSE TRUE
                                                ENDIF
                                              ENDIF THEN 
                                              IF a116 THEN a200
                                              ELSE 
                                                IF a200 THEN FALSE
                                                ELSE TRUE
                                                ENDIF
                                              ENDIF
                                            ELSE FALSE
                                            ENDIF THEN 
                                            IF 
                                              IF a204 THEN a206
                                              ELSE 
                                                IF a206 THEN FALSE
                                                ELSE TRUE
                                                ENDIF
                                              ENDIF THEN 
                                              IF 
                                                IF a111 THEN TRUE
                                                ELSE a205
                                                ENDIF THEN 
                                                IF 
                                                  IF a46 THEN TRUE
                                                  ELSE 
                                                    IF 
                                                      IF a210 THEN p
                                                      ELSE FALSE
                                                      ENDIF THEN FALSE
                                                    ELSE TRUE
                                                    ENDIF
                                                  ENDIF THEN 
                                                  IF 
                                                    IF a210 THEN a214
                                                    ELSE 
                                                      IF a214 THEN FALSE
                                                      ELSE TRUE
                                                      ENDIF
                                                    ENDIF THEN 
                                                    IF a145 THEN 
                                                      IF 
                                                        IF a162 THEN a153
                                                        ELSE 
                                                          IF a153 THEN FALSE
                                                          ELSE TRUE
                                                          ENDIF
                                                        ENDIF THEN 
                                                        IF 
                                                          IF 
                                                            IF p THEN a130
                                                            ELSE TRUE
                                                            ENDIF THEN a221
                                                          ELSE 
                                                            IF a221 THEN FALSE
                                                            ELSE TRUE
                                                            ENDIF
                                                          ENDIF THEN 
                                                          IF 
                                                            IF 
                                                              IF p THEN a112
                                                              ELSE FALSE
                                                              ENDIF THEN a225
                                                            ELSE 
                                                              IF a225 THEN FALSE
                                                              ELSE TRUE
                                                              ENDIF
                                                            ENDIF THEN 
                                                            IF 
                                                              IF 
                                                                IF p THEN a228
                                                                ELSE 
                                                                  IF a228 THEN FALSE
                                                                  ELSE TRUE
                                                                  ENDIF
                                                                ENDIF THEN a231
                                                              ELSE 
                                                                IF a231 THEN FALSE
                                                                ELSE TRUE
                                                                ENDIF
                                                              ENDIF THEN 
                                                              IF 
                                                                IF 
                                                                  IF p THEN a88
                                                                  ELSE 
                                                                    IF a46 THEN s
                                                                    ELSE FALSE
                                                                    ENDIF
                                                                  ENDIF THEN a237
                                                                ELSE 
                                                                  IF a237 THEN FALSE
                                                                  ELSE TRUE
                                                                  ENDIF
                                                                ENDIF THEN 
                                                                IF 
                                                                  IF 
                                                                    IF P1 THEN 
                                                                      IF P2 THEN TRUE
                                                                      ELSE P3
                                                                      ENDIF
                                                                    ELSE 
                                                                      IF P3 THEN TRUE
                                                                      ELSE P4
                                                                      ENDIF
                                                                    ENDIF THEN 
                                                                    IF 
                                                                      IF P3 THEN 
                                                                        IF P6 THEN FALSE
                                                                        ELSE TRUE
                                                                        ENDIF
                                                                      ELSE 
                                                                        IF P4 THEN P1
                                                                        ELSE TRUE
                                                                        ENDIF
                                                                      ENDIF THEN 
                                                                      IF 
                                                                        IF 
                                                                          IF P2 THEN P5
                                                                          ELSE FALSE
                                                                          ENDIF THEN FALSE
                                                                        ELSE TRUE
                                                                        ENDIF THEN 
                                                                        IF P2 THEN P5
                                                                        ELSE TRUE
                                                                        ENDIF
                                                                      ELSE FALSE
                                                                      ENDIF
                                                                    ELSE FALSE
                                                                    ENDIF
                                                                  ELSE FALSE
                                                                  ENDIF THEN 
                                                                  IF 
                                                                    IF P3 THEN P6
                                                                    ELSE TRUE
                                                                    ENDIF THEN FALSE
                                                                  ELSE TRUE
                                                                  ENDIF
                                                                ELSE TRUE
                                                                ENDIF
                                                              ELSE FALSE
                                                              ENDIF
                                                            ELSE FALSE
                                                            ENDIF
                                                          ELSE FALSE
                                                          ENDIF
                                                        ELSE FALSE
                                                        ENDIF
                                                      ELSE FALSE
                                                      ENDIF
                                                    ELSE FALSE
                                                    ENDIF
                                                  ELSE FALSE
                                                  ENDIF
                                                ELSE FALSE
                                                ENDIF
                                              ELSE FALSE
                                              ENDIF
                                            ELSE FALSE
                                            ENDIF
                                          ELSE FALSE
                                          ENDIF
                                        ELSE FALSE
                                        ENDIF
                                      ELSE FALSE
                                      ENDIF
                                    ELSE FALSE
                                    ENDIF
                                  ELSE FALSE
                                  ENDIF
                                ELSE FALSE
                                ENDIF
                              ELSE FALSE
                              ENDIF
                            ELSE FALSE
                            ENDIF
                          ELSE FALSE
                          ENDIF
                        ELSE FALSE
                        ENDIF
                      ELSE FALSE
                      ENDIF
                    ELSE FALSE
                    ENDIF
                  ELSE FALSE
                  ENDIF
                ELSE FALSE
                ENDIF
              ELSE FALSE
              ENDIF
            ELSE FALSE
            ENDIF
          ELSE FALSE
          ENDIF
        ELSE FALSE
        ENDIF;
QUERY a288;