overflow.smt2

(set-option :produce-interpolants true)
(set-option :produce-unsat-cores true)
(set-option :simplify-interpolants true)
(set-logic QF_UFLIRA)
(set-option :verbosity 2)
(declare-fun |$b[0][0]| () Int)
(declare-fun |$b[0][1]| () Int)
(declare-fun |$b[0][2]| () Int)
(declare-fun |$b[0][3]| () Int)
(declare-fun |$b[0][4]| () Int)
(declare-fun |$b[1][0]| () Int)
(declare-fun |$b[1][1]| () Int)
(declare-fun |$b[1][2]| () Int)
(declare-fun |$b[1][3]| () Int)
(declare-fun |$b[1][4]| () Int)
(declare-fun |$b[2][0]| () Int)
(declare-fun |$b[2][1]| () Int)
(declare-fun |$b[2][2]| () Int)
(declare-fun |$b[2][3]| () Int)
(declare-fun |$b[2][4]| () Int)
(declare-fun |$b[3][0]| () Int)
(declare-fun |$b[3][1]| () Int)
(declare-fun |$b[3][2]| () Int)
(declare-fun |$b[3][3]| () Int)
(declare-fun |$b[3][4]| () Int)
(declare-fun |$b[4][0]| () Int)
(declare-fun |$b[4][1]| () Int)
(declare-fun |$b[4][2]| () Int)
(declare-fun |$b[4][3]| () Int)
(declare-fun |$b[4][4]| () Int)
(declare-fun $p () Int)
(declare-fun $m.x () Int)
(declare-fun $m.y () Int)
(declare-fun $game_complete () Bool)
(declare-fun $low_turn_bound () Bool)
(declare-fun $initial~0.a () Bool)
(declare-fun $initial~0.holds () Bool)
(declare-fun $initial~1.a () Bool)
(declare-fun $initial~1.holds () Bool)
(declare-fun $global_always~0.a () Bool)
(declare-fun $global_always~0.holds () Bool)
(declare-fun $global_always~1.a () Bool)
(declare-fun $global_always~1.holds () Bool)
(declare-fun $global_always~2.a () Bool)
(declare-fun $global_always~2.holds () Bool)
(declare-fun $global_always~3.a () Bool)
(declare-fun $global_always~3.holds () Bool)
(declare-fun $global_always~4.a () Bool)
(declare-fun $global_always~4.holds () Bool)
(declare-fun $H~0.a () Bool)
(declare-fun $H~0.holds () Bool)
(declare-fun $H~0.Z~0.holds () Bool)
(declare-fun %init () Bool)
(declare-fun |$b[0][0]-| () Int)
(declare-fun |$b[0][1]-| () Int)
(declare-fun |$b[0][2]-| () Int)
(declare-fun |$b[0][3]-| () Int)
(declare-fun |$b[0][4]-| () Int)
(declare-fun |$b[1][0]-| () Int)
(declare-fun |$b[1][1]-| () Int)
(declare-fun |$b[1][2]-| () Int)
(declare-fun |$b[1][3]-| () Int)
(declare-fun |$b[1][4]-| () Int)
(declare-fun |$b[2][0]-| () Int)
(declare-fun |$b[2][1]-| () Int)
(declare-fun |$b[2][2]-| () Int)
(declare-fun |$b[2][3]-| () Int)
(declare-fun |$b[2][4]-| () Int)
(declare-fun |$b[3][0]-| () Int)
(declare-fun |$b[3][1]-| () Int)
(declare-fun |$b[3][2]-| () Int)
(declare-fun |$b[3][3]-| () Int)
(declare-fun |$b[3][4]-| () Int)
(declare-fun |$b[4][0]-| () Int)
(declare-fun |$b[4][1]-| () Int)
(declare-fun |$b[4][2]-| () Int)
(declare-fun |$b[4][3]-| () Int)
(declare-fun |$b[4][4]-| () Int)
(declare-fun $p- () Int)
(declare-fun $m.x- () Int)
(declare-fun $m.y- () Int)
(declare-fun $game_complete- () Bool)
(declare-fun $low_turn_bound- () Bool)
(declare-fun $initial~0.a- () Bool)
(declare-fun $initial~0.holds- () Bool)
(declare-fun $initial~1.a- () Bool)
(declare-fun $initial~1.holds- () Bool)
(declare-fun $global_always~0.a- () Bool)
(declare-fun $global_always~0.holds- () Bool)
(declare-fun $global_always~1.a- () Bool)
(declare-fun $global_always~1.holds- () Bool)
(declare-fun $global_always~2.a- () Bool)
(declare-fun $global_always~2.holds- () Bool)
(declare-fun $global_always~3.a- () Bool)
(declare-fun $global_always~3.holds- () Bool)
(declare-fun $global_always~4.a- () Bool)
(declare-fun $global_always~4.holds- () Bool)
(declare-fun $H~0.a- () Bool)
(declare-fun $H~0.holds- () Bool)
(declare-fun $H~0.Z~0.holds- () Bool)
(declare-fun %init- () Bool)
(declare-fun |$b[0][0]-'| () Int)
(declare-fun |$b[0][1]-'| () Int)
(declare-fun |$b[0][2]-'| () Int)
(declare-fun |$b[0][3]-'| () Int)
(declare-fun |$b[0][4]-'| () Int)
(declare-fun |$b[1][0]-'| () Int)
(declare-fun |$b[1][1]-'| () Int)
(declare-fun |$b[1][2]-'| () Int)
(declare-fun |$b[1][3]-'| () Int)
(declare-fun |$b[1][4]-'| () Int)
(declare-fun |$b[2][0]-'| () Int)
(declare-fun |$b[2][1]-'| () Int)
(declare-fun |$b[2][2]-'| () Int)
(declare-fun |$b[2][3]-'| () Int)
(declare-fun |$b[2][4]-'| () Int)
(declare-fun |$b[3][0]-'| () Int)
(declare-fun |$b[3][1]-'| () Int)
(declare-fun |$b[3][2]-'| () Int)
(declare-fun |$b[3][3]-'| () Int)
(declare-fun |$b[3][4]-'| () Int)
(declare-fun |$b[4][0]-'| () Int)
(declare-fun |$b[4][1]-'| () Int)
(declare-fun |$b[4][2]-'| () Int)
(declare-fun |$b[4][3]-'| () Int)
(declare-fun |$b[4][4]-'| () Int)
(declare-fun |$p-'| () Int)
(declare-fun |$m.x-'| () Int)
(declare-fun |$m.y-'| () Int)
(declare-fun |$game_complete-'| () Bool)
(declare-fun |$low_turn_bound-'| () Bool)
(declare-fun |$initial~0.a-'| () Bool)
(declare-fun |$initial~0.holds-'| () Bool)
(declare-fun |$initial~1.a-'| () Bool)
(declare-fun |$initial~1.holds-'| () Bool)
(declare-fun |$global_always~0.a-'| () Bool)
(declare-fun |$global_always~0.holds-'| () Bool)
(declare-fun |$global_always~1.a-'| () Bool)
(declare-fun |$global_always~1.holds-'| () Bool)
(declare-fun |$global_always~2.a-'| () Bool)
(declare-fun |$global_always~2.holds-'| () Bool)
(declare-fun |$global_always~3.a-'| () Bool)
(declare-fun |$global_always~3.holds-'| () Bool)
(declare-fun |$global_always~4.a-'| () Bool)
(declare-fun |$global_always~4.holds-'| () Bool)
(declare-fun |$H~0.a-'| () Bool)
(declare-fun |$H~0.holds-'| () Bool)
(declare-fun |$H~0.Z~0.holds-'| () Bool)
(declare-fun |%init-'| () Bool)
(declare-fun |$b[0][0]'| () Int)
(declare-fun |$b[0][1]'| () Int)
(declare-fun |$b[0][2]'| () Int)
(declare-fun |$b[0][3]'| () Int)
(declare-fun |$b[0][4]'| () Int)
(declare-fun |$b[1][0]'| () Int)
(declare-fun |$b[1][1]'| () Int)
(declare-fun |$b[1][2]'| () Int)
(declare-fun |$b[1][3]'| () Int)
(declare-fun |$b[1][4]'| () Int)
(declare-fun |$b[2][0]'| () Int)
(declare-fun |$b[2][1]'| () Int)
(declare-fun |$b[2][2]'| () Int)
(declare-fun |$b[2][3]'| () Int)
(declare-fun |$b[2][4]'| () Int)
(declare-fun |$b[3][0]'| () Int)
(declare-fun |$b[3][1]'| () Int)
(declare-fun |$b[3][2]'| () Int)
(declare-fun |$b[3][3]'| () Int)
(declare-fun |$b[3][4]'| () Int)
(declare-fun |$b[4][0]'| () Int)
(declare-fun |$b[4][1]'| () Int)
(declare-fun |$b[4][2]'| () Int)
(declare-fun |$b[4][3]'| () Int)
(declare-fun |$b[4][4]'| () Int)
(declare-fun |$p'| () Int)
(declare-fun |$m.x'| () Int)
(declare-fun |$m.y'| () Int)
(declare-fun |$game_complete'| () Bool)
(declare-fun |$low_turn_bound'| () Bool)
(declare-fun |$initial~0.a'| () Bool)
(declare-fun |$initial~0.holds'| () Bool)
(declare-fun |$initial~1.a'| () Bool)
(declare-fun |$initial~1.holds'| () Bool)
(declare-fun |$global_always~0.a'| () Bool)
(declare-fun |$global_always~0.holds'| () Bool)
(declare-fun |$global_always~1.a'| () Bool)
(declare-fun |$global_always~1.holds'| () Bool)
(declare-fun |$global_always~2.a'| () Bool)
(declare-fun |$global_always~2.holds'| () Bool)
(declare-fun |$global_always~3.a'| () Bool)
(declare-fun |$global_always~3.holds'| () Bool)
(declare-fun |$global_always~4.a'| () Bool)
(declare-fun |$global_always~4.holds'| () Bool)
(declare-fun |$H~0.a'| () Bool)
(declare-fun |$H~0.holds'| () Bool)
(declare-fun |$H~0.Z~0.holds'| () Bool)
(declare-fun |%init'| () Bool)
(define-fun T ((|$b[0][0]| Int) (|$b[0][1]| Int) (|$b[0][2]| Int) (|$b[0][3]| Int) (|$b[0][4]| Int) (|$b[1][0]| Int) (|$b[1][1]| Int) (|$b[1][2]| Int) (|$b[1][3]| Int) (|$b[1][4]| Int) (|$b[2][0]| Int) (|$b[2][1]| Int) (|$b[2][2]| Int) (|$b[2][3]| Int) (|$b[2][4]| Int) (|$b[3][0]| Int) (|$b[3][1]| Int) (|$b[3][2]| Int) (|$b[3][3]| Int) (|$b[3][4]| Int) (|$b[4][0]| Int) (|$b[4][1]| Int) (|$b[4][2]| Int) (|$b[4][3]| Int) (|$b[4][4]| Int) ($p Int) ($m.x Int) ($m.y Int) ($game_complete Bool) ($low_turn_bound Bool) ($initial~0.a Bool) ($initial~0.holds Bool) ($initial~1.a Bool) ($initial~1.holds Bool) ($global_always~0.a Bool) ($global_always~0.holds Bool) ($global_always~1.a Bool) ($global_always~1.holds Bool) ($global_always~2.a Bool) ($global_always~2.holds Bool) ($global_always~3.a Bool) ($global_always~3.holds Bool) ($global_always~4.a Bool) ($global_always~4.holds Bool) ($H~0.a Bool) ($H~0.holds Bool) ($H~0.Z~0.holds Bool) (%init Bool) (|$b[0][0]'| Int) (|$b[0][1]'| Int) (|$b[0][2]'| Int) (|$b[0][3]'| Int) (|$b[0][4]'| Int) (|$b[1][0]'| Int) (|$b[1][1]'| Int) (|$b[1][2]'| Int) (|$b[1][3]'| Int) (|$b[1][4]'| Int) (|$b[2][0]'| Int) (|$b[2][1]'| Int) (|$b[2][2]'| Int) (|$b[2][3]'| Int) (|$b[2][4]'| Int) (|$b[3][0]'| Int) (|$b[3][1]'| Int) (|$b[3][2]'| Int) (|$b[3][3]'| Int) (|$b[3][4]'| Int) (|$b[4][0]'| Int) (|$b[4][1]'| Int) (|$b[4][2]'| Int) (|$b[4][3]'| Int) (|$b[4][4]'| Int) (|$p'| Int) (|$m.x'| Int) (|$m.y'| Int) (|$game_complete'| Bool) (|$low_turn_bound'| Bool) (|$initial~0.a'| Bool) (|$initial~0.holds'| Bool) (|$initial~1.a'| Bool) (|$initial~1.holds'| Bool) (|$global_always~0.a'| Bool) (|$global_always~0.holds'| Bool) (|$global_always~1.a'| Bool) (|$global_always~1.holds'| Bool) (|$global_always~2.a'| Bool) (|$global_always~2.holds'| Bool) (|$global_always~3.a'| Bool) (|$global_always~3.holds'| Bool) (|$global_always~4.a'| Bool) (|$global_always~4.holds'| Bool) (|$H~0.a'| Bool) (|$H~0.holds'| Bool) (|$H~0.Z~0.holds'| Bool) (|%init'| Bool)) Bool (and (= |$low_turn_bound'| (=> |$H~0.holds'| |$global_always~4.holds'|)) (= |$initial~0.a'| (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= |$b[0][0]'| 0) (= |$b[0][1]'| 0)) (= |$b[0][2]'| 0)) (= |$b[0][3]'| 0)) (= |$b[0][4]'| 0)) (= |$b[1][0]'| 0)) (= |$b[1][1]'| 0)) (= |$b[1][2]'| 0)) (= |$b[1][3]'| 0)) (= |$b[1][4]'| 0)) (= |$b[2][0]'| 0)) (= |$b[2][1]'| 0)) (= |$b[2][2]'| 0)) (= |$b[2][3]'| 0)) (= |$b[2][4]'| 0)) (= |$b[3][0]'| 0)) (= |$b[3][1]'| 0)) (= |$b[3][2]'| 0)) (= |$b[3][3]'| 0)) (= |$b[3][4]'| 0)) (= |$b[4][0]'| 0)) (= |$b[4][1]'| 0)) (= |$b[4][2]'| 0)) (= |$b[4][3]'| 0)) (= |$b[4][4]'| 0))) (= |$initial~0.holds'| (or (not %init) |$initial~0.a'|)) (= |$initial~1.a'| (= |$p'| 1)) (= |$initial~1.holds'| (or (not %init) |$initial~1.a'|)) (= |$global_always~0.a'| (or %init (ite (= $p 0) (= |$p'| 1) (= |$p'| 0)))) (= |$global_always~0.holds'| (and |$global_always~0.a'| (or %init $global_always~0.holds))) (= |$global_always~1.a'| (or %init (= (ite (= |$m.y'| 0) (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0))))) (ite (= |$m.y'| 1) (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0))))) (ite (= |$m.y'| 2) (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0))))) (ite (= |$m.y'| 3) (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0))))) (ite (= |$m.y'| 4) (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0))))) 0))))) 0))) (= |$global_always~1.holds'| (and |$global_always~1.a'| (or %init $global_always~1.holds))) (= |$global_always~2.a'| (or %init (ite (= |$p'| 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 0) 1 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[0][0]|) |$b[0][0]'|) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 1) 1 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[0][1]|) |$b[0][1]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 2) 1 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[0][2]|) |$b[0][2]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 3) 1 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[0][3]|) |$b[0][3]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 4) 1 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[0][4]|) |$b[0][4]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 0) 1 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[1][0]|) |$b[1][0]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 1) 1 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[1][1]|) |$b[1][1]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 2) 1 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[1][2]|) |$b[1][2]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 3) 1 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[1][3]|) |$b[1][3]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 4) 1 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[1][4]|) |$b[1][4]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 0) 1 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[2][0]|) |$b[2][0]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 1) 1 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[2][1]|) |$b[2][1]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 2) 1 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[2][2]|) |$b[2][2]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 3) 1 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[2][3]|) |$b[2][3]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 4) 1 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[2][4]|) |$b[2][4]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 0) 1 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[3][0]|) |$b[3][0]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 1) 1 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[3][1]|) |$b[3][1]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 2) 1 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[3][2]|) |$b[3][2]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 3) 1 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[3][3]|) |$b[3][3]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 4) 1 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[3][4]|) |$b[3][4]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 0) 1 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[4][0]|) |$b[4][0]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 1) 1 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[4][1]|) |$b[4][1]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 2) 1 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[4][2]|) |$b[4][2]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 3) 1 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[4][3]|) |$b[4][3]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 4) 1 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[4][4]|) |$b[4][4]'|)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 0) 2 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[0][0]|) |$b[0][0]'|) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 1) 2 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[0][1]|) |$b[0][1]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 2) 2 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[0][2]|) |$b[0][2]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 3) 2 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[0][3]|) |$b[0][3]'|)) (= (ite (= |$m.x'| 0) (ite (= |$m.y'| 4) 2 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[0][4]|) |$b[0][4]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 0) 2 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[1][0]|) |$b[1][0]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 1) 2 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[1][1]|) |$b[1][1]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 2) 2 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[1][2]|) |$b[1][2]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 3) 2 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[1][3]|) |$b[1][3]'|)) (= (ite (= |$m.x'| 1) (ite (= |$m.y'| 4) 2 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[1][4]|) |$b[1][4]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 0) 2 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[2][0]|) |$b[2][0]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 1) 2 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[2][1]|) |$b[2][1]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 2) 2 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[2][2]|) |$b[2][2]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 3) 2 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[2][3]|) |$b[2][3]'|)) (= (ite (= |$m.x'| 2) (ite (= |$m.y'| 4) 2 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[2][4]|) |$b[2][4]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 0) 2 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[3][0]|) |$b[3][0]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 1) 2 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[3][1]|) |$b[3][1]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 2) 2 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[3][2]|) |$b[3][2]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 3) 2 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[3][3]|) |$b[3][3]'|)) (= (ite (= |$m.x'| 3) (ite (= |$m.y'| 4) 2 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[3][4]|) |$b[3][4]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 0) 2 (ite (= |$m.x'| 0) |$b[0][0]| (ite (= |$m.x'| 1) |$b[1][0]| (ite (= |$m.x'| 2) |$b[2][0]| (ite (= |$m.x'| 3) |$b[3][0]| (ite (= |$m.x'| 4) |$b[4][0]| 0)))))) |$b[4][0]|) |$b[4][0]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 1) 2 (ite (= |$m.x'| 0) |$b[0][1]| (ite (= |$m.x'| 1) |$b[1][1]| (ite (= |$m.x'| 2) |$b[2][1]| (ite (= |$m.x'| 3) |$b[3][1]| (ite (= |$m.x'| 4) |$b[4][1]| 0)))))) |$b[4][1]|) |$b[4][1]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 2) 2 (ite (= |$m.x'| 0) |$b[0][2]| (ite (= |$m.x'| 1) |$b[1][2]| (ite (= |$m.x'| 2) |$b[2][2]| (ite (= |$m.x'| 3) |$b[3][2]| (ite (= |$m.x'| 4) |$b[4][2]| 0)))))) |$b[4][2]|) |$b[4][2]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 3) 2 (ite (= |$m.x'| 0) |$b[0][3]| (ite (= |$m.x'| 1) |$b[1][3]| (ite (= |$m.x'| 2) |$b[2][3]| (ite (= |$m.x'| 3) |$b[3][3]| (ite (= |$m.x'| 4) |$b[4][3]| 0)))))) |$b[4][3]|) |$b[4][3]'|)) (= (ite (= |$m.x'| 4) (ite (= |$m.y'| 4) 2 (ite (= |$m.x'| 0) |$b[0][4]| (ite (= |$m.x'| 1) |$b[1][4]| (ite (= |$m.x'| 2) |$b[2][4]| (ite (= |$m.x'| 3) |$b[3][4]| (ite (= |$m.x'| 4) |$b[4][4]| 0)))))) |$b[4][4]|) |$b[4][4]'|))))) (= |$global_always~2.holds'| (and |$global_always~2.a'| (or %init $global_always~2.holds))) (= |$global_always~3.a'| (ite (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= |$b[0][0]'| 0)) (not (= |$b[0][1]'| 0))) (not (= |$b[0][2]'| 0))) (not (= |$b[0][3]'| 0))) (not (= |$b[0][4]'| 0))) (not (= |$b[1][0]'| 0))) (not (= |$b[1][1]'| 0))) (not (= |$b[1][2]'| 0))) (not (= |$b[1][3]'| 0))) (not (= |$b[1][4]'| 0))) (not (= |$b[2][0]'| 0))) (not (= |$b[2][1]'| 0))) (not (= |$b[2][2]'| 0))) (not (= |$b[2][3]'| 0))) (not (= |$b[2][4]'| 0))) (not (= |$b[3][0]'| 0))) (not (= |$b[3][1]'| 0))) (not (= |$b[3][2]'| 0))) (not (= |$b[3][3]'| 0))) (not (= |$b[3][4]'| 0))) (not (= |$b[4][0]'| 0))) (not (= |$b[4][1]'| 0))) (not (= |$b[4][2]'| 0))) (not (= |$b[4][3]'| 0))) (not (= |$b[4][4]'| 0))) (or (or (or (or (or (and (not (= 0 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 0) (= |$b[1][0]'| 0)) (= |$b[2][0]'| 0)) (= |$b[3][0]'| 0)) (= |$b[4][0]'| 0)) (and (and (and (and (= |$b[0][1]'| 0) (= |$b[1][1]'| 0)) (= |$b[2][1]'| 0)) (= |$b[3][1]'| 0)) (= |$b[4][1]'| 0))) (and (and (and (and (= |$b[0][2]'| 0) (= |$b[1][2]'| 0)) (= |$b[2][2]'| 0)) (= |$b[3][2]'| 0)) (= |$b[4][2]'| 0))) (and (and (and (and (= |$b[0][3]'| 0) (= |$b[1][3]'| 0)) (= |$b[2][3]'| 0)) (= |$b[3][3]'| 0)) (= |$b[4][3]'| 0))) (and (and (and (and (= |$b[0][4]'| 0) (= |$b[1][4]'| 0)) (= |$b[2][4]'| 0)) (= |$b[3][4]'| 0)) (= |$b[4][4]'| 0)))) (and (not (= 1 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 1) (= |$b[1][0]'| 1)) (= |$b[2][0]'| 1)) (= |$b[3][0]'| 1)) (= |$b[4][0]'| 1)) (and (and (and (and (= |$b[0][1]'| 1) (= |$b[1][1]'| 1)) (= |$b[2][1]'| 1)) (= |$b[3][1]'| 1)) (= |$b[4][1]'| 1))) (and (and (and (and (= |$b[0][2]'| 1) (= |$b[1][2]'| 1)) (= |$b[2][2]'| 1)) (= |$b[3][2]'| 1)) (= |$b[4][2]'| 1))) (and (and (and (and (= |$b[0][3]'| 1) (= |$b[1][3]'| 1)) (= |$b[2][3]'| 1)) (= |$b[3][3]'| 1)) (= |$b[4][3]'| 1))) (and (and (and (and (= |$b[0][4]'| 1) (= |$b[1][4]'| 1)) (= |$b[2][4]'| 1)) (= |$b[3][4]'| 1)) (= |$b[4][4]'| 1))))) (and (not (= 2 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 2) (= |$b[1][0]'| 2)) (= |$b[2][0]'| 2)) (= |$b[3][0]'| 2)) (= |$b[4][0]'| 2)) (and (and (and (and (= |$b[0][1]'| 2) (= |$b[1][1]'| 2)) (= |$b[2][1]'| 2)) (= |$b[3][1]'| 2)) (= |$b[4][1]'| 2))) (and (and (and (and (= |$b[0][2]'| 2) (= |$b[1][2]'| 2)) (= |$b[2][2]'| 2)) (= |$b[3][2]'| 2)) (= |$b[4][2]'| 2))) (and (and (and (and (= |$b[0][3]'| 2) (= |$b[1][3]'| 2)) (= |$b[2][3]'| 2)) (= |$b[3][3]'| 2)) (= |$b[4][3]'| 2))) (and (and (and (and (= |$b[0][4]'| 2) (= |$b[1][4]'| 2)) (= |$b[2][4]'| 2)) (= |$b[3][4]'| 2)) (= |$b[4][4]'| 2))))) (or (or (and (not (= 0 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 0) (= |$b[0][1]'| 0)) (= |$b[0][2]'| 0)) (= |$b[0][3]'| 0)) (= |$b[0][4]'| 0)) (and (and (and (and (= |$b[1][0]'| 0) (= |$b[1][1]'| 0)) (= |$b[1][2]'| 0)) (= |$b[1][3]'| 0)) (= |$b[1][4]'| 0))) (and (and (and (and (= |$b[2][0]'| 0) (= |$b[2][1]'| 0)) (= |$b[2][2]'| 0)) (= |$b[2][3]'| 0)) (= |$b[2][4]'| 0))) (and (and (and (and (= |$b[3][0]'| 0) (= |$b[3][1]'| 0)) (= |$b[3][2]'| 0)) (= |$b[3][3]'| 0)) (= |$b[3][4]'| 0))) (and (and (and (and (= |$b[4][0]'| 0) (= |$b[4][1]'| 0)) (= |$b[4][2]'| 0)) (= |$b[4][3]'| 0)) (= |$b[4][4]'| 0)))) (and (not (= 1 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 1) (= |$b[0][1]'| 1)) (= |$b[0][2]'| 1)) (= |$b[0][3]'| 1)) (= |$b[0][4]'| 1)) (and (and (and (and (= |$b[1][0]'| 1) (= |$b[1][1]'| 1)) (= |$b[1][2]'| 1)) (= |$b[1][3]'| 1)) (= |$b[1][4]'| 1))) (and (and (and (and (= |$b[2][0]'| 1) (= |$b[2][1]'| 1)) (= |$b[2][2]'| 1)) (= |$b[2][3]'| 1)) (= |$b[2][4]'| 1))) (and (and (and (and (= |$b[3][0]'| 1) (= |$b[3][1]'| 1)) (= |$b[3][2]'| 1)) (= |$b[3][3]'| 1)) (= |$b[3][4]'| 1))) (and (and (and (and (= |$b[4][0]'| 1) (= |$b[4][1]'| 1)) (= |$b[4][2]'| 1)) (= |$b[4][3]'| 1)) (= |$b[4][4]'| 1))))) (and (not (= 2 0)) (or (or (or (or (and (and (and (and (= |$b[0][0]'| 2) (= |$b[0][1]'| 2)) (= |$b[0][2]'| 2)) (= |$b[0][3]'| 2)) (= |$b[0][4]'| 2)) (and (and (and (and (= |$b[1][0]'| 2) (= |$b[1][1]'| 2)) (= |$b[1][2]'| 2)) (= |$b[1][3]'| 2)) (= |$b[1][4]'| 2))) (and (and (and (and (= |$b[2][0]'| 2) (= |$b[2][1]'| 2)) (= |$b[2][2]'| 2)) (= |$b[2][3]'| 2)) (= |$b[2][4]'| 2))) (and (and (and (and (= |$b[3][0]'| 2) (= |$b[3][1]'| 2)) (= |$b[3][2]'| 2)) (= |$b[3][3]'| 2)) (= |$b[3][4]'| 2))) (and (and (and (and (= |$b[4][0]'| 2) (= |$b[4][1]'| 2)) (= |$b[4][2]'| 2)) (= |$b[4][3]'| 2)) (= |$b[4][4]'| 2)))))) (or (or (and (not (= 0 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= 0 0) (= |$b[0][0]'| 0)) (=> (= 0 1) (= |$b[0][1]'| 0))) (=> (= 0 2) (= |$b[0][2]'| 0))) (=> (= 0 3) (= |$b[0][3]'| 0))) (=> (= 0 4) (= |$b[0][4]'| 0))) (=> (= 1 0) (= |$b[1][0]'| 0))) (=> (= 1 1) (= |$b[1][1]'| 0))) (=> (= 1 2) (= |$b[1][2]'| 0))) (=> (= 1 3) (= |$b[1][3]'| 0))) (=> (= 1 4) (= |$b[1][4]'| 0))) (=> (= 2 0) (= |$b[2][0]'| 0))) (=> (= 2 1) (= |$b[2][1]'| 0))) (=> (= 2 2) (= |$b[2][2]'| 0))) (=> (= 2 3) (= |$b[2][3]'| 0))) (=> (= 2 4) (= |$b[2][4]'| 0))) (=> (= 3 0) (= |$b[3][0]'| 0))) (=> (= 3 1) (= |$b[3][1]'| 0))) (=> (= 3 2) (= |$b[3][2]'| 0))) (=> (= 3 3) (= |$b[3][3]'| 0))) (=> (= 3 4) (= |$b[3][4]'| 0))) (=> (= 4 0) (= |$b[4][0]'| 0))) (=> (= 4 1) (= |$b[4][1]'| 0))) (=> (= 4 2) (= |$b[4][2]'| 0))) (=> (= 4 3) (= |$b[4][3]'| 0))) (=> (= 4 4) (= |$b[4][4]'| 0)))) (and (not (= 1 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= 0 0) (= |$b[0][0]'| 1)) (=> (= 0 1) (= |$b[0][1]'| 1))) (=> (= 0 2) (= |$b[0][2]'| 1))) (=> (= 0 3) (= |$b[0][3]'| 1))) (=> (= 0 4) (= |$b[0][4]'| 1))) (=> (= 1 0) (= |$b[1][0]'| 1))) (=> (= 1 1) (= |$b[1][1]'| 1))) (=> (= 1 2) (= |$b[1][2]'| 1))) (=> (= 1 3) (= |$b[1][3]'| 1))) (=> (= 1 4) (= |$b[1][4]'| 1))) (=> (= 2 0) (= |$b[2][0]'| 1))) (=> (= 2 1) (= |$b[2][1]'| 1))) (=> (= 2 2) (= |$b[2][2]'| 1))) (=> (= 2 3) (= |$b[2][3]'| 1))) (=> (= 2 4) (= |$b[2][4]'| 1))) (=> (= 3 0) (= |$b[3][0]'| 1))) (=> (= 3 1) (= |$b[3][1]'| 1))) (=> (= 3 2) (= |$b[3][2]'| 1))) (=> (= 3 3) (= |$b[3][3]'| 1))) (=> (= 3 4) (= |$b[3][4]'| 1))) (=> (= 4 0) (= |$b[4][0]'| 1))) (=> (= 4 1) (= |$b[4][1]'| 1))) (=> (= 4 2) (= |$b[4][2]'| 1))) (=> (= 4 3) (= |$b[4][3]'| 1))) (=> (= 4 4) (= |$b[4][4]'| 1))))) (and (not (= 2 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= 0 0) (= |$b[0][0]'| 2)) (=> (= 0 1) (= |$b[0][1]'| 2))) (=> (= 0 2) (= |$b[0][2]'| 2))) (=> (= 0 3) (= |$b[0][3]'| 2))) (=> (= 0 4) (= |$b[0][4]'| 2))) (=> (= 1 0) (= |$b[1][0]'| 2))) (=> (= 1 1) (= |$b[1][1]'| 2))) (=> (= 1 2) (= |$b[1][2]'| 2))) (=> (= 1 3) (= |$b[1][3]'| 2))) (=> (= 1 4) (= |$b[1][4]'| 2))) (=> (= 2 0) (= |$b[2][0]'| 2))) (=> (= 2 1) (= |$b[2][1]'| 2))) (=> (= 2 2) (= |$b[2][2]'| 2))) (=> (= 2 3) (= |$b[2][3]'| 2))) (=> (= 2 4) (= |$b[2][4]'| 2))) (=> (= 3 0) (= |$b[3][0]'| 2))) (=> (= 3 1) (= |$b[3][1]'| 2))) (=> (= 3 2) (= |$b[3][2]'| 2))) (=> (= 3 3) (= |$b[3][3]'| 2))) (=> (= 3 4) (= |$b[3][4]'| 2))) (=> (= 4 0) (= |$b[4][0]'| 2))) (=> (= 4 1) (= |$b[4][1]'| 2))) (=> (= 4 2) (= |$b[4][2]'| 2))) (=> (= 4 3) (= |$b[4][3]'| 2))) (=> (= 4 4) (= |$b[4][4]'| 2)))))) (or (or (and (not (= 0 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= (+ 0 0) (- 5 1)) (= |$b[0][0]'| 0)) (=> (= (+ 0 1) (- 5 1)) (= |$b[0][1]'| 0))) (=> (= (+ 0 2) (- 5 1)) (= |$b[0][2]'| 0))) (=> (= (+ 0 3) (- 5 1)) (= |$b[0][3]'| 0))) (=> (= (+ 0 4) (- 5 1)) (= |$b[0][4]'| 0))) (=> (= (+ 1 0) (- 5 1)) (= |$b[1][0]'| 0))) (=> (= (+ 1 1) (- 5 1)) (= |$b[1][1]'| 0))) (=> (= (+ 1 2) (- 5 1)) (= |$b[1][2]'| 0))) (=> (= (+ 1 3) (- 5 1)) (= |$b[1][3]'| 0))) (=> (= (+ 1 4) (- 5 1)) (= |$b[1][4]'| 0))) (=> (= (+ 2 0) (- 5 1)) (= |$b[2][0]'| 0))) (=> (= (+ 2 1) (- 5 1)) (= |$b[2][1]'| 0))) (=> (= (+ 2 2) (- 5 1)) (= |$b[2][2]'| 0))) (=> (= (+ 2 3) (- 5 1)) (= |$b[2][3]'| 0))) (=> (= (+ 2 4) (- 5 1)) (= |$b[2][4]'| 0))) (=> (= (+ 3 0) (- 5 1)) (= |$b[3][0]'| 0))) (=> (= (+ 3 1) (- 5 1)) (= |$b[3][1]'| 0))) (=> (= (+ 3 2) (- 5 1)) (= |$b[3][2]'| 0))) (=> (= (+ 3 3) (- 5 1)) (= |$b[3][3]'| 0))) (=> (= (+ 3 4) (- 5 1)) (= |$b[3][4]'| 0))) (=> (= (+ 4 0) (- 5 1)) (= |$b[4][0]'| 0))) (=> (= (+ 4 1) (- 5 1)) (= |$b[4][1]'| 0))) (=> (= (+ 4 2) (- 5 1)) (= |$b[4][2]'| 0))) (=> (= (+ 4 3) (- 5 1)) (= |$b[4][3]'| 0))) (=> (= (+ 4 4) (- 5 1)) (= |$b[4][4]'| 0)))) (and (not (= 1 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= (+ 0 0) (- 5 1)) (= |$b[0][0]'| 1)) (=> (= (+ 0 1) (- 5 1)) (= |$b[0][1]'| 1))) (=> (= (+ 0 2) (- 5 1)) (= |$b[0][2]'| 1))) (=> (= (+ 0 3) (- 5 1)) (= |$b[0][3]'| 1))) (=> (= (+ 0 4) (- 5 1)) (= |$b[0][4]'| 1))) (=> (= (+ 1 0) (- 5 1)) (= |$b[1][0]'| 1))) (=> (= (+ 1 1) (- 5 1)) (= |$b[1][1]'| 1))) (=> (= (+ 1 2) (- 5 1)) (= |$b[1][2]'| 1))) (=> (= (+ 1 3) (- 5 1)) (= |$b[1][3]'| 1))) (=> (= (+ 1 4) (- 5 1)) (= |$b[1][4]'| 1))) (=> (= (+ 2 0) (- 5 1)) (= |$b[2][0]'| 1))) (=> (= (+ 2 1) (- 5 1)) (= |$b[2][1]'| 1))) (=> (= (+ 2 2) (- 5 1)) (= |$b[2][2]'| 1))) (=> (= (+ 2 3) (- 5 1)) (= |$b[2][3]'| 1))) (=> (= (+ 2 4) (- 5 1)) (= |$b[2][4]'| 1))) (=> (= (+ 3 0) (- 5 1)) (= |$b[3][0]'| 1))) (=> (= (+ 3 1) (- 5 1)) (= |$b[3][1]'| 1))) (=> (= (+ 3 2) (- 5 1)) (= |$b[3][2]'| 1))) (=> (= (+ 3 3) (- 5 1)) (= |$b[3][3]'| 1))) (=> (= (+ 3 4) (- 5 1)) (= |$b[3][4]'| 1))) (=> (= (+ 4 0) (- 5 1)) (= |$b[4][0]'| 1))) (=> (= (+ 4 1) (- 5 1)) (= |$b[4][1]'| 1))) (=> (= (+ 4 2) (- 5 1)) (= |$b[4][2]'| 1))) (=> (= (+ 4 3) (- 5 1)) (= |$b[4][3]'| 1))) (=> (= (+ 4 4) (- 5 1)) (= |$b[4][4]'| 1))))) (and (not (= 2 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> (= (+ 0 0) (- 5 1)) (= |$b[0][0]'| 2)) (=> (= (+ 0 1) (- 5 1)) (= |$b[0][1]'| 2))) (=> (= (+ 0 2) (- 5 1)) (= |$b[0][2]'| 2))) (=> (= (+ 0 3) (- 5 1)) (= |$b[0][3]'| 2))) (=> (= (+ 0 4) (- 5 1)) (= |$b[0][4]'| 2))) (=> (= (+ 1 0) (- 5 1)) (= |$b[1][0]'| 2))) (=> (= (+ 1 1) (- 5 1)) (= |$b[1][1]'| 2))) (=> (= (+ 1 2) (- 5 1)) (= |$b[1][2]'| 2))) (=> (= (+ 1 3) (- 5 1)) (= |$b[1][3]'| 2))) (=> (= (+ 1 4) (- 5 1)) (= |$b[1][4]'| 2))) (=> (= (+ 2 0) (- 5 1)) (= |$b[2][0]'| 2))) (=> (= (+ 2 1) (- 5 1)) (= |$b[2][1]'| 2))) (=> (= (+ 2 2) (- 5 1)) (= |$b[2][2]'| 2))) (=> (= (+ 2 3) (- 5 1)) (= |$b[2][3]'| 2))) (=> (= (+ 2 4) (- 5 1)) (= |$b[2][4]'| 2))) (=> (= (+ 3 0) (- 5 1)) (= |$b[3][0]'| 2))) (=> (= (+ 3 1) (- 5 1)) (= |$b[3][1]'| 2))) (=> (= (+ 3 2) (- 5 1)) (= |$b[3][2]'| 2))) (=> (= (+ 3 3) (- 5 1)) (= |$b[3][3]'| 2))) (=> (= (+ 3 4) (- 5 1)) (= |$b[3][4]'| 2))) (=> (= (+ 4 0) (- 5 1)) (= |$b[4][0]'| 2))) (=> (= (+ 4 1) (- 5 1)) (= |$b[4][1]'| 2))) (=> (= (+ 4 2) (- 5 1)) (= |$b[4][2]'| 2))) (=> (= (+ 4 3) (- 5 1)) (= |$b[4][3]'| 2))) (=> (= (+ 4 4) (- 5 1)) (= |$b[4][4]'| 2))))))) |$game_complete'| (not |$game_complete'|))) (= |$global_always~3.holds'| (and |$global_always~3.a'| (or %init $global_always~3.holds))) (= |$global_always~4.a'| (=> |$game_complete'| (<= (- (* 2 5) 1) (+ (+ (+ (+ (+ (+ (+ (+ (ite (not (= |$b[0][0]'| 0)) 1 0) (ite (not (= |$b[0][1]'| 0)) 1 0)) (ite (not (= |$b[0][2]'| 0)) 1 0)) (ite (not (= |$b[0][3]'| 0)) 1 0)) (ite (not (= |$b[0][4]'| 0)) 1 0)) (+ (+ (+ (+ (ite (not (= |$b[1][0]'| 0)) 1 0) (ite (not (= |$b[1][1]'| 0)) 1 0)) (ite (not (= |$b[1][2]'| 0)) 1 0)) (ite (not (= |$b[1][3]'| 0)) 1 0)) (ite (not (= |$b[1][4]'| 0)) 1 0))) (+ (+ (+ (+ (ite (not (= |$b[2][0]'| 0)) 1 0) (ite (not (= |$b[2][1]'| 0)) 1 0)) (ite (not (= |$b[2][2]'| 0)) 1 0)) (ite (not (= |$b[2][3]'| 0)) 1 0)) (ite (not (= |$b[2][4]'| 0)) 1 0))) (+ (+ (+ (+ (ite (not (= |$b[3][0]'| 0)) 1 0) (ite (not (= |$b[3][1]'| 0)) 1 0)) (ite (not (= |$b[3][2]'| 0)) 1 0)) (ite (not (= |$b[3][3]'| 0)) 1 0)) (ite (not (= |$b[3][4]'| 0)) 1 0))) (+ (+ (+ (+ (ite (not (= |$b[4][0]'| 0)) 1 0) (ite (not (= |$b[4][1]'| 0)) 1 0)) (ite (not (= |$b[4][2]'| 0)) 1 0)) (ite (not (= |$b[4][3]'| 0)) 1 0)) (ite (not (= |$b[4][4]'| 0)) 1 0)))))) (= |$global_always~4.holds'| (and |$global_always~4.a'| (or %init $global_always~4.holds))) (= |$H~0.a'| (and (and (and (and (and |$initial~0.holds'| |$initial~1.holds'|) |$global_always~0.holds'|) |$global_always~1.holds'|) |$global_always~2.holds'|) |$global_always~3.holds'|)) (= |$H~0.holds'| (and |$H~0.a'| |$H~0.Z~0.holds'|)) (= |$H~0.Z~0.holds'| (or %init $H~0.holds)) (<= 0 |$b[0][0]|) (<= |$b[0][0]| 2) (<= 0 |$b[0][0]'|) (<= |$b[0][0]'| 2) (<= 0 |$b[0][1]|) (<= |$b[0][1]| 2) (<= 0 |$b[0][1]'|) (<= |$b[0][1]'| 2) (<= 0 |$b[0][2]|) (<= |$b[0][2]| 2) (<= 0 |$b[0][2]'|) (<= |$b[0][2]'| 2) (<= 0 |$b[0][3]|) (<= |$b[0][3]| 2) (<= 0 |$b[0][3]'|) (<= |$b[0][3]'| 2) (<= 0 |$b[0][4]|) (<= |$b[0][4]| 2) (<= 0 |$b[0][4]'|) (<= |$b[0][4]'| 2) (<= 0 |$b[1][0]|) (<= |$b[1][0]| 2) (<= 0 |$b[1][0]'|) (<= |$b[1][0]'| 2) (<= 0 |$b[1][1]|) (<= |$b[1][1]| 2) (<= 0 |$b[1][1]'|) (<= |$b[1][1]'| 2) (<= 0 |$b[1][2]|) (<= |$b[1][2]| 2) (<= 0 |$b[1][2]'|) (<= |$b[1][2]'| 2) (<= 0 |$b[1][3]|) (<= |$b[1][3]| 2) (<= 0 |$b[1][3]'|) (<= |$b[1][3]'| 2) (<= 0 |$b[1][4]|) (<= |$b[1][4]| 2) (<= 0 |$b[1][4]'|) (<= |$b[1][4]'| 2) (<= 0 |$b[2][0]|) (<= |$b[2][0]| 2) (<= 0 |$b[2][0]'|) (<= |$b[2][0]'| 2) (<= 0 |$b[2][1]|) (<= |$b[2][1]| 2) (<= 0 |$b[2][1]'|) (<= |$b[2][1]'| 2) (<= 0 |$b[2][2]|) (<= |$b[2][2]| 2) (<= 0 |$b[2][2]'|) (<= |$b[2][2]'| 2) (<= 0 |$b[2][3]|) (<= |$b[2][3]| 2) (<= 0 |$b[2][3]'|) (<= |$b[2][3]'| 2) (<= 0 |$b[2][4]|) (<= |$b[2][4]| 2) (<= 0 |$b[2][4]'|) (<= |$b[2][4]'| 2) (<= 0 |$b[3][0]|) (<= |$b[3][0]| 2) (<= 0 |$b[3][0]'|) (<= |$b[3][0]'| 2) (<= 0 |$b[3][1]|) (<= |$b[3][1]| 2) (<= 0 |$b[3][1]'|) (<= |$b[3][1]'| 2) (<= 0 |$b[3][2]|) (<= |$b[3][2]| 2) (<= 0 |$b[3][2]'|) (<= |$b[3][2]'| 2) (<= 0 |$b[3][3]|) (<= |$b[3][3]| 2) (<= 0 |$b[3][3]'|) (<= |$b[3][3]'| 2) (<= 0 |$b[3][4]|) (<= |$b[3][4]| 2) (<= 0 |$b[3][4]'|) (<= |$b[3][4]'| 2) (<= 0 |$b[4][0]|) (<= |$b[4][0]| 2) (<= 0 |$b[4][0]'|) (<= |$b[4][0]'| 2) (<= 0 |$b[4][1]|) (<= |$b[4][1]| 2) (<= 0 |$b[4][1]'|) (<= |$b[4][1]'| 2) (<= 0 |$b[4][2]|) (<= |$b[4][2]| 2) (<= 0 |$b[4][2]'|) (<= |$b[4][2]'| 2) (<= 0 |$b[4][3]|) (<= |$b[4][3]| 2) (<= 0 |$b[4][3]'|) (<= |$b[4][3]'| 2) (<= 0 |$b[4][4]|) (<= |$b[4][4]| 2) (<= 0 |$b[4][4]'|) (<= |$b[4][4]'| 2) (<= 0 $p) (<= $p 1) (<= 0 |$p'|) (<= |$p'| 1) (<= 0 $m.x) (<= $m.x 4) (<= 0 |$m.x'|) (<= |$m.x'| 4) (<= 0 $m.y) (<= $m.y 4) (<= 0 |$m.y'|) (<= |$m.y'| 4) (not |%init'|)))
(assert (! (T |$b[0][0]-| |$b[0][1]-| |$b[0][2]-| |$b[0][3]-| |$b[0][4]-| |$b[1][0]-| |$b[1][1]-| |$b[1][2]-| |$b[1][3]-| |$b[1][4]-| |$b[2][0]-| |$b[2][1]-| |$b[2][2]-| |$b[2][3]-| |$b[2][4]-| |$b[3][0]-| |$b[3][1]-| |$b[3][2]-| |$b[3][3]-| |$b[3][4]-| |$b[4][0]-| |$b[4][1]-| |$b[4][2]-| |$b[4][3]-| |$b[4][4]-| $p- $m.x- $m.y- $game_complete- $low_turn_bound- $initial~0.a- $initial~0.holds- $initial~1.a- $initial~1.holds- $global_always~0.a- $global_always~0.holds- $global_always~1.a- $global_always~1.holds- $global_always~2.a- $global_always~2.holds- $global_always~3.a- $global_always~3.holds- $global_always~4.a- $global_always~4.holds- $H~0.a- $H~0.holds- $H~0.Z~0.holds- %init- |$b[0][0]-'| |$b[0][1]-'| |$b[0][2]-'| |$b[0][3]-'| |$b[0][4]-'| |$b[1][0]-'| |$b[1][1]-'| |$b[1][2]-'| |$b[1][3]-'| |$b[1][4]-'| |$b[2][0]-'| |$b[2][1]-'| |$b[2][2]-'| |$b[2][3]-'| |$b[2][4]-'| |$b[3][0]-'| |$b[3][1]-'| |$b[3][2]-'| |$b[3][3]-'| |$b[3][4]-'| |$b[4][0]-'| |$b[4][1]-'| |$b[4][2]-'| |$b[4][3]-'| |$b[4][4]-'| |$p-'| |$m.x-'| |$m.y-'| |$game_complete-'| |$low_turn_bound-'| |$initial~0.a-'| |$initial~0.holds-'| |$initial~1.a-'| |$initial~1.holds-'| |$global_always~0.a-'| |$global_always~0.holds-'| |$global_always~1.a-'| |$global_always~1.holds-'| |$global_always~2.a-'| |$global_always~2.holds-'| |$global_always~3.a-'| |$global_always~3.holds-'| |$global_always~4.a-'| |$global_always~4.holds-'| |$H~0.a-'| |$H~0.holds-'| |$H~0.Z~0.holds-'| |%init-'|) :named abstract0))
(assert (! (= %init %init-) :named abstract1))
(assert (! (= |%init-'| |%init'|) :named abstract2))
(assert (! (= $low_turn_bound $low_turn_bound-) :named abstract3))
(assert (! (= |$low_turn_bound-'| |$low_turn_bound'|) :named abstract4))
(push 1)
(assert (and %init (not (or $low_turn_bound %init))))
(check-sat)
(pop 1)
(push 1)
(assert (not (or $low_turn_bound %init)))
(check-sat)
(pop 1)
(push 1)
(assert (and (not $low_turn_bound) (not %init)))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not $low_turn_bound) (not %init))))
(assert (! %init :named F0))
(assert (! true :named F1))
(assert true)
(assert (! (not |$low_turn_bound'|) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert %init)
(assert (! %init :named F0))
(assert (! true :named F1))
(assert true)
(assert (! (not |%init'|) :named P0))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (and (not $low_turn_bound) (not %init))) (not (or $low_turn_bound %init))))
(check-sat)
(pop 1)
(push 1)
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert true)
(assert (! (not |$low_turn_bound'|) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (not (or $low_turn_bound %init)))
(check-sat)
(pop 1)
(push 1)
(assert (and (not $low_turn_bound) (not %init)))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not $low_turn_bound) (not %init))))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert true)
(assert (! (not |$low_turn_bound'|) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (and $low_turn_bound (not %init) (not (and (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and $low_turn_bound (not %init))))
(assert (! %init :named F0))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert true)
(assert (! |$low_turn_bound'| :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(declare-fun |$b[0][0]$~1| () Int)
(declare-fun |$b[0][1]$~1| () Int)
(declare-fun |$b[0][2]$~1| () Int)
(declare-fun |$b[0][3]$~1| () Int)
(declare-fun |$b[0][4]$~1| () Int)
(declare-fun |$b[1][0]$~1| () Int)
(declare-fun |$b[1][1]$~1| () Int)
(declare-fun |$b[1][2]$~1| () Int)
(declare-fun |$b[1][3]$~1| () Int)
(declare-fun |$b[1][4]$~1| () Int)
(declare-fun |$b[2][0]$~1| () Int)
(declare-fun |$b[2][1]$~1| () Int)
(declare-fun |$b[2][2]$~1| () Int)
(declare-fun |$b[2][3]$~1| () Int)
(declare-fun |$b[2][4]$~1| () Int)
(declare-fun |$b[3][0]$~1| () Int)
(declare-fun |$b[3][1]$~1| () Int)
(declare-fun |$b[3][2]$~1| () Int)
(declare-fun |$b[3][3]$~1| () Int)
(declare-fun |$b[3][4]$~1| () Int)
(declare-fun |$b[4][0]$~1| () Int)
(declare-fun |$b[4][1]$~1| () Int)
(declare-fun |$b[4][2]$~1| () Int)
(declare-fun |$b[4][3]$~1| () Int)
(declare-fun |$b[4][4]$~1| () Int)
(declare-fun $p$~1 () Int)
(declare-fun $m.x$~1 () Int)
(declare-fun $m.y$~1 () Int)
(declare-fun $game_complete$~1 () Bool)
(declare-fun $low_turn_bound$~1 () Bool)
(declare-fun $initial~0.a$~1 () Bool)
(declare-fun $initial~0.holds$~1 () Bool)
(declare-fun $initial~1.a$~1 () Bool)
(declare-fun $initial~1.holds$~1 () Bool)
(declare-fun $global_always~0.a$~1 () Bool)
(declare-fun $global_always~0.holds$~1 () Bool)
(declare-fun $global_always~1.a$~1 () Bool)
(declare-fun $global_always~1.holds$~1 () Bool)
(declare-fun $global_always~2.a$~1 () Bool)
(declare-fun $global_always~2.holds$~1 () Bool)
(declare-fun $global_always~3.a$~1 () Bool)
(declare-fun $global_always~3.holds$~1 () Bool)
(declare-fun $global_always~4.a$~1 () Bool)
(declare-fun $global_always~4.holds$~1 () Bool)
(declare-fun $H~0.a$~1 () Bool)
(declare-fun $H~0.holds$~1 () Bool)
(declare-fun $H~0.Z~0.holds$~1 () Bool)
(declare-fun %init$~1 () Bool)
(declare-fun |$b[0][0]$0| () Int)
(declare-fun |$b[0][1]$0| () Int)
(declare-fun |$b[0][2]$0| () Int)
(declare-fun |$b[0][3]$0| () Int)
(declare-fun |$b[0][4]$0| () Int)
(declare-fun |$b[1][0]$0| () Int)
(declare-fun |$b[1][1]$0| () Int)
(declare-fun |$b[1][2]$0| () Int)
(declare-fun |$b[1][3]$0| () Int)
(declare-fun |$b[1][4]$0| () Int)
(declare-fun |$b[2][0]$0| () Int)
(declare-fun |$b[2][1]$0| () Int)
(declare-fun |$b[2][2]$0| () Int)
(declare-fun |$b[2][3]$0| () Int)
(declare-fun |$b[2][4]$0| () Int)
(declare-fun |$b[3][0]$0| () Int)
(declare-fun |$b[3][1]$0| () Int)
(declare-fun |$b[3][2]$0| () Int)
(declare-fun |$b[3][3]$0| () Int)
(declare-fun |$b[3][4]$0| () Int)
(declare-fun |$b[4][0]$0| () Int)
(declare-fun |$b[4][1]$0| () Int)
(declare-fun |$b[4][2]$0| () Int)
(declare-fun |$b[4][3]$0| () Int)
(declare-fun |$b[4][4]$0| () Int)
(declare-fun $p$0 () Int)
(declare-fun $m.x$0 () Int)
(declare-fun $m.y$0 () Int)
(declare-fun $game_complete$0 () Bool)
(declare-fun $low_turn_bound$0 () Bool)
(declare-fun $initial~0.a$0 () Bool)
(declare-fun $initial~0.holds$0 () Bool)
(declare-fun $initial~1.a$0 () Bool)
(declare-fun $initial~1.holds$0 () Bool)
(declare-fun $global_always~0.a$0 () Bool)
(declare-fun $global_always~0.holds$0 () Bool)
(declare-fun $global_always~1.a$0 () Bool)
(declare-fun $global_always~1.holds$0 () Bool)
(declare-fun $global_always~2.a$0 () Bool)
(declare-fun $global_always~2.holds$0 () Bool)
(declare-fun $global_always~3.a$0 () Bool)
(declare-fun $global_always~3.holds$0 () Bool)
(declare-fun $global_always~4.a$0 () Bool)
(declare-fun $global_always~4.holds$0 () Bool)
(declare-fun $H~0.a$0 () Bool)
(declare-fun $H~0.holds$0 () Bool)
(declare-fun $H~0.Z~0.holds$0 () Bool)
(declare-fun %init$0 () Bool)
(declare-fun |$b[0][0]$1| () Int)
(declare-fun |$b[0][1]$1| () Int)
(declare-fun |$b[0][2]$1| () Int)
(declare-fun |$b[0][3]$1| () Int)
(declare-fun |$b[0][4]$1| () Int)
(declare-fun |$b[1][0]$1| () Int)
(declare-fun |$b[1][1]$1| () Int)
(declare-fun |$b[1][2]$1| () Int)
(declare-fun |$b[1][3]$1| () Int)
(declare-fun |$b[1][4]$1| () Int)
(declare-fun |$b[2][0]$1| () Int)
(declare-fun |$b[2][1]$1| () Int)
(declare-fun |$b[2][2]$1| () Int)
(declare-fun |$b[2][3]$1| () Int)
(declare-fun |$b[2][4]$1| () Int)
(declare-fun |$b[3][0]$1| () Int)
(declare-fun |$b[3][1]$1| () Int)
(declare-fun |$b[3][2]$1| () Int)
(declare-fun |$b[3][3]$1| () Int)
(declare-fun |$b[3][4]$1| () Int)
(declare-fun |$b[4][0]$1| () Int)
(declare-fun |$b[4][1]$1| () Int)
(declare-fun |$b[4][2]$1| () Int)
(declare-fun |$b[4][3]$1| () Int)
(declare-fun |$b[4][4]$1| () Int)
(declare-fun $p$1 () Int)
(declare-fun $m.x$1 () Int)
(declare-fun $m.y$1 () Int)
(declare-fun $game_complete$1 () Bool)
(declare-fun $low_turn_bound$1 () Bool)
(declare-fun $initial~0.a$1 () Bool)
(declare-fun $initial~0.holds$1 () Bool)
(declare-fun $initial~1.a$1 () Bool)
(declare-fun $initial~1.holds$1 () Bool)
(declare-fun $global_always~0.a$1 () Bool)
(declare-fun $global_always~0.holds$1 () Bool)
(declare-fun $global_always~1.a$1 () Bool)
(declare-fun $global_always~1.holds$1 () Bool)
(declare-fun $global_always~2.a$1 () Bool)
(declare-fun $global_always~2.holds$1 () Bool)
(declare-fun $global_always~3.a$1 () Bool)
(declare-fun $global_always~3.holds$1 () Bool)
(declare-fun $global_always~4.a$1 () Bool)
(declare-fun $global_always~4.holds$1 () Bool)
(declare-fun $H~0.a$1 () Bool)
(declare-fun $H~0.holds$1 () Bool)
(declare-fun $H~0.Z~0.holds$1 () Bool)
(declare-fun %init$1 () Bool)
(push 1)
(assert (! (and (not $low_turn_bound$~1) %init$~1 (T |$b[0][0]$~1| |$b[0][1]$~1| |$b[0][2]$~1| |$b[0][3]$~1| |$b[0][4]$~1| |$b[1][0]$~1| |$b[1][1]$~1| |$b[1][2]$~1| |$b[1][3]$~1| |$b[1][4]$~1| |$b[2][0]$~1| |$b[2][1]$~1| |$b[2][2]$~1| |$b[2][3]$~1| |$b[2][4]$~1| |$b[3][0]$~1| |$b[3][1]$~1| |$b[3][2]$~1| |$b[3][3]$~1| |$b[3][4]$~1| |$b[4][0]$~1| |$b[4][1]$~1| |$b[4][2]$~1| |$b[4][3]$~1| |$b[4][4]$~1| $p$~1 $m.x$~1 $m.y$~1 $game_complete$~1 $low_turn_bound$~1 $initial~0.a$~1 $initial~0.holds$~1 $initial~1.a$~1 $initial~1.holds$~1 $global_always~0.a$~1 $global_always~0.holds$~1 $global_always~1.a$~1 $global_always~1.holds$~1 $global_always~2.a$~1 $global_always~2.holds$~1 $global_always~3.a$~1 $global_always~3.holds$~1 $global_always~4.a$~1 $global_always~4.holds$~1 $H~0.a$~1 $H~0.holds$~1 $H~0.Z~0.holds$~1 %init$~1 |$b[0][0]$0| |$b[0][1]$0| |$b[0][2]$0| |$b[0][3]$0| |$b[0][4]$0| |$b[1][0]$0| |$b[1][1]$0| |$b[1][2]$0| |$b[1][3]$0| |$b[1][4]$0| |$b[2][0]$0| |$b[2][1]$0| |$b[2][2]$0| |$b[2][3]$0| |$b[2][4]$0| |$b[3][0]$0| |$b[3][1]$0| |$b[3][2]$0| |$b[3][3]$0| |$b[3][4]$0| |$b[4][0]$0| |$b[4][1]$0| |$b[4][2]$0| |$b[4][3]$0| |$b[4][4]$0| $p$0 $m.x$0 $m.y$0 $game_complete$0 $low_turn_bound$0 $initial~0.a$0 $initial~0.holds$0 $initial~1.a$0 $initial~1.holds$0 $global_always~0.a$0 $global_always~0.holds$0 $global_always~1.a$0 $global_always~1.holds$0 $global_always~2.a$0 $global_always~2.holds$0 $global_always~3.a$0 $global_always~3.holds$0 $global_always~4.a$0 $global_always~4.holds$0 $H~0.a$0 $H~0.holds$0 $H~0.Z~0.holds$0 %init$0)) :named I0))
(assert (! (and $low_turn_bound$0 (not %init$0) (T |$b[0][0]$0| |$b[0][1]$0| |$b[0][2]$0| |$b[0][3]$0| |$b[0][4]$0| |$b[1][0]$0| |$b[1][1]$0| |$b[1][2]$0| |$b[1][3]$0| |$b[1][4]$0| |$b[2][0]$0| |$b[2][1]$0| |$b[2][2]$0| |$b[2][3]$0| |$b[2][4]$0| |$b[3][0]$0| |$b[3][1]$0| |$b[3][2]$0| |$b[3][3]$0| |$b[3][4]$0| |$b[4][0]$0| |$b[4][1]$0| |$b[4][2]$0| |$b[4][3]$0| |$b[4][4]$0| $p$0 $m.x$0 $m.y$0 $game_complete$0 $low_turn_bound$0 $initial~0.a$0 $initial~0.holds$0 $initial~1.a$0 $initial~1.holds$0 $global_always~0.a$0 $global_always~0.holds$0 $global_always~1.a$0 $global_always~1.holds$0 $global_always~2.a$0 $global_always~2.holds$0 $global_always~3.a$0 $global_always~3.holds$0 $global_always~4.a$0 $global_always~4.holds$0 $H~0.a$0 $H~0.holds$0 $H~0.Z~0.holds$0 %init$0 |$b[0][0]$1| |$b[0][1]$1| |$b[0][2]$1| |$b[0][3]$1| |$b[0][4]$1| |$b[1][0]$1| |$b[1][1]$1| |$b[1][2]$1| |$b[1][3]$1| |$b[1][4]$1| |$b[2][0]$1| |$b[2][1]$1| |$b[2][2]$1| |$b[2][3]$1| |$b[2][4]$1| |$b[3][0]$1| |$b[3][1]$1| |$b[3][2]$1| |$b[3][3]$1| |$b[3][4]$1| |$b[4][0]$1| |$b[4][1]$1| |$b[4][2]$1| |$b[4][3]$1| |$b[4][4]$1| $p$1 $m.x$1 $m.y$1 $game_complete$1 $low_turn_bound$1 $initial~0.a$1 $initial~0.holds$1 $initial~1.a$1 $initial~1.holds$1 $global_always~0.a$1 $global_always~0.holds$1 $global_always~1.a$1 $global_always~1.holds$1 $global_always~2.a$1 $global_always~2.holds$1 $global_always~3.a$1 $global_always~3.holds$1 $global_always~4.a$1 $global_always~4.holds$1 $H~0.a$1 $H~0.holds$1 $H~0.Z~0.holds$1 %init$1)) :named I1))
(assert (! (and (not $low_turn_bound$1) (not %init$1) (not (or $low_turn_bound$1 %init$1))) :named I2))
(check-sat)
(pop 1)
(assert (! (= (<= |$b[0][3]| 0) (<= |$b[0][3]-| 0)) :named abstract5))
(assert (! (= (<= |$b[0][3]-'| 0) (<= |$b[0][3]'| 0)) :named abstract6))
(assert (! (= $H~0.holds $H~0.holds-) :named abstract7))
(assert (! (= |$H~0.holds-'| |$H~0.holds'|) :named abstract8))
(assert (! (= (<= |$b[2][1]| 0) (<= |$b[2][1]-| 0)) :named abstract9))
(assert (! (= (<= |$b[2][1]-'| 0) (<= |$b[2][1]'| 0)) :named abstract10))
(assert (! (= (<= 0 (+ $p (- 1))) (<= 0 (+ $p- (- 1)))) :named abstract11))
(assert (! (= (<= 0 (+ |$p-'| (- 1))) (<= 0 (+ |$p'| (- 1)))) :named abstract12))
(assert (! (= (<= |$b[2][0]| 0) (<= |$b[2][0]-| 0)) :named abstract13))
(assert (! (= (<= |$b[2][0]-'| 0) (<= |$b[2][0]'| 0)) :named abstract14))
(assert (! (= (<= |$b[2][4]| 0) (<= |$b[2][4]-| 0)) :named abstract15))
(assert (! (= (<= |$b[2][4]-'| 0) (<= |$b[2][4]'| 0)) :named abstract16))
(assert (! (= (<= |$b[3][3]| 0) (<= |$b[3][3]-| 0)) :named abstract17))
(assert (! (= (<= |$b[3][3]-'| 0) (<= |$b[3][3]'| 0)) :named abstract18))
(assert (! (= (<= |$b[3][0]| 0) (<= |$b[3][0]-| 0)) :named abstract19))
(assert (! (= (<= |$b[3][0]-'| 0) (<= |$b[3][0]'| 0)) :named abstract20))
(assert (! (= (<= |$b[1][3]| 0) (<= |$b[1][3]-| 0)) :named abstract21))
(assert (! (= (<= |$b[1][3]-'| 0) (<= |$b[1][3]'| 0)) :named abstract22))
(assert (! (= (<= |$b[4][2]| 0) (<= |$b[4][2]-| 0)) :named abstract23))
(assert (! (= (<= |$b[4][2]-'| 0) (<= |$b[4][2]'| 0)) :named abstract24))
(assert (! (= (<= |$b[0][0]| 0) (<= |$b[0][0]-| 0)) :named abstract25))
(assert (! (= (<= |$b[0][0]-'| 0) (<= |$b[0][0]'| 0)) :named abstract26))
(assert (! (= (<= |$b[1][1]| 0) (<= |$b[1][1]-| 0)) :named abstract27))
(assert (! (= (<= |$b[1][1]-'| 0) (<= |$b[1][1]'| 0)) :named abstract28))
(assert (! (= (<= |$b[2][3]| 0) (<= |$b[2][3]-| 0)) :named abstract29))
(assert (! (= (<= |$b[2][3]-'| 0) (<= |$b[2][3]'| 0)) :named abstract30))
(assert (! (= (<= |$b[1][0]| 0) (<= |$b[1][0]-| 0)) :named abstract31))
(assert (! (= (<= |$b[1][0]-'| 0) (<= |$b[1][0]'| 0)) :named abstract32))
(assert (! (= (<= |$b[2][2]| 0) (<= |$b[2][2]-| 0)) :named abstract33))
(assert (! (= (<= |$b[2][2]-'| 0) (<= |$b[2][2]'| 0)) :named abstract34))
(assert (! (= $global_always~4.holds $global_always~4.holds-) :named abstract35))
(assert (! (= |$global_always~4.holds-'| |$global_always~4.holds'|) :named abstract36))
(assert (! (= (<= |$b[0][2]| 0) (<= |$b[0][2]-| 0)) :named abstract37))
(assert (! (= (<= |$b[0][2]-'| 0) (<= |$b[0][2]'| 0)) :named abstract38))
(assert (! (= (<= |$b[0][1]| 0) (<= |$b[0][1]-| 0)) :named abstract39))
(assert (! (= (<= |$b[0][1]-'| 0) (<= |$b[0][1]'| 0)) :named abstract40))
(assert (! (= (<= |$b[1][4]| 0) (<= |$b[1][4]-| 0)) :named abstract41))
(assert (! (= (<= |$b[1][4]-'| 0) (<= |$b[1][4]'| 0)) :named abstract42))
(assert (! (= (<= |$b[4][1]| 0) (<= |$b[4][1]-| 0)) :named abstract43))
(assert (! (= (<= |$b[4][1]-'| 0) (<= |$b[4][1]'| 0)) :named abstract44))
(assert (! (= (<= |$b[3][1]| 0) (<= |$b[3][1]-| 0)) :named abstract45))
(assert (! (= (<= |$b[3][1]-'| 0) (<= |$b[3][1]'| 0)) :named abstract46))
(assert (! (= (<= |$b[4][0]| 0) (<= |$b[4][0]-| 0)) :named abstract47))
(assert (! (= (<= |$b[4][0]-'| 0) (<= |$b[4][0]'| 0)) :named abstract48))
(push 1)
(assert (not (or $low_turn_bound %init)))
(check-sat)
(pop 1)
(push 1)
(assert (and (<= |$b[0][3]| 0) (not $H~0.holds) (not (<= |$b[2][1]| 0)) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (<= |$b[3][0]| 0) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (not (<= |$b[0][0]| 0)) (<= |$b[1][1]| 0) (<= |$b[2][3]| 0) (not (<= |$b[1][0]| 0)) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (<= |$b[3][1]| 0) (not (<= |$b[4][0]| 0))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (<= |$b[0][3]| 0) (not $H~0.holds) (not (<= |$b[2][1]| 0)) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (<= |$b[3][0]| 0) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (not (<= |$b[0][0]| 0)) (<= |$b[1][1]| 0) (<= |$b[2][3]| 0) (not (<= |$b[1][0]| 0)) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (<= |$b[3][1]| 0) (not (<= |$b[4][0]| 0)))))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert true)
(assert (! (<= |$b[0][3]'| 0) :named P0))
(assert (! (not |$H~0.holds'|) :named P1))
(assert (! (not (<= |$b[2][1]'| 0)) :named P2))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (<= |$b[3][0]'| 0) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (<= |$b[4][2]'| 0) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (not (<= |$b[0][0]'| 0)) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (<= |$b[2][3]'| 0) :named P14))
(assert (! (not (<= |$b[1][0]'| 0)) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (<= |$b[0][1]'| 0) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (<= |$b[3][1]'| 0) :named P22))
(assert (! (not (<= |$b[4][0]'| 0)) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not $low_turn_bound) (not %init))))
(assert true)
(assert (! (not |$low_turn_bound'|) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) (not $H~0.holds))))
(assert true)
(assert (! (not |%init'|) :named P0))
(assert (! (not |$H~0.holds'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (or $low_turn_bound %init))))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not $low_turn_bound) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! %init :named F0))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! |$low_turn_bound'| :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and $H~0.holds (not %init))))
(assert (! %init :named F0))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! |$H~0.holds'| :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) (not (<= |$b[0][3]| 0)))))
(assert (! %init :named F0))
(assert (! (not (and (not $low_turn_bound) (not %init))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not |%init'|) :named P0))
(assert (! (not (<= |$b[0][3]'| 0)) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (and (<= |$b[0][3]| 0) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and (not $low_turn_bound) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (<= |$b[0][3]| 0) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! %init :named F0))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (<= |$b[0][3]'| 0) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! |$low_turn_bound'| :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= 0 (+ $p (- 1)))) (not %init))))
(assert (! %init :named F0))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) $H~0.holds)))
(assert (! %init :named F0))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not |%init'|) :named P0))
(assert (! |$H~0.holds'| :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= |$b[2][1]| 0) (<= 0 (+ $p (- 1))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and $H~0.holds (<= 0 (+ $p (- 1))) (not %init))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! |$H~0.holds'| :named P0))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P1))
(assert (! (not |%init'|) :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (<= 0 (+ $p (- 1))) (not %init) (not (<= |$b[0][3]| 0)))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (<= 0 (+ |$p'| (- 1))) :named P0))
(assert (! (not |%init'|) :named P1))
(assert (! (not (<= |$b[0][3]'| 0)) :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) (not (<= |$b[0][3]| 0)) $H~0.holds)))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! true :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not |%init'|) :named P0))
(assert (! (not (<= |$b[0][3]'| 0)) :named P1))
(assert (! |$H~0.holds'| :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (and (<= |$b[0][3]| 0) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (<= |$b[0][3]| 0) $H~0.holds (<= |$b[2][1]| 0) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) $low_turn_bound (not (<= |$b[4][2]| 0)) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (not (<= |$b[0][1]| 0)) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) :named F2))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (<= |$b[0][3]'| 0) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (<= |$b[2][1]'| 0) :named P2))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! |$low_turn_bound'| :named P9))
(assert (! (not (<= |$b[4][2]'| 0)) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (not (<= |$b[0][1]'| 0)) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not $global_always~4.holds) $low_turn_bound (not %init))))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not |$global_always~4.holds'|) :named P0))
(assert (! |$low_turn_bound'| :named P1))
(assert (! (not |%init'|) :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (not (and $low_turn_bound (not %init) $H~0.holds)))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! |$low_turn_bound'| :named P0))
(assert (! (not |%init'|) :named P1))
(assert (! |$H~0.holds'| :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) $H~0.holds (not $global_always~4.holds))))
(assert (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))))
(assert (! (not |%init'|) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (not |$global_always~4.holds'|) :named P2))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (or $low_turn_bound %init))))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (<= |$b[3][0]| 0) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) $global_always~4.holds (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0) (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (<= |$b[2][4]| 0) (not (<= |$b[3][3]| 0)) (<= |$b[3][0]| 0) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (<= |$b[0][0]| 0) (<= |$b[1][1]| 0) (not (<= |$b[2][3]| 0)) (<= |$b[1][0]| 0) (<= |$b[2][2]| 0) $global_always~4.holds (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (<= |$b[1][4]| 0) (<= |$b[4][1]| 0) (not (<= |$b[3][1]| 0)) (<= |$b[4][0]| 0))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) :named F2))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init)))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (not (<= |$b[2][1]'| 0)) :named P2))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (<= |$b[2][4]'| 0) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (<= |$b[3][0]'| 0) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (<= |$b[4][2]'| 0) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (<= |$b[1][1]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (<= |$b[1][0]'| 0) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! |$global_always~4.holds'| :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (<= |$b[0][1]'| 0) :named P19))
(assert (! (<= |$b[1][4]'| 0) :named P20))
(assert (! (<= |$b[4][1]'| 0) :named P21))
(assert (! (not (<= |$b[3][1]'| 0)) :named P22))
(assert (! (<= |$b[4][0]'| 0) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not $low_turn_bound) (not %init))))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init)))))
(assert (! (not |$low_turn_bound'|) :named P0))
(assert (! (not |%init'|) :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not %init) $global_always~4.holds)))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init)))))
(assert (! (not |%init'|) :named P0))
(assert (! |$global_always~4.holds'| :named P1))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (and $global_always~4.holds (not $low_turn_bound) (not %init))) (not (or $low_turn_bound %init))))
(check-sat)
(pop 1)
(push 1)
(assert (and (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (not (<= |$b[2][4]| 0)) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (<= |$b[0][0]| 0) (not (<= |$b[1][1]| 0)) (not (<= |$b[2][3]| 0)) (not (<= |$b[1][0]| 0)) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (not (<= |$b[1][4]| 0)) (not (<= |$b[4][1]| 0)) (<= |$b[3][1]| 0) (not (<= |$b[4][0]| 0)) (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (and $global_always~4.holds (not $low_turn_bound) (not %init)))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= 0 (+ $p (- 1)))) (not (<= |$b[2][0]| 0)) (not (<= |$b[2][4]| 0)) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (not %init) (<= |$b[0][0]| 0) (not (<= |$b[1][1]| 0)) (not (<= |$b[2][3]| 0)) (not (<= |$b[1][0]| 0)) (<= |$b[2][2]| 0) (not $global_always~4.holds) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (not (<= |$b[1][4]| 0)) (not (<= |$b[4][1]| 0)) (<= |$b[3][1]| 0) (not (<= |$b[4][0]| 0)))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) :named F2))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (and $global_always~4.holds (not $low_turn_bound) (not %init)))))
(assert (! (not (<= |$b[0][3]'| 0)) :named P0))
(assert (! |$H~0.holds'| :named P1))
(assert (! (not (<= |$b[2][1]'| 0)) :named P2))
(assert (! (not (<= 0 (+ |$p'| (- 1)))) :named P3))
(assert (! (not (<= |$b[2][0]'| 0)) :named P4))
(assert (! (not (<= |$b[2][4]'| 0)) :named P5))
(assert (! (not (<= |$b[3][3]'| 0)) :named P6))
(assert (! (not (<= |$b[3][0]'| 0)) :named P7))
(assert (! (not (<= |$b[1][3]'| 0)) :named P8))
(assert (! (not |$low_turn_bound'|) :named P9))
(assert (! (<= |$b[4][2]'| 0) :named P10))
(assert (! (not |%init'|) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (not (<= |$b[1][1]'| 0)) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (not (<= |$b[1][0]'| 0)) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not |$global_always~4.holds'|) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (<= |$b[0][1]'| 0) :named P19))
(assert (! (not (<= |$b[1][4]'| 0)) :named P20))
(assert (! (not (<= |$b[4][1]'| 0)) :named P21))
(assert (! (<= |$b[3][1]'| 0) :named P22))
(assert (! (not (<= |$b[4][0]'| 0)) :named P23))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[1][4]| 0)) (not (<= |$b[4][0]| 0)) (<= |$b[3][1]| 0) (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= |$b[2][0]| 0)) (not (<= |$b[2][4]| 0)) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (<= |$b[0][0]| 0) (not (<= |$b[2][3]| 0)) (not (<= |$b[1][1]| 0)) (<= |$b[2][2]| 0) (not (<= |$b[1][0]| 0)) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (not %init))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) :named F2))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (and $global_always~4.holds (not $low_turn_bound) (not %init)))))
(assert (! (not (<= |$b[1][4]'| 0)) :named P0))
(assert (! (not (<= |$b[4][0]'| 0)) :named P1))
(assert (! (<= |$b[3][1]'| 0) :named P2))
(assert (! (not (<= |$b[0][3]'| 0)) :named P3))
(assert (! |$H~0.holds'| :named P4))
(assert (! (not (<= |$b[2][1]'| 0)) :named P5))
(assert (! (not (<= |$b[2][0]'| 0)) :named P6))
(assert (! (not (<= |$b[2][4]'| 0)) :named P7))
(assert (! (not (<= |$b[3][3]'| 0)) :named P8))
(assert (! (not (<= |$b[3][0]'| 0)) :named P9))
(assert (! (not (<= |$b[1][3]'| 0)) :named P10))
(assert (! (not |$low_turn_bound'|) :named P11))
(assert (! (<= |$b[4][2]'| 0) :named P12))
(assert (! (<= |$b[0][0]'| 0) :named P13))
(assert (! (not (<= |$b[2][3]'| 0)) :named P14))
(assert (! (not (<= |$b[1][1]'| 0)) :named P15))
(assert (! (<= |$b[2][2]'| 0) :named P16))
(assert (! (not (<= |$b[1][0]'| 0)) :named P17))
(assert (! (not (<= |$b[0][2]'| 0)) :named P18))
(assert (! (<= |$b[0][1]'| 0) :named P19))
(assert (! (not |%init'|) :named P20))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (not (<= |$b[4][0]| 0)) (<= |$b[3][1]| 0) (not (<= |$b[0][3]| 0)) $H~0.holds (not (<= |$b[2][1]| 0)) (not (<= |$b[2][0]| 0)) (not (<= |$b[2][4]| 0)) (not (<= |$b[3][3]| 0)) (not (<= |$b[3][0]| 0)) (not (<= |$b[1][3]| 0)) (not $low_turn_bound) (<= |$b[4][2]| 0) (<= |$b[0][0]| 0) (not (<= |$b[2][3]| 0)) (not (<= |$b[1][1]| 0)) (<= |$b[2][2]| 0) (not (<= |$b[1][0]| 0)) (not (<= |$b[0][2]| 0)) (<= |$b[0][1]| 0) (not %init))))
(assert (! (and (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (not %init))) (not (and $H~0.holds (not (<= 0 (+ $p (- 1)))) (not %init))) (not (and (not $low_turn_bound) (not %init)))) :named F1))
(assert (! (not (and (not (<= |$b[0][3]| 0)) $H~0.holds (<= 0 (+ $p (- 1))) (not %init))) :named F2))
(assert (and (not (and (not $H~0.holds) (not $low_turn_bound) (not %init))) (not (and $H~0.holds (not $global_always~4.holds) $low_turn_bound (not %init))) (not (and $global_always~4.holds (not $low_turn_bound) (not %init)))))
(assert (! (not (<= |$b[4][0]'| 0)) :named P0))
(assert (! (<= |$b[3][1]'| 0) :named P1))
(assert (! (not (<= |$b[0][3]'| 0)) :named P2))
(assert (! |$H~0.holds'| :named P3))
(assert (! (not (<= |$b[2][1]'| 0)) :named P4))
(assert (! (not (<= |$b[2][0]'| 0)) :named P5))
(assert (! (not (<= |$b[2][4]'| 0)) :named P6))
(assert (! (not (<= |$b[3][3]'| 0)) :named P7))
(assert (! (not (<= |$b[3][0]'| 0)) :named P8))
(assert (! (not (<= |$b[1][3]'| 0)) :named P9))
(assert (! (not |$low_turn_bound'|) :named P10))
(assert (! (<= |$b[4][2]'| 0) :named P11))
(assert (! (<= |$b[0][0]'| 0) :named P12))
(assert (! (not (<= |$b[2][3]'| 0)) :named P13))
(assert (! (not (<= |$b[1][1]'| 0)) :named P14))
(assert (! (<= |$b[2][2]'| 0) :named P15))
(assert (! (not (<= |$b[1][0]'| 0)) :named P16))
(assert (! (not (<= |$b[0][2]'| 0)) :named P17))
(assert (! (<= |$b[0][1]'| 0) :named P18))
(assert (! (not |%init'|) :named P19))
(check-sat)
(get-unsat-core)