```python
from sympy import *
```


```python
x1, x2, x3, x4, x5 = symbols('x1 x2 x3 x4 x5')
```


```python
Phi1 = x1 | x2 | x3 | x4 | x5
```


```python
x6, x7, x8, x9, x10 = symbols('x6 x7 x8 x9 x10')
```


```python
Phi2 = x6 | x7 | x8 | x9 | x10
```


```python
Psi = (Phi1 & Phi2) | (Not(Phi1) & Not(Phi2))
```


```python
to_cnf(Psi, simplify=True)
```




    (x1 | x2 | x3 | x4 | x5 | ~x10) & (x1 | x2 | x3 | x4 | x5 | ~x6) & (x1 | x2 | x3 | x4 | x5 | ~x7) & (x1 | x2 | x3 | x4 | x5 | ~x8) & (x1 | x2 | x3 | x4 | x5 | ~x9) & (x10 | x6 | x7 | x8 | x9 | ~x1) & (x10 | x6 | x7 | x8 | x9 | ~x2) & (x10 | x6 | x7 | x8 | x9 | ~x3) & (x10 | x6 | x7 | x8 | x9 | ~x4) & (x10 | x6 | x7 | x8 | x9 | ~x5)




```python
Psi = ( Not(Phi1) | Phi2) & (Not(Phi2) | Phi1)
```


```python
to_cnf(Psi, simplify=True)
```




    (x1 | x2 | x3 | x4 | x5 | ~x10) & (x1 | x2 | x3 | x4 | x5 | ~x6) & (x1 | x2 | x3 | x4 | x5 | ~x7) & (x1 | x2 | x3 | x4 | x5 | ~x8) & (x1 | x2 | x3 | x4 | x5 | ~x9) & (x10 | x6 | x7 | x8 | x9 | ~x1) & (x10 | x6 | x7 | x8 | x9 | ~x2) & (x10 | x6 | x7 | x8 | x9 | ~x3) & (x10 | x6 | x7 | x8 | x9 | ~x4) & (x10 | x6 | x7 | x8 | x9 | ~x5)




```python
Psi = Not(Phi1) | Phi2
```


```python
to_cnf(Psi, simplify=True)
```




    (x10 | x6 | x7 | x8 | x9 | ~x1) & (x10 | x6 | x7 | x8 | x9 | ~x2) & (x10 | x6 | x7 | x8 | x9 | ~x3) & (x10 | x6 | x7 | x8 | x9 | ~x4) & (x10 | x6 | x7 | x8 | x9 | ~x5)




```python
Psi = Phi1 >> Phi2
```


```python
to_cnf(Psi, simplify=True)
```




    (x10 | x6 | x7 | x8 | x9 | ~x1) & (x10 | x6 | x7 | x8 | x9 | ~x2) & (x10 | x6 | x7 | x8 | x9 | ~x3) & (x10 | x6 | x7 | x8 | x9 | ~x4) & (x10 | x6 | x7 | x8 | x9 | ~x5)




```python
y1, y2, y3 = symbols('y1 y2 y3')
```


```python
sign1 = y1 >> Not(y2 & y3)
```


```python
to_cnf(sign1,simplify=True)
```




    ~y1 | ~y2 | ~y3




```python
sign2 = y1 >> (y2 | y3)
```


```python
to_cnf(sign2,simplify=True)
```




    y2 | y3 | ~y1




```python
sign3 = y1 >> ((y2 >> y3)&(y3 >> y2))
```


```python
to_cnf(sign3,simplify=True)
```




    (y2 | ~y1 | ~y3) & (y3 | ~y1 | ~y2)




```python
extension1 = y1 >> (y2 >> y3)
```


```python
to_cnf(extension1,simplify=True)
```




    y3 | ~y1 | ~y2




```python

```

4886e808871c3b3f2d6ab3a1cd54b343da988287
ipynb
Jupyter Notebook
cnf tester.ipynb
zl674421351/transform-order-by-reversals
3a0231e33e410c0aab3a6baa7a2a67983bcbc585
MIT
cnf tester.ipynb
zl674421351/transform-order-by-reversals
3a0231e33e410c0aab3a6baa7a2a67983bcbc585
MIT
cnf tester.ipynb
zl674421351/transform-order-by-reversals
3a0231e33e410c0aab3a6baa7a2a67983bcbc585
MIT
2019-11-22T22:31:42.000Z
2019-11-22T22:31:42.000Z
Qwen/Qwen-72B
1. YES
2. YES