Commit 6bd62edb authored by Christian Müller's avatar Christian Müller

results

parent b499357a
......@@ -23,3 +23,6 @@ build
.classpath
.settings/
/bin/
# Resulting ltl formulas
results/*.wf
G (
(n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)
) ∧ G (
¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)
) ∧ G (
((n0 ∧ X n1) → (
(X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧
(X O_a ↔ O_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n1 ∧ X n3) → (
(X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a)
)) ∧
((n1 ∧ X n2) → (
(X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n2 ∧ X n2) → (
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n3 ∧ X n1) → (
(X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
))
) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a
G (
n0
)
\ No newline at end of file
G((n0→Xn1)∧(n1→X(n3∨n2))∧(n2→Xn2)∧(n3→Xn1))∧G(¬(n0∧n1)∧¬(n0∧n2)∧¬(n0∧n3)∧¬(n1∧n2)∧¬(n1∧n3)∧¬(n2∧n3))∧G(((n0∧Xn1)→((XQ_a_a↔(Q_a_a∨(O_a∧choice0_a_a)))∧(XO_a↔O_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n1∧Xn3)→((XS_a_a_a↔(S_a_a_a∨(R_a_a∧choice1_a_a_a)))∧(XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)))∧((n1∧Xn2)→((XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n2∧Xn2)→((XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n3∧Xn1)→((XR_a_a↔(R_a_a∨Q_a_a))∧(XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XS_a_a_a↔S_a_a_a))))∧n0∧¬n1∧¬n2∧¬n3∧¬Q_a_a∧¬R_a_a∧¬S_a_a_a
\ No newline at end of file
G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ G (((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X Q_b_a ↔ (Q_b_a ∨ (O_a ∧ choice0_b_a))) ∧ (X Q_a_b ↔ (Q_a_b ∨ (O_b ∧ choice0_a_b))) ∧ (X Q_b_b ↔ (Q_b_b ∨ (O_b ∧ choice0_b_b))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ (R_a_a ∧ choice1_b_a_a))) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ (R_b_a ∧ choice1_a_b_a))) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ (R_b_a ∧ choice1_b_b_a))) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ (R_a_b ∧ choice1_a_a_b))) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ (R_a_b ∧ choice1_b_a_b))) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ (R_b_b ∧ choice1_a_b_b))) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ (R_b_b ∧ choice1_b_b_b))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b)))))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X R_b_a ↔ (R_b_a ∨ Q_b_a)) ∧ (X R_a_b ↔ (R_a_b ∨ Q_a_b)) ∧ (X R_b_b ↔ (R_b_b ∨ Q_b_b)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b))))))) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬Q_b_a ∧ ¬Q_a_b ∧ ¬Q_b_b ∧ (¬R_a_a ∧ ¬R_b_a ∧ ¬R_a_b ∧ ¬R_b_b ∧ (¬S_a_a_a ∧ ¬S_b_a_a ∧ ¬S_a_b_a ∧ ¬S_b_b_a ∧ ¬S_a_a_b ∧ ¬S_b_a_b ∧ ¬S_a_b_b ∧ ¬S_b_b_b))
G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ G (((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X Q_b_a ↔ (Q_b_a ∨ (O_a ∧ choice0_b_a))) ∧ (X Q_c_a ↔ (Q_c_a ∨ (O_a ∧ choice0_c_a))) ∧ (X Q_a_b ↔ (Q_a_b ∨ (O_b ∧ choice0_a_b))) ∧ (X Q_b_b ↔ (Q_b_b ∨ (O_b ∧ choice0_b_b))) ∧ (X Q_c_b ↔ (Q_c_b ∨ (O_b ∧ choice0_c_b))) ∧ (X Q_a_c ↔ (Q_a_c ∨ (O_c ∧ choice0_a_c))) ∧ (X Q_b_c ↔ (Q_b_c ∨ (O_c ∧ choice0_b_c))) ∧ (X Q_c_c ↔ (Q_c_c ∨ (O_c ∧ choice0_c_c))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ (R_a_a ∧ choice1_b_a_a))) ∧ (X S_c_a_a ↔ (S_c_a_a ∨ (R_a_a ∧ choice1_c_a_a))) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ (R_b_a ∧ choice1_a_b_a))) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ (R_b_a ∧ choice1_b_b_a))) ∧ (X S_c_b_a ↔ (S_c_b_a ∨ (R_b_a ∧ choice1_c_b_a))) ∧ (X S_a_c_a ↔ (S_a_c_a ∨ (R_c_a ∧ choice1_a_c_a))) ∧ (X S_b_c_a ↔ (S_b_c_a ∨ (R_c_a ∧ choice1_b_c_a))) ∧ (X S_c_c_a ↔ (S_c_c_a ∨ (R_c_a ∧ choice1_c_c_a))) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ (R_a_b ∧ choice1_a_a_b))) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ (R_a_b ∧ choice1_b_a_b))) ∧ (X S_c_a_b ↔ (S_c_a_b ∨ (R_a_b ∧ choice1_c_a_b))) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ (R_b_b ∧ choice1_a_b_b))) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ (R_b_b ∧ choice1_b_b_b))) ∧ (X S_c_b_b ↔ (S_c_b_b ∨ (R_b_b ∧ choice1_c_b_b))) ∧ (X S_a_c_b ↔ (S_a_c_b ∨ (R_c_b ∧ choice1_a_c_b))) ∧ (X S_b_c_b ↔ (S_b_c_b ∨ (R_c_b ∧ choice1_b_c_b))) ∧ (X S_c_c_b ↔ (S_c_c_b ∨ (R_c_b ∧ choice1_c_c_b))) ∧ (X S_a_a_c ↔ (S_a_a_c ∨ (R_a_c ∧ choice1_a_a_c))) ∧ (X S_b_a_c ↔ (S_b_a_c ∨ (R_a_c ∧ choice1_b_a_c))) ∧ (X S_c_a_c ↔ (S_c_a_c ∨ (R_a_c ∧ choice1_c_a_c))) ∧ (X S_a_b_c ↔ (S_a_b_c ∨ (R_b_c ∧ choice1_a_b_c))) ∧ (X S_b_b_c ↔ (S_b_b_c ∨ (R_b_c ∧ choice1_b_b_c))) ∧ (X S_c_b_c ↔ (S_c_b_c ∨ (R_b_c ∧ choice1_c_b_c))) ∧ (X S_a_c_c ↔ (S_a_c_c ∨ (R_c_c ∧ choice1_a_c_c))) ∧ (X S_b_c_c ↔ (S_b_c_c ∨ (R_c_c ∧ choice1_b_c_c))) ∧ (X S_c_c_c ↔ (S_c_c_c ∨ (R_c_c ∧ choice1_c_c_c))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c)))))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X R_b_a ↔ (R_b_a ∨ Q_b_a)) ∧ (X R_c_a ↔ (R_c_a ∨ Q_c_a)) ∧ (X R_a_b ↔ (R_a_b ∨ Q_a_b)) ∧ (X R_b_b ↔ (R_b_b ∨ Q_b_b)) ∧ (X R_c_b ↔ (R_c_b ∨ Q_c_b)) ∧ (X R_a_c ↔ (R_a_c ∨ Q_a_c)) ∧ (X R_b_c ↔ (R_b_c ∨ Q_b_c)) ∧ (X R_c_c ↔ (R_c_c ∨ Q_c_c)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c))))))) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬Q_b_a ∧ ¬Q_c_a ∧ ¬Q_a_b ∧ ¬Q_b_b ∧ ¬Q_c_b ∧ ¬Q_a_c ∧ ¬Q_b_c ∧ ¬Q_c_c ∧ (¬R_a_a ∧ ¬R_b_a ∧ ¬R_c_a ∧ ¬R_a_b ∧ ¬R_b_b ∧ ¬R_c_b ∧ ¬R_a_c ∧ ¬R_b_c ∧ ¬R_c_c ∧ (¬S_a_a_a ∧ ¬S_b_a_a ∧ ¬S_c_a_a ∧ ¬S_a_b_a ∧ ¬S_b_b_a ��� ¬S_c_b_a ∧ ¬S_a_c_a ∧ ¬S_b_c_a ∧ ¬S_c_c_a ∧ ¬S_a_a_b ∧ ¬S_b_a_b ∧ ¬S_c_a_b ∧ ¬S_a_b_b ∧ ¬S_b_b_b ∧ ¬S_c_b_b ∧ ¬S_a_c_b ∧ ¬S_b_c_b ∧ ¬S_c_c_b ∧ ¬S_a_a_c ∧ ¬S_b_a_c ∧ ¬S_c_a_c ∧ ¬S_a_b_c ∧ ¬S_b_b_c ∧ ¬S_c_b_c ∧ ¬S_a_c_c ∧ ¬S_b_c_c ∧ ¬S_c_c_c))
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment