Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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