-
Notifications
You must be signed in to change notification settings - Fork 0
/
LogicResolustion.fas
111 lines (111 loc) · 6.22 KB
/
LogicResolustion.fas
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
(|SYSTEM|::|VERSION| '(20080430.))
#0Y_ #0Y |CHARSET|::|UTF-8|
#Y(#:|1 54 (DEFUN RESOLUTION (LC) ...)-1|
#20Y(00 00 00 00 00 00 00 00 20 01 DA 2F 01 DA DC 32 9C C5 19 01)
(|COMMON-LISP-USER|::|RESOLUTION| |SYSTEM|::|REMOVE-OLD-DEFINITIONS|
#Y(|COMMON-LISP-USER|::|RESOLUTION|
#207Y(00 00 00 00 01 00 00 00 26 02 93 01 08 9E 0F 01 14 63 1B 80 96 C5
1B 80 AE 87 01 00 21 08 93 00 05 DC 38 01 31 8E AC 6B 01 38 07 32
69 94 00 63 1B 28 87 01 00 6B 01 63 1B 18 87 01 00 14 6B 01 38 07
32 69 0F 01 AC 6B 01 B0 DD 2D 04 04 0F 01 83 01 AD 8D 9F 64 16 02
83 01 AD 8D 9F 54 16 02 9D 5C 78 63 1B 34 87 01 00 6B 01 63 1B 24
CD 1B 01 CE 14 38 01 31 8E 00 19 02 87 01 00 14 6B 01 38 07 32 69
0F 01 AC 6B 01 B0 DF 2D 04 04 0F 01 83 01 AD 8D 9F 64 16 02 83 01
AD 8D 9F 48 16 02 9D 5B 0F 06 9D 5C 5B 0F 07 83 01 AD 8D 9F FF 69
16 02 0E 01 1D FF B7 0E 01 5B 1C 0A 0E 01 79 63 7B 01 8E 14 FF AB
CF 14 38 01 31 8E 02 19 02)
("No contradiction (Empty clauses)" |COMMON-LISP-USER|::|REMAINDER|
"Invalid input, enter clausal form" |COMMON-LISP-USER|::|R|
|COMMON-LISP-USER|::|RESOLVE_EACH| |COMMON-LISP-USER|::|L|
|COMMON-LISP-USER|::|CURRENT_LEFT| |COMMON-LISP-USER|::|CURRENT_RIGHT|
"A Contradiction has been found" "A Contradiction has been found"
"No contradiction has been found")
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|)
(|COMMON-LISP-USER|::|LC|) |COMMON-LISP|::|NIL| 1))
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|))
#Y(#:|57 93 (DEFUN RESOLVE_EACH (CURRENT_CLAUSE REMAINING CURRENT_ATOM ...) ...)-2|
#20Y(00 00 00 00 00 00 00 00 20 01 DA 2F 01 DA DC 32 9C C5 19 01)
(|COMMON-LISP-USER|::|RESOLVE_EACH| |SYSTEM|::|REMOVE-OLD-DEFINITIONS|
#Y(|COMMON-LISP-USER|::|RESOLVE_EACH|
#131Y(00 00 00 00 04 00 00 00 26 05 AD 24 00 0E A1 5C 78 38 06 32 6F 0F
02 14 63 1B 80 4C 94 04 38 06 32 6F 0F 01 14 63 1B 19 87 01 00 14
B1 8F 14 0F AC 94 07 38 07 72 69 7B 01 95 07 82 02 23 06 83 01 AD
8D 9F 63 16 02 1B 25 A0 19 05 87 01 00 14 B1 8F 14 12 94 06 7B 01
AD A5 5C 78 38 07 72 69 7B 01 82 02 23 06 83 01 AD 8D 9F 60 16 02
A1 5B 1C 08 95 04 63 7B 01 8E 14 4F B0 7B 01 B0 33 02 23 19 05)
(|COMMON-LISP-USER|::|L| |COMMON-LISP-USER|::|LHS|
|COMMON-LISP-USER|::|RHS|)
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|)
(|COMMON-LISP-USER|::|CURRENT_CLAUSE| |COMMON-LISP-USER|::|REMAINING|
|COMMON-LISP-USER|::|CURRENT_ATOM| |COMMON-LISP-USER|::|OPTION|)
|COMMON-LISP|::|NIL| 1))
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|))
#Y(#:|93 109 (DEFUN TEST-RESOLUTION NIL ...)-3|
#20Y(00 00 00 00 00 00 00 00 20 01 DA 2F 01 DA DC 32 9C C5 19 01)
(|COMMON-LISP-USER|::|TEST-RESOLUTION| |SYSTEM|::|REMOVE-OLD-DEFINITIONS|
#Y(|COMMON-LISP-USER|::|TEST-RESOLUTION|
#97Y(00 00 00 00 00 00 00 00 26 01 DA 6F 01 38 01 31 8E DC 6F 01 38 01
31 8E DD 6F 01 38 01 31 8E DE 6F 01 38 01 31 8E DF 6F 01 38 01 31
8E E0 6F 01 38 01 31 8E E1 6F 01 38 01 31 8E E2 6F 01 38 01 31 8E
63 6F 01 38 01 31 8E E3 6F 01 38 01 31 8E E4 6F 01 38 01 31 8E E5
6F 01 38 01 31 8E 02 19 01)
((((|COMMON-LISP-USER|::|A|)
(|COMMON-LISP-USER|::|B| |COMMON-LISP-USER|::|C|))
((|COMMON-LISP-USER|::|B|) |COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|C|) |COMMON-LISP|::|NIL|))
|COMMON-LISP-USER|::|RESOLUTION|
(((|COMMON-LISP-USER|::|A|)
(|COMMON-LISP-USER|::|B| |COMMON-LISP-USER|::|C|))
((|COMMON-LISP-USER|::|B|) |COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|A|))
((|COMMON-LISP-USER|::|C|) |COMMON-LISP|::|NIL|))
(((|COMMON-LISP-USER|::|C| |COMMON-LISP-USER|::|D|)
(|COMMON-LISP-USER|::|A|))
((|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|D|
|COMMON-LISP-USER|::|E|)
|COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL|
(|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|C|))
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|D|))
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|E|)))
(((|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|B|)
|COMMON-LISP|::|NIL|))
(((|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|B|)
|COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|B|) |COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|C|) |COMMON-LISP|::|NIL|))
(((|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|B|)
|COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|B| |COMMON-LISP-USER|::|C|)
|COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL|
(|COMMON-LISP-USER|::|A| |COMMON-LISP-USER|::|B|
|COMMON-LISP-USER|::|C|)))
(((|COMMON-LISP-USER|::|C| |COMMON-LISP-USER|::|D|)
|COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|B|) |COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL|
(|COMMON-LISP-USER|::|B| |COMMON-LISP-USER|::|C|
|COMMON-LISP-USER|::|D|)))
((|COMMON-LISP|::|NIL|
(|COMMON-LISP-USER|::|X| |COMMON-LISP-USER|::|Y|))
((|COMMON-LISP-USER|::|B|) |COMMON-LISP|::|NIL|))
(((|COMMON-LISP-USER|::|A|) (|COMMON-LISP-USER|::|B|))
((|COMMON-LISP-USER|::|B|) (|COMMON-LISP-USER|::|A|)))
(((|COMMON-LISP-USER|::|X| |COMMON-LISP-USER|::|Y|)
|COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|Y|))
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|X|)))
(((|COMMON-LISP-USER|::|X| |COMMON-LISP-USER|::|Z|)
|COMMON-LISP|::|NIL|)
((|COMMON-LISP-USER|::|Y|) |COMMON-LISP|::|NIL|)
(|COMMON-LISP|::|NIL| (|COMMON-LISP-USER|::|X|))
(|COMMON-LISP|::|NIL|
(|COMMON-LISP-USER|::|Y| |COMMON-LISP-USER|::|Z|))))
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|) ()
|COMMON-LISP|::|NIL| 1))
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|))
#Y(#:|111 111 (TEST-RESOLUTION)-4|
#14Y(00 00 00 00 00 00 00 00 20 01 2E 00 19 01)
(|COMMON-LISP-USER|::|TEST-RESOLUTION|)
(|COMMON-LISP|::|T| |COMMON-LISP|::|T| |COMMON-LISP|::|T|))