Library ExtractionCubes
Require Import Generate.
Require Import CubeAndConquer.
Require Import SetChecker.
Extraction Language Ocaml.
Extract Inductive positive => int [ "(fun x -> 2*x+1)" "(fun x -> 2*x)" "1" ]
"(fun fI fO fH n -> if n=1 then fH () else if n mod 2 = 0 then fO (n/2) else fI (n/2))".
Extract Inlined Constant Pos.compare => "(fun x y -> if x = y then Eq else (if x < y then Lt else Gt))".
Extract Inductive nat => int [ "0" "Pervasives.succ" ]
"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Constant TheBreak => "2520".
Extract Constant TheN => "7826".
Extract Constant The_List => "let rec ltl l = (match l with | [] -> Nil | x::m -> Cons (x,ltl m)) in ltl [3;4;5;7;11;13;19;181;23;313;421;31;613;761;43;1013;47;1201;1301;59;1741;61;1861;2113;67;2381;71;2521;79;3121;83;3613;4513;5101;103;107;7321;7812;6;8;10;14;101;22;26;197;226;257;38;362;401;46;577;626;677;842;62;1226;1297;1522;1601;86;2026;94;2303;2402;2602;2917;3137;118;3482;122;3722;4226;4357;134;4762;4899;142;5042;5477;158;6242;6399;6723;166;7057;7226;7568;5223;5583;6339;7143;7563;202;394;514;802;1154;1354;2594;3202;4606;5834;6274;6726;6964;7444;4803;6078;6909;7206;7806;49;2947;4291;5327;7091;29;173;229;293;733;1093;1229;1373;2021;2029;2213;3253;4229;4493;4757;5333;6404;6557;7229;7573;149;269;317;617;929;1109;1409;2969;3449;3617;4517;5309;5517;6389;6849;7316;7817;121;1991;3443;4631;6743;7356;7782;98;2534;2807;4039;4382;4739;5894;58;346;458;586;874;1466;2186;2458;2746;4042;4058;4426;6506;6736;178;298;409;538;634;1033;1234;1453;1609;1858;2218;2713;2818;3373;3853;4909;5193;5634;5938;6093;6733;6898;7234;7578;7753;361;3439;5947;6573;242;2167;2486;2827;3982;4411;6347;6886;7447;4163;529;7199;6063;6087;6639;157;193;233;277;433;557;773;853;937;1117;1213;1637;1753;1873;1997;2393;2677;3457;3797;4153;4337;5113;5737;5953;6173;6397;6857;7333;7552;7577;4887;2758;3598;5614;5611;137;241;457;641;713;857;977;1697;2417;2617;3041;3953;4241;5609;5641;6257;6416;6577;5973;218;818;2066;2906;3218;4214;5426;6746;7218;7706;3743;4294;4883;722;6878;7581;7619;7602;7783;2222;4334;5654;4531;5198;5911;6558;7374;337;389;569;709;1129;343;1429;2137;2269;2689;2837;3469;3637;4349;4729;5749;6637;6869;7589;194;281;314;349;386;466;509;554;601;701;809;866;1049;1114;1181;1321;1546;1706;1789;1874;2141;2234;2426;2729;2891;3274;3389;3506;3746;3994;4649;4786;5209;5354;5451;5501;5751;5801;6914;7594;7719;4827;5319;5574;6102;6321;6654;6939;5131;7196;7651;6441;6667;6107;7006;2219;4319;6503;7763;274;482;914;1282;1426;1714;1954;3394;4834;5234;6082;6304;7168;7232;6501;7458;268;469;7571;7797;397;589;661;877;997;1333;2437;2773;3061;3517;4189;4261;5077;5293;5589;5893;6277;6436;6597;7432;7533;4911;5259;5619;5991;7179;3838;7486;353;461;521;653;881;1553;1901;2153;4001;5553;5981;6653;7121;249;415;581;1591;1903;2519;3223;4646;1739;5091;7251;373;449;674;778;1138;1418;1493;2258;686;2549;2753;2858;3413;4274;4538;4673;5233;5378;5427;5674;5727;6133;6449;6938;7274;7347;7793;1639;2959;3487;6787;562;698;1018;1202;1402;1618;2098;2362;2642;3578;4282;5458;5782;6548;6778;7012;7492;7638;309;412;428;535;749;5454;6198;7404;2422;3206;4102;6118;541;673;821;1361;1801;2441;3181;3673;4021;4201;4961;5573;6221;6673;1331;7381;7504;6262;2863;3766;4438;7231;381;508;635;1651;889;5207;1397;7747;593;1153;1289;1433;1457;1913;2089;2273;2537;3089;3313;4289;5393;5561;5689;6464;6788;6992;7808;393;524;655;1703;917;5371;6534;6666;938;417;556;695;1807;973;5699;794;1178;1322;1754;1994;2666;4874;5274;5546;6122;7034;6411;6807;5118;5367;5622;6423;6702;7278;453;604;755;1963;1057;6191;3287;4351;5567;7676;7623;7777;6478;706;757;922;1042;1237;1306;1762;2017;3106;3217;3283;3802;4177;4306;4842;5557;5706;5857;6481;7144;7477;489;652;815;2119;1141;6683;498;830;1162;6806;501;668;835;2171;1169;6847;6153;769;1009;1097;1489;1597;1709;2069;2749;2897;3049;3529;3697;4409;4597;4789;1391;6469;7236;7649;2831;5111;6023;3182;3031;3899;5411;5971;6559;7819;3806;5038;6446;537;716;895;2327;1253;7339;3979;5267;6739;7544;7626;3478;6657;7749;573;764;955;2483;1337;5142;5862;746;898;2986;5098;5506;6174;6826;1958;3278;4499;5918;6974;597;796;995;2587;1393;829;941;1061;989;1621;1949;2309;2909;3149;3581;3821;4661;4861;6029;6661;6824;7156;7496;7669;618;824;1030;2678;1442;3427;6187;7291;633;844;1055;2743;1477;642;856;1070;2782;1498;6183;7311;7608;669;892;1115;2899;1561;3199;4487;4991;5999;6412;6839;797;953;1217;1973;2357;2633;2777;3557;4073;4253;4817;5013;5417;6053;6957;7193;7433;7677;681;908;1135;2951;1589;717;956;1195;3107;1673;1021;1082;1277;1346;1642;1721;2237;2621;2722;3037;3257;3602;3479;4217;4477;1474;4882;5021;1562;5897;1738;6362;6521;6603;1826;7177;7346;7517;5703;6459;7263;5363;7099;753;1004;1255;3263;1757;5726;7532;762;1016;2159;1270;3302;4699;1778;1186;2306;2578;2866;2914;3826;4178;4546;5074;6178;6626;6856;7328;7816;786;1048;2227;1310;3406;4847;1834;789;1052;1315;3419;1841;5709;7557;813;1084;1355;3523;1897;1727;2123;2563;3047;4763;6127;834;1112;2363;1390;3614;5143;1946;4619;849;1132;1415;3679;1981;817;1081;1993;2953;2881;3169;3337;4897;5769;6073;6544;6417;7369;7713;1069;1249;1549;1657;2129;2389;2957;3109;3929;4657;1751;5449;5657;1819;5869;6529;6774;7353;7647;4917;4854;6294;7086;906;1208;2567;1510;3926;5587;2114;7248;1102;6574;921;1228;1535;3991;2149;7368;7416;933;1244;1555;4043;2177;7464;1514;2474;4034;5994;6434;6566;7362;7604;978;1304;2771;1630;4238;6031;993;1324;1655;4303;6142;1002;1336;2839;1670;4342;6179;7266;1193;1538;1613;1933;2018;2194;2473;2978;3194;3418;3533;3769;4013;4138;4793;4731;5498;5794;6098;6231;6569;2158;7058;7394;3382;5662;7771;2359;2723;3983;4963;7439;1041;1388;1735;4511;2198;2443;2702;3262;3563;3878;4207;4907;5663;6062;7343;7798;1507;2651;5027;7051;7612;1074;1432;3043;1790;4654;6623;1077;1436;1795;4667;893;1381;1481;1693;1121;2293;1273;1349;1501;3301;3461;1577;3793;5081;5281;1957;5693;2033;6121;6793;2299;5403;7323;1101;1468;1835;4771;6258;1137;1516;1895;4927;1143;4953;1146;1528;3247;1910;4966;7067;1149;1532;1915;4979;5739;6267;6819;7692;6407;1877;1829;2221;2797;3221;3053;3677;3917;3773;4421;4957;5237;5821;1179;5109;2398;6556;1194;1592;3383;1990;5174;7363;1658;1882;2122;1978;3242;3898;4618;5818;6472;6298;6928;7162;7642;7437;3502;7622;4094;6854;7659;1251;5421;7733;1257;1676;2095;5447;1266;1688;3587;2110;5486;7807;7003;3638;1293;1724;2155;5603;5262;5982;1317;1756;2195;5707;1733;2081;2333;2741;3833;4733;5121;6381;6833;7301;7541;1329;1772;2215;5759;1338;1784;3791;2230;5798;3374;6398;1594;1669;1906;2161;2341;2434;3361;3946;3871;4714;4986;5266;5409;5554;5701;6309;6949;7114;7281;7621;7794;1359;5889;1362;1816;3859;2270;5902;1389;1852;2315;6019;1401;1868;2335;6071;1711;2983;3667;4427;5263;1434;1912;4063;2390;6214;1437;1916;2395;6227;2042;2554;3442;4474;5242;6074;6514;6486;7204;6958;4806;5286;6051;1461;1948;2435;6331;1467;6357;1473;1964;2455;6383;6474;1497;1996;2495;6487;1503;6513;1506;2008;4267;2510;6526;1509;2012;2515;6539;2779;4627;6139;6979;4791;5127;6207;1524;2032;4318;6604;1777;2281;2657;2857;3713;4481;5297;5881;7312;7481;7652;7313;1569;2092;2615;6276;6799;1572;2096;4454;6288;6812;5817;1578;2104;4471;2630;6312;6838;1889;1357;2377;1541;1587;2116;1633;3229;1817;1909;3709;3877;4049;4969;2369;5569;2461;6348;6877;7109;5251;6372;5159;6968;1611;6444;6981;3707;4279;6259;7799;1626;2168;4607;2710;6504;7046;1641;2188;2735;6564;7111;2134;3091;3454;3839;4246;5126;5599;6094;6611;7711;1668;2224;4726;6672;7228;5518;1689;2252;2815;6756;7319;1698;2264;4811;2830;6792;7358;2471;3227;3647;4571;6167;1713;2284;2855;6852;7423;1719;6876;7449;2231;3611;4439;5359;2645;6371;1634;2162;3986;5906;5762;6338;7016;6674;2053;2138;2498;2593;2789;3098;3314;3889;4133;4258;4067;4778;5189;5914;6218;6373;6689;7013;7107;1761;2348;2935;7044;7631;7657;5874;7722;1791;7164;7761;1797;2396;2995;7188;7787;4863;5847;6927;1812;2416;5134;1821;2428;3035;2603;3971;4579;1842;3070;2456;5219;5929;1854;1857;2476;3095;1866;3110;2488;5287;2297;2557;2693;2833;3433;3593;4273;4637;5413;6037;6473;6532;7393;1893;2524;3155;1899;1905;3175;6319;1926;1929;2572;3215;1941;2588;3235;2077;3397;3901;4549;4813;5653;5949;7048;7213;6901;7549;1956;2608;5542;1965;3275;5593;1977;2636;3295;1986;3310;2648;5627;2004;2672;5678;2007;5211;5919;6291;7071;7479;2386;3226;3866;4946;6388;6836;7066;7538;2043;2049;2732;3415;4142;6764;2611;3143;4718;5446;5831;2073;2764;3455;2082;3470;2776;5899;2085;3475;3934;4886;6524;7126;7756;3014;4598;5302;6776;6018;2148;2864;6086;2151;2154;3590;2872;6103;2157;2876;3595;2477;1786;2762;2861;2962;3386;2242;4457;4586;2546;5261;2698;3002;6602;6761;6922;3154;7417;7586;7757;4926;5163;6711;2181;2908;3635;2609;3329;2187;4877;5669;5877;6089;6977;2202;3670;2936;6239;3151;5543;7084;2217;2956;3695;2229;2972;3715;2253;3004;3755;2259;2265;3775;2274;3790;3032;6443;2286;6477;2292;3056;6494;2298;3830;3064;6511;6918;6966;7734;7654;4867;5983;7223;3754;3658;4442;5594;6442;6106;7354;2358;6681;2361;3148;3935;2367;4367;7271;2388;3184;6766;2801;2201;3001;3209;3881;3569;4889;5441;6329;6484;6961;7456;7796;2433;3244;4055;2439;2445;4075;2469;3292;4115;7004;5181;6369;7689;7021;2481;3308;4135;5014;7038;2502;7089;2505;4175;2514;4190;3352;7123;2517;3356;4195;3541;3701;4561;4933;5521;6361;6581;7741;2532;3376;7174;3431;3787;4711;5747;2547;7242;7276;2577;3436;4295;2586;4310;3448;7327;2589;3452;4315;5979;6507;4971;6387;7167;7378;2634;4390;3512;7463;3466;4162;4666;5482;6066;6217;6841;7002;7666;2649;3532;4415;2658;4430;3544;7531;2661;3548;4435;4445;3883;5071;5731;7183;2676;3568;7582;2685;4475;4151;6748;3338;4322;4682;5058;6282;6722;2718;7701;2721;3628;4535;2724;3632;7718;2733;3644;4555;4585;2757;3676;4595;2763;2778;3704;4630;2781;2527;6403;7391;2799;2802;3736;4670;3422;2841;3788;4735;3686;5339;5966;6631;7334;2865;4775;2868;3824;2874;3832;4790;2449;3761;2573;4093;4441;4621;2883;3844;4805;4993;5381;5581;3193;3317;6421;7561;2889;2901;3868;4835;3733;4973;5813;6413;6568;6884;6077;2913;3884;4855;5886;7422;4865;2922;3896;4870;2934;4890;2946;3928;4910;2949;3932;4915;2973;3964;4955;4247;6479;7471;2979;4965;2985;4975;2994;3992;4990;3006;5010;3012;4016;3018;4024;5030;5558;4839;5799;6054;6582;7419;2540;2667;3683;3048;4064;3556;6731;3057;4076;5095;3554;4562;4096;5314;5714;7712;7077;3090;5150;3093;4124;5155;3117;4156;5195;3123;5205;3138;4184;5230;2620;2751;3799;3144;4192;3668;6943;5901;6594;7329;3153;4204;5255;3156;4208;3165;5275;4228;5285;3778;2714;4129;4373;4754;3082;5153;3174;4232;5290;3266;6458;3634;5871;7253;3818;7418;7754;3189;4252;5315;7049;3210;5350;3222;5370;6751;3231;5385;4103;4939;7414;5079;6879;3252;4336;3261;4348;5435;3989;4157;4869;5849;6057;6269;7389;3273;4364;5455;3282;4376;5470;6182;6908;7678;3303;5505;3309;4412;5515;2780;2919;4031;3336;4448;3892;7367;3345;5575;6758;3369;4492;5615;3378;4504;5630;3703;7751;3396;4528;4532;4942;5299;6454;7294;3405;5675;7526;3411;5685;4564;5705;3426;4568;5710;3429;5715;3438;5730;3447;5745;4462;6463;7222;3453;4604;5755;4057;4297;4801;5337;6352;6976;6313;4106;5186;5578;6628;7778;5810;3489;4652;5815;4676;5845;3513;4684;5855;3522;4696;5870;7379;5631;6663;4708;3537;4716;5895;5383;7063;7679;3561;4748;5935;7194;3582;4776;5970;3585;5975;3594;4792;5990;4974;5646;6366;7536;4891;7303;3020;3171;4379;3624;4832;3642;4856;6070;5206;3669;4892;6115;4397;4937;6337;6553;6997;7457;7693;3684;4912;3693;4924;6155;3714;4952;6190;7521;3732;4976;4594;4721;5114;5386;5666;6101;6709;6866;7186;6099;7349;7681;3753;5004;6255;5012;6265;3765;6275;3771;5028;6285;3777;5036;6295;3786;5048;6310;3798;5064;6330;3810;6350;6390;7739;3837;5116;6395;3849;5132;6415;3858;5144;6430;3873;5164;6455;3879;5172;6465;3882;5176;6470;4154;7146;7376;5192;6490;3909;5212;6515;3260;3423;4727;3912;5216;6520;3921;5228;6535;3930;6550;3945;6575;3951;5268;6585;3954;5272;6590;3957;5276;6595;5199;6243;6999;3972;5296;6620;3981;5308;6635;5312;3987;5316;6645;5951;3993;5324;6655;7403;3340;3507;4843;4008;5344;6680;5348;6685;4014;5352;6690;5754;4782;5007;5238;5718;6483;7023;7302;7587;5437;5717;6301;6452;6917;7237;7732;4065;5420;6775;6785;4077;5436;6795;4086;5448;6810;4098;5464;6830;4101;5468;6835;7543;5009;5197;6197;7069;7297;7529;5222;6286;5891;4146;5528;6910;4164;5552;6940;4167;5556;6945;4170;5560;6950;5572;6965;4191;5588;6985;4197;5596;6995;5803;6587;7427;4203;5604;7005;7035;6523;4245;5660;7075;7110;4269;5692;7115;5529;4281;5708;7135;3580;3759;5191;4296;5728;7160;4302;5736;7170;4308;5744;7180;4311;5748;7185;4314;5752;7190;4317;5756;7195;4323;5764;7205;7210;4954;5722;6772;5776;7220;4341;5788;7235;4353;5804;7255;6126;7662;4362;5816;7270;7285;5218;3834;6354;5047;6658;6813;4266;7129;4374;7290;4377;5836;7295;4383;5844;7305;7315;4401;5868;7335;4404;5872;7340;4413;5884;7355;6302;4419;5892;7365;4422;5908;7385;4434;5912;7390;4449;5932;7415;4458;5944;7430;4461;5948;7435;7455;7470;4491;5988;7485;7490;4497;5996;7495;4506;6008;7510;4509;6012;7515;6439;4518;6024;7530;4527;6036;7545;4530;6040;7550;4533;6044;7555;4548;6064;7580;4123;7595;5273;5861;6701;6921;4569;6092;7615;4572;6096;7620;3820;4011;5539;4584;6112;7640;4587;6116;7645;4593;6124;7655;4596;6128;7660;4605;6140;7675;5331;4779;6843;6707;7695;7705;4629;6172;7715;7725;6014;7755;4665;6220;7775;4677;6236;7795;6244;7805;6248;7810;6113;4841;6713;7184;7508;7673;5579;6671;5566;5667;7131;3980;4179;5771;5602;4402;6002;6418;6632;7528;7762;5829;4326;5974;6402;5819;6499;5741;6353;6781;7001;6317;5243;7082;7402;4220;4431;6119;6862;7147;7574;7413;4494;6206;4902;7398;6159;6414;7494;7779;6714;6932;7766;4460;4683;6467;7672;4429;6229;6376;6676;5029;6829;7461;7624;7789;4540;4767;6583;7809;4601;7309;7537;7519;7087;5054;4761;6891;7671;7372;4780;5019;6931;6737;4898;7522;7469;5885;7811;7018;7466;7221;5020;5271;7279;5719;7483;7173;7158;5080;5334;7366;7108;7482;5240;5502;7598;5260;5523;7627;5214;7556;7714;7772;7431;5358;7489;5346;7717;17;209;6138;6762;1271;332;6944;418;2989;1919;658;2542;321;1891;649;869;7452;5022;5978;6969;1558;1079;5428;3131;5959;5311;1139;682;3782;1219;6831;1298;3721;5922;1369;4819;5453;7448;2071;6432;1159;1598;2911;2278;2438;4859;7171;7442;5976;2738;1462;7029;5822;5828;1342;2318;5642;3350;3296;2291;3424;6622;5487;5459;4635;3610;2759;3379;2568;4815;5671;2948;2166;4120;4949;3071;4280;4648;2739;3399;5768;3531;5992;5082;6972;2905;3685;2996;3745;5170;4136;6431;6461;6640;3751;6162;3618;5896;7370;4482;6164;4686;4818;4582;4223;5665;5586;341;3599;7553;7198;671;2884;5457;4387;5369;7387;2472;721;5253;3652;4565;6059;3959;5329]".
Extract Inlined Constant force => "Lazy.force".
Extract Inlined Constant fromVal => "Lazy.from_val".
Extract Constant LazyT "'a" => "'a Lazy.t".
Extraction "Coq" The_Asymmetric_CNF Cubed_CNF refute.
Require Import CubeAndConquer.
Require Import SetChecker.
Extraction Language Ocaml.
Extract Inductive positive => int [ "(fun x -> 2*x+1)" "(fun x -> 2*x)" "1" ]
"(fun fI fO fH n -> if n=1 then fH () else if n mod 2 = 0 then fO (n/2) else fI (n/2))".
Extract Inlined Constant Pos.compare => "(fun x y -> if x = y then Eq else (if x < y then Lt else Gt))".
Extract Inductive nat => int [ "0" "Pervasives.succ" ]
"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Constant TheBreak => "2520".
Extract Constant TheN => "7826".
Extract Constant The_List => "let rec ltl l = (match l with | [] -> Nil | x::m -> Cons (x,ltl m)) in ltl [3;4;5;7;11;13;19;181;23;313;421;31;613;761;43;1013;47;1201;1301;59;1741;61;1861;2113;67;2381;71;2521;79;3121;83;3613;4513;5101;103;107;7321;7812;6;8;10;14;101;22;26;197;226;257;38;362;401;46;577;626;677;842;62;1226;1297;1522;1601;86;2026;94;2303;2402;2602;2917;3137;118;3482;122;3722;4226;4357;134;4762;4899;142;5042;5477;158;6242;6399;6723;166;7057;7226;7568;5223;5583;6339;7143;7563;202;394;514;802;1154;1354;2594;3202;4606;5834;6274;6726;6964;7444;4803;6078;6909;7206;7806;49;2947;4291;5327;7091;29;173;229;293;733;1093;1229;1373;2021;2029;2213;3253;4229;4493;4757;5333;6404;6557;7229;7573;149;269;317;617;929;1109;1409;2969;3449;3617;4517;5309;5517;6389;6849;7316;7817;121;1991;3443;4631;6743;7356;7782;98;2534;2807;4039;4382;4739;5894;58;346;458;586;874;1466;2186;2458;2746;4042;4058;4426;6506;6736;178;298;409;538;634;1033;1234;1453;1609;1858;2218;2713;2818;3373;3853;4909;5193;5634;5938;6093;6733;6898;7234;7578;7753;361;3439;5947;6573;242;2167;2486;2827;3982;4411;6347;6886;7447;4163;529;7199;6063;6087;6639;157;193;233;277;433;557;773;853;937;1117;1213;1637;1753;1873;1997;2393;2677;3457;3797;4153;4337;5113;5737;5953;6173;6397;6857;7333;7552;7577;4887;2758;3598;5614;5611;137;241;457;641;713;857;977;1697;2417;2617;3041;3953;4241;5609;5641;6257;6416;6577;5973;218;818;2066;2906;3218;4214;5426;6746;7218;7706;3743;4294;4883;722;6878;7581;7619;7602;7783;2222;4334;5654;4531;5198;5911;6558;7374;337;389;569;709;1129;343;1429;2137;2269;2689;2837;3469;3637;4349;4729;5749;6637;6869;7589;194;281;314;349;386;466;509;554;601;701;809;866;1049;1114;1181;1321;1546;1706;1789;1874;2141;2234;2426;2729;2891;3274;3389;3506;3746;3994;4649;4786;5209;5354;5451;5501;5751;5801;6914;7594;7719;4827;5319;5574;6102;6321;6654;6939;5131;7196;7651;6441;6667;6107;7006;2219;4319;6503;7763;274;482;914;1282;1426;1714;1954;3394;4834;5234;6082;6304;7168;7232;6501;7458;268;469;7571;7797;397;589;661;877;997;1333;2437;2773;3061;3517;4189;4261;5077;5293;5589;5893;6277;6436;6597;7432;7533;4911;5259;5619;5991;7179;3838;7486;353;461;521;653;881;1553;1901;2153;4001;5553;5981;6653;7121;249;415;581;1591;1903;2519;3223;4646;1739;5091;7251;373;449;674;778;1138;1418;1493;2258;686;2549;2753;2858;3413;4274;4538;4673;5233;5378;5427;5674;5727;6133;6449;6938;7274;7347;7793;1639;2959;3487;6787;562;698;1018;1202;1402;1618;2098;2362;2642;3578;4282;5458;5782;6548;6778;7012;7492;7638;309;412;428;535;749;5454;6198;7404;2422;3206;4102;6118;541;673;821;1361;1801;2441;3181;3673;4021;4201;4961;5573;6221;6673;1331;7381;7504;6262;2863;3766;4438;7231;381;508;635;1651;889;5207;1397;7747;593;1153;1289;1433;1457;1913;2089;2273;2537;3089;3313;4289;5393;5561;5689;6464;6788;6992;7808;393;524;655;1703;917;5371;6534;6666;938;417;556;695;1807;973;5699;794;1178;1322;1754;1994;2666;4874;5274;5546;6122;7034;6411;6807;5118;5367;5622;6423;6702;7278;453;604;755;1963;1057;6191;3287;4351;5567;7676;7623;7777;6478;706;757;922;1042;1237;1306;1762;2017;3106;3217;3283;3802;4177;4306;4842;5557;5706;5857;6481;7144;7477;489;652;815;2119;1141;6683;498;830;1162;6806;501;668;835;2171;1169;6847;6153;769;1009;1097;1489;1597;1709;2069;2749;2897;3049;3529;3697;4409;4597;4789;1391;6469;7236;7649;2831;5111;6023;3182;3031;3899;5411;5971;6559;7819;3806;5038;6446;537;716;895;2327;1253;7339;3979;5267;6739;7544;7626;3478;6657;7749;573;764;955;2483;1337;5142;5862;746;898;2986;5098;5506;6174;6826;1958;3278;4499;5918;6974;597;796;995;2587;1393;829;941;1061;989;1621;1949;2309;2909;3149;3581;3821;4661;4861;6029;6661;6824;7156;7496;7669;618;824;1030;2678;1442;3427;6187;7291;633;844;1055;2743;1477;642;856;1070;2782;1498;6183;7311;7608;669;892;1115;2899;1561;3199;4487;4991;5999;6412;6839;797;953;1217;1973;2357;2633;2777;3557;4073;4253;4817;5013;5417;6053;6957;7193;7433;7677;681;908;1135;2951;1589;717;956;1195;3107;1673;1021;1082;1277;1346;1642;1721;2237;2621;2722;3037;3257;3602;3479;4217;4477;1474;4882;5021;1562;5897;1738;6362;6521;6603;1826;7177;7346;7517;5703;6459;7263;5363;7099;753;1004;1255;3263;1757;5726;7532;762;1016;2159;1270;3302;4699;1778;1186;2306;2578;2866;2914;3826;4178;4546;5074;6178;6626;6856;7328;7816;786;1048;2227;1310;3406;4847;1834;789;1052;1315;3419;1841;5709;7557;813;1084;1355;3523;1897;1727;2123;2563;3047;4763;6127;834;1112;2363;1390;3614;5143;1946;4619;849;1132;1415;3679;1981;817;1081;1993;2953;2881;3169;3337;4897;5769;6073;6544;6417;7369;7713;1069;1249;1549;1657;2129;2389;2957;3109;3929;4657;1751;5449;5657;1819;5869;6529;6774;7353;7647;4917;4854;6294;7086;906;1208;2567;1510;3926;5587;2114;7248;1102;6574;921;1228;1535;3991;2149;7368;7416;933;1244;1555;4043;2177;7464;1514;2474;4034;5994;6434;6566;7362;7604;978;1304;2771;1630;4238;6031;993;1324;1655;4303;6142;1002;1336;2839;1670;4342;6179;7266;1193;1538;1613;1933;2018;2194;2473;2978;3194;3418;3533;3769;4013;4138;4793;4731;5498;5794;6098;6231;6569;2158;7058;7394;3382;5662;7771;2359;2723;3983;4963;7439;1041;1388;1735;4511;2198;2443;2702;3262;3563;3878;4207;4907;5663;6062;7343;7798;1507;2651;5027;7051;7612;1074;1432;3043;1790;4654;6623;1077;1436;1795;4667;893;1381;1481;1693;1121;2293;1273;1349;1501;3301;3461;1577;3793;5081;5281;1957;5693;2033;6121;6793;2299;5403;7323;1101;1468;1835;4771;6258;1137;1516;1895;4927;1143;4953;1146;1528;3247;1910;4966;7067;1149;1532;1915;4979;5739;6267;6819;7692;6407;1877;1829;2221;2797;3221;3053;3677;3917;3773;4421;4957;5237;5821;1179;5109;2398;6556;1194;1592;3383;1990;5174;7363;1658;1882;2122;1978;3242;3898;4618;5818;6472;6298;6928;7162;7642;7437;3502;7622;4094;6854;7659;1251;5421;7733;1257;1676;2095;5447;1266;1688;3587;2110;5486;7807;7003;3638;1293;1724;2155;5603;5262;5982;1317;1756;2195;5707;1733;2081;2333;2741;3833;4733;5121;6381;6833;7301;7541;1329;1772;2215;5759;1338;1784;3791;2230;5798;3374;6398;1594;1669;1906;2161;2341;2434;3361;3946;3871;4714;4986;5266;5409;5554;5701;6309;6949;7114;7281;7621;7794;1359;5889;1362;1816;3859;2270;5902;1389;1852;2315;6019;1401;1868;2335;6071;1711;2983;3667;4427;5263;1434;1912;4063;2390;6214;1437;1916;2395;6227;2042;2554;3442;4474;5242;6074;6514;6486;7204;6958;4806;5286;6051;1461;1948;2435;6331;1467;6357;1473;1964;2455;6383;6474;1497;1996;2495;6487;1503;6513;1506;2008;4267;2510;6526;1509;2012;2515;6539;2779;4627;6139;6979;4791;5127;6207;1524;2032;4318;6604;1777;2281;2657;2857;3713;4481;5297;5881;7312;7481;7652;7313;1569;2092;2615;6276;6799;1572;2096;4454;6288;6812;5817;1578;2104;4471;2630;6312;6838;1889;1357;2377;1541;1587;2116;1633;3229;1817;1909;3709;3877;4049;4969;2369;5569;2461;6348;6877;7109;5251;6372;5159;6968;1611;6444;6981;3707;4279;6259;7799;1626;2168;4607;2710;6504;7046;1641;2188;2735;6564;7111;2134;3091;3454;3839;4246;5126;5599;6094;6611;7711;1668;2224;4726;6672;7228;5518;1689;2252;2815;6756;7319;1698;2264;4811;2830;6792;7358;2471;3227;3647;4571;6167;1713;2284;2855;6852;7423;1719;6876;7449;2231;3611;4439;5359;2645;6371;1634;2162;3986;5906;5762;6338;7016;6674;2053;2138;2498;2593;2789;3098;3314;3889;4133;4258;4067;4778;5189;5914;6218;6373;6689;7013;7107;1761;2348;2935;7044;7631;7657;5874;7722;1791;7164;7761;1797;2396;2995;7188;7787;4863;5847;6927;1812;2416;5134;1821;2428;3035;2603;3971;4579;1842;3070;2456;5219;5929;1854;1857;2476;3095;1866;3110;2488;5287;2297;2557;2693;2833;3433;3593;4273;4637;5413;6037;6473;6532;7393;1893;2524;3155;1899;1905;3175;6319;1926;1929;2572;3215;1941;2588;3235;2077;3397;3901;4549;4813;5653;5949;7048;7213;6901;7549;1956;2608;5542;1965;3275;5593;1977;2636;3295;1986;3310;2648;5627;2004;2672;5678;2007;5211;5919;6291;7071;7479;2386;3226;3866;4946;6388;6836;7066;7538;2043;2049;2732;3415;4142;6764;2611;3143;4718;5446;5831;2073;2764;3455;2082;3470;2776;5899;2085;3475;3934;4886;6524;7126;7756;3014;4598;5302;6776;6018;2148;2864;6086;2151;2154;3590;2872;6103;2157;2876;3595;2477;1786;2762;2861;2962;3386;2242;4457;4586;2546;5261;2698;3002;6602;6761;6922;3154;7417;7586;7757;4926;5163;6711;2181;2908;3635;2609;3329;2187;4877;5669;5877;6089;6977;2202;3670;2936;6239;3151;5543;7084;2217;2956;3695;2229;2972;3715;2253;3004;3755;2259;2265;3775;2274;3790;3032;6443;2286;6477;2292;3056;6494;2298;3830;3064;6511;6918;6966;7734;7654;4867;5983;7223;3754;3658;4442;5594;6442;6106;7354;2358;6681;2361;3148;3935;2367;4367;7271;2388;3184;6766;2801;2201;3001;3209;3881;3569;4889;5441;6329;6484;6961;7456;7796;2433;3244;4055;2439;2445;4075;2469;3292;4115;7004;5181;6369;7689;7021;2481;3308;4135;5014;7038;2502;7089;2505;4175;2514;4190;3352;7123;2517;3356;4195;3541;3701;4561;4933;5521;6361;6581;7741;2532;3376;7174;3431;3787;4711;5747;2547;7242;7276;2577;3436;4295;2586;4310;3448;7327;2589;3452;4315;5979;6507;4971;6387;7167;7378;2634;4390;3512;7463;3466;4162;4666;5482;6066;6217;6841;7002;7666;2649;3532;4415;2658;4430;3544;7531;2661;3548;4435;4445;3883;5071;5731;7183;2676;3568;7582;2685;4475;4151;6748;3338;4322;4682;5058;6282;6722;2718;7701;2721;3628;4535;2724;3632;7718;2733;3644;4555;4585;2757;3676;4595;2763;2778;3704;4630;2781;2527;6403;7391;2799;2802;3736;4670;3422;2841;3788;4735;3686;5339;5966;6631;7334;2865;4775;2868;3824;2874;3832;4790;2449;3761;2573;4093;4441;4621;2883;3844;4805;4993;5381;5581;3193;3317;6421;7561;2889;2901;3868;4835;3733;4973;5813;6413;6568;6884;6077;2913;3884;4855;5886;7422;4865;2922;3896;4870;2934;4890;2946;3928;4910;2949;3932;4915;2973;3964;4955;4247;6479;7471;2979;4965;2985;4975;2994;3992;4990;3006;5010;3012;4016;3018;4024;5030;5558;4839;5799;6054;6582;7419;2540;2667;3683;3048;4064;3556;6731;3057;4076;5095;3554;4562;4096;5314;5714;7712;7077;3090;5150;3093;4124;5155;3117;4156;5195;3123;5205;3138;4184;5230;2620;2751;3799;3144;4192;3668;6943;5901;6594;7329;3153;4204;5255;3156;4208;3165;5275;4228;5285;3778;2714;4129;4373;4754;3082;5153;3174;4232;5290;3266;6458;3634;5871;7253;3818;7418;7754;3189;4252;5315;7049;3210;5350;3222;5370;6751;3231;5385;4103;4939;7414;5079;6879;3252;4336;3261;4348;5435;3989;4157;4869;5849;6057;6269;7389;3273;4364;5455;3282;4376;5470;6182;6908;7678;3303;5505;3309;4412;5515;2780;2919;4031;3336;4448;3892;7367;3345;5575;6758;3369;4492;5615;3378;4504;5630;3703;7751;3396;4528;4532;4942;5299;6454;7294;3405;5675;7526;3411;5685;4564;5705;3426;4568;5710;3429;5715;3438;5730;3447;5745;4462;6463;7222;3453;4604;5755;4057;4297;4801;5337;6352;6976;6313;4106;5186;5578;6628;7778;5810;3489;4652;5815;4676;5845;3513;4684;5855;3522;4696;5870;7379;5631;6663;4708;3537;4716;5895;5383;7063;7679;3561;4748;5935;7194;3582;4776;5970;3585;5975;3594;4792;5990;4974;5646;6366;7536;4891;7303;3020;3171;4379;3624;4832;3642;4856;6070;5206;3669;4892;6115;4397;4937;6337;6553;6997;7457;7693;3684;4912;3693;4924;6155;3714;4952;6190;7521;3732;4976;4594;4721;5114;5386;5666;6101;6709;6866;7186;6099;7349;7681;3753;5004;6255;5012;6265;3765;6275;3771;5028;6285;3777;5036;6295;3786;5048;6310;3798;5064;6330;3810;6350;6390;7739;3837;5116;6395;3849;5132;6415;3858;5144;6430;3873;5164;6455;3879;5172;6465;3882;5176;6470;4154;7146;7376;5192;6490;3909;5212;6515;3260;3423;4727;3912;5216;6520;3921;5228;6535;3930;6550;3945;6575;3951;5268;6585;3954;5272;6590;3957;5276;6595;5199;6243;6999;3972;5296;6620;3981;5308;6635;5312;3987;5316;6645;5951;3993;5324;6655;7403;3340;3507;4843;4008;5344;6680;5348;6685;4014;5352;6690;5754;4782;5007;5238;5718;6483;7023;7302;7587;5437;5717;6301;6452;6917;7237;7732;4065;5420;6775;6785;4077;5436;6795;4086;5448;6810;4098;5464;6830;4101;5468;6835;7543;5009;5197;6197;7069;7297;7529;5222;6286;5891;4146;5528;6910;4164;5552;6940;4167;5556;6945;4170;5560;6950;5572;6965;4191;5588;6985;4197;5596;6995;5803;6587;7427;4203;5604;7005;7035;6523;4245;5660;7075;7110;4269;5692;7115;5529;4281;5708;7135;3580;3759;5191;4296;5728;7160;4302;5736;7170;4308;5744;7180;4311;5748;7185;4314;5752;7190;4317;5756;7195;4323;5764;7205;7210;4954;5722;6772;5776;7220;4341;5788;7235;4353;5804;7255;6126;7662;4362;5816;7270;7285;5218;3834;6354;5047;6658;6813;4266;7129;4374;7290;4377;5836;7295;4383;5844;7305;7315;4401;5868;7335;4404;5872;7340;4413;5884;7355;6302;4419;5892;7365;4422;5908;7385;4434;5912;7390;4449;5932;7415;4458;5944;7430;4461;5948;7435;7455;7470;4491;5988;7485;7490;4497;5996;7495;4506;6008;7510;4509;6012;7515;6439;4518;6024;7530;4527;6036;7545;4530;6040;7550;4533;6044;7555;4548;6064;7580;4123;7595;5273;5861;6701;6921;4569;6092;7615;4572;6096;7620;3820;4011;5539;4584;6112;7640;4587;6116;7645;4593;6124;7655;4596;6128;7660;4605;6140;7675;5331;4779;6843;6707;7695;7705;4629;6172;7715;7725;6014;7755;4665;6220;7775;4677;6236;7795;6244;7805;6248;7810;6113;4841;6713;7184;7508;7673;5579;6671;5566;5667;7131;3980;4179;5771;5602;4402;6002;6418;6632;7528;7762;5829;4326;5974;6402;5819;6499;5741;6353;6781;7001;6317;5243;7082;7402;4220;4431;6119;6862;7147;7574;7413;4494;6206;4902;7398;6159;6414;7494;7779;6714;6932;7766;4460;4683;6467;7672;4429;6229;6376;6676;5029;6829;7461;7624;7789;4540;4767;6583;7809;4601;7309;7537;7519;7087;5054;4761;6891;7671;7372;4780;5019;6931;6737;4898;7522;7469;5885;7811;7018;7466;7221;5020;5271;7279;5719;7483;7173;7158;5080;5334;7366;7108;7482;5240;5502;7598;5260;5523;7627;5214;7556;7714;7772;7431;5358;7489;5346;7717;17;209;6138;6762;1271;332;6944;418;2989;1919;658;2542;321;1891;649;869;7452;5022;5978;6969;1558;1079;5428;3131;5959;5311;1139;682;3782;1219;6831;1298;3721;5922;1369;4819;5453;7448;2071;6432;1159;1598;2911;2278;2438;4859;7171;7442;5976;2738;1462;7029;5822;5828;1342;2318;5642;3350;3296;2291;3424;6622;5487;5459;4635;3610;2759;3379;2568;4815;5671;2948;2166;4120;4949;3071;4280;4648;2739;3399;5768;3531;5992;5082;6972;2905;3685;2996;3745;5170;4136;6431;6461;6640;3751;6162;3618;5896;7370;4482;6164;4686;4818;4582;4223;5665;5586;341;3599;7553;7198;671;2884;5457;4387;5369;7387;2472;721;5253;3652;4565;6059;3959;5329]".
Extract Inlined Constant force => "Lazy.force".
Extract Inlined Constant fromVal => "Lazy.from_val".
Extract Constant LazyT "'a" => "'a Lazy.t".
Extraction "Coq" The_Asymmetric_CNF Cubed_CNF refute.