; Automatically generated by map2smt (set-logic HORN) (declare-fun new9 (Int) Bool) (declare-fun new8 (Bool Int) Bool) (declare-fun new6 (Bool) Bool) (declare-fun new5 (Bool) Bool) (declare-fun new31 (Int) Bool) (declare-fun new30 (Int Bool) Bool) (declare-fun new3 (Bool Int) Bool) (declare-fun new251 (Bool Int) Bool) (declare-fun new2 (Int Int Bool Bool) Bool) (declare-fun new187 (Int Int Int Bool Int) Bool) (declare-fun new150 (Int Int Int Int Int) Bool) (declare-fun new148 (Int Bool Int Int Int) Bool) (declare-fun new147 (Int Int) Bool) (declare-fun new146 (Int Int Int Int) Bool) (declare-fun new145 (Int Int Bool) Bool) (declare-fun new144 (Int Bool Int Int Int Int) Bool) (declare-fun new138 (Int Int Int Int Bool) Bool) (declare-fun new137 (Int Int) Bool) (declare-fun new134 (Int) Bool) (declare-fun new133 (Int Int Int Bool) Bool) (declare-fun new124 (Int Int Int Int) Bool) (declare-fun new122 (Int Bool Int Int) Bool) (declare-fun new121 (Int Bool) Bool) (declare-fun new120 (Int Int Int) Bool) (declare-fun new119 (Int Bool) Bool) (declare-fun new114 (Int Int Int Int Bool Int) Bool) (declare-fun new113 (Int Bool Int) Bool) (declare-fun new110 (Int Bool Int) Bool) (declare-fun new107 (Int Bool Int) Bool) (declare-fun new1 (Int Bool Bool) Bool) (declare-fun diff_new701 (Bool Bool Int) Bool) (declare-fun diff_new136 (Bool Int Bool) Bool) (declare-fun diff_new131 (Bool Int Int Bool) Bool) (declare-fun diff_new112 (Bool Int Bool Int) Bool) (declare-fun diff_new109 (Bool Int Int Bool Int) Bool) (declare-fun not_fun_diff_new701 () Bool) (declare-fun constr (Bool) Bool) (declare-fun not_fun_diff_new136 () Bool) (declare-fun not_fun_diff_new131 () Bool) (declare-fun not_fun_diff_new112 () Bool) (declare-fun not_fun_diff_new109 () Bool) (declare-fun ff () Bool) (assert (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Bool) (F Int) ) (=> (and (diff_new701 A B C) (diff_new701 D E F) (and (= A D) (or (not (= B E)) (not (= C F)))) ) not_fun_diff_new701 ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) ) (=> (and (diff_new136 A B C) (diff_new136 D E F) (and (= A D) (or (not (= B E)) (not (= C F)))) ) not_fun_diff_new136 ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Bool) ) (=> (and (diff_new131 A B C D) (diff_new131 E F G H) (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H))))) ) not_fun_diff_new131 ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) ) (=> (and (diff_new112 A B C D) (diff_new112 E F G H) (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H))))) ) not_fun_diff_new112 ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Int) (H Int) (I Bool) (J Int) ) (=> (and (diff_new109 A B C D E) (diff_new109 F G H I J) (and (= A F) (or (not (= B G)) (or (not (= C H)) (or (not (= D I)) (not (= E J)))))) ) not_fun_diff_new109 ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) ) (=> (and (= B true) (= A true) (= C 0) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= C D) (<= C D) (= E (+ 1 C)) (= B (+ 1 C)) (new3 A D) (new3 A C) ) (diff_new701 A A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (= B (+ 1 C)) (new9 C) (new5 A) ) (diff_new701 A A B) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= A false) (= C (+ 1 D)) (new3 B D) (new5 A) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= B false) (= A false) (>= D (+ E 1)) (= C (+ 1 D)) (new3 A E) (new9 D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (<= (+ D 1) (+ 1 E)) (= C (+ 1 E)) (new9 E) (new5 A) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (= C (+ 1 E)) (new9 E) (new5 A) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= A false) (= C (+ 1 D)) (new5 B) (new3 A D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (= B (+ 1 C)) (new3 A C) ) (diff_new701 A A B) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= B false) (= A false) (>= D (+ E 1)) (= C (+ 1 D)) (new9 E) (new3 A D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (<= (+ D 1) (+ 1 E)) (= C (+ 1 E)) (new3 A E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (= C (+ 1 E)) (new3 A E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= A false) (= B false) (= A false) (>= D (+ E 1)) (= C (+ 1 D)) (new3 B E) (new9 D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= A false) (= B false) (= A false) (>= D (+ E 1)) (= C (+ 1 D)) (new3 B D) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (= B false) (= A false) (>= D (+ E 1)) (>= D (+ E 1)) (= C (+ 1 D)) (new9 E) (new9 D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= B false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (= C (+ 1 D)) (new9 E) (new9 D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (= C (+ 1 E)) (new9 F) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (<= (+ D 1) (+ 1 E)) (= C (+ 1 E)) (new5 B) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (<= (+ D 1) (+ 1 E)) (= C (+ 1 E)) (new3 B E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= B false) (= B false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (= C (+ 1 D)) (new9 E) (new9 D) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (<= (+ D 1) (+ 1 E)) (= C (+ 1 E)) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (= C (+ 1 E)) (new5 B) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (= C (+ 1 E)) (new3 B E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= B false) (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (= C (+ 1 E)) (new9 F) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= A false) (>= D (+ (+ 1 E) 1)) (= C (+ 1 E)) (new9 E) ) (diff_new701 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A true) (= B 0) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (<= C D) (= E (+ 1 C)) (= B (+ 1 C)) (new251 A D) (new251 A C) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new31 C) (new6 A) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new251 A C) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (>= C (+ D 1)) (= B (+ 1 C)) (new31 D) (new31 C) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (<= (+ C 1) (+ 1 D)) (= B (+ 1 D)) (new31 D) ) (new251 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (>= C (+ (+ 1 D) 1)) (= B (+ 1 D)) (new31 D) ) (new251 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) ) (=> (and (= C true) (= D 0) (= A 1) ) (new187 A A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= D true) (= D true) (<= H I) (<= J (- C 1)) (<= K L) (= L 0) (= A (+ 1 K)) (= K (+ 1 H)) (= E (+ 1 H)) (= B 1) (new251 D I) (new251 D H) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= D false) (<= H (- C 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new6 D) (new31 K) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= D false) (<= H (- C 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new251 D K) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= D false) (= D false) (>= H (+ I 1)) (<= J (- C 1)) (<= K L) (= L 0) (= A (+ 1 K)) (= E (+ 1 H)) (= B 1) (new31 I) (new31 H) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= D false) (<= (+ H 1) (+ 1 I)) (<= J (- C 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= E (+ 1 I)) (= B 1) (new31 I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= D false) (>= H (+ (+ 1 I) 1)) (<= J (- C 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= E (+ 1 I)) (= B 1) (new31 I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (= D true) (= D true) (>= H (+ I 1)) (<= J K) (<= L (- C 1)) (= I 0) (= M 0) (= A (+ 1 M)) (= H (+ 1 J)) (= E (+ 1 J)) (= B 1) (new251 D K) (new251 D J) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= D false) (>= H (+ I 1)) (<= J (- C 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= E (+ 1 L)) (= B 1) (new6 D) (new31 L) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= D false) (>= H (+ I 1)) (<= J (- C 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= E (+ 1 L)) (= B 1) (new251 D L) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (= D false) (= D false) (>= H (+ I 1)) (>= J (+ K 1)) (<= L (- C 1)) (= K 0) (= M 0) (= A (+ 1 M)) (= E (+ 1 H)) (= B 1) (new31 I) (new31 H) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= D false) (>= H (+ I 1)) (<= (+ H 1) (+ 1 J)) (<= K (- C 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= E (+ 1 J)) (= B 1) (new31 J) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= D false) (>= H (+ I 1)) (>= H (+ (+ 1 J) 1)) (<= K (- C 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= E (+ 1 J)) (= B 1) (new31 J) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= D true) (= D true) (>= H C) (<= I J) (<= K L) (= M (+ 1 I)) (= A (+ 1 K)) (= E (+ 1 I)) (= B 1) (new110 L D J) (new187 K B C D I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= D false) (>= H C) (<= I J) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new121 J D) (new146 I B C K) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= D false) (>= H C) (<= I J) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new134 J) (new187 I B C D K) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (= D false) (= D false) (>= H (+ I 1)) (>= J C) (<= K L) (= A (+ 1 K)) (= E (+ 1 H)) (= B 1) (new147 L I) (new146 K B C H) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (= D false) (>= H C) (<= (+ I 1) (+ 1 J)) (<= K L) (= A (+ 1 K)) (= E (+ 1 J)) (= B 1) (new134 L) (new146 K B C J) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (= D false) (>= H (+ (+ 1 I) 1)) (>= J C) (<= K L) (= A (+ 1 K)) (= E (+ 1 I)) (= B 1) (new134 L) (new146 K B C I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= D true) (= D true) (>= H (+ I 1)) (>= J C) (<= K L) (= M (+ 1 K)) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new187 H B C D K) (new110 I D L) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= D false) (>= H (+ I 1)) (>= J C) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new146 H B C K) (new121 I D) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= D false) (>= H (+ I 1)) (>= J C) (= A (+ 1 I)) (= E (+ 1 K)) (= B 1) (new187 H B C D K) (new134 I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= D false) (= D false) (>= H (+ I 1)) (>= J (+ K 1)) (>= L C) (= A (+ 1 K)) (= E (+ 1 H)) (= B 1) (new146 J B C H) (new147 K I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= D false) (>= H (+ I 1)) (>= J C) (<= (+ K 1) (+ 1 L)) (= A (+ 1 I)) (= E (+ 1 L)) (= B 1) (new146 H B C L) (new134 I) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= D false) (>= H (+ (+ 1 I) 1)) (>= J (+ K 1)) (>= L C) (= A (+ 1 K)) (= E (+ 1 I)) (= B 1) (new146 J B C I) (new134 K) ) (new187 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= E 0) (= D 0) (= A 1) (= B (+ 1 E)) ) (new150 A B A C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (<= H (- D 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= K (+ 1 L)) (= E (+ 1 L)) (= C 1) (= B (+ 1 K)) (new9 L) ) (new150 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (>= H (+ I 1)) (<= J (- D 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= L 0) (= E (+ 1 M)) (= C 1) (= B (+ 1 L)) (new31 M) ) (new150 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (>= H D) (<= I J) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (= B (+ 1 L)) (new134 J) (new150 I L C D K) ) (new150 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (>= H (+ I 1)) (>= J D) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (= B (+ 1 L)) (new146 H C D K) (new137 I L) ) (new150 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= B true) (= B true) (= B true) (= B true) (<= E F) (= E 0) (= F 0) (= G 0) (= D 0) (= A (+ 1 G)) (= A 1) ) (new148 A B A C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= F true) (= G true) (= B true) (= B true) (= B true) (= B true) (= B true) (<= H I) (<= J K) (<= L (- D 1)) (<= M N) (= J (+ 1 H)) (= K 0) (= N 0) (= O (+ 1 H)) (= A (+ 1 O)) (= A (+ 1 M)) (= M (+ 1 H)) (= E (+ 1 H)) (= C 1) (new3 B I) (new3 B H) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (<= H (- D 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new31 K) (new5 B) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (<= H (- D 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new30 K B) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (= B false) (>= H (+ I 1)) (<= J (- D 1)) (<= K L) (= L 0) (= A (+ 1 K)) (= E (+ 1 H)) (= C 1) (new9 I) (new9 H) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (<= (+ H 1) (+ 1 I)) (<= J (- D 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= E (+ 1 I)) (= C 1) (new9 I) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (>= H (+ (+ 1 I) 1)) (<= J (- D 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= E (+ 1 I)) (= C 1) (new9 I) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G true) (= B false) (= B false) (>= H (+ I 1)) (<= J (- D 1)) (<= K L) (= H (+ 1 M)) (= I 0) (= L 0) (= A (+ 1 K)) (= E (+ 1 M)) (= C 1) (new9 M) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= B false) (<= (+ A 1) (+ 1 H)) (<= I (- D 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= A (+ 1 J)) (= E (+ 1 L)) (= C 1) (new9 L) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= B false) (>= A (+ (+ 1 H) 1)) (<= I (- D 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= A (+ 1 J)) (= E (+ 1 L)) (= C 1) (new9 L) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) ) (=> (and (= F false) (= G true) (= B true) (= B true) (= B true) (= B true) (= B true) (>= H (+ I 1)) (<= J K) (<= L M) (<= N (- D 1)) (= L 0) (= M (+ 1 J)) (= I 0) (= O 0) (= P 0) (= A (+ 1 O)) (= A (+ 1 P)) (= H (+ 1 J)) (= E (+ 1 J)) (= C 1) (new3 B K) (new3 B J) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (>= H (+ I 1)) (<= J (- D 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= E (+ 1 L)) (= C 1) (new31 L) (new5 B) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (>= H (+ I 1)) (<= J (- D 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= E (+ 1 L)) (= C 1) (new30 L B) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (= B false) (>= H (+ I 1)) (>= J (+ K 1)) (<= L (- D 1)) (= K 0) (= M 0) (= A (+ 1 M)) (= E (+ 1 H)) (= C 1) (new9 I) (new9 H) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (>= H (+ I 1)) (<= (+ H 1) (+ 1 J)) (<= K (- D 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= E (+ 1 J)) (= C 1) (new9 J) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (>= H (+ I 1)) (>= H (+ (+ 1 J) 1)) (<= K (- D 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= E (+ 1 J)) (= C 1) (new9 J) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= F false) (= G true) (= B false) (= B false) (>= H (+ I 1)) (>= J (+ K 1)) (<= L (- D 1)) (= H 0) (= I (+ 1 M)) (= K 0) (= N 0) (= A (+ 1 N)) (= E (+ 1 M)) (= C 1) (new9 M) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= B true) (= B true) (>= H D) (<= I J) (<= K L) (= A (+ 1 I)) (= A (+ 1 K)) (= E (+ 1 M)) (= C 1) (new107 L B J) (new144 K B I C D M) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= B false) (>= H D) (<= I J) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new119 J B) (new146 I C D K) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= B false) (>= H D) (<= I J) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new134 J) (new148 I B C D K) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= B false) (= B false) (>= H (+ I 1)) (>= J D) (<= K L) (= A (+ 1 K)) (= E (+ 1 M)) (= C 1) (new137 L I) (new150 K H C D M) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (= B false) (>= H D) (<= (+ A 1) (+ 1 I)) (<= J K) (= A (+ 1 J)) (= E (+ 1 L)) (= C 1) (new134 K) (new150 J I C D L) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G false) (= B false) (>= A (+ (+ 1 H) 1)) (>= I D) (<= J K) (= A (+ 1 J)) (= E (+ 1 L)) (= C 1) (new134 K) (new150 J H C D L) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= B true) (= B true) (>= H (+ I 1)) (>= J D) (<= K L) (= A (+ 1 K)) (= A (+ 1 I)) (= E (+ 1 M)) (= C 1) (new144 H B L C D M) (new107 I B K) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= B false) (>= H (+ I 1)) (>= J D) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new148 H B C D K) (new134 I) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= B false) (>= H (+ I 1)) (>= J D) (= A (+ 1 I)) (= E (+ 1 K)) (= C 1) (new146 H C D K) (new119 I B) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= B false) (= B false) (>= H (+ I 1)) (>= J (+ K 1)) (>= L D) (= A (+ 1 K)) (= E (+ 1 M)) (= C 1) (new150 J I C D M) (new137 K H) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= B false) (>= H (+ I 1)) (>= J D) (<= (+ A 1) (+ 1 K)) (= A (+ 1 I)) (= E (+ 1 L)) (= C 1) (new146 H C D L) (new137 I K) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= B false) (>= H (+ I 1)) (>= A (+ (+ 1 J) 1)) (>= K D) (= A (+ 1 I)) (= E (+ 1 L)) (= C 1) (new146 H C D L) (new137 I J) ) (new148 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) ) (=> (and (= B 0) (= A 0) ) (new147 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) ) (=> (and (= B (+ 1 C)) (new31 C) ) (new147 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) ) (=> (and (= C 0) (= A 1) ) (new146 A A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (<= G (- C 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= D (+ 1 J)) (= B 1) (new31 J) ) (new146 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (>= G (+ H 1)) (<= I (- C 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= D (+ 1 K)) (= B 1) (new31 K) ) (new146 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (>= G C) (<= H I) (= A (+ 1 H)) (= D (+ 1 J)) (= B 1) (new134 I) (new146 H B C J) ) (new146 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (>= G (+ H 1)) (>= I C) (= A (+ 1 H)) (= D (+ 1 J)) (= B 1) (new146 G B C J) (new134 H) ) (new146 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) ) (=> (and (= C true) (= B 0) (= A 0) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C true) (= C true) (<= D E) (= A (+ 1 D)) (= B (+ 1 D)) (new3 C E) (new3 C D) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) ) (=> (and (= C false) (= B (+ 1 D)) (new31 D) (new5 C) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) ) (=> (and (= C false) (= B (+ 1 D)) (new30 D C) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= C false) (>= D (+ E 1)) (= B (+ 1 D)) (new9 E) (new9 D) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) ) (=> (and (= C false) (<= (+ A 1) (+ 1 D)) (= B (+ 1 D)) (new9 D) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Int) ) (=> (and (= C false) (>= A (+ (+ 1 D) 1)) (= B (+ 1 D)) (new9 D) ) (new145 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= B true) (= B true) (= B true) (= B true) (<= F G) (= F 0) (= G 0) (= H 0) (= I 0) (= E 0) (= A (+ 1 H)) (= A 1) (= C (+ 1 I)) ) (new144 A B C A D E) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) ) (=> (and (= G true) (= H true) (= B true) (= B true) (= B true) (= B true) (= B true) (<= I J) (<= K L) (<= M (- E 1)) (<= N O) (= K (+ 1 I)) (= L 0) (= O 0) (= P (+ 1 I)) (= A (+ 1 P)) (= A (+ 1 N)) (= N (+ 1 I)) (= Q (+ 1 I)) (= F (+ 1 I)) (= D 1) (= C (+ 1 Q)) (new3 B J) (new3 B I) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (<= I (- E 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= L (+ 1 M)) (= F (+ 1 M)) (= D 1) (= C (+ 1 L)) (new5 B) (new9 M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (<= I (- E 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= L (+ 1 M)) (= F (+ 1 M)) (= D 1) (= C (+ 1 L)) (new3 B M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (= B false) (>= I (+ J 1)) (<= K (- E 1)) (<= L M) (= M 0) (= A (+ 1 L)) (= N (+ 1 I)) (= F (+ 1 I)) (= D 1) (= C (+ 1 N)) (new9 J) (new9 I) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (<= (+ I 1) (+ 1 J)) (<= K (- E 1)) (<= I L) (= L 0) (= A (+ 1 I)) (= M (+ 1 J)) (= F (+ 1 J)) (= D 1) (= C (+ 1 M)) (new9 J) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (>= I (+ (+ 1 J) 1)) (<= K (- E 1)) (<= I L) (= L 0) (= A (+ 1 I)) (= M (+ 1 J)) (= F (+ 1 J)) (= D 1) (= C (+ 1 M)) (new9 J) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= G true) (= H true) (= B false) (= B false) (>= I (+ J 1)) (<= K (- E 1)) (<= L M) (= I (+ 1 N)) (= J 0) (= M 0) (= A (+ 1 L)) (= O (+ 1 N)) (= F (+ 1 N)) (= D 1) (= C (+ 1 O)) (new9 N) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H true) (= B false) (<= (+ A 1) (+ 1 I)) (<= J (- E 1)) (<= K L) (= I (+ 1 M)) (= L 0) (= A (+ 1 K)) (= N (+ 1 M)) (= F (+ 1 M)) (= D 1) (= C (+ 1 N)) (new9 M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H true) (= B false) (>= A (+ (+ 1 I) 1)) (<= J (- E 1)) (<= K L) (= I (+ 1 M)) (= L 0) (= A (+ 1 K)) (= N (+ 1 M)) (= F (+ 1 M)) (= D 1) (= C (+ 1 N)) (new9 M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) ) (=> (and (= G false) (= H true) (= B true) (= B true) (= B true) (= B true) (= B true) (>= I (+ J 1)) (<= K L) (<= M N) (<= O (- E 1)) (= M 0) (= N (+ 1 K)) (= J 0) (= P 0) (= Q 0) (= A (+ 1 P)) (= A (+ 1 Q)) (= I (+ 1 K)) (= R 0) (= F (+ 1 K)) (= D 1) (= C (+ 1 R)) (new3 B L) (new3 B K) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (>= I (+ J 1)) (<= K (- E 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= M 0) (= F (+ 1 N)) (= D 1) (= C (+ 1 M)) (new31 N) (new5 B) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (>= I (+ J 1)) (<= K (- E 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= M 0) (= F (+ 1 N)) (= D 1) (= C (+ 1 M)) (new30 N B) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (= B false) (>= I (+ J 1)) (>= K (+ L 1)) (<= M (- E 1)) (= L 0) (= N 0) (= A (+ 1 N)) (= O 0) (= F (+ 1 I)) (= D 1) (= C (+ 1 O)) (new9 J) (new9 I) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (>= I (+ J 1)) (<= (+ I 1) (+ 1 K)) (<= L (- E 1)) (= J 0) (= M 0) (= A (+ 1 M)) (= N 0) (= F (+ 1 K)) (= D 1) (= C (+ 1 N)) (new9 K) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (>= I (+ J 1)) (>= I (+ (+ 1 K) 1)) (<= L (- E 1)) (= J 0) (= M 0) (= A (+ 1 M)) (= N 0) (= F (+ 1 K)) (= D 1) (= C (+ 1 N)) (new9 K) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) ) (=> (and (= G false) (= H true) (= B false) (= B false) (>= I (+ J 1)) (>= K (+ L 1)) (<= M (- E 1)) (= I 0) (= J (+ 1 N)) (= L 0) (= O 0) (= A (+ 1 O)) (= P 0) (= F (+ 1 N)) (= D 1) (= C (+ 1 P)) (new9 N) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H false) (= B true) (= B true) (>= I E) (<= J K) (<= L M) (= A (+ 1 L)) (= A (+ 1 J)) (= F (+ 1 N)) (= D 1) (= C (+ 1 J)) (new107 M B K) (new144 L B J D E N) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= B false) (>= I E) (<= J K) (= A (+ 1 J)) (= F (+ 1 L)) (= D 1) (= C (+ 1 M)) (new119 K B) (new150 J M D E L) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= B false) (>= I E) (<= J K) (= A (+ 1 J)) (= F (+ 1 L)) (= D 1) (= C (+ 1 M)) (new134 K) (new144 J B M D E L) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H false) (= B false) (= B false) (>= I (+ J 1)) (>= K E) (<= L M) (= A (+ 1 L)) (= F (+ 1 N)) (= D 1) (= C (+ 1 I)) (new137 M J) (new150 L I D E N) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= B false) (>= I E) (<= (+ A 1) (+ 1 J)) (<= K L) (= A (+ 1 K)) (= F (+ 1 M)) (= D 1) (= C (+ 1 J)) (new134 L) (new150 K J D E M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= B false) (>= A (+ (+ 1 I) 1)) (>= J E) (<= K L) (= A (+ 1 K)) (= F (+ 1 M)) (= D 1) (= C (+ 1 I)) (new134 L) (new150 K I D E M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H false) (= B true) (= B true) (>= I (+ J 1)) (>= K E) (<= L M) (= A (+ 1 J)) (= A (+ 1 L)) (= F (+ 1 N)) (= D 1) (= C (+ 1 L)) (new144 I B M D E N) (new107 J B L) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= B false) (>= I (+ J 1)) (>= K E) (= A (+ 1 J)) (= F (+ 1 L)) (= D 1) (= C (+ 1 M)) (new148 I B D E L) (new137 J M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= B false) (>= I (+ J 1)) (>= K E) (= A (+ 1 J)) (= F (+ 1 L)) (= D 1) (= C (+ 1 M)) (new146 I D E L) (new107 J B M) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H false) (= B false) (= B false) (>= I (+ J 1)) (>= K (+ L 1)) (>= M E) (= A (+ 1 L)) (= F (+ 1 N)) (= D 1) (= C (+ 1 I)) (new150 K J D E N) (new137 L I) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= B false) (>= I (+ J 1)) (>= K E) (<= (+ A 1) (+ 1 L)) (= A (+ 1 J)) (= F (+ 1 M)) (= D 1) (= C (+ 1 L)) (new146 I D E M) (new137 J L) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= B false) (>= I (+ J 1)) (>= A (+ (+ 1 K) 1)) (>= L E) (= A (+ 1 J)) (= F (+ 1 M)) (= D 1) (= C (+ 1 K)) (new146 I D E M) (new137 J K) ) (new144 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) ) (=> (and (= D true) (= E 0) (= A 1) (= B (+ 1 E)) ) (new138 A B A C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G true) (= E true) (= E true) (<= H I) (<= J (- D 1)) (<= K L) (= L 0) (= A (+ 1 K)) (= K (+ 1 H)) (= M (+ 1 H)) (= C 1) (= B (+ 1 M)) (new251 E I) (new8 E H) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= E false) (<= H (- D 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= K (+ 1 L)) (= C 1) (= B (+ 1 K)) (new6 E) (new9 L) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= E false) (<= H (- D 1)) (<= I J) (= J 0) (= A (+ 1 I)) (= K (+ 1 L)) (= C 1) (= B (+ 1 K)) (new8 E L) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G true) (= E false) (= E false) (>= H (+ I 1)) (<= J (- D 1)) (<= K L) (= L 0) (= A (+ 1 K)) (= M (+ 1 H)) (= C 1) (= B (+ 1 M)) (new31 I) (new9 H) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= E false) (<= (+ H 1) (+ 1 I)) (<= J (- D 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= L (+ 1 I)) (= C 1) (= B (+ 1 L)) (new9 I) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F true) (= G true) (= E false) (>= H (+ (+ 1 I) 1)) (<= J (- D 1)) (<= H K) (= K 0) (= A (+ 1 H)) (= L (+ 1 I)) (= C 1) (= B (+ 1 L)) (new9 I) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= F false) (= G true) (= E true) (= E true) (>= H (+ I 1)) (<= J K) (<= L (- D 1)) (= I 0) (= M 0) (= A (+ 1 M)) (= H (+ 1 J)) (= N 0) (= C 1) (= B (+ 1 N)) (new251 E K) (new251 E J) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= E false) (>= H (+ I 1)) (<= J (- D 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= L 0) (= C 1) (= B (+ 1 L)) (new6 E) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G true) (= E false) (>= H (+ I 1)) (<= J (- D 1)) (= I 0) (= K 0) (= A (+ 1 K)) (= L 0) (= C 1) (= B (+ 1 L)) (new6 E) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= F false) (= G true) (= E false) (= E false) (>= H (+ I 1)) (>= J (+ K 1)) (<= L (- D 1)) (= K 0) (= M 0) (= A (+ 1 M)) (= N 0) (= C 1) (= B (+ 1 N)) (new31 I) (new31 H) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (= E false) (>= H (+ I 1)) (<= (+ H 1) (+ 1 J)) (<= K (- D 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= M 0) (= C 1) (= B (+ 1 M)) (new31 J) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G true) (= E false) (>= H (+ I 1)) (>= H (+ (+ 1 J) 1)) (<= K (- D 1)) (= I 0) (= L 0) (= A (+ 1 L)) (= M 0) (= C 1) (= B (+ 1 M)) (new31 J) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= F true) (= G false) (= E true) (= E true) (>= H D) (<= I J) (<= K L) (= M (+ 1 I)) (= A (+ 1 K)) (= C 1) (= B (+ 1 N)) (new110 L E J) (new114 K N C D E I) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= E false) (>= H D) (<= I J) (= A (+ 1 I)) (= C 1) (= B (+ 1 K)) (new121 J E) (new124 I K C D) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F true) (= G false) (= E false) (>= H D) (<= I J) (= A (+ 1 I)) (= C 1) (= B (+ 1 K)) (new134 J) (new138 I K C D E) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= E false) (= E false) (>= H (+ I 1)) (>= J D) (<= K L) (= A (+ 1 K)) (= C 1) (= B (+ 1 M)) (new147 L I) (new150 K M C D H) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= E false) (>= H D) (<= (+ I 1) (+ 1 J)) (<= K L) (= A (+ 1 K)) (= C 1) (= B (+ 1 M)) (new134 L) (new150 K M C D J) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F true) (= G false) (= E false) (>= H (+ (+ 1 I) 1)) (>= J D) (<= K L) (= A (+ 1 K)) (= C 1) (= B (+ 1 M)) (new134 L) (new150 K M C D I) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= E true) (= E true) (>= H (+ I 1)) (>= J D) (<= K L) (= M (+ 1 K)) (= A (+ 1 I)) (= C 1) (= B (+ 1 L)) (new187 H C D E K) (new113 I E L) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= E false) (>= H (+ I 1)) (>= J D) (= A (+ 1 I)) (= C 1) (= B (+ 1 K)) (new120 H C D) (new113 I E K) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= F false) (= G false) (= E false) (>= H (+ I 1)) (>= J D) (= A (+ 1 I)) (= C 1) (= B (+ 1 K)) (new133 H C D E) (new137 I K) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= F false) (= G false) (= E false) (= E false) (>= H (+ I 1)) (>= J (+ K 1)) (>= L D) (= A (+ 1 K)) (= C 1) (= B (+ 1 I)) (new146 J C D H) (new137 K I) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= E false) (>= H (+ I 1)) (>= J D) (<= (+ K 1) (+ 1 L)) (= A (+ 1 I)) (= C 1) (= B (+ 1 M)) (new146 H C D L) (new137 I M) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= F false) (= G false) (= E false) (>= H (+ (+ 1 I) 1)) (>= J (+ K 1)) (>= L D) (= A (+ 1 K)) (= C 1) (= B (+ 1 M)) (new146 J C D I) (new137 K M) ) (new138 A B C D E) ) ) ) (assert (forall ( (A Int) (B Int) ) (=> (and (= B 0) (= A 0) ) (new137 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) ) (=> (and (= B (+ 1 C)) (new9 C) ) (new137 A B) ) ) ) (assert (forall ( (A Int) ) (=> (= A 0) (new134 A) ) ) ) (assert (forall ( (A Int) ) (new134 A) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C true) (= A true) (= B 0) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C true) (= A true) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= C D) (<= C D) (= E (+ 1 C)) (= B 0) (new251 A D) (new251 A C) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= C D) (<= C D) (= E (+ 1 C)) (new251 A D) (new251 A C) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A false) (= A false) (= B 0) (new6 A) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C false) (= A false) (= B 0) (new6 C) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (= B 0) (new251 A E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (= B 0) (new31 E) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (= B 0) (new31 E) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A false) (= A false) (new6 A) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C false) (= A false) (new6 C) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (new251 A E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (new31 E) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (new31 E) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C false) (= A false) (= B 0) (new6 C) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A false) (= A false) (= B 0) (new6 A) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (= B 0) (new31 E) (new251 A D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (= B 0) (new251 A E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (= B 0) (new251 A E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) ) (=> (and (= C false) (= A false) (new6 C) (new6 A) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A false) (= A false) (new6 A) ) (diff_new136 A B A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (new31 E) (new251 A D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (new251 A E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (new251 A E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (= B 0) (new251 C E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (= B 0) (new251 C D) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= C false) (= A false) (>= D (+ E 1)) (>= D (+ E 1)) (= B 0) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (= B 0) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (= B 0) (new31 F) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (new251 C E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (new251 C D) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= C false) (= A false) (>= D (+ E 1)) (>= D (+ E 1)) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (new31 F) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (= B 0) (new6 C) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (= B 0) (new251 C E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (= B 0) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (= B 0) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (new6 C) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (new251 C E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ E 1)) (<= (+ F 1) (+ 1 D)) (new31 E) (new31 D) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (<= (+ D 1) (+ 1 E)) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (= B 0) (new6 C) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (= B 0) (new251 C E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (= B 0) (new31 F) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (= B 0) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (new6 C) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (new251 C E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (>= E (+ F 1)) (new31 F) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (>= D (+ (+ 1 E) 1)) (new31 E) ) (diff_new136 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) ) (=> (and (= C true) (= A 1) ) (new133 A A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D true) (= D true) (<= G H) (<= I (- C 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= J (+ 1 G)) (= B 1) (new251 D H) (new251 D G) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F true) (= D false) (<= G (- C 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= B 1) (new6 D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F true) (= D false) (<= G (- C 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= B 1) (new6 D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (>= G (+ H 1)) (<= I (- C 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= B 1) (new31 H) (new31 G) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= D false) (<= (+ G 1) (+ 1 H)) (<= I (- C 1)) (<= G J) (= J 0) (= A (+ 1 G)) (= B 1) (new31 H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= D false) (>= G (+ (+ 1 H) 1)) (<= I (- C 1)) (<= G J) (= J 0) (= A (+ 1 G)) (= B 1) (new31 H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D true) (= D true) (>= G (+ H 1)) (<= I J) (<= K (- C 1)) (= H 0) (= L 0) (= A (+ 1 L)) (= G (+ 1 I)) (= B 1) (new251 D J) (new251 D I) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F true) (= D false) (>= G (+ H 1)) (<= I (- C 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= B 1) (new6 D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F true) (= D false) (>= G (+ H 1)) (<= I (- C 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= B 1) (new6 D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- C 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= B 1) (new31 H) (new31 G) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= D false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- C 1)) (= H 0) (= K 0) (= A (+ 1 K)) (= B 1) (new31 I) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= D false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- C 1)) (= H 0) (= K 0) (= A (+ 1 K)) (= B 1) (new31 I) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D true) (= D true) (>= G C) (<= H I) (<= J K) (= L (+ 1 H)) (= A (+ 1 J)) (= B 1) (new110 K D I) (new187 J B C D H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F false) (= D false) (>= G C) (<= H I) (= A (+ 1 H)) (= B 1) (new121 I D) (new120 H B C) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F false) (= D false) (>= G C) (<= H I) (= A (+ 1 H)) (= B 1) (new134 I) (new133 H B C D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (= D false) (>= G (+ H 1)) (>= I C) (<= J K) (= A (+ 1 J)) (= B 1) (new147 K H) (new146 J B C G) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (>= G C) (<= (+ H 1) (+ 1 I)) (<= J K) (= A (+ 1 J)) (= B 1) (new134 K) (new146 J B C I) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (>= G (+ (+ 1 H) 1)) (>= I C) (<= J K) (= A (+ 1 J)) (= B 1) (new134 K) (new146 J B C H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D true) (= D true) (>= G (+ H 1)) (>= I C) (<= J K) (= L (+ 1 J)) (= A (+ 1 H)) (= B 1) (new187 G B C D J) (new110 H D K) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E false) (= F false) (= D false) (>= G (+ H 1)) (>= I C) (= A (+ 1 H)) (= B 1) (new120 G B C) (new121 H D) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E false) (= F false) (= D false) (>= G (+ H 1)) (>= I C) (= A (+ 1 H)) (= B 1) (new133 G B C D) (new134 H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (= D false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K C) (= A (+ 1 J)) (= B 1) (new146 I B C G) (new147 J H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (>= G (+ H 1)) (>= I C) (<= (+ J 1) (+ 1 K)) (= A (+ 1 H)) (= B 1) (new146 G B C K) (new134 H) ) (new133 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K C) (= A (+ 1 J)) (= B 1) (new146 I B C H) (new134 J) ) (new133 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) ) (=> (and (= D true) (= A true) (= C 0) (= B 0) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) ) (=> (and (= D true) (= A true) (= C (+ 1 E)) (new9 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= D E) (<= D E) (= F (+ 1 D)) (= C 0) (= B 0) (new251 A E) (new251 A D) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= D E) (<= D E) (= F (+ 1 D)) (= C (+ 1 G)) (new9 G) (new251 A E) (new251 A D) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (= C 0) (= B 0) (new6 A) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) ) (=> (and (= D false) (= A false) (= C 0) (= B 0) (new6 D) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (= C 0) (= B 0) (new251 A F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C 0) (= B 0) (new31 F) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C 0) (= B 0) (new31 F) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (new9 D) (new6 A) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) ) (=> (and (= D false) (= A false) (= C (+ 1 E)) (new6 D) (new9 E) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (= C (+ 1 G)) (new251 A F) (new31 E) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C (+ 1 G)) (new31 F) (new9 G) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C (+ 1 G)) (new31 F) (new9 G) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) ) (=> (and (= D false) (= A false) (= C 0) (= B 0) (new6 D) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (= C 0) (= B 0) (new6 A) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (= C 0) (= B 0) (new31 F) (new251 A E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C 0) (= B 0) (new251 A F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C 0) (= B 0) (new251 A F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) ) (=> (and (= D false) (= A false) (= C (+ 1 E)) (new6 D) (new9 E) (new6 A) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (new9 D) (new6 A) ) (diff_new131 A B C A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (= C (+ 1 G)) (new31 F) (new251 A E) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C (+ 1 G)) (new251 A F) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C (+ 1 G)) (new251 A F) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (= C 0) (= B 0) (new251 D F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (= C 0) (= B 0) (new251 D E) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (= D false) (= A false) (>= E (+ F 1)) (>= E (+ F 1)) (= C 0) (= B 0) (new31 F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= C 0) (= B 0) (new31 F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= C 0) (= B 0) (new31 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (= C (+ 1 G)) (new251 D F) (new9 G) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (= C (+ 1 G)) (new251 D E) (new9 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (= D false) (= A false) (>= E (+ F 1)) (>= E (+ F 1)) (= C (+ 1 G)) (new9 G) (new31 F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= C (+ 1 H)) (new9 H) (new31 F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= C (+ 1 H)) (new9 H) (new31 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C 0) (= B 0) (new6 D) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C 0) (= B 0) (new251 D F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= C 0) (= B 0) (new31 F) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C 0) (= B 0) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C (+ 1 G)) (new6 D) (new9 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C (+ 1 G)) (new251 D F) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= C (+ 1 H)) (new31 F) (new9 H) (new31 E) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ E 1) (+ 1 F)) (= C (+ 1 G)) (new9 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C 0) (= B 0) (new6 D) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C 0) (= B 0) (new251 D F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= C 0) (= B 0) (new31 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C 0) (= B 0) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C (+ 1 G)) (new6 D) (new9 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C (+ 1 G)) (new251 D F) (new9 G) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= C (+ 1 H)) (new31 G) (new9 H) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= E (+ (+ 1 F) 1)) (= C (+ 1 G)) (new9 G) (new31 F) ) (diff_new131 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) ) (=> (and (= D 0) (= A 1) (= B (+ 1 D)) ) (new124 A B A C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (<= G (- D 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= J (+ 1 K)) (= C 1) (= B (+ 1 J)) (new9 K) ) (new124 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (>= G (+ H 1)) (<= I (- D 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= K 0) (= C 1) (= B (+ 1 K)) ) (new124 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (>= G D) (<= H I) (= A (+ 1 H)) (= C 1) (= B (+ 1 J)) (new134 I) (new124 H J C D) ) (new124 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (>= G (+ H 1)) (>= I D) (= A (+ 1 H)) (= C 1) (= B (+ 1 J)) (new120 G C D) (new137 H J) ) (new124 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= B true) (= B true) (= B true) (= B true) (<= D E) (= D 0) (= E 0) (= F 0) (= A (+ 1 F)) (= A 1) ) (new122 A B A C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F true) (= B true) (= B true) (= B true) (= B true) (= B true) (<= G H) (<= I J) (<= K (- D 1)) (<= L M) (= I (+ 1 G)) (= J 0) (= M 0) (= N (+ 1 G)) (= A (+ 1 N)) (= A (+ 1 L)) (= L (+ 1 G)) (= C 1) (new3 B H) (new3 B G) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (<= G (- D 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= C 1) (new5 B) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (<= G (- D 1)) (<= H I) (= I 0) (= A (+ 1 H)) (= C 1) (new5 B) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (= B false) (>= G (+ H 1)) (<= I (- D 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= C 1) (new9 H) (new9 G) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (<= (+ G 1) (+ 1 H)) (<= I (- D 1)) (<= G J) (= J 0) (= A (+ 1 G)) (= C 1) (new9 H) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (>= G (+ (+ 1 H) 1)) (<= I (- D 1)) (<= G J) (= J 0) (= A (+ 1 G)) (= C 1) (new9 H) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= B false) (= B false) (>= G (+ H 1)) (<= I (- D 1)) (<= J K) (= G (+ 1 L)) (= H 0) (= K 0) (= A (+ 1 J)) (= C 1) (new9 L) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= B false) (<= (+ A 1) (+ 1 G)) (<= H (- D 1)) (<= I J) (= G (+ 1 K)) (= J 0) (= A (+ 1 I)) (= C 1) (new9 K) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= B false) (>= A (+ (+ 1 G) 1)) (<= H (- D 1)) (<= I J) (= G (+ 1 K)) (= J 0) (= A (+ 1 I)) (= C 1) (new9 K) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= E false) (= F true) (= B true) (= B true) (= B true) (= B true) (= B true) (>= G (+ H 1)) (<= I J) (<= K L) (<= M (- D 1)) (= K 0) (= L (+ 1 I)) (= H 0) (= N 0) (= O 0) (= A (+ 1 N)) (= A (+ 1 O)) (= G (+ 1 I)) (= C 1) (new3 B J) (new3 B I) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (>= G (+ H 1)) (<= I (- D 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= C 1) (new5 B) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (>= G (+ H 1)) (<= I (- D 1)) (= H 0) (= J 0) (= A (+ 1 J)) (= C 1) (new5 B) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (= B false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- D 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= C 1) (new9 H) (new9 G) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- D 1)) (= H 0) (= K 0) (= A (+ 1 K)) (= C 1) (new9 I) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- D 1)) (= H 0) (= K 0) (= A (+ 1 K)) (= C 1) (new9 I) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= B false) (= B false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- D 1)) (= G 0) (= H (+ 1 L)) (= J 0) (= M 0) (= A (+ 1 M)) (= C 1) (new9 L) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Bool) ) (=> (and (= E true) (= F false) (= B true) (>= G D) (<= H I) (<= J K) (= C 1) (= A (+ 1 H)) (= A (+ 1 J)) (diff_new701 L B H) (new107 K B I) (new122 J L C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F false) (= B false) (>= G D) (<= H I) (= A (+ 1 H)) (= C 1) (new119 I B) (new120 H C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E true) (= F false) (= B false) (>= G D) (<= H I) (= A (+ 1 H)) (= C 1) (new134 I) (new122 H B C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= B false) (= B false) (>= G (+ H 1)) (>= I D) (<= J K) (= A (+ 1 J)) (= C 1) (new137 K H) (new124 J G C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (= B false) (>= G D) (<= (+ A 1) (+ 1 H)) (<= I J) (= A (+ 1 I)) (= C 1) (new134 J) (new124 I H C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (= B false) (>= A (+ (+ 1 G) 1)) (>= H D) (<= I J) (= A (+ 1 I)) (= C 1) (new134 J) (new124 I G C D) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Bool) ) (=> (and (= E false) (= F false) (= B true) (>= G D) (>= H (+ I 1)) (<= J K) (= C 1) (= A (+ 1 J)) (= A (+ 1 I)) (diff_new701 L B K) (new122 H L C D) (new107 I B J) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E false) (= F false) (= B false) (>= G (+ H 1)) (>= I D) (= A (+ 1 H)) (= C 1) (new122 G B C D) (new134 H) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) ) (=> (and (= E false) (= F false) (= B false) (>= G (+ H 1)) (>= I D) (= A (+ 1 H)) (= C 1) (new120 G C D) (new119 H B) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= B false) (= B false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K D) (= A (+ 1 J)) (= C 1) (new124 I H C D) (new137 J G) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (= B false) (>= G (+ H 1)) (>= I D) (<= (+ A 1) (+ 1 J)) (= A (+ 1 H)) (= C 1) (new120 G C D) (new137 H J) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (= B false) (>= G (+ H 1)) (>= A (+ (+ 1 I) 1)) (>= J D) (= A (+ 1 H)) (= C 1) (new120 G C D) (new137 H I) ) (new122 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B true) (= A 0) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B true) (= B true) (<= C D) (= A (+ 1 C)) (new251 B D) (new251 B C) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B false) (new6 B) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B false) (new6 B) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= B false) (>= C (+ D 1)) (new31 D) (new31 C) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (<= (+ A 1) (+ 1 C)) (new31 C) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (>= A (+ (+ 1 C) 1)) (new31 C) ) (new121 A B) ) ) ) (assert (forall ( (A Int) (B Int) ) (=> (= A 1) (new120 A A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) ) (=> (and (= D true) (= E true) (<= F (- C 1)) (<= G H) (= H 0) (= A (+ 1 G)) (= B 1) ) (new120 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D false) (= E true) (>= F (+ G 1)) (<= H (- C 1)) (= G 0) (= I 0) (= A (+ 1 I)) (= B 1) ) (new120 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) ) (=> (and (= D true) (= E false) (>= F C) (<= G H) (= A (+ 1 G)) (= B 1) (new134 H) (new120 G B C) ) (new120 A B C) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= E false) (>= F (+ G 1)) (>= H C) (= A (+ 1 G)) (= B 1) (new120 F B C) (new134 G) ) (new120 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B true) (= A 0) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B true) (= B true) (<= C D) (= A (+ 1 C)) (new3 B D) (new3 B C) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B false) (new5 B) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B false) (new5 B) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= B false) (>= C (+ D 1)) (new9 D) (new9 C) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (<= (+ A 1) (+ 1 C)) (new9 C) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (>= A (+ (+ 1 C) 1)) (new9 C) ) (new119 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D true) (= F 0) (= E 0) (= A 1) (= B (+ 1 F)) ) (new114 A B A C D E) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H true) (= E true) (= E true) (<= I J) (<= K (- D 1)) (<= L M) (= M 0) (= A (+ 1 L)) (= L (+ 1 I)) (= N (+ 1 I)) (= F (+ 1 I)) (= C 1) (= B (+ 1 N)) (new251 E J) (new8 E I) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= E false) (<= I (- D 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= L (+ 1 M)) (= F (+ 1 M)) (= C 1) (= B (+ 1 L)) (new6 E) (new9 M) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= E false) (<= I (- D 1)) (<= J K) (= K 0) (= A (+ 1 J)) (= L (+ 1 M)) (= F (+ 1 M)) (= C 1) (= B (+ 1 L)) (new8 E M) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H true) (= E false) (= E false) (>= I (+ J 1)) (<= K (- D 1)) (<= L M) (= M 0) (= A (+ 1 L)) (= N (+ 1 I)) (= F (+ 1 I)) (= C 1) (= B (+ 1 N)) (new31 J) (new9 I) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= E false) (<= (+ I 1) (+ 1 J)) (<= K (- D 1)) (<= I L) (= L 0) (= A (+ 1 I)) (= M (+ 1 J)) (= F (+ 1 J)) (= C 1) (= B (+ 1 M)) (new9 J) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H true) (= E false) (>= I (+ (+ 1 J) 1)) (<= K (- D 1)) (<= I L) (= L 0) (= A (+ 1 I)) (= M (+ 1 J)) (= F (+ 1 J)) (= C 1) (= B (+ 1 M)) (new9 J) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= G false) (= H true) (= E true) (= E true) (>= I (+ J 1)) (<= K L) (<= M (- D 1)) (= J 0) (= N 0) (= A (+ 1 N)) (= I (+ 1 K)) (= O 0) (= F (+ 1 K)) (= C 1) (= B (+ 1 O)) (new251 E L) (new251 E K) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= E false) (>= I (+ J 1)) (<= K (- D 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= M 0) (= F (+ 1 N)) (= C 1) (= B (+ 1 M)) (new6 E) (new31 N) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= E false) (>= I (+ J 1)) (<= K (- D 1)) (= J 0) (= L 0) (= A (+ 1 L)) (= M 0) (= F (+ 1 N)) (= C 1) (= B (+ 1 M)) (new251 E N) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= G false) (= H true) (= E false) (= E false) (>= I (+ J 1)) (>= K (+ L 1)) (<= M (- D 1)) (= L 0) (= N 0) (= A (+ 1 N)) (= O 0) (= F (+ 1 I)) (= C 1) (= B (+ 1 O)) (new31 J) (new31 I) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= E false) (>= I (+ J 1)) (<= (+ I 1) (+ 1 K)) (<= L (- D 1)) (= J 0) (= M 0) (= A (+ 1 M)) (= N 0) (= F (+ 1 K)) (= C 1) (= B (+ 1 N)) (new31 K) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H true) (= E false) (>= I (+ J 1)) (>= I (+ (+ 1 K) 1)) (<= L (- D 1)) (= J 0) (= M 0) (= A (+ 1 M)) (= N 0) (= F (+ 1 K)) (= C 1) (= B (+ 1 N)) (new31 K) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= G true) (= H false) (= E true) (= E true) (>= I D) (<= J K) (<= L M) (= N (+ 1 J)) (= A (+ 1 L)) (= F (+ 1 J)) (= C 1) (= B (+ 1 O)) (new110 M E K) (new114 L O C D E J) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= E false) (>= I D) (<= J K) (= A (+ 1 J)) (= F (+ 1 L)) (= C 1) (= B (+ 1 M)) (new121 K E) (new150 J M C D L) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G true) (= H false) (= E false) (>= I D) (<= J K) (= A (+ 1 J)) (= F (+ 1 L)) (= C 1) (= B (+ 1 M)) (new134 K) (new114 J M C D E L) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H false) (= E false) (= E false) (>= I (+ J 1)) (>= K D) (<= L M) (= A (+ 1 L)) (= F (+ 1 I)) (= C 1) (= B (+ 1 N)) (new147 M J) (new150 L N C D I) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H false) (= E false) (>= I D) (<= (+ J 1) (+ 1 K)) (<= L M) (= A (+ 1 L)) (= F (+ 1 K)) (= C 1) (= B (+ 1 N)) (new134 M) (new150 L N C D K) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G true) (= H false) (= E false) (>= I (+ (+ 1 J) 1)) (>= K D) (<= L M) (= A (+ 1 L)) (= F (+ 1 J)) (= C 1) (= B (+ 1 N)) (new134 M) (new150 L N C D J) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H false) (= E true) (= E true) (>= I (+ J 1)) (>= K D) (<= L M) (= N (+ 1 L)) (= A (+ 1 J)) (= F (+ 1 L)) (= C 1) (= B (+ 1 M)) (new187 I C D E L) (new113 J E M) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= E false) (>= I (+ J 1)) (>= K D) (= A (+ 1 J)) (= F (+ 1 L)) (= C 1) (= B (+ 1 M)) (new146 I C D L) (new113 J E M) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= E false) (>= I (+ J 1)) (>= K D) (= A (+ 1 J)) (= F (+ 1 L)) (= C 1) (= B (+ 1 M)) (new187 I C D E L) (new137 J M) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= G false) (= H false) (= E false) (= E false) (>= I (+ J 1)) (>= K (+ L 1)) (>= M D) (= A (+ 1 L)) (= F (+ 1 I)) (= C 1) (= B (+ 1 J)) (new146 K C D I) (new137 L J) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H false) (= E false) (>= I (+ J 1)) (>= K D) (<= (+ L 1) (+ 1 M)) (= A (+ 1 J)) (= F (+ 1 M)) (= C 1) (= B (+ 1 N)) (new146 I C D M) (new137 J N) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= G false) (= H false) (= E false) (>= I (+ (+ 1 J) 1)) (>= K (+ L 1)) (>= M D) (= A (+ 1 L)) (= F (+ 1 J)) (= C 1) (= B (+ 1 N)) (new146 K C D J) (new137 L N) ) (new114 A B C D E F) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B true) (= C 0) (= A 0) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B true) (= B true) (<= D E) (= A (+ 1 D)) (= C (+ 1 D)) (new251 B E) (new251 B D) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new9 D) (new6 B) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new8 B D) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= B false) (>= D (+ E 1)) (= C (+ 1 D)) (new31 E) (new31 D) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (<= (+ A 1) (+ 1 D)) (= C (+ 1 D)) (new31 D) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (>= A (+ (+ 1 D) 1)) (= C (+ 1 D)) (new31 D) ) (new113 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B true) (= C 0) (= A 0) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B true) (= B true) (<= D E) (= A (+ 1 D)) (= C (+ 1 D)) (new251 B E) (new251 B D) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new31 D) (new6 B) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new251 B D) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= B false) (>= D (+ E 1)) (= C (+ 1 D)) (new31 E) (new31 D) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (<= (+ A 1) (+ 1 D)) (= C (+ 1 D)) (new31 D) ) (new110 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (>= A (+ (+ 1 D) 1)) (= C (+ 1 D)) (new31 D) ) (new110 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) ) (=> (and (= C true) (= A true) (= D 0) (= B 0) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) ) (=> (and (= C true) (= A true) (= D 0) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= D E) (<= D E) (= F (+ 1 D)) (= C (+ 1 D)) (= B 0) (new251 A E) (new251 A D) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= D E) (<= D E) (= F (+ 1 D)) (= C (+ 1 D)) (new251 A E) (new251 A D) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (= B 0) (new31 D) (new6 A) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= D (+ 1 E)) (= B 0) (new251 C E) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (= B 0) (new251 A F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (= B 0) (new31 F) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (= B 0) (new31 F) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (new31 D) (new6 A) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= D (+ 1 E)) (new251 C E) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (new251 A F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (new31 F) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (new31 F) (new6 A) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= D (+ 1 E)) (= B 0) (new6 C) (new251 A E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (= B 0) (new251 A D) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (= B 0) (new31 F) (new251 A E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (= B 0) (new251 A F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (= B 0) (new251 A F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) ) (=> (and (= C false) (= A false) (= D (+ 1 E)) (new6 C) (new251 A E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (= C (+ 1 D)) (new251 A D) ) (diff_new112 A B A C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (new31 F) (new251 A E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (new251 A F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (new251 A F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (= B 0) (new251 C F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (= B 0) (new251 C E) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (= C false) (= A false) (>= E (+ F 1)) (>= E (+ F 1)) (= D (+ 1 E)) (= B 0) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= D (+ 1 E)) (= B 0) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= D (+ 1 F)) (= B 0) (new31 G) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (new251 C F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (= D (+ 1 E)) (new251 C E) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (= C false) (= A false) (>= E (+ F 1)) (>= E (+ F 1)) (= D (+ 1 E)) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= D (+ 1 E)) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= D (+ 1 F)) (new31 G) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (= B 0) (new6 C) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (= B 0) (new251 C F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= D (+ 1 E)) (= B 0) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (= B 0) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (new6 C) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (new251 C F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ F 1)) (<= (+ G 1) (+ 1 E)) (= D (+ 1 E)) (new31 F) (new31 E) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (<= (+ E 1) (+ 1 F)) (= D (+ 1 F)) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (= B 0) (new6 C) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (= B 0) (new251 C F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= D (+ 1 F)) (= B 0) (new31 G) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (= B 0) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (new6 C) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (new251 C F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= C false) (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (>= F (+ G 1)) (= D (+ 1 F)) (new31 G) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) ) (=> (and (= C false) (= A false) (>= E (+ (+ 1 F) 1)) (= D (+ 1 F)) (new31 F) ) (diff_new112 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B true) (= C 0) (= A 0) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B true) (= B true) (<= D E) (= A (+ 1 D)) (= C (+ 1 D)) (new3 B E) (new3 B D) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new9 D) (new5 B) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= C (+ 1 D)) (new3 B D) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B false) (= B false) (>= D (+ E 1)) (= C (+ 1 D)) (new9 E) (new9 D) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (<= (+ A 1) (+ 1 D)) (= C (+ 1 D)) (new9 D) ) (new107 A B C) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (>= A (+ (+ 1 D) 1)) (= C (+ 1 D)) (new9 D) ) (new107 A B C) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) ) (=> (and (= D true) (= A true) (= E 0) (= C 0) (= B 0) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D true) (= A true) (= E 0) (= C (+ 1 F)) (new9 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= E F) (<= E F) (= G (+ 1 E)) (= D (+ 1 E)) (= C 0) (= B 0) (new251 A F) (new251 A E) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A true) (= A true) (= A true) (= A true) (<= E F) (<= E F) (= G (+ 1 E)) (= D (+ 1 E)) (= C (+ 1 H)) (new9 H) (new251 A F) (new251 A E) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A false) (= A false) (= D (+ 1 E)) (= C 0) (= B 0) (new31 E) (new6 A) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (= E (+ 1 F)) (= C 0) (= B 0) (new251 D F) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C 0) (= B 0) (new251 A G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 G) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 G) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= A false) (= D (+ 1 E)) (= C (+ 1 F)) (new9 F) (new31 E) (new6 A) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (= E (+ 1 F)) (= C (+ 1 G)) (new251 D F) (new9 G) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C (+ 1 H)) (new251 A G) (new9 H) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new31 G) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new31 G) (new6 A) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) ) (=> (and (= D false) (= A false) (= E (+ 1 F)) (= C 0) (= B 0) (new6 D) (new251 A F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A false) (= A false) (= D (+ 1 E)) (= C 0) (= B 0) (new251 A E) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C 0) (= B 0) (new31 G) (new251 A F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C 0) (= B 0) (new251 A G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new251 A G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (= E (+ 1 F)) (= C (+ 1 G)) (new6 D) (new9 G) (new251 A F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) ) (=> (and (= A false) (= A false) (= D (+ 1 E)) (= C (+ 1 F)) (new9 F) (new251 A E) ) (diff_new109 A B C A D) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C (+ 1 H)) (new31 G) (new9 H) (new251 A F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new251 A G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new251 A G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C 0) (= B 0) (new251 D G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C 0) (= B 0) (new251 D F) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (= D false) (= A false) (>= F (+ G 1)) (>= F (+ G 1)) (= E (+ 1 F)) (= C 0) (= B 0) (new31 G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (<= (+ H 1) (+ 1 F)) (= E (+ 1 F)) (= C 0) (= B 0) (new31 G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (>= G (+ H 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C (+ 1 H)) (new251 D G) (new9 H) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (= E (+ 1 F)) (= C (+ 1 H)) (new251 D F) (new9 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (= D false) (= A false) (>= F (+ G 1)) (>= F (+ G 1)) (= E (+ 1 F)) (= C (+ 1 H)) (new9 H) (new31 G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ G 1)) (<= (+ H 1) (+ 1 F)) (= E (+ 1 F)) (= C (+ 1 I)) (new9 I) (new31 G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= A false) (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (>= G (+ H 1)) (= E (+ 1 G)) (= C (+ 1 I)) (new9 I) (new31 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C 0) (= B 0) (new6 D) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C 0) (= B 0) (new251 D G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (<= (+ H 1) (+ 1 F)) (= E (+ 1 F)) (= C 0) (= B 0) (new31 G) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C (+ 1 H)) (new6 D) (new9 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C (+ 1 H)) (new251 D G) (new9 H) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ G 1)) (<= (+ H 1) (+ 1 F)) (= E (+ 1 F)) (= C (+ 1 I)) (new31 G) (new9 I) (new31 F) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (<= (+ F 1) (+ 1 G)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new6 D) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new251 D G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (>= G (+ H 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C 0) (= B 0) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C (+ 1 H)) (new6 D) (new9 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C (+ 1 H)) (new251 D G) (new9 H) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D false) (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (>= G (+ H 1)) (= E (+ 1 G)) (= C (+ 1 I)) (new31 H) (new9 I) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) ) (=> (and (= D false) (= A false) (>= F (+ (+ 1 G) 1)) (= E (+ 1 G)) (= C (+ 1 H)) (new9 H) (new31 G) ) (diff_new109 A B C D E) ) ) ) (assert (forall ( (A Int) ) (=> (= A 0) (new31 A) ) ) ) (assert (forall ( (A Int) (B Int) ) (=> (and (= A (+ 1 B)) (new31 B) ) (new31 A) ) ) ) (assert (forall ( (A Int) (B Bool) ) (=> (and (= B true) (= A 0) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) ) (=> (and (= B true) (= B true) (<= C D) (= E (+ 1 C)) (= A (+ 1 C)) (new3 B D) (new3 B C) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (= A (+ 1 C)) (new31 C) (new5 B) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) ) (=> (and (= B false) (= A (+ 1 C)) (new30 C B) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (= B false) (>= C (+ D 1)) (= A (+ 1 C)) (new9 D) (new9 C) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (<= (+ C 1) (+ 1 D)) (= A (+ 1 D)) (new9 D) ) (new30 A B) ) ) ) (assert (forall ( (A Int) (B Bool) (C Int) (D Int) ) (=> (and (= B false) (>= C (+ (+ 1 D) 1)) (= A (+ 1 D)) (new9 D) ) (new30 A B) ) ) ) (assert (forall ( (A Int) ) (=> (= A 0) (new9 A) ) ) ) (assert (forall ( (A Int) (B Int) ) (=> (and (= A (+ 1 B)) (new9 B) ) (new9 A) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A true) (= B 0) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (<= C D) (= E (+ 1 C)) (= B (+ 1 C)) (new251 A D) (new251 A C) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new9 C) (new6 A) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new8 A C) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (>= C (+ D 1)) (= B (+ 1 C)) (new31 D) (new31 C) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (<= (+ C 1) (+ 1 D)) (= B (+ 1 D)) (new31 D) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (>= C (+ (+ 1 D) 1)) (= B (+ 1 D)) (new31 D) ) (new8 A B) ) ) ) (assert (forall ( (A Bool) ) (=> (= A true) (new6 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A true) (= A true) (<= B C) (= D (+ 1 B)) (new251 A C) (new251 A B) ) (new6 A) ) ) ) (assert (forall ( (A Bool) ) (=> (and (= A false) (new6 A) ) (new6 A) ) ) ) (assert (forall ( (A Bool) ) (=> (and (= A false) (new6 A) ) (new6 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (>= B (+ C 1)) (new31 C) (new31 B) ) (new6 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (<= (+ B 1) (+ 1 C)) (new31 C) ) (new6 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (>= B (+ (+ 1 C) 1)) (new31 C) ) (new6 A) ) ) ) (assert (forall ( (A Bool) ) (=> (= A true) (new5 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A true) (= A true) (<= B C) (= D (+ 1 B)) (new3 A C) (new3 A B) ) (new5 A) ) ) ) (assert (forall ( (A Bool) ) (=> (and (= A false) (new5 A) ) (new5 A) ) ) ) (assert (forall ( (A Bool) ) (=> (and (= A false) (new5 A) ) (new5 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= A false) (>= B (+ C 1)) (new9 C) (new9 B) ) (new5 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (<= (+ B 1) (+ 1 C)) (new9 C) ) (new5 A) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (>= B (+ (+ 1 C) 1)) (new9 C) ) (new5 A) ) ) ) (assert (forall ( (A Bool) (B Int) ) (=> (and (= A true) (= B 0) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) ) (=> (and (= A true) (= A true) (<= C D) (= E (+ 1 C)) (= B (+ 1 C)) (new3 A D) (new3 A C) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new9 C) (new5 A) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) ) (=> (and (= A false) (= B (+ 1 C)) (new3 A C) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (= A false) (>= C (+ D 1)) (= B (+ 1 C)) (new9 D) (new9 C) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (<= (+ C 1) (+ 1 D)) (= B (+ 1 D)) (new9 D) ) (new3 A B) ) ) ) (assert (forall ( (A Bool) (B Int) (C Int) (D Int) ) (=> (and (= A false) (>= C (+ (+ 1 D) 1)) (= B (+ 1 D)) (new9 D) ) (new3 A B) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Int) ) (=> (and (= D true) (= D true) (= D true) (= D true) (= C true) (<= E F) (= E 0) (= F 0) (= G 0) (= A (+ 1 G)) (= A 1) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= D true) (= E true) (= C true) (= C true) (= C true) (= C true) (= C true) (= C true) (= C true) (<= F G) (<= H I) (<= F G) (<= J (- B 1)) (<= K L) (= H (+ 1 F)) (= I 0) (= L 0) (= M (+ 1 F)) (= N (+ 1 M)) (= N (+ 1 K)) (= K (+ 1 F)) (= K (+ 1 F)) (= A 1) (new3 C G) (new3 C F) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D true) (= E true) (= C false) (= C false) (= C false) (<= F (- B 1)) (<= G H) (= H 0) (= I (+ 1 G)) (= A 1) (new5 C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= G (- B 1)) (<= H I) (= I 0) (= J (+ 1 H)) (= A 1) (new6 C) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= K 0) (= L (+ 1 J)) (= A 1) (new8 C H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new6 C) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new6 C) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= G (+ 1 L)) (= H 0) (= K 0) (= M (+ 1 J)) (= A 1) (new6 C) (new9 L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= G (+ 1 J)) (= A 1) (new6 C) (new9 L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= G (+ 1 J)) (= A 1) (new6 C) (new9 L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= G (- B 1)) (<= H I) (= I 0) (= J (+ 1 H)) (= A 1) (new6 C) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D true) (= E true) (= C false) (= C false) (= C false) (<= F (- B 1)) (<= G H) (= H 0) (= I (+ 1 G)) (= A 1) (new5 C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= K 0) (= L (+ 1 J)) (= A 1) (new8 C G) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new8 C H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new8 C H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= G (+ 1 L)) (= H 0) (= K 0) (= M (+ 1 J)) (= A 1) (new8 C L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= G (+ 1 J)) (= A 1) (new8 C L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= J K) (= H (+ 1 L)) (= K 0) (= G (+ 1 J)) (= A 1) (new8 C L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= K 0) (= L (+ 1 J)) (= A 1) (new30 H D) (new31 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= K 0) (= L (+ 1 J)) (= A 1) (new31 H) (new30 G D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ H 1)) (<= I (- B 1)) (<= J K) (= K 0) (= L (+ 1 J)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ I 1) (+ 1 G)) (<= J (- B 1)) (<= I K) (= K 0) (= L (+ 1 I)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 G) 1)) (<= J (- B 1)) (<= I K) (= K 0) (= L (+ 1 I)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (<= L M) (= G (+ 1 I)) (= H 0) (= M 0) (= N (+ 1 L)) (= A 1) (new31 J) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F true) (= C false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ I 1) (+ 1 J)) (<= K (- B 1)) (<= L M) (= J (+ 1 G)) (= M 0) (= I (+ 1 L)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F true) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (<= K (- B 1)) (<= L M) (= J (+ 1 G)) (= M 0) (= I (+ 1 L)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new31 H) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new30 H D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ I 1) (+ 1 G)) (<= J (- B 1)) (<= I K) (= K 0) (= L (+ 1 I)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= (+ G 1) (+ 1 H)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ I 1) (+ 1 J)) (<= K (- B 1)) (<= I L) (= G (+ 1 J)) (= H 0) (= L 0) (= M (+ 1 I)) (= A 1) (new9 J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (<= (+ G 1) (+ 1 H)) (<= (+ I 1) (+ 1 J)) (<= K (- B 1)) (<= I L) (= H (+ 1 J)) (= L 0) (= G (+ 1 I)) (= A 1) (new9 J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new31 H) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new30 H D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 G) 1)) (<= J (- B 1)) (<= I K) (= K 0) (= L (+ 1 I)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F true) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= G (+ (+ 1 H) 1)) (<= I (- B 1)) (<= G J) (= J 0) (= K (+ 1 G)) (= A 1) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F true) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ (+ 1 J) 1)) (<= K (- B 1)) (<= I L) (= H (+ 1 J)) (= L 0) (= G (+ 1 I)) (= A 1) (new9 J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= D false) (= E true) (= C true) (= C true) (= C true) (= C true) (= C true) (= C true) (= C true) (>= F (+ G 1)) (<= H I) (<= J K) (<= H I) (<= L (- B 1)) (= J 0) (= K (+ 1 H)) (= G 0) (= M 0) (= N 0) (= O (+ 1 M)) (= O (+ 1 N)) (= F (+ 1 H)) (= F (+ 1 H)) (= A 1) (new3 C I) (new3 C H) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= D false) (= E true) (= C false) (= C false) (= C false) (>= F (+ G 1)) (<= H (- B 1)) (= G 0) (= I 0) (= J (+ 1 I)) (= A 1) (new5 C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (= H 0) (= J 0) (= K (+ 1 J)) (= A 1) (new6 C) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new8 C H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new6 C) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new6 C) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= G 0) (= H (+ 1 L)) (= J 0) (= M 0) (= N (+ 1 M)) (= A 1) (new6 C) (new9 L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= I (- B 1)) (= H 0) (= J 0) (= K (+ 1 J)) (= A 1) (new6 C) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= D false) (= E true) (= C false) (= C false) (= C false) (>= F (+ G 1)) (<= H (- B 1)) (= G 0) (= I 0) (= J (+ 1 I)) (= A 1) (new5 C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new8 C G) (new9 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new8 C I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new8 C I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= G 0) (= H (+ 1 L)) (= J 0) (= M 0) (= N (+ 1 M)) (= A 1) (new8 C L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new30 H D) (new31 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new31 H) (new30 G D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ H 1)) (>= I (+ J 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= (+ I 1) (+ 1 G)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= I (+ (+ 1 G) 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new31 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) ) (=> (and (= E false) (= F true) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K (+ L 1)) (<= M (- B 1)) (= G 0) (= H (+ 1 I)) (= L 0) (= N 0) (= O (+ 1 N)) (= A 1) (new31 J) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new31 I) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new30 I D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (<= (+ I 1) (+ 1 G)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (<= (+ G 1) (+ 1 I)) (<= (+ G 1) (+ 1 I)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new31 I) (new5 D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new30 I D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= I (+ (+ 1 G) 1)) (<= K (- B 1)) (= J 0) (= L 0) (= M (+ 1 L)) (= A 1) (new9 H) (new9 G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= G (+ (+ 1 I) 1)) (>= G (+ (+ 1 I) 1)) (<= J (- B 1)) (= H 0) (= K 0) (= L (+ 1 K)) (= A 1) (new9 I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F true) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= I (+ (+ 1 K) 1)) (<= L (- B 1)) (= G 0) (= H (+ 1 K)) (= J 0) (= M 0) (= N (+ 1 M)) (= A 1) (new9 K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) ) (=> (and (= D true) (= E false) (= C true) (>= F B) (<= G H) (<= I H) (<= J K) (= L (+ 1 G)) (= M (+ 1 I)) (= M (+ 1 J)) (= A 1) (diff_new109 N J I C G) (new107 K C H) (new2 A B N C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) ) (=> (and (= E true) (= F false) (= D false) (= C true) (>= G B) (<= H I) (<= J K) (= L (+ 1 H)) (= M (+ 1 J)) (= A 1) (diff_new112 N J C H) (new110 K C I) (new2 A B N D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= D false) (= C true) (= D false) (= C true) (>= G (+ H 1)) (>= I B) (<= J H) (<= K L) (= M (+ 1 J)) (= N (+ 1 K)) (= A 1) (new113 L C H) (new114 K G A B C J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= C true) (= D false) (= C true) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (<= L M) (= N (+ 1 J)) (= H (+ 1 L)) (= A 1) (new110 M C K) (new114 L I A B C J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= C true) (= D false) (= C true) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (<= L M) (= N (+ 1 J)) (= G (+ 1 L)) (= A 1) (new110 M C K) (new114 L H A B C J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D true) (= E false) (= C false) (= C false) (>= F B) (<= G H) (= I (+ 1 G)) (= A 1) (new119 H C) (new120 G A B) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= H I) (= J (+ 1 H)) (= A 1) (new121 I C) (new122 H D A B) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new113 K C H) (new124 J G A B) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (= H (+ 1 J)) (= A 1) (new121 K C) (new124 J I A B) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (= G (+ 1 J)) (= A 1) (new121 K C) (new124 J H A B) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Bool) ) (=> (and (= E true) (= F false) (= D true) (= C false) (>= G B) (<= H I) (<= J K) (= L (+ 1 H)) (= L (+ 1 J)) (= A 1) (diff_new131 M J H C) (new107 K D I) (new2 A B M D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= H I) (= J (+ 1 H)) (= A 1) (new119 I D) (new133 H A B C) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Bool) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= H I) (= J (+ 1 H)) (= A 1) (diff_new136 K H C) (new134 I) (new2 A B K D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new137 K H) (new138 J G A B C) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (= H (+ 1 J)) (= A 1) (new134 K) (new138 J I A B C) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (= G (+ 1 J)) (= A 1) (new134 K) (new138 J H A B C) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D true) (= C false) (= D true) (= C false) (>= G (+ H 1)) (>= I B) (<= J H) (<= K L) (= M (+ 1 J)) (= M (+ 1 K)) (= A 1) (new107 L D H) (new144 K D J A B G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new145 K H D) (new146 J A B G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new147 K H) (new148 J D A B G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ H 1)) (>= J B) (<= K L) (= M (+ 1 K)) (= A 1) (new137 L H) (new150 K G A B I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L M) (= J (+ 1 L)) (= A 1) (new147 M H) (new150 L K A B G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (<= L M) (= I (+ 1 L)) (= A 1) (new147 M H) (new150 L J A B G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= D true) (= D true) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (<= L M) (= N (+ 1 J)) (= N (+ 1 L)) (= A 1) (new107 M D K) (new144 L D J A B I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (= L (+ 1 J)) (= A 1) (new119 K D) (new146 J A B I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= J K) (= L (+ 1 J)) (= A 1) (new134 K) (new148 J D A B I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L M) (= N (+ 1 L)) (= A 1) (new137 M H) (new150 L G A B K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G B) (<= (+ H 1) (+ 1 I)) (<= (+ J 1) (+ 1 K)) (<= L M) (= J (+ 1 L)) (= A 1) (new134 M) (new150 L K A B I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L M) (= G (+ 1 L)) (= A 1) (new134 M) (new150 L H A B K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= D true) (= D true) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (<= L M) (= N (+ 1 J)) (= N (+ 1 L)) (= A 1) (new107 M D K) (new144 L D J A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new119 K D) (new146 J A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= A 1) (new134 K) (new148 J D A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E true) (= F false) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K B) (<= L M) (= N (+ 1 L)) (= A 1) (new137 M J) (new150 L I A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L M) (= J (+ 1 L)) (= A 1) (new134 M) (new150 L K A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E true) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (<= L M) (= I (+ 1 L)) (= A 1) (new134 M) (new150 L J A B H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) ) (=> (and (= D false) (= E false) (= C true) (>= F (+ G 1)) (>= H B) (<= I J) (<= J K) (= L (+ 1 I)) (= M (+ 1 J)) (= M (+ 1 G)) (= A 1) (diff_new109 N F K C I) (new2 A B N C) (new107 G C J) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) ) (=> (and (= E false) (= F false) (= D false) (= C true) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= M (+ 1 H)) (= A 1) (diff_new112 N G C J) (new2 A B N D) (new110 H C K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F false) (= D false) (= C true) (= D false) (= C true) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (<= L G) (= M (+ 1 L)) (= N (+ 1 J)) (= A 1) (new114 I H A B C L) (new113 J C G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= C true) (= D false) (= C true) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L K) (= M (+ 1 L)) (= J (+ 1 H)) (= A 1) (new187 G A B C L) (new113 H C K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= C true) (= D false) (= C true) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (<= L J) (= M (+ 1 L)) (= I (+ 1 H)) (= A 1) (new187 G A B C L) (new113 H C J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (= J (+ 1 H)) (= A 1) (new122 G D A B) (new121 H C) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) ) (=> (and (= D false) (= E false) (= C false) (= C false) (>= F (+ G 1)) (>= H B) (= I (+ 1 G)) (= A 1) (new120 F A B) (new119 G C) ) (new2 A B C C) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new124 I H A B) (new113 J C G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (= J (+ 1 H)) (= A 1) (new120 G A B) (new113 H C K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (= I (+ 1 H)) (= A 1) (new120 G A B) (new113 H C J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Bool) ) (=> (and (= E false) (= F false) (= D true) (= C false) (>= G (+ H 1)) (>= I B) (<= J K) (= L (+ 1 J)) (= L (+ 1 H)) (= A 1) (diff_new131 M G K C) (new2 A B M D) (new107 H D J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Bool) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (= J (+ 1 H)) (= A 1) (diff_new136 K G C) (new2 A B K D) (new134 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (= J (+ 1 H)) (= A 1) (new133 G A B C) (new119 H D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new138 I H A B C) (new137 J G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (= J (+ 1 H)) (= A 1) (new133 G A B C) (new137 H K) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (= I (+ 1 H)) (= A 1) (new133 G A B C) (new137 H J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D true) (= C false) (= D true) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (<= H L) (= M (+ 1 H)) (= M (+ 1 J)) (= A 1) (new144 I D L A B G) (new107 J D H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new148 I D A B G) (new147 J H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new146 I A B G) (new145 J H D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ G 1)) (>= J (+ K 1)) (>= L B) (= M (+ 1 K)) (= A 1) (new150 J H A B I) (new137 K G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (<= (+ L 1) (+ 1 H)) (= L (+ 1 J)) (= A 1) (new146 I A B G) (new137 J H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= C false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K (+ (+ 1 H) 1)) (>= L B) (= K (+ 1 J)) (= A 1) (new146 I A B G) (new137 J H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F false) (= D true) (= D true) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= L M) (= N (+ 1 L)) (= N (+ 1 H)) (= A 1) (new144 G D M A B K) (new107 H D L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (= L (+ 1 H)) (= A 1) (new148 G D A B K) (new134 H) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (= L (+ 1 H)) (= A 1) (new146 G A B K) (new119 H D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F false) (= D false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ J 1)) (>= K B) (<= (+ L 1) (+ 1 M)) (= N (+ 1 J)) (= A 1) (new150 I H A B M) (new137 J G) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I B) (<= (+ J 1) (+ 1 K)) (<= (+ L 1) (+ 1 M)) (= L (+ 1 H)) (= A 1) (new146 G A B K) (new137 H M) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ H 1)) (>= I (+ (+ 1 J) 1)) (>= K B) (<= (+ L 1) (+ 1 M)) (= I (+ 1 H)) (= A 1) (new146 G A B M) (new137 H J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F false) (= D true) (= D true) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K B) (<= L M) (= N (+ 1 L)) (= N (+ 1 J)) (= A 1) (new144 I D M A B H) (new107 J D L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new148 I D A B H) (new134 J) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K B) (= L (+ 1 J)) (= A 1) (new146 I A B H) (new119 J D) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) ) (=> (and (= E false) (= F false) (= D false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K (+ L 1)) (>= M B) (= N (+ 1 L)) (= A 1) (new150 K J A B H) (new137 L I) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K B) (<= (+ L 1) (+ 1 M)) (= L (+ 1 J)) (= A 1) (new146 I A B H) (new137 J M) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) ) (=> (and (= E false) (= F false) (= D false) (= C false) (>= G (+ (+ 1 H) 1)) (>= I (+ J 1)) (>= K (+ (+ 1 L) 1)) (>= M B) (= K (+ 1 J)) (= A 1) (new146 I A B H) (new137 J L) ) (new2 A B C D) ) ) ) (assert (forall ( (A Int) (B Bool) (C Bool) (D Int) ) (=> (and (= D 1) (new2 D A C B) ) (new1 A B C) ) ) ) (assert (forall ( (A Bool) (B Bool) (C Int) ) (=> (and (= A false) (= B true) (new1 C A B) ) ff ) ) ) (assert (not ff)) (check-sat)