(bakery (phase_inclusive 0 (phase_inclusive-1 nil 3237458137 nil nil nil nil nil nil nil shostak)) (phase_disjoint 0 (phase_disjoint-1 nil 3237458137 nil nil nil nil nil nil nil shostak)) (phase_induction 0 (phase_induction-1 nil 3237458137 nil nil nil nil nil nil nil shostak)) (first_try 0 (first_try-1 nil 3237458137 3237650320 ("" (expand "indinv") (("" (ground) (("1" (grind) nil nil) ("2" (skosimp) (("2" (expand "transitions") (("2" (ground) (("1" (expand "P1_transition") (("1" (bddsimp) (("1" (grind) nil nil) ("2" (grind) (("2" (postpone) nil nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 27873 3350 t shostak)) (second_try 0 (second_try-1 nil 3237458137 3237650352 ("" (expand "indinv") (("" (ground) (("1" (grind) nil nil) ("2" (skosimp) (("2" (expand "transitions") (("2" (ground) (("1" (expand "P1_transition") (("1" (bddsimp) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) (("3" (postpone) nil nil)) nil) ("4" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 26699 3730 t shostak)) (third_try 0 (third_try-1 nil 3237458137 3237650367 ("" (expand "indinv") (("" (ground) (("1" (grind) nil nil) ("2" (skosimp) (("2" (expand "transitions") (("2" (ground) (("1" (expand "P1_transition") (("1" (bddsimp) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((init const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil) (strong_safe const-decl "bool" bakery nil) (inductive_safe const-decl "bool" bakery nil) (P1_transition const-decl "boolean" bakery nil) (P2_transition const-decl "boolean" bakery nil) (transitions const-decl "bool" bakery nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (state type-eq-decl nil bakery nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phase type-decl nil bakery nil) (indinv const-decl "bool" transitions nil)) 8767 4090 t shostak)) (init_simulation 0 (init_simulation-1 nil 3237458137 3237650387 ("" (grind) nil nil) proved ((init const-decl "boolean" bakery nil) (abst const-decl "abstract_state" bakery nil) (a_init const-decl "bool" bakery nil)) 5108 380 t shostak)) (trans_simulation 0 (trans_simulation-1 nil 3237458137 3237650557 ("" (skosimp) (("" (expand "transitions") (("" (expand "a_trans") (("" (ground) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 1) (("2" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 165275 29070 t shostak)) (safety_preserved 0 (safety_preserved-1 nil 3237458137 3237650567 ("" (grind) nil nil) proved ((abst const-decl "abstract_state" bakery nil) (a_safe const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil)) 2821 340 t shostak)) (abs_invariant_ctl 0 (abs_invariant_ctl-1 nil 3237458137 3237650581 ("" (model-check) nil nil) proved ((a_init const-decl "bool" bakery nil) (AG const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EX const-decl "bool" ctlops nil) (a_safe const-decl "boolean" bakery nil) (a_P1_transition const-decl "bool" bakery nil) (a_P2_transition const-decl "bool" bakery nil) (a_trans const-decl "bool" bakery nil)) 8030 750 t shostak)) (extra 0 (extra-1 nil 3237458137 3237650589 ("" (grind) nil nil) proved ((init const-decl "boolean" bakery nil) (not_eq const-decl "bool" bakery nil) (P1_transition const-decl "boolean" bakery nil) (P2_transition const-decl "boolean" bakery nil) (transitions const-decl "bool" bakery nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (state type-eq-decl nil bakery nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phase type-decl nil bakery nil) (indinv const-decl "bool" transitions nil)) 2656 1050 t shostak)) (strong_trans_simulation 0 (strong_trans_simulation-1 nil 3237458137 3237650694 ("" (skosimp) (("" (expand "transitions") (("" (ground) (("1" (expand "P1_transition") (("1" (apply (then (ground) (grind))) nil nil)) nil) ("2" (expand "P2_transition") (("2" (apply (then (ground) (grind))) nil nil)) nil)) nil)) nil)) nil) proved ((transitions const-decl "bool" bakery nil) (P1_transition const-decl "boolean" bakery nil) (a_trans const-decl "bool" bakery nil) (a_P2_transition const-decl "bool" bakery nil) (a_P1_transition const-decl "bool" bakery nil) (abst const-decl "abstract_state" bakery nil) (indinv const-decl "bool" transitions nil) (phase type-decl nil bakery nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (state type-eq-decl nil bakery nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (P2_transition const-decl "boolean" bakery nil) (not_eq const-decl "bool" bakery nil) (init const-decl "boolean" bakery nil)) 101488 40100 t shostak)) (auto_abstract 0 (auto_abstract-1 nil 3237458137 3237650743 ("" (abstract-and-mc "state" "abstract_state" (("t1_is_0" "lambda (s): s`t1=0") ("t2_is_0" "lambda (s): s`t2=0") ("t1_lt_t2" "lambda (s): s`t1 < s`t2"))) nil nil) proved ((transitions const-decl "bool" bakery nil) (P2_transition const-decl "boolean" bakery nil) (P1_transition const-decl "boolean" bakery nil) (safe const-decl "boolean" bakery nil) (a_safe const-decl "boolean" bakery nil) (abst const-decl "abstract_state" bakery nil) (EX const-decl "bool" ctlops nil) (EU const-decl "pred[state]" ctlops nil) (EF const-decl "pred[state]" ctlops nil) (AG const-decl "pred[state]" ctlops nil) (init const-decl "boolean" bakery nil)) 40856 5260 t shostak)))