Timings for job503to506.v

  1. /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-fourcolor.dev/./theories/job503to506.v.timing
  2. /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-fourcolor.dev/./theories/job503to506.v.timing
(* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
From fourcolor Require Import cfmap cfreducible configurations.
(******************************************************************************) (* Reducibility of configurations number 503 to 506, whose indices in *) (* the_configs range over segment [502, 506). *) (******************************************************************************)
Lemma red502to506 : reducible_in_range 502 506 the_configs.
Proof.
CheckReducible.
Qed.