lustrec / bench / distrib / misc / durationThm_1_e1_350 / conds / durationThm_1_e1_350.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) |