Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/SMT_Examples/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 193 kB image not shown  

Quelle  Boogie_Dijkstra.certs   Sprache: unbekannt

 
0a2d12aeeed9535b86d7d58cd35af090d5095447 2983 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!20 () B_Vertex$)
(declare-fun ?v0!19 () B_Vertex$)
(declare-fun ?v1!18 () 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 ((?x260 (fun_upd$ v_b_Visited_G_1$ v_b_v_G_1$ true)))
(let (($x5237 (fun_app$ ?x260 ?v0!20)))
(let (($x9037 (not $x5237)))
(let (($x261 (= v_b_Visited_G_2$ ?x260)))
(let (($x3724 (forall ((?v1 B_Vertex$) )(! (let ((?x1906 (v_b_SP_G_2$ ?v0!20)))
(let ((?x1907 (* (- 1) ?x1906)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let (($x2237 (= (+ ?x268 ?x1907 (b_G$ (pair$ ?v1 ?v0!20))) 0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x295 (not $x286)))
(or (>= (+ ?x268 ?x1907) 0) $x295 (not $x2237)))))))) :pattern ( (v_b_SP_G_2$ ?v1) ) :pattern ( (fun_app$ v_b_Visited_G_2$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!20) ) :qid k!38))
))
(let (($x3729 (not $x3724)))
(let ((?x1906 (v_b_SP_G_2$ ?v0!20)))
(let ((?x1907 (* (- 1) ?x1906)))
(let ((?x1908 (+ b_Infinity$ ?x1907)))
(let (($x1909 (<= ?x1908 0)))
(let (($x1904 (= ?v0!20 b_Source$)))
(let (($x3715 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x298 (v_b_SP_G_2$ ?v0)))
(let ((?x1258 (* (- 1) ?x298)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1277 (>= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x295 (not $x286)))
(or $x295 $x917 $x1277))))))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!38))
))
(let (($x3720 (not $x3715)))
(let (($x3732 (or $x3720 $x1904 $x1909 $x3729)))
(let (($x3735 (not $x3732)))
(let ((?x1888 (v_b_SP_G_2$ ?v0!19)))
(let ((?x1889 (* (- 1) ?x1888)))
(let ((?x1887 (v_b_SP_G_2$ ?v1!18)))
(let ((?x1879 (pair$ ?v1!18 ?v0!19)))
(let ((?x1880 (b_G$ ?x1879)))
(let (($x1891 (>= (+ ?x1880 ?x1887 ?x1889) 0)))
(let (($x1883 (<= (+ b_Infinity$ (* (- 1) ?x1880)) 0)))
(let (($x1878 (fun_app$ v_b_Visited_G_2$ ?v1!18)))
(let (($x2786 (not $x1878)))
(let (($x2801 (or $x2786 $x1883 $x1891)))
(let (($x2806 (not $x2801)))
(let (($x3738 (or $x2806 $x3735)))
(let (($x3741 (not $x3738)))
(let (($x3707 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x1257 (>= (+ (v_b_SP_G_2$ ?v1) (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x296 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x2763 (not $x296)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(or $x286 $x2763 $x1257))))) :pattern ( (v_b_SP_G_2$ ?v1) (v_b_SP_G_2$ ?v0) ) :qid k!38))
))
(let (($x3712 (not $x3707)))
(let (($x3744 (or $x3712 $x3741)))
(let (($x3747 (not $x3744)))
(let (($x1864 (>= (+ (v_b_SP_G_2$ ?v1!16) (* (- 1) (v_b_SP_G_2$ ?v0!17))) 0)))
(let (($x1857 (fun_app$ v_b_Visited_G_2$ ?v0!17)))
(let (($x2740 (not $x1857)))
(let (($x1855 (fun_app$ v_b_Visited_G_2$ ?v1!16)))
(let (($x2755 (or $x1855 $x2740 $x1864)))
(let (($x2760 (not $x2755)))
(let (($x3750 (or $x2760 $x3747)))
(let (($x3753 (not $x3750)))
(let (($x3698 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v0)))
(>= ?x268 0)) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!38))
))
(let (($x3703 (not $x3698)))
(let (($x3756 (or $x3703 $x3753)))
(let (($x3759 (not $x3756)))
(let ((?x1841 (v_b_SP_G_2$ ?v0!15)))
(let (($x1842 (>= ?x1841 0)))
(let (($x1843 (not $x1842)))
(let (($x3762 (or $x1843 $x3759)))
(let (($x3765 (not $x3762)))
(let ((?x291 (v_b_SP_G_2$ b_Source$)))
(let (($x292 (= ?x291 0)))
(let (($x768 (not $x292)))
(let (($x3768 (or $x768 $x3765)))
(let (($x3771 (not $x3768)))
(let (($x3774 (or $x768 $x3771)))
(let (($x3777 (not $x3774)))
(let (($x3690 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x295 (not $x286)))
(or $x295 $x273)))))) :pattern ( (fun_app$ v_b_Visited_G_2$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :qid k!38))
))
(let (($x3695 (not $x3690)))
(let (($x3780 (or $x3695 $x3777)))
(let (($x3783 (not $x3780)))
(let ((?x1822 (fun_app$a v_b_SP_G_1$ ?v0!14)))
(let ((?x1821 (v_b_SP_G_2$ ?v0!14)))
(let (($x1823 (= ?x1821 ?x1822)))
(let (($x1824 (or (not (fun_app$ v_b_Visited_G_2$ ?v0!14)) $x1823)))
(let (($x1825 (not $x1824)))
(let (($x3786 (or $x1825 $x3783)))
(let (($x3789 (not $x3786)))
(let (($x3681 (forall ((?v0 B_Vertex$) )(! (>= (+ (fun_app$a v_b_SP_G_1$ ?v0) (* (- 1) (v_b_SP_G_2$ ?v0))) 0) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!38))
))
(let (($x3686 (not $x3681)))
(let (($x3792 (or $x3686 $x3789)))
(let (($x3795 (not $x3792)))
(let ((?x1804 (v_b_SP_G_2$ ?v0!13)))
(let ((?x1805 (* (- 1) ?x1804)))
(let ((?x1803 (fun_app$a v_b_SP_G_1$ ?v0!13)))
(let ((?x1806 (+ ?x1803 ?x1805)))
(let (($x1807 (>= ?x1806 0)))
(let (($x1808 (not $x1807)))
(let (($x3798 (or $x1808 $x3795)))
(let (($x3801 (not $x3798)))
(let (($x3673 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1168 (* (- 1) ?x254)))
(let (($x1170 (<= (+ ?x171 ?x1168 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1164 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x2712 (or $x1164 $x1170)))
(let (($x2713 (not $x2712)))
(or $x2713 $x273)))))))))) :pattern ( (pair$ v_b_v_G_1$ ?v0) ) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!38))
))
(let (($x3678 (not $x3673)))
(let (($x3665 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v0)))
(let ((?x1181 (* (- 1) ?x268)))
(let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x1180 (= (+ ?x254 ?x263 ?x1181) 0)))
(let (($x1170 (<= (+ (fun_app$a v_b_SP_G_1$ ?v0) (* (- 1) ?x254) (* (- 1) ?x263)) 0)))
(let (($x1164 (<= (+ b_Infinity$ (* (- 1) ?x263)) 0)))
(or $x1164 $x1170 $x1180)))))))) :pattern ( (pair$ v_b_v_G_1$ ?v0) ) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :pattern ( (v_b_SP_G_2$ ?v0) ) :qid k!38))
))
(let (($x3670 (not $x3665)))
(let (($x2930 (not $x261)))
(let (($x3655 (forall ((?v0 B_Vertex$) )(! (let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1168 (* (- 1) ?x254)))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x175 (>= (+ ?x171 ?x1168) 0)))))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v0) ) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :qid k!38))
))
(let (($x3660 (not $x3655)))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1168 (* (- 1) ?x254)))
(let ((?x1207 (+ b_Infinity$ ?x1168)))
(let (($x1208 (<= ?x1207 0)))
(let (($x252 (fun_app$ v_b_Visited_G_1$ v_b_v_G_1$)))
(let ((?x1770 (fun_app$a v_b_SP_G_1$ ?v0!12)))
(let ((?x1771 (* (- 1) ?x1770)))
(let ((?x1772 (+ b_Infinity$ ?x1771)))
(let (($x1773 (<= ?x1772 0)))
(let (($x1768 (fun_app$ v_b_Visited_G_1$ ?v0!12)))
(let (($x3804 (or $x1768 $x1773 $x252 $x1208 $x3660 $x2930 $x3670 $x3678 $x3801)))
(let (($x3807 (not $x3804)))
(let ((?x242 (fun_app$a v_b_SP_G_3$ b_Source$)))
(let (($x243 (= ?x242 0)))
(let (($x3617 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1135 (>= (+ ?x152 ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0))) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x1094 (<= (+ b_Infinity$ (* (- 1) ?x227)) 0)))
(or $x1094 $x917 $x1135)))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!38))
))
(let (($x3622 (not $x3617)))
(let (($x3625 (or $x3622 $x243)))
(let (($x3628 (not $x3625)))
(let ((?x1729 (fun_app$a v_b_SP_G_3$ ?v0!11)))
(let ((?x1730 (* (- 1) ?x1729)))
(let ((?x1721 (pair$ ?v1!10 ?v0!11)))
(let ((?x1722 (b_G$ ?x1721)))
(let ((?x1716 (fun_app$a v_b_SP_G_3$ ?v1!10)))
(let ((?x2201 (+ ?x1716 ?x1722 ?x1730)))
(let (($x2204 (>= ?x2201 0)))
(let (($x1725 (<= (+ b_Infinity$ (* (- 1) ?x1722)) 0)))
(let (($x1719 (<= (+ b_Infinity$ (* (- 1) ?x1716)) 0)))
(let (($x2640 (or $x1719 $x1725 $x2204)))
(let (($x2645 (not $x2640)))
(let (($x3631 (or $x2645 $x3628)))
(let (($x3634 (not $x3631)))
(let (($x3609 (forall ((?v0 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v0)))
(let ((?x2186 (+ ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ (?v1!9 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!9 ?v0) ?v0))))))
(let (($x2187 (= ?x2186 0)))
(let (($x2171 (<= (+ ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ (?v1!9 ?v0)))) 0)))
(let (($x2612 (not (or $x2171 (not $x2187)))))
(let (($x1094 (<= (+ b_Infinity$ (* (- 1) ?x227)) 0)))
(let (($x123 (= ?v0 b_Source$)))
(or $x123 $x1094 $x2612)))))))) :pattern ( (fun_app$a v_b_SP_G_3$ ?v0) ) :qid k!38))
))
(let (($x3614 (not $x3609)))
(let (($x3637 (or $x3614 $x3634)))
(let (($x3640 (not $x3637)))
(let (($x3595 (forall ((?v1 B_Vertex$) )(! (let ((?x1656 (fun_app$a v_b_SP_G_3$ ?v0!8)))
(let ((?x1657 (* (- 1) ?x1656)))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let (($x2143 (= (+ ?x227 ?x1657 (b_G$ (pair$ ?v1 ?v0!8))) 0)))
(or (>= (+ ?x227 ?x1657) 0) (not $x2143)))))) :pattern ( (fun_app$a v_b_SP_G_3$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!8) ) :qid k!38))
))
(let (($x3600 (not $x3595)))
(let (($x1659 (<= (+ b_Infinity$ (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0!8))) 0)))
(let (($x1654 (= ?v0!8 b_Source$)))
(let (($x3603 (or $x1654 $x1659 $x3600)))
(let (($x3606 (not $x3603)))
(let (($x3643 (or $x3606 $x3640)))
(let (($x3646 (not $x3643)))
(let (($x217 (= v_b_oldSP_G_1$ v_b_oldSP_G_0$)))
(let (($x2704 (not $x217)))
(let (($x214 (= v_b_SP_G_3$ v_b_SP_G_1$)))
(let (($x2703 (not $x214)))
(let (($x212 (= v_b_v_G_2$ v_b_v_G_0$)))
(let (($x2702 (not $x212)))
(let (($x209 (= v_b_Visited_G_3$ v_b_Visited_G_1$)))
(let (($x2701 (not $x209)))
(let (($x3585 (forall ((?v0 B_Vertex$) )(! (let (($x997 (<= (+ b_Infinity$ (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x175 $x997))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v0) ) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :qid k!38))
))
(let (($x3590 (not $x3585)))
(let (($x3649 (or $x3590 $x2701 $x2702 $x2703 $x2704 $x3646)))
(let (($x3652 (not $x3649)))
(let (($x3810 (or $x3652 $x3807)))
(let (($x3813 (not $x3810)))
(let (($x3576 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x2123 (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ (?v1!7 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!7 ?v0) ?v0))))))
(let (($x2124 (= ?x2123 0)))
(let (($x2108 (<= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ (?v1!7 ?v0)))) 0)))
(let (($x2546 (not (or $x2108 (not (fun_app$ v_b_Visited_G_1$ (?v1!7 ?v0))) (not $x2124)))))
(let (($x997 (<= (+ b_Infinity$ (* (- 1) ?x171)) 0)))
(let (($x123 (= ?v0 b_Source$)))
(or $x123 $x997 $x2546)))))))) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :qid k!38))
))
(let (($x3581 (not $x3576)))
(let (($x3568 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x985 (>= (+ ?x152 ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x176 (not $x175)))
(or $x176 $x917 $x985))))))) :pattern ( (pair$ ?v1 ?v0) ) :qid k!38))
))
(let (($x3573 (not $x3568)))
(let (($x3560 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let (($x1010 (>= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(or $x175 (not (fun_app$ v_b_Visited_G_1$ ?v0)) $x1010)))) :pattern ( (fun_app$ v_b_Visited_G_1$ ?v1) (fun_app$ v_b_Visited_G_1$ ?v0) ) :qid k!38))
))
(let (($x3565 (not $x3560)))
(let (($x3551 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(>= ?x171 0)) :pattern ( (fun_app$a v_b_SP_G_1$ ?v0) ) :qid k!38))
))
(let (($x3556 (not $x3551)))
(let ((?x169 (fun_app$a v_b_SP_G_1$ b_Source$)))
(let (($x170 (= ?x169 0)))
(let (($x2947 (not $x170)))
(let (($x3542 (forall ((?v0 B_Vertex$) )(! (let ((?x124 (v_b_SP_G_0$ ?v0)))
(let ((?x2085 (+ ?x124 (* (- 1) (v_b_SP_G_0$ (?v1!6 ?v0))) (* (- 1) (b_G$ (pair$ (?v1!6 ?v0) ?v0))))))
(let (($x2086 (= ?x2085 0)))
(let (($x2070 (<= (+ ?x124 (* (- 1) (v_b_SP_G_0$ (?v1!6 ?v0)))) 0)))
(let (($x2473 (not (or $x2070 (not (fun_app$ v_b_Visited_G_0$ (?v1!6 ?v0))) (not $x2086)))))
(let (($x942 (<= (+ b_Infinity$ (* (- 1) ?x124)) 0)))
(let (($x123 (= ?v0 b_Source$)))
(or $x123 $x942 $x2473)))))))) :pattern ( (v_b_SP_G_0$ ?v0) ) :qid k!38))
))
(let (($x3547 (not $x3542)))
(let (($x3816 (or $x3547 $x2947 $x3556 $x3565 $x3573 $x3581 $x3813)))
(let (($x3819 (not $x3816)))
(let (($x3528 (forall ((?v1 B_Vertex$) )(! (let ((?x1535 (v_b_SP_G_0$ ?v0!5)))
(let ((?x1536 (* (- 1) ?x1535)))
(let ((?x124 (v_b_SP_G_0$ ?v1)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x134 (not $x133)))
(or (>= (+ ?x124 ?x1536) 0) $x134 (not (= (+ ?x124 ?x1536 (b_G$ (pair$ ?v1 ?v0!5))) 0)))))))) :pattern ( (v_b_SP_G_0$ ?v1) ) :pattern ( (fun_app$ v_b_Visited_G_0$ ?v1) ) :pattern ( (pair$ ?v1 ?v0!5) ) :qid k!38))
))
(let (($x3533 (not $x3528)))
(let ((?x1535 (v_b_SP_G_0$ ?v0!5)))
(let ((?x1536 (* (- 1) ?x1535)))
(let ((?x1537 (+ b_Infinity$ ?x1536)))
(let (($x1538 (<= ?x1537 0)))
(let (($x1533 (= ?v0!5 b_Source$)))
(let (($x3536 (or $x1533 $x1538 $x3533)))
(let (($x1534 (not $x1533)))
(let ((@x5072 (unit-resolution (def-axiom (or $x3536 $x1534)) (hypothesis (not $x3536)) $x1534)))
(let (($x5500 (= b_Infinity$ ?x1535)))
(let (($x6555 (not $x5500)))
(let (($x1539 (not $x1538)))
(let ((@x5027 (unit-resolution (def-axiom (or $x3536 $x1539)) (hypothesis (not $x3536)) $x1539)))
(let ((@x5583 (symm (commutativity (= $x5500 (= ?x1535 b_Infinity$))) (= (= ?x1535 b_Infinity$) $x5500))))
(let (($x5648 (= ?x1535 b_Infinity$)))
(let (($x3488 (forall ((?v0 B_Vertex$) )(! (let (($x123 (= ?v0 b_Source$)))
(or $x123 (= (v_b_SP_G_0$ ?v0) b_Infinity$))) :pattern ( (v_b_SP_G_0$ ?v0) ) :qid k!38))
))
(let (($x355 (forall ((?v0 B_Vertex$) )(! (let (($x123 (= ?v0 b_Source$)))
(or $x123 (= (v_b_SP_G_0$ ?v0) b_Infinity$))) :qid k!38))
))
(let (($x123 (= ?0 b_Source$)))
(let (($x352 (or $x123 (= (v_b_SP_G_0$ ?0) b_Infinity$))))
(let (($x135 (forall ((?v0 B_Vertex$) )(! (let (($x133 (fun_app$ v_b_Visited_G_0$ ?v0)))
(not $x133)) :qid k!38))
))
(let (($x349 (forall ((?v0 B_Vertex$) )(! (let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(or $x128 (= (v_b_SP_G_0$ ?v0) 0)))) :qid k!38))
))
(let (($x885 (and $x349 $x355 $x135)))
(let (($x1324 (forall ((?v0 B_Vertex$) )(! (let (($x1318 (exists ((?v1 B_Vertex$) )(! (let ((?x298 (v_b_SP_G_2$ ?v0)))
(let ((?x1258 (* (- 1) ?x298)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1301 (= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1257 (>= (+ ?x268 ?x1258) 0)))
(let (($x1304 (not $x1257)))
(and $x1304 $x286 $x1301))))))))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x1295 (and $x128 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))))
(or (not $x1295) $x1318))))) :qid k!38))
))
(let (($x1284 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x298 (v_b_SP_G_2$ ?v0)))
(let ((?x1258 (* (- 1) ?x298)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1277 (>= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x918 (not $x917)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1271 (and $x286 $x918)))
(let (($x1274 (not $x1271)))
(or $x1274 $x1277))))))))))) :qid k!38))
))
(let (($x1287 (not $x1284)))
(let (($x1327 (or $x1287 $x1324)))
(let (($x1330 (and $x1284 $x1327)))
(let (($x1265 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x1257 (>= (+ (v_b_SP_G_2$ ?v1) (* (- 1) (v_b_SP_G_2$ ?v0))) 0)))
(let (($x296 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x295 (not $x286)))
(let (($x297 (and $x295 $x296)))
(let (($x659 (not $x297)))
(or $x659 $x1257))))))) :qid k!38))
))
(let (($x1268 (not $x1265)))
(let (($x1333 (or $x1268 $x1330)))
(let (($x1336 (and $x1265 $x1333)))
(let (($x1251 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v0)))
(>= ?x268 0)) :qid k!38))
))
(let (($x1254 (not $x1251)))
(let (($x1339 (or $x1254 $x1336)))
(let (($x1342 (and $x1251 $x1339)))
(let (($x1345 (or $x768 $x1342)))
(let (($x1348 (and $x292 $x1345)))
(let (($x647 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x295 (not $x286)))
(or $x295 $x273)))))) :qid k!38))
))
(let (($x780 (not $x647)))
(let (($x1351 (or $x780 $x1348)))
(let (($x1354 (and $x647 $x1351)))
(let (($x1242 (forall ((?v0 B_Vertex$) )(! (>= (+ (fun_app$a v_b_SP_G_1$ ?v0) (* (- 1) (v_b_SP_G_2$ ?v0))) 0) :qid k!38))
))
(let (($x1245 (not $x1242)))
(let (($x1357 (or $x1245 $x1354)))
(let (($x1360 (and $x1242 $x1357)))
(let (($x1194 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1168 (* (- 1) ?x254)))
(let (($x1170 (<= (+ ?x171 ?x1168 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1164 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?v0)))) 0)))
(let (($x1174 (and (not $x1164) (not $x1170))))
(or $x1174 $x273))))))))) :qid k!38))
))
(let (($x1188 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v0)))
(let ((?x1181 (* (- 1) ?x268)))
(let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x1180 (= (+ ?x254 ?x263 ?x1181) 0)))
(let (($x1170 (<= (+ (fun_app$a v_b_SP_G_1$ ?v0) (* (- 1) ?x254) (* (- 1) ?x263)) 0)))
(let (($x1174 (and (not (<= (+ b_Infinity$ (* (- 1) ?x263)) 0)) (not $x1170))))
(let (($x1177 (not $x1174)))
(or $x1177 $x1180))))))))) :qid k!38))
))
(let (($x1204 (forall ((?v0 B_Vertex$) )(! (let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x1168 (* (- 1) ?x254)))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x175 (>= (+ ?x171 ?x1168) 0)))))) :qid k!38))
))
(let (($x1209 (not $x1208)))
(let (($x253 (not $x252)))
(let (($x1075 (exists ((?v0 B_Vertex$) )(! (let (($x997 (<= (+ b_Infinity$ (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x998 (not $x997)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x176 (not $x175)))
(and $x176 $x998))))) :qid k!38))
))
(let (($x1230 (and $x1075 $x253 $x1209 $x1204 $x261 $x1188 $x1194)))
(let (($x1235 (not $x1230)))
(let (($x1363 (or $x1235 $x1360)))
(let (($x1141 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1135 (>= (+ ?x152 ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0))) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x918 (not $x917)))
(let (($x1094 (<= (+ b_Infinity$ (* (- 1) ?x227)) 0)))
(let (($x1095 (not $x1094)))
(let (($x1129 (and $x1095 $x918)))
(let (($x1132 (not $x1129)))
(or $x1132 $x1135)))))))))) :qid k!38))
))
(let (($x1144 (not $x1141)))
(let (($x1147 (or $x1144 $x243)))
(let (($x1150 (and $x1141 $x1147)))
(let (($x1123 (forall ((?v0 B_Vertex$) )(! (let (($x1117 (exists ((?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(and (not (>= (+ ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0))) 0)) (= (+ ?x152 ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0))) 0)))) :qid k!38))
))
(let (($x1094 (<= (+ b_Infinity$ (* (- 1) (fun_app$a v_b_SP_G_3$ ?v0))) 0)))
(let (($x1095 (not $x1094)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x1098 (and $x128 $x1095)))
(let (($x1101 (not $x1098)))
(or $x1101 $x1117)))))))) :qid k!38))
))
(let (($x1126 (not $x1123)))
(let (($x1153 (or $x1126 $x1150)))
(let (($x1156 (and $x1123 $x1153)))
(let (($x1078 (not $x1075)))
(let (($x1084 (and $x1078 $x209 $x212 $x214 $x217)))
(let (($x1089 (not $x1084)))
(let (($x1159 (or $x1089 $x1156)))
(let (($x1366 (and $x1159 $x1363)))
(let (($x1032 (forall ((?v0 B_Vertex$) )(! (let (($x1026 (exists ((?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x1007 (= (+ ?x152 ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x1010 (>= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x1012 (not $x1010)))
(and $x1012 $x175 $x1007))))))) :qid k!38))
))
(let (($x997 (<= (+ b_Infinity$ (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x998 (not $x997)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x1001 (and $x128 $x998)))
(let (($x1004 (not $x1001)))
(or $x1004 $x1026)))))))) :qid k!38))
))
(let (($x992 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x985 (>= (+ ?x152 ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x918 (not $x917)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x978 (and $x175 $x918)))
(let (($x981 (not $x978)))
(or $x981 $x985))))))))) :qid k!38))
))
(let (($x1040 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let (($x1010 (>= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?v0))) 0)))
(let (($x177 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x176 (not $x175)))
(let (($x178 (and $x176 $x177)))
(let (($x398 (not $x178)))
(or $x398 $x1010)))))))) :qid k!38))
))
(let (($x1046 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(>= ?x171 0)) :qid k!38))
))
(let (($x975 (forall ((?v0 B_Vertex$) )(! (let (($x969 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x124 (v_b_SP_G_0$ ?v1)))
(let (($x952 (= (+ ?x124 (* (- 1) (v_b_SP_G_0$ ?v0)) ?x152) 0)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x902 (>= (+ ?x124 (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))
(let (($x955 (not $x902)))
(and $x955 $x133 $x952))))))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x946 (and $x128 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))))
(let (($x949 (not $x946)))
(or $x949 $x969)))))) :qid k!38))
))
(let (($x1064 (and $x975 $x170 $x1046 $x1040 $x992 $x1032)))
(let (($x1069 (not $x1064)))
(let (($x1369 (or $x1069 $x1366)))
(let (($x1372 (and $x975 $x1369)))
(let (($x934 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x124 (v_b_SP_G_0$ ?v1)))
(let (($x928 (>= (+ ?x124 (* (- 1) (v_b_SP_G_0$ ?v0)) ?x152) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x918 (not $x917)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x921 (and $x133 $x918)))
(let (($x924 (not $x921)))
(or $x924 $x928))))))))) :qid k!38))
))
(let (($x937 (not $x934)))
(let (($x1375 (or $x937 $x1372)))
(let (($x1378 (and $x934 $x1375)))
(let (($x909 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let (($x902 (>= (+ (v_b_SP_G_0$ ?v1) (* (- 1) (v_b_SP_G_0$ ?v0))) 0)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x134 (not $x133)))
(let (($x146 (and $x134 (fun_app$ v_b_Visited_G_0$ ?v0))))
(let (($x377 (not $x146)))
(or $x377 $x902)))))) :qid k!38))
))
(let (($x912 (not $x909)))
(let (($x1381 (or $x912 $x1378)))
(let (($x1384 (and $x909 $x1381)))
(let (($x894 (forall ((?v0 B_Vertex$) )(! (let ((?x124 (v_b_SP_G_0$ ?v0)))
(>= ?x124 0)) :qid k!38))
))
(let (($x897 (not $x894)))
(let (($x1387 (or $x897 $x1384)))
(let (($x1390 (and $x894 $x1387)))
(let ((?x141 (v_b_SP_G_0$ b_Source$)))
(let (($x142 (= ?x141 0)))
(let (($x864 (not $x142)))
(let (($x1393 (or $x864 $x1390)))
(let (($x1396 (and $x142 $x1393)))
(let (($x1402 (not (or (not $x885) $x1396))))
(let (($x315 (forall ((?v0 B_Vertex$) )(! (let (($x313 (exists ((?v1 B_Vertex$) )(! (let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x311 (and $x286 (= (v_b_SP_G_2$ ?v0) (+ (v_b_SP_G_2$ ?v1) (b_G$ (pair$ ?v1 ?v0)))))))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let (($x309 (< ?x268 ?x298)))
(and $x309 $x311)))))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x308 (and $x128 (< (v_b_SP_G_2$ ?v0) b_Infinity$))))
(=> $x308 $x313))))) :qid k!38))
))
(let (($x316 (and $x315 false)))
(let (($x317 (=> $x316 true)))
(let (($x318 (and $x315 $x317)))
(let (($x306 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x303 (+ ?x268 ?x152)))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x302 (and $x286 $x153)))
(=> $x302 (<= ?x298 ?x303))))))))) :qid k!38))
))
(let (($x319 (=> $x306 $x318)))
(let (($x301 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let (($x299 (<= ?x298 ?x268)))
(let (($x296 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x295 (not $x286)))
(let (($x297 (and $x295 $x296)))
(=> $x297 $x299)))))))) :qid k!38))
))
(let (($x321 (=> $x301 (and $x306 $x319))))
(let (($x294 (forall ((?v0 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v0)))
(<= 0 ?x268)) :qid k!38))
))
(let (($x323 (=> $x294 (and $x301 $x321))))
(let (($x325 (=> $x292 (and $x294 $x323))))
(let (($x288 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v0)))
(=> $x286 $x273))))) :qid k!38))
))
(let (($x290 (and $x288 (and true true))))
(let (($x327 (=> $x290 (and $x292 $x325))))
(let (($x285 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(<= ?x268 ?x171))) :qid k!38))
))
(let (($x329 (=> $x285 (and $x288 $x327))))
(let (($x275 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x265 (+ ?x254 ?x263)))
(let (($x267 (and (< ?x263 b_Infinity$) (< ?x265 ?x171))))
(let (($x272 (not $x267)))
(=> $x272 $x273))))))))) :qid k!38))
))
(let (($x271 (forall ((?v0 B_Vertex$) )(! (let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x265 (+ ?x254 ?x263)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x269 (= ?x268 ?x265)))
(let (($x267 (and (< ?x263 b_Infinity$) (< ?x265 (fun_app$a v_b_SP_G_1$ ?v0)))))
(=> $x267 $x269))))))) :qid k!38))
))
(let (($x258 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x256 (<= ?x254 ?x171)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x176 (not $x175)))
(=> $x176 $x256)))))) :qid k!38))
))
(let (($x255 (< ?x254 b_Infinity$)))
(let (($x206 (exists ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x188 (< ?x171 b_Infinity$)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x176 (not $x175)))
(and $x176 $x188))))) :qid k!38))
))
(let (($x281 (and $x206 (and $x253 (and $x255 (and $x258 (and $x261 (and $x271 $x275))))))))
(let (($x282 (and true $x281)))
(let (($x283 (and true $x282)))
(let (($x331 (=> $x283 (and $x285 $x329))))
(let (($x245 (and $x243 (=> $x243 true))))
(let (($x241 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x232 (+ ?x227 ?x152)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x228 (< ?x227 b_Infinity$)))
(let (($x238 (and $x228 $x153)))
(=> $x238 (<= ?x230 ?x232))))))))) :qid k!38))
))
(let (($x246 (=> $x241 $x245)))
(let (($x237 (forall ((?v0 B_Vertex$) )(! (let (($x235 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x232 (+ ?x227 ?x152)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x231 (< ?x227 ?x230)))
(and $x231 (= ?x230 ?x232))))))) :qid k!38))
))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x228 (< ?x227 b_Infinity$)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x229 (and $x128 $x228)))
(=> $x229 $x235))))))) :qid k!38))
))
(let (($x248 (=> $x237 (and $x241 $x246))))
(let (($x222 (and true (and $x209 (and $x212 (and $x214 (and $x217 true)))))))
(let (($x223 (and true $x222)))
(let (($x207 (not $x206)))
(let (($x225 (and true (and $x207 $x223))))
(let (($x226 (and true $x225)))
(let (($x250 (=> $x226 (and $x237 $x248))))
(let (($x196 (forall ((?v0 B_Vertex$) )(! (let (($x194 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x184 (+ ?x171 ?x152)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x190 (< ?x171 ?x179)))
(and $x190 (and $x175 (= ?x179 ?x184))))))))) :qid k!38))
))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x188 (< ?x171 b_Infinity$)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x189 (and $x128 $x188)))
(=> $x189 $x194))))))) :qid k!38))
))
(let (($x197 (and $x196 true)))
(let (($x187 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x184 (+ ?x171 ?x152)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x183 (and $x175 $x153)))
(=> $x183 (<= ?x179 ?x184))))))))) :qid k!38))
))
(let (($x182 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x180 (<= ?x179 ?x171)))
(let (($x177 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x176 (not $x175)))
(let (($x178 (and $x176 $x177)))
(=> $x178 $x180)))))))) :qid k!38))
))
(let (($x173 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(<= 0 ?x171)) :qid k!38))
))
(let (($x202 (and true (and $x170 (and $x173 (and $x182 (and $x187 $x197)))))))
(let (($x203 (and true $x202)))
(let (($x167 (forall ((?v0 B_Vertex$) )(! (let (($x165 (exists ((?v1 B_Vertex$) )(! (let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x163 (and $x133 (= (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)) $x163))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x160 (and $x128 (< (v_b_SP_G_0$ ?v0) b_Infinity$))))
(=> $x160 $x165))))) :qid k!38))
))
(let (($x333 (=> (and $x167 $x203) (and $x250 $x331))))
(let (($x158 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x147 (v_b_SP_G_0$ ?v0)))
(let (($x156 (<= ?x147 (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0))))))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x154 (and $x133 $x153)))
(=> $x154 $x156))))))) :qid k!38))
))
(let (($x335 (=> $x158 (and $x167 $x333))))
(let (($x150 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x124 (v_b_SP_G_0$ ?v1)))
(let ((?x147 (v_b_SP_G_0$ ?v0)))
(let (($x148 (<= ?x147 ?x124)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x134 (not $x133)))
(let (($x146 (and $x134 (fun_app$ v_b_Visited_G_0$ ?v0))))
(=> $x146 $x148))))))) :qid k!38))
))
(let (($x337 (=> $x150 (and $x158 $x335))))
(let (($x144 (forall ((?v0 B_Vertex$) )(! (let ((?x124 (v_b_SP_G_0$ ?v0)))
(<= 0 ?x124)) :qid k!38))
))
(let (($x339 (=> $x144 (and $x150 $x337))))
(let (($x341 (=> $x142 (and $x144 $x339))))
(let (($x131 (forall ((?v0 B_Vertex$) )(! (let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(=> $x128 (= (v_b_SP_G_0$ ?v0) b_Infinity$)))) :qid k!38))
))
(let (($x127 (forall ((?v0 B_Vertex$) )(! (let (($x123 (= ?v0 b_Source$)))
(=> $x123 (= (v_b_SP_G_0$ ?v0) 0))) :qid k!38))
))
(let (($x139 (and true (and $x127 (and $x131 (and $x135 true))))))
(let (($x140 (and true $x139)))
(let (($x343 (=> $x140 (and $x142 $x341))))
(let (($x344 (not $x343)))
(let (($x705 (forall ((?v0 B_Vertex$) )(! (let (($x693 (exists ((?v1 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x666 (+ ?x152 ?x268)))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let (($x684 (= ?x298 ?x666)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x687 (and $x286 $x684)))
(let (($x309 (< ?x268 ?x298)))
(and $x309 $x687))))))))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x308 (and $x128 (< (v_b_SP_G_2$ ?v0) b_Infinity$))))
(or (not $x308) $x693))))) :qid k!38))
))
(let (($x681 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x666 (+ ?x152 ?x268)))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let (($x669 (<= ?x298 ?x666)))
(or (not (and (fun_app$ v_b_Visited_G_2$ ?v1) (< ?x152 b_Infinity$))) $x669)))))) :qid k!38))
))
(let (($x733 (or (not $x681) $x705)))
(let (($x738 (and $x681 $x733)))
(let (($x663 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x298 (v_b_SP_G_2$ ?v0)))
(let (($x299 (<= ?x298 ?x268)))
(let (($x296 (fun_app$ v_b_Visited_G_2$ ?v0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x295 (not $x286)))
(let (($x297 (and $x295 $x296)))
(let (($x659 (not $x297)))
(or $x659 $x299))))))))) :qid k!38))
))
(let (($x745 (or (not $x663) $x738)))
(let (($x750 (and $x663 $x745)))
(let (($x757 (or (not $x294) $x750)))
(let (($x762 (and $x294 $x757)))
(let (($x769 (or $x768 $x762)))
(let (($x774 (and $x292 $x769)))
(let (($x781 (or $x780 $x774)))
(let (($x786 (and $x647 $x781)))
(let (($x793 (or (not $x285) $x786)))
(let (($x798 (and $x285 $x793)))
(let (($x612 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x273 (= ?x268 ?x171)))
(let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x265 (+ ?x254 ?x263)))
(let (($x267 (and (< ?x263 b_Infinity$) (< ?x265 ?x171))))
(or $x267 $x273)))))))) :qid k!38))
))
(let (($x606 (forall ((?v0 B_Vertex$) )(! (let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?v0))))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let ((?x265 (+ ?x254 ?x263)))
(let ((?x268 (v_b_SP_G_2$ ?v0)))
(let (($x269 (= ?x268 ?x265)))
(let (($x267 (and (< ?x263 b_Infinity$) (< ?x265 (fun_app$a v_b_SP_G_1$ ?v0)))))
(let (($x272 (not $x267)))
(or $x272 $x269)))))))) :qid k!38))
))
(let (($x615 (and $x606 $x612)))
(let (($x618 (and $x261 $x615)))
(let (($x600 (forall ((?v0 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let ((?x254 (fun_app$a v_b_SP_G_1$ v_b_v_G_1$)))
(let (($x256 (<= ?x254 ?x171)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v0)))
(or $x175 $x256))))) :qid k!38))
))
(let (($x621 (and $x600 $x618)))
(let (($x624 (and $x255 $x621)))
(let (($x627 (and $x253 $x624)))
(let (($x630 (and $x206 $x627)))
(let (($x805 (or (not $x630) $x798)))
(let (($x552 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x516 (+ ?x152 ?x227)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x540 (<= ?x230 ?x516)))
(or (not (and (< ?x227 b_Infinity$) (< ?x152 b_Infinity$))) $x540)))))) :qid k!38))
))
(let (($x568 (or (not $x552) $x243)))
(let (($x573 (and $x552 $x568)))
(let (($x537 (forall ((?v0 B_Vertex$) )(! (let (($x525 (exists ((?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x516 (+ ?x152 ?x227)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x519 (= ?x230 ?x516)))
(let (($x231 (< ?x227 ?x230)))
(and $x231 $x519))))))) :qid k!38))
))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v0)))
(let (($x228 (< ?x227 b_Infinity$)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x229 (and $x128 $x228)))
(or (not $x229) $x525))))))) :qid k!38))
))
(let (($x580 (or (not $x537) $x573)))
(let (($x585 (and $x537 $x580)))
(let (($x592 (or (not (and $x207 (and $x209 (and $x212 (and $x214 $x217))))) $x585)))
(let (($x810 (and $x592 $x805)))
(let (($x444 (forall ((?v0 B_Vertex$) )(! (let (($x432 (exists ((?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x405 (+ ?x152 ?x171)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x423 (= ?x179 ?x405)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x426 (and $x175 $x423)))
(let (($x190 (< ?x171 ?x179)))
(and $x190 $x426))))))))) :qid k!38))
))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x188 (< ?x171 b_Infinity$)))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x189 (and $x128 $x188)))
(or (not $x189) $x432))))))) :qid k!38))
))
(let (($x420 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let ((?x405 (+ ?x152 ?x171)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x408 (<= ?x179 ?x405)))
(or (not (and (fun_app$ v_b_Visited_G_1$ ?v1) (< ?x152 b_Infinity$))) $x408)))))) :qid k!38))
))
(let (($x454 (and $x420 $x444)))
(let (($x402 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?v0)))
(let (($x180 (<= ?x179 ?x171)))
(let (($x177 (fun_app$ v_b_Visited_G_1$ ?v0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x176 (not $x175)))
(let (($x178 (and $x176 $x177)))
(let (($x398 (not $x178)))
(or $x398 $x180))))))))) :qid k!38))
))
(let (($x457 (and $x402 $x454)))
(let (($x460 (and $x173 $x457)))
(let (($x463 (and $x170 $x460)))
(let (($x395 (forall ((?v0 B_Vertex$) )(! (let (($x165 (exists ((?v1 B_Vertex$) )(! (let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x163 (and $x133 (= (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)) $x163))) :qid k!38))
))
(let (($x123 (= ?v0 b_Source$)))
(let (($x128 (not $x123)))
(let (($x160 (and $x128 (< (v_b_SP_G_0$ ?v0) b_Infinity$))))
(or (not $x160) $x165))))) :qid k!38))
))
(let (($x477 (and $x395 $x463)))
(let (($x817 (or (not $x477) $x810)))
(let (($x822 (and $x395 $x817)))
(let (($x388 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x147 (v_b_SP_G_0$ ?v0)))
(let (($x156 (<= ?x147 (+ (v_b_SP_G_0$ ?v1) (b_G$ (pair$ ?v1 ?v0))))))
(let ((?x152 (b_G$ (pair$ ?v1 ?v0))))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x154 (and $x133 $x153)))
(or (not $x154) $x156))))))) :qid k!38))
))
(let (($x829 (or (not $x388) $x822)))
(let (($x834 (and $x388 $x829)))
(let (($x381 (forall ((?v0 B_Vertex$) (?v1 B_Vertex$) )(! (let ((?x124 (v_b_SP_G_0$ ?v1)))
(let ((?x147 (v_b_SP_G_0$ ?v0)))
(let (($x148 (<= ?x147 ?x124)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x134 (not $x133)))
(let (($x146 (and $x134 (fun_app$ v_b_Visited_G_0$ ?v0))))
(let (($x377 (not $x146)))
(or $x377 $x148)))))))) :qid k!38))
))
(let (($x841 (or (not $x381) $x834)))
(let (($x846 (and $x381 $x841)))
(let (($x853 (or (not $x144) $x846)))
(let (($x858 (and $x144 $x853)))
(let (($x865 (or $x864 $x858)))
(let (($x870 (and $x142 $x865)))
(let (($x877 (or (not (and $x349 (and $x355 $x135))) $x870)))
(let (($x1318 (exists ((?v1 B_Vertex$) )(! (let ((?x298 (v_b_SP_G_2$ ?0)))
(let ((?x1258 (* (- 1) ?x298)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let (($x1301 (= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x1257 (>= (+ ?x268 ?x1258) 0)))
(let (($x1304 (not $x1257)))
(and $x1304 $x286 $x1301))))))))) :qid k!38))
))
(let (($x128 (not $x123)))
(let (($x1295 (and $x128 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_2$ ?0))) 0)))))
(let (($x693 (exists ((?v1 B_Vertex$) )(! (let ((?x268 (v_b_SP_G_2$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x666 (+ ?x152 ?x268)))
(let ((?x298 (v_b_SP_G_2$ ?0)))
(let (($x684 (= ?x298 ?x666)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x687 (and $x286 $x684)))
(let (($x309 (< ?x268 ?x298)))
(and $x309 $x687))))))))) :qid k!38))
))
(let (($x700 (or (not (and $x128 (< (v_b_SP_G_2$ ?0) b_Infinity$))) $x693)))
(let ((?x298 (v_b_SP_G_2$ ?1)))
(let ((?x1258 (* (- 1) ?x298)))
(let ((?x268 (v_b_SP_G_2$ ?0)))
(let ((?x152 (b_G$ (pair$ ?0 ?1))))
(let (($x1301 (= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x286 (fun_app$ v_b_Visited_G_2$ ?0)))
(let (($x1257 (>= (+ ?x268 ?x1258) 0)))
(let (($x1304 (not $x1257)))
(let (($x1313 (and $x1304 $x286 $x1301)))
(let ((?x666 (+ ?x152 ?x268)))
(let (($x684 (= ?x298 ?x666)))
(let (($x687 (and $x286 $x684)))
(let (($x309 (< ?x268 ?x298)))
(let (($x690 (and $x309 $x687)))
(let ((@x1312 (monotonicity (rewrite (= $x309 $x1304)) (monotonicity (rewrite (= $x684 $x1301)) (= $x687 (and $x286 $x1301))) (= $x690 (and $x1304 (and $x286 $x1301))))))
(let ((@x1317 (trans @x1312 (rewrite (= (and $x1304 (and $x286 $x1301)) $x1313)) (= $x690 $x1313))))
(let (($x1293 (= (< ?x268 b_Infinity$) (not (<= (+ b_Infinity$ (* (- 1) ?x268)) 0)))))
(let ((@x1297 (monotonicity (rewrite $x1293) (= (and $x128 (< ?x268 b_Infinity$)) $x1295))))
(let ((@x1300 (monotonicity @x1297 (= (not (and $x128 (< ?x268 b_Infinity$))) (not $x1295)))))
(let ((@x1323 (monotonicity @x1300 (quant-intro @x1317 (= $x693 $x1318)) (= $x700 (or (not $x1295) $x1318)))))
(let (($x1277 (>= (+ ?x152 ?x268 ?x1258) 0)))
(let (($x917 (<= (+ b_Infinity$ (* (- 1) ?x152)) 0)))
(let (($x918 (not $x917)))
(let (($x1271 (and $x286 $x918)))
(let (($x1274 (not $x1271)))
(let (($x1281 (or $x1274 $x1277)))
(let (($x669 (<= ?x298 ?x666)))
(let (($x676 (or (not (and $x286 (< ?x152 b_Infinity$))) $x669)))
(let ((@x920 (rewrite (= (< ?x152 b_Infinity$) $x918))))
(let ((@x1276 (monotonicity (monotonicity @x920 (= (and $x286 (< ?x152 b_Infinity$)) $x1271)) (= (not (and $x286 (< ?x152 b_Infinity$))) $x1274))))
(let ((@x1286 (quant-intro (monotonicity @x1276 (rewrite (= $x669 $x1277)) (= $x676 $x1281)) (= $x681 $x1284))))
(let ((@x1329 (monotonicity (monotonicity @x1286 (= (not $x681) $x1287)) (quant-intro @x1323 (= $x705 $x1324)) (= $x733 $x1327))))
(let (($x296 (fun_app$ v_b_Visited_G_2$ ?1)))
(let (($x295 (not $x286)))
(let (($x297 (and $x295 $x296)))
(let (($x659 (not $x297)))
(let (($x1262 (or $x659 $x1257)))
(let (($x299 (<= ?x298 ?x268)))
(let (($x660 (or $x659 $x299)))
(let ((@x1267 (quant-intro (monotonicity (rewrite (= $x299 $x1257)) (= $x660 $x1262)) (= $x663 $x1265))))
(let ((@x1335 (monotonicity (monotonicity @x1267 (= (not $x663) $x1268)) (monotonicity @x1286 @x1329 (= $x738 $x1330)) (= $x745 $x1333))))
(let ((@x1253 (quant-intro (rewrite (= (<= 0 ?x268) (>= ?x268 0))) (= $x294 $x1251))))
(let ((@x1341 (monotonicity (monotonicity @x1253 (= (not $x294) $x1254)) (monotonicity @x1267 @x1335 (= $x750 $x1336)) (= $x757 $x1339))))
(let ((@x1347 (monotonicity (monotonicity @x1253 @x1341 (= $x762 $x1342)) (= $x769 $x1345))))
(let ((@x1356 (monotonicity (monotonicity (monotonicity @x1347 (= $x774 $x1348)) (= $x781 $x1351)) (= $x786 $x1354))))
(let (($x1238 (>= (+ (fun_app$a v_b_SP_G_1$ ?0) (* (- 1) ?x268)) 0)))
(let ((@x1244 (quant-intro (rewrite (= (<= ?x268 (fun_app$a v_b_SP_G_1$ ?0)) $x1238)) (= $x285 $x1242))))
(let ((@x1359 (monotonicity (monotonicity @x1244 (= (not $x285) $x1245)) @x1356 (= $x793 $x1357))))
(let (($x1227 (and $x1075 (and $x253 (and $x1209 (and $x1204 (and $x261 (and $x1188 $x1194))))))))
(let (($x1225 (= $x627 (and $x253 (and $x1209 (and $x1204 (and $x261 (and $x1188 $x1194))))))))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?0)))
(let (($x273 (= ?x268 ?x171)))
(let (($x1170 (<= (+ ?x171 ?x1168 (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?0)))) 0)))
(let (($x1164 (<= (+ b_Infinity$ (* (- 1) (b_G$ (pair$ v_b_v_G_1$ ?0)))) 0)))
(let (($x1174 (and (not $x1164) (not $x1170))))
(let (($x1191 (or $x1174 $x273)))
(let (($x267 (and (< (b_G$ (pair$ v_b_v_G_1$ ?0)) b_Infinity$) (< (+ ?x254 (b_G$ (pair$ v_b_v_G_1$ ?0))) ?x171))))
(let (($x609 (or $x267 $x273)))
(let ((@x1173 (rewrite (= (< (+ ?x254 (b_G$ (pair$ v_b_v_G_1$ ?0))) ?x171) (not $x1170)))))
(let ((@x1167 (rewrite (= (< (b_G$ (pair$ v_b_v_G_1$ ?0)) b_Infinity$) (not $x1164)))))
(let ((@x1193 (monotonicity (monotonicity @x1167 @x1173 (= $x267 $x1174)) (= $x609 $x1191))))
(let (($x1180 (= (+ ?x254 (b_G$ (pair$ v_b_v_G_1$ ?0)) (* (- 1) ?x268)) 0)))
(let (($x1177 (not $x1174)))
(let (($x1185 (or $x1177 $x1180)))
(let ((?x263 (b_G$ (pair$ v_b_v_G_1$ ?0))))
(let ((?x265 (+ ?x254 ?x263)))
(let (($x269 (= ?x268 ?x265)))
(let (($x272 (not $x267)))
(let (($x603 (or $x272 $x269)))
(let ((@x1179 (monotonicity (monotonicity @x1167 @x1173 (= $x267 $x1174)) (= $x272 $x1177))))
(let ((@x1190 (quant-intro (monotonicity @x1179 (rewrite (= $x269 $x1180)) (= $x603 $x1185)) (= $x606 $x1188))))
(let ((@x1214 (monotonicity @x1190 (quant-intro @x1193 (= $x612 $x1194)) (= $x615 (and $x1188 $x1194)))))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?0)))
(let (($x1201 (or $x175 (>= (+ ?x171 ?x1168) 0))))
(let (($x256 (<= ?x254 ?x171)))
(let (($x597 (or $x175 $x256)))
(let ((@x1203 (monotonicity (rewrite (= $x256 (>= (+ ?x171 ?x1168) 0))) (= $x597 $x1201))))
(let ((@x1220 (monotonicity (quant-intro @x1203 (= $x600 $x1204)) (monotonicity @x1214 (= $x618 (and $x261 (and $x1188 $x1194)))) (= $x621 (and $x1204 (and $x261 (and $x1188 $x1194)))))))
(let ((@x1223 (monotonicity (rewrite (= $x255 $x1209)) @x1220 (= $x624 (and $x1209 (and $x1204 (and $x261 (and $x1188 $x1194))))))))
(let (($x997 (<= (+ b_Infinity$ (* (- 1) ?x171)) 0)))
(let (($x998 (not $x997)))
(let (($x176 (not $x175)))
(let (($x1072 (and $x176 $x998)))
(let ((@x1074 (monotonicity (rewrite (= (< ?x171 b_Infinity$) $x998)) (= (and $x176 (< ?x171 b_Infinity$)) $x1072))))
(let ((@x1229 (monotonicity (quant-intro @x1074 (= $x206 $x1075)) (monotonicity @x1223 $x1225) (= $x630 $x1227))))
(let ((@x1237 (monotonicity (trans @x1229 (rewrite (= $x1227 $x1230)) (= $x630 $x1230)) (= (not $x630) $x1235))))
(let ((@x1365 (monotonicity @x1237 (monotonicity @x1244 @x1359 (= $x798 $x1360)) (= $x805 $x1363))))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?0)))
(let (($x1135 (>= (+ ?x152 ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?1))) 0)))
(let (($x1094 (<= (+ b_Infinity$ (* (- 1) ?x227)) 0)))
(let (($x1095 (not $x1094)))
(let (($x1129 (and $x1095 $x918)))
(let (($x1132 (not $x1129)))
(let (($x1138 (or $x1132 $x1135)))
(let ((?x516 (+ ?x152 ?x227)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?1)))
(let (($x540 (<= ?x230 ?x516)))
(let (($x547 (or (not (and (< ?x227 b_Infinity$) (< ?x152 b_Infinity$))) $x540)))
(let ((@x1131 (monotonicity (rewrite (= (< ?x227 b_Infinity$) $x1095)) @x920 (= (and (< ?x227 b_Infinity$) (< ?x152 b_Infinity$)) $x1129))))
(let ((@x1134 (monotonicity @x1131 (= (not (and (< ?x227 b_Infinity$) (< ?x152 b_Infinity$))) $x1132))))
(let ((@x1143 (quant-intro (monotonicity @x1134 (rewrite (= $x540 $x1135)) (= $x547 $x1138)) (= $x552 $x1141))))
(let ((@x1149 (monotonicity (monotonicity @x1143 (= (not $x552) $x1144)) (= $x568 $x1147))))
(let (($x1117 (exists ((?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(and (not (>= (+ ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?0))) 0)) (= (+ ?x152 ?x227 (* (- 1) (fun_app$a v_b_SP_G_3$ ?0))) 0)))) :qid k!38))
))
(let (($x1098 (and $x128 $x1095)))
(let (($x1101 (not $x1098)))
(let (($x1120 (or $x1101 $x1117)))
(let (($x525 (exists ((?v1 B_Vertex$) )(! (let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x516 (+ ?x152 ?x227)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?0)))
(let (($x519 (= ?x230 ?x516)))
(let (($x231 (< ?x227 ?x230)))
(and $x231 $x519))))))) :qid k!38))
))
(let (($x532 (or (not (and $x128 (< ?x227 b_Infinity$))) $x525)))
(let (($x1114 (and (not (>= (+ ?x227 (* (- 1) ?x230)) 0)) (= (+ ?x152 ?x227 (* (- 1) ?x230)) 0))))
(let (($x519 (= ?x230 ?x516)))
(let (($x231 (< ?x227 ?x230)))
(let (($x522 (and $x231 $x519)))
(let ((@x1116 (monotonicity (rewrite (= $x231 (not (>= (+ ?x227 (* (- 1) ?x230)) 0)))) (rewrite (= $x519 (= (+ ?x152 ?x227 (* (- 1) ?x230)) 0))) (= $x522 $x1114))))
(let ((@x1100 (monotonicity (rewrite (= (< ?x227 b_Infinity$) $x1095)) (= (and $x128 (< ?x227 b_Infinity$)) $x1098))))
(let ((@x1122 (monotonicity (monotonicity @x1100 (= (not (and $x128 (< ?x227 b_Infinity$))) $x1101)) (quant-intro @x1116 (= $x525 $x1117)) (= $x532 $x1120))))
(let ((@x1128 (monotonicity (quant-intro @x1122 (= $x537 $x1123)) (= (not $x537) $x1126))))
(let ((@x1155 (monotonicity @x1128 (monotonicity @x1143 @x1149 (= $x573 $x1150)) (= $x580 $x1153))))
(let ((@x1086 (rewrite (= (and $x1078 (and $x209 (and $x212 (and $x214 $x217)))) $x1084))))
(let (($x488 (and $x209 (and $x212 (and $x214 $x217)))))
(let (($x502 (and $x207 $x488)))
(let ((@x1083 (monotonicity (monotonicity (quant-intro @x1074 (= $x206 $x1075)) (= $x207 $x1078)) (= $x502 (and $x1078 $x488)))))
(let ((@x1091 (monotonicity (trans @x1083 @x1086 (= $x502 $x1084)) (= (not $x502) $x1089))))
(let ((@x1161 (monotonicity @x1091 (monotonicity (quant-intro @x1122 (= $x537 $x1123)) @x1155 (= $x585 $x1156)) (= $x592 $x1159))))
(let (($x1065 (= (and $x975 (and $x170 (and $x1046 (and $x1040 (and $x992 $x1032))))) $x1064)))
(let (($x1062 (= $x477 (and $x975 (and $x170 (and $x1046 (and $x1040 (and $x992 $x1032))))))))
(let (($x1026 (exists ((?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let (($x1007 (= (+ ?x152 ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?0))) 0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x1010 (>= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?0))) 0)))
(let (($x1012 (not $x1010)))
(and $x1012 $x175 $x1007))))))) :qid k!38))
))
(let (($x1001 (and $x128 $x998)))
(let (($x1004 (not $x1001)))
(let (($x1029 (or $x1004 $x1026)))
(let (($x432 (exists ((?v1 B_Vertex$) )(! (let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x405 (+ ?x152 ?x171)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?0)))
(let (($x423 (= ?x179 ?x405)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x426 (and $x175 $x423)))
(let (($x190 (< ?x171 ?x179)))
(and $x190 $x426))))))))) :qid k!38))
))
(let (($x439 (or (not (and $x128 (< ?x171 b_Infinity$))) $x432)))
(let (($x1007 (= (+ ?x152 ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?1))) 0)))
(let (($x1010 (>= (+ ?x171 (* (- 1) (fun_app$a v_b_SP_G_1$ ?1))) 0)))
(let (($x1012 (not $x1010)))
(let (($x1021 (and $x1012 $x175 $x1007)))
(let ((?x405 (+ ?x152 ?x171)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?1)))
(let (($x423 (= ?x179 ?x405)))
(let (($x426 (and $x175 $x423)))
(let (($x190 (< ?x171 ?x179)))
(let (($x429 (and $x190 $x426)))
(let ((@x1020 (monotonicity (rewrite (= $x190 $x1012)) (monotonicity (rewrite (= $x423 $x1007)) (= $x426 (and $x175 $x1007))) (= $x429 (and $x1012 (and $x175 $x1007))))))
(let ((@x1025 (trans @x1020 (rewrite (= (and $x1012 (and $x175 $x1007)) $x1021)) (= $x429 $x1021))))
(let ((@x1003 (monotonicity (rewrite (= (< ?x171 b_Infinity$) $x998)) (= (and $x128 (< ?x171 b_Infinity$)) $x1001))))
(let ((@x1031 (monotonicity (monotonicity @x1003 (= (not (and $x128 (< ?x171 b_Infinity$))) $x1004)) (quant-intro @x1025 (= $x432 $x1026)) (= $x439 $x1029))))
(let (($x985 (>= (+ ?x152 ?x171 (* (- 1) ?x179)) 0)))
(let (($x978 (and $x175 $x918)))
(let (($x981 (not $x978)))
(let (($x989 (or $x981 $x985)))
(let (($x408 (<= ?x179 ?x405)))
(let (($x415 (or (not (and $x175 (< ?x152 b_Infinity$))) $x408)))
(let ((@x983 (monotonicity (monotonicity @x920 (= (and $x175 (< ?x152 b_Infinity$)) $x978)) (= (not (and $x175 (< ?x152 b_Infinity$))) $x981))))
(let ((@x994 (quant-intro (monotonicity @x983 (rewrite (= $x408 $x985)) (= $x415 $x989)) (= $x420 $x992))))
(let ((@x1051 (monotonicity @x994 (quant-intro @x1031 (= $x444 $x1032)) (= $x454 (and $x992 $x1032)))))
(let (($x177 (fun_app$ v_b_Visited_G_1$ ?1)))
(let (($x178 (and $x176 $x177)))
(let (($x398 (not $x178)))
(let (($x1037 (or $x398 $x1010)))
(let (($x180 (<= ?x179 ?x171)))
(let (($x399 (or $x398 $x180)))
(let ((@x1042 (quant-intro (monotonicity (rewrite (= $x180 $x1010)) (= $x399 $x1037)) (= $x402 $x1040))))
(let ((@x1048 (quant-intro (rewrite (= (<= 0 ?x171) (>= ?x171 0))) (= $x173 $x1046))))
(let ((@x1057 (monotonicity @x1048 (monotonicity @x1042 @x1051 (= $x457 (and $x1040 (and $x992 $x1032)))) (= $x460 (and $x1046 (and $x1040 (and $x992 $x1032)))))))
(let ((@x1060 (monotonicity @x1057 (= $x463 (and $x170 (and $x1046 (and $x1040 (and $x992 $x1032))))))))
(let (($x969 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x124 (v_b_SP_G_0$ ?v1)))
(let (($x952 (= (+ ?x124 (* (- 1) (v_b_SP_G_0$ ?0)) ?x152) 0)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x902 (>= (+ ?x124 (* (- 1) (v_b_SP_G_0$ ?0))) 0)))
(let (($x955 (not $x902)))
(and $x955 $x133 $x952))))))) :qid k!38))
))
(let (($x946 (and $x128 (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?0))) 0)))))
(let (($x949 (not $x946)))
(let (($x972 (or $x949 $x969)))
(let (($x165 (exists ((?v1 B_Vertex$) )(! (let (($x133 (fun_app$ v_b_Visited_G_0$ ?v1)))
(let (($x163 (and $x133 (= (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)) $x163))) :qid k!38))
))
(let (($x392 (or (not (and $x128 (< (v_b_SP_G_0$ ?0) b_Infinity$))) $x165)))
(let (($x952 (= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1)) ?x152) 0)))
(let (($x133 (fun_app$ v_b_Visited_G_0$ ?0)))
(let (($x902 (>= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1))) 0)))
(let (($x955 (not $x902)))
(let (($x964 (and $x955 $x133 $x952)))
(let (($x164 (and (< (v_b_SP_G_0$ ?0) (v_b_SP_G_0$ ?1)) (and $x133 (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x152))))))
(let (($x959 (= (and $x133 (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x152))) (and $x133 $x952))))
(let ((@x954 (rewrite (= (= (v_b_SP_G_0$ ?1) (+ (v_b_SP_G_0$ ?0) ?x152)) $x952))))
(let ((@x963 (monotonicity (rewrite (= (< (v_b_SP_G_0$ ?0) (v_b_SP_G_0$ ?1)) $x955)) (monotonicity @x954 $x959) (= $x164 (and $x955 (and $x133 $x952))))))
(let ((@x968 (trans @x963 (rewrite (= (and $x955 (and $x133 $x952)) $x964)) (= $x164 $x964))))
(let (($x944 (= (< (v_b_SP_G_0$ ?0) b_Infinity$) (not (<= (+ b_Infinity$ (* (- 1) (v_b_SP_G_0$ ?0))) 0)))))
(let ((@x948 (monotonicity (rewrite $x944) (= (and $x128 (< (v_b_SP_G_0$ ?0) b_Infinity$)) $x946))))
(let ((@x951 (monotonicity @x948 (= (not (and $x128 (< (v_b_SP_G_0$ ?0) b_Infinity$))) $x949))))
(let ((@x977 (quant-intro (monotonicity @x951 (quant-intro @x968 (= $x165 $x969)) (= $x392 $x972)) (= $x395 $x975))))
(let ((@x1071 (monotonicity (trans (monotonicity @x977 @x1060 $x1062) (rewrite $x1065) (= $x477 $x1064)) (= (not $x477) $x1069))))
(let ((@x1371 (monotonicity @x1071 (monotonicity @x1161 @x1365 (= $x810 $x1366)) (= $x817 $x1369))))
(let (($x928 (>= (+ (v_b_SP_G_0$ ?0) (* (- 1) (v_b_SP_G_0$ ?1)) ?x152) 0)))
(let (($x921 (and $x133 $x918)))
(let (($x924 (not $x921)))
(let (($x931 (or $x924 $x928)))
(let ((?x147 (v_b_SP_G_0$ ?1)))
(let (($x156 (<= ?x147 (+ (v_b_SP_G_0$ ?0) ?x152))))
(let (($x385 (or (not (and $x133 (< ?x152 b_Infinity$))) $x156)))
(let ((@x926 (monotonicity (monotonicity @x920 (= (and $x133 (< ?x152 b_Infinity$)) $x921)) (= (not (and $x133 (< ?x152 b_Infinity$))) $x924))))
(let ((@x936 (quant-intro (monotonicity @x926 (rewrite (= $x156 $x928)) (= $x385 $x931)) (= $x388 $x934))))
(let ((@x1377 (monotonicity (monotonicity @x936 (= (not $x388) $x937)) (monotonicity @x977 @x1371 (= $x822 $x1372)) (= $x829 $x1375))))
(let (($x134 (not $x133)))
(let (($x146 (and $x134 (fun_app$ v_b_Visited_G_0$ ?1))))
(let (($x377 (not $x146)))
(let (($x906 (or $x377 $x902)))
(let ((?x124 (v_b_SP_G_0$ ?0)))
(let (($x148 (<= ?x147 ?x124)))
(let (($x378 (or $x377 $x148)))
(let ((@x911 (quant-intro (monotonicity (rewrite (= $x148 $x902)) (= $x378 $x906)) (= $x381 $x909))))
(let ((@x1383 (monotonicity (monotonicity @x911 (= (not $x381) $x912)) (monotonicity @x936 @x1377 (= $x834 $x1378)) (= $x841 $x1381))))
(let ((@x896 (quant-intro (rewrite (= (<= 0 ?x124) (>= ?x124 0))) (= $x144 $x894))))
(let ((@x1389 (monotonicity (monotonicity @x896 (= (not $x144) $x897)) (monotonicity @x911 @x1383 (= $x846 $x1384)) (= $x853 $x1387))))
(let ((@x1395 (monotonicity (monotonicity @x896 @x1389 (= $x858 $x1390)) (= $x865 $x1393))))
(let ((@x890 (monotonicity (rewrite (= (and $x349 (and $x355 $x135)) $x885)) (= (not (and $x349 (and $x355 $x135))) (not $x885)))))
(let ((@x1401 (monotonicity @x890 (monotonicity @x1395 (= $x870 $x1396)) (= $x877 (or (not $x885) $x1396)))))
(let (($x313 (exists ((?v1 B_Vertex$) )(! (let (($x286 (fun_app$ v_b_Visited_G_2$ ?v1)))
(let (($x311 (and $x286 (= (v_b_SP_G_2$ ?0) (+ (v_b_SP_G_2$ ?v1) (b_G$ (pair$ ?v1 ?0)))))))
(let ((?x298 (v_b_SP_G_2$ ?0)))
(let ((?x268 (v_b_SP_G_2$ ?v1)))
(let (($x309 (< ?x268 ?x298)))
(and $x309 $x311)))))) :qid k!38))
))
(let (($x308 (and $x128 (< ?x268 b_Infinity$))))
(let (($x314 (=> $x308 $x313)))
(let ((@x686 (monotonicity (rewrite (= (+ ?x268 ?x152) ?x666)) (= (= ?x298 (+ ?x268 ?x152)) $x684))))
(let ((@x692 (monotonicity (monotonicity @x686 (= (and $x286 (= ?x298 (+ ?x268 ?x152))) $x687)) (= (and $x309 (and $x286 (= ?x298 (+ ?x268 ?x152)))) $x690))))
(let ((@x698 (monotonicity (quant-intro @x692 (= $x313 $x693)) (= $x314 (=> $x308 $x693)))))
(let ((@x707 (quant-intro (trans @x698 (rewrite (= (=> $x308 $x693) $x700)) (= $x314 $x700)) (= $x315 $x705))))
(let ((@x714 (trans (monotonicity @x707 (= $x316 (and $x705 false))) (rewrite (= (and $x705 false) false)) (= $x316 false))))
(let ((@x721 (trans (monotonicity @x714 (= $x317 (=> false true))) (rewrite (= (=> false true) true)) (= $x317 true))))
(let ((@x728 (trans (monotonicity @x707 @x721 (= $x318 (and $x705 true))) (rewrite (= (and $x705 true) $x705)) (= $x318 $x705))))
(let (($x153 (< ?x152 b_Infinity$)))
(let (($x302 (and $x286 $x153)))
(let (($x305 (=> $x302 (<= ?x298 (+ ?x268 ?x152)))))
(let ((@x671 (monotonicity (rewrite (= (+ ?x268 ?x152) ?x666)) (= (<= ?x298 (+ ?x268 ?x152)) $x669))))
(let ((@x680 (trans (monotonicity @x671 (= $x305 (=> $x302 $x669))) (rewrite (= (=> $x302 $x669) $x676)) (= $x305 $x676))))
(let ((@x731 (monotonicity (quant-intro @x680 (= $x306 $x681)) @x728 (= $x319 (=> $x681 $x705)))))
(let ((@x740 (monotonicity (quant-intro @x680 (= $x306 $x681)) (trans @x731 (rewrite (= (=> $x681 $x705) $x733)) (= $x319 $x733)) (= (and $x306 $x319) $x738))))
(let ((@x743 (monotonicity (quant-intro (rewrite (= (=> $x297 $x299) $x660)) (= $x301 $x663)) @x740 (= $x321 (=> $x663 $x738)))))
(let ((@x752 (monotonicity (quant-intro (rewrite (= (=> $x297 $x299) $x660)) (= $x301 $x663)) (trans @x743 (rewrite (= (=> $x663 $x738) $x745)) (= $x321 $x745)) (= (and $x301 $x321) $x750))))
(let ((@x761 (trans (monotonicity @x752 (= $x323 (=> $x294 $x750))) (rewrite (= (=> $x294 $x750) $x757)) (= $x323 $x757))))
(let ((@x767 (monotonicity (monotonicity @x761 (= (and $x294 $x323) $x762)) (= $x325 (=> $x292 $x762)))))
(let ((@x776 (monotonicity (trans @x767 (rewrite (= (=> $x292 $x762) $x769)) (= $x325 $x769)) (= (and $x292 $x325) $x774))))
(let ((@x649 (quant-intro (rewrite (= (=> $x286 $x273) (or $x295 $x273))) (= $x288 $x647))))
(let ((@x654 (monotonicity @x649 (rewrite (= (and true true) true)) (= $x290 (and $x647 true)))))
(let ((@x779 (monotonicity (trans @x654 (rewrite (= (and $x647 true) $x647)) (= $x290 $x647)) @x776 (= $x327 (=> $x647 $x774)))))
(let ((@x788 (monotonicity @x649 (trans @x779 (rewrite (= (=> $x647 $x774) $x781)) (= $x327 $x781)) (= (and $x288 $x327) $x786))))
(let ((@x797 (trans (monotonicity @x788 (= $x329 (=> $x285 $x786))) (rewrite (= (=> $x285 $x786) $x793)) (= $x329 $x793))))
(let (($x628 (= (and $x253 (and $x255 (and $x258 (and $x261 (and $x271 $x275))))) $x627)))
(let ((@x617 (monotonicity (quant-intro (rewrite (= (=> $x267 $x269) $x603)) (= $x271 $x606)) (quant-intro (rewrite (= (=> $x272 $x273) $x609)) (= $x275 $x612)) (= (and $x271 $x275) $x615))))
(let ((@x623 (monotonicity (quant-intro (rewrite (= (=> $x176 $x256) $x597)) (= $x258 $x600)) (monotonicity @x617 (= (and $x261 (and $x271 $x275)) $x618)) (= (and $x258 (and $x261 (and $x271 $x275))) $x621))))
(let ((@x626 (monotonicity @x623 (= (and $x255 (and $x258 (and $x261 (and $x271 $x275)))) $x624))))
(let ((@x635 (monotonicity (monotonicity (monotonicity @x626 $x628) (= $x281 $x630)) (= $x282 (and true $x630)))))
(let ((@x641 (monotonicity (trans @x635 (rewrite (= (and true $x630) $x630)) (= $x282 $x630)) (= $x283 (and true $x630)))))
(let ((@x803 (monotonicity (trans @x641 (rewrite (= (and true $x630) $x630)) (= $x283 $x630)) (monotonicity @x797 (= (and $x285 $x329) $x798)) (= $x331 (=> $x630 $x798)))))
(let ((@x559 (monotonicity (rewrite (= (=> $x243 true) true)) (= $x245 (and $x243 true)))))
(let (($x228 (< ?x227 b_Infinity$)))
(let (($x238 (and $x228 $x153)))
(let (($x240 (=> $x238 (<= ?x230 (+ ?x227 ?x152)))))
(let ((@x542 (monotonicity (rewrite (= (+ ?x227 ?x152) ?x516)) (= (<= ?x230 (+ ?x227 ?x152)) $x540))))
(let ((@x551 (trans (monotonicity @x542 (= $x240 (=> $x238 $x540))) (rewrite (= (=> $x238 $x540) $x547)) (= $x240 $x547))))
(let ((@x566 (monotonicity (quant-intro @x551 (= $x241 $x552)) (trans @x559 (rewrite (= (and $x243 true) $x243)) (= $x245 $x243)) (= $x246 (=> $x552 $x243)))))
(let ((@x575 (monotonicity (quant-intro @x551 (= $x241 $x552)) (trans @x566 (rewrite (= (=> $x552 $x243) $x568)) (= $x246 $x568)) (= (and $x241 $x246) $x573))))
(let (($x235 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x227 (fun_app$a v_b_SP_G_3$ ?v1)))
(let ((?x232 (+ ?x227 ?x152)))
(let ((?x230 (fun_app$a v_b_SP_G_3$ ?0)))
(let (($x231 (< ?x227 ?x230)))
(and $x231 (= ?x230 ?x232))))))) :qid k!38))
))
(let (($x229 (and $x128 $x228)))
(let (($x236 (=> $x229 $x235)))
(let ((@x521 (monotonicity (rewrite (= (+ ?x227 ?x152) ?x516)) (= (= ?x230 (+ ?x227 ?x152)) $x519))))
(let ((@x527 (quant-intro (monotonicity @x521 (= (and $x231 (= ?x230 (+ ?x227 ?x152))) $x522)) (= $x235 $x525))))
(let ((@x536 (trans (monotonicity @x527 (= $x236 (=> $x229 $x525))) (rewrite (= (=> $x229 $x525) $x532)) (= $x236 $x532))))
(let ((@x578 (monotonicity (quant-intro @x536 (= $x237 $x537)) @x575 (= $x248 (=> $x537 $x573)))))
(let ((@x587 (monotonicity (quant-intro @x536 (= $x237 $x537)) (trans @x578 (rewrite (= (=> $x537 $x573) $x580)) (= $x248 $x580)) (= (and $x237 $x248) $x585))))
(let (($x486 (= (and $x212 (and $x214 (and $x217 true))) (and $x212 (and $x214 $x217)))))
(let ((@x484 (monotonicity (rewrite (= (and $x217 true) $x217)) (= (and $x214 (and $x217 true)) (and $x214 $x217)))))
(let ((@x490 (monotonicity (monotonicity @x484 $x486) (= (and $x209 (and $x212 (and $x214 (and $x217 true)))) $x488))))
(let ((@x497 (trans (monotonicity @x490 (= $x222 (and true $x488))) (rewrite (= (and true $x488) $x488)) (= $x222 $x488))))
(let ((@x501 (trans (monotonicity @x497 (= $x223 (and true $x488))) (rewrite (= (and true $x488) $x488)) (= $x223 $x488))))
(let ((@x507 (monotonicity (monotonicity @x501 (= (and $x207 $x223) $x502)) (= $x225 (and true $x502)))))
(let ((@x513 (monotonicity (trans @x507 (rewrite (= (and true $x502) $x502)) (= $x225 $x502)) (= $x226 (and true $x502)))))
(let ((@x590 (monotonicity (trans @x513 (rewrite (= (and true $x502) $x502)) (= $x226 $x502)) @x587 (= $x250 (=> $x502 $x585)))))
(let ((@x812 (monotonicity (trans @x590 (rewrite (= (=> $x502 $x585) $x592)) (= $x250 $x592)) (trans @x803 (rewrite (= (=> $x630 $x798) $x805)) (= $x331 $x805)) (= (and $x250 $x331) $x810))))
(let (($x194 (exists ((?v1 B_Vertex$) )(! (let ((?x152 (b_G$ (pair$ ?v1 ?0))))
(let ((?x171 (fun_app$a v_b_SP_G_1$ ?v1)))
(let ((?x184 (+ ?x171 ?x152)))
(let ((?x179 (fun_app$a v_b_SP_G_1$ ?0)))
(let (($x175 (fun_app$ v_b_Visited_G_1$ ?v1)))
(let (($x190 (< ?x171 ?x179)))
(and $x190 (and $x175 (= ?x179 ?x184))))))))) :qid k!38))
))
(let (($x188 (< ?x171 b_Infinity$)))
(let (($x189 (and $x128 $x188)))
(let (($x195 (=> $x189 $x194)))
(let ((@x425 (monotonicity (rewrite (= (+ ?x171 ?x152) ?x405)) (= (= ?x179 (+ ?x171 ?x152)) $x423))))
(let ((@x431 (monotonicity (monotonicity @x425 (= (and $x175 (= ?x179 (+ ?x171 ?x152))) $x426)) (= (and $x190 (and $x175 (= ?x179 (+ ?x171 ?x152)))) $x429))))
(let ((@x437 (monotonicity (quant-intro @x431 (= $x194 $x432)) (= $x195 (=> $x189 $x432)))))
(let ((@x446 (quant-intro (trans @x437 (rewrite (= (=> $x189 $x432) $x439)) (= $x195 $x439)) (= $x196 $x444))))
(let ((@x453 (trans (monotonicity @x446 (= $x197 (and $x444 true))) (rewrite (= (and $x444 true) $x444)) (= $x197 $x444))))
(let (($x183 (and $x175 $x153)))
(let (($x186 (=> $x183 (<= ?x179 (+ ?x171 ?x152)))))
(let ((@x410 (monotonicity (rewrite (= (+ ?x171 ?x152) ?x405)) (= (<= ?x179 (+ ?x171 ?x152)) $x408))))
(let ((@x419 (trans (monotonicity @x410 (= $x186 (=> $x183 $x408))) (rewrite (= (=> $x183 $x408) $x415)) (= $x186 $x415))))
(let ((@x456 (monotonicity (quant-intro @x419 (= $x187 $x420)) @x453 (= (and $x187 $x197) $x454))))
--> --------------------

--> maximum size reached

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

[ Dauer der Verarbeitung: 0.29 Sekunden  (vorverarbeitet)  ]