kind2 v2.0.0-7-gdcc7f6f



====================================================================================================================
Analyzing proof_ev_false
  with First top: 'proof_ev_false'
             subsystems
               | concrete: timeab_tmp, timeab_exp, timeab, min, forall_a, exist, eventually_false, P_at_k

<Success> Property eventually_false[l223c25].timeab[l203c16].assume[l110c2] is valid by property directed reachability (IA) after 0.440s.

<Success> Property eventually_false[l223c25].timeab[l203c16].timeab_exp[l111c19].assume[l82c5] is valid by 2-induction after 0.550s.

<Success> Property eventually_false[l222c21].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2] is valid by inductive step after 0.550s.

<Success> Property eventually_false[l223c25].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2] is valid by 2-induction after 0.550s.

<Success> Property eventually_false[l222c21].timeab[l203c16].timeab_exp[l111c19].assume[l82c5] is valid by inductive step after 0.550s.

<Success> Property eventually_false[l223c25].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2] is valid by 2-induction after 0.550s.

<Success> Property eventually_false[l222c21].timeab[l203c16].assume[l110c2] is valid by inductive step after 0.550s.

<Success> Property eventually_false[l222c21].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2] is valid by 2-induction after 0.550s.

<Success> Property eventually_false[l223c25].timeab[l203c16].guarantee[l111c2] is valid by 2-induction after 54.192s.

<Success> Property eventually_false[l222c21].timeab[l203c16].guarantee[l111c2] is valid by 2-induction after 54.192s.

<Success> Property guarantee[l213c5] is valid by 2-induction after 54.192s.

<Success> Property guarantee[l212c5] is valid by 2-induction after 54.192s.

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l212c5]: valid (k=2)
guarantee[l213c5]: valid (k=2)
eventually_false[l222c21].timeab[l203c16].guarantee[l111c2]: valid (k=2)
eventually_false[l222c21].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_false[l222c21].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_false[l222c21].timeab[l203c16].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_false[l222c21].timeab[l203c16].assume[l110c2]: valid (k=1)
eventually_false[l223c25].timeab[l203c16].guarantee[l111c2]: valid (k=2)
eventually_false[l223c25].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_false[l223c25].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_false[l223c25].timeab[l203c16].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_false[l223c25].timeab[l203c16].assume[l110c2]: valid (k=1)
====================================================================================================================