-
Notifications
You must be signed in to change notification settings - Fork 1
/
out.txt
122 lines (118 loc) · 5.09 KB
/
out.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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
BNF:
tree: (&, (&, (&, A, (+, (-, A, ), B)), (-, C, )), (+, (-, B, ), C))
BNF:
tree: (-, (&, (&, (&, A, (+, (-, A, ), B)), (-, C, )), (+, (-, B, ), C)), )
Attempting to resolve the formula: Original Formula: (-(((A&((-A)+B))&(-C))&((-B)+C)))
Clause Normal Form: [[A, -A, B, C], [-A, -B, B, C], [A, -A, C, -C], [-A, -B, C, -C]]
Attempting to resolve [-A, -B, B, C] & [A, -A, C, -C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, -B, B, C] & [-A, -B, C, -C]
Found complimentary literal B
Clauses resolved to [-A, -B, C, -C]
Attempting to resolve [-A, -B, B, C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C]
Attempting to resolve [A, -A, C, -C] & [-A, -B, C, -C]
Found complimentary literal A
Clauses resolved to [-A, -B, C, -C]
Attempting to resolve [A, -A, C, -C] & [A, -A, B, C]
Found complimentary literal A
Clauses resolved to [-A, A, B, C, -C]
Attempting to resolve [-A, -B, C, -C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, -B, B, C] & [A, -A, C, -C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, -B, B, C] & [-A, -B, C, -C]
Found complimentary literal B
Clauses resolved to [-A, -B, C, -C]
Attempting to resolve [-A, -B, B, C] & [-A, A, B, C, -C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, -B, B, C] & [-A, -B, B, C, -C]
Found complimentary literal -B
Clauses resolved to [-A, B, -B, C, -C]
Attempting to resolve [-A, -B, B, C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C]
Attempting to resolve [A, -A, C, -C] & [-A, -B, C, -C]
Found complimentary literal A
Clauses resolved to [-A, -B, C, -C]
Attempting to resolve [A, -A, C, -C] & [-A, A, B, C, -C]
Found complimentary literal A
Clauses resolved to [-A, A, B, C, -C]
Attempting to resolve [A, -A, C, -C] & [-A, -B, B, C, -C]
Found complimentary literal A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [A, -A, C, -C] & [A, -A, B, C]
Found complimentary literal A
Clauses resolved to [-A, A, B, C, -C]
Attempting to resolve [-A, -B, C, -C] & [-A, A, B, C, -C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, -B, C, -C] & [-A, -B, B, C, -C]
Found complimentary literal -B
Clauses resolved to [-A, -B, C, -C]
Attempting to resolve [-A, -B, C, -C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
Attempting to resolve [-A, A, B, C, -C] & [-A, -B, B, C, -C]
Found complimentary literal A
Clauses resolved to [-A, B, -B, C, -C]
Attempting to resolve [-A, A, B, C, -C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [A, -A, B, C, -C]
Attempting to resolve [-A, -B, B, C, -C] & [A, -A, B, C]
Found complimentary literal -A
Clauses resolved to [-A, -B, B, C, -C]
No more clauses resolved, negated formula satisfiable
#=================================================#
# #
# Proving: (((A&((-A)+B))&(-C))&((-B)+C)) #
# #
# Proof for: (-(((A&((-A)+B))&(-C))&((-B)+C))) #
# #
# Line no. | Clauses | Resolvant #
# ---------+------------+---------------------- #
# 0 | -, - | [-A, -B, B, C] #
# 1 | -, - | [A, -A, C, -C] #
# 2 | -, - | [-A, -B, C, -C] #
# 3 | -, - | [A, -A, B, C] #
# 4 | 0, 1 | [-A, -B, B, C, -C] #
# 5 | 1, 3 | [-A, A, B, C, -C] #
# #
# This negated formula is satisfiable #
# Therefore the original formula is invalid #
# #
# Execution completed in: #
# 6394235 nanoseconds #
# #
#=================================================#
Initialized model:
A Free
B Free
C Free
Recursing on: Original Formula: (((A&((-A)+B))&(-C))&((-B)+C))
Clause Normal Form: [[A], [-A, B], [-C], [-B, C]]
Unit literal on: A
Recursing on: Original Formula: (((A&((-A)+B))&(-C))&((-B)+C))
Clause Normal Form: [[B], [-C], [-B, C]]
Unit literal on: B
Recursing on: Original Formula: (((A&((-A)+B))&(-C))&((-B)+C))
Clause Normal Form: [[-C], [C]]
Unit literal on: -C
Recursing on: Original Formula: (((A&((-A)+B))&(-C))&((-B)+C))
Clause Normal Form: [[]]
#===============================================#
# #
# Proof for: (((A&((-A)+B))&(-C))&((-B)+C)) #
# #
# #
# This formula is unsatisfiable. #
# #
# Execution completed in: #
# 70731549 nanoseconds #
# #
#===============================================#