Safe Haskell | Safe |
---|
Testing Var Int
Satisfiable CNF formula. \[(x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)\]
>>>
fml2
[[+1,-2,-3,+4]]
Satisfiable CNF formula. \[(x_1 \vee \neg x_3) \wedge (x_1 \vee x_4 \vee \neg x_5) \wedge (x_2 \vee x_3 \vee x_4) \wedge (\neg x_1 \vee \neg x_3 \vee \neg x_5) \wedge (x_4 \vee x_5) \wedge (\neg x_3 \vee \neg x_4 \vee x_5) \wedge (x_2)\]
>>>
fml3
[[+1,-3],[+1,+4,-5],[+2,+3,+4],[-1,-3,-5],[+4,+5],[-3,-4,+5],[+2]]
Satisfiable CNF formula. \[(x_1 \vee \neg x_1 \vee \neg x_3) \wedge (x_1 \vee x_4 \vee \neg x_5 \vee x_6 \vee \neg x_7) \wedge (x_2 \vee x_3 \vee x_4 \vee x_8 \vee x_9)\]
>>>
fml4
[[+1,-1,-3],[+1,+4,-5,+6,-7],[+2,+3,+4,+8,+9]]
Satisfiable CNF formula. \[(x_1 \vee \neg x_2) \wedge (x_1 \vee x_4) \wedge (x_8 \vee x_9) \wedge (\neg x_1 \vee \neg x_8) \wedge (x_4 \vee x_5)\]
>>>
fml5
[[+1,-2],[+1,+4],[+8,+9],[-1,-8],[+4,+5]]
Unsatisfiable CNF formula. \[(x_1 \vee x_2) \wedge (\neg x_1 \vee x_2) \wedge (x_1 \vee \neg x_2) \wedge (\neg x_1 \vee \neg x_2)\]
>>>
fml6
[[+1,+2],[-1,+2],[+1,-2],[-1,-2]]
Satisfiable CNF formula \[(x_1) \wedge (\neg x_2 ) \wedge (x_3) \wedge (x_4) \wedge (\neg x_5) \wedge (x_6) \wedge (\neg x_7) \wedge (\neg x_8) \wedge (\neg x_9)\]
>>>
fml7
[[+1],[-2],[+3],[+4],[-5],[+6],[-7],[-8],[-9]]
Satisfiable CNF formula \[(x_1 \vee x_2) \wedge (x_2 \vee \neg x_3) \wedge (\neg x_3 \vee x_4) \wedge (x_4 \vee \neg x_5) \wedge (\neg x_5 \vee x_6) \wedge (x_6 \vee \neg x_7) \wedge (\neg x_7 \vee x_8) \wedge (x_8 \vee \neg x_9) \wedge (\neg x_9 \vee \neg x_1)\]
>>>
fml8
[[+1,+2],[+2,-3],[-3,+4],[+4,-5],[-5,+6],[+6,-7],[-7,+8],[+8,-9],[-1,-9]]
Satisfiable CNF formula \[(x_1) \wedge (\neg x_2) \wedge (x_3) \wedge (\neg x_1 \vee x_2 \vee \neg x_4) \wedge (\neg x_3 \vee \neg x_5) \wedge (x_4 \vee x_5 \vee \neg x_6) \wedge (x_6 \vee x_7) \wedge (\neg x_7 \vee x_8) \wedge (\neg x_8 \vee x_9)\]
>>>
fml9
[[+1],[-2],[+3],[-1,+2,-4],[-3,-5],[+4,+5,-6],[+6,+7],[-7,+8],[-8,+9]]
Unsatisfiable CNF formula \[(x_1) \wedge (x_2) \wedge (x_3) \wedge (\neg x_1 \vee x_4) \wedge (\neg x_2 \vee x_5) \wedge (\neg x_3 \vee x_6) \wedge (\neg x_4 \vee x_7) \wedge (\neg x_5 \vee x_8) \wedge (\neg x_7 \vee \neg x_8)\]
>>>
fml10
[[+1],[+2],[+3],[-1,+4],[-2,+5],[-3,+6],[-4,+7],[-5,+8],[-7,-8]]
Satisfiable CNF formula \[(x_1 \vee x_2) \wedge (\neg x_2 \vee \neg x_3) \wedge (x_3 \vee x_4) \wedge (\neg x_4 \vee \neg x_5) \wedge (x_5 \vee x_6) \wedge (\neg x_6 \vee \neg x_7) \wedge (x_7 \vee x_8) \wedge (\neg x_8 \vee \neg x_9) \wedge (x_9 \vee \neg x_1)\]
>>>
fml11
[[+1,+2],[-2,-3],[+3,+4],[-4,-5],[+5,+6],[-6,-7],[+7,+8],[-8,-9],[-1,+9]]
Teting Var String
fmlEvt1 :: Fml String Source #
Satisfiable CNF formula \[(\texttt{evt A} \vee \texttt{evt B}) \wedge (\neg \texttt{evt A} \vee \texttt{evt C}) \wedge (\texttt{evt A} \vee \neg \texttt{evt B} \neg \texttt{evt C})\]
>>>
fmlEvt2
[[+"Evt A"],[-"Evt A",+"Evt B"],[-"Evt B",-"Evt C"],[-"Evt A",-"Evt B",+"Evt C"]]
fmlEvt2 :: Fml String Source #
Unsatisfiable CNF formula \[(\texttt{evt A}) \wedge (\neg \texttt{evt A} \vee \texttt{evt B}) \wedge (\neg \texttt{evt B} \vee \neg \texttt{evt C}) \wedge (\texttt{evt A} \vee \neg \texttt{evt B} \vee \texttt{evt C})\]
>>>
fmlEvt2
[[+"Evt A"],[-"Evt A",+"Evt B"],[-"Evt B",-"Evt C"],[-"Evt A",-"Evt B",+"Evt C"]]