ForAll(~((x2_s_B5) ^ (tau_B3)))
ForAll((l_s_B13) => Exist(set_status))
ForAll(~((x3_s_B4) ^ (x3_e_B4)))
Exist(x2_s_B1 | x2_e_B1)
ForAll(~((l_s_B6) ^ (reopen)))
ForAll(~((l_s_B5) ^ (tau_B7)))
ForAll(~((x2_s_B0) ^ (x2_e_B0)))
ForAll((x2_s_B6) => ((Exist(tau_B8) ^ ~(Exist(l_s_B6 | reopen))) | (~(Exist(tau_B8)) ^ Exist(l_s_B6 | reopen))))
ForAll(~((l_s_B9) ^ (tau_B12)))
ForAll((x2_s_B2) => ((Exist(x2_s_B3 | fin) ^ ~(Exist(l_s_B10 | manual))) | (~(Exist(x2_s_B3 | fin)) ^ Exist(l_s_B10 | manual))))
ForAll(~((l_s_B13) ^ (set_status)))
ForAll(~((x2_s_B2 | code_ok) ^ (l_s_B13 | set_status)))
ForAll(~((x2_s_B3) ^ (tau_B2)))
ForAll((l_s_B0 | new) => Exist(x2_s_B0 | x2_e_B0))
ForAll(~((release) ^ (tau_B14)))
ForAll(~((tau_B19) ^ (x2_e_B9)))
ForAll(~((l_s_B4) ^ (code_nok)))
ForAll(~((x2_s_B8) ^ (tau_B18)))
ForAll((l_s_B7) => Exist(change_diagn))
ForAll((tau_B14) => Exist(release))
ForAll(~((x3_s_B4) ^ (l_s_B8 | change_end)))
ForAll(~((x2_s_B2) ^ (x2_e_B2)))
ForAll((tau_B6) => Exist(code_nok))
Exist(l_s_B3)
ForAll((l_s_B4) => Exist(code_nok))
ForAll((x2_s_B5 | x2_e_B5) => Exist(a2_s_B1 | a2_e_B1))
ForAll(~((l_s_B9) ^ (fin)))
ForAll(~((new) ^ (tau_B0)))
ForAll((new) => ((Exist(tau_B0) ^ Exist(new)) | (~(Exist(tau_B0)))))
ForAll(~((x2_s_B9) ^ (tau_B19)))
ForAll(~((x2_s_B1 | x2_e_B1) ^ (x2_s_B7 | x2_e_B7)))
ForAll(~((x2_s_B5) ^ (l_s_B2 | code_error)))
ForAll(~((l_s_B2) ^ (code_error)))
ForAll((tau_B16) => Exist(set_status))
ForAll((x2_s_B7) => ((Exist(tau_B17) ^ ~(Exist(zdbc_behan))) | (~(Exist(tau_B17)) ^ Exist(zdbc_behan))))
ForAll(~((tau_B3) ^ (l_s_B2 | code_error)))
ForAll(~((l_s_B7) ^ (tau_B10)))
ForAll(((x2_s_B2 | code_ok) | (l_s_B13 | set_status)) => Exist(x2_e_B1))
ForAll(~((l_s_B10) ^ (manual)))
ForAll(~((l_s_B2 | code_error) ^ (x2_e_B5)))
Exist(l_s_B14)
ForAll((l_s_B14) => Exist(delete))
Exist(l_s_B5)
ForAll(~((storno) ^ (tau_B5)))
ForAll(~((x2_s_B1) ^ (l_s_B13 | set_status)))
Exist(l_s_B0)
Exist(x2_s_B2 | x2_e_B2)
ForAll(~(((l_s_B4 | code_nok) | (l_s_B5 | reject)) ^ (a2_e_B2)))
Exist(x2_s_B5)
ForAll(~(((l_s_B3 | storno) | (a2_s_B2 | a2_e_B2)) ^ (a2_e_B1)))
ForAll(~((l_s_B12) ^ (code_ok)))
ForAll((a2_s_B0 | x2_e_B8) => Exist(x2_s_B9 | x2_e_B9))
ForAll((l_s_B10) => Exist(manual))
ForAll((code_ok) => ((Exist(tau_B15) ^ Exist(code_ok)) | (~(Exist(tau_B15)))))
ForAll((x2_s_B5) => ((Exist(tau_B3) ^ ~(Exist(l_s_B2 | code_error))) | (~(Exist(tau_B3)) ^ Exist(l_s_B2 | code_error))))
ForAll(~((a2_s_B2) ^ ((l_s_B4 | code_nok) | (l_s_B5 | reject))))
ForAll((a2_s_B0 | a2_e_B0) => Exist(x2_s_B8 | x2_e_B8))
Exist(x2_s_B3)
ForAll(~((x2_s_B0) ^ (a2_s_B0 | x2_e_B9)))
ForAll((l_s_B6) => Exist(reopen))
Exist(l_s_B7)
Exist(l_s_B15)
ForAll((join_pat) => ((Exist(tau_B21) ^ Exist(join_pat)) | (~(Exist(tau_B21)))))
ForAll(~((l_s_B14) ^ (tau_B20)))
ForAll(~((x2_s_B9) ^ (x2_e_B9)))
ForAll(~((l_s_B8) ^ (tau_B11)))
ForAll(~(((l_s_B1 | billed) | (x2_s_B1 | x2_e_B7)) ^ (a2_e_B0)))
ForAll((change_end) => ((Exist(tau_B11) ^ Exist(change_end)) | (~(Exist(tau_B11)))))
ForAll(~((l_s_B11 | release) ^ (l_s_B12 | code_ok)))
ForAll((fin) => ((Exist(tau_B12) ^ Exist(fin)) | (~(Exist(tau_B12)))))
ForAll(((tau_B17) | (zdbc_behan)) => Exist(x2_e_B7))
ForAll(~((x2_s_B5 | x2_e_B5) ^ (a2_s_B1 | a2_e_B1)))
ForAll(~((l_s_B8) ^ (change_end)))
ForAll(~((x2_s_B5 | x2_e_B6) ^ (l_s_B8 | change_end)))
ForAll((tau_B1) => Exist(billed))
ForAll((tau_B21) => Exist(join_pat))
ForAll((x3_s_B4) => ((Exist(x2_s_B5 | x2_e_B6) ^ ~(Exist(l_s_B7 | change_diagn)) ^ ~(Exist(l_s_B8 | change_end))) | ((~(Exist(x2_s_B5 | x2_e_B6)) ^ Exist(l_s_B7 | change_diagn) ^ ~(Exist(l_s_B8 | change_end))) | (~(Exist(x2_s_B5 | x2_e_B6)) ^ ~(Exist(l_s_B7 | change_diagn)) ^ Exist(l_s_B8 | change_end)))))
ForAll((tau_B5) => Exist(storno))
ForAll(~((tau_B2) ^ (x2_e_B3)))
Exist(l_s_B9)
Exist(x2_s_B6)
ForAll(~((tau_B18) ^ (empty)))
ForAll(((tau_B18) | (empty)) => Exist(x2_e_B8))
Exist(l_s_B2)
ForAll((l_s_B2) => Exist(code_error))
ForAll((l_s_B9) => Exist(fin))
ForAll(~((l_s_B13) ^ (tau_B16)))
ForAll(~((x2_s_B7) ^ (zdbc_behan)))
ForAll(~((change_end) ^ (tau_B11)))
ForAll(~((x2_s_B3 | x2_e_B3) ^ (l_s_B9 | fin)))
ForAll((reopen) => ((Exist(tau_B9) ^ Exist(reopen)) | (~(Exist(tau_B9)))))
ForAll(~((l_s_B14) ^ (delete)))
ForAll(~((x2_s_B1) ^ (x2_s_B2 | code_ok)))
Exist(x2_s_B8)
ForAll((l_s_B4 | code_nok) => Exist(a2_e_B2))
ForAll(~((l_s_B7 | change_diagn) ^ (l_s_B8 | change_end)))
ForAll(~((l_s_B1) ^ (tau_B1)))
ForAll(~((x2_s_B7) ^ (x2_e_B7)))
ForAll((x2_s_B3) => ((Exist(tau_B2) ^ ~(Exist(x3_s_B4 | x3_e_B4))) | (~(Exist(tau_B2)) ^ Exist(x3_s_B4 | x3_e_B4))))
ForAll(~((x2_s_B2 | code_ok) ^ (x2_e_B1)))
ForAll((l_s_B1 | billed) => Exist(a2_e_B0))
ForAll(~((x2_s_B7) ^ (tau_B17)))
ForAll(~((delete) ^ (tau_B20)))
ForAll(((x2_s_B3 | fin) | (l_s_B10 | manual)) => Exist(x2_e_B2))
ForAll(~((x2_s_B6) ^ (x2_e_B6)))
ForAll(~((tau_B17) ^ (x2_e_B7)))
ForAll(((tau_B19) | (l_s_B14 | delete)) => Exist(x2_e_B9))
ForAll(~((a2_s_B0 | x2_e_B9) ^ (x2_e_B0)))
ForAll(~((tau_B2) ^ (x3_s_B4 | x3_e_B4)))
Exist(a2_s_B0 | x2_e_B8)
ForAll(~((l_s_B15 | join_pat) ^ (x2_e_B0)))
Exist(x2_s_B3 | x2_e_B3)
ForAll((x2_s_B1 | x2_e_B1) => Exist(x2_s_B7 | x2_e_B7))
Exist(l_s_B8)
ForAll((tau_B7) => Exist(reject))
Exist(l_s_B4)
ForAll((tau_B9) => Exist(reopen))
ForAll((billed) => ((Exist(tau_B1) ^ Exist(billed)) | (~(Exist(tau_B1)))))
ForAll((tau_B0) => Exist(new))
Exist(a2_s_B0 | a2_e_B0)
Exist(a2_s_B1)
ForAll((a2_s_B2 | a2_e_B2) => Exist(a2_e_B1))
ForAll(~((a2_s_B0 | a2_e_B0) ^ (x2_s_B8 | x2_e_B8)))
ForAll((l_s_B0) => Exist(new))
Exist(x2_s_B9)
ForAll(~((x2_s_B6) ^ (l_s_B6 | reopen)))
ForAll(~((l_s_B0) ^ (tau_B0)))
Exist(l_s_B6)
ForAll((x2_s_B1 | x2_e_B7) => Exist(a2_e_B0))
ForAll(~((x2_s_B5 | a2_e_B1) ^ (x2_s_B6 | x2_e_B6)))
ForAll(~((l_s_B11) ^ (tau_B14)))
ForAll(((tau_B2) | (x3_s_B4 | x3_e_B4)) => Exist(x2_e_B3))
ForAll((reject) => ((Exist(tau_B7) ^ Exist(reject)) | (~(Exist(tau_B7)))))
Exist(x2_s_B5 | x2_e_B5)
ForAll((tau_B20) => Exist(delete))
Exist(l_s_B1)
ForAll(~((x2_s_B5 | x2_e_B6) ^ (l_s_B7 | change_diagn)))
ForAll(~((billed) ^ (tau_B1)))
ForAll(~((tau_B8) ^ (x2_e_B6)))
ForAll(~((l_s_B4) ^ (tau_B6)))
ForAll((x2_s_B5 | a2_e_B1) => Exist(x2_s_B6 | x2_e_B6))
ForAll((delete) => ((Exist(tau_B20) ^ Exist(delete)) | (~(Exist(tau_B20)))))
ForAll(~((x2_s_B3) ^ (x3_s_B4 | x3_e_B4)))
ForAll(~((l_s_B5) ^ (reject)))
ForAll(~((l_s_B7) ^ (change_diagn)))
ForAll((x2_s_B1) => ((Exist(x2_s_B2 | code_ok) ^ ~(Exist(l_s_B13 | set_status))) | (~(Exist(x2_s_B2 | code_ok)) ^ Exist(l_s_B13 | set_status))))
ForAll(~((l_s_B6 | reopen) ^ (x2_e_B6)))
ForAll((tau_B13) => Exist(manual))
ForAll(~((x2_s_B0) ^ (l_s_B15 | join_pat)))
ForAll((tau_B10) => Exist(change_diagn))
ForAll(~((l_s_B7 | change_diagn) ^ (x3_e_B4)))
ForAll(~((l_s_B10 | manual) ^ (x2_e_B2)))
Exist(a2_s_B2)
ForAll(~((l_s_B3) ^ (storno)))
ForAll(~((change_diagn) ^ (tau_B10)))
ForAll(~((tau_B3) ^ (x2_e_B5)))
ForAll((l_s_B5 | reject) => Exist(a2_e_B2))
ForAll((tau_B11) => Exist(change_end))
ForAll(~((manual) ^ (tau_B13)))
ForAll(~((set_status) ^ (tau_B16)))
ForAll(~((zdbc_behan) ^ (x2_e_B7)))
ForAll(~((l_s_B0) ^ (new)))
ForAll(~((reject) ^ (tau_B7)))
ForAll(~((x2_s_B8) ^ (empty)))
ForAll((manual) => ((Exist(tau_B13) ^ Exist(manual)) | (~(Exist(tau_B13)))))
ForAll(~((x2_s_B2) ^ (x2_s_B3 | fin)))
ForAll(~((x2_s_B3) ^ (x2_e_B3)))
ForAll((x2_s_B2 | x2_e_B2) => Exist(l_s_B11 | release))
ForAll((x2_s_B9) => ((Exist(tau_B19) ^ ~(Exist(l_s_B14 | delete))) | (~(Exist(tau_B19)) ^ Exist(l_s_B14 | delete))))
ForAll(~((a2_s_B1) ^ ((l_s_B3 | storno) | (a2_s_B2 | a2_e_B2))))
ForAll(~((l_s_B6) ^ (tau_B9)))
ForAll(~((l_s_B3) ^ (tau_B5)))
ForAll(((a2_s_B0 | x2_e_B9) | (l_s_B15 | join_pat)) => Exist(x2_e_B0))
ForAll((code_error) => ((Exist(tau_B4) ^ Exist(code_error)) | (~(Exist(tau_B4)))))
ForAll(~((x2_s_B1) ^ (x2_e_B1)))
ForAll(~((l_s_B0 | new) ^ (x2_s_B0 | x2_e_B0)))
ForAll(~((x2_s_B2 | x2_e_B2) ^ (l_s_B11 | release)))
ForAll(~((x2_s_B9) ^ (l_s_B14 | delete)))
ForAll((tau_B4) => Exist(code_error))
ForAll((change_diagn) => ((Exist(tau_B10) ^ Exist(change_diagn)) | (~(Exist(tau_B10)))))
ForAll((l_s_B15) => Exist(join_pat))
ForAll(~((l_s_B15) ^ (join_pat)))
ForAll((x2_s_B0) => ((Exist(a2_s_B0 | x2_e_B9) ^ ~(Exist(l_s_B15 | join_pat))) | (~(Exist(a2_s_B0 | x2_e_B9)) ^ Exist(l_s_B15 | join_pat))))
ForAll((a2_s_B0) => (Exist(l_s_B1 | billed) ^ Exist(x2_s_B1 | x2_e_B7)))
Exist(x3_s_B4)
ForAll(~((l_s_B1) ^ (billed)))
Exist(l_s_B13)
ForAll((tau_B12) => Exist(fin))
ForAll(~((l_s_B12) ^ (tau_B15)))
ForAll(~((l_s_B8 | change_end) ^ (x3_e_B4)))
Exist(l_s_B12)
ForAll((l_s_B5) => Exist(reject))
ForAll(~((x2_s_B2 | x2_e_B2) ^ (l_s_B12 | code_ok)))
Exist(l_s_B0 | new)
ForAll(~((empty) ^ (x2_e_B8)))
ForAll(~((a2_s_B0 | x2_e_B8) ^ (x2_s_B9 | x2_e_B9)))
Exist(x2_s_B5 | a2_e_B1)
ForAll(~((l_s_B2) ^ (tau_B4)))
Exist(l_s_B11)
ForAll(~((join_pat) ^ (tau_B21)))
ForAll(~((x2_s_B2) ^ (l_s_B10 | manual)))
ForAll(~((x2_s_B5 | x2_e_B6) ^ (x3_e_B4)))
ForAll((a2_s_B2) => (Exist(l_s_B4 | code_nok) ^ Exist(l_s_B5 | reject)))
Exist(x2_s_B0)
Exist(a2_s_B0)
ForAll((code_nok) => ((Exist(tau_B6) ^ Exist(code_nok)) | (~(Exist(tau_B6)))))
ForAll(~((l_s_B15) ^ (tau_B21)))
Exist(x2_s_B7)
ForAll(~((x2_s_B3 | fin) ^ (l_s_B10 | manual)))
Exist(l_s_B10)
Exist(x2_s_B1)
ForAll(~((l_s_B14 | delete) ^ (x2_e_B9)))
ForAll(~((x2_s_B5) ^ (x2_e_B5)))
ForAll(~((x2_s_B6) ^ (tau_B8)))
ForAll(~((a2_s_B0 | x2_e_B9) ^ (l_s_B15 | join_pat)))
ForAll((l_s_B11 | release) => Exist(l_s_B12 | code_ok))
Exist(x2_s_B2)
ForAll((storno) => ((Exist(tau_B5) ^ Exist(storno)) | (~(Exist(tau_B5)))))
ForAll(~((code_nok) ^ (tau_B6)))
ForAll(~((code_ok) ^ (tau_B15)))
ForAll(~((tau_B17) ^ (zdbc_behan)))
ForAll(((tau_B3) | (l_s_B2 | code_error)) => Exist(x2_e_B5))
ForAll((l_s_B3) => Exist(storno))
ForAll(~((fin) ^ (tau_B12)))
ForAll(~((tau_B18) ^ (x2_e_B8)))
ForAll((l_s_B11) => Exist(release))
ForAll((a2_s_B1) => (Exist(l_s_B3 | storno) ^ Exist(a2_s_B2 | a2_e_B2)))
ForAll((l_s_B12) => Exist(code_ok))
ForAll(~((a2_s_B0) ^ ((l_s_B1 | billed) | (x2_s_B1 | x2_e_B7))))
ForAll(~((x3_s_B4) ^ (x2_s_B5 | x2_e_B6)))
ForAll(~((reopen) ^ (tau_B9)))
ForAll((l_s_B3 | storno) => Exist(a2_e_B1))
ForAll((x2_s_B3 | x2_e_B3) => Exist(l_s_B9 | fin))
ForAll(~((l_s_B13 | set_status) ^ (x2_e_B1)))
ForAll(~((x2_s_B8) ^ (x2_e_B8)))
ForAll(~((x3_s_B4) ^ (l_s_B7 | change_diagn)))
ForAll(~((l_s_B11) ^ (release)))
ForAll(~((tau_B19) ^ (l_s_B14 | delete)))
ForAll(~((x3_s_B4 | x3_e_B4) ^ (x2_e_B3)))
ForAll((l_s_B1) => Exist(billed))
ForAll((l_s_B8) => Exist(change_end))
ForAll((release) => ((Exist(tau_B14) ^ Exist(release)) | (~(Exist(tau_B14)))))
ForAll((set_status) => ((Exist(tau_B16) ^ Exist(set_status)) | (~(Exist(tau_B16)))))
ForAll(~((l_s_B10) ^ (tau_B13)))
ForAll(~((x2_s_B3 | fin) ^ (x2_e_B2)))
ForAll(((x2_s_B5 | x2_e_B6) | (l_s_B7 | change_diagn) | (l_s_B8 | change_end)) => Exist(x3_e_B4))
ForAll((x2_s_B8) => ((Exist(tau_B18) ^ ~(Exist(empty))) | (~(Exist(tau_B18)) ^ Exist(empty))))
ForAll(((tau_B8) | (l_s_B6 | reopen)) => Exist(x2_e_B6))
ForAll((tau_B15) => Exist(code_ok))
ForAll(~((tau_B8) ^ (l_s_B6 | reopen)))
ForAll(~((code_error) ^ (tau_B4)))