-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathproblem.txt
More file actions
51 lines (51 loc) · 2.4 KB
/
problem.txt
File metadata and controls
51 lines (51 loc) · 2.4 KB
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
48
49
50
51
ForAll(~((l_s | Repair_Complex) ^ (x3_e)))
ForAll((tau) => Exist(Test_Repair))
ForAll((Analyze_Defect) => Exist(a2_s | a2_e))
ForAll(~((Repair_Simple) ^ (tau)))
ForAll(~((l_s) ^ (Repair_Simple)))
ForAll(~((l_s) ^ (Repair_Complex)))
Exist(x3_s)
ForAll(~((Analyze_Defect) ^ (a2_s | a2_e)))
ForAll(~((x3_s) ^ (x3_e)))
ForAll(~((l_s) ^ (tau)))
ForAll(~((l_s | Test_Repair) ^ (l_s | Repair_Complex)))
ForAll((Test_Repair) => ((Exist(tau) ^ Exist(Test_Repair)) | (~(Exist(tau)))))
Exist(Register)
ForAll((l_s) => Exist(Test_Repair))
ForAll(~((Register) ^ (Analyze_Defect)))
ForAll(~((l_s | Repair_Complex) ^ (l_s | Repair_Simple)))
ForAll((Archive_Repair) => Exist(End))
ForAll((Inform_User) => Exist(a2_e))
ForAll((tau) => Exist(Repair_Simple))
ForAll(~((x3_s) ^ (l_s | Test_Repair)))
Exist(a2_s)
ForAll((x3_s | x3_e) => Exist(a2_e))
ForAll(~((l_s) ^ (Test_Repair)))
ForAll((l_s) => Exist(Repair_Simple))
ForAll(~((Register) ^ (End)))
ForAll(~((a2_s | a2_e) ^ (End)))
ForAll(~((x3_s) ^ (l_s | Repair_Complex)))
ForAll(~((Register) ^ (Archive_Repair)))
ForAll((a2_s | a2_e) => Exist(Archive_Repair))
ForAll(~((Analyze_Defect) ^ (End)))
ForAll(~((a2_s) ^ ((Inform_User) | (x3_s | x3_e))))
ForAll(~((l_s | Test_Repair) ^ (l_s | Repair_Simple)))
ForAll((x3_s) => ((Exist(l_s | Test_Repair) ^ ~(Exist(l_s | Repair_Complex)) ^ ~(Exist(l_s | Repair_Simple))) | ((~(Exist(l_s | Test_Repair)) ^ Exist(l_s | Repair_Complex) ^ ~(Exist(l_s | Repair_Simple))) | (~(Exist(l_s | Test_Repair)) ^ ~(Exist(l_s | Repair_Complex)) ^ Exist(l_s | Repair_Simple)))))
ForAll(((l_s | Test_Repair) | (l_s | Repair_Complex) | (l_s | Repair_Simple)) => Exist(x3_e))
ForAll(~((Archive_Repair) ^ (End)))
ForAll(~((l_s | Repair_Simple) ^ (x3_e)))
ForAll(~((Analyze_Defect) ^ (Archive_Repair)))
ForAll((tau) => Exist(Repair_Complex))
ForAll((Repair_Complex) => ((Exist(tau) ^ Exist(Repair_Complex)) | (~(Exist(tau)))))
ForAll(~(((Inform_User) | (x3_s | x3_e)) ^ (a2_e)))
ForAll((a2_s) => (Exist(Inform_User) ^ Exist(x3_s | x3_e)))
ForAll(~((Repair_Complex) ^ (tau)))
ForAll((Repair_Simple) => ((Exist(tau) ^ Exist(Repair_Simple)) | (~(Exist(tau)))))
ForAll((Register) => Exist(Analyze_Defect))
ForAll(~((Register) ^ (a2_s | a2_e)))
ForAll(~((x3_s) ^ (l_s | Repair_Simple)))
ForAll(~((a2_s | a2_e) ^ (Archive_Repair)))
ForAll((l_s) => Exist(Repair_Complex))
ForAll(~((l_s | Test_Repair) ^ (x3_e)))
Exist(l_s)
ForAll(~((Test_Repair) ^ (tau)))