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
|
(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-var A Bool)
(declare-var B Bool)
(declare-var C Bool)
(declare-var D Bool)
(declare-var E Bool)
(declare-var F Bool)
(declare-var G Bool)
(declare-var H Bool)
(declare-var I Bool)
(declare-var J Bool)
(declare-var K Bool)
(declare-var L Bool)
(declare-var M Bool)
(declare-var N Bool)
(declare-var O Bool)
(declare-var P Bool)
(declare-var Q Bool)
(declare-var R Bool)
(declare-var S Bool)
(declare-var T Bool)
(declare-var U Bool)
(declare-var V Bool)
(declare-var W Bool)
(declare-var X Bool)
(rule (=> (not (or L K J I H G F E D C B A)) (Invariant L K J I H G F E D C B A)))
(rule (let ((a!1 (and (Invariant X W V U T S R Q P O N M)
(=> (not (and true)) (not F))
(=> (not (and true)) (not E))
(=> (not (and W)) (not D))
(=> (not (and W)) (not C))
(=> (not (and U)) (not B))
(=> (not (and U)) (not A))
(= L (xor F X))
(= K (xor E W))
(= J (xor D V))
(= I (xor C U))
(= H (xor B T))
(= G (xor A S))
(=> D (not E))
(=> C (not E))
(=> B (not C))
(=> A (not C))
((_ at-most 5) L K J I H G))))
(=> a!1 (Invariant L K J I H G F E D C B A))))
(rule (=> (and (Invariant L K J I H G F E D C B A) L (not K) J (not I) H G)
(Goal L K J I H G F E D C B A)))
(query Goal)
|
