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) |