## lustrec / bench / distrib / misc / durationThm_1_e3_389 / conds / durationThm_1_e3_389.conds @ 43a2cae9

History | View | Annotate | Download (5.43 KB)

1 |
V16_env and (OK != ((not V16_env) => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |
---|---|

2 |
(not V16_env) and (OK != ((not V16_env) => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

3 |
(V68_age_of_p >= (V14_k + V15_m)) and (OK != (V16_env => (true -> ((not (V68_age_of_p >= (V14_k + V15_m))) => r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

4 |
(not (V68_age_of_p >= (V14_k + V15_m))) and (OK != (V16_env => (true -> ((not (V68_age_of_p >= (V14_k + V15_m))) => r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

5 |
r and (OK != (V16_env => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => (not r))))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

6 |
(not r) and (OK != (V16_env => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => (not r))))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

7 |
V55_X and (V16_env != ((not V55_X) -> (V55_X and pre V16_env))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

8 |
(not V55_X) and (V16_env != ((not V55_X) -> (V55_X and pre V16_env))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

9 |
V55_X and (V16_env != (V55_X -> ((not V55_X) and pre V16_env))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

10 |
(not V55_X) and (V16_env != (V55_X -> ((not V55_X) and pre V16_env))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

11 |
pre V16_env and (V16_env != (V55_X -> (V55_X and pre (not V16_env)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

12 |
(not pre V16_env) and (V16_env != (V55_X -> (V55_X and pre (not V16_env)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

13 |
(V14_k >= 1) and (V55_X != ((((not (V14_k >= 1)) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

14 |
(not (V14_k >= 1)) and (V55_X != ((((not (V14_k >= 1)) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

15 |
(V15_m >= 1) and (V55_X != ((((V14_k >= 1) and (not (V15_m >= 1))) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

16 |
(not (V15_m >= 1)) and (V55_X != ((((V14_k >= 1) and (not (V15_m >= 1))) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

17 |
(V45_age_of_p >= V14_k) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((not (V45_age_of_p >= V14_k)) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

18 |
(not (V45_age_of_p >= V14_k)) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((not (V45_age_of_p >= V14_k)) => q)) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

19 |
q and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => (not q))) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

20 |
(not q) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => (not q))) and ((V52_age_of_p >= V15_m) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

21 |
(V52_age_of_p >= V15_m) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((not (V52_age_of_p >= V15_m)) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

22 |
(not (V52_age_of_p >= V15_m)) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((not (V52_age_of_p >= V15_m)) => r))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

23 |
r and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => (not r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |

24 |
(not r) and (V55_X != ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) and ((V52_age_of_p >= V15_m) => (not r)))) and (ik > 0 or ik <= 0) and (im > 0 or im <= 0) and (p or not p) and (q or not q) and (r or not r) and (OK or not OK) |