-
Notifications
You must be signed in to change notification settings - Fork 0
/
SelectedFormulasRaw.txt
47 lines (47 loc) · 3.21 KB
/
SelectedFormulasRaw.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
◻ ◻ ◻ ⊥
◇ ⊤ → ◇ ( p ∧ q )
◇ ⊤ → ◇ ( p ∧ ¬ q )
◇ ⊤ → ◇ ( ¬ p ∧ q )
◇ ⊤ → ◇ ( ¬ p ∧ ¬ q )
◇ ◇ ⊤ → ◇ ( p ∧ ( q ∧ ◇ ( p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( q ∧ ◇ ( p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( q ∧ ◇ ( ¬ p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( q ∧ ◇ ( ¬ p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( ¬ q ∧ ◇ ( p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( ¬ q ∧ ◇ ( p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( ¬ q ∧ ◇ ( ¬ p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( p ∧ ( ¬ q ∧ ◇ ( ¬ p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( q ∧ ◇ ( p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( q ∧ ◇ ( p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( q ∧ ◇ ( ¬ p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( q ∧ ◇ ( ¬ p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( ¬ q ∧ ◇ ( p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( ¬ q ∧ ◇ ( p ∧ ¬ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( ¬ q ∧ ◇ ( ¬ p ∧ q ) ) )
◇ ◇ ⊤ → ◇ ( ¬ p ∧ ( ¬ q ∧ ◇ ( ¬ p ∧ ¬ q ) ) )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◇ ⊤ ∧ ◻ p ) ∧ ◇ ( ◇ ⊤ ∧ ◻ q ) ) ) → ◻ ( ◇ ⊤ → ◇ ( p ∧ q ) )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◇ ⊤ ∧ ◻ p ) ∧ ◇ ( ◇ ⊤ ∧ ◻ ¬ q ) ) ) → ◻ ( ◇ ⊤ → ◇ ( p ∧ ¬ q ) )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◇ ⊤ ∧ ◻ ¬ p ) ∧ ◇ ( ◇ ⊤ ∧ ◻ q ) ) ) → ◻ ( ◇ ⊤ → ◇ ( ¬ p ∧ q ) )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◇ ⊤ ∧ ◻ ¬ p ) ∧ ◇ ( ◇ ⊤ ∧ ◻ ¬ q ) ) ) → ◻ ( ◇ ⊤ → ◇ ( ¬ p ∧ ¬ q ) )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◻ ⊥ ∧ p ) ∧ ◇ ( ◻ ⊥ ∧ q ) ) ) → ◇ ( ◇ p ∧ ◇ q )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◻ ⊥ ∧ p ) ∧ ◇ ( ◻ ⊥ ∧ ¬ q ) ) ) → ◇ ( ◇ p ∧ ◇ ¬ q )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◻ ⊥ ∧ ¬ p ) ∧ ◇ ( ◻ ⊥ ∧ q ) ) ) → ◇ ( ◇ ¬ p ∧ ◇ q )
( ◇ ◇ ⊤ ∧ ( ◇ ( ◻ ⊥ ∧ ¬ p ) ∧ ◇ ( ◻ ⊥ ∧ ¬ q ) ) ) → ◇ ( ◇ ¬ p ∧ ◇ ¬ q )
¬ ( p ∧ ◇ ( ¬ p ∧ ◇ ( p ∧ ◇ ¬ p ) ) )
¬ ( p ∧ ◇ ( ¬ p ∧ ( q ∧ ◇ ( ¬ q ∧ ( p ∧ ◇ ¬ p ) ) ) ) )
¬ ( p ∧ ◇ ( ¬ p ∧ ( ¬ q ∧ ◇ ( q ∧ ( p ∧ ◇ ¬ p ) ) ) ) )
( p ∧ ◇ ( ¬ p ∧ ( ( p → q ) ∧ ◇ ¬ ( p → q ) ) ) ) → ◇ ( p ∧ ◇ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p ↔ q ) ∧ ◇ ¬ ( p ↔ q ) ) ) ) → ◇ ( p ∧ ◇ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p → q ) ∧ ◇ ¬ ( p → q ) ) ) ) → ◇ ( ¬ p ∧ ◇ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p ↔ q ) ∧ ◇ ¬ ( p ↔ q ) ) ) ) → ◇ ( ¬ p ∧ ◇ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p → q ) ∧ ◇ ¬ ( p → q ) ) ) ) → ◇ ( p ∧ ◇ ¬ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p ↔ q ) ∧ ◇ ¬ ( p ↔ q ) ) ) ) → ◇ ( p ∧ ◇ ¬ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p → q ) ∧ ◇ ¬ ( p → q ) ) ) ) → ◇ ( ¬ p ∧ ◇ ¬ q )
( p ∧ ◇ ( ¬ p ∧ ( ( p ↔ q ) ∧ ◇ ¬ ( p ↔ q ) ) ) ) → ◇ ( ¬ p ∧ ◇ ¬ q )
( p → ◻ p ) ∨ ◇ p
( p → ◻ p ) ∨ ◇ ( p ∧ q )
( ¬ p → ◻ ¬ p ) ∨ ◇ p
( p → ◻ p ) ∨ ◇ ( p ∧ q )
( ¬ p → ◻ ¬ p ) ∨ ◇ ( p ∧ q )
q ∧ ¬ p ∧ ◻ ◻ ( ( p ∨ q ) → ¬ ◇ ( p ∨ q ) ) ∧ ◻ ◇ p
¬ ◻ ◻ ( p ↔ ¬ ◇ p )