ForAll(~((tau_10) ^ (a2_s_2 | a2_e_2)))
ForAll((x2_s_4 | x2_e_4) => Exist(a2_e_1))
ForAll(~((a2_s_1) ^ ((x2_s_3 | x2_e_3) | (x2_s_4 | x2_e_4))))
ForAll(~((tau_21) ^ (x2_e_17)))
ForAll((x2_s_8) => ((Exist(tau_10) ^ ~(Exist(a2_s_2 | a2_e_2))) | (~(Exist(tau_10)) ^ Exist(a2_s_2 | a2_e_2))))
ForAll(~((tau_4) ^ (a2_s_1 | x2_e_23)))
ForAll((l_s_5) => Exist(release))
ForAll(~((x2_s_18) ^ (x2_e_18)))
ForAll((x2_s_3) => ((Exist(tau_5) ^ ~(Exist(l_s_2 | join_pat))) | (~(Exist(tau_5)) ^ Exist(l_s_2 | join_pat))))
ForAll(~((l_s_2) ^ (tau_6)))
ForAll(~((x2_s_12 | x2_e_12) ^ (x2_e_11)))
ForAll(((manual) | (code_ok)) => Exist(x2_e_12))
ForAll((join_pat) => ((Exist(tau_6) ^ Exist(join_pat)) | (~(Exist(tau_6)))))
ForAll(~((x2_s_7) ^ (x2_e_7)))
ForAll(~((l_s_6) ^ (tau_18)))
ForAll(~((tau_17) ^ (x2_e_14)))
ForAll(~((tau_27) ^ (x2_e_20)))
ForAll(~((release) ^ (tau_14)))
ForAll((tau_18) => Exist(code_nok))
ForAll(~((tau_30) ^ (l_s_10 | delete)))
ForAll(~((tau_13) ^ (l_s_5 | release)))
ForAll(~((change_diagn) ^ (x3_e_6)))
ForAll(~((l_s_6 | code_nok) ^ (x2_e_14)))
ForAll(~((a2_s_3) ^ ((x2_s_14 | x2_e_14) | (x2_s_15 | x2_e_15))))
ForAll((l_s_0) => Exist(new))
ForAll(~((change_end) ^ (x3_e_6)))
ForAll(~((tau_25) ^ (l_s_9 | reopen)))
ForAll(~((x2_s_20) ^ (fin)))
ForAll((x2_s_15 | x2_e_15) => Exist(a2_e_3))
Exist(l_s_10)
ForAll(~((l_s_8) ^ (tau_22)))
ForAll(~((x2_s_14) ^ (x2_e_14)))
ForAll(~(((x2_s_19 | x2_e_19) | (x2_s_20 | x2_e_20)) ^ (a2_e_4)))
ForAll((x2_s_10 | x2_e_10) => Exist(x2_s_11 | x2_e_11))
ForAll(~((x2_s_16) ^ (l_s_7 | x2_e_17)))
ForAll(~((tau_15) ^ (x2_s_12 | x2_e_12)))
ForAll(~((x2_s_22) ^ (l_s_10 | delete)))
ForAll(~((a2_s_4 | a2_e_4) ^ (x2_e_18)))
ForAll((storno) => Exist(x2_s_17 | x2_e_17))
ForAll(~((fin) ^ (x2_e_20)))
ForAll(~((x2_s_14) ^ (l_s_6 | code_nok)))
ForAll(~((tau_20) ^ (x2_e_16)))
ForAll(~((x2_s_2) ^ (a2_s_1 | x2_e_23)))
ForAll(~((tau_11) ^ (l_s_4 | code_error)))
ForAll(~((x2_s_7) ^ (set_status)))
ForAll((x2_s_4) => ((Exist(tau_7) ^ ~(Exist(x2_s_5 | x2_e_22))) | (~(Exist(tau_7)) ^ Exist(x2_s_5 | x2_e_22))))
ForAll((l_s_9) => Exist(reopen))
ForAll(~((x2_s_7 | x2_e_8) ^ (change_end)))
Exist(l_s_6)
ForAll((l_s_3) => Exist(x3_s_6 | x3_e_6))
Exist(l_s_8)
ForAll(~((x2_s_5) ^ (tau_8)))
ForAll((release) => ((Exist(tau_14) ^ Exist(release)) | (~(Exist(tau_14)))))
Exist(x2_s_5 | x2_e_5)
ForAll((l_s_6) => Exist(code_nok))
ForAll((x2_s_17) => ((Exist(tau_21) ^ ~(Exist(l_s_8 | reject))) | (~(Exist(tau_21)) ^ Exist(l_s_8 | reject))))
ForAll(~((x2_s_20) ^ (x2_e_20)))
ForAll(~((l_s_5 | release) ^ (x2_e_10)))
Exist(l_s_0 | new)
ForAll((x2_s_11 | x2_e_11) => Exist(x2_s_13 | x2_e_13))
ForAll((new) => ((Exist(tau_0) ^ Exist(new)) | (~(Exist(tau_0)))))
ForAll((delete) => ((Exist(tau_31) ^ Exist(delete)) | (~(Exist(tau_31)))))
ForAll(~((x2_s_20) ^ (tau_27)))
ForAll(~((l_s_8 | reject) ^ (x2_e_17)))
ForAll((tau_3) => Exist(billed))
ForAll(~((x2_s_19) ^ (l_s_9 | reopen)))
ForAll(~(((x2_s_9 | x2_e_9) | (x2_s_10 | x2_e_13)) ^ (a2_e_2)))
Exist(x2_s_16)
ForAll(~((empty) ^ (x2_e_21)))
ForAll((l_s_2) => Exist(join_pat))
Exist(l_s_9)
ForAll(((tau_1) | (a2_s_0 | a2_e_0)) => Exist(x2_e_0))
ForAll(~((storno) ^ (x2_s_17 | x2_e_17)))
Exist(x2_s_21)
ForAll(~((x2_s_23) ^ (tau_32)))
ForAll(~((l_s_5) ^ (tau_14)))
ForAll(~((reject) ^ (tau_22)))
ForAll(~((x2_s_11) ^ (x2_e_11)))
ForAll(~((l_s_0) ^ (new)))
ForAll((x2_s_10) => ((Exist(tau_13) ^ ~(Exist(l_s_5 | release))) | (~(Exist(tau_13)) ^ Exist(l_s_5 | release))))
ForAll(~((tau_20) ^ (l_s_7 | x2_e_17)))
ForAll((x2_s_20) => ((Exist(tau_27) ^ ~(Exist(fin))) | (~(Exist(tau_27)) ^ Exist(fin))))
ForAll(~((tau_5) ^ (l_s_2 | join_pat)))
ForAll(~((x2_s_4) ^ (x2_s_5 | x2_e_22)))
ForAll(~((a2_s_2) ^ ((x2_s_9 | x2_e_9) | (x2_s_10 | x2_e_13))))
ForAll(~((l_s_8) ^ (reject)))
ForAll(~((x2_s_8) ^ (tau_10)))
ForAll(((tau_17) | (l_s_6 | code_nok)) => Exist(x2_e_14))
ForAll((a2_s_3) => (Exist(x2_s_14 | x2_e_14) ^ Exist(x2_s_15 | x2_e_15)))
ForAll((storno | x2_e_17) => ((Exist(tau_23) ^ Exist(storno | x2_e_17)) | (~(Exist(tau_23)))))
ForAll(~((code_error) ^ (tau_12)))
ForAll(((tau_29) | (empty)) => Exist(x2_e_21))
ForAll(~((l_s_1) ^ (tau_3)))
ForAll((l_s_0 | new) => Exist(x2_s_0 | x2_e_0))
ForAll((x2_s_12) => ((Exist(manual) ^ ~(Exist(code_ok))) | (~(Exist(manual)) ^ Exist(code_ok))))
ForAll((x2_s_11) => ((Exist(tau_15) ^ ~(Exist(x2_s_12 | x2_e_12))) | (~(Exist(tau_15)) ^ Exist(x2_s_12 | x2_e_12))))
Exist(l_s_4)
ForAll((x2_s_13) => ((Exist(tau_16) ^ ~(Exist(a2_s_3 | a2_e_3))) | (~(Exist(tau_16)) ^ Exist(a2_s_3 | a2_e_3))))
ForAll((tau_6) => Exist(join_pat))
ForAll(~((x2_s_10 | x2_e_10) ^ (x2_s_13 | x2_e_13)))
ForAll(~((a2_s_3 | a2_e_3) ^ (x2_e_13)))
ForAll(~(((x2_s_1 | x2_e_1) | (x2_s_2 | x2_e_2)) ^ (a2_e_0)))
ForAll(~((tau_5) ^ (x2_e_3)))
ForAll((x2_s_16 | x2_e_16) => Exist(x2_s_18 | x2_e_18))
Exist(a2_s_1)
Exist(a2_s_4)
ForAll((tau_0) => Exist(new))
ForAll((tau_22) => Exist(reject))
ForAll(~((tau_11) ^ (x2_e_9)))
ForAll(~((storno | x2_e_17) ^ (tau_23)))
ForAll(~((x2_s_17) ^ (x2_e_17)))
ForAll((x2_s_20 | x2_e_20) => Exist(a2_e_4))
ForAll((billed) => ((Exist(tau_3) ^ Exist(billed)) | (~(Exist(tau_3)))))
ForAll(~((x2_s_16) ^ (x2_e_16)))
ForAll(~((code_ok) ^ (x2_e_12)))
ForAll(~((x2_s_8) ^ (x2_e_8)))
ForAll((x2_s_23) => ((Exist(tau_32) ^ ~(Exist(zdbc_behan))) | (~(Exist(tau_32)) ^ Exist(zdbc_behan))))
ForAll(((tau_21) | (l_s_8 | reject)) => Exist(x2_e_17))
ForAll(~((l_s_1) ^ (billed)))
ForAll(~((x2_s_4) ^ (tau_7)))
ForAll(((tau_16) | (a2_s_3 | a2_e_3)) => Exist(x2_e_13))
ForAll((tau_23) => Exist(storno | x2_e_17))
ForAll(~((x2_s_10) ^ (x2_e_10)))
ForAll(((x2_s_7 | x2_e_8) | (change_end) | (change_diagn)) => Exist(x3_e_6))
ForAll((x2_s_1 | x2_e_1) => Exist(a2_e_0))
Exist(x2_s_7)
ForAll(~((a2_s_0 | a2_e_0) ^ (x2_e_0)))
Exist(x2_s_23)
ForAll(~((x2_s_3) ^ (l_s_2 | join_pat)))
ForAll(~((x2_s_11) ^ (x2_s_12 | x2_e_12)))
ForAll(~((x2_s_0) ^ (x2_e_0)))
Exist(a2_s_1 | a2_e_1)
ForAll(~((tau_7) ^ (x2_e_4)))
Exist(l_s_0)
ForAll(~((x2_s_17) ^ (l_s_8 | reject)))
ForAll((tau_26) => Exist(reopen))
ForAll(~((l_s_3 | x3_e_6) ^ (x2_s_21 | x2_e_21)))
Exist(x2_s_16 | x2_e_16)
ForAll((l_s_4) => Exist(code_error))
ForAll(((tau_27) | (fin)) => Exist(x2_e_20))
Exist(l_s_3)
ForAll(~((tau_17) ^ (l_s_6 | code_nok)))
ForAll(~((x2_s_7) ^ (tau_9)))
ForAll(~((billed) ^ (tau_3)))
ForAll(~((l_s_7) ^ (storno | x2_e_17)))
ForAll(~((delete) ^ (tau_31)))
ForAll(~((x2_s_19) ^ (x2_e_19)))
ForAll((tau_31) => Exist(delete))
ForAll(~((x2_s_8) ^ (a2_s_2 | a2_e_2)))
Exist(l_s_2)
ForAll(((tau_19) | (x2_s_16 | x2_e_18)) => Exist(x2_e_15))
Exist(x2_s_3)
ForAll(~((x2_s_0) ^ (a2_s_0 | a2_e_0)))
ForAll(~((x2_s_18) ^ (tau_24)))
ForAll(((tau_15) | (x2_s_12 | x2_e_12)) => Exist(x2_e_11))
ForAll(~((a2_s_0) ^ ((x2_s_1 | x2_e_1) | (x2_s_2 | x2_e_2))))
ForAll((x3_s_6 | x3_e_6) => ((Exist(tau_28) ^ Exist(x3_s_6 | x3_e_6)) | (~(Exist(tau_28)))))
ForAll((x2_s_9) => ((Exist(tau_11) ^ ~(Exist(l_s_4 | code_error))) | (~(Exist(tau_11)) ^ Exist(l_s_4 | code_error))))
ForAll(~((tau_24) ^ (a2_s_4 | a2_e_4)))
ForAll((a2_s_2) => (Exist(x2_s_9 | x2_e_9) ^ Exist(x2_s_10 | x2_e_13)))
ForAll(~((x2_s_0) ^ (tau_1)))
ForAll(~((x2_s_15) ^ (tau_19)))
ForAll(~((x2_s_22) ^ (tau_30)))
ForAll(~((x2_s_16 | x2_e_16) ^ (x2_s_18 | x2_e_18)))
ForAll(((tau_4) | (a2_s_1 | x2_e_23)) => Exist(x2_e_2))
ForAll(~((tau_9) ^ (set_status)))
ForAll(((tau_30) | (l_s_10 | delete)) => Exist(x2_e_22))
ForAll(~((l_s_9) ^ (reopen)))
ForAll(~((tau_16) ^ (x2_e_13)))
ForAll((a2_s_1) => (Exist(x2_s_3 | x2_e_3) ^ Exist(x2_s_4 | x2_e_4)))
ForAll(((tau_7) | (x2_s_5 | x2_e_22)) => Exist(x2_e_4))
ForAll((x2_s_3 | x2_e_3) => Exist(a2_e_1))
ForAll(~((change_end) ^ (change_diagn)))
ForAll(((tau_13) | (l_s_5 | release)) => Exist(x2_e_10))
ForAll(~((x2_s_12) ^ (x2_e_12)))
ForAll(~((x2_s_13) ^ (x2_e_13)))
ForAll(((tau_25) | (l_s_9 | reopen)) => Exist(x2_e_19))
ForAll((x2_s_2) => ((Exist(tau_4) ^ ~(Exist(a2_s_1 | x2_e_23))) | (~(Exist(tau_4)) ^ Exist(a2_s_1 | x2_e_23))))
ForAll(~((x2_s_1) ^ (x2_e_1)))
ForAll(~((code_nok) ^ (tau_18)))
ForAll((x2_s_18) => ((Exist(tau_24) ^ ~(Exist(a2_s_4 | a2_e_4))) | (~(Exist(tau_24)) ^ Exist(a2_s_4 | a2_e_4))))
ForAll((x2_s_14) => ((Exist(tau_17) ^ ~(Exist(l_s_6 | code_nok))) | (~(Exist(tau_17)) ^ Exist(l_s_6 | code_nok))))
ForAll(~((x2_s_1) ^ (l_s_1 | billed)))
Exist(x2_s_8)
ForAll(~((tau_13) ^ (x2_e_10)))
ForAll(~((x2_s_21) ^ (empty)))
ForAll(~((set_status) ^ (x2_e_7)))
ForAll(~((x2_s_22) ^ (x2_e_22)))
Exist(x2_s_5)
ForAll(~((tau_2) ^ (l_s_1 | billed)))
ForAll(~((x2_s_3) ^ (x2_e_3)))
ForAll(~((tau_7) ^ (x2_s_5 | x2_e_22)))
ForAll(~((l_s_0) ^ (tau_0)))
ForAll(~((x2_s_21) ^ (tau_29)))
ForAll((l_s_10) => Exist(delete))
ForAll((x2_s_19) => ((Exist(tau_25) ^ ~(Exist(l_s_9 | reopen))) | (~(Exist(tau_25)) ^ Exist(l_s_9 | reopen))))
ForAll(~((x2_s_5 | x2_e_22) ^ (x2_e_4)))
ForAll(~((x2_s_15) ^ (x2_e_15)))
ForAll(~((tau_27) ^ (fin)))
ForAll(~((x2_s_11) ^ (tau_15)))
ForAll((x2_s_2 | x2_e_2) => Exist(a2_e_0))
ForAll(~((x2_s_9) ^ (tau_11)))
ForAll((x2_s_5) => ((Exist(tau_8) ^ ~(Exist(l_s_3 | x2_e_21))) | (~(Exist(tau_8)) ^ Exist(l_s_3 | x2_e_21))))
ForAll((l_s_7) => Exist(storno | x2_e_17))
Exist(x2_s_20)
ForAll(((tau_10) | (a2_s_2 | a2_e_2)) => Exist(x2_e_8))
Exist(l_s_1)
ForAll(~((a2_s_1 | a2_e_1) ^ (x2_s_23 | x2_e_23)))
Exist(x2_s_17)
ForAll(~((reopen) ^ (tau_26)))
ForAll((tau_28) => Exist(x3_s_6 | x3_e_6))
ForAll(~((l_s_6) ^ (code_nok)))
ForAll(~((x3_s_6) ^ (x3_e_6)))
ForAll(~((tau_4) ^ (x2_e_2)))
ForAll((a2_s_0) => (Exist(x2_s_1 | x2_e_1) ^ Exist(x2_s_2 | x2_e_2)))
ForAll(~((x2_s_7 | x2_e_7) ^ (x2_s_8 | x2_e_8)))
ForAll(~((x2_s_16) ^ (tau_20)))
ForAll(~((l_s_3) ^ (x3_s_6 | x3_e_6)))
ForAll(((tau_8) | (l_s_3 | x2_e_21)) => Exist(x2_e_5))
Exist(x2_s_12)
Exist(a2_s_2)
ForAll((a2_s_4) => (Exist(x2_s_19 | x2_e_19) ^ Exist(x2_s_20 | x2_e_20)))
ForAll(((tau_24) | (a2_s_4 | a2_e_4)) => Exist(x2_e_18))
Exist(x2_s_4)
ForAll((code_nok) => ((Exist(tau_18) ^ Exist(code_nok)) | (~(Exist(tau_18)))))
ForAll((l_s_8) => Exist(reject))
ForAll(~((x3_s_6) ^ (x2_s_7 | x2_e_8)))
ForAll(~((x2_s_1) ^ (tau_2)))
ForAll((x2_s_9 | x2_e_9) => Exist(a2_e_2))
ForAll(~((tau_19) ^ (x2_e_15)))
ForAll(~((tau_30) ^ (x2_e_22)))
Exist(x2_s_9)
ForAll(~((l_s_9 | reopen) ^ (x2_e_19)))
ForAll(~((x2_s_7 | x2_e_8) ^ (change_diagn)))
ForAll(~((l_s_4 | code_error) ^ (x2_e_9)))
ForAll(~((x2_s_7 | x2_e_8) ^ (x3_e_6)))
ForAll(~((join_pat) ^ (tau_6)))
ForAll(~((x2_s_19) ^ (tau_25)))
ForAll(~((x2_s_21) ^ (x2_e_21)))
ForAll((reject) => ((Exist(tau_22) ^ Exist(reject)) | (~(Exist(tau_22)))))
ForAll(~((tau_21) ^ (l_s_8 | reject)))
ForAll(~((x2_s_2) ^ (x2_e_2)))
ForAll(~((tau_19) ^ (x2_s_16 | x2_e_18)))
ForAll(~((a2_s_2 | a2_e_2) ^ (x2_e_8)))
Exist(x2_s_15)
ForAll(~((x2_s_13) ^ (tau_16)))
Exist(x2_s_22)
ForAll(~((l_s_10) ^ (delete)))
Exist(x2_s_19)
ForAll(~((tau_25) ^ (x2_e_19)))
ForAll((x3_s_6) => ((Exist(x2_s_7 | x2_e_8) ^ ~(Exist(change_end)) ^ ~(Exist(change_diagn))) | ((~(Exist(x2_s_7 | x2_e_8)) ^ Exist(change_end) ^ ~(Exist(change_diagn))) | (~(Exist(x2_s_7 | x2_e_8)) ^ ~(Exist(change_end)) ^ Exist(change_diagn)))))
Exist(a2_s_3)
ForAll(~((x2_s_2) ^ (tau_4)))
ForAll(~((tau_1) ^ (a2_s_0 | a2_e_0)))
ForAll(((tau_32) | (zdbc_behan)) => Exist(x2_e_23))
ForAll(~((l_s_2) ^ (join_pat)))
ForAll(((tau_9) | (set_status)) => Exist(x2_e_7))
ForAll((x2_s_7 | x2_e_7) => Exist(x2_s_8 | x2_e_8))
ForAll(~((tau_8) ^ (x2_e_5)))
Exist(a2_s_0)
ForAll(~((x3_s_6) ^ (change_end)))
ForAll(~((x2_s_16 | x2_e_18) ^ (x2_e_15)))
ForAll((tau_14) => Exist(release))
ForAll(~((l_s_7 | x2_e_17) ^ (x2_e_16)))
Exist(x2_s_7 | x2_e_7)
ForAll(~((x2_s_13) ^ (a2_s_3 | a2_e_3)))
ForAll(((tau_5) | (l_s_2 | join_pat)) => Exist(x2_e_3))
ForAll(~((tau_16) ^ (a2_s_3 | a2_e_3)))
ForAll(~((tau_32) ^ (zdbc_behan)))
ForAll(~((x2_s_17) ^ (tau_21)))
ForAll((x2_s_14 | x2_e_14) => Exist(a2_e_3))
ForAll(~((manual) ^ (code_ok)))
ForAll(~((x2_s_9) ^ (x2_e_9)))
ForAll((tau_12) => Exist(code_error))
Exist(x2_s_11)
ForAll(~((x2_s_9) ^ (l_s_4 | code_error)))
Exist(l_s_3 | x3_e_6)
Exist(x2_s_14)
ForAll(~((x2_s_10 | x2_e_10) ^ (x2_s_11 | x2_e_11)))
ForAll(~((x2_s_23) ^ (zdbc_behan)))
ForAll(~((x2_s_23) ^ (x2_e_23)))
Exist(x2_s_10 | x2_e_10)
ForAll(~((a2_s_4) ^ ((x2_s_19 | x2_e_19) | (x2_s_20 | x2_e_20))))
ForAll(~((x2_s_5) ^ (l_s_3 | x2_e_21)))
Exist(x2_s_0)
ForAll(~((x2_s_10) ^ (tau_13)))
ForAll(~((l_s_0 | new) ^ (x2_s_0 | x2_e_0)))
ForAll(((tau_20) | (l_s_7 | x2_e_17)) => Exist(x2_e_16))
ForAll((reopen) => ((Exist(tau_26) ^ Exist(reopen)) | (~(Exist(tau_26)))))
ForAll(~((x2_s_5) ^ (x2_e_5)))
ForAll((x2_s_22) => ((Exist(tau_30) ^ ~(Exist(l_s_10 | delete))) | (~(Exist(tau_30)) ^ Exist(l_s_10 | delete))))
ForAll(~((x2_s_18) ^ (a2_s_4 | a2_e_4)))
ForAll(~((tau_10) ^ (x2_e_8)))
ForAll((l_s_1) => Exist(billed))
ForAll(~((tau_8) ^ (l_s_3 | x2_e_21)))
ForAll(~((x2_s_4) ^ (x2_e_4)))
ForAll(~((tau_15) ^ (x2_e_11)))
ForAll(((tau_11) | (l_s_4 | code_error)) => Exist(x2_e_9))
ForAll((x2_s_0) => ((Exist(tau_1) ^ ~(Exist(a2_s_0 | a2_e_0))) | (~(Exist(tau_1)) ^ Exist(a2_s_0 | a2_e_0))))
ForAll(~((l_s_4) ^ (tau_12)))
Exist(x2_s_10)
ForAll((x2_s_19 | x2_e_19) => Exist(a2_e_4))
ForAll(~((l_s_5) ^ (release)))
ForAll(~((x2_s_12) ^ (manual)))
ForAll(~((tau_2) ^ (x2_e_1)))
ForAll(~(((x2_s_14 | x2_e_14) | (x2_s_15 | x2_e_15)) ^ (a2_e_3)))
ForAll(~((x2_s_3) ^ (tau_5)))
ForAll(~((x2_s_14) ^ (tau_17)))
ForAll(~((tau_29) ^ (empty)))
ForAll(~((tau_1) ^ (x2_e_0)))
ForAll(~((l_s_4) ^ (code_error)))
ForAll(~((l_s_10) ^ (tau_31)))
ForAll((x2_s_1) => ((Exist(tau_2) ^ ~(Exist(l_s_1 | billed))) | (~(Exist(tau_2)) ^ Exist(l_s_1 | billed))))
ForAll(~((l_s_10 | delete) ^ (x2_e_22)))
Exist(l_s_7)
ForAll(~((l_s_3 | x2_e_21) ^ (x2_e_5)))
ForAll(~((tau_24) ^ (x2_e_18)))
ForAll(~((x3_s_6) ^ (change_diagn)))
ForAll((a2_s_1 | a2_e_1) => Exist(x2_s_23 | x2_e_23))
ForAll(~((x2_s_11 | x2_e_11) ^ (x2_s_13 | x2_e_13)))
ForAll(~((l_s_1 | billed) ^ (x2_e_1)))
Exist(x3_s_6)
ForAll((l_s_3 | x3_e_6) => Exist(x2_s_21 | x2_e_21))
ForAll(~((manual) ^ (x2_e_12)))
ForAll(~((tau_9) ^ (x2_e_7)))
ForAll(~((x2_s_15) ^ (x2_s_16 | x2_e_18)))
ForAll(~((x3_s_6 | x3_e_6) ^ (tau_28)))
ForAll((code_error) => ((Exist(tau_12) ^ Exist(code_error)) | (~(Exist(tau_12)))))
ForAll(~((l_s_9) ^ (tau_26)))
ForAll((x2_s_16) => ((Exist(tau_20) ^ ~(Exist(l_s_7 | x2_e_17))) | (~(Exist(tau_20)) ^ Exist(l_s_7 | x2_e_17))))
Exist(x2_s_1)
ForAll(~((x2_s_12) ^ (code_ok)))
ForAll(((tau_2) | (l_s_1 | billed)) => Exist(x2_e_1))
Exist(l_s_5)
ForAll(~((l_s_7) ^ (tau_23)))
ForAll(~((l_s_3) ^ (tau_28)))
ForAll(~((tau_29) ^ (x2_e_21)))
Exist(x2_s_2)
ForAll(~((l_s_2 | join_pat) ^ (x2_e_3)))
Exist(x2_s_13)
ForAll(~((x2_s_5 | x2_e_5) ^ (x2_s_22 | x2_e_22)))
ForAll((x2_s_21) => ((Exist(tau_29) ^ ~(Exist(empty))) | (~(Exist(tau_29)) ^ Exist(empty))))
ForAll((x2_s_7) => ((Exist(tau_9) ^ ~(Exist(set_status))) | (~(Exist(tau_9)) ^ Exist(set_status))))
ForAll((x2_s_10 | x2_e_13) => Exist(a2_e_2))
Exist(storno)
ForAll(~((zdbc_behan) ^ (x2_e_23)))
ForAll((x2_s_5 | x2_e_5) => Exist(x2_s_22 | x2_e_22))
ForAll((x2_s_15) => ((Exist(tau_19) ^ ~(Exist(x2_s_16 | x2_e_18))) | (~(Exist(tau_19)) ^ Exist(x2_s_16 | x2_e_18))))
ForAll(~((x2_s_10) ^ (l_s_5 | release)))
ForAll(~((tau_32) ^ (x2_e_23)))
ForAll(~(((x2_s_3 | x2_e_3) | (x2_s_4 | x2_e_4)) ^ (a2_e_1)))
ForAll(~((a2_s_1 | x2_e_23) ^ (x2_e_2)))
ForAll(~((new) ^ (tau_0)))
Exist(x2_s_18)