blob: 1b5117a70a413b96cc838ce6184aba908a852398 (
plain)
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
|
; Depends on er.plf
; This is a circuitous proof that uses the definition introduction and
; unrolling rules
(check
(% v1 var
(% v2 var
(% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
(% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
(% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
(% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
(: (holds cln)
(decl_definition
(neg v1)
(clc (neg v2) cln)
(\ v3
(\ def3
(clausify_definition _ _ _ def3 _
(\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
(\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
(\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln)))
(@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf)
; Clauses
(satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2
(satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3
(satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1
(satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1
(satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2
(satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty
pf_c13
))
))
))
))
))
))
)
)))
)
))
)
)
))))
))
)
; This is a test of ER proof produced by drat2er on Example 1 from:
; https://www.cs.utexas.edu/~marijn/drat-trim/
(check
(% v1 var
(% v2 var
(% v3 var
(% v4 var
(% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
(% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
(% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
(% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
(% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
(% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
(% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
(% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
(: (holds cln)
(decl_definition
(neg v1)
cln
(\ v5
(\ def1
(clausify_definition _ _ _ def1 _
(\ pf_c9 ; type: (holds (clc (pos def1v) cln))
(\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
(\ idc0 ; type: (common_tail_cnf cln _)
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
(satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
(satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
pf_c18
))))))))))))))))
)))
)
))
)
)
))))))))
))))
)
|