ForAll((x2_s_1) => ((Exist(x2_s_2 | code_ok) ^ ~(Exist(l_s_13 | set_status))) | (~(Exist(x2_s_2 | code_ok)) ^ Exist(l_s_13 | set_status))))
ForAll(~((x2_s_1) ^ (l_s_13 | set_status)))
Exist(x2_s_5)
ForAll((tau_5) => Exist(storno))
ForAll(~((l_s_11) ^ (release)))
ForAll(~((x2_s_3) ^ (tau_2)))
ForAll(~(((l_s_3 | storno) | (a2_s_2 | a2_e_2)) ^ (a2_e_1)))
ForAll(~((x2_s_2 | x2_e_2) ^ (l_s_11 | release)))
ForAll((l_s_0 | new) => Exist(x2_s_0 | x2_e_0))
ForAll((x2_s_0) => ((Exist(a2_s_0 | x2_e_9) ^ ~(Exist(l_s_15 | join_pat))) | (~(Exist(a2_s_0 | x2_e_9)) ^ Exist(l_s_15 | join_pat))))
ForAll(~((tau_19) ^ (x2_e_9)))
ForAll(~((l_s_2) ^ (code_error)))
ForAll(~((l_s_13) ^ (tau_16)))
ForAll((set_status) => ((Exist(tau_16) ^ Exist(set_status)) | (~(Exist(tau_16)))))
ForAll(~((x2_s_3) ^ (x2_e_3)))
ForAll((manual) => ((Exist(tau_13) ^ Exist(manual)) | (~(Exist(tau_13)))))
Exist(l_s_4)
Exist(x3_s_4)
ForAll(~((l_s_0) ^ (tau_0)))
ForAll(~((x2_s_3 | fin) ^ (x2_e_2)))
ForAll(~((x2_s_9) ^ (x2_e_9)))
ForAll(~((l_s_13) ^ (set_status)))
ForAll(~((fin) ^ (tau_12)))
ForAll(~((l_s_5) ^ (tau_7)))
ForAll(~((l_s_6) ^ (reopen)))
ForAll(~((billed) ^ (tau_1)))
ForAll(~((tau_8) ^ (l_s_6 | reopen)))
ForAll(~((x2_s_2 | x2_e_2) ^ (l_s_12 | code_ok)))
ForAll(~((reject) ^ (tau_7)))
ForAll(~((x2_s_5 | x2_e_5) ^ (a2_s_1 | a2_e_1)))
ForAll(~((l_s_6 | reopen) ^ (x2_e_6)))
ForAll(~((l_s_13 | set_status) ^ (x2_e_1)))
ForAll((l_s_4) => Exist(code_nok))
ForAll(~((x2_s_5 | x2_e_6) ^ (l_s_8 | change_end)))
Exist(a2_s_1)
Exist(x2_s_3 | x2_e_3)
ForAll(~((tau_19) ^ (l_s_14 | delete)))
ForAll((tau_0) => Exist(new))
ForAll(~((l_s_5) ^ (reject)))
ForAll((change_end) => ((Exist(tau_11) ^ Exist(change_end)) | (~(Exist(tau_11)))))
ForAll(~((a2_s_2) ^ ((l_s_4 | code_nok) | (l_s_5 | reject))))
ForAll(~((x2_s_9) ^ (l_s_14 | delete)))
ForAll(~((x2_s_3) ^ (x3_s_4 | x3_e_4)))
ForAll((a2_s_2 | a2_e_2) => Exist(a2_e_1))
ForAll((l_s_13) => Exist(set_status))
Exist(x2_s_0)
ForAll(~((x2_s_6) ^ (tau_8)))
ForAll(~((x2_s_7) ^ (x2_e_7)))
ForAll(~((l_s_0 | new) ^ (x2_s_0 | x2_e_0)))
Exist(l_s_11)
ForAll(~((x2_s_6) ^ (x2_e_6)))
ForAll(~((l_s_10 | manual) ^ (x2_e_2)))
ForAll(~((x2_s_8) ^ (tau_18)))
ForAll(~((x2_s_5) ^ (x2_e_5)))
ForAll((tau_6) => Exist(code_nok))
ForAll(~((l_s_9) ^ (fin)))
ForAll(~((l_s_7 | change_diagn) ^ (x3_e_4)))
ForAll(~((l_s_11 | release) ^ (l_s_12 | code_ok)))
Exist(x2_s_1 | x2_e_1)
ForAll(~((x2_s_8) ^ (x2_e_8)))
ForAll(~((l_s_1) ^ (billed)))
ForAll((a2_s_2) => (Exist(l_s_4 | code_nok) ^ Exist(l_s_5 | reject)))
ForAll((tau_16) => Exist(set_status))
ForAll((tau_9) => Exist(reopen))
ForAll((l_s_1) => Exist(billed))
ForAll(~((release) ^ (tau_14)))
ForAll((x2_s_2 | x2_e_2) => Exist(l_s_11 | release))
ForAll(~((l_s_3) ^ (tau_5)))
ForAll((x2_s_8) => ((Exist(tau_18) ^ ~(Exist(empty))) | (~(Exist(tau_18)) ^ Exist(empty))))
ForAll(~((l_s_7 | change_diagn) ^ (l_s_8 | change_end)))
ForAll(~((x2_s_2 | code_ok) ^ (l_s_13 | set_status)))
ForAll(~((l_s_6) ^ (tau_9)))
ForAll((change_diagn) => ((Exist(tau_10) ^ Exist(change_diagn)) | (~(Exist(tau_10)))))
ForAll(((tau_2) | (x3_s_4 | x3_e_4)) => Exist(x2_e_3))
Exist(a2_s_0 | a2_e_0)
ForAll(((tau_3) | (l_s_2 | code_error)) => Exist(x2_e_5))
ForAll((l_s_0) => Exist(new))
Exist(l_s_1)
ForAll(~((tau_18) ^ (empty)))
ForAll((tau_12) => Exist(fin))
ForAll((tau_7) => Exist(reject))
ForAll(~((x2_s_3 | x2_e_3) ^ (l_s_9 | fin)))
Exist(x2_s_7)
ForAll(~((a2_s_1) ^ ((l_s_3 | storno) | (a2_s_2 | a2_e_2))))
ForAll(((x2_s_2 | code_ok) | (l_s_13 | set_status)) => Exist(x2_e_1))
ForAll((a2_s_0 | x2_e_8) => Exist(x2_s_9 | x2_e_9))
ForAll(~((l_s_1) ^ (tau_1)))
ForAll(~(((l_s_4 | code_nok) | (l_s_5 | reject)) ^ (a2_e_2)))
ForAll((reject) => ((Exist(tau_7) ^ Exist(reject)) | (~(Exist(tau_7)))))
ForAll(~((l_s_8) ^ (change_end)))
ForAll(~((l_s_2) ^ (tau_4)))
ForAll(~((l_s_4) ^ (code_nok)))
ForAll(((x2_s_5 | x2_e_6) | (l_s_7 | change_diagn) | (l_s_8 | change_end)) => Exist(x3_e_4))
ForAll(~((l_s_7) ^ (change_diagn)))
Exist(l_s_10)
ForAll(((tau_17) | (zdbc_behan)) => Exist(x2_e_7))
ForAll((x2_s_9) => ((Exist(tau_19) ^ ~(Exist(l_s_14 | delete))) | (~(Exist(tau_19)) ^ Exist(l_s_14 | delete))))
ForAll(~((a2_s_0) ^ ((l_s_1 | billed) | (x2_s_1 | x2_e_7))))
ForAll((l_s_3) => Exist(storno))
ForAll(~((l_s_11) ^ (tau_14)))
ForAll(~((delete) ^ (tau_20)))
ForAll(~((x2_s_6) ^ (l_s_6 | reopen)))
Exist(l_s_13)
ForAll((l_s_1 | billed) => Exist(a2_e_0))
ForAll(~((l_s_14) ^ (tau_20)))
ForAll(~((x2_s_0) ^ (l_s_15 | join_pat)))
Exist(l_s_0)
Exist(a2_s_2)
ForAll(~((code_error) ^ (tau_4)))
ForAll((x2_s_1 | x2_e_7) => Exist(a2_e_0))
ForAll(~((l_s_12) ^ (tau_15)))
ForAll(~((empty) ^ (x2_e_8)))
ForAll((l_s_8) => Exist(change_end))
ForAll((x2_s_5) => ((Exist(tau_3) ^ ~(Exist(l_s_2 | code_error))) | (~(Exist(tau_3)) ^ Exist(l_s_2 | code_error))))
ForAll(~((x3_s_4 | x3_e_4) ^ (x2_e_3)))
ForAll(~((l_s_3) ^ (storno)))
ForAll((tau_4) => Exist(code_error))
ForAll(((x2_s_3 | fin) | (l_s_10 | manual)) => Exist(x2_e_2))
Exist(l_s_12)
ForAll((x2_s_2) => ((Exist(x2_s_3 | fin) ^ ~(Exist(l_s_10 | manual))) | (~(Exist(x2_s_3 | fin)) ^ Exist(l_s_10 | manual))))
ForAll(~((x2_s_2) ^ (x2_s_3 | fin)))
ForAll((code_ok) => ((Exist(tau_15) ^ Exist(code_ok)) | (~(Exist(tau_15)))))
ForAll(~((l_s_2 | code_error) ^ (x2_e_5)))
ForAll((l_s_5 | reject) => Exist(a2_e_2))
ForAll(~((l_s_14) ^ (delete)))
Exist(l_s_15)
ForAll(~(((l_s_1 | billed) | (x2_s_1 | x2_e_7)) ^ (a2_e_0)))
ForAll(~((tau_2) ^ (x2_e_3)))
ForAll((l_s_14) => Exist(delete))
Exist(x2_s_5 | a2_e_1)
Exist(l_s_3)
ForAll(~((x3_s_4) ^ (l_s_8 | change_end)))
ForAll((x2_s_3) => ((Exist(tau_2) ^ ~(Exist(x3_s_4 | x3_e_4))) | (~(Exist(tau_2)) ^ Exist(x3_s_4 | x3_e_4))))
ForAll(~((zdbc_behan) ^ (x2_e_7)))
ForAll((x2_s_1 | x2_e_1) => Exist(x2_s_7 | x2_e_7))
ForAll((a2_s_0 | a2_e_0) => Exist(x2_s_8 | x2_e_8))
ForAll(~((join_pat) ^ (tau_21)))
ForAll((l_s_7) => Exist(change_diagn))
ForAll((x2_s_3 | x2_e_3) => Exist(l_s_9 | fin))
ForAll((a2_s_0) => (Exist(l_s_1 | billed) ^ Exist(x2_s_1 | x2_e_7)))
ForAll((tau_21) => Exist(join_pat))
Exist(l_s_7)
ForAll(~((l_s_10) ^ (manual)))
ForAll((tau_11) => Exist(change_end))
ForAll((l_s_12) => Exist(code_ok))
ForAll(~((l_s_10) ^ (tau_13)))
Exist(x2_s_9)
ForAll(~((a2_s_0 | x2_e_8) ^ (x2_s_9 | x2_e_9)))
Exist(l_s_2)
ForAll(~((tau_8) ^ (x2_e_6)))
Exist(l_s_6)
ForAll((code_error) => ((Exist(tau_4) ^ Exist(code_error)) | (~(Exist(tau_4)))))
Exist(x2_s_3)
Exist(l_s_8)
ForAll(~((manual) ^ (tau_13)))
ForAll(~((l_s_8) ^ (tau_11)))
ForAll(~((x2_s_8) ^ (empty)))
ForAll(~((x2_s_2 | code_ok) ^ (x2_e_1)))
ForAll((release) => ((Exist(tau_14) ^ Exist(release)) | (~(Exist(tau_14)))))
ForAll((l_s_3 | storno) => Exist(a2_e_1))
ForAll((tau_13) => Exist(manual))
Exist(x2_s_5 | x2_e_5)
ForAll(~((l_s_15) ^ (tau_21)))
ForAll(((tau_18) | (empty)) => Exist(x2_e_8))
ForAll(~((x2_s_5 | x2_e_6) ^ (l_s_7 | change_diagn)))
ForAll(~((a2_s_0 | a2_e_0) ^ (x2_s_8 | x2_e_8)))
ForAll(~((l_s_15 | join_pat) ^ (x2_e_0)))
Exist(l_s_0 | new)
ForAll(~((x3_s_4) ^ (x2_s_5 | x2_e_6)))
ForAll(~((x2_s_0) ^ (a2_s_0 | x2_e_9)))
ForAll((reopen) => ((Exist(tau_9) ^ Exist(reopen)) | (~(Exist(tau_9)))))
ForAll(~((x2_s_2) ^ (x2_e_2)))
ForAll(~((change_end) ^ (tau_11)))
ForAll(~((x2_s_5 | x2_e_6) ^ (x3_e_4)))
ForAll((new) => ((Exist(tau_0) ^ Exist(new)) | (~(Exist(tau_0)))))
ForAll((a2_s_1) => (Exist(l_s_3 | storno) ^ Exist(a2_s_2 | a2_e_2)))
ForAll(~((set_status) ^ (tau_16)))
Exist(x2_s_2 | x2_e_2)
ForAll(~((l_s_4) ^ (tau_6)))
ForAll(~((x3_s_4) ^ (l_s_7 | change_diagn)))
ForAll(~((tau_18) ^ (x2_e_8)))
ForAll(((tau_19) | (l_s_14 | delete)) => Exist(x2_e_9))
ForAll((tau_15) => Exist(code_ok))
ForAll((storno) => ((Exist(tau_5) ^ Exist(storno)) | (~(Exist(tau_5)))))
ForAll(~((a2_s_0 | x2_e_9) ^ (x2_e_0)))
Exist(l_s_14)
ForAll((l_s_15) => Exist(join_pat))
ForAll(~((l_s_15) ^ (join_pat)))
ForAll((code_nok) => ((Exist(tau_6) ^ Exist(code_nok)) | (~(Exist(tau_6)))))
ForAll(~((x2_s_9) ^ (tau_19)))
ForAll((tau_20) => Exist(delete))
ForAll(~((tau_2) ^ (x3_s_4 | x3_e_4)))
ForAll((fin) => ((Exist(tau_12) ^ Exist(fin)) | (~(Exist(tau_12)))))
ForAll((x2_s_5 | x2_e_5) => Exist(a2_s_1 | a2_e_1))
ForAll((x2_s_6) => ((Exist(tau_8) ^ ~(Exist(l_s_6 | reopen))) | (~(Exist(tau_8)) ^ Exist(l_s_6 | reopen))))
ForAll(~((x2_s_5 | a2_e_1) ^ (x2_s_6 | x2_e_6)))
ForAll(((tau_8) | (l_s_6 | reopen)) => Exist(x2_e_6))
ForAll(~((x2_s_2) ^ (l_s_10 | manual)))
ForAll((l_s_2) => Exist(code_error))
Exist(x2_s_6)
ForAll(~((l_s_7) ^ (tau_10)))
ForAll(~((l_s_8 | change_end) ^ (x3_e_4)))
ForAll((l_s_6) => Exist(reopen))
ForAll(~((a2_s_0 | x2_e_9) ^ (l_s_15 | join_pat)))
ForAll(~((x2_s_3 | fin) ^ (l_s_10 | manual)))
ForAll(~((x2_s_5) ^ (l_s_2 | code_error)))
Exist(x2_s_1)
Exist(l_s_9)
ForAll((x2_s_5 | a2_e_1) => Exist(x2_s_6 | x2_e_6))
Exist(l_s_5)
ForAll(~((change_diagn) ^ (tau_10)))
Exist(x2_s_2)
ForAll(~((code_ok) ^ (tau_15)))
ForAll((l_s_4 | code_nok) => Exist(a2_e_2))
ForAll(~((x2_s_7) ^ (zdbc_behan)))
Exist(a2_s_0)
ForAll(~((x2_s_1) ^ (x2_s_2 | code_ok)))
ForAll(~((storno) ^ (tau_5)))
ForAll((tau_14) => Exist(release))
ForAll(~((l_s_9) ^ (tau_12)))
ForAll(~((tau_17) ^ (x2_e_7)))
ForAll((l_s_11) => Exist(release))
ForAll(~((l_s_0) ^ (new)))
ForAll((l_s_11 | release) => Exist(l_s_12 | code_ok))
ForAll(~((x2_s_1) ^ (x2_e_1)))
ForAll((delete) => ((Exist(tau_20) ^ Exist(delete)) | (~(Exist(tau_20)))))
Exist(a2_s_0 | x2_e_8)
ForAll(~((reopen) ^ (tau_9)))
ForAll((billed) => ((Exist(tau_1) ^ Exist(billed)) | (~(Exist(tau_1)))))
ForAll((l_s_9) => Exist(fin))
ForAll((x3_s_4) => ((Exist(x2_s_5 | x2_e_6) ^ ~(Exist(l_s_7 | change_diagn)) ^ ~(Exist(l_s_8 | change_end))) | ((~(Exist(x2_s_5 | x2_e_6)) ^ Exist(l_s_7 | change_diagn) ^ ~(Exist(l_s_8 | change_end))) | (~(Exist(x2_s_5 | x2_e_6)) ^ ~(Exist(l_s_7 | change_diagn)) ^ Exist(l_s_8 | change_end)))))
ForAll(~((x2_s_7) ^ (tau_17)))
ForAll(~((l_s_12) ^ (code_ok)))
ForAll(~((x2_s_1 | x2_e_1) ^ (x2_s_7 | x2_e_7)))
ForAll(~((x2_s_5) ^ (tau_3)))
ForAll(~((l_s_14 | delete) ^ (x2_e_9)))
ForAll((join_pat) => ((Exist(tau_21) ^ Exist(join_pat)) | (~(Exist(tau_21)))))
Exist(x2_s_8)
ForAll(~((tau_3) ^ (l_s_2 | code_error)))
ForAll(~((tau_3) ^ (x2_e_5)))
ForAll(~((tau_17) ^ (zdbc_behan)))
ForAll((tau_1) => Exist(billed))
ForAll((l_s_10) => Exist(manual))
ForAll((x2_s_7) => ((Exist(tau_17) ^ ~(Exist(zdbc_behan))) | (~(Exist(tau_17)) ^ Exist(zdbc_behan))))
ForAll(((a2_s_0 | x2_e_9) | (l_s_15 | join_pat)) => Exist(x2_e_0))
ForAll((tau_10) => Exist(change_diagn))
ForAll((l_s_5) => Exist(reject))
ForAll(~((code_nok) ^ (tau_6)))
ForAll(~((x3_s_4) ^ (x3_e_4)))
ForAll(~((new) ^ (tau_0)))
ForAll(~((x2_s_0) ^ (x2_e_0)))