products/Sources/formale Sprachen/Isabelle/HOL/SMT_Examples/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Quotient_Rat.thy   Sprache: Isabelle

rahmenlose Ansicht.certs DruckansichtIsabelle {Isabelle[160] Coq[188] BAT[326]}Entwicklung

9d6b81d96fb21c8c08e3f1fd649ce37bdafb5f92 3015 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!19 () B_Vertex$)
(declare-fun ?v1!18 () B_Vertex$)
(declare-fun ?v0!20 () B_Vertex$)
(declare-fun ?v0!17 () B_Vertex$)
(declare-fun ?v1!16 () B_Vertex$)
(declare-fun ?v0!15 () B_Vertex$)
(declare-fun ?v0!14 () B_Vertex$)
(declare-fun ?v0!13 () B_Vertex$)
(declare-fun ?v0!12 () B_Vertex$)
(declare-fun ?v0!11 () B_Vertex$)
(declare-fun ?v1!10 () B_Vertex$)
(declare-fun ?v1!9 (B_Vertex$) B_Vertex$)
(declare-fun ?v0!8 () B_Vertex$)
(declare-fun ?v1!7 (B_Vertex$) B_Vertex$)
(declare-fun ?v1!6 (B_Vertex$) B_Vertex$)
(declare-fun ?v0!5 () B_Vertex$)
(declare-fun ?v0!4 () B_Vertex$)
(declare-fun ?v1!3 () B_Vertex$)
(declare-fun ?v0!2 () B_Vertex$)
(declare-fun ?v1!1 () B_Vertex$)
(declare-fun ?v0!0 () B_Vertex$)
(proof
(let ((?x1893 (v_b_SP_G_2$ ?v0!19)))
(let ((?x1894 (* (- 1) ?x1893)))
(let ((?x1892 (v_b_SP_G_2$ ?v1!18)))
(let ((?x1884 (pair$ ?v1!18 ?v0!19)))
(let ((?x1885 (b_G$ ?x1884)))
(let (($x1896 (>= (+ ?x1885 ?x1892 ?x1894) 0)))
(let (($x1888 (<= (+ b_Infinity$ (* (- 1) ?x1885)) 0)))
(let (($x1883 (fun_app$ v_b_Visited_G_2$ ?v1!18)))
(let (($x2791 (not $x1883)))
(let (($x2806 (or $x2791 $x1888 $x1896)))
(let (($x2811 (not $x2806)))
(let (($x3729 (forall ((?v1 B_Vertex$) )(! (let ((?x1911 (v_b_SP_G_2$ ?v0!20)))
(let ((?x1912 (* (- 1) ?x1911)))
(let ((?x273 (v_b_SP_G_2$ ?v1)))
(let (($x2242 (= (+ ?x273 ?x1912 (b_G$ (pair$ ?v1 ?v0!20))) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x300 (not $x291)))
(or (>= (+ ?x273 ?x1912) 0) $x300 (not $x2242)))))))) :pattern ( (v_b_SP_G_2$ ?v1) ) :pattern ( (fun_app$ v_b_Visited_G_2$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!20) ) :qid k!42))
))
(let (($x3734 (not $x3729)))
(let (($x1914 (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_2$ ?v0!20))) 0)))
(let (($x1909 (= ?v0!20 b_Source$)))
(let (($x3720 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1282 (>= (+ ?x155 ?x273 (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x300 (not $x291)))
(or $x300 $x922 $x1282))))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!42))
))
(let (($x3725 (not $x3720)))
(let (($x3737 (or $x3725 $x1909 $x1914 $x3734)))
(let ((?x4393 (fun_app$c v_b_SP_G_1$ ?v0!20)))
(let ((?x4418 (* (- 1) ?x4393)))
(let ((?x1911 (v_b_SP_G_2$ ?v0!20)))
(let ((?x4419 (+ ?x1911 ?x4418)))
(let (($x5977 (>= ?x4419 0)))
(let (($x4400 (= ?x1911 ?x4393)))
(let ((?x4434 (pair$ v_b_v_G_1$ ?v0!20)))
(let ((?x4435 (b_G$ ?x4434)))
(let ((?x4436 (* (- 1) ?x4435)))
(let ((?x3104 (v_b_SP_G_2$ v_b_v_G_1$)))
(let ((?x3105 (* (- 1) ?x3104)))
(let ((?x4546 (+ ?x1911 ?x3105 ?x4436)))
(let (($x4569 (<= ?x4546 0)))
(let (($x3740 (not $x3737)))
(let ((@x4391 (hypothesis $x3740)))
(let ((@x3222 (def-axiom (or $x3737 $x3720))))
(let (($x4161 (>= ?x3104 0)))
(let (($x3703 (forall ((?v0 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v0)))
(>= ?x273 0)) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!42))
))
(let (($x3743 (or $x2811 $x3740)))
(let (($x3746 (not $x3743)))
(let (($x3712 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x1262 (>= (+ (v_b_SP_G_2$ ?v1) (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x2768 (not (fun_app$ v_b_Visited_G_2$ ?v0))))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(or $x291 $x2768 $x1262)))) :pattern ( (v_b_SP_G_2$ ?v1) (v_b_SP_G_2$ ?v0) ) :qid k!42))
))
(let (($x3717 (not $x3712)))
(let (($x3749 (or $x3717 $x3746)))
(let (($x3752 (not $x3749)))
(let (($x1869 (>= (+ (v_b_SP_G_2$ ?v1!16) (* (- 1) (v_b_SP_G_2$ ?v0!17))) 0)))
(let (($x1862 (fun_app$ v_b_Visited_G_2$ ?v0!17)))
(let (($x2745 (not $x1862)))
(let (($x1860 (fun_app$ v_b_Visited_G_2$ ?v1!16)))
(let (($x2760 (or $x1860 $x2745 $x1869)))
(let (($x2765 (not $x2760)))
(let (($x3755 (or $x2765 $x3752)))
(let (($x3758 (not $x3755)))
(let (($x3708 (not $x3703)))
(let (($x3761 (or $x3708 $x3758)))
(let (($x3764 (not $x3761)))
(let ((?x1846 (v_b_SP_G_2$ ?v0!15)))
(let (($x1847 (>= ?x1846 0)))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x3904 (>= ?x257 0)))
(let (($x3556 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(>= ?x174 0)) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :qid k!42))
))
(let (($x1848 (not $x1847)))
(let (($x3767 (or $x1848 $x3764)))
(let (($x3770 (not $x3767)))
(let ((?x296 (v_b_SP_G_2$ b_Source$)))
(let (($x297 (= ?x296 0)))
(let (($x773 (not $x297)))
(let (($x3773 (or $x773 $x3770)))
(let (($x3776 (not $x3773)))
(let (($x3779 (or $x773 $x3776)))
(let (($x3782 (not $x3779)))
(let (($x3695 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x300 (not $x291)))
(or $x300 $x278)))))) :pattern ( (fun_app$ v_b_Visited_G_2$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :qid k!42))
))
(let (($x3700 (not $x3695)))
(let (($x3785 (or $x3700 $x3782)))
(let (($x3788 (not $x3785)))
(let ((?x1827 (fun_app$c v_b_SP_G_1$ ?v0!14)))
(let ((?x1826 (v_b_SP_G_2$ ?v0!14)))
(let (($x1828 (= ?x1826 ?x1827)))
(let (($x1829 (or (not (fun_app$ v_b_Visited_G_2$ ?v0!14)) $x1828)))
(let (($x1830 (not $x1829)))
(let (($x3791 (or $x1830 $x3788)))
(let (($x3794 (not $x3791)))
(let (($x3686 (forall ((?v0 B_Vertex$) )(! (>= (+ (fun_app$c v_b_SP_G_1$ ?v0) (* (- 1) (v_b_SP_G_2$ ?v0))) 0) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!42))
))
(let (($x3691 (not $x3686)))
(let (($x3797 (or $x3691 $x3794)))
(let (($x3800 (not $x3797)))
(let ((?x1809 (v_b_SP_G_2$ ?v0!13)))
(let ((?x1810 (* (- 1) ?x1809)))
(let ((?x1808 (fun_app$c v_b_SP_G_1$ ?v0!13)))
(let ((?x1811 (+ ?x1808 ?x1810)))
(let (($x1812 (>= ?x1811 0)))
(let (($x1813 (not $x1812)))
(let (($x3803 (or $x1813 $x3800)))
(let (($x3806 (not $x3803)))
(let (($x3678 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1173 (* (- 1) ?x257)))
(let (($x1175 (<= (+ ?x174 ?x1173 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1169 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x2717 (or $x1169 $x1175)))
(let (($x2718 (not $x2717)))
(or $x2718 $x278)))))))))) :pattern ( (pair$ v_b_v_G_1$ ?v0) ) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!42))
))
(let (($x3683 (not $x3678)))
(let (($x3670 (forall ((?v0 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v0)))
(let ((?x1186 (* (- 1) ?x273)))
(let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x1185 (= (+ ?x257 ?x268 ?x1186) 0)))
(let (($x1175 (<= (+ (fun_app$c v_b_SP_G_1$ ?v0) (* (- 1) ?x257) (* (- 1) ?x268)) 0)))
(let (($x1169 (<= (+ b_Infinity$ (* (- 1) ?x268)) 0)))
(or $x1169 $x1175 $x1185)))))))) :pattern ( (pair$ v_b_v_G_1$ ?v0) ) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!42))
))
(let (($x3675 (not $x3670)))
(let ((?x263 (fun_upd$ v_b_Visited_G_1$)))
(let ((?x264 (fun_app$b ?x263 v_b_v_G_1$)))
(let ((?x265 (fun_app$a ?x264 true)))
(let (($x266 (= v_b_Visited_G_2$ ?x265)))
(let (($x2935 (not $x266)))
(let (($x3660 (forall ((?v0 B_Vertex$) )(! (let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1173 (* (- 1) ?x257)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x178 (>= (+ ?x174 ?x1173) 0)))))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v0) ) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :qid k!42))
))
(let (($x3665 (not $x3660)))
(let ((?x1173 (* (- 1) ?x257)))
(let ((?x1212 (+ b_Infinity$ ?x1173)))
(let (($x1213 (<= ?x1212 0)))
(let (($x255 (fun_app$ v_b_Visited_G_1$ v_b_v_G_1$)))
(let ((?x1775 (fun_app$c v_b_SP_G_1$ ?v0!12)))
(let ((?x1776 (* (- 1) ?x1775)))
(let ((?x1777 (+ b_Infinity$ ?x1776)))
(let (($x1778 (<= ?x1777 0)))
(let (($x1773 (fun_app$ v_b_Visited_G_1$ ?v0!12)))
(let (($x3809 (or $x1773 $x1778 $x255 $x1213 $x3665 $x2935 $x3675 $x3683 $x3806)))
(let (($x3812 (not $x3809)))
(let ((?x245 (fun_app$c v_b_SP_G_3$ b_Source$)))
(let (($x246 (= ?x245 0)))
(let (($x3622 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1140 (>= (+ ?x155 ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0))) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x1099 (<= (+ b_Infinity$ (* (- 1) ?x230)) 0)))
(or $x1099 $x922 $x1140)))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!42))
))
(let (($x3627 (not $x3622)))
(let (($x3630 (or $x3627 $x246)))
(let (($x3633 (not $x3630)))
(let ((?x1734 (fun_app$c v_b_SP_G_3$ ?v0!11)))
(let ((?x1735 (* (- 1) ?x1734)))
(let ((?x1726 (pair$ ?v1!10 ?v0!11)))
(let ((?x1727 (b_G$ ?x1726)))
(let ((?x1721 (fun_app$c v_b_SP_G_3$ ?v1!10)))
(let ((?x2206 (+ ?x1721 ?x1727 ?x1735)))
(let (($x2209 (>= ?x2206 0)))
(let (($x1730 (<= (+ b_Infinity$ (* (- 1) ?x1727)) 0)))
(let (($x1724 (<= (+ b_Infinity$ (* (- 1) ?x1721)) 0)))
(let (($x2645 (or $x1724 $x1730 $x2209)))
(let (($x2650 (not $x2645)))
(let (($x3636 (or $x2650 $x3633)))
(let (($x3639 (not $x3636)))
(let (($x3614 (forall ((?v0 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v0)))
(let ((?x2191 (+ ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ (?v1!9 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!9 ?v0) ?v0))))))
(let (($x2192 (= ?x2191 0)))
(let (($x2176 (<= (+ ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ (?v1!9 ?v0)))) 0)))
(let (($x2617 (not (or $x2176 (not $x2192)))))
(let (($x1099 (<= (+ b_Infinity$ (* (- 1) ?x230)) 0)))
(let (($x127 (= ?v0 b_Source$)))
(or $x127 $x1099 $x2617)))))))) :pattern ( (fun_app$c v_b_SP_G_3$ ?v0) ) :qid k!42))
))
(let (($x3619 (not $x3614)))
(let (($x3642 (or $x3619 $x3639)))
(let (($x3645 (not $x3642)))
(let (($x3600 (forall ((?v1 B_Vertex$) )(! (let ((?x1661 (fun_app$c v_b_SP_G_3$ ?v0!8)))
(let ((?x1662 (* (- 1) ?x1661)))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let (($x2148 (= (+ ?x230 ?x1662 (b_G$ (pair$ ?v1 ?v0!8))) 0)))
(or (>= (+ ?x230 ?x1662) 0) (not $x2148)))))) :pattern ( (fun_app$c v_b_SP_G_3$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!8) ) :qid k!42))
))
(let (($x3605 (not $x3600)))
(let (($x1664 (<= (+ b_Infinity$ (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0!8))) 0)))
(let (($x1659 (= ?v0!8 b_Source$)))
(let (($x3608 (or $x1659 $x1664 $x3605)))
(let (($x3611 (not $x3608)))
(let (($x3648 (or $x3611 $x3645)))
(let (($x3651 (not $x3648)))
(let (($x220 (= v_b_oldSP_G_1$ v_b_oldSP_G_0$)))
(let (($x2709 (not $x220)))
(let (($x217 (= v_b_SP_G_3$ v_b_SP_G_1$)))
(let (($x2708 (not $x217)))
(let (($x215 (= v_b_v_G_2$ v_b_v_G_0$)))
(let (($x2707 (not $x215)))
(let (($x212 (= v_b_Visited_G_3$ v_b_Visited_G_1$)))
(let (($x2706 (not $x212)))
(let (($x3590 (forall ((?v0 B_Vertex$) )(! (let (($x1002 (<= (+ b_Infinity$ (* (- 1) (fun_app$c v_b_SP_G_1$ ?v0))) 0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x178 $x1002))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v0) ) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :qid k!42))
))
(let (($x3595 (not $x3590)))
(let (($x3654 (or $x3595 $x2706 $x2707 $x2708 $x2709 $x3651)))
(let (($x3657 (not $x3654)))
(let (($x3815 (or $x3657 $x3812)))
(let (($x3818 (not $x3815)))
(let (($x3581 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x2128 (+ ?x174 (* (- 1) (fun_app$c v_b_SP_G_1$ (?v1!7 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!7 ?v0) ?v0))))))
(let (($x2129 (= ?x2128 0)))
(let (($x2113 (<= (+ ?x174 (* (- 1) (fun_app$c v_b_SP_G_1$ (?v1!7 ?v0)))) 0)))
(let (($x2551 (not (or $x2113 (not (fun_app$ v_b_Visited_G_1$ (?v1!7 ?v0))) (not $x2129)))))
(let (($x1002 (<= (+ b_Infinity$ (* (- 1) ?x174)) 0)))
(let (($x127 (= ?v0 b_Source$)))
(or $x127 $x1002 $x2551)))))))) :pattern ( (fun_app$c v_b_SP_G_1$ ?v0) ) :qid k!42))
))
(let (($x3586 (not $x3581)))
(let (($x3573 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x990 (>= (+ ?x155 ?x174 ?x991) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x179 (not $x178)))
(or $x179 $x922 $x990))))))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!42))
))
(let (($x3578 (not $x3573)))
(let (($x3565 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let (($x1015 (>= (+ ?x174 ?x991) 0)))
(let (($x180 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x2492 (not $x180)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(or $x178 $x2492 $x1015)))))))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v1) (fun_app$ v_b_Visited_G_1$ ?v0) ) :qid k!42))
))
(let (($x3570 (not $x3565)))
(let (($x3561 (not $x3556)))
(let ((?x172 (fun_app$c v_b_SP_G_1$ b_Source$)))
(let (($x173 (= ?x172 0)))
(let (($x2952 (not $x173)))
(let (($x3547 (forall ((?v0 B_Vertex$) )(! (let ((?x128 (v_b_SP_G_0$ ?v0)))
(let ((?x2090 (+ ?x128 (* (- 1) (v_b_SP_G_0$ (?v1!6 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!6 ?v0) ?v0))))))
(let (($x2091 (= ?x2090 0)))
(let (($x2075 (<= (+ ?x128 (* (- 1) (v_b_SP_G_0$ (?v1!6 ?v0)))) 0)))
(let (($x2478 (not (or $x2075 (not (v_b_Visited_G_0$ (?v1!6 ?v0))) (not $x2091)))))
(let (($x947 (<= (+ b_Infinity$ (* (- 1) ?x128)) 0)))
(let (($x127 (= ?v0 b_Source$)))
(or $x127 $x947 $x2478)))))))) :pattern ( (v_b_SP_G_0$ ?v0) ) :qid k!42))
))
(let (($x3552 (not $x3547)))
(let (($x3821 (or $x3552 $x2952 $x3561 $x3570 $x3578 $x3586 $x3818)))
(let (($x3824 (not $x3821)))
(let (($x3533 (forall ((?v1 B_Vertex$) )(! (let ((?x1540 (v_b_SP_G_0$ ?v0!5)))
(let ((?x1541 (* (- 1) ?x1540)))
(let ((?x128 (v_b_SP_G_0$ ?v1)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x137 (not $x136)))
(or (>= (+ ?x128 ?x1541) 0) $x137 (not (= (+ ?x128 ?x1541 (b_G$ (pair$ ?v1 ?v0!5))) 0)))))))) :pattern ( (v_b_SP_G_0$ ?v1) ) :pattern ( (v_b_Visited_G_0$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!5) ) :qid k!42))
))
(let (($x3538 (not $x3533)))
(let ((?x1540 (v_b_SP_G_0$ ?v0!5)))
(let ((?x1541 (* (- 1) ?x1540)))
(let ((?x1542 (+ b_Infinity$ ?x1541)))
(let (($x1543 (<= ?x1542 0)))
(let (($x1538 (= ?v0!5 b_Source$)))
(let (($x3541 (or $x1538 $x1543 $x3538)))
(let (($x1539 (not $x1538)))
(let ((@x6246 (unit-resolution (def-axiom (or $x3541 $x1539)) (hypothesis (not $x3541)) $x1539)))
(let (($x5625 (= b_Infinity$ ?x1540)))
(let (($x6457 (not $x5625)))
(let (($x1544 (not $x1543)))
(let ((@x6514 (unit-resolution (def-axiom (or $x3541 $x1544)) (hypothesis (not $x3541)) $x1544)))
(let ((@x5778 (symm (commutativity (= $x5625 (= ?x1540 b_Infinity$))) (= (= ?x1540 b_Infinity$) $x5625))))
(let (($x5616 (= ?x1540 b_Infinity$)))
(let (($x3493 (forall ((?v0 B_Vertex$) )(! (let (($x127 (= ?v0 b_Source$)))
(or $x127 (= (v_b_SP_G_0$ ?v0) b_Infinity$))) :pattern ( (v_b_SP_G_0$ ?v0) ) :qid k!42))
))
(let (($x360 (forall ((?v0 B_Vertex$) )(! (let (($x127 (= ?v0 b_Source$)))
(or $x127 (= (v_b_SP_G_0$ ?v0) b_Infinity$))) :qid k!42))
))
(let (($x127 (= ?0 b_Source$)))
(let (($x357 (or $x127 (= (v_b_SP_G_0$ ?0) b_Infinity$))))
(let (($x138 (forall ((?v0 B_Vertex$) )(! (let (($x136 (v_b_Visited_G_0$ ?v0)))
(not $x136)) :qid k!42))
))
(let (($x354 (forall ((?v0 B_Vertex$) )(! (let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(or $x132 (= (v_b_SP_G_0$ ?v0) 0)))) :qid k!42))
))
(let (($x890 (and $x354 $x360 $x138)))
(let (($x1329 (forall ((?v0 B_Vertex$) )(! (let (($x1323 (exists ((?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1306 (= (+ ?x155 ?x273 (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1262 (>= (+ ?x273 (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x1309 (not $x1262)))
(and $x1309 $x291 $x1306))))))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x1300 (and $x132 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))))
(or (not $x1300) $x1323))))) :qid k!42))
))
(let (($x1289 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1282 (>= (+ ?x155 ?x273 (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x923 (not $x922)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1276 (and $x291 $x923)))
(let (($x1279 (not $x1276)))
(or $x1279 $x1282))))))))) :qid k!42))
))
(let (($x1292 (not $x1289)))
(let (($x1332 (or $x1292 $x1329)))
(let (($x1335 (and $x1289 $x1332)))
(let (($x1270 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x1262 (>= (+ (v_b_SP_G_2$ ?v1) (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x300 (not $x291)))
(let (($x302 (and $x300 (fun_app$ v_b_Visited_G_2$ ?v0))))
(let (($x664 (not $x302)))
(or $x664 $x1262)))))) :qid k!42))
))
(let (($x1273 (not $x1270)))
(let (($x1338 (or $x1273 $x1335)))
(let (($x1341 (and $x1270 $x1338)))
(let (($x1256 (forall ((?v0 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v0)))
(>= ?x273 0)) :qid k!42))
))
(let (($x1259 (not $x1256)))
(let (($x1344 (or $x1259 $x1341)))
(let (($x1347 (and $x1256 $x1344)))
(let (($x1350 (or $x773 $x1347)))
(let (($x1353 (and $x297 $x1350)))
(let (($x652 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x300 (not $x291)))
(or $x300 $x278)))))) :qid k!42))
))
(let (($x785 (not $x652)))
(let (($x1356 (or $x785 $x1353)))
(let (($x1359 (and $x652 $x1356)))
(let (($x1247 (forall ((?v0 B_Vertex$) )(! (>= (+ (fun_app$c v_b_SP_G_1$ ?v0) (* (- 1) (v_b_SP_G_2$ ?v0))) 0) :qid k!42))
))
(let (($x1250 (not $x1247)))
(let (($x1362 (or $x1250 $x1359)))
(let (($x1365 (and $x1247 $x1362)))
(let (($x1199 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1173 (* (- 1) ?x257)))
(let (($x1175 (<= (+ ?x174 ?x1173 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1169 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1179 (and (not $x1169) (not $x1175))))
(or $x1179 $x278))))))))) :qid k!42))
))
(let (($x1193 (forall ((?v0 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v0)))
(let ((?x1186 (* (- 1) ?x273)))
(let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x1185 (= (+ ?x257 ?x268 ?x1186) 0)))
(let (($x1175 (<= (+ (fun_app$c v_b_SP_G_1$ ?v0) (* (- 1) ?x257) (* (- 1) ?x268)) 0)))
(let (($x1179 (and (not (<= (+ b_Infinity$ (* (- 1) ?x268)) 0)) (not $x1175))))
(let (($x1182 (not $x1179)))
(or $x1182 $x1185))))))))) :qid k!42))
))
(let (($x1209 (forall ((?v0 B_Vertex$) )(! (let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1173 (* (- 1) ?x257)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x178 (>= (+ ?x174 ?x1173) 0)))))) :qid k!42))
))
(let (($x1214 (not $x1213)))
(let (($x256 (not $x255)))
(let (($x1080 (exists ((?v0 B_Vertex$) )(! (let (($x1002 (<= (+ b_Infinity$ (* (- 1) (fun_app$c v_b_SP_G_1$ ?v0))) 0)))
(let (($x1003 (not $x1002)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x179 (not $x178)))
(and $x179 $x1003))))) :qid k!42))
))
(let (($x1235 (and $x1080 $x256 $x1214 $x1209 $x266 $x1193 $x1199)))
(let (($x1240 (not $x1235)))
(let (($x1368 (or $x1240 $x1365)))
(let (($x1146 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1140 (>= (+ ?x155 ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0))) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x923 (not $x922)))
(let (($x1099 (<= (+ b_Infinity$ (* (- 1) ?x230)) 0)))
(let (($x1100 (not $x1099)))
(let (($x1134 (and $x1100 $x923)))
(let (($x1137 (not $x1134)))
(or $x1137 $x1140)))))))))) :qid k!42))
))
(let (($x1149 (not $x1146)))
(let (($x1152 (or $x1149 $x246)))
(let (($x1155 (and $x1146 $x1152)))
(let (($x1128 (forall ((?v0 B_Vertex$) )(! (let (($x1122 (exists ((?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(and (not (>= (+ ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0))) 0)) (= (+ ?x155 ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0))) 0)))) :qid k!42))
))
(let (($x1099 (<= (+ b_Infinity$ (* (- 1) (fun_app$c v_b_SP_G_3$ ?v0))) 0)))
(let (($x1100 (not $x1099)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x1103 (and $x132 $x1100)))
(let (($x1106 (not $x1103)))
(or $x1106 $x1122)))))))) :qid k!42))
))
(let (($x1131 (not $x1128)))
(let (($x1158 (or $x1131 $x1155)))
(let (($x1161 (and $x1128 $x1158)))
(let (($x1083 (not $x1080)))
(let (($x1089 (and $x1083 $x212 $x215 $x217 $x220)))
(let (($x1094 (not $x1089)))
(let (($x1164 (or $x1094 $x1161)))
(let (($x1371 (and $x1164 $x1368)))
(let (($x1037 (forall ((?v0 B_Vertex$) )(! (let (($x1031 (exists ((?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1012 (= (+ ?x155 ?x174 ?x991) 0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x1015 (>= (+ ?x174 ?x991) 0)))
(let (($x1017 (not $x1015)))
(and $x1017 $x178 $x1012))))))))) :qid k!42))
))
(let (($x1002 (<= (+ b_Infinity$ (* (- 1) (fun_app$c v_b_SP_G_1$ ?v0))) 0)))
(let (($x1003 (not $x1002)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x1006 (and $x132 $x1003)))
(let (($x1009 (not $x1006)))
(or $x1009 $x1031)))))))) :qid k!42))
))
(let (($x997 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x990 (>= (+ ?x155 ?x174 ?x991) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x923 (not $x922)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x983 (and $x178 $x923)))
(let (($x986 (not $x983)))
(or $x986 $x990))))))))))) :qid k!42))
))
(let (($x1045 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let (($x1015 (>= (+ ?x174 ?x991) 0)))
(let (($x180 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x179 (not $x178)))
(let (($x181 (and $x179 $x180)))
(let (($x403 (not $x181)))
(or $x403 $x1015)))))))))) :qid k!42))
))
(let (($x1051 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(>= ?x174 0)) :qid k!42))
))
(let (($x980 (forall ((?v0 B_Vertex$) )(! (let (($x974 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x128 (v_b_SP_G_0$ ?v1)))
(let (($x957 (= (+ ?x128 (* (- 1) (v_b_SP_G_0$ ?v0)) ?x155) 0)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x907 (>= (+ ?x128 (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))
(let (($x960 (not $x907)))
(and $x960 $x136 $x957))))))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x951 (and $x132 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))))
(let (($x954 (not $x951)))
(or $x954 $x974)))))) :qid k!42))
))
(let (($x1069 (and $x980 $x173 $x1051 $x1045 $x997 $x1037)))
(let (($x1074 (not $x1069)))
(let (($x1374 (or $x1074 $x1371)))
(let (($x1377 (and $x980 $x1374)))
(let (($x939 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x128 (v_b_SP_G_0$ ?v1)))
(let (($x933 (>= (+ ?x128 (* (- 1) (v_b_SP_G_0$ ?v0)) ?x155) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x923 (not $x922)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x926 (and $x136 $x923)))
(let (($x929 (not $x926)))
(or $x929 $x933))))))))) :qid k!42))
))
(let (($x942 (not $x939)))
(let (($x1380 (or $x942 $x1377)))
(let (($x1383 (and $x939 $x1380)))
(let (($x914 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x907 (>= (+ (v_b_SP_G_0$ ?v1) (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))
(let (($x148 (v_b_Visited_G_0$ ?v0)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x137 (not $x136)))
(let (($x149 (and $x137 $x148)))
(let (($x382 (not $x149)))
(or $x382 $x907))))))) :qid k!42))
))
(let (($x917 (not $x914)))
(let (($x1386 (or $x917 $x1383)))
(let (($x1389 (and $x914 $x1386)))
(let (($x899 (forall ((?v0 B_Vertex$) )(! (let ((?x128 (v_b_SP_G_0$ ?v0)))
(>= ?x128 0)) :qid k!42))
))
(let (($x902 (not $x899)))
(let (($x1392 (or $x902 $x1389)))
(let (($x1395 (and $x899 $x1392)))
(let ((?x144 (v_b_SP_G_0$ b_Source$)))
(let (($x145 (= ?x144 0)))
(let (($x869 (not $x145)))
(let (($x1398 (or $x869 $x1395)))
(let (($x1401 (and $x145 $x1398)))
(let (($x1407 (not (or (not $x890) $x1401))))
(let (($x320 (forall ((?v0 B_Vertex$) )(! (let (($x318 (exists ((?v1 B_Vertex$) )(! (let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x316 (and $x291 (= (v_b_SP_G_2$ ?v0) (+ (v_b_SP_G_2$ ?v1) (b_G$ (pair$ ?v1 ?v0)))))))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v1)))
(let (($x314 (< ?x273 ?x303)))
(and $x314 $x316)))))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x313 (and $x132 (< (v_b_SP_G_2$ ?v0) b_Infinity$))))
(=> $x313 $x318))))) :qid k!42))
))
(let (($x321 (and $x320 false)))
(let (($x322 (=> $x321 true)))
(let (($x323 (and $x320 $x322)))
(let (($x311 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x308 (+ ?x273 ?x155)))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x307 (and $x291 $x156)))
(=> $x307 (<= ?x303 ?x308))))))))) :qid k!42))
))
(let (($x324 (=> $x311 $x323)))
(let (($x306 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let (($x304 (<= ?x303 ?x273)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x300 (not $x291)))
(let (($x302 (and $x300 (fun_app$ v_b_Visited_G_2$ ?v0))))
(=> $x302 $x304))))))) :qid k!42))
))
(let (($x326 (=> $x306 (and $x311 $x324))))
(let (($x299 (forall ((?v0 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v0)))
(<= 0 ?x273)) :qid k!42))
))
(let (($x328 (=> $x299 (and $x306 $x326))))
(let (($x330 (=> $x297 (and $x299 $x328))))
(let (($x293 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v0)))
(=> $x291 $x278))))) :qid k!42))
))
(let (($x295 (and $x293 (and true true))))
(let (($x332 (=> $x295 (and $x297 $x330))))
(let (($x290 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(<= ?x273 ?x174))) :qid k!42))
))
(let (($x334 (=> $x290 (and $x293 $x332))))
(let (($x280 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x270 (+ ?x257 ?x268)))
(let (($x272 (and (< ?x268 b_Infinity$) (< ?x270 ?x174))))
(let (($x277 (not $x272)))
(=> $x277 $x278))))))))) :qid k!42))
))
(let (($x276 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x270 (+ ?x257 ?x268)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x274 (= ?x273 ?x270)))
(let (($x272 (and (< ?x268 b_Infinity$) (< ?x270 (fun_app$c v_b_SP_G_1$ ?v0)))))
(=> $x272 $x274))))))) :qid k!42))
))
(let (($x261 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x259 (<= ?x257 ?x174)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x179 (not $x178)))
(=> $x179 $x259)))))) :qid k!42))
))
(let (($x258 (< ?x257 b_Infinity$)))
(let (($x209 (exists ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x191 (< ?x174 b_Infinity$)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x179 (not $x178)))
(and $x179 $x191))))) :qid k!42))
))
(let (($x286 (and $x209 (and $x256 (and $x258 (and $x261 (and $x266 (and $x276 $x280))))))))
(let (($x287 (and true $x286)))
(let (($x288 (and true $x287)))
(let (($x336 (=> $x288 (and $x290 $x334))))
(let (($x248 (and $x246 (=> $x246 true))))
(let (($x244 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x235 (+ ?x230 ?x155)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x231 (< ?x230 b_Infinity$)))
(let (($x241 (and $x231 $x156)))
(=> $x241 (<= ?x233 ?x235))))))))) :qid k!42))
))
(let (($x249 (=> $x244 $x248)))
(let (($x240 (forall ((?v0 B_Vertex$) )(! (let (($x238 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x235 (+ ?x230 ?x155)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x234 (< ?x230 ?x233)))
(and $x234 (= ?x233 ?x235))))))) :qid k!42))
))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x231 (< ?x230 b_Infinity$)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x232 (and $x132 $x231)))
(=> $x232 $x238))))))) :qid k!42))
))
(let (($x251 (=> $x240 (and $x244 $x249))))
(let (($x225 (and true (and $x212 (and $x215 (and $x217 (and $x220 true)))))))
(let (($x226 (and true $x225)))
(let (($x210 (not $x209)))
(let (($x228 (and true (and $x210 $x226))))
(let (($x229 (and true $x228)))
(let (($x253 (=> $x229 (and $x240 $x251))))
(let (($x199 (forall ((?v0 B_Vertex$) )(! (let (($x197 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x187 (+ ?x174 ?x155)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x193 (< ?x174 ?x182)))
(and $x193 (and $x178 (= ?x182 ?x187))))))))) :qid k!42))
))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x191 (< ?x174 b_Infinity$)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x192 (and $x132 $x191)))
(=> $x192 $x197))))))) :qid k!42))
))
(let (($x200 (and $x199 true)))
(let (($x190 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x187 (+ ?x174 ?x155)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x186 (and $x178 $x156)))
(=> $x186 (<= ?x182 ?x187))))))))) :qid k!42))
))
(let (($x185 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x183 (<= ?x182 ?x174)))
(let (($x180 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x179 (not $x178)))
(let (($x181 (and $x179 $x180)))
(=> $x181 $x183)))))))) :qid k!42))
))
(let (($x176 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(<= 0 ?x174)) :qid k!42))
))
(let (($x205 (and true (and $x173 (and $x176 (and $x185 (and $x190 $x200)))))))
(let (($x206 (and true $x205)))
(let (($x170 (forall ((?v0 B_Vertex$) )(! (let (($x168 (exists ((?v1 B_Vertex$) )(! (let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x166 (and $x136 (= (v_b_SP_G_0$ ?v0) (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0)))))))
(and (< (v_b_SP_G_0$ ?v1) (v_b_SP_G_0$ ?v0)) $x166))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x163 (and $x132 (< (v_b_SP_G_0$ ?v0) b_Infinity$))))
(=> $x163 $x168))))) :qid k!42))
))
(let (($x338 (=> (and $x170 $x206) (and $x253 $x336))))
(let (($x161 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x150 (v_b_SP_G_0$ ?v0)))
(let (($x159 (<= ?x150 (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0))))))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x157 (and $x136 $x156)))
(=> $x157 $x159))))))) :qid k!42))
))
(let (($x340 (=> $x161 (and $x170 $x338))))
(let (($x153 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x128 (v_b_SP_G_0$ ?v1)))
(let ((?x150 (v_b_SP_G_0$ ?v0)))
(let (($x151 (<= ?x150 ?x128)))
(let (($x148 (v_b_Visited_G_0$ ?v0)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x137 (not $x136)))
(let (($x149 (and $x137 $x148)))
(=> $x149 $x151)))))))) :qid k!42))
))
(let (($x342 (=> $x153 (and $x161 $x340))))
(let (($x147 (forall ((?v0 B_Vertex$) )(! (let ((?x128 (v_b_SP_G_0$ ?v0)))
(<= 0 ?x128)) :qid k!42))
))
(let (($x344 (=> $x147 (and $x153 $x342))))
(let (($x346 (=> $x145 (and $x147 $x344))))
(let (($x135 (forall ((?v0 B_Vertex$) )(! (let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(=> $x132 (= (v_b_SP_G_0$ ?v0) b_Infinity$)))) :qid k!42))
))
(let (($x131 (forall ((?v0 B_Vertex$) )(! (let (($x127 (= ?v0 b_Source$)))
(=> $x127 (= (v_b_SP_G_0$ ?v0) 0))) :qid k!42))
))
(let (($x142 (and true (and $x131 (and $x135 (and $x138 true))))))
(let (($x143 (and true $x142)))
(let (($x348 (=> $x143 (and $x145 $x346))))
(let (($x349 (not $x348)))
(let (($x710 (forall ((?v0 B_Vertex$) )(! (let (($x698 (exists ((?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x671 (+ ?x155 ?x273)))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let (($x689 (= ?x303 ?x671)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x692 (and $x291 $x689)))
(let (($x314 (< ?x273 ?x303)))
(and $x314 $x692))))))))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x313 (and $x132 (< (v_b_SP_G_2$ ?v0) b_Infinity$))))
(or (not $x313) $x698))))) :qid k!42))
))
(let (($x686 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x671 (+ ?x155 ?x273)))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let (($x674 (<= ?x303 ?x671)))
(or (not (and (fun_app$ v_b_Visited_G_2$ ?v1) (< ?x155 b_Infinity$))) $x674)))))) :qid k!42))
))
(let (($x738 (or (not $x686) $x710)))
(let (($x743 (and $x686 $x738)))
(let (($x668 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x303 (v_b_SP_G_2$ ?v0)))
(let (($x304 (<= ?x303 ?x273)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x300 (not $x291)))
(let (($x302 (and $x300 (fun_app$ v_b_Visited_G_2$ ?v0))))
(let (($x664 (not $x302)))
(or $x664 $x304)))))))) :qid k!42))
))
(let (($x750 (or (not $x668) $x743)))
(let (($x755 (and $x668 $x750)))
(let (($x762 (or (not $x299) $x755)))
(let (($x767 (and $x299 $x762)))
(let (($x774 (or $x773 $x767)))
(let (($x779 (and $x297 $x774)))
(let (($x786 (or $x785 $x779)))
(let (($x791 (and $x652 $x786)))
(let (($x798 (or (not $x290) $x791)))
(let (($x803 (and $x290 $x798)))
(let (($x617 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x278 (= ?x273 ?x174)))
(let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x270 (+ ?x257 ?x268)))
(let (($x272 (and (< ?x268 b_Infinity$) (< ?x270 ?x174))))
(or $x272 $x278)))))))) :qid k!42))
))
(let (($x611 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x270 (+ ?x257 ?x268)))
(let ((?x273 (v_b_SP_G_2$ ?v0)))
(let (($x274 (= ?x273 ?x270)))
(let (($x272 (and (< ?x268 b_Infinity$) (< ?x270 (fun_app$c v_b_SP_G_1$ ?v0)))))
(let (($x277 (not $x272)))
(or $x277 $x274)))))))) :qid k!42))
))
(let (($x620 (and $x611 $x617)))
(let (($x623 (and $x266 $x620)))
(let (($x605 (forall ((?v0 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let ((?x257 (fun_app$c v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x259 (<= ?x257 ?x174)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x178 $x259))))) :qid k!42))
))
(let (($x626 (and $x605 $x623)))
(let (($x629 (and $x258 $x626)))
(let (($x632 (and $x256 $x629)))
(let (($x635 (and $x209 $x632)))
(let (($x810 (or (not $x635) $x803)))
(let (($x557 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x521 (+ ?x155 ?x230)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x545 (<= ?x233 ?x521)))
(or (not (and (< ?x230 b_Infinity$) (< ?x155 b_Infinity$))) $x545)))))) :qid k!42))
))
(let (($x573 (or (not $x557) $x246)))
(let (($x578 (and $x557 $x573)))
(let (($x542 (forall ((?v0 B_Vertex$) )(! (let (($x530 (exists ((?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x521 (+ ?x155 ?x230)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x524 (= ?x233 ?x521)))
(let (($x234 (< ?x230 ?x233)))
(and $x234 $x524))))))) :qid k!42))
))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v0)))
(let (($x231 (< ?x230 b_Infinity$)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x232 (and $x132 $x231)))
(or (not $x232) $x530))))))) :qid k!42))
))
(let (($x585 (or (not $x542) $x578)))
(let (($x590 (and $x542 $x585)))
(let (($x597 (or (not (and $x210 (and $x212 (and $x215 (and $x217 $x220))))) $x590)))
(let (($x815 (and $x597 $x810)))
(let (($x449 (forall ((?v0 B_Vertex$) )(! (let (($x437 (exists ((?v1 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x410 (+ ?x155 ?x174)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x428 (= ?x182 ?x410)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x431 (and $x178 $x428)))
(let (($x193 (< ?x174 ?x182)))
(and $x193 $x431))))))))) :qid k!42))
))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x191 (< ?x174 b_Infinity$)))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x192 (and $x132 $x191)))
(or (not $x192) $x437))))))) :qid k!42))
))
(let (($x425 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x410 (+ ?x155 ?x174)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x413 (<= ?x182 ?x410)))
(or (not (and (fun_app$ v_b_Visited_G_1$ ?v1) (< ?x155 b_Infinity$))) $x413)))))) :qid k!42))
))
(let (($x459 (and $x425 $x449)))
(let (($x407 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?v0)))
(let (($x183 (<= ?x182 ?x174)))
(let (($x180 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x179 (not $x178)))
(let (($x181 (and $x179 $x180)))
(let (($x403 (not $x181)))
(or $x403 $x183))))))))) :qid k!42))
))
(let (($x462 (and $x407 $x459)))
(let (($x465 (and $x176 $x462)))
(let (($x468 (and $x173 $x465)))
(let (($x400 (forall ((?v0 B_Vertex$) )(! (let (($x168 (exists ((?v1 B_Vertex$) )(! (let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x166 (and $x136 (= (v_b_SP_G_0$ ?v0) (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0)))))))
(and (< (v_b_SP_G_0$ ?v1) (v_b_SP_G_0$ ?v0)) $x166))) :qid k!42))
))
(let (($x127 (= ?v0 b_Source$)))
(let (($x132 (not $x127)))
(let (($x163 (and $x132 (< (v_b_SP_G_0$ ?v0) b_Infinity$))))
(or (not $x163) $x168))))) :qid k!42))
))
(let (($x482 (and $x400 $x468)))
(let (($x822 (or (not $x482) $x815)))
(let (($x827 (and $x400 $x822)))
(let (($x393 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x150 (v_b_SP_G_0$ ?v0)))
(let (($x159 (<= ?x150 (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0))))))
(let ((?x155 (b_G$ (pair$ ?v1 ?v0))))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x157 (and $x136 $x156)))
(or (not $x157) $x159))))))) :qid k!42))
))
(let (($x834 (or (not $x393) $x827)))
(let (($x839 (and $x393 $x834)))
(let (($x386 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x128 (v_b_SP_G_0$ ?v1)))
(let ((?x150 (v_b_SP_G_0$ ?v0)))
(let (($x151 (<= ?x150 ?x128)))
(let (($x148 (v_b_Visited_G_0$ ?v0)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x137 (not $x136)))
(let (($x149 (and $x137 $x148)))
(let (($x382 (not $x149)))
(or $x382 $x151))))))))) :qid k!42))
))
(let (($x846 (or (not $x386) $x839)))
(let (($x851 (and $x386 $x846)))
(let (($x858 (or (not $x147) $x851)))
(let (($x863 (and $x147 $x858)))
(let (($x870 (or $x869 $x863)))
(let (($x875 (and $x145 $x870)))
(let (($x882 (or (not (and $x354 (and $x360 $x138))) $x875)))
(let (($x1323 (exists ((?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let (($x1306 (= (+ ?x155 ?x273 (* (- 1) (v_b_SP_G_2$ ?0))) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1262 (>= (+ ?x273 (* (- 1) (v_b_SP_G_2$ ?0))) 0)))
(let (($x1309 (not $x1262)))
(and $x1309 $x291 $x1306))))))) :qid k!42))
))
(let (($x132 (not $x127)))
(let (($x1300 (and $x132 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_2$ ?0))) 0)))))
(let (($x698 (exists ((?v1 B_Vertex$) )(! (let ((?x273 (v_b_SP_G_2$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x671 (+ ?x155 ?x273)))
(let ((?x303 (v_b_SP_G_2$ ?0)))
(let (($x689 (= ?x303 ?x671)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x692 (and $x291 $x689)))
(let (($x314 (< ?x273 ?x303)))
(and $x314 $x692))))))))) :qid k!42))
))
(let (($x705 (or (not (and $x132 (< (v_b_SP_G_2$ ?0) b_Infinity$))) $x698)))
(let ((?x273 (v_b_SP_G_2$ ?0)))
(let ((?x155 (b_G$ (pair$ ?0 ?1))))
(let (($x1306 (= (+ ?x155 ?x273 (* (- 1) (v_b_SP_G_2$ ?1))) 0)))
(let (($x291 (fun_app$ v_b_Visited_G_2$ ?0)))
(let (($x1262 (>= (+ ?x273 (* (- 1) (v_b_SP_G_2$ ?1))) 0)))
(let (($x1309 (not $x1262)))
(let (($x1318 (and $x1309 $x291 $x1306)))
(let ((?x671 (+ ?x155 ?x273)))
(let ((?x303 (v_b_SP_G_2$ ?1)))
(let (($x689 (= ?x303 ?x671)))
(let (($x692 (and $x291 $x689)))
(let (($x314 (< ?x273 ?x303)))
(let (($x695 (and $x314 $x692)))
(let ((@x1317 (monotonicity (rewrite (= $x314 $x1309)) (monotonicity (rewrite (= $x689 $x1306)) (= $x692 (and $x291 $x1306))) (= $x695 (and $x1309 (and $x291 $x1306))))))
(let ((@x1322 (trans @x1317 (rewrite (= (and $x1309 (and $x291 $x1306)) $x1318)) (= $x695 $x1318))))
(let (($x1298 (= (< ?x273 b_Infinity$) (not (<= (+ b_Infinity$ (* (- 1) ?x273)) 0)))))
(let ((@x1302 (monotonicity (rewrite $x1298) (= (and $x132 (< ?x273 b_Infinity$)) $x1300))))
(let ((@x1305 (monotonicity @x1302 (= (not (and $x132 (< ?x273 b_Infinity$))) (not $x1300)))))
(let ((@x1328 (monotonicity @x1305 (quant-intro @x1322 (= $x698 $x1323)) (= $x705 (or (not $x1300) $x1323)))))
(let (($x1282 (>= (+ ?x155 ?x273 (* (- 1) ?x303)) 0)))
(let (($x922 (<= (+ b_Infinity$ (* (- 1) ?x155)) 0)))
(let (($x923 (not $x922)))
(let (($x1276 (and $x291 $x923)))
(let (($x1279 (not $x1276)))
(let (($x1286 (or $x1279 $x1282)))
(let (($x674 (<= ?x303 ?x671)))
(let (($x681 (or (not (and $x291 (< ?x155 b_Infinity$))) $x674)))
(let ((@x925 (rewrite (= (< ?x155 b_Infinity$) $x923))))
(let ((@x1281 (monotonicity (monotonicity @x925 (= (and $x291 (< ?x155 b_Infinity$)) $x1276)) (= (not (and $x291 (< ?x155 b_Infinity$))) $x1279))))
(let ((@x1291 (quant-intro (monotonicity @x1281 (rewrite (= $x674 $x1282)) (= $x681 $x1286)) (= $x686 $x1289))))
(let ((@x1334 (monotonicity (monotonicity @x1291 (= (not $x686) $x1292)) (quant-intro @x1328 (= $x710 $x1329)) (= $x738 $x1332))))
(let (($x300 (not $x291)))
(let (($x302 (and $x300 (fun_app$ v_b_Visited_G_2$ ?1))))
(let (($x664 (not $x302)))
(let (($x1267 (or $x664 $x1262)))
(let (($x304 (<= ?x303 ?x273)))
(let (($x665 (or $x664 $x304)))
(let ((@x1272 (quant-intro (monotonicity (rewrite (= $x304 $x1262)) (= $x665 $x1267)) (= $x668 $x1270))))
(let ((@x1340 (monotonicity (monotonicity @x1272 (= (not $x668) $x1273)) (monotonicity @x1291 @x1334 (= $x743 $x1335)) (= $x750 $x1338))))
(let ((@x1258 (quant-intro (rewrite (= (<= 0 ?x273) (>= ?x273 0))) (= $x299 $x1256))))
(let ((@x1346 (monotonicity (monotonicity @x1258 (= (not $x299) $x1259)) (monotonicity @x1272 @x1340 (= $x755 $x1341)) (= $x762 $x1344))))
(let ((@x1352 (monotonicity (monotonicity @x1258 @x1346 (= $x767 $x1347)) (= $x774 $x1350))))
(let ((@x1361 (monotonicity (monotonicity (monotonicity @x1352 (= $x779 $x1353)) (= $x786 $x1356)) (= $x791 $x1359))))
(let (($x1243 (>= (+ (fun_app$c v_b_SP_G_1$ ?0) (* (- 1) ?x273)) 0)))
(let ((@x1249 (quant-intro (rewrite (= (<= ?x273 (fun_app$c v_b_SP_G_1$ ?0)) $x1243)) (= $x290 $x1247))))
(let ((@x1364 (monotonicity (monotonicity @x1249 (= (not $x290) $x1250)) @x1361 (= $x798 $x1362))))
(let (($x1232 (and $x1080 (and $x256 (and $x1214 (and $x1209 (and $x266 (and $x1193 $x1199))))))))
(let (($x1230 (= $x632 (and $x256 (and $x1214 (and $x1209 (and $x266 (and $x1193 $x1199))))))))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?0)))
(let (($x278 (= ?x273 ?x174)))
(let (($x1175 (<= (+ ?x174 ?x1173 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?0)))) 0)))
(let (($x1169 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?0)))) 0)))
(let (($x1179 (and (not $x1169) (not $x1175))))
(let (($x1196 (or $x1179 $x278)))
(let (($x272 (and (< (b_G$ (pair$ v_b_v_G_1$ ?0)) b_Infinity$) (< (+ ?x257 (b_G$ (pair$ v_b_v_G_1$ ?0))) ?x174))))
(let (($x614 (or $x272 $x278)))
(let ((@x1178 (rewrite (= (< (+ ?x257 (b_G$ (pair$ v_b_v_G_1$ ?0))) ?x174) (not $x1175)))))
(let ((@x1172 (rewrite (= (< (b_G$ (pair$ v_b_v_G_1$ ?0)) b_Infinity$) (not $x1169)))))
(let ((@x1198 (monotonicity (monotonicity @x1172 @x1178 (= $x272 $x1179)) (= $x614 $x1196))))
(let (($x1185 (= (+ ?x257 (b_G$ (pair$ v_b_v_G_1$ ?0)) (* (- 1) ?x273)) 0)))
(let (($x1182 (not $x1179)))
(let (($x1190 (or $x1182 $x1185)))
(let ((?x268 (b_G$ (pair$ v_b_v_G_1$ ?0))))
(let ((?x270 (+ ?x257 ?x268)))
(let (($x274 (= ?x273 ?x270)))
(let (($x277 (not $x272)))
(let (($x608 (or $x277 $x274)))
(let ((@x1184 (monotonicity (monotonicity @x1172 @x1178 (= $x272 $x1179)) (= $x277 $x1182))))
(let ((@x1195 (quant-intro (monotonicity @x1184 (rewrite (= $x274 $x1185)) (= $x608 $x1190)) (= $x611 $x1193))))
(let ((@x1219 (monotonicity @x1195 (quant-intro @x1198 (= $x617 $x1199)) (= $x620 (and $x1193 $x1199)))))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?0)))
(let (($x1206 (or $x178 (>= (+ ?x174 ?x1173) 0))))
(let (($x259 (<= ?x257 ?x174)))
(let (($x602 (or $x178 $x259)))
(let ((@x1208 (monotonicity (rewrite (= $x259 (>= (+ ?x174 ?x1173) 0))) (= $x602 $x1206))))
(let ((@x1225 (monotonicity (quant-intro @x1208 (= $x605 $x1209)) (monotonicity @x1219 (= $x623 (and $x266 (and $x1193 $x1199)))) (= $x626 (and $x1209 (and $x266 (and $x1193 $x1199)))))))
(let ((@x1228 (monotonicity (rewrite (= $x258 $x1214)) @x1225 (= $x629 (and $x1214 (and $x1209 (and $x266 (and $x1193 $x1199))))))))
(let (($x1002 (<= (+ b_Infinity$ (* (- 1) ?x174)) 0)))
(let (($x1003 (not $x1002)))
(let (($x179 (not $x178)))
(let (($x1077 (and $x179 $x1003)))
(let ((@x1079 (monotonicity (rewrite (= (< ?x174 b_Infinity$) $x1003)) (= (and $x179 (< ?x174 b_Infinity$)) $x1077))))
(let ((@x1234 (monotonicity (quant-intro @x1079 (= $x209 $x1080)) (monotonicity @x1228 $x1230) (= $x635 $x1232))))
(let ((@x1242 (monotonicity (trans @x1234 (rewrite (= $x1232 $x1235)) (= $x635 $x1235)) (= (not $x635) $x1240))))
(let ((@x1370 (monotonicity @x1242 (monotonicity @x1249 @x1364 (= $x803 $x1365)) (= $x810 $x1368))))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?0)))
(let (($x1140 (>= (+ ?x155 ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?1))) 0)))
(let (($x1099 (<= (+ b_Infinity$ (* (- 1) ?x230)) 0)))
(let (($x1100 (not $x1099)))
(let (($x1134 (and $x1100 $x923)))
(let (($x1137 (not $x1134)))
(let (($x1143 (or $x1137 $x1140)))
(let ((?x521 (+ ?x155 ?x230)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?1)))
(let (($x545 (<= ?x233 ?x521)))
(let (($x552 (or (not (and (< ?x230 b_Infinity$) (< ?x155 b_Infinity$))) $x545)))
(let ((@x1136 (monotonicity (rewrite (= (< ?x230 b_Infinity$) $x1100)) @x925 (= (and (< ?x230 b_Infinity$) (< ?x155 b_Infinity$)) $x1134))))
(let ((@x1139 (monotonicity @x1136 (= (not (and (< ?x230 b_Infinity$) (< ?x155 b_Infinity$))) $x1137))))
(let ((@x1148 (quant-intro (monotonicity @x1139 (rewrite (= $x545 $x1140)) (= $x552 $x1143)) (= $x557 $x1146))))
(let ((@x1154 (monotonicity (monotonicity @x1148 (= (not $x557) $x1149)) (= $x573 $x1152))))
(let (($x1122 (exists ((?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(and (not (>= (+ ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?0))) 0)) (= (+ ?x155 ?x230 (* (- 1) (fun_app$c v_b_SP_G_3$ ?0))) 0)))) :qid k!42))
))
(let (($x1103 (and $x132 $x1100)))
(let (($x1106 (not $x1103)))
(let (($x1125 (or $x1106 $x1122)))
(let (($x530 (exists ((?v1 B_Vertex$) )(! (let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x521 (+ ?x155 ?x230)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?0)))
(let (($x524 (= ?x233 ?x521)))
(let (($x234 (< ?x230 ?x233)))
(and $x234 $x524))))))) :qid k!42))
))
(let (($x537 (or (not (and $x132 (< ?x230 b_Infinity$))) $x530)))
(let (($x1119 (and (not (>= (+ ?x230 (* (- 1) ?x233)) 0)) (= (+ ?x155 ?x230 (* (- 1) ?x233)) 0))))
(let (($x524 (= ?x233 ?x521)))
(let (($x234 (< ?x230 ?x233)))
(let (($x527 (and $x234 $x524)))
(let ((@x1121 (monotonicity (rewrite (= $x234 (not (>= (+ ?x230 (* (- 1) ?x233)) 0)))) (rewrite (= $x524 (= (+ ?x155 ?x230 (* (- 1) ?x233)) 0))) (= $x527 $x1119))))
(let ((@x1105 (monotonicity (rewrite (= (< ?x230 b_Infinity$) $x1100)) (= (and $x132 (< ?x230 b_Infinity$)) $x1103))))
(let ((@x1127 (monotonicity (monotonicity @x1105 (= (not (and $x132 (< ?x230 b_Infinity$))) $x1106)) (quant-intro @x1121 (= $x530 $x1122)) (= $x537 $x1125))))
(let ((@x1133 (monotonicity (quant-intro @x1127 (= $x542 $x1128)) (= (not $x542) $x1131))))
(let ((@x1160 (monotonicity @x1133 (monotonicity @x1148 @x1154 (= $x578 $x1155)) (= $x585 $x1158))))
(let ((@x1091 (rewrite (= (and $x1083 (and $x212 (and $x215 (and $x217 $x220)))) $x1089))))
(let (($x493 (and $x212 (and $x215 (and $x217 $x220)))))
(let (($x507 (and $x210 $x493)))
(let ((@x1088 (monotonicity (monotonicity (quant-intro @x1079 (= $x209 $x1080)) (= $x210 $x1083)) (= $x507 (and $x1083 $x493)))))
(let ((@x1096 (monotonicity (trans @x1088 @x1091 (= $x507 $x1089)) (= (not $x507) $x1094))))
(let ((@x1166 (monotonicity @x1096 (monotonicity (quant-intro @x1127 (= $x542 $x1128)) @x1160 (= $x590 $x1161)) (= $x597 $x1164))))
(let (($x1070 (= (and $x980 (and $x173 (and $x1051 (and $x1045 (and $x997 $x1037))))) $x1069)))
(let (($x1067 (= $x482 (and $x980 (and $x173 (and $x1051 (and $x1045 (and $x997 $x1037))))))))
(let (($x1031 (exists ((?v1 B_Vertex$) )(! (let ((?x182 (fun_app$c v_b_SP_G_1$ ?0)))
(let ((?x991 (* (- 1) ?x182)))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let (($x1012 (= (+ ?x155 ?x174 ?x991) 0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x1015 (>= (+ ?x174 ?x991) 0)))
(let (($x1017 (not $x1015)))
(and $x1017 $x178 $x1012))))))))) :qid k!42))
))
(let (($x1006 (and $x132 $x1003)))
(let (($x1009 (not $x1006)))
(let (($x1034 (or $x1009 $x1031)))
(let (($x437 (exists ((?v1 B_Vertex$) )(! (let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x410 (+ ?x155 ?x174)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?0)))
(let (($x428 (= ?x182 ?x410)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x431 (and $x178 $x428)))
(let (($x193 (< ?x174 ?x182)))
(and $x193 $x431))))))))) :qid k!42))
))
(let (($x444 (or (not (and $x132 (< ?x174 b_Infinity$))) $x437)))
(let (($x1012 (= (+ ?x155 ?x174 (* (- 1) (fun_app$c v_b_SP_G_1$ ?1))) 0)))
(let (($x1015 (>= (+ ?x174 (* (- 1) (fun_app$c v_b_SP_G_1$ ?1))) 0)))
(let (($x1017 (not $x1015)))
(let (($x1026 (and $x1017 $x178 $x1012)))
(let ((?x410 (+ ?x155 ?x174)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?1)))
(let (($x428 (= ?x182 ?x410)))
(let (($x431 (and $x178 $x428)))
(let (($x193 (< ?x174 ?x182)))
(let (($x434 (and $x193 $x431)))
(let ((@x1025 (monotonicity (rewrite (= $x193 $x1017)) (monotonicity (rewrite (= $x428 $x1012)) (= $x431 (and $x178 $x1012))) (= $x434 (and $x1017 (and $x178 $x1012))))))
(let ((@x1030 (trans @x1025 (rewrite (= (and $x1017 (and $x178 $x1012)) $x1026)) (= $x434 $x1026))))
(let ((@x1008 (monotonicity (rewrite (= (< ?x174 b_Infinity$) $x1003)) (= (and $x132 (< ?x174 b_Infinity$)) $x1006))))
(let ((@x1036 (monotonicity (monotonicity @x1008 (= (not (and $x132 (< ?x174 b_Infinity$))) $x1009)) (quant-intro @x1030 (= $x437 $x1031)) (= $x444 $x1034))))
(let (($x990 (>= (+ ?x155 ?x174 (* (- 1) ?x182)) 0)))
(let (($x983 (and $x178 $x923)))
(let (($x986 (not $x983)))
(let (($x994 (or $x986 $x990)))
(let (($x413 (<= ?x182 ?x410)))
(let (($x420 (or (not (and $x178 (< ?x155 b_Infinity$))) $x413)))
(let ((@x988 (monotonicity (monotonicity @x925 (= (and $x178 (< ?x155 b_Infinity$)) $x983)) (= (not (and $x178 (< ?x155 b_Infinity$))) $x986))))
(let ((@x999 (quant-intro (monotonicity @x988 (rewrite (= $x413 $x990)) (= $x420 $x994)) (= $x425 $x997))))
(let ((@x1056 (monotonicity @x999 (quant-intro @x1036 (= $x449 $x1037)) (= $x459 (and $x997 $x1037)))))
(let (($x180 (fun_app$ v_b_Visited_G_1$ ?1)))
(let (($x181 (and $x179 $x180)))
(let (($x403 (not $x181)))
(let (($x1042 (or $x403 $x1015)))
(let (($x183 (<= ?x182 ?x174)))
(let (($x404 (or $x403 $x183)))
(let ((@x1047 (quant-intro (monotonicity (rewrite (= $x183 $x1015)) (= $x404 $x1042)) (= $x407 $x1045))))
(let ((@x1053 (quant-intro (rewrite (= (<= 0 ?x174) (>= ?x174 0))) (= $x176 $x1051))))
(let ((@x1062 (monotonicity @x1053 (monotonicity @x1047 @x1056 (= $x462 (and $x1045 (and $x997 $x1037)))) (= $x465 (and $x1051 (and $x1045 (and $x997 $x1037)))))))
(let ((@x1065 (monotonicity @x1062 (= $x468 (and $x173 (and $x1051 (and $x1045 (and $x997 $x1037))))))))
(let (($x974 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x128 (v_b_SP_G_0$ ?v1)))
(let (($x957 (= (+ ?x128 (* (- 1) (v_b_SP_G_0$ ?0)) ?x155) 0)))
(let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x907 (>= (+ ?x128 (* (- 1) (v_b_SP_G_0$ ?0))) 0)))
(let (($x960 (not $x907)))
(and $x960 $x136 $x957))))))) :qid k!42))
))
(let (($x951 (and $x132 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?0))) 0)))))
(let (($x954 (not $x951)))
(let (($x977 (or $x954 $x974)))
(let (($x168 (exists ((?v1 B_Vertex$) )(! (let (($x136 (v_b_Visited_G_0$ ?v1)))
(let (($x166 (and $x136 (= (v_b_SP_G_0$ ?0) (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?0)))))))
(and (< (v_b_SP_G_0$ ?v1) (v_b_SP_G_0$ ?0)) $x166))) :qid k!42))
))
(let (($x397 (or (not (and $x132 (< (v_b_SP_G_0$ ?0) b_Infinity$))) $x168)))
(let (($x957 (= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1)) ?x155) 0)))
(let (($x136 (v_b_Visited_G_0$ ?0)))
(let (($x907 (>= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1))) 0)))
(let (($x960 (not $x907)))
(let (($x969 (and $x960 $x136 $x957)))
(let (($x167 (and (< (v_b_SP_G_0$ ?0) (v_b_SP_G_0$ ?1)) (and $x136 (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x155))))))
(let (($x964 (= (and $x136 (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x155))) (and $x136 $x957))))
(let ((@x959 (rewrite (= (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x155)) $x957))))
(let ((@x968 (monotonicity (rewrite (= (< (v_b_SP_G_0$ ?0) (v_b_SP_G_0$ ?1)) $x960)) (monotonicity @x959 $x964) (= $x167 (and $x960 (and $x136 $x957))))))
(let ((@x973 (trans @x968 (rewrite (= (and $x960 (and $x136 $x957)) $x969)) (= $x167 $x969))))
(let (($x949 (= (< (v_b_SP_G_0$ ?0) b_Infinity$) (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?0))) 0)))))
(let ((@x953 (monotonicity (rewrite $x949) (= (and $x132 (< (v_b_SP_G_0$ ?0) b_Infinity$)) $x951))))
(let ((@x956 (monotonicity @x953 (= (not (and $x132 (< (v_b_SP_G_0$ ?0) b_Infinity$))) $x954))))
(let ((@x982 (quant-intro (monotonicity @x956 (quant-intro @x973 (= $x168 $x974)) (= $x397 $x977)) (= $x400 $x980))))
(let ((@x1076 (monotonicity (trans (monotonicity @x982 @x1065 $x1067) (rewrite $x1070) (= $x482 $x1069)) (= (not $x482) $x1074))))
(let ((@x1376 (monotonicity @x1076 (monotonicity @x1166 @x1370 (= $x815 $x1371)) (= $x822 $x1374))))
(let (($x933 (>= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1)) ?x155) 0)))
(let (($x926 (and $x136 $x923)))
(let (($x929 (not $x926)))
(let (($x936 (or $x929 $x933)))
(let ((?x150 (v_b_SP_G_0$ ?1)))
(let (($x159 (<= ?x150 (+ (v_b_SP_G_0$ ?0) ?x155))))
(let (($x390 (or (not (and $x136 (< ?x155 b_Infinity$))) $x159)))
(let ((@x931 (monotonicity (monotonicity @x925 (= (and $x136 (< ?x155 b_Infinity$)) $x926)) (= (not (and $x136 (< ?x155 b_Infinity$))) $x929))))
(let ((@x941 (quant-intro (monotonicity @x931 (rewrite (= $x159 $x933)) (= $x390 $x936)) (= $x393 $x939))))
(let ((@x1382 (monotonicity (monotonicity @x941 (= (not $x393) $x942)) (monotonicity @x982 @x1376 (= $x827 $x1377)) (= $x834 $x1380))))
(let (($x148 (v_b_Visited_G_0$ ?1)))
(let (($x137 (not $x136)))
(let (($x149 (and $x137 $x148)))
(let (($x382 (not $x149)))
(let (($x911 (or $x382 $x907)))
(let ((?x128 (v_b_SP_G_0$ ?0)))
(let (($x151 (<= ?x150 ?x128)))
(let (($x383 (or $x382 $x151)))
(let ((@x916 (quant-intro (monotonicity (rewrite (= $x151 $x907)) (= $x383 $x911)) (= $x386 $x914))))
(let ((@x1388 (monotonicity (monotonicity @x916 (= (not $x386) $x917)) (monotonicity @x941 @x1382 (= $x839 $x1383)) (= $x846 $x1386))))
(let ((@x901 (quant-intro (rewrite (= (<= 0 ?x128) (>= ?x128 0))) (= $x147 $x899))))
(let ((@x1394 (monotonicity (monotonicity @x901 (= (not $x147) $x902)) (monotonicity @x916 @x1388 (= $x851 $x1389)) (= $x858 $x1392))))
(let ((@x1400 (monotonicity (monotonicity @x901 @x1394 (= $x863 $x1395)) (= $x870 $x1398))))
(let ((@x895 (monotonicity (rewrite (= (and $x354 (and $x360 $x138)) $x890)) (= (not (and $x354 (and $x360 $x138))) (not $x890)))))
(let ((@x1406 (monotonicity @x895 (monotonicity @x1400 (= $x875 $x1401)) (= $x882 (or (not $x890) $x1401)))))
(let (($x318 (exists ((?v1 B_Vertex$) )(! (let (($x291 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x316 (and $x291 (= (v_b_SP_G_2$ ?0) (+ (v_b_SP_G_2$ ?v1) (b_G$ (pair$ ?v1 ?0)))))))
(let ((?x303 (v_b_SP_G_2$ ?0)))
(let ((?x273 (v_b_SP_G_2$ ?v1)))
(let (($x314 (< ?x273 ?x303)))
(and $x314 $x316)))))) :qid k!42))
))
(let (($x313 (and $x132 (< ?x273 b_Infinity$))))
(let (($x319 (=> $x313 $x318)))
(let ((@x691 (monotonicity (rewrite (= (+ ?x273 ?x155) ?x671)) (= (= ?x303 (+ ?x273 ?x155)) $x689))))
(let ((@x697 (monotonicity (monotonicity @x691 (= (and $x291 (= ?x303 (+ ?x273 ?x155))) $x692)) (= (and $x314 (and $x291 (= ?x303 (+ ?x273 ?x155)))) $x695))))
(let ((@x703 (monotonicity (quant-intro @x697 (= $x318 $x698)) (= $x319 (=> $x313 $x698)))))
(let ((@x712 (quant-intro (trans @x703 (rewrite (= (=> $x313 $x698) $x705)) (= $x319 $x705)) (= $x320 $x710))))
(let ((@x719 (trans (monotonicity @x712 (= $x321 (and $x710 false))) (rewrite (= (and $x710 false) false)) (= $x321 false))))
(let ((@x726 (trans (monotonicity @x719 (= $x322 (=> false true))) (rewrite (= (=> false true) true)) (= $x322 true))))
(let ((@x733 (trans (monotonicity @x712 @x726 (= $x323 (and $x710 true))) (rewrite (= (and $x710 true) $x710)) (= $x323 $x710))))
(let (($x156 (< ?x155 b_Infinity$)))
(let (($x307 (and $x291 $x156)))
(let (($x310 (=> $x307 (<= ?x303 (+ ?x273 ?x155)))))
(let ((@x676 (monotonicity (rewrite (= (+ ?x273 ?x155) ?x671)) (= (<= ?x303 (+ ?x273 ?x155)) $x674))))
(let ((@x685 (trans (monotonicity @x676 (= $x310 (=> $x307 $x674))) (rewrite (= (=> $x307 $x674) $x681)) (= $x310 $x681))))
(let ((@x736 (monotonicity (quant-intro @x685 (= $x311 $x686)) @x733 (= $x324 (=> $x686 $x710)))))
(let ((@x745 (monotonicity (quant-intro @x685 (= $x311 $x686)) (trans @x736 (rewrite (= (=> $x686 $x710) $x738)) (= $x324 $x738)) (= (and $x311 $x324) $x743))))
(let ((@x748 (monotonicity (quant-intro (rewrite (= (=> $x302 $x304) $x665)) (= $x306 $x668)) @x745 (= $x326 (=> $x668 $x743)))))
(let ((@x757 (monotonicity (quant-intro (rewrite (= (=> $x302 $x304) $x665)) (= $x306 $x668)) (trans @x748 (rewrite (= (=> $x668 $x743) $x750)) (= $x326 $x750)) (= (and $x306 $x326) $x755))))
(let ((@x766 (trans (monotonicity @x757 (= $x328 (=> $x299 $x755))) (rewrite (= (=> $x299 $x755) $x762)) (= $x328 $x762))))
(let ((@x772 (monotonicity (monotonicity @x766 (= (and $x299 $x328) $x767)) (= $x330 (=> $x297 $x767)))))
(let ((@x781 (monotonicity (trans @x772 (rewrite (= (=> $x297 $x767) $x774)) (= $x330 $x774)) (= (and $x297 $x330) $x779))))
(let ((@x654 (quant-intro (rewrite (= (=> $x291 $x278) (or $x300 $x278))) (= $x293 $x652))))
(let ((@x659 (monotonicity @x654 (rewrite (= (and true true) true)) (= $x295 (and $x652 true)))))
(let ((@x784 (monotonicity (trans @x659 (rewrite (= (and $x652 true) $x652)) (= $x295 $x652)) @x781 (= $x332 (=> $x652 $x779)))))
(let ((@x793 (monotonicity @x654 (trans @x784 (rewrite (= (=> $x652 $x779) $x786)) (= $x332 $x786)) (= (and $x293 $x332) $x791))))
(let ((@x802 (trans (monotonicity @x793 (= $x334 (=> $x290 $x791))) (rewrite (= (=> $x290 $x791) $x798)) (= $x334 $x798))))
(let (($x633 (= (and $x256 (and $x258 (and $x261 (and $x266 (and $x276 $x280))))) $x632)))
(let ((@x622 (monotonicity (quant-intro (rewrite (= (=> $x272 $x274) $x608)) (= $x276 $x611)) (quant-intro (rewrite (= (=> $x277 $x278) $x614)) (= $x280 $x617)) (= (and $x276 $x280) $x620))))
(let ((@x628 (monotonicity (quant-intro (rewrite (= (=> $x179 $x259) $x602)) (= $x261 $x605)) (monotonicity @x622 (= (and $x266 (and $x276 $x280)) $x623)) (= (and $x261 (and $x266 (and $x276 $x280))) $x626))))
(let ((@x631 (monotonicity @x628 (= (and $x258 (and $x261 (and $x266 (and $x276 $x280)))) $x629))))
(let ((@x640 (monotonicity (monotonicity (monotonicity @x631 $x633) (= $x286 $x635)) (= $x287 (and true $x635)))))
(let ((@x646 (monotonicity (trans @x640 (rewrite (= (and true $x635) $x635)) (= $x287 $x635)) (= $x288 (and true $x635)))))
(let ((@x808 (monotonicity (trans @x646 (rewrite (= (and true $x635) $x635)) (= $x288 $x635)) (monotonicity @x802 (= (and $x290 $x334) $x803)) (= $x336 (=> $x635 $x803)))))
(let ((@x564 (monotonicity (rewrite (= (=> $x246 true) true)) (= $x248 (and $x246 true)))))
(let (($x231 (< ?x230 b_Infinity$)))
(let (($x241 (and $x231 $x156)))
(let (($x243 (=> $x241 (<= ?x233 (+ ?x230 ?x155)))))
(let ((@x547 (monotonicity (rewrite (= (+ ?x230 ?x155) ?x521)) (= (<= ?x233 (+ ?x230 ?x155)) $x545))))
(let ((@x556 (trans (monotonicity @x547 (= $x243 (=> $x241 $x545))) (rewrite (= (=> $x241 $x545) $x552)) (= $x243 $x552))))
(let ((@x571 (monotonicity (quant-intro @x556 (= $x244 $x557)) (trans @x564 (rewrite (= (and $x246 true) $x246)) (= $x248 $x246)) (= $x249 (=> $x557 $x246)))))
(let ((@x580 (monotonicity (quant-intro @x556 (= $x244 $x557)) (trans @x571 (rewrite (= (=> $x557 $x246) $x573)) (= $x249 $x573)) (= (and $x244 $x249) $x578))))
(let (($x238 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x230 (fun_app$c v_b_SP_G_3$ ?v1)))
(let ((?x235 (+ ?x230 ?x155)))
(let ((?x233 (fun_app$c v_b_SP_G_3$ ?0)))
(let (($x234 (< ?x230 ?x233)))
(and $x234 (= ?x233 ?x235))))))) :qid k!42))
))
(let (($x232 (and $x132 $x231)))
(let (($x239 (=> $x232 $x238)))
(let ((@x526 (monotonicity (rewrite (= (+ ?x230 ?x155) ?x521)) (= (= ?x233 (+ ?x230 ?x155)) $x524))))
(let ((@x532 (quant-intro (monotonicity @x526 (= (and $x234 (= ?x233 (+ ?x230 ?x155))) $x527)) (= $x238 $x530))))
(let ((@x541 (trans (monotonicity @x532 (= $x239 (=> $x232 $x530))) (rewrite (= (=> $x232 $x530) $x537)) (= $x239 $x537))))
(let ((@x583 (monotonicity (quant-intro @x541 (= $x240 $x542)) @x580 (= $x251 (=> $x542 $x578)))))
(let ((@x592 (monotonicity (quant-intro @x541 (= $x240 $x542)) (trans @x583 (rewrite (= (=> $x542 $x578) $x585)) (= $x251 $x585)) (= (and $x240 $x251) $x590))))
(let (($x491 (= (and $x215 (and $x217 (and $x220 true))) (and $x215 (and $x217 $x220)))))
(let ((@x489 (monotonicity (rewrite (= (and $x220 true) $x220)) (= (and $x217 (and $x220 true)) (and $x217 $x220)))))
(let ((@x495 (monotonicity (monotonicity @x489 $x491) (= (and $x212 (and $x215 (and $x217 (and $x220 true)))) $x493))))
(let ((@x502 (trans (monotonicity @x495 (= $x225 (and true $x493))) (rewrite (= (and true $x493) $x493)) (= $x225 $x493))))
(let ((@x506 (trans (monotonicity @x502 (= $x226 (and true $x493))) (rewrite (= (and true $x493) $x493)) (= $x226 $x493))))
(let ((@x512 (monotonicity (monotonicity @x506 (= (and $x210 $x226) $x507)) (= $x228 (and true $x507)))))
(let ((@x518 (monotonicity (trans @x512 (rewrite (= (and true $x507) $x507)) (= $x228 $x507)) (= $x229 (and true $x507)))))
(let ((@x595 (monotonicity (trans @x518 (rewrite (= (and true $x507) $x507)) (= $x229 $x507)) @x592 (= $x253 (=> $x507 $x590)))))
(let ((@x817 (monotonicity (trans @x595 (rewrite (= (=> $x507 $x590) $x597)) (= $x253 $x597)) (trans @x808 (rewrite (= (=> $x635 $x803) $x810)) (= $x336 $x810)) (= (and $x253 $x336) $x815))))
(let (($x197 (exists ((?v1 B_Vertex$) )(! (let ((?x155 (b_G$ (pair$ ?v1 ?0))))
(let ((?x174 (fun_app$c v_b_SP_G_1$ ?v1)))
(let ((?x187 (+ ?x174 ?x155)))
(let ((?x182 (fun_app$c v_b_SP_G_1$ ?0)))
(let (($x178 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x193 (< ?x174 ?x182)))
(and $x193 (and $x178 (= ?x182 ?x187))))))))) :qid k!42))
))
(let (($x191 (< ?x174 b_Infinity$)))
(let (($x192 (and $x132 $x191)))
(let (($x198 (=> $x192 $x197)))
(let ((@x430 (monotonicity (rewrite (= (+ ?x174 ?x155) ?x410)) (= (= ?x182 (+ ?x174 ?x155)) $x428))))
(let ((@x436 (monotonicity (monotonicity @x430 (= (and $x178 (= ?x182 (+ ?x174 ?x155))) $x431)) (= (and $x193 (and $x178 (= ?x182 (+ ?x174 ?x155)))) $x434))))
(let ((@x442 (monotonicity (quant-intro @x436 (= $x197 $x437)) (= $x198 (=> $x192 $x437)))))
(let ((@x451 (quant-intro (trans @x442 (rewrite (= (=> $x192 $x437) $x444)) (= $x198 $x444)) (= $x199 $x449))))
(let ((@x458 (trans (monotonicity @x451 (= $x200 (and $x449 true))) (rewrite (= (and $x449 true) $x449)) (= $x200 $x449))))
--> --------------------

--> maximum size reached

--> --------------------

[ Verzeichnis aufwärts0.923unsichere Verbindung  ]