%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : LCL675+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:57:09 AM UTC 2026
% Result : CounterSatisfiable 17.96s 3.13s
% Output : FiniteModel 18.06s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d62"
| X = "d61"
| X = "d60"
| X = "d59"
| X = "d58"
| X = "d57"
| X = "d56"
| X = "d55"
| X = "d54"
| X = "d53"
| X = "d52"
| X = "d51"
| X = "d50"
| X = "d49"
| X = "d48"
| X = "d47"
| X = "d46"
| X = "d45"
| X = "d44"
| X = "d43"
| X = "d42"
| X = "d41"
| X = "d40"
| X = "d39"
| X = "d38"
| X = "d37"
| X = "d36"
| X = "d35"
| X = "d34"
| X = "d33"
| X = "d32"
| X = "d31"
| X = "d30"
| X = "d29"
| X = "d28"
| X = "d27"
| X = "d26"
| X = "d25"
| X = "d24"
| X = "d23"
| X = "d22"
| X = "d21"
| X = "d20"
| X = "d19"
| X = "d18"
| X = "d17"
| X = "d16"
| X = "d15"
| X = "d14"
| X = "d13"
| X = "d12"
| X = "d11"
| X = "d10"
| X = "d9"
| X = "d8"
| X = "d7"
| X = "d6"
| X = "d5"
| X = "d4"
| X = "d3"
| X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( f10("d62") = "d0"
& f10("d61") = "d0"
& f10("d60") = "d0"
& f10("d59") = "d0"
& f10("d58") = "d0"
& f10("d57") = "d0"
& f10("d56") = "d0"
& f10("d55") = "d0"
& f10("d54") = "d0"
& f10("d53") = "d0"
& f10("d52") = "d0"
& f10("d51") = "d0"
& f10("d50") = "d0"
& f10("d49") = "d0"
& f10("d48") = "d0"
& f10("d47") = "d0"
& f10("d46") = "d0"
& f10("d45") = "d0"
& f10("d44") = "d0"
& f10("d43") = "d0"
& f10("d42") = "d0"
& f10("d41") = "d0"
& f10("d40") = "d0"
& f10("d39") = "d0"
& f10("d38") = "d0"
& f10("d37") = "d0"
& f10("d36") = "d0"
& f10("d35") = "d0"
& f10("d34") = "d0"
& f10("d33") = "d0"
& f10("d32") = "d0"
& f10("d31") = "d0"
& f10("d30") = "d0"
& f10("d29") = "d0"
& f10("d28") = "d0"
& f10("d27") = "d0"
& f10("d26") = "d0"
& f10("d25") = "d0"
& f10("d24") = "d0"
& f10("d23") = "d0"
& f10("d22") = "d0"
& f10("d21") = "d0"
& f10("d20") = "d0"
& f10("d19") = "d0"
& f10("d18") = "d0"
& f10("d17") = "d0"
& f10("d16") = "d0"
& f10("d15") = "d0"
& f10("d14") = "d0"
& f10("d13") = "d0"
& f10("d12") = "d0"
& f10("d11") = "d0"
& f10("d10") = "d0"
& f10("d9") = "d0"
& f10("d8") = "d0"
& f10("d7") = "d0"
& f10("d6") = "d0"
& f10("d5") = "d0"
& f10("d4") = "d0"
& f10("d3") = "d0"
& f10("d2") = "d0"
& f10("d1") = "d0"
& f10("d0") = "d2"
& f9("d62") = "d0"
& f9("d61") = "d0"
& f9("d60") = "d0"
& f9("d59") = "d0"
& f9("d58") = "d0"
& f9("d57") = "d0"
& f9("d56") = "d0"
& f9("d55") = "d0"
& f9("d54") = "d0"
& f9("d53") = "d0"
& f9("d52") = "d0"
& f9("d51") = "d0"
& f9("d50") = "d0"
& f9("d49") = "d0"
& f9("d48") = "d0"
& f9("d47") = "d0"
& f9("d46") = "d0"
& f9("d45") = "d0"
& f9("d44") = "d0"
& f9("d43") = "d0"
& f9("d42") = "d0"
& f9("d41") = "d0"
& f9("d40") = "d0"
& f9("d39") = "d0"
& f9("d38") = "d0"
& f9("d37") = "d0"
& f9("d36") = "d0"
& f9("d35") = "d0"
& f9("d34") = "d0"
& f9("d33") = "d0"
& f9("d32") = "d0"
& f9("d31") = "d0"
& f9("d30") = "d0"
& f9("d29") = "d0"
& f9("d28") = "d0"
& f9("d27") = "d0"
& f9("d26") = "d0"
& f9("d25") = "d0"
& f9("d24") = "d0"
& f9("d23") = "d0"
& f9("d22") = "d0"
& f9("d21") = "d0"
& f9("d20") = "d0"
& f9("d19") = "d0"
& f9("d18") = "d0"
& f9("d17") = "d0"
& f9("d16") = "d0"
& f9("d15") = "d0"
& f9("d14") = "d0"
& f9("d13") = "d0"
& f9("d12") = "d0"
& f9("d11") = "d0"
& f9("d10") = "d0"
& f9("d9") = "d0"
& f9("d8") = "d0"
& f9("d7") = "d0"
& f9("d6") = "d0"
& f9("d5") = "d0"
& f9("d4") = "d0"
& f9("d3") = "d0"
& f9("d2") = "d0"
& f9("d1") = "d0"
& f9("d0") = "d1"
& f8("d62") = "d0"
& f8("d61") = "d0"
& f8("d60") = "d0"
& f8("d59") = "d0"
& f8("d58") = "d0"
& f8("d57") = "d0"
& f8("d56") = "d0"
& f8("d55") = "d0"
& f8("d54") = "d0"
& f8("d53") = "d0"
& f8("d52") = "d0"
& f8("d51") = "d0"
& f8("d50") = "d0"
& f8("d49") = "d0"
& f8("d48") = "d0"
& f8("d47") = "d0"
& f8("d46") = "d0"
& f8("d45") = "d0"
& f8("d44") = "d0"
& f8("d43") = "d0"
& f8("d42") = "d0"
& f8("d41") = "d0"
& f8("d40") = "d0"
& f8("d39") = "d0"
& f8("d38") = "d0"
& f8("d37") = "d0"
& f8("d36") = "d0"
& f8("d35") = "d0"
& f8("d34") = "d0"
& f8("d33") = "d0"
& f8("d32") = "d0"
& f8("d31") = "d0"
& f8("d30") = "d0"
& f8("d29") = "d0"
& f8("d28") = "d0"
& f8("d27") = "d0"
& f8("d26") = "d0"
& f8("d25") = "d0"
& f8("d24") = "d0"
& f8("d23") = "d0"
& f8("d22") = "d0"
& f8("d21") = "d0"
& f8("d20") = "d0"
& f8("d19") = "d0"
& f8("d18") = "d0"
& f8("d17") = "d0"
& f8("d16") = "d0"
& f8("d15") = "d0"
& f8("d14") = "d0"
& f8("d13") = "d0"
& f8("d12") = "d0"
& f8("d11") = "d0"
& f8("d10") = "d0"
& f8("d9") = "d0"
& f8("d8") = "d0"
& f8("d7") = "d0"
& f8("d6") = "d0"
& f8("d5") = "d0"
& f8("d4") = "d0"
& f8("d3") = "d0"
& f8("d2") = "d6"
& f8("d1") = "d4"
& f8("d0") = "d0"
& f7("d62") = "d0"
& f7("d61") = "d0"
& f7("d60") = "d0"
& f7("d59") = "d0"
& f7("d58") = "d0"
& f7("d57") = "d0"
& f7("d56") = "d0"
& f7("d55") = "d0"
& f7("d54") = "d0"
& f7("d53") = "d0"
& f7("d52") = "d0"
& f7("d51") = "d0"
& f7("d50") = "d0"
& f7("d49") = "d0"
& f7("d48") = "d0"
& f7("d47") = "d0"
& f7("d46") = "d0"
& f7("d45") = "d0"
& f7("d44") = "d0"
& f7("d43") = "d0"
& f7("d42") = "d0"
& f7("d41") = "d0"
& f7("d40") = "d0"
& f7("d39") = "d0"
& f7("d38") = "d0"
& f7("d37") = "d0"
& f7("d36") = "d0"
& f7("d35") = "d0"
& f7("d34") = "d0"
& f7("d33") = "d0"
& f7("d32") = "d0"
& f7("d31") = "d0"
& f7("d30") = "d0"
& f7("d29") = "d0"
& f7("d28") = "d0"
& f7("d27") = "d0"
& f7("d26") = "d0"
& f7("d25") = "d0"
& f7("d24") = "d0"
& f7("d23") = "d0"
& f7("d22") = "d0"
& f7("d21") = "d0"
& f7("d20") = "d0"
& f7("d19") = "d0"
& f7("d18") = "d0"
& f7("d17") = "d0"
& f7("d16") = "d0"
& f7("d15") = "d0"
& f7("d14") = "d0"
& f7("d13") = "d0"
& f7("d12") = "d0"
& f7("d11") = "d0"
& f7("d10") = "d0"
& f7("d9") = "d0"
& f7("d8") = "d0"
& f7("d7") = "d0"
& f7("d6") = "d0"
& f7("d5") = "d0"
& f7("d4") = "d0"
& f7("d3") = "d0"
& f7("d2") = "d5"
& f7("d1") = "d3"
& f7("d0") = "d0"
& f6("d62") = "d0"
& f6("d61") = "d0"
& f6("d60") = "d0"
& f6("d59") = "d0"
& f6("d58") = "d0"
& f6("d57") = "d0"
& f6("d56") = "d0"
& f6("d55") = "d0"
& f6("d54") = "d0"
& f6("d53") = "d0"
& f6("d52") = "d0"
& f6("d51") = "d0"
& f6("d50") = "d0"
& f6("d49") = "d0"
& f6("d48") = "d0"
& f6("d47") = "d0"
& f6("d46") = "d0"
& f6("d45") = "d0"
& f6("d44") = "d0"
& f6("d43") = "d0"
& f6("d42") = "d0"
& f6("d41") = "d0"
& f6("d40") = "d0"
& f6("d39") = "d0"
& f6("d38") = "d0"
& f6("d37") = "d0"
& f6("d36") = "d0"
& f6("d35") = "d0"
& f6("d34") = "d0"
& f6("d33") = "d0"
& f6("d32") = "d0"
& f6("d31") = "d0"
& f6("d30") = "d0"
& f6("d29") = "d0"
& f6("d28") = "d0"
& f6("d27") = "d0"
& f6("d26") = "d0"
& f6("d25") = "d0"
& f6("d24") = "d0"
& f6("d23") = "d0"
& f6("d22") = "d0"
& f6("d21") = "d0"
& f6("d20") = "d0"
& f6("d19") = "d0"
& f6("d18") = "d0"
& f6("d17") = "d0"
& f6("d16") = "d0"
& f6("d15") = "d0"
& f6("d14") = "d0"
& f6("d13") = "d0"
& f6("d12") = "d0"
& f6("d11") = "d0"
& f6("d10") = "d0"
& f6("d9") = "d0"
& f6("d8") = "d0"
& f6("d7") = "d0"
& f6("d6") = "d14"
& f6("d5") = "d12"
& f6("d4") = "d10"
& f6("d3") = "d8"
& f6("d2") = "d0"
& f6("d1") = "d0"
& f6("d0") = "d0"
& f5("d62") = "d0"
& f5("d61") = "d0"
& f5("d60") = "d0"
& f5("d59") = "d0"
& f5("d58") = "d0"
& f5("d57") = "d0"
& f5("d56") = "d0"
& f5("d55") = "d0"
& f5("d54") = "d0"
& f5("d53") = "d0"
& f5("d52") = "d0"
& f5("d51") = "d0"
& f5("d50") = "d0"
& f5("d49") = "d0"
& f5("d48") = "d0"
& f5("d47") = "d0"
& f5("d46") = "d0"
& f5("d45") = "d0"
& f5("d44") = "d0"
& f5("d43") = "d0"
& f5("d42") = "d0"
& f5("d41") = "d0"
& f5("d40") = "d0"
& f5("d39") = "d0"
& f5("d38") = "d0"
& f5("d37") = "d0"
& f5("d36") = "d0"
& f5("d35") = "d0"
& f5("d34") = "d0"
& f5("d33") = "d0"
& f5("d32") = "d0"
& f5("d31") = "d0"
& f5("d30") = "d0"
& f5("d29") = "d0"
& f5("d28") = "d0"
& f5("d27") = "d0"
& f5("d26") = "d0"
& f5("d25") = "d0"
& f5("d24") = "d0"
& f5("d23") = "d0"
& f5("d22") = "d0"
& f5("d21") = "d0"
& f5("d20") = "d0"
& f5("d19") = "d0"
& f5("d18") = "d0"
& f5("d17") = "d0"
& f5("d16") = "d0"
& f5("d15") = "d0"
& f5("d14") = "d0"
& f5("d13") = "d0"
& f5("d12") = "d0"
& f5("d11") = "d0"
& f5("d10") = "d0"
& f5("d9") = "d0"
& f5("d8") = "d0"
& f5("d7") = "d0"
& f5("d6") = "d13"
& f5("d5") = "d11"
& f5("d4") = "d9"
& f5("d3") = "d7"
& f5("d2") = "d0"
& f5("d1") = "d0"
& f5("d0") = "d0"
& f4("d62") = "d0"
& f4("d61") = "d0"
& f4("d60") = "d0"
& f4("d59") = "d0"
& f4("d58") = "d0"
& f4("d57") = "d0"
& f4("d56") = "d0"
& f4("d55") = "d0"
& f4("d54") = "d0"
& f4("d53") = "d0"
& f4("d52") = "d0"
& f4("d51") = "d0"
& f4("d50") = "d0"
& f4("d49") = "d0"
& f4("d48") = "d0"
& f4("d47") = "d0"
& f4("d46") = "d0"
& f4("d45") = "d0"
& f4("d44") = "d0"
& f4("d43") = "d0"
& f4("d42") = "d0"
& f4("d41") = "d0"
& f4("d40") = "d0"
& f4("d39") = "d0"
& f4("d38") = "d0"
& f4("d37") = "d0"
& f4("d36") = "d0"
& f4("d35") = "d0"
& f4("d34") = "d0"
& f4("d33") = "d0"
& f4("d32") = "d0"
& f4("d31") = "d0"
& f4("d30") = "d0"
& f4("d29") = "d0"
& f4("d28") = "d0"
& f4("d27") = "d0"
& f4("d26") = "d0"
& f4("d25") = "d0"
& f4("d24") = "d0"
& f4("d23") = "d0"
& f4("d22") = "d0"
& f4("d21") = "d0"
& f4("d20") = "d0"
& f4("d19") = "d0"
& f4("d18") = "d0"
& f4("d17") = "d0"
& f4("d16") = "d0"
& f4("d15") = "d0"
& f4("d14") = "d30"
& f4("d13") = "d28"
& f4("d12") = "d26"
& f4("d11") = "d24"
& f4("d10") = "d22"
& f4("d9") = "d20"
& f4("d8") = "d18"
& f4("d7") = "d16"
& f4("d6") = "d0"
& f4("d5") = "d0"
& f4("d4") = "d0"
& f4("d3") = "d0"
& f4("d2") = "d0"
& f4("d1") = "d0"
& f4("d0") = "d0"
& f3("d62") = "d0"
& f3("d61") = "d0"
& f3("d60") = "d0"
& f3("d59") = "d0"
& f3("d58") = "d0"
& f3("d57") = "d0"
& f3("d56") = "d0"
& f3("d55") = "d0"
& f3("d54") = "d0"
& f3("d53") = "d0"
& f3("d52") = "d0"
& f3("d51") = "d0"
& f3("d50") = "d0"
& f3("d49") = "d0"
& f3("d48") = "d0"
& f3("d47") = "d0"
& f3("d46") = "d0"
& f3("d45") = "d0"
& f3("d44") = "d0"
& f3("d43") = "d0"
& f3("d42") = "d0"
& f3("d41") = "d0"
& f3("d40") = "d0"
& f3("d39") = "d0"
& f3("d38") = "d0"
& f3("d37") = "d0"
& f3("d36") = "d0"
& f3("d35") = "d0"
& f3("d34") = "d0"
& f3("d33") = "d0"
& f3("d32") = "d0"
& f3("d31") = "d0"
& f3("d30") = "d0"
& f3("d29") = "d0"
& f3("d28") = "d0"
& f3("d27") = "d0"
& f3("d26") = "d0"
& f3("d25") = "d0"
& f3("d24") = "d0"
& f3("d23") = "d0"
& f3("d22") = "d0"
& f3("d21") = "d0"
& f3("d20") = "d0"
& f3("d19") = "d0"
& f3("d18") = "d0"
& f3("d17") = "d0"
& f3("d16") = "d0"
& f3("d15") = "d0"
& f3("d14") = "d29"
& f3("d13") = "d27"
& f3("d12") = "d25"
& f3("d11") = "d23"
& f3("d10") = "d21"
& f3("d9") = "d19"
& f3("d8") = "d17"
& f3("d7") = "d15"
& f3("d6") = "d0"
& f3("d5") = "d0"
& f3("d4") = "d0"
& f3("d3") = "d0"
& f3("d2") = "d0"
& f3("d1") = "d0"
& f3("d0") = "d0"
& f2("d62") = "d0"
& f2("d61") = "d0"
& f2("d60") = "d0"
& f2("d59") = "d0"
& f2("d58") = "d0"
& f2("d57") = "d0"
& f2("d56") = "d0"
& f2("d55") = "d0"
& f2("d54") = "d0"
& f2("d53") = "d0"
& f2("d52") = "d0"
& f2("d51") = "d0"
& f2("d50") = "d0"
& f2("d49") = "d0"
& f2("d48") = "d0"
& f2("d47") = "d0"
& f2("d46") = "d0"
& f2("d45") = "d0"
& f2("d44") = "d0"
& f2("d43") = "d0"
& f2("d42") = "d0"
& f2("d41") = "d0"
& f2("d40") = "d0"
& f2("d39") = "d0"
& f2("d38") = "d0"
& f2("d37") = "d0"
& f2("d36") = "d0"
& f2("d35") = "d0"
& f2("d34") = "d0"
& f2("d33") = "d0"
& f2("d32") = "d0"
& f2("d31") = "d0"
& f2("d30") = "d62"
& f2("d29") = "d60"
& f2("d28") = "d58"
& f2("d27") = "d56"
& f2("d26") = "d54"
& f2("d25") = "d52"
& f2("d24") = "d50"
& f2("d23") = "d48"
& f2("d22") = "d46"
& f2("d21") = "d44"
& f2("d20") = "d42"
& f2("d19") = "d40"
& f2("d18") = "d38"
& f2("d17") = "d36"
& f2("d16") = "d34"
& f2("d15") = "d32"
& f2("d14") = "d0"
& f2("d13") = "d0"
& f2("d12") = "d0"
& f2("d11") = "d0"
& f2("d10") = "d0"
& f2("d9") = "d0"
& f2("d8") = "d0"
& f2("d7") = "d0"
& f2("d6") = "d0"
& f2("d5") = "d0"
& f2("d4") = "d0"
& f2("d3") = "d0"
& f2("d2") = "d0"
& f2("d1") = "d0"
& f2("d0") = "d0"
& f1("d62") = "d0"
& f1("d61") = "d0"
& f1("d60") = "d0"
& f1("d59") = "d0"
& f1("d58") = "d0"
& f1("d57") = "d0"
& f1("d56") = "d0"
& f1("d55") = "d0"
& f1("d54") = "d0"
& f1("d53") = "d0"
& f1("d52") = "d0"
& f1("d51") = "d0"
& f1("d50") = "d0"
& f1("d49") = "d0"
& f1("d48") = "d0"
& f1("d47") = "d0"
& f1("d46") = "d0"
& f1("d45") = "d0"
& f1("d44") = "d0"
& f1("d43") = "d0"
& f1("d42") = "d0"
& f1("d41") = "d0"
& f1("d40") = "d0"
& f1("d39") = "d0"
& f1("d38") = "d0"
& f1("d37") = "d0"
& f1("d36") = "d0"
& f1("d35") = "d0"
& f1("d34") = "d0"
& f1("d33") = "d0"
& f1("d32") = "d0"
& f1("d31") = "d0"
& f1("d30") = "d61"
& f1("d29") = "d59"
& f1("d28") = "d57"
& f1("d27") = "d55"
& f1("d26") = "d53"
& f1("d25") = "d51"
& f1("d24") = "d49"
& f1("d23") = "d47"
& f1("d22") = "d45"
& f1("d21") = "d43"
& f1("d20") = "d41"
& f1("d19") = "d39"
& f1("d18") = "d37"
& f1("d17") = "d35"
& f1("d16") = "d33"
& f1("d15") = "d31"
& f1("d14") = "d0"
& f1("d13") = "d0"
& f1("d12") = "d0"
& f1("d11") = "d0"
& f1("d10") = "d0"
& f1("d9") = "d0"
& f1("d8") = "d0"
& f1("d7") = "d0"
& f1("d6") = "d0"
& f1("d5") = "d0"
& f1("d4") = "d0"
& f1("d3") = "d0"
& f1("d2") = "d0"
& f1("d1") = "d0"
& f1("d0") = "d0"
& c1 = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( r1("d62","d62")
& ~ r1("d62","d61")
& ~ r1("d62","d60")
& ~ r1("d62","d59")
& ~ r1("d62","d58")
& ~ r1("d62","d57")
& ~ r1("d62","d56")
& ~ r1("d62","d55")
& ~ r1("d62","d54")
& ~ r1("d62","d53")
& ~ r1("d62","d52")
& ~ r1("d62","d51")
& ~ r1("d62","d50")
& ~ r1("d62","d49")
& ~ r1("d62","d48")
& ~ r1("d62","d47")
& ~ r1("d62","d46")
& ~ r1("d62","d45")
& ~ r1("d62","d44")
& ~ r1("d62","d43")
& ~ r1("d62","d42")
& ~ r1("d62","d41")
& ~ r1("d62","d40")
& ~ r1("d62","d39")
& ~ r1("d62","d38")
& ~ r1("d62","d37")
& ~ r1("d62","d36")
& ~ r1("d62","d35")
& ~ r1("d62","d34")
& ~ r1("d62","d33")
& ~ r1("d62","d32")
& ~ r1("d62","d31")
& ~ r1("d62","d30")
& ~ r1("d62","d29")
& ~ r1("d62","d28")
& ~ r1("d62","d27")
& ~ r1("d62","d26")
& ~ r1("d62","d25")
& ~ r1("d62","d24")
& ~ r1("d62","d23")
& ~ r1("d62","d22")
& ~ r1("d62","d21")
& ~ r1("d62","d20")
& ~ r1("d62","d19")
& ~ r1("d62","d18")
& ~ r1("d62","d17")
& ~ r1("d62","d16")
& ~ r1("d62","d15")
& ~ r1("d62","d14")
& ~ r1("d62","d13")
& ~ r1("d62","d12")
& ~ r1("d62","d11")
& ~ r1("d62","d10")
& ~ r1("d62","d9")
& ~ r1("d62","d8")
& ~ r1("d62","d7")
& ~ r1("d62","d6")
& ~ r1("d62","d5")
& ~ r1("d62","d4")
& ~ r1("d62","d3")
& ~ r1("d62","d2")
& ~ r1("d62","d1")
& ~ r1("d62","d0")
& ~ r1("d61","d62")
& r1("d61","d61")
& ~ r1("d61","d60")
& ~ r1("d61","d59")
& ~ r1("d61","d58")
& ~ r1("d61","d57")
& ~ r1("d61","d56")
& ~ r1("d61","d55")
& ~ r1("d61","d54")
& ~ r1("d61","d53")
& ~ r1("d61","d52")
& ~ r1("d61","d51")
& ~ r1("d61","d50")
& ~ r1("d61","d49")
& ~ r1("d61","d48")
& ~ r1("d61","d47")
& ~ r1("d61","d46")
& ~ r1("d61","d45")
& ~ r1("d61","d44")
& ~ r1("d61","d43")
& ~ r1("d61","d42")
& ~ r1("d61","d41")
& ~ r1("d61","d40")
& ~ r1("d61","d39")
& ~ r1("d61","d38")
& ~ r1("d61","d37")
& ~ r1("d61","d36")
& ~ r1("d61","d35")
& ~ r1("d61","d34")
& ~ r1("d61","d33")
& ~ r1("d61","d32")
& ~ r1("d61","d31")
& ~ r1("d61","d30")
& ~ r1("d61","d29")
& ~ r1("d61","d28")
& ~ r1("d61","d27")
& ~ r1("d61","d26")
& ~ r1("d61","d25")
& ~ r1("d61","d24")
& ~ r1("d61","d23")
& ~ r1("d61","d22")
& ~ r1("d61","d21")
& ~ r1("d61","d20")
& ~ r1("d61","d19")
& ~ r1("d61","d18")
& ~ r1("d61","d17")
& ~ r1("d61","d16")
& ~ r1("d61","d15")
& ~ r1("d61","d14")
& ~ r1("d61","d13")
& ~ r1("d61","d12")
& ~ r1("d61","d11")
& ~ r1("d61","d10")
& ~ r1("d61","d9")
& ~ r1("d61","d8")
& ~ r1("d61","d7")
& ~ r1("d61","d6")
& ~ r1("d61","d5")
& ~ r1("d61","d4")
& ~ r1("d61","d3")
& ~ r1("d61","d2")
& ~ r1("d61","d1")
& ~ r1("d61","d0")
& ~ r1("d60","d62")
& ~ r1("d60","d61")
& r1("d60","d60")
& ~ r1("d60","d59")
& ~ r1("d60","d58")
& ~ r1("d60","d57")
& ~ r1("d60","d56")
& ~ r1("d60","d55")
& ~ r1("d60","d54")
& ~ r1("d60","d53")
& ~ r1("d60","d52")
& ~ r1("d60","d51")
& ~ r1("d60","d50")
& ~ r1("d60","d49")
& ~ r1("d60","d48")
& ~ r1("d60","d47")
& ~ r1("d60","d46")
& ~ r1("d60","d45")
& ~ r1("d60","d44")
& ~ r1("d60","d43")
& ~ r1("d60","d42")
& ~ r1("d60","d41")
& ~ r1("d60","d40")
& ~ r1("d60","d39")
& ~ r1("d60","d38")
& ~ r1("d60","d37")
& ~ r1("d60","d36")
& ~ r1("d60","d35")
& ~ r1("d60","d34")
& ~ r1("d60","d33")
& ~ r1("d60","d32")
& ~ r1("d60","d31")
& ~ r1("d60","d30")
& ~ r1("d60","d29")
& ~ r1("d60","d28")
& ~ r1("d60","d27")
& ~ r1("d60","d26")
& ~ r1("d60","d25")
& ~ r1("d60","d24")
& ~ r1("d60","d23")
& ~ r1("d60","d22")
& ~ r1("d60","d21")
& ~ r1("d60","d20")
& ~ r1("d60","d19")
& ~ r1("d60","d18")
& ~ r1("d60","d17")
& ~ r1("d60","d16")
& ~ r1("d60","d15")
& ~ r1("d60","d14")
& ~ r1("d60","d13")
& ~ r1("d60","d12")
& ~ r1("d60","d11")
& ~ r1("d60","d10")
& ~ r1("d60","d9")
& ~ r1("d60","d8")
& ~ r1("d60","d7")
& ~ r1("d60","d6")
& ~ r1("d60","d5")
& ~ r1("d60","d4")
& ~ r1("d60","d3")
& ~ r1("d60","d2")
& ~ r1("d60","d1")
& ~ r1("d60","d0")
& ~ r1("d59","d62")
& ~ r1("d59","d61")
& ~ r1("d59","d60")
& r1("d59","d59")
& ~ r1("d59","d58")
& ~ r1("d59","d57")
& ~ r1("d59","d56")
& ~ r1("d59","d55")
& ~ r1("d59","d54")
& ~ r1("d59","d53")
& ~ r1("d59","d52")
& ~ r1("d59","d51")
& ~ r1("d59","d50")
& ~ r1("d59","d49")
& ~ r1("d59","d48")
& ~ r1("d59","d47")
& ~ r1("d59","d46")
& ~ r1("d59","d45")
& ~ r1("d59","d44")
& ~ r1("d59","d43")
& ~ r1("d59","d42")
& ~ r1("d59","d41")
& ~ r1("d59","d40")
& ~ r1("d59","d39")
& ~ r1("d59","d38")
& ~ r1("d59","d37")
& ~ r1("d59","d36")
& ~ r1("d59","d35")
& ~ r1("d59","d34")
& ~ r1("d59","d33")
& ~ r1("d59","d32")
& ~ r1("d59","d31")
& ~ r1("d59","d30")
& ~ r1("d59","d29")
& ~ r1("d59","d28")
& ~ r1("d59","d27")
& ~ r1("d59","d26")
& ~ r1("d59","d25")
& ~ r1("d59","d24")
& ~ r1("d59","d23")
& ~ r1("d59","d22")
& ~ r1("d59","d21")
& ~ r1("d59","d20")
& ~ r1("d59","d19")
& ~ r1("d59","d18")
& ~ r1("d59","d17")
& ~ r1("d59","d16")
& ~ r1("d59","d15")
& ~ r1("d59","d14")
& ~ r1("d59","d13")
& ~ r1("d59","d12")
& ~ r1("d59","d11")
& ~ r1("d59","d10")
& ~ r1("d59","d9")
& ~ r1("d59","d8")
& ~ r1("d59","d7")
& ~ r1("d59","d6")
& ~ r1("d59","d5")
& ~ r1("d59","d4")
& ~ r1("d59","d3")
& ~ r1("d59","d2")
& ~ r1("d59","d1")
& ~ r1("d59","d0")
& ~ r1("d58","d62")
& ~ r1("d58","d61")
& ~ r1("d58","d60")
& ~ r1("d58","d59")
& r1("d58","d58")
& ~ r1("d58","d57")
& ~ r1("d58","d56")
& ~ r1("d58","d55")
& ~ r1("d58","d54")
& ~ r1("d58","d53")
& ~ r1("d58","d52")
& ~ r1("d58","d51")
& ~ r1("d58","d50")
& ~ r1("d58","d49")
& ~ r1("d58","d48")
& ~ r1("d58","d47")
& ~ r1("d58","d46")
& ~ r1("d58","d45")
& ~ r1("d58","d44")
& ~ r1("d58","d43")
& ~ r1("d58","d42")
& ~ r1("d58","d41")
& ~ r1("d58","d40")
& ~ r1("d58","d39")
& ~ r1("d58","d38")
& ~ r1("d58","d37")
& ~ r1("d58","d36")
& ~ r1("d58","d35")
& ~ r1("d58","d34")
& ~ r1("d58","d33")
& ~ r1("d58","d32")
& ~ r1("d58","d31")
& ~ r1("d58","d30")
& ~ r1("d58","d29")
& ~ r1("d58","d28")
& ~ r1("d58","d27")
& ~ r1("d58","d26")
& ~ r1("d58","d25")
& ~ r1("d58","d24")
& ~ r1("d58","d23")
& ~ r1("d58","d22")
& ~ r1("d58","d21")
& ~ r1("d58","d20")
& ~ r1("d58","d19")
& ~ r1("d58","d18")
& ~ r1("d58","d17")
& ~ r1("d58","d16")
& ~ r1("d58","d15")
& ~ r1("d58","d14")
& ~ r1("d58","d13")
& ~ r1("d58","d12")
& ~ r1("d58","d11")
& ~ r1("d58","d10")
& ~ r1("d58","d9")
& ~ r1("d58","d8")
& ~ r1("d58","d7")
& ~ r1("d58","d6")
& ~ r1("d58","d5")
& ~ r1("d58","d4")
& ~ r1("d58","d3")
& ~ r1("d58","d2")
& ~ r1("d58","d1")
& ~ r1("d58","d0")
& ~ r1("d57","d62")
& ~ r1("d57","d61")
& ~ r1("d57","d60")
& ~ r1("d57","d59")
& ~ r1("d57","d58")
& r1("d57","d57")
& ~ r1("d57","d56")
& ~ r1("d57","d55")
& ~ r1("d57","d54")
& ~ r1("d57","d53")
& ~ r1("d57","d52")
& ~ r1("d57","d51")
& ~ r1("d57","d50")
& ~ r1("d57","d49")
& ~ r1("d57","d48")
& ~ r1("d57","d47")
& ~ r1("d57","d46")
& ~ r1("d57","d45")
& ~ r1("d57","d44")
& ~ r1("d57","d43")
& ~ r1("d57","d42")
& ~ r1("d57","d41")
& ~ r1("d57","d40")
& ~ r1("d57","d39")
& ~ r1("d57","d38")
& ~ r1("d57","d37")
& ~ r1("d57","d36")
& ~ r1("d57","d35")
& ~ r1("d57","d34")
& ~ r1("d57","d33")
& ~ r1("d57","d32")
& ~ r1("d57","d31")
& ~ r1("d57","d30")
& ~ r1("d57","d29")
& ~ r1("d57","d28")
& ~ r1("d57","d27")
& ~ r1("d57","d26")
& ~ r1("d57","d25")
& ~ r1("d57","d24")
& ~ r1("d57","d23")
& ~ r1("d57","d22")
& ~ r1("d57","d21")
& ~ r1("d57","d20")
& ~ r1("d57","d19")
& ~ r1("d57","d18")
& ~ r1("d57","d17")
& ~ r1("d57","d16")
& ~ r1("d57","d15")
& ~ r1("d57","d14")
& ~ r1("d57","d13")
& ~ r1("d57","d12")
& ~ r1("d57","d11")
& ~ r1("d57","d10")
& ~ r1("d57","d9")
& ~ r1("d57","d8")
& ~ r1("d57","d7")
& ~ r1("d57","d6")
& ~ r1("d57","d5")
& ~ r1("d57","d4")
& ~ r1("d57","d3")
& ~ r1("d57","d2")
& ~ r1("d57","d1")
& ~ r1("d57","d0")
& ~ r1("d56","d62")
& ~ r1("d56","d61")
& ~ r1("d56","d60")
& ~ r1("d56","d59")
& ~ r1("d56","d58")
& ~ r1("d56","d57")
& r1("d56","d56")
& ~ r1("d56","d55")
& ~ r1("d56","d54")
& ~ r1("d56","d53")
& ~ r1("d56","d52")
& ~ r1("d56","d51")
& ~ r1("d56","d50")
& ~ r1("d56","d49")
& ~ r1("d56","d48")
& ~ r1("d56","d47")
& ~ r1("d56","d46")
& ~ r1("d56","d45")
& ~ r1("d56","d44")
& ~ r1("d56","d43")
& ~ r1("d56","d42")
& ~ r1("d56","d41")
& ~ r1("d56","d40")
& ~ r1("d56","d39")
& ~ r1("d56","d38")
& ~ r1("d56","d37")
& ~ r1("d56","d36")
& ~ r1("d56","d35")
& ~ r1("d56","d34")
& ~ r1("d56","d33")
& ~ r1("d56","d32")
& ~ r1("d56","d31")
& ~ r1("d56","d30")
& ~ r1("d56","d29")
& ~ r1("d56","d28")
& ~ r1("d56","d27")
& ~ r1("d56","d26")
& ~ r1("d56","d25")
& ~ r1("d56","d24")
& ~ r1("d56","d23")
& ~ r1("d56","d22")
& ~ r1("d56","d21")
& ~ r1("d56","d20")
& ~ r1("d56","d19")
& ~ r1("d56","d18")
& ~ r1("d56","d17")
& ~ r1("d56","d16")
& ~ r1("d56","d15")
& ~ r1("d56","d14")
& ~ r1("d56","d13")
& ~ r1("d56","d12")
& ~ r1("d56","d11")
& ~ r1("d56","d10")
& ~ r1("d56","d9")
& ~ r1("d56","d8")
& ~ r1("d56","d7")
& ~ r1("d56","d6")
& ~ r1("d56","d5")
& ~ r1("d56","d4")
& ~ r1("d56","d3")
& ~ r1("d56","d2")
& ~ r1("d56","d1")
& ~ r1("d56","d0")
& ~ r1("d55","d62")
& ~ r1("d55","d61")
& ~ r1("d55","d60")
& ~ r1("d55","d59")
& ~ r1("d55","d58")
& ~ r1("d55","d57")
& ~ r1("d55","d56")
& r1("d55","d55")
& ~ r1("d55","d54")
& ~ r1("d55","d53")
& ~ r1("d55","d52")
& ~ r1("d55","d51")
& ~ r1("d55","d50")
& ~ r1("d55","d49")
& ~ r1("d55","d48")
& ~ r1("d55","d47")
& ~ r1("d55","d46")
& ~ r1("d55","d45")
& ~ r1("d55","d44")
& ~ r1("d55","d43")
& ~ r1("d55","d42")
& ~ r1("d55","d41")
& ~ r1("d55","d40")
& ~ r1("d55","d39")
& ~ r1("d55","d38")
& ~ r1("d55","d37")
& ~ r1("d55","d36")
& ~ r1("d55","d35")
& ~ r1("d55","d34")
& ~ r1("d55","d33")
& ~ r1("d55","d32")
& ~ r1("d55","d31")
& ~ r1("d55","d30")
& ~ r1("d55","d29")
& ~ r1("d55","d28")
& ~ r1("d55","d27")
& ~ r1("d55","d26")
& ~ r1("d55","d25")
& ~ r1("d55","d24")
& ~ r1("d55","d23")
& ~ r1("d55","d22")
& ~ r1("d55","d21")
& ~ r1("d55","d20")
& ~ r1("d55","d19")
& ~ r1("d55","d18")
& ~ r1("d55","d17")
& ~ r1("d55","d16")
& ~ r1("d55","d15")
& ~ r1("d55","d14")
& ~ r1("d55","d13")
& ~ r1("d55","d12")
& ~ r1("d55","d11")
& ~ r1("d55","d10")
& ~ r1("d55","d9")
& ~ r1("d55","d8")
& ~ r1("d55","d7")
& ~ r1("d55","d6")
& ~ r1("d55","d5")
& ~ r1("d55","d4")
& ~ r1("d55","d3")
& ~ r1("d55","d2")
& ~ r1("d55","d1")
& ~ r1("d55","d0")
& ~ r1("d54","d62")
& ~ r1("d54","d61")
& ~ r1("d54","d60")
& ~ r1("d54","d59")
& ~ r1("d54","d58")
& ~ r1("d54","d57")
& ~ r1("d54","d56")
& ~ r1("d54","d55")
& r1("d54","d54")
& ~ r1("d54","d53")
& ~ r1("d54","d52")
& ~ r1("d54","d51")
& ~ r1("d54","d50")
& ~ r1("d54","d49")
& ~ r1("d54","d48")
& ~ r1("d54","d47")
& ~ r1("d54","d46")
& ~ r1("d54","d45")
& ~ r1("d54","d44")
& ~ r1("d54","d43")
& ~ r1("d54","d42")
& ~ r1("d54","d41")
& ~ r1("d54","d40")
& ~ r1("d54","d39")
& ~ r1("d54","d38")
& ~ r1("d54","d37")
& ~ r1("d54","d36")
& ~ r1("d54","d35")
& ~ r1("d54","d34")
& ~ r1("d54","d33")
& ~ r1("d54","d32")
& ~ r1("d54","d31")
& ~ r1("d54","d30")
& ~ r1("d54","d29")
& ~ r1("d54","d28")
& ~ r1("d54","d27")
& ~ r1("d54","d26")
& ~ r1("d54","d25")
& ~ r1("d54","d24")
& ~ r1("d54","d23")
& ~ r1("d54","d22")
& ~ r1("d54","d21")
& ~ r1("d54","d20")
& ~ r1("d54","d19")
& ~ r1("d54","d18")
& ~ r1("d54","d17")
& ~ r1("d54","d16")
& ~ r1("d54","d15")
& ~ r1("d54","d14")
& ~ r1("d54","d13")
& ~ r1("d54","d12")
& ~ r1("d54","d11")
& ~ r1("d54","d10")
& ~ r1("d54","d9")
& ~ r1("d54","d8")
& ~ r1("d54","d7")
& ~ r1("d54","d6")
& ~ r1("d54","d5")
& ~ r1("d54","d4")
& ~ r1("d54","d3")
& ~ r1("d54","d2")
& ~ r1("d54","d1")
& ~ r1("d54","d0")
& ~ r1("d53","d62")
& ~ r1("d53","d61")
& ~ r1("d53","d60")
& ~ r1("d53","d59")
& ~ r1("d53","d58")
& ~ r1("d53","d57")
& ~ r1("d53","d56")
& ~ r1("d53","d55")
& ~ r1("d53","d54")
& r1("d53","d53")
& ~ r1("d53","d52")
& ~ r1("d53","d51")
& ~ r1("d53","d50")
& ~ r1("d53","d49")
& ~ r1("d53","d48")
& ~ r1("d53","d47")
& ~ r1("d53","d46")
& ~ r1("d53","d45")
& ~ r1("d53","d44")
& ~ r1("d53","d43")
& ~ r1("d53","d42")
& ~ r1("d53","d41")
& ~ r1("d53","d40")
& ~ r1("d53","d39")
& ~ r1("d53","d38")
& ~ r1("d53","d37")
& ~ r1("d53","d36")
& ~ r1("d53","d35")
& ~ r1("d53","d34")
& ~ r1("d53","d33")
& ~ r1("d53","d32")
& ~ r1("d53","d31")
& ~ r1("d53","d30")
& ~ r1("d53","d29")
& ~ r1("d53","d28")
& ~ r1("d53","d27")
& ~ r1("d53","d26")
& ~ r1("d53","d25")
& ~ r1("d53","d24")
& ~ r1("d53","d23")
& ~ r1("d53","d22")
& ~ r1("d53","d21")
& ~ r1("d53","d20")
& ~ r1("d53","d19")
& ~ r1("d53","d18")
& ~ r1("d53","d17")
& ~ r1("d53","d16")
& ~ r1("d53","d15")
& ~ r1("d53","d14")
& ~ r1("d53","d13")
& ~ r1("d53","d12")
& ~ r1("d53","d11")
& ~ r1("d53","d10")
& ~ r1("d53","d9")
& ~ r1("d53","d8")
& ~ r1("d53","d7")
& ~ r1("d53","d6")
& ~ r1("d53","d5")
& ~ r1("d53","d4")
& ~ r1("d53","d3")
& ~ r1("d53","d2")
& ~ r1("d53","d1")
& ~ r1("d53","d0")
& ~ r1("d52","d62")
& ~ r1("d52","d61")
& ~ r1("d52","d60")
& ~ r1("d52","d59")
& ~ r1("d52","d58")
& ~ r1("d52","d57")
& ~ r1("d52","d56")
& ~ r1("d52","d55")
& ~ r1("d52","d54")
& ~ r1("d52","d53")
& r1("d52","d52")
& ~ r1("d52","d51")
& ~ r1("d52","d50")
& ~ r1("d52","d49")
& ~ r1("d52","d48")
& ~ r1("d52","d47")
& ~ r1("d52","d46")
& ~ r1("d52","d45")
& ~ r1("d52","d44")
& ~ r1("d52","d43")
& ~ r1("d52","d42")
& ~ r1("d52","d41")
& ~ r1("d52","d40")
& ~ r1("d52","d39")
& ~ r1("d52","d38")
& ~ r1("d52","d37")
& ~ r1("d52","d36")
& ~ r1("d52","d35")
& ~ r1("d52","d34")
& ~ r1("d52","d33")
& ~ r1("d52","d32")
& ~ r1("d52","d31")
& ~ r1("d52","d30")
& ~ r1("d52","d29")
& ~ r1("d52","d28")
& ~ r1("d52","d27")
& ~ r1("d52","d26")
& ~ r1("d52","d25")
& ~ r1("d52","d24")
& ~ r1("d52","d23")
& ~ r1("d52","d22")
& ~ r1("d52","d21")
& ~ r1("d52","d20")
& ~ r1("d52","d19")
& ~ r1("d52","d18")
& ~ r1("d52","d17")
& ~ r1("d52","d16")
& ~ r1("d52","d15")
& ~ r1("d52","d14")
& ~ r1("d52","d13")
& ~ r1("d52","d12")
& ~ r1("d52","d11")
& ~ r1("d52","d10")
& ~ r1("d52","d9")
& ~ r1("d52","d8")
& ~ r1("d52","d7")
& ~ r1("d52","d6")
& ~ r1("d52","d5")
& ~ r1("d52","d4")
& ~ r1("d52","d3")
& ~ r1("d52","d2")
& ~ r1("d52","d1")
& ~ r1("d52","d0")
& ~ r1("d51","d62")
& ~ r1("d51","d61")
& ~ r1("d51","d60")
& ~ r1("d51","d59")
& ~ r1("d51","d58")
& ~ r1("d51","d57")
& ~ r1("d51","d56")
& ~ r1("d51","d55")
& ~ r1("d51","d54")
& ~ r1("d51","d53")
& ~ r1("d51","d52")
& r1("d51","d51")
& ~ r1("d51","d50")
& ~ r1("d51","d49")
& ~ r1("d51","d48")
& ~ r1("d51","d47")
& ~ r1("d51","d46")
& ~ r1("d51","d45")
& ~ r1("d51","d44")
& ~ r1("d51","d43")
& ~ r1("d51","d42")
& ~ r1("d51","d41")
& ~ r1("d51","d40")
& ~ r1("d51","d39")
& ~ r1("d51","d38")
& ~ r1("d51","d37")
& ~ r1("d51","d36")
& ~ r1("d51","d35")
& ~ r1("d51","d34")
& ~ r1("d51","d33")
& ~ r1("d51","d32")
& ~ r1("d51","d31")
& ~ r1("d51","d30")
& ~ r1("d51","d29")
& ~ r1("d51","d28")
& ~ r1("d51","d27")
& ~ r1("d51","d26")
& ~ r1("d51","d25")
& ~ r1("d51","d24")
& ~ r1("d51","d23")
& ~ r1("d51","d22")
& ~ r1("d51","d21")
& ~ r1("d51","d20")
& ~ r1("d51","d19")
& ~ r1("d51","d18")
& ~ r1("d51","d17")
& ~ r1("d51","d16")
& ~ r1("d51","d15")
& ~ r1("d51","d14")
& ~ r1("d51","d13")
& ~ r1("d51","d12")
& ~ r1("d51","d11")
& ~ r1("d51","d10")
& ~ r1("d51","d9")
& ~ r1("d51","d8")
& ~ r1("d51","d7")
& ~ r1("d51","d6")
& ~ r1("d51","d5")
& ~ r1("d51","d4")
& ~ r1("d51","d3")
& ~ r1("d51","d2")
& ~ r1("d51","d1")
& ~ r1("d51","d0")
& ~ r1("d50","d62")
& ~ r1("d50","d61")
& ~ r1("d50","d60")
& ~ r1("d50","d59")
& ~ r1("d50","d58")
& ~ r1("d50","d57")
& ~ r1("d50","d56")
& ~ r1("d50","d55")
& ~ r1("d50","d54")
& ~ r1("d50","d53")
& ~ r1("d50","d52")
& ~ r1("d50","d51")
& r1("d50","d50")
& ~ r1("d50","d49")
& ~ r1("d50","d48")
& ~ r1("d50","d47")
& ~ r1("d50","d46")
& ~ r1("d50","d45")
& ~ r1("d50","d44")
& ~ r1("d50","d43")
& ~ r1("d50","d42")
& ~ r1("d50","d41")
& ~ r1("d50","d40")
& ~ r1("d50","d39")
& ~ r1("d50","d38")
& ~ r1("d50","d37")
& ~ r1("d50","d36")
& ~ r1("d50","d35")
& ~ r1("d50","d34")
& ~ r1("d50","d33")
& ~ r1("d50","d32")
& ~ r1("d50","d31")
& ~ r1("d50","d30")
& ~ r1("d50","d29")
& ~ r1("d50","d28")
& ~ r1("d50","d27")
& ~ r1("d50","d26")
& ~ r1("d50","d25")
& ~ r1("d50","d24")
& ~ r1("d50","d23")
& ~ r1("d50","d22")
& ~ r1("d50","d21")
& ~ r1("d50","d20")
& ~ r1("d50","d19")
& ~ r1("d50","d18")
& ~ r1("d50","d17")
& ~ r1("d50","d16")
& ~ r1("d50","d15")
& ~ r1("d50","d14")
& ~ r1("d50","d13")
& ~ r1("d50","d12")
& ~ r1("d50","d11")
& ~ r1("d50","d10")
& ~ r1("d50","d9")
& ~ r1("d50","d8")
& ~ r1("d50","d7")
& ~ r1("d50","d6")
& ~ r1("d50","d5")
& ~ r1("d50","d4")
& ~ r1("d50","d3")
& ~ r1("d50","d2")
& ~ r1("d50","d1")
& ~ r1("d50","d0")
& ~ r1("d49","d62")
& ~ r1("d49","d61")
& ~ r1("d49","d60")
& ~ r1("d49","d59")
& ~ r1("d49","d58")
& ~ r1("d49","d57")
& ~ r1("d49","d56")
& ~ r1("d49","d55")
& ~ r1("d49","d54")
& ~ r1("d49","d53")
& ~ r1("d49","d52")
& ~ r1("d49","d51")
& ~ r1("d49","d50")
& r1("d49","d49")
& ~ r1("d49","d48")
& ~ r1("d49","d47")
& ~ r1("d49","d46")
& ~ r1("d49","d45")
& ~ r1("d49","d44")
& ~ r1("d49","d43")
& ~ r1("d49","d42")
& ~ r1("d49","d41")
& ~ r1("d49","d40")
& ~ r1("d49","d39")
& ~ r1("d49","d38")
& ~ r1("d49","d37")
& ~ r1("d49","d36")
& ~ r1("d49","d35")
& ~ r1("d49","d34")
& ~ r1("d49","d33")
& ~ r1("d49","d32")
& ~ r1("d49","d31")
& ~ r1("d49","d30")
& ~ r1("d49","d29")
& ~ r1("d49","d28")
& ~ r1("d49","d27")
& ~ r1("d49","d26")
& ~ r1("d49","d25")
& ~ r1("d49","d24")
& ~ r1("d49","d23")
& ~ r1("d49","d22")
& ~ r1("d49","d21")
& ~ r1("d49","d20")
& ~ r1("d49","d19")
& ~ r1("d49","d18")
& ~ r1("d49","d17")
& ~ r1("d49","d16")
& ~ r1("d49","d15")
& ~ r1("d49","d14")
& ~ r1("d49","d13")
& ~ r1("d49","d12")
& ~ r1("d49","d11")
& ~ r1("d49","d10")
& ~ r1("d49","d9")
& ~ r1("d49","d8")
& ~ r1("d49","d7")
& ~ r1("d49","d6")
& ~ r1("d49","d5")
& ~ r1("d49","d4")
& ~ r1("d49","d3")
& ~ r1("d49","d2")
& ~ r1("d49","d1")
& ~ r1("d49","d0")
& ~ r1("d48","d62")
& ~ r1("d48","d61")
& ~ r1("d48","d60")
& ~ r1("d48","d59")
& ~ r1("d48","d58")
& ~ r1("d48","d57")
& ~ r1("d48","d56")
& ~ r1("d48","d55")
& ~ r1("d48","d54")
& ~ r1("d48","d53")
& ~ r1("d48","d52")
& ~ r1("d48","d51")
& ~ r1("d48","d50")
& ~ r1("d48","d49")
& r1("d48","d48")
& ~ r1("d48","d47")
& ~ r1("d48","d46")
& ~ r1("d48","d45")
& ~ r1("d48","d44")
& ~ r1("d48","d43")
& ~ r1("d48","d42")
& ~ r1("d48","d41")
& ~ r1("d48","d40")
& ~ r1("d48","d39")
& ~ r1("d48","d38")
& ~ r1("d48","d37")
& ~ r1("d48","d36")
& ~ r1("d48","d35")
& ~ r1("d48","d34")
& ~ r1("d48","d33")
& ~ r1("d48","d32")
& ~ r1("d48","d31")
& ~ r1("d48","d30")
& ~ r1("d48","d29")
& ~ r1("d48","d28")
& ~ r1("d48","d27")
& ~ r1("d48","d26")
& ~ r1("d48","d25")
& ~ r1("d48","d24")
& ~ r1("d48","d23")
& ~ r1("d48","d22")
& ~ r1("d48","d21")
& ~ r1("d48","d20")
& ~ r1("d48","d19")
& ~ r1("d48","d18")
& ~ r1("d48","d17")
& ~ r1("d48","d16")
& ~ r1("d48","d15")
& ~ r1("d48","d14")
& ~ r1("d48","d13")
& ~ r1("d48","d12")
& ~ r1("d48","d11")
& ~ r1("d48","d10")
& ~ r1("d48","d9")
& ~ r1("d48","d8")
& ~ r1("d48","d7")
& ~ r1("d48","d6")
& ~ r1("d48","d5")
& ~ r1("d48","d4")
& ~ r1("d48","d3")
& ~ r1("d48","d2")
& ~ r1("d48","d1")
& ~ r1("d48","d0")
& ~ r1("d47","d62")
& ~ r1("d47","d61")
& ~ r1("d47","d60")
& ~ r1("d47","d59")
& ~ r1("d47","d58")
& ~ r1("d47","d57")
& ~ r1("d47","d56")
& ~ r1("d47","d55")
& ~ r1("d47","d54")
& ~ r1("d47","d53")
& ~ r1("d47","d52")
& ~ r1("d47","d51")
& ~ r1("d47","d50")
& ~ r1("d47","d49")
& ~ r1("d47","d48")
& r1("d47","d47")
& ~ r1("d47","d46")
& ~ r1("d47","d45")
& ~ r1("d47","d44")
& ~ r1("d47","d43")
& ~ r1("d47","d42")
& ~ r1("d47","d41")
& ~ r1("d47","d40")
& ~ r1("d47","d39")
& ~ r1("d47","d38")
& ~ r1("d47","d37")
& ~ r1("d47","d36")
& ~ r1("d47","d35")
& ~ r1("d47","d34")
& ~ r1("d47","d33")
& ~ r1("d47","d32")
& ~ r1("d47","d31")
& ~ r1("d47","d30")
& ~ r1("d47","d29")
& ~ r1("d47","d28")
& ~ r1("d47","d27")
& ~ r1("d47","d26")
& ~ r1("d47","d25")
& ~ r1("d47","d24")
& ~ r1("d47","d23")
& ~ r1("d47","d22")
& ~ r1("d47","d21")
& ~ r1("d47","d20")
& ~ r1("d47","d19")
& ~ r1("d47","d18")
& ~ r1("d47","d17")
& ~ r1("d47","d16")
& ~ r1("d47","d15")
& ~ r1("d47","d14")
& ~ r1("d47","d13")
& ~ r1("d47","d12")
& ~ r1("d47","d11")
& ~ r1("d47","d10")
& ~ r1("d47","d9")
& ~ r1("d47","d8")
& ~ r1("d47","d7")
& ~ r1("d47","d6")
& ~ r1("d47","d5")
& ~ r1("d47","d4")
& ~ r1("d47","d3")
& ~ r1("d47","d2")
& ~ r1("d47","d1")
& ~ r1("d47","d0")
& ~ r1("d46","d62")
& ~ r1("d46","d61")
& ~ r1("d46","d60")
& ~ r1("d46","d59")
& ~ r1("d46","d58")
& ~ r1("d46","d57")
& ~ r1("d46","d56")
& ~ r1("d46","d55")
& ~ r1("d46","d54")
& ~ r1("d46","d53")
& ~ r1("d46","d52")
& ~ r1("d46","d51")
& ~ r1("d46","d50")
& ~ r1("d46","d49")
& ~ r1("d46","d48")
& ~ r1("d46","d47")
& r1("d46","d46")
& ~ r1("d46","d45")
& ~ r1("d46","d44")
& ~ r1("d46","d43")
& ~ r1("d46","d42")
& ~ r1("d46","d41")
& ~ r1("d46","d40")
& ~ r1("d46","d39")
& ~ r1("d46","d38")
& ~ r1("d46","d37")
& ~ r1("d46","d36")
& ~ r1("d46","d35")
& ~ r1("d46","d34")
& ~ r1("d46","d33")
& ~ r1("d46","d32")
& ~ r1("d46","d31")
& ~ r1("d46","d30")
& ~ r1("d46","d29")
& ~ r1("d46","d28")
& ~ r1("d46","d27")
& ~ r1("d46","d26")
& ~ r1("d46","d25")
& ~ r1("d46","d24")
& ~ r1("d46","d23")
& ~ r1("d46","d22")
& ~ r1("d46","d21")
& ~ r1("d46","d20")
& ~ r1("d46","d19")
& ~ r1("d46","d18")
& ~ r1("d46","d17")
& ~ r1("d46","d16")
& ~ r1("d46","d15")
& ~ r1("d46","d14")
& ~ r1("d46","d13")
& ~ r1("d46","d12")
& ~ r1("d46","d11")
& ~ r1("d46","d10")
& ~ r1("d46","d9")
& ~ r1("d46","d8")
& ~ r1("d46","d7")
& ~ r1("d46","d6")
& ~ r1("d46","d5")
& ~ r1("d46","d4")
& ~ r1("d46","d3")
& ~ r1("d46","d2")
& ~ r1("d46","d1")
& ~ r1("d46","d0")
& ~ r1("d45","d62")
& ~ r1("d45","d61")
& ~ r1("d45","d60")
& ~ r1("d45","d59")
& ~ r1("d45","d58")
& ~ r1("d45","d57")
& ~ r1("d45","d56")
& ~ r1("d45","d55")
& ~ r1("d45","d54")
& ~ r1("d45","d53")
& ~ r1("d45","d52")
& ~ r1("d45","d51")
& ~ r1("d45","d50")
& ~ r1("d45","d49")
& ~ r1("d45","d48")
& ~ r1("d45","d47")
& ~ r1("d45","d46")
& r1("d45","d45")
& ~ r1("d45","d44")
& ~ r1("d45","d43")
& ~ r1("d45","d42")
& ~ r1("d45","d41")
& ~ r1("d45","d40")
& ~ r1("d45","d39")
& ~ r1("d45","d38")
& ~ r1("d45","d37")
& ~ r1("d45","d36")
& ~ r1("d45","d35")
& ~ r1("d45","d34")
& ~ r1("d45","d33")
& ~ r1("d45","d32")
& ~ r1("d45","d31")
& ~ r1("d45","d30")
& ~ r1("d45","d29")
& ~ r1("d45","d28")
& ~ r1("d45","d27")
& ~ r1("d45","d26")
& ~ r1("d45","d25")
& ~ r1("d45","d24")
& ~ r1("d45","d23")
& ~ r1("d45","d22")
& ~ r1("d45","d21")
& ~ r1("d45","d20")
& ~ r1("d45","d19")
& ~ r1("d45","d18")
& ~ r1("d45","d17")
& ~ r1("d45","d16")
& ~ r1("d45","d15")
& ~ r1("d45","d14")
& ~ r1("d45","d13")
& ~ r1("d45","d12")
& ~ r1("d45","d11")
& ~ r1("d45","d10")
& ~ r1("d45","d9")
& ~ r1("d45","d8")
& ~ r1("d45","d7")
& ~ r1("d45","d6")
& ~ r1("d45","d5")
& ~ r1("d45","d4")
& ~ r1("d45","d3")
& ~ r1("d45","d2")
& ~ r1("d45","d1")
& ~ r1("d45","d0")
& ~ r1("d44","d62")
& ~ r1("d44","d61")
& ~ r1("d44","d60")
& ~ r1("d44","d59")
& ~ r1("d44","d58")
& ~ r1("d44","d57")
& ~ r1("d44","d56")
& ~ r1("d44","d55")
& ~ r1("d44","d54")
& ~ r1("d44","d53")
& ~ r1("d44","d52")
& ~ r1("d44","d51")
& ~ r1("d44","d50")
& ~ r1("d44","d49")
& ~ r1("d44","d48")
& ~ r1("d44","d47")
& ~ r1("d44","d46")
& ~ r1("d44","d45")
& r1("d44","d44")
& ~ r1("d44","d43")
& ~ r1("d44","d42")
& ~ r1("d44","d41")
& ~ r1("d44","d40")
& ~ r1("d44","d39")
& ~ r1("d44","d38")
& ~ r1("d44","d37")
& ~ r1("d44","d36")
& ~ r1("d44","d35")
& ~ r1("d44","d34")
& ~ r1("d44","d33")
& ~ r1("d44","d32")
& ~ r1("d44","d31")
& ~ r1("d44","d30")
& ~ r1("d44","d29")
& ~ r1("d44","d28")
& ~ r1("d44","d27")
& ~ r1("d44","d26")
& ~ r1("d44","d25")
& ~ r1("d44","d24")
& ~ r1("d44","d23")
& ~ r1("d44","d22")
& ~ r1("d44","d21")
& ~ r1("d44","d20")
& ~ r1("d44","d19")
& ~ r1("d44","d18")
& ~ r1("d44","d17")
& ~ r1("d44","d16")
& ~ r1("d44","d15")
& ~ r1("d44","d14")
& ~ r1("d44","d13")
& ~ r1("d44","d12")
& ~ r1("d44","d11")
& ~ r1("d44","d10")
& ~ r1("d44","d9")
& ~ r1("d44","d8")
& ~ r1("d44","d7")
& ~ r1("d44","d6")
& ~ r1("d44","d5")
& ~ r1("d44","d4")
& ~ r1("d44","d3")
& ~ r1("d44","d2")
& ~ r1("d44","d1")
& ~ r1("d44","d0")
& ~ r1("d43","d62")
& ~ r1("d43","d61")
& ~ r1("d43","d60")
& ~ r1("d43","d59")
& ~ r1("d43","d58")
& ~ r1("d43","d57")
& ~ r1("d43","d56")
& ~ r1("d43","d55")
& ~ r1("d43","d54")
& ~ r1("d43","d53")
& ~ r1("d43","d52")
& ~ r1("d43","d51")
& ~ r1("d43","d50")
& ~ r1("d43","d49")
& ~ r1("d43","d48")
& ~ r1("d43","d47")
& ~ r1("d43","d46")
& ~ r1("d43","d45")
& ~ r1("d43","d44")
& r1("d43","d43")
& ~ r1("d43","d42")
& ~ r1("d43","d41")
& ~ r1("d43","d40")
& ~ r1("d43","d39")
& ~ r1("d43","d38")
& ~ r1("d43","d37")
& ~ r1("d43","d36")
& ~ r1("d43","d35")
& ~ r1("d43","d34")
& ~ r1("d43","d33")
& ~ r1("d43","d32")
& ~ r1("d43","d31")
& ~ r1("d43","d30")
& ~ r1("d43","d29")
& ~ r1("d43","d28")
& ~ r1("d43","d27")
& ~ r1("d43","d26")
& ~ r1("d43","d25")
& ~ r1("d43","d24")
& ~ r1("d43","d23")
& ~ r1("d43","d22")
& ~ r1("d43","d21")
& ~ r1("d43","d20")
& ~ r1("d43","d19")
& ~ r1("d43","d18")
& ~ r1("d43","d17")
& ~ r1("d43","d16")
& ~ r1("d43","d15")
& ~ r1("d43","d14")
& ~ r1("d43","d13")
& ~ r1("d43","d12")
& ~ r1("d43","d11")
& ~ r1("d43","d10")
& ~ r1("d43","d9")
& ~ r1("d43","d8")
& ~ r1("d43","d7")
& ~ r1("d43","d6")
& ~ r1("d43","d5")
& ~ r1("d43","d4")
& ~ r1("d43","d3")
& ~ r1("d43","d2")
& ~ r1("d43","d1")
& ~ r1("d43","d0")
& ~ r1("d42","d62")
& ~ r1("d42","d61")
& ~ r1("d42","d60")
& ~ r1("d42","d59")
& ~ r1("d42","d58")
& ~ r1("d42","d57")
& ~ r1("d42","d56")
& ~ r1("d42","d55")
& ~ r1("d42","d54")
& ~ r1("d42","d53")
& ~ r1("d42","d52")
& ~ r1("d42","d51")
& ~ r1("d42","d50")
& ~ r1("d42","d49")
& ~ r1("d42","d48")
& ~ r1("d42","d47")
& ~ r1("d42","d46")
& ~ r1("d42","d45")
& ~ r1("d42","d44")
& ~ r1("d42","d43")
& r1("d42","d42")
& ~ r1("d42","d41")
& ~ r1("d42","d40")
& ~ r1("d42","d39")
& ~ r1("d42","d38")
& ~ r1("d42","d37")
& ~ r1("d42","d36")
& ~ r1("d42","d35")
& ~ r1("d42","d34")
& ~ r1("d42","d33")
& ~ r1("d42","d32")
& ~ r1("d42","d31")
& ~ r1("d42","d30")
& ~ r1("d42","d29")
& ~ r1("d42","d28")
& ~ r1("d42","d27")
& ~ r1("d42","d26")
& ~ r1("d42","d25")
& ~ r1("d42","d24")
& ~ r1("d42","d23")
& ~ r1("d42","d22")
& ~ r1("d42","d21")
& ~ r1("d42","d20")
& ~ r1("d42","d19")
& ~ r1("d42","d18")
& ~ r1("d42","d17")
& ~ r1("d42","d16")
& ~ r1("d42","d15")
& ~ r1("d42","d14")
& ~ r1("d42","d13")
& ~ r1("d42","d12")
& ~ r1("d42","d11")
& ~ r1("d42","d10")
& ~ r1("d42","d9")
& ~ r1("d42","d8")
& ~ r1("d42","d7")
& ~ r1("d42","d6")
& ~ r1("d42","d5")
& ~ r1("d42","d4")
& ~ r1("d42","d3")
& ~ r1("d42","d2")
& ~ r1("d42","d1")
& ~ r1("d42","d0")
& ~ r1("d41","d62")
& ~ r1("d41","d61")
& ~ r1("d41","d60")
& ~ r1("d41","d59")
& ~ r1("d41","d58")
& ~ r1("d41","d57")
& ~ r1("d41","d56")
& ~ r1("d41","d55")
& ~ r1("d41","d54")
& ~ r1("d41","d53")
& ~ r1("d41","d52")
& ~ r1("d41","d51")
& ~ r1("d41","d50")
& ~ r1("d41","d49")
& ~ r1("d41","d48")
& ~ r1("d41","d47")
& ~ r1("d41","d46")
& ~ r1("d41","d45")
& ~ r1("d41","d44")
& ~ r1("d41","d43")
& ~ r1("d41","d42")
& r1("d41","d41")
& ~ r1("d41","d40")
& ~ r1("d41","d39")
& ~ r1("d41","d38")
& ~ r1("d41","d37")
& ~ r1("d41","d36")
& ~ r1("d41","d35")
& ~ r1("d41","d34")
& ~ r1("d41","d33")
& ~ r1("d41","d32")
& ~ r1("d41","d31")
& ~ r1("d41","d30")
& ~ r1("d41","d29")
& ~ r1("d41","d28")
& ~ r1("d41","d27")
& ~ r1("d41","d26")
& ~ r1("d41","d25")
& ~ r1("d41","d24")
& ~ r1("d41","d23")
& ~ r1("d41","d22")
& ~ r1("d41","d21")
& ~ r1("d41","d20")
& ~ r1("d41","d19")
& ~ r1("d41","d18")
& ~ r1("d41","d17")
& ~ r1("d41","d16")
& ~ r1("d41","d15")
& ~ r1("d41","d14")
& ~ r1("d41","d13")
& ~ r1("d41","d12")
& ~ r1("d41","d11")
& ~ r1("d41","d10")
& ~ r1("d41","d9")
& ~ r1("d41","d8")
& ~ r1("d41","d7")
& ~ r1("d41","d6")
& ~ r1("d41","d5")
& ~ r1("d41","d4")
& ~ r1("d41","d3")
& ~ r1("d41","d2")
& ~ r1("d41","d1")
& ~ r1("d41","d0")
& ~ r1("d40","d62")
& ~ r1("d40","d61")
& ~ r1("d40","d60")
& ~ r1("d40","d59")
& ~ r1("d40","d58")
& ~ r1("d40","d57")
& ~ r1("d40","d56")
& ~ r1("d40","d55")
& ~ r1("d40","d54")
& ~ r1("d40","d53")
& ~ r1("d40","d52")
& ~ r1("d40","d51")
& ~ r1("d40","d50")
& ~ r1("d40","d49")
& ~ r1("d40","d48")
& ~ r1("d40","d47")
& ~ r1("d40","d46")
& ~ r1("d40","d45")
& ~ r1("d40","d44")
& ~ r1("d40","d43")
& ~ r1("d40","d42")
& ~ r1("d40","d41")
& r1("d40","d40")
& ~ r1("d40","d39")
& ~ r1("d40","d38")
& ~ r1("d40","d37")
& ~ r1("d40","d36")
& ~ r1("d40","d35")
& ~ r1("d40","d34")
& ~ r1("d40","d33")
& ~ r1("d40","d32")
& ~ r1("d40","d31")
& ~ r1("d40","d30")
& ~ r1("d40","d29")
& ~ r1("d40","d28")
& ~ r1("d40","d27")
& ~ r1("d40","d26")
& ~ r1("d40","d25")
& ~ r1("d40","d24")
& ~ r1("d40","d23")
& ~ r1("d40","d22")
& ~ r1("d40","d21")
& ~ r1("d40","d20")
& ~ r1("d40","d19")
& ~ r1("d40","d18")
& ~ r1("d40","d17")
& ~ r1("d40","d16")
& ~ r1("d40","d15")
& ~ r1("d40","d14")
& ~ r1("d40","d13")
& ~ r1("d40","d12")
& ~ r1("d40","d11")
& ~ r1("d40","d10")
& ~ r1("d40","d9")
& ~ r1("d40","d8")
& ~ r1("d40","d7")
& ~ r1("d40","d6")
& ~ r1("d40","d5")
& ~ r1("d40","d4")
& ~ r1("d40","d3")
& ~ r1("d40","d2")
& ~ r1("d40","d1")
& ~ r1("d40","d0")
& ~ r1("d39","d62")
& ~ r1("d39","d61")
& ~ r1("d39","d60")
& ~ r1("d39","d59")
& ~ r1("d39","d58")
& ~ r1("d39","d57")
& ~ r1("d39","d56")
& ~ r1("d39","d55")
& ~ r1("d39","d54")
& ~ r1("d39","d53")
& ~ r1("d39","d52")
& ~ r1("d39","d51")
& ~ r1("d39","d50")
& ~ r1("d39","d49")
& ~ r1("d39","d48")
& ~ r1("d39","d47")
& ~ r1("d39","d46")
& ~ r1("d39","d45")
& ~ r1("d39","d44")
& ~ r1("d39","d43")
& ~ r1("d39","d42")
& ~ r1("d39","d41")
& ~ r1("d39","d40")
& r1("d39","d39")
& ~ r1("d39","d38")
& ~ r1("d39","d37")
& ~ r1("d39","d36")
& ~ r1("d39","d35")
& ~ r1("d39","d34")
& ~ r1("d39","d33")
& ~ r1("d39","d32")
& ~ r1("d39","d31")
& ~ r1("d39","d30")
& ~ r1("d39","d29")
& ~ r1("d39","d28")
& ~ r1("d39","d27")
& ~ r1("d39","d26")
& ~ r1("d39","d25")
& ~ r1("d39","d24")
& ~ r1("d39","d23")
& ~ r1("d39","d22")
& ~ r1("d39","d21")
& ~ r1("d39","d20")
& ~ r1("d39","d19")
& ~ r1("d39","d18")
& ~ r1("d39","d17")
& ~ r1("d39","d16")
& ~ r1("d39","d15")
& ~ r1("d39","d14")
& ~ r1("d39","d13")
& ~ r1("d39","d12")
& ~ r1("d39","d11")
& ~ r1("d39","d10")
& ~ r1("d39","d9")
& ~ r1("d39","d8")
& ~ r1("d39","d7")
& ~ r1("d39","d6")
& ~ r1("d39","d5")
& ~ r1("d39","d4")
& ~ r1("d39","d3")
& ~ r1("d39","d2")
& ~ r1("d39","d1")
& ~ r1("d39","d0")
& ~ r1("d38","d62")
& ~ r1("d38","d61")
& ~ r1("d38","d60")
& ~ r1("d38","d59")
& ~ r1("d38","d58")
& ~ r1("d38","d57")
& ~ r1("d38","d56")
& ~ r1("d38","d55")
& ~ r1("d38","d54")
& ~ r1("d38","d53")
& ~ r1("d38","d52")
& ~ r1("d38","d51")
& ~ r1("d38","d50")
& ~ r1("d38","d49")
& ~ r1("d38","d48")
& ~ r1("d38","d47")
& ~ r1("d38","d46")
& ~ r1("d38","d45")
& ~ r1("d38","d44")
& ~ r1("d38","d43")
& ~ r1("d38","d42")
& ~ r1("d38","d41")
& ~ r1("d38","d40")
& ~ r1("d38","d39")
& r1("d38","d38")
& ~ r1("d38","d37")
& ~ r1("d38","d36")
& ~ r1("d38","d35")
& ~ r1("d38","d34")
& ~ r1("d38","d33")
& ~ r1("d38","d32")
& ~ r1("d38","d31")
& ~ r1("d38","d30")
& ~ r1("d38","d29")
& ~ r1("d38","d28")
& ~ r1("d38","d27")
& ~ r1("d38","d26")
& ~ r1("d38","d25")
& ~ r1("d38","d24")
& ~ r1("d38","d23")
& ~ r1("d38","d22")
& ~ r1("d38","d21")
& ~ r1("d38","d20")
& ~ r1("d38","d19")
& ~ r1("d38","d18")
& ~ r1("d38","d17")
& ~ r1("d38","d16")
& ~ r1("d38","d15")
& ~ r1("d38","d14")
& ~ r1("d38","d13")
& ~ r1("d38","d12")
& ~ r1("d38","d11")
& ~ r1("d38","d10")
& ~ r1("d38","d9")
& ~ r1("d38","d8")
& ~ r1("d38","d7")
& ~ r1("d38","d6")
& ~ r1("d38","d5")
& ~ r1("d38","d4")
& ~ r1("d38","d3")
& ~ r1("d38","d2")
& ~ r1("d38","d1")
& ~ r1("d38","d0")
& ~ r1("d37","d62")
& ~ r1("d37","d61")
& ~ r1("d37","d60")
& ~ r1("d37","d59")
& ~ r1("d37","d58")
& ~ r1("d37","d57")
& ~ r1("d37","d56")
& ~ r1("d37","d55")
& ~ r1("d37","d54")
& ~ r1("d37","d53")
& ~ r1("d37","d52")
& ~ r1("d37","d51")
& ~ r1("d37","d50")
& ~ r1("d37","d49")
& ~ r1("d37","d48")
& ~ r1("d37","d47")
& ~ r1("d37","d46")
& ~ r1("d37","d45")
& ~ r1("d37","d44")
& ~ r1("d37","d43")
& ~ r1("d37","d42")
& ~ r1("d37","d41")
& ~ r1("d37","d40")
& ~ r1("d37","d39")
& ~ r1("d37","d38")
& r1("d37","d37")
& ~ r1("d37","d36")
& ~ r1("d37","d35")
& ~ r1("d37","d34")
& ~ r1("d37","d33")
& ~ r1("d37","d32")
& ~ r1("d37","d31")
& ~ r1("d37","d30")
& ~ r1("d37","d29")
& ~ r1("d37","d28")
& ~ r1("d37","d27")
& ~ r1("d37","d26")
& ~ r1("d37","d25")
& ~ r1("d37","d24")
& ~ r1("d37","d23")
& ~ r1("d37","d22")
& ~ r1("d37","d21")
& ~ r1("d37","d20")
& ~ r1("d37","d19")
& ~ r1("d37","d18")
& ~ r1("d37","d17")
& ~ r1("d37","d16")
& ~ r1("d37","d15")
& ~ r1("d37","d14")
& ~ r1("d37","d13")
& ~ r1("d37","d12")
& ~ r1("d37","d11")
& ~ r1("d37","d10")
& ~ r1("d37","d9")
& ~ r1("d37","d8")
& ~ r1("d37","d7")
& ~ r1("d37","d6")
& ~ r1("d37","d5")
& ~ r1("d37","d4")
& ~ r1("d37","d3")
& ~ r1("d37","d2")
& ~ r1("d37","d1")
& ~ r1("d37","d0")
& ~ r1("d36","d62")
& ~ r1("d36","d61")
& ~ r1("d36","d60")
& ~ r1("d36","d59")
& ~ r1("d36","d58")
& ~ r1("d36","d57")
& ~ r1("d36","d56")
& ~ r1("d36","d55")
& ~ r1("d36","d54")
& ~ r1("d36","d53")
& ~ r1("d36","d52")
& ~ r1("d36","d51")
& ~ r1("d36","d50")
& ~ r1("d36","d49")
& ~ r1("d36","d48")
& ~ r1("d36","d47")
& ~ r1("d36","d46")
& ~ r1("d36","d45")
& ~ r1("d36","d44")
& ~ r1("d36","d43")
& ~ r1("d36","d42")
& ~ r1("d36","d41")
& ~ r1("d36","d40")
& ~ r1("d36","d39")
& ~ r1("d36","d38")
& ~ r1("d36","d37")
& r1("d36","d36")
& ~ r1("d36","d35")
& ~ r1("d36","d34")
& ~ r1("d36","d33")
& ~ r1("d36","d32")
& ~ r1("d36","d31")
& ~ r1("d36","d30")
& ~ r1("d36","d29")
& ~ r1("d36","d28")
& ~ r1("d36","d27")
& ~ r1("d36","d26")
& ~ r1("d36","d25")
& ~ r1("d36","d24")
& ~ r1("d36","d23")
& ~ r1("d36","d22")
& ~ r1("d36","d21")
& ~ r1("d36","d20")
& ~ r1("d36","d19")
& ~ r1("d36","d18")
& ~ r1("d36","d17")
& ~ r1("d36","d16")
& ~ r1("d36","d15")
& ~ r1("d36","d14")
& ~ r1("d36","d13")
& ~ r1("d36","d12")
& ~ r1("d36","d11")
& ~ r1("d36","d10")
& ~ r1("d36","d9")
& ~ r1("d36","d8")
& ~ r1("d36","d7")
& ~ r1("d36","d6")
& ~ r1("d36","d5")
& ~ r1("d36","d4")
& ~ r1("d36","d3")
& ~ r1("d36","d2")
& ~ r1("d36","d1")
& ~ r1("d36","d0")
& ~ r1("d35","d62")
& ~ r1("d35","d61")
& ~ r1("d35","d60")
& ~ r1("d35","d59")
& ~ r1("d35","d58")
& ~ r1("d35","d57")
& ~ r1("d35","d56")
& ~ r1("d35","d55")
& ~ r1("d35","d54")
& ~ r1("d35","d53")
& ~ r1("d35","d52")
& ~ r1("d35","d51")
& ~ r1("d35","d50")
& ~ r1("d35","d49")
& ~ r1("d35","d48")
& ~ r1("d35","d47")
& ~ r1("d35","d46")
& ~ r1("d35","d45")
& ~ r1("d35","d44")
& ~ r1("d35","d43")
& ~ r1("d35","d42")
& ~ r1("d35","d41")
& ~ r1("d35","d40")
& ~ r1("d35","d39")
& ~ r1("d35","d38")
& ~ r1("d35","d37")
& ~ r1("d35","d36")
& r1("d35","d35")
& ~ r1("d35","d34")
& ~ r1("d35","d33")
& ~ r1("d35","d32")
& ~ r1("d35","d31")
& ~ r1("d35","d30")
& ~ r1("d35","d29")
& ~ r1("d35","d28")
& ~ r1("d35","d27")
& ~ r1("d35","d26")
& ~ r1("d35","d25")
& ~ r1("d35","d24")
& ~ r1("d35","d23")
& ~ r1("d35","d22")
& ~ r1("d35","d21")
& ~ r1("d35","d20")
& ~ r1("d35","d19")
& ~ r1("d35","d18")
& ~ r1("d35","d17")
& ~ r1("d35","d16")
& ~ r1("d35","d15")
& ~ r1("d35","d14")
& ~ r1("d35","d13")
& ~ r1("d35","d12")
& ~ r1("d35","d11")
& ~ r1("d35","d10")
& ~ r1("d35","d9")
& ~ r1("d35","d8")
& ~ r1("d35","d7")
& ~ r1("d35","d6")
& ~ r1("d35","d5")
& ~ r1("d35","d4")
& ~ r1("d35","d3")
& ~ r1("d35","d2")
& ~ r1("d35","d1")
& ~ r1("d35","d0")
& ~ r1("d34","d62")
& ~ r1("d34","d61")
& ~ r1("d34","d60")
& ~ r1("d34","d59")
& ~ r1("d34","d58")
& ~ r1("d34","d57")
& ~ r1("d34","d56")
& ~ r1("d34","d55")
& ~ r1("d34","d54")
& ~ r1("d34","d53")
& ~ r1("d34","d52")
& ~ r1("d34","d51")
& ~ r1("d34","d50")
& ~ r1("d34","d49")
& ~ r1("d34","d48")
& ~ r1("d34","d47")
& ~ r1("d34","d46")
& ~ r1("d34","d45")
& ~ r1("d34","d44")
& ~ r1("d34","d43")
& ~ r1("d34","d42")
& ~ r1("d34","d41")
& ~ r1("d34","d40")
& ~ r1("d34","d39")
& ~ r1("d34","d38")
& ~ r1("d34","d37")
& ~ r1("d34","d36")
& ~ r1("d34","d35")
& r1("d34","d34")
& ~ r1("d34","d33")
& ~ r1("d34","d32")
& ~ r1("d34","d31")
& ~ r1("d34","d30")
& ~ r1("d34","d29")
& ~ r1("d34","d28")
& ~ r1("d34","d27")
& ~ r1("d34","d26")
& ~ r1("d34","d25")
& ~ r1("d34","d24")
& ~ r1("d34","d23")
& ~ r1("d34","d22")
& ~ r1("d34","d21")
& ~ r1("d34","d20")
& ~ r1("d34","d19")
& ~ r1("d34","d18")
& ~ r1("d34","d17")
& ~ r1("d34","d16")
& ~ r1("d34","d15")
& ~ r1("d34","d14")
& ~ r1("d34","d13")
& ~ r1("d34","d12")
& ~ r1("d34","d11")
& ~ r1("d34","d10")
& ~ r1("d34","d9")
& ~ r1("d34","d8")
& ~ r1("d34","d7")
& ~ r1("d34","d6")
& ~ r1("d34","d5")
& ~ r1("d34","d4")
& ~ r1("d34","d3")
& ~ r1("d34","d2")
& ~ r1("d34","d1")
& ~ r1("d34","d0")
& ~ r1("d33","d62")
& ~ r1("d33","d61")
& ~ r1("d33","d60")
& ~ r1("d33","d59")
& ~ r1("d33","d58")
& ~ r1("d33","d57")
& ~ r1("d33","d56")
& ~ r1("d33","d55")
& ~ r1("d33","d54")
& ~ r1("d33","d53")
& ~ r1("d33","d52")
& ~ r1("d33","d51")
& ~ r1("d33","d50")
& ~ r1("d33","d49")
& ~ r1("d33","d48")
& ~ r1("d33","d47")
& ~ r1("d33","d46")
& ~ r1("d33","d45")
& ~ r1("d33","d44")
& ~ r1("d33","d43")
& ~ r1("d33","d42")
& ~ r1("d33","d41")
& ~ r1("d33","d40")
& ~ r1("d33","d39")
& ~ r1("d33","d38")
& ~ r1("d33","d37")
& ~ r1("d33","d36")
& ~ r1("d33","d35")
& ~ r1("d33","d34")
& r1("d33","d33")
& ~ r1("d33","d32")
& ~ r1("d33","d31")
& ~ r1("d33","d30")
& ~ r1("d33","d29")
& ~ r1("d33","d28")
& ~ r1("d33","d27")
& ~ r1("d33","d26")
& ~ r1("d33","d25")
& ~ r1("d33","d24")
& ~ r1("d33","d23")
& ~ r1("d33","d22")
& ~ r1("d33","d21")
& ~ r1("d33","d20")
& ~ r1("d33","d19")
& ~ r1("d33","d18")
& ~ r1("d33","d17")
& ~ r1("d33","d16")
& ~ r1("d33","d15")
& ~ r1("d33","d14")
& ~ r1("d33","d13")
& ~ r1("d33","d12")
& ~ r1("d33","d11")
& ~ r1("d33","d10")
& ~ r1("d33","d9")
& ~ r1("d33","d8")
& ~ r1("d33","d7")
& ~ r1("d33","d6")
& ~ r1("d33","d5")
& ~ r1("d33","d4")
& ~ r1("d33","d3")
& ~ r1("d33","d2")
& ~ r1("d33","d1")
& ~ r1("d33","d0")
& ~ r1("d32","d62")
& ~ r1("d32","d61")
& ~ r1("d32","d60")
& ~ r1("d32","d59")
& ~ r1("d32","d58")
& ~ r1("d32","d57")
& ~ r1("d32","d56")
& ~ r1("d32","d55")
& ~ r1("d32","d54")
& ~ r1("d32","d53")
& ~ r1("d32","d52")
& ~ r1("d32","d51")
& ~ r1("d32","d50")
& ~ r1("d32","d49")
& ~ r1("d32","d48")
& ~ r1("d32","d47")
& ~ r1("d32","d46")
& ~ r1("d32","d45")
& ~ r1("d32","d44")
& ~ r1("d32","d43")
& ~ r1("d32","d42")
& ~ r1("d32","d41")
& ~ r1("d32","d40")
& ~ r1("d32","d39")
& ~ r1("d32","d38")
& ~ r1("d32","d37")
& ~ r1("d32","d36")
& ~ r1("d32","d35")
& ~ r1("d32","d34")
& ~ r1("d32","d33")
& r1("d32","d32")
& ~ r1("d32","d31")
& ~ r1("d32","d30")
& ~ r1("d32","d29")
& ~ r1("d32","d28")
& ~ r1("d32","d27")
& ~ r1("d32","d26")
& ~ r1("d32","d25")
& ~ r1("d32","d24")
& ~ r1("d32","d23")
& ~ r1("d32","d22")
& ~ r1("d32","d21")
& ~ r1("d32","d20")
& ~ r1("d32","d19")
& ~ r1("d32","d18")
& ~ r1("d32","d17")
& ~ r1("d32","d16")
& ~ r1("d32","d15")
& ~ r1("d32","d14")
& ~ r1("d32","d13")
& ~ r1("d32","d12")
& ~ r1("d32","d11")
& ~ r1("d32","d10")
& ~ r1("d32","d9")
& ~ r1("d32","d8")
& ~ r1("d32","d7")
& ~ r1("d32","d6")
& ~ r1("d32","d5")
& ~ r1("d32","d4")
& ~ r1("d32","d3")
& ~ r1("d32","d2")
& ~ r1("d32","d1")
& ~ r1("d32","d0")
& ~ r1("d31","d62")
& ~ r1("d31","d61")
& ~ r1("d31","d60")
& ~ r1("d31","d59")
& ~ r1("d31","d58")
& ~ r1("d31","d57")
& ~ r1("d31","d56")
& ~ r1("d31","d55")
& ~ r1("d31","d54")
& ~ r1("d31","d53")
& ~ r1("d31","d52")
& ~ r1("d31","d51")
& ~ r1("d31","d50")
& ~ r1("d31","d49")
& ~ r1("d31","d48")
& ~ r1("d31","d47")
& ~ r1("d31","d46")
& ~ r1("d31","d45")
& ~ r1("d31","d44")
& ~ r1("d31","d43")
& ~ r1("d31","d42")
& ~ r1("d31","d41")
& ~ r1("d31","d40")
& ~ r1("d31","d39")
& ~ r1("d31","d38")
& ~ r1("d31","d37")
& ~ r1("d31","d36")
& ~ r1("d31","d35")
& ~ r1("d31","d34")
& ~ r1("d31","d33")
& ~ r1("d31","d32")
& r1("d31","d31")
& ~ r1("d31","d30")
& ~ r1("d31","d29")
& ~ r1("d31","d28")
& ~ r1("d31","d27")
& ~ r1("d31","d26")
& ~ r1("d31","d25")
& ~ r1("d31","d24")
& ~ r1("d31","d23")
& ~ r1("d31","d22")
& ~ r1("d31","d21")
& ~ r1("d31","d20")
& ~ r1("d31","d19")
& ~ r1("d31","d18")
& ~ r1("d31","d17")
& ~ r1("d31","d16")
& ~ r1("d31","d15")
& ~ r1("d31","d14")
& ~ r1("d31","d13")
& ~ r1("d31","d12")
& ~ r1("d31","d11")
& ~ r1("d31","d10")
& ~ r1("d31","d9")
& ~ r1("d31","d8")
& ~ r1("d31","d7")
& ~ r1("d31","d6")
& ~ r1("d31","d5")
& ~ r1("d31","d4")
& ~ r1("d31","d3")
& ~ r1("d31","d2")
& ~ r1("d31","d1")
& ~ r1("d31","d0")
& r1("d30","d62")
& r1("d30","d61")
& ~ r1("d30","d60")
& ~ r1("d30","d59")
& ~ r1("d30","d58")
& ~ r1("d30","d57")
& ~ r1("d30","d56")
& ~ r1("d30","d55")
& ~ r1("d30","d54")
& ~ r1("d30","d53")
& ~ r1("d30","d52")
& ~ r1("d30","d51")
& ~ r1("d30","d50")
& ~ r1("d30","d49")
& ~ r1("d30","d48")
& ~ r1("d30","d47")
& ~ r1("d30","d46")
& ~ r1("d30","d45")
& ~ r1("d30","d44")
& ~ r1("d30","d43")
& ~ r1("d30","d42")
& ~ r1("d30","d41")
& ~ r1("d30","d40")
& ~ r1("d30","d39")
& ~ r1("d30","d38")
& ~ r1("d30","d37")
& ~ r1("d30","d36")
& ~ r1("d30","d35")
& ~ r1("d30","d34")
& ~ r1("d30","d33")
& ~ r1("d30","d32")
& ~ r1("d30","d31")
& r1("d30","d30")
& ~ r1("d30","d29")
& ~ r1("d30","d28")
& ~ r1("d30","d27")
& ~ r1("d30","d26")
& ~ r1("d30","d25")
& ~ r1("d30","d24")
& ~ r1("d30","d23")
& ~ r1("d30","d22")
& ~ r1("d30","d21")
& ~ r1("d30","d20")
& ~ r1("d30","d19")
& ~ r1("d30","d18")
& ~ r1("d30","d17")
& ~ r1("d30","d16")
& ~ r1("d30","d15")
& ~ r1("d30","d14")
& ~ r1("d30","d13")
& ~ r1("d30","d12")
& ~ r1("d30","d11")
& ~ r1("d30","d10")
& ~ r1("d30","d9")
& ~ r1("d30","d8")
& ~ r1("d30","d7")
& ~ r1("d30","d6")
& ~ r1("d30","d5")
& ~ r1("d30","d4")
& ~ r1("d30","d3")
& ~ r1("d30","d2")
& ~ r1("d30","d1")
& ~ r1("d30","d0")
& ~ r1("d29","d62")
& ~ r1("d29","d61")
& r1("d29","d60")
& r1("d29","d59")
& ~ r1("d29","d58")
& ~ r1("d29","d57")
& ~ r1("d29","d56")
& ~ r1("d29","d55")
& ~ r1("d29","d54")
& ~ r1("d29","d53")
& ~ r1("d29","d52")
& ~ r1("d29","d51")
& ~ r1("d29","d50")
& ~ r1("d29","d49")
& ~ r1("d29","d48")
& ~ r1("d29","d47")
& ~ r1("d29","d46")
& ~ r1("d29","d45")
& ~ r1("d29","d44")
& ~ r1("d29","d43")
& ~ r1("d29","d42")
& ~ r1("d29","d41")
& ~ r1("d29","d40")
& ~ r1("d29","d39")
& ~ r1("d29","d38")
& ~ r1("d29","d37")
& ~ r1("d29","d36")
& ~ r1("d29","d35")
& ~ r1("d29","d34")
& ~ r1("d29","d33")
& ~ r1("d29","d32")
& ~ r1("d29","d31")
& ~ r1("d29","d30")
& r1("d29","d29")
& ~ r1("d29","d28")
& ~ r1("d29","d27")
& ~ r1("d29","d26")
& ~ r1("d29","d25")
& ~ r1("d29","d24")
& ~ r1("d29","d23")
& ~ r1("d29","d22")
& ~ r1("d29","d21")
& ~ r1("d29","d20")
& ~ r1("d29","d19")
& ~ r1("d29","d18")
& ~ r1("d29","d17")
& ~ r1("d29","d16")
& ~ r1("d29","d15")
& ~ r1("d29","d14")
& ~ r1("d29","d13")
& ~ r1("d29","d12")
& ~ r1("d29","d11")
& ~ r1("d29","d10")
& ~ r1("d29","d9")
& ~ r1("d29","d8")
& ~ r1("d29","d7")
& ~ r1("d29","d6")
& ~ r1("d29","d5")
& ~ r1("d29","d4")
& ~ r1("d29","d3")
& ~ r1("d29","d2")
& ~ r1("d29","d1")
& ~ r1("d29","d0")
& ~ r1("d28","d62")
& ~ r1("d28","d61")
& ~ r1("d28","d60")
& ~ r1("d28","d59")
& r1("d28","d58")
& r1("d28","d57")
& ~ r1("d28","d56")
& ~ r1("d28","d55")
& ~ r1("d28","d54")
& ~ r1("d28","d53")
& ~ r1("d28","d52")
& ~ r1("d28","d51")
& ~ r1("d28","d50")
& ~ r1("d28","d49")
& ~ r1("d28","d48")
& ~ r1("d28","d47")
& ~ r1("d28","d46")
& ~ r1("d28","d45")
& ~ r1("d28","d44")
& ~ r1("d28","d43")
& ~ r1("d28","d42")
& ~ r1("d28","d41")
& ~ r1("d28","d40")
& ~ r1("d28","d39")
& ~ r1("d28","d38")
& ~ r1("d28","d37")
& ~ r1("d28","d36")
& ~ r1("d28","d35")
& ~ r1("d28","d34")
& ~ r1("d28","d33")
& ~ r1("d28","d32")
& ~ r1("d28","d31")
& ~ r1("d28","d30")
& ~ r1("d28","d29")
& r1("d28","d28")
& ~ r1("d28","d27")
& ~ r1("d28","d26")
& ~ r1("d28","d25")
& ~ r1("d28","d24")
& ~ r1("d28","d23")
& ~ r1("d28","d22")
& ~ r1("d28","d21")
& ~ r1("d28","d20")
& ~ r1("d28","d19")
& ~ r1("d28","d18")
& ~ r1("d28","d17")
& ~ r1("d28","d16")
& ~ r1("d28","d15")
& ~ r1("d28","d14")
& ~ r1("d28","d13")
& ~ r1("d28","d12")
& ~ r1("d28","d11")
& ~ r1("d28","d10")
& ~ r1("d28","d9")
& ~ r1("d28","d8")
& ~ r1("d28","d7")
& ~ r1("d28","d6")
& ~ r1("d28","d5")
& ~ r1("d28","d4")
& ~ r1("d28","d3")
& ~ r1("d28","d2")
& ~ r1("d28","d1")
& ~ r1("d28","d0")
& ~ r1("d27","d62")
& ~ r1("d27","d61")
& ~ r1("d27","d60")
& ~ r1("d27","d59")
& ~ r1("d27","d58")
& ~ r1("d27","d57")
& r1("d27","d56")
& r1("d27","d55")
& ~ r1("d27","d54")
& ~ r1("d27","d53")
& ~ r1("d27","d52")
& ~ r1("d27","d51")
& ~ r1("d27","d50")
& ~ r1("d27","d49")
& ~ r1("d27","d48")
& ~ r1("d27","d47")
& ~ r1("d27","d46")
& ~ r1("d27","d45")
& ~ r1("d27","d44")
& ~ r1("d27","d43")
& ~ r1("d27","d42")
& ~ r1("d27","d41")
& ~ r1("d27","d40")
& ~ r1("d27","d39")
& ~ r1("d27","d38")
& ~ r1("d27","d37")
& ~ r1("d27","d36")
& ~ r1("d27","d35")
& ~ r1("d27","d34")
& ~ r1("d27","d33")
& ~ r1("d27","d32")
& ~ r1("d27","d31")
& ~ r1("d27","d30")
& ~ r1("d27","d29")
& ~ r1("d27","d28")
& r1("d27","d27")
& ~ r1("d27","d26")
& ~ r1("d27","d25")
& ~ r1("d27","d24")
& ~ r1("d27","d23")
& ~ r1("d27","d22")
& ~ r1("d27","d21")
& ~ r1("d27","d20")
& ~ r1("d27","d19")
& ~ r1("d27","d18")
& ~ r1("d27","d17")
& ~ r1("d27","d16")
& ~ r1("d27","d15")
& ~ r1("d27","d14")
& ~ r1("d27","d13")
& ~ r1("d27","d12")
& ~ r1("d27","d11")
& ~ r1("d27","d10")
& ~ r1("d27","d9")
& ~ r1("d27","d8")
& ~ r1("d27","d7")
& ~ r1("d27","d6")
& ~ r1("d27","d5")
& ~ r1("d27","d4")
& ~ r1("d27","d3")
& ~ r1("d27","d2")
& ~ r1("d27","d1")
& ~ r1("d27","d0")
& ~ r1("d26","d62")
& ~ r1("d26","d61")
& ~ r1("d26","d60")
& ~ r1("d26","d59")
& ~ r1("d26","d58")
& ~ r1("d26","d57")
& ~ r1("d26","d56")
& ~ r1("d26","d55")
& r1("d26","d54")
& r1("d26","d53")
& ~ r1("d26","d52")
& ~ r1("d26","d51")
& ~ r1("d26","d50")
& ~ r1("d26","d49")
& ~ r1("d26","d48")
& ~ r1("d26","d47")
& ~ r1("d26","d46")
& ~ r1("d26","d45")
& ~ r1("d26","d44")
& ~ r1("d26","d43")
& ~ r1("d26","d42")
& ~ r1("d26","d41")
& ~ r1("d26","d40")
& ~ r1("d26","d39")
& ~ r1("d26","d38")
& ~ r1("d26","d37")
& ~ r1("d26","d36")
& ~ r1("d26","d35")
& ~ r1("d26","d34")
& ~ r1("d26","d33")
& ~ r1("d26","d32")
& ~ r1("d26","d31")
& ~ r1("d26","d30")
& ~ r1("d26","d29")
& ~ r1("d26","d28")
& ~ r1("d26","d27")
& r1("d26","d26")
& ~ r1("d26","d25")
& ~ r1("d26","d24")
& ~ r1("d26","d23")
& ~ r1("d26","d22")
& ~ r1("d26","d21")
& ~ r1("d26","d20")
& ~ r1("d26","d19")
& ~ r1("d26","d18")
& ~ r1("d26","d17")
& ~ r1("d26","d16")
& ~ r1("d26","d15")
& ~ r1("d26","d14")
& ~ r1("d26","d13")
& ~ r1("d26","d12")
& ~ r1("d26","d11")
& ~ r1("d26","d10")
& ~ r1("d26","d9")
& ~ r1("d26","d8")
& ~ r1("d26","d7")
& ~ r1("d26","d6")
& ~ r1("d26","d5")
& ~ r1("d26","d4")
& ~ r1("d26","d3")
& ~ r1("d26","d2")
& ~ r1("d26","d1")
& ~ r1("d26","d0")
& ~ r1("d25","d62")
& ~ r1("d25","d61")
& ~ r1("d25","d60")
& ~ r1("d25","d59")
& ~ r1("d25","d58")
& ~ r1("d25","d57")
& ~ r1("d25","d56")
& ~ r1("d25","d55")
& ~ r1("d25","d54")
& ~ r1("d25","d53")
& r1("d25","d52")
& r1("d25","d51")
& ~ r1("d25","d50")
& ~ r1("d25","d49")
& ~ r1("d25","d48")
& ~ r1("d25","d47")
& ~ r1("d25","d46")
& ~ r1("d25","d45")
& ~ r1("d25","d44")
& ~ r1("d25","d43")
& ~ r1("d25","d42")
& ~ r1("d25","d41")
& ~ r1("d25","d40")
& ~ r1("d25","d39")
& ~ r1("d25","d38")
& ~ r1("d25","d37")
& ~ r1("d25","d36")
& ~ r1("d25","d35")
& ~ r1("d25","d34")
& ~ r1("d25","d33")
& ~ r1("d25","d32")
& ~ r1("d25","d31")
& ~ r1("d25","d30")
& ~ r1("d25","d29")
& ~ r1("d25","d28")
& ~ r1("d25","d27")
& ~ r1("d25","d26")
& r1("d25","d25")
& ~ r1("d25","d24")
& ~ r1("d25","d23")
& ~ r1("d25","d22")
& ~ r1("d25","d21")
& ~ r1("d25","d20")
& ~ r1("d25","d19")
& ~ r1("d25","d18")
& ~ r1("d25","d17")
& ~ r1("d25","d16")
& ~ r1("d25","d15")
& ~ r1("d25","d14")
& ~ r1("d25","d13")
& ~ r1("d25","d12")
& ~ r1("d25","d11")
& ~ r1("d25","d10")
& ~ r1("d25","d9")
& ~ r1("d25","d8")
& ~ r1("d25","d7")
& ~ r1("d25","d6")
& ~ r1("d25","d5")
& ~ r1("d25","d4")
& ~ r1("d25","d3")
& ~ r1("d25","d2")
& ~ r1("d25","d1")
& ~ r1("d25","d0")
& ~ r1("d24","d62")
& ~ r1("d24","d61")
& ~ r1("d24","d60")
& ~ r1("d24","d59")
& ~ r1("d24","d58")
& ~ r1("d24","d57")
& ~ r1("d24","d56")
& ~ r1("d24","d55")
& ~ r1("d24","d54")
& ~ r1("d24","d53")
& ~ r1("d24","d52")
& ~ r1("d24","d51")
& r1("d24","d50")
& r1("d24","d49")
& ~ r1("d24","d48")
& ~ r1("d24","d47")
& ~ r1("d24","d46")
& ~ r1("d24","d45")
& ~ r1("d24","d44")
& ~ r1("d24","d43")
& ~ r1("d24","d42")
& ~ r1("d24","d41")
& ~ r1("d24","d40")
& ~ r1("d24","d39")
& ~ r1("d24","d38")
& ~ r1("d24","d37")
& ~ r1("d24","d36")
& ~ r1("d24","d35")
& ~ r1("d24","d34")
& ~ r1("d24","d33")
& ~ r1("d24","d32")
& ~ r1("d24","d31")
& ~ r1("d24","d30")
& ~ r1("d24","d29")
& ~ r1("d24","d28")
& ~ r1("d24","d27")
& ~ r1("d24","d26")
& ~ r1("d24","d25")
& r1("d24","d24")
& ~ r1("d24","d23")
& ~ r1("d24","d22")
& ~ r1("d24","d21")
& ~ r1("d24","d20")
& ~ r1("d24","d19")
& ~ r1("d24","d18")
& ~ r1("d24","d17")
& ~ r1("d24","d16")
& ~ r1("d24","d15")
& ~ r1("d24","d14")
& ~ r1("d24","d13")
& ~ r1("d24","d12")
& ~ r1("d24","d11")
& ~ r1("d24","d10")
& ~ r1("d24","d9")
& ~ r1("d24","d8")
& ~ r1("d24","d7")
& ~ r1("d24","d6")
& ~ r1("d24","d5")
& ~ r1("d24","d4")
& ~ r1("d24","d3")
& ~ r1("d24","d2")
& ~ r1("d24","d1")
& ~ r1("d24","d0")
& ~ r1("d23","d62")
& ~ r1("d23","d61")
& ~ r1("d23","d60")
& ~ r1("d23","d59")
& ~ r1("d23","d58")
& ~ r1("d23","d57")
& ~ r1("d23","d56")
& ~ r1("d23","d55")
& ~ r1("d23","d54")
& ~ r1("d23","d53")
& ~ r1("d23","d52")
& ~ r1("d23","d51")
& ~ r1("d23","d50")
& ~ r1("d23","d49")
& r1("d23","d48")
& r1("d23","d47")
& ~ r1("d23","d46")
& ~ r1("d23","d45")
& ~ r1("d23","d44")
& ~ r1("d23","d43")
& ~ r1("d23","d42")
& ~ r1("d23","d41")
& ~ r1("d23","d40")
& ~ r1("d23","d39")
& ~ r1("d23","d38")
& ~ r1("d23","d37")
& ~ r1("d23","d36")
& ~ r1("d23","d35")
& ~ r1("d23","d34")
& ~ r1("d23","d33")
& ~ r1("d23","d32")
& ~ r1("d23","d31")
& ~ r1("d23","d30")
& ~ r1("d23","d29")
& ~ r1("d23","d28")
& ~ r1("d23","d27")
& ~ r1("d23","d26")
& ~ r1("d23","d25")
& ~ r1("d23","d24")
& r1("d23","d23")
& ~ r1("d23","d22")
& ~ r1("d23","d21")
& ~ r1("d23","d20")
& ~ r1("d23","d19")
& ~ r1("d23","d18")
& ~ r1("d23","d17")
& ~ r1("d23","d16")
& ~ r1("d23","d15")
& ~ r1("d23","d14")
& ~ r1("d23","d13")
& ~ r1("d23","d12")
& ~ r1("d23","d11")
& ~ r1("d23","d10")
& ~ r1("d23","d9")
& ~ r1("d23","d8")
& ~ r1("d23","d7")
& ~ r1("d23","d6")
& ~ r1("d23","d5")
& ~ r1("d23","d4")
& ~ r1("d23","d3")
& ~ r1("d23","d2")
& ~ r1("d23","d1")
& ~ r1("d23","d0")
& ~ r1("d22","d62")
& ~ r1("d22","d61")
& ~ r1("d22","d60")
& ~ r1("d22","d59")
& ~ r1("d22","d58")
& ~ r1("d22","d57")
& ~ r1("d22","d56")
& ~ r1("d22","d55")
& ~ r1("d22","d54")
& ~ r1("d22","d53")
& ~ r1("d22","d52")
& ~ r1("d22","d51")
& ~ r1("d22","d50")
& ~ r1("d22","d49")
& ~ r1("d22","d48")
& ~ r1("d22","d47")
& r1("d22","d46")
& r1("d22","d45")
& ~ r1("d22","d44")
& ~ r1("d22","d43")
& ~ r1("d22","d42")
& ~ r1("d22","d41")
& ~ r1("d22","d40")
& ~ r1("d22","d39")
& ~ r1("d22","d38")
& ~ r1("d22","d37")
& ~ r1("d22","d36")
& ~ r1("d22","d35")
& ~ r1("d22","d34")
& ~ r1("d22","d33")
& ~ r1("d22","d32")
& ~ r1("d22","d31")
& ~ r1("d22","d30")
& ~ r1("d22","d29")
& ~ r1("d22","d28")
& ~ r1("d22","d27")
& ~ r1("d22","d26")
& ~ r1("d22","d25")
& ~ r1("d22","d24")
& ~ r1("d22","d23")
& r1("d22","d22")
& ~ r1("d22","d21")
& ~ r1("d22","d20")
& ~ r1("d22","d19")
& ~ r1("d22","d18")
& ~ r1("d22","d17")
& ~ r1("d22","d16")
& ~ r1("d22","d15")
& ~ r1("d22","d14")
& ~ r1("d22","d13")
& ~ r1("d22","d12")
& ~ r1("d22","d11")
& ~ r1("d22","d10")
& ~ r1("d22","d9")
& ~ r1("d22","d8")
& ~ r1("d22","d7")
& ~ r1("d22","d6")
& ~ r1("d22","d5")
& ~ r1("d22","d4")
& ~ r1("d22","d3")
& ~ r1("d22","d2")
& ~ r1("d22","d1")
& ~ r1("d22","d0")
& ~ r1("d21","d62")
& ~ r1("d21","d61")
& ~ r1("d21","d60")
& ~ r1("d21","d59")
& ~ r1("d21","d58")
& ~ r1("d21","d57")
& ~ r1("d21","d56")
& ~ r1("d21","d55")
& ~ r1("d21","d54")
& ~ r1("d21","d53")
& ~ r1("d21","d52")
& ~ r1("d21","d51")
& ~ r1("d21","d50")
& ~ r1("d21","d49")
& ~ r1("d21","d48")
& ~ r1("d21","d47")
& ~ r1("d21","d46")
& ~ r1("d21","d45")
& r1("d21","d44")
& r1("d21","d43")
& ~ r1("d21","d42")
& ~ r1("d21","d41")
& ~ r1("d21","d40")
& ~ r1("d21","d39")
& ~ r1("d21","d38")
& ~ r1("d21","d37")
& ~ r1("d21","d36")
& ~ r1("d21","d35")
& ~ r1("d21","d34")
& ~ r1("d21","d33")
& ~ r1("d21","d32")
& ~ r1("d21","d31")
& ~ r1("d21","d30")
& ~ r1("d21","d29")
& ~ r1("d21","d28")
& ~ r1("d21","d27")
& ~ r1("d21","d26")
& ~ r1("d21","d25")
& ~ r1("d21","d24")
& ~ r1("d21","d23")
& ~ r1("d21","d22")
& r1("d21","d21")
& ~ r1("d21","d20")
& ~ r1("d21","d19")
& ~ r1("d21","d18")
& ~ r1("d21","d17")
& ~ r1("d21","d16")
& ~ r1("d21","d15")
& ~ r1("d21","d14")
& ~ r1("d21","d13")
& ~ r1("d21","d12")
& ~ r1("d21","d11")
& ~ r1("d21","d10")
& ~ r1("d21","d9")
& ~ r1("d21","d8")
& ~ r1("d21","d7")
& ~ r1("d21","d6")
& ~ r1("d21","d5")
& ~ r1("d21","d4")
& ~ r1("d21","d3")
& ~ r1("d21","d2")
& ~ r1("d21","d1")
& ~ r1("d21","d0")
& ~ r1("d20","d62")
& ~ r1("d20","d61")
& ~ r1("d20","d60")
& ~ r1("d20","d59")
& ~ r1("d20","d58")
& ~ r1("d20","d57")
& ~ r1("d20","d56")
& ~ r1("d20","d55")
& ~ r1("d20","d54")
& ~ r1("d20","d53")
& ~ r1("d20","d52")
& ~ r1("d20","d51")
& ~ r1("d20","d50")
& ~ r1("d20","d49")
& ~ r1("d20","d48")
& ~ r1("d20","d47")
& ~ r1("d20","d46")
& ~ r1("d20","d45")
& ~ r1("d20","d44")
& ~ r1("d20","d43")
& r1("d20","d42")
& r1("d20","d41")
& ~ r1("d20","d40")
& ~ r1("d20","d39")
& ~ r1("d20","d38")
& ~ r1("d20","d37")
& ~ r1("d20","d36")
& ~ r1("d20","d35")
& ~ r1("d20","d34")
& ~ r1("d20","d33")
& ~ r1("d20","d32")
& ~ r1("d20","d31")
& ~ r1("d20","d30")
& ~ r1("d20","d29")
& ~ r1("d20","d28")
& ~ r1("d20","d27")
& ~ r1("d20","d26")
& ~ r1("d20","d25")
& ~ r1("d20","d24")
& ~ r1("d20","d23")
& ~ r1("d20","d22")
& ~ r1("d20","d21")
& r1("d20","d20")
& ~ r1("d20","d19")
& ~ r1("d20","d18")
& ~ r1("d20","d17")
& ~ r1("d20","d16")
& ~ r1("d20","d15")
& ~ r1("d20","d14")
& ~ r1("d20","d13")
& ~ r1("d20","d12")
& ~ r1("d20","d11")
& ~ r1("d20","d10")
& ~ r1("d20","d9")
& ~ r1("d20","d8")
& ~ r1("d20","d7")
& ~ r1("d20","d6")
& ~ r1("d20","d5")
& ~ r1("d20","d4")
& ~ r1("d20","d3")
& ~ r1("d20","d2")
& ~ r1("d20","d1")
& ~ r1("d20","d0")
& ~ r1("d19","d62")
& ~ r1("d19","d61")
& ~ r1("d19","d60")
& ~ r1("d19","d59")
& ~ r1("d19","d58")
& ~ r1("d19","d57")
& ~ r1("d19","d56")
& ~ r1("d19","d55")
& ~ r1("d19","d54")
& ~ r1("d19","d53")
& ~ r1("d19","d52")
& ~ r1("d19","d51")
& ~ r1("d19","d50")
& ~ r1("d19","d49")
& ~ r1("d19","d48")
& ~ r1("d19","d47")
& ~ r1("d19","d46")
& ~ r1("d19","d45")
& ~ r1("d19","d44")
& ~ r1("d19","d43")
& ~ r1("d19","d42")
& ~ r1("d19","d41")
& r1("d19","d40")
& r1("d19","d39")
& ~ r1("d19","d38")
& ~ r1("d19","d37")
& ~ r1("d19","d36")
& ~ r1("d19","d35")
& ~ r1("d19","d34")
& ~ r1("d19","d33")
& ~ r1("d19","d32")
& ~ r1("d19","d31")
& ~ r1("d19","d30")
& ~ r1("d19","d29")
& ~ r1("d19","d28")
& ~ r1("d19","d27")
& ~ r1("d19","d26")
& ~ r1("d19","d25")
& ~ r1("d19","d24")
& ~ r1("d19","d23")
& ~ r1("d19","d22")
& ~ r1("d19","d21")
& ~ r1("d19","d20")
& r1("d19","d19")
& ~ r1("d19","d18")
& ~ r1("d19","d17")
& ~ r1("d19","d16")
& ~ r1("d19","d15")
& ~ r1("d19","d14")
& ~ r1("d19","d13")
& ~ r1("d19","d12")
& ~ r1("d19","d11")
& ~ r1("d19","d10")
& ~ r1("d19","d9")
& ~ r1("d19","d8")
& ~ r1("d19","d7")
& ~ r1("d19","d6")
& ~ r1("d19","d5")
& ~ r1("d19","d4")
& ~ r1("d19","d3")
& ~ r1("d19","d2")
& ~ r1("d19","d1")
& ~ r1("d19","d0")
& ~ r1("d18","d62")
& ~ r1("d18","d61")
& ~ r1("d18","d60")
& ~ r1("d18","d59")
& ~ r1("d18","d58")
& ~ r1("d18","d57")
& ~ r1("d18","d56")
& ~ r1("d18","d55")
& ~ r1("d18","d54")
& ~ r1("d18","d53")
& ~ r1("d18","d52")
& ~ r1("d18","d51")
& ~ r1("d18","d50")
& ~ r1("d18","d49")
& ~ r1("d18","d48")
& ~ r1("d18","d47")
& ~ r1("d18","d46")
& ~ r1("d18","d45")
& ~ r1("d18","d44")
& ~ r1("d18","d43")
& ~ r1("d18","d42")
& ~ r1("d18","d41")
& ~ r1("d18","d40")
& ~ r1("d18","d39")
& r1("d18","d38")
& r1("d18","d37")
& ~ r1("d18","d36")
& ~ r1("d18","d35")
& ~ r1("d18","d34")
& ~ r1("d18","d33")
& ~ r1("d18","d32")
& ~ r1("d18","d31")
& ~ r1("d18","d30")
& ~ r1("d18","d29")
& ~ r1("d18","d28")
& ~ r1("d18","d27")
& ~ r1("d18","d26")
& ~ r1("d18","d25")
& ~ r1("d18","d24")
& ~ r1("d18","d23")
& ~ r1("d18","d22")
& ~ r1("d18","d21")
& ~ r1("d18","d20")
& ~ r1("d18","d19")
& r1("d18","d18")
& ~ r1("d18","d17")
& ~ r1("d18","d16")
& ~ r1("d18","d15")
& ~ r1("d18","d14")
& ~ r1("d18","d13")
& ~ r1("d18","d12")
& ~ r1("d18","d11")
& ~ r1("d18","d10")
& ~ r1("d18","d9")
& ~ r1("d18","d8")
& ~ r1("d18","d7")
& ~ r1("d18","d6")
& ~ r1("d18","d5")
& ~ r1("d18","d4")
& ~ r1("d18","d3")
& ~ r1("d18","d2")
& ~ r1("d18","d1")
& ~ r1("d18","d0")
& ~ r1("d17","d62")
& ~ r1("d17","d61")
& ~ r1("d17","d60")
& ~ r1("d17","d59")
& ~ r1("d17","d58")
& ~ r1("d17","d57")
& ~ r1("d17","d56")
& ~ r1("d17","d55")
& ~ r1("d17","d54")
& ~ r1("d17","d53")
& ~ r1("d17","d52")
& ~ r1("d17","d51")
& ~ r1("d17","d50")
& ~ r1("d17","d49")
& ~ r1("d17","d48")
& ~ r1("d17","d47")
& ~ r1("d17","d46")
& ~ r1("d17","d45")
& ~ r1("d17","d44")
& ~ r1("d17","d43")
& ~ r1("d17","d42")
& ~ r1("d17","d41")
& ~ r1("d17","d40")
& ~ r1("d17","d39")
& ~ r1("d17","d38")
& ~ r1("d17","d37")
& r1("d17","d36")
& r1("d17","d35")
& ~ r1("d17","d34")
& ~ r1("d17","d33")
& ~ r1("d17","d32")
& ~ r1("d17","d31")
& ~ r1("d17","d30")
& ~ r1("d17","d29")
& ~ r1("d17","d28")
& ~ r1("d17","d27")
& ~ r1("d17","d26")
& ~ r1("d17","d25")
& ~ r1("d17","d24")
& ~ r1("d17","d23")
& ~ r1("d17","d22")
& ~ r1("d17","d21")
& ~ r1("d17","d20")
& ~ r1("d17","d19")
& ~ r1("d17","d18")
& r1("d17","d17")
& ~ r1("d17","d16")
& ~ r1("d17","d15")
& ~ r1("d17","d14")
& ~ r1("d17","d13")
& ~ r1("d17","d12")
& ~ r1("d17","d11")
& ~ r1("d17","d10")
& ~ r1("d17","d9")
& ~ r1("d17","d8")
& ~ r1("d17","d7")
& ~ r1("d17","d6")
& ~ r1("d17","d5")
& ~ r1("d17","d4")
& ~ r1("d17","d3")
& ~ r1("d17","d2")
& ~ r1("d17","d1")
& ~ r1("d17","d0")
& ~ r1("d16","d62")
& ~ r1("d16","d61")
& ~ r1("d16","d60")
& ~ r1("d16","d59")
& ~ r1("d16","d58")
& ~ r1("d16","d57")
& ~ r1("d16","d56")
& ~ r1("d16","d55")
& ~ r1("d16","d54")
& ~ r1("d16","d53")
& ~ r1("d16","d52")
& ~ r1("d16","d51")
& ~ r1("d16","d50")
& ~ r1("d16","d49")
& ~ r1("d16","d48")
& ~ r1("d16","d47")
& ~ r1("d16","d46")
& ~ r1("d16","d45")
& ~ r1("d16","d44")
& ~ r1("d16","d43")
& ~ r1("d16","d42")
& ~ r1("d16","d41")
& ~ r1("d16","d40")
& ~ r1("d16","d39")
& ~ r1("d16","d38")
& ~ r1("d16","d37")
& ~ r1("d16","d36")
& ~ r1("d16","d35")
& r1("d16","d34")
& r1("d16","d33")
& ~ r1("d16","d32")
& ~ r1("d16","d31")
& ~ r1("d16","d30")
& ~ r1("d16","d29")
& ~ r1("d16","d28")
& ~ r1("d16","d27")
& ~ r1("d16","d26")
& ~ r1("d16","d25")
& ~ r1("d16","d24")
& ~ r1("d16","d23")
& ~ r1("d16","d22")
& ~ r1("d16","d21")
& ~ r1("d16","d20")
& ~ r1("d16","d19")
& ~ r1("d16","d18")
& ~ r1("d16","d17")
& r1("d16","d16")
& ~ r1("d16","d15")
& ~ r1("d16","d14")
& ~ r1("d16","d13")
& ~ r1("d16","d12")
& ~ r1("d16","d11")
& ~ r1("d16","d10")
& ~ r1("d16","d9")
& ~ r1("d16","d8")
& ~ r1("d16","d7")
& ~ r1("d16","d6")
& ~ r1("d16","d5")
& ~ r1("d16","d4")
& ~ r1("d16","d3")
& ~ r1("d16","d2")
& ~ r1("d16","d1")
& ~ r1("d16","d0")
& ~ r1("d15","d62")
& ~ r1("d15","d61")
& ~ r1("d15","d60")
& ~ r1("d15","d59")
& ~ r1("d15","d58")
& ~ r1("d15","d57")
& ~ r1("d15","d56")
& ~ r1("d15","d55")
& ~ r1("d15","d54")
& ~ r1("d15","d53")
& ~ r1("d15","d52")
& ~ r1("d15","d51")
& ~ r1("d15","d50")
& ~ r1("d15","d49")
& ~ r1("d15","d48")
& ~ r1("d15","d47")
& ~ r1("d15","d46")
& ~ r1("d15","d45")
& ~ r1("d15","d44")
& ~ r1("d15","d43")
& ~ r1("d15","d42")
& ~ r1("d15","d41")
& ~ r1("d15","d40")
& ~ r1("d15","d39")
& ~ r1("d15","d38")
& ~ r1("d15","d37")
& ~ r1("d15","d36")
& ~ r1("d15","d35")
& ~ r1("d15","d34")
& ~ r1("d15","d33")
& r1("d15","d32")
& r1("d15","d31")
& ~ r1("d15","d30")
& ~ r1("d15","d29")
& ~ r1("d15","d28")
& ~ r1("d15","d27")
& ~ r1("d15","d26")
& ~ r1("d15","d25")
& ~ r1("d15","d24")
& ~ r1("d15","d23")
& ~ r1("d15","d22")
& ~ r1("d15","d21")
& ~ r1("d15","d20")
& ~ r1("d15","d19")
& ~ r1("d15","d18")
& ~ r1("d15","d17")
& ~ r1("d15","d16")
& r1("d15","d15")
& ~ r1("d15","d14")
& ~ r1("d15","d13")
& ~ r1("d15","d12")
& ~ r1("d15","d11")
& ~ r1("d15","d10")
& ~ r1("d15","d9")
& ~ r1("d15","d8")
& ~ r1("d15","d7")
& ~ r1("d15","d6")
& ~ r1("d15","d5")
& ~ r1("d15","d4")
& ~ r1("d15","d3")
& ~ r1("d15","d2")
& ~ r1("d15","d1")
& ~ r1("d15","d0")
& r1("d14","d62")
& r1("d14","d61")
& r1("d14","d60")
& r1("d14","d59")
& ~ r1("d14","d58")
& ~ r1("d14","d57")
& ~ r1("d14","d56")
& ~ r1("d14","d55")
& ~ r1("d14","d54")
& ~ r1("d14","d53")
& ~ r1("d14","d52")
& ~ r1("d14","d51")
& ~ r1("d14","d50")
& ~ r1("d14","d49")
& ~ r1("d14","d48")
& ~ r1("d14","d47")
& ~ r1("d14","d46")
& ~ r1("d14","d45")
& ~ r1("d14","d44")
& ~ r1("d14","d43")
& ~ r1("d14","d42")
& ~ r1("d14","d41")
& ~ r1("d14","d40")
& ~ r1("d14","d39")
& ~ r1("d14","d38")
& ~ r1("d14","d37")
& ~ r1("d14","d36")
& ~ r1("d14","d35")
& ~ r1("d14","d34")
& ~ r1("d14","d33")
& ~ r1("d14","d32")
& ~ r1("d14","d31")
& r1("d14","d30")
& r1("d14","d29")
& ~ r1("d14","d28")
& ~ r1("d14","d27")
& ~ r1("d14","d26")
& ~ r1("d14","d25")
& ~ r1("d14","d24")
& ~ r1("d14","d23")
& ~ r1("d14","d22")
& ~ r1("d14","d21")
& ~ r1("d14","d20")
& ~ r1("d14","d19")
& ~ r1("d14","d18")
& ~ r1("d14","d17")
& ~ r1("d14","d16")
& ~ r1("d14","d15")
& r1("d14","d14")
& ~ r1("d14","d13")
& ~ r1("d14","d12")
& ~ r1("d14","d11")
& ~ r1("d14","d10")
& ~ r1("d14","d9")
& ~ r1("d14","d8")
& ~ r1("d14","d7")
& ~ r1("d14","d6")
& ~ r1("d14","d5")
& ~ r1("d14","d4")
& ~ r1("d14","d3")
& ~ r1("d14","d2")
& ~ r1("d14","d1")
& ~ r1("d14","d0")
& ~ r1("d13","d62")
& ~ r1("d13","d61")
& ~ r1("d13","d60")
& ~ r1("d13","d59")
& r1("d13","d58")
& r1("d13","d57")
& r1("d13","d56")
& r1("d13","d55")
& ~ r1("d13","d54")
& ~ r1("d13","d53")
& ~ r1("d13","d52")
& ~ r1("d13","d51")
& ~ r1("d13","d50")
& ~ r1("d13","d49")
& ~ r1("d13","d48")
& ~ r1("d13","d47")
& ~ r1("d13","d46")
& ~ r1("d13","d45")
& ~ r1("d13","d44")
& ~ r1("d13","d43")
& ~ r1("d13","d42")
& ~ r1("d13","d41")
& ~ r1("d13","d40")
& ~ r1("d13","d39")
& ~ r1("d13","d38")
& ~ r1("d13","d37")
& ~ r1("d13","d36")
& ~ r1("d13","d35")
& ~ r1("d13","d34")
& ~ r1("d13","d33")
& ~ r1("d13","d32")
& ~ r1("d13","d31")
& ~ r1("d13","d30")
& ~ r1("d13","d29")
& r1("d13","d28")
& r1("d13","d27")
& ~ r1("d13","d26")
& ~ r1("d13","d25")
& ~ r1("d13","d24")
& ~ r1("d13","d23")
& ~ r1("d13","d22")
& ~ r1("d13","d21")
& ~ r1("d13","d20")
& ~ r1("d13","d19")
& ~ r1("d13","d18")
& ~ r1("d13","d17")
& ~ r1("d13","d16")
& ~ r1("d13","d15")
& ~ r1("d13","d14")
& r1("d13","d13")
& ~ r1("d13","d12")
& ~ r1("d13","d11")
& ~ r1("d13","d10")
& ~ r1("d13","d9")
& ~ r1("d13","d8")
& ~ r1("d13","d7")
& ~ r1("d13","d6")
& ~ r1("d13","d5")
& ~ r1("d13","d4")
& ~ r1("d13","d3")
& ~ r1("d13","d2")
& ~ r1("d13","d1")
& ~ r1("d13","d0")
& ~ r1("d12","d62")
& ~ r1("d12","d61")
& ~ r1("d12","d60")
& ~ r1("d12","d59")
& ~ r1("d12","d58")
& ~ r1("d12","d57")
& ~ r1("d12","d56")
& ~ r1("d12","d55")
& r1("d12","d54")
& r1("d12","d53")
& r1("d12","d52")
& r1("d12","d51")
& ~ r1("d12","d50")
& ~ r1("d12","d49")
& ~ r1("d12","d48")
& ~ r1("d12","d47")
& ~ r1("d12","d46")
& ~ r1("d12","d45")
& ~ r1("d12","d44")
& ~ r1("d12","d43")
& ~ r1("d12","d42")
& ~ r1("d12","d41")
& ~ r1("d12","d40")
& ~ r1("d12","d39")
& ~ r1("d12","d38")
& ~ r1("d12","d37")
& ~ r1("d12","d36")
& ~ r1("d12","d35")
& ~ r1("d12","d34")
& ~ r1("d12","d33")
& ~ r1("d12","d32")
& ~ r1("d12","d31")
& ~ r1("d12","d30")
& ~ r1("d12","d29")
& ~ r1("d12","d28")
& ~ r1("d12","d27")
& r1("d12","d26")
& r1("d12","d25")
& ~ r1("d12","d24")
& ~ r1("d12","d23")
& ~ r1("d12","d22")
& ~ r1("d12","d21")
& ~ r1("d12","d20")
& ~ r1("d12","d19")
& ~ r1("d12","d18")
& ~ r1("d12","d17")
& ~ r1("d12","d16")
& ~ r1("d12","d15")
& ~ r1("d12","d14")
& ~ r1("d12","d13")
& r1("d12","d12")
& ~ r1("d12","d11")
& ~ r1("d12","d10")
& ~ r1("d12","d9")
& ~ r1("d12","d8")
& ~ r1("d12","d7")
& ~ r1("d12","d6")
& ~ r1("d12","d5")
& ~ r1("d12","d4")
& ~ r1("d12","d3")
& ~ r1("d12","d2")
& ~ r1("d12","d1")
& ~ r1("d12","d0")
& ~ r1("d11","d62")
& ~ r1("d11","d61")
& ~ r1("d11","d60")
& ~ r1("d11","d59")
& ~ r1("d11","d58")
& ~ r1("d11","d57")
& ~ r1("d11","d56")
& ~ r1("d11","d55")
& ~ r1("d11","d54")
& ~ r1("d11","d53")
& ~ r1("d11","d52")
& ~ r1("d11","d51")
& r1("d11","d50")
& r1("d11","d49")
& r1("d11","d48")
& r1("d11","d47")
& ~ r1("d11","d46")
& ~ r1("d11","d45")
& ~ r1("d11","d44")
& ~ r1("d11","d43")
& ~ r1("d11","d42")
& ~ r1("d11","d41")
& ~ r1("d11","d40")
& ~ r1("d11","d39")
& ~ r1("d11","d38")
& ~ r1("d11","d37")
& ~ r1("d11","d36")
& ~ r1("d11","d35")
& ~ r1("d11","d34")
& ~ r1("d11","d33")
& ~ r1("d11","d32")
& ~ r1("d11","d31")
& ~ r1("d11","d30")
& ~ r1("d11","d29")
& ~ r1("d11","d28")
& ~ r1("d11","d27")
& ~ r1("d11","d26")
& ~ r1("d11","d25")
& r1("d11","d24")
& r1("d11","d23")
& ~ r1("d11","d22")
& ~ r1("d11","d21")
& ~ r1("d11","d20")
& ~ r1("d11","d19")
& ~ r1("d11","d18")
& ~ r1("d11","d17")
& ~ r1("d11","d16")
& ~ r1("d11","d15")
& ~ r1("d11","d14")
& ~ r1("d11","d13")
& ~ r1("d11","d12")
& r1("d11","d11")
& ~ r1("d11","d10")
& ~ r1("d11","d9")
& ~ r1("d11","d8")
& ~ r1("d11","d7")
& ~ r1("d11","d6")
& ~ r1("d11","d5")
& ~ r1("d11","d4")
& ~ r1("d11","d3")
& ~ r1("d11","d2")
& ~ r1("d11","d1")
& ~ r1("d11","d0")
& ~ r1("d10","d62")
& ~ r1("d10","d61")
& ~ r1("d10","d60")
& ~ r1("d10","d59")
& ~ r1("d10","d58")
& ~ r1("d10","d57")
& ~ r1("d10","d56")
& ~ r1("d10","d55")
& ~ r1("d10","d54")
& ~ r1("d10","d53")
& ~ r1("d10","d52")
& ~ r1("d10","d51")
& ~ r1("d10","d50")
& ~ r1("d10","d49")
& ~ r1("d10","d48")
& ~ r1("d10","d47")
& r1("d10","d46")
& r1("d10","d45")
& r1("d10","d44")
& r1("d10","d43")
& ~ r1("d10","d42")
& ~ r1("d10","d41")
& ~ r1("d10","d40")
& ~ r1("d10","d39")
& ~ r1("d10","d38")
& ~ r1("d10","d37")
& ~ r1("d10","d36")
& ~ r1("d10","d35")
& ~ r1("d10","d34")
& ~ r1("d10","d33")
& ~ r1("d10","d32")
& ~ r1("d10","d31")
& ~ r1("d10","d30")
& ~ r1("d10","d29")
& ~ r1("d10","d28")
& ~ r1("d10","d27")
& ~ r1("d10","d26")
& ~ r1("d10","d25")
& ~ r1("d10","d24")
& ~ r1("d10","d23")
& r1("d10","d22")
& r1("d10","d21")
& ~ r1("d10","d20")
& ~ r1("d10","d19")
& ~ r1("d10","d18")
& ~ r1("d10","d17")
& ~ r1("d10","d16")
& ~ r1("d10","d15")
& ~ r1("d10","d14")
& ~ r1("d10","d13")
& ~ r1("d10","d12")
& ~ r1("d10","d11")
& r1("d10","d10")
& ~ r1("d10","d9")
& ~ r1("d10","d8")
& ~ r1("d10","d7")
& ~ r1("d10","d6")
& ~ r1("d10","d5")
& ~ r1("d10","d4")
& ~ r1("d10","d3")
& ~ r1("d10","d2")
& ~ r1("d10","d1")
& ~ r1("d10","d0")
& ~ r1("d9","d62")
& ~ r1("d9","d61")
& ~ r1("d9","d60")
& ~ r1("d9","d59")
& ~ r1("d9","d58")
& ~ r1("d9","d57")
& ~ r1("d9","d56")
& ~ r1("d9","d55")
& ~ r1("d9","d54")
& ~ r1("d9","d53")
& ~ r1("d9","d52")
& ~ r1("d9","d51")
& ~ r1("d9","d50")
& ~ r1("d9","d49")
& ~ r1("d9","d48")
& ~ r1("d9","d47")
& ~ r1("d9","d46")
& ~ r1("d9","d45")
& ~ r1("d9","d44")
& ~ r1("d9","d43")
& r1("d9","d42")
& r1("d9","d41")
& r1("d9","d40")
& r1("d9","d39")
& ~ r1("d9","d38")
& ~ r1("d9","d37")
& ~ r1("d9","d36")
& ~ r1("d9","d35")
& ~ r1("d9","d34")
& ~ r1("d9","d33")
& ~ r1("d9","d32")
& ~ r1("d9","d31")
& ~ r1("d9","d30")
& ~ r1("d9","d29")
& ~ r1("d9","d28")
& ~ r1("d9","d27")
& ~ r1("d9","d26")
& ~ r1("d9","d25")
& ~ r1("d9","d24")
& ~ r1("d9","d23")
& ~ r1("d9","d22")
& ~ r1("d9","d21")
& r1("d9","d20")
& r1("d9","d19")
& ~ r1("d9","d18")
& ~ r1("d9","d17")
& ~ r1("d9","d16")
& ~ r1("d9","d15")
& ~ r1("d9","d14")
& ~ r1("d9","d13")
& ~ r1("d9","d12")
& ~ r1("d9","d11")
& ~ r1("d9","d10")
& r1("d9","d9")
& ~ r1("d9","d8")
& ~ r1("d9","d7")
& ~ r1("d9","d6")
& ~ r1("d9","d5")
& ~ r1("d9","d4")
& ~ r1("d9","d3")
& ~ r1("d9","d2")
& ~ r1("d9","d1")
& ~ r1("d9","d0")
& ~ r1("d8","d62")
& ~ r1("d8","d61")
& ~ r1("d8","d60")
& ~ r1("d8","d59")
& ~ r1("d8","d58")
& ~ r1("d8","d57")
& ~ r1("d8","d56")
& ~ r1("d8","d55")
& ~ r1("d8","d54")
& ~ r1("d8","d53")
& ~ r1("d8","d52")
& ~ r1("d8","d51")
& ~ r1("d8","d50")
& ~ r1("d8","d49")
& ~ r1("d8","d48")
& ~ r1("d8","d47")
& ~ r1("d8","d46")
& ~ r1("d8","d45")
& ~ r1("d8","d44")
& ~ r1("d8","d43")
& ~ r1("d8","d42")
& ~ r1("d8","d41")
& ~ r1("d8","d40")
& ~ r1("d8","d39")
& r1("d8","d38")
& r1("d8","d37")
& r1("d8","d36")
& r1("d8","d35")
& ~ r1("d8","d34")
& ~ r1("d8","d33")
& ~ r1("d8","d32")
& ~ r1("d8","d31")
& ~ r1("d8","d30")
& ~ r1("d8","d29")
& ~ r1("d8","d28")
& ~ r1("d8","d27")
& ~ r1("d8","d26")
& ~ r1("d8","d25")
& ~ r1("d8","d24")
& ~ r1("d8","d23")
& ~ r1("d8","d22")
& ~ r1("d8","d21")
& ~ r1("d8","d20")
& ~ r1("d8","d19")
& r1("d8","d18")
& r1("d8","d17")
& ~ r1("d8","d16")
& ~ r1("d8","d15")
& ~ r1("d8","d14")
& ~ r1("d8","d13")
& ~ r1("d8","d12")
& ~ r1("d8","d11")
& ~ r1("d8","d10")
& ~ r1("d8","d9")
& r1("d8","d8")
& ~ r1("d8","d7")
& ~ r1("d8","d6")
& ~ r1("d8","d5")
& ~ r1("d8","d4")
& ~ r1("d8","d3")
& ~ r1("d8","d2")
& ~ r1("d8","d1")
& ~ r1("d8","d0")
& ~ r1("d7","d62")
& ~ r1("d7","d61")
& ~ r1("d7","d60")
& ~ r1("d7","d59")
& ~ r1("d7","d58")
& ~ r1("d7","d57")
& ~ r1("d7","d56")
& ~ r1("d7","d55")
& ~ r1("d7","d54")
& ~ r1("d7","d53")
& ~ r1("d7","d52")
& ~ r1("d7","d51")
& ~ r1("d7","d50")
& ~ r1("d7","d49")
& ~ r1("d7","d48")
& ~ r1("d7","d47")
& ~ r1("d7","d46")
& ~ r1("d7","d45")
& ~ r1("d7","d44")
& ~ r1("d7","d43")
& ~ r1("d7","d42")
& ~ r1("d7","d41")
& ~ r1("d7","d40")
& ~ r1("d7","d39")
& ~ r1("d7","d38")
& ~ r1("d7","d37")
& ~ r1("d7","d36")
& ~ r1("d7","d35")
& r1("d7","d34")
& r1("d7","d33")
& r1("d7","d32")
& r1("d7","d31")
& ~ r1("d7","d30")
& ~ r1("d7","d29")
& ~ r1("d7","d28")
& ~ r1("d7","d27")
& ~ r1("d7","d26")
& ~ r1("d7","d25")
& ~ r1("d7","d24")
& ~ r1("d7","d23")
& ~ r1("d7","d22")
& ~ r1("d7","d21")
& ~ r1("d7","d20")
& ~ r1("d7","d19")
& ~ r1("d7","d18")
& ~ r1("d7","d17")
& r1("d7","d16")
& r1("d7","d15")
& ~ r1("d7","d14")
& ~ r1("d7","d13")
& ~ r1("d7","d12")
& ~ r1("d7","d11")
& ~ r1("d7","d10")
& ~ r1("d7","d9")
& ~ r1("d7","d8")
& r1("d7","d7")
& ~ r1("d7","d6")
& ~ r1("d7","d5")
& ~ r1("d7","d4")
& ~ r1("d7","d3")
& ~ r1("d7","d2")
& ~ r1("d7","d1")
& ~ r1("d7","d0")
& r1("d6","d62")
& r1("d6","d61")
& r1("d6","d60")
& r1("d6","d59")
& r1("d6","d58")
& r1("d6","d57")
& r1("d6","d56")
& r1("d6","d55")
& ~ r1("d6","d54")
& ~ r1("d6","d53")
& ~ r1("d6","d52")
& ~ r1("d6","d51")
& ~ r1("d6","d50")
& ~ r1("d6","d49")
& ~ r1("d6","d48")
& ~ r1("d6","d47")
& ~ r1("d6","d46")
& ~ r1("d6","d45")
& ~ r1("d6","d44")
& ~ r1("d6","d43")
& ~ r1("d6","d42")
& ~ r1("d6","d41")
& ~ r1("d6","d40")
& ~ r1("d6","d39")
& ~ r1("d6","d38")
& ~ r1("d6","d37")
& ~ r1("d6","d36")
& ~ r1("d6","d35")
& ~ r1("d6","d34")
& ~ r1("d6","d33")
& ~ r1("d6","d32")
& ~ r1("d6","d31")
& r1("d6","d30")
& r1("d6","d29")
& r1("d6","d28")
& r1("d6","d27")
& ~ r1("d6","d26")
& ~ r1("d6","d25")
& ~ r1("d6","d24")
& ~ r1("d6","d23")
& ~ r1("d6","d22")
& ~ r1("d6","d21")
& ~ r1("d6","d20")
& ~ r1("d6","d19")
& ~ r1("d6","d18")
& ~ r1("d6","d17")
& ~ r1("d6","d16")
& ~ r1("d6","d15")
& r1("d6","d14")
& r1("d6","d13")
& ~ r1("d6","d12")
& ~ r1("d6","d11")
& ~ r1("d6","d10")
& ~ r1("d6","d9")
& ~ r1("d6","d8")
& ~ r1("d6","d7")
& r1("d6","d6")
& ~ r1("d6","d5")
& ~ r1("d6","d4")
& ~ r1("d6","d3")
& ~ r1("d6","d2")
& ~ r1("d6","d1")
& ~ r1("d6","d0")
& ~ r1("d5","d62")
& ~ r1("d5","d61")
& ~ r1("d5","d60")
& ~ r1("d5","d59")
& ~ r1("d5","d58")
& ~ r1("d5","d57")
& ~ r1("d5","d56")
& ~ r1("d5","d55")
& r1("d5","d54")
& r1("d5","d53")
& r1("d5","d52")
& r1("d5","d51")
& r1("d5","d50")
& r1("d5","d49")
& r1("d5","d48")
& r1("d5","d47")
& ~ r1("d5","d46")
& ~ r1("d5","d45")
& ~ r1("d5","d44")
& ~ r1("d5","d43")
& ~ r1("d5","d42")
& ~ r1("d5","d41")
& ~ r1("d5","d40")
& ~ r1("d5","d39")
& ~ r1("d5","d38")
& ~ r1("d5","d37")
& ~ r1("d5","d36")
& ~ r1("d5","d35")
& ~ r1("d5","d34")
& ~ r1("d5","d33")
& ~ r1("d5","d32")
& ~ r1("d5","d31")
& ~ r1("d5","d30")
& ~ r1("d5","d29")
& ~ r1("d5","d28")
& ~ r1("d5","d27")
& r1("d5","d26")
& r1("d5","d25")
& r1("d5","d24")
& r1("d5","d23")
& ~ r1("d5","d22")
& ~ r1("d5","d21")
& ~ r1("d5","d20")
& ~ r1("d5","d19")
& ~ r1("d5","d18")
& ~ r1("d5","d17")
& ~ r1("d5","d16")
& ~ r1("d5","d15")
& ~ r1("d5","d14")
& ~ r1("d5","d13")
& r1("d5","d12")
& r1("d5","d11")
& ~ r1("d5","d10")
& ~ r1("d5","d9")
& ~ r1("d5","d8")
& ~ r1("d5","d7")
& ~ r1("d5","d6")
& r1("d5","d5")
& ~ r1("d5","d4")
& ~ r1("d5","d3")
& ~ r1("d5","d2")
& ~ r1("d5","d1")
& ~ r1("d5","d0")
& ~ r1("d4","d62")
& ~ r1("d4","d61")
& ~ r1("d4","d60")
& ~ r1("d4","d59")
& ~ r1("d4","d58")
& ~ r1("d4","d57")
& ~ r1("d4","d56")
& ~ r1("d4","d55")
& ~ r1("d4","d54")
& ~ r1("d4","d53")
& ~ r1("d4","d52")
& ~ r1("d4","d51")
& ~ r1("d4","d50")
& ~ r1("d4","d49")
& ~ r1("d4","d48")
& ~ r1("d4","d47")
& r1("d4","d46")
& r1("d4","d45")
& r1("d4","d44")
& r1("d4","d43")
& r1("d4","d42")
& r1("d4","d41")
& r1("d4","d40")
& r1("d4","d39")
& ~ r1("d4","d38")
& ~ r1("d4","d37")
& ~ r1("d4","d36")
& ~ r1("d4","d35")
& ~ r1("d4","d34")
& ~ r1("d4","d33")
& ~ r1("d4","d32")
& ~ r1("d4","d31")
& ~ r1("d4","d30")
& ~ r1("d4","d29")
& ~ r1("d4","d28")
& ~ r1("d4","d27")
& ~ r1("d4","d26")
& ~ r1("d4","d25")
& ~ r1("d4","d24")
& ~ r1("d4","d23")
& r1("d4","d22")
& r1("d4","d21")
& r1("d4","d20")
& r1("d4","d19")
& ~ r1("d4","d18")
& ~ r1("d4","d17")
& ~ r1("d4","d16")
& ~ r1("d4","d15")
& ~ r1("d4","d14")
& ~ r1("d4","d13")
& ~ r1("d4","d12")
& ~ r1("d4","d11")
& r1("d4","d10")
& r1("d4","d9")
& ~ r1("d4","d8")
& ~ r1("d4","d7")
& ~ r1("d4","d6")
& ~ r1("d4","d5")
& r1("d4","d4")
& ~ r1("d4","d3")
& ~ r1("d4","d2")
& ~ r1("d4","d1")
& ~ r1("d4","d0")
& ~ r1("d3","d62")
& ~ r1("d3","d61")
& ~ r1("d3","d60")
& ~ r1("d3","d59")
& ~ r1("d3","d58")
& ~ r1("d3","d57")
& ~ r1("d3","d56")
& ~ r1("d3","d55")
& ~ r1("d3","d54")
& ~ r1("d3","d53")
& ~ r1("d3","d52")
& ~ r1("d3","d51")
& ~ r1("d3","d50")
& ~ r1("d3","d49")
& ~ r1("d3","d48")
& ~ r1("d3","d47")
& ~ r1("d3","d46")
& ~ r1("d3","d45")
& ~ r1("d3","d44")
& ~ r1("d3","d43")
& ~ r1("d3","d42")
& ~ r1("d3","d41")
& ~ r1("d3","d40")
& ~ r1("d3","d39")
& r1("d3","d38")
& r1("d3","d37")
& r1("d3","d36")
& r1("d3","d35")
& r1("d3","d34")
& r1("d3","d33")
& r1("d3","d32")
& r1("d3","d31")
& ~ r1("d3","d30")
& ~ r1("d3","d29")
& ~ r1("d3","d28")
& ~ r1("d3","d27")
& ~ r1("d3","d26")
& ~ r1("d3","d25")
& ~ r1("d3","d24")
& ~ r1("d3","d23")
& ~ r1("d3","d22")
& ~ r1("d3","d21")
& ~ r1("d3","d20")
& ~ r1("d3","d19")
& r1("d3","d18")
& r1("d3","d17")
& r1("d3","d16")
& r1("d3","d15")
& ~ r1("d3","d14")
& ~ r1("d3","d13")
& ~ r1("d3","d12")
& ~ r1("d3","d11")
& ~ r1("d3","d10")
& ~ r1("d3","d9")
& r1("d3","d8")
& r1("d3","d7")
& ~ r1("d3","d6")
& ~ r1("d3","d5")
& ~ r1("d3","d4")
& r1("d3","d3")
& ~ r1("d3","d2")
& ~ r1("d3","d1")
& ~ r1("d3","d0")
& r1("d2","d62")
& r1("d2","d61")
& r1("d2","d60")
& r1("d2","d59")
& r1("d2","d58")
& r1("d2","d57")
& r1("d2","d56")
& r1("d2","d55")
& r1("d2","d54")
& r1("d2","d53")
& r1("d2","d52")
& r1("d2","d51")
& r1("d2","d50")
& r1("d2","d49")
& r1("d2","d48")
& r1("d2","d47")
& ~ r1("d2","d46")
& ~ r1("d2","d45")
& ~ r1("d2","d44")
& ~ r1("d2","d43")
& ~ r1("d2","d42")
& ~ r1("d2","d41")
& ~ r1("d2","d40")
& ~ r1("d2","d39")
& ~ r1("d2","d38")
& ~ r1("d2","d37")
& ~ r1("d2","d36")
& ~ r1("d2","d35")
& ~ r1("d2","d34")
& ~ r1("d2","d33")
& ~ r1("d2","d32")
& ~ r1("d2","d31")
& r1("d2","d30")
& r1("d2","d29")
& r1("d2","d28")
& r1("d2","d27")
& r1("d2","d26")
& r1("d2","d25")
& r1("d2","d24")
& r1("d2","d23")
& ~ r1("d2","d22")
& ~ r1("d2","d21")
& ~ r1("d2","d20")
& ~ r1("d2","d19")
& ~ r1("d2","d18")
& ~ r1("d2","d17")
& ~ r1("d2","d16")
& ~ r1("d2","d15")
& r1("d2","d14")
& r1("d2","d13")
& r1("d2","d12")
& r1("d2","d11")
& ~ r1("d2","d10")
& ~ r1("d2","d9")
& ~ r1("d2","d8")
& ~ r1("d2","d7")
& r1("d2","d6")
& r1("d2","d5")
& ~ r1("d2","d4")
& ~ r1("d2","d3")
& r1("d2","d2")
& ~ r1("d2","d1")
& ~ r1("d2","d0")
& ~ r1("d1","d62")
& ~ r1("d1","d61")
& ~ r1("d1","d60")
& ~ r1("d1","d59")
& ~ r1("d1","d58")
& ~ r1("d1","d57")
& ~ r1("d1","d56")
& ~ r1("d1","d55")
& ~ r1("d1","d54")
& ~ r1("d1","d53")
& ~ r1("d1","d52")
& ~ r1("d1","d51")
& ~ r1("d1","d50")
& ~ r1("d1","d49")
& ~ r1("d1","d48")
& ~ r1("d1","d47")
& r1("d1","d46")
& r1("d1","d45")
& r1("d1","d44")
& r1("d1","d43")
& r1("d1","d42")
& r1("d1","d41")
& r1("d1","d40")
& r1("d1","d39")
& r1("d1","d38")
& r1("d1","d37")
& r1("d1","d36")
& r1("d1","d35")
& r1("d1","d34")
& r1("d1","d33")
& r1("d1","d32")
& r1("d1","d31")
& ~ r1("d1","d30")
& ~ r1("d1","d29")
& ~ r1("d1","d28")
& ~ r1("d1","d27")
& ~ r1("d1","d26")
& ~ r1("d1","d25")
& ~ r1("d1","d24")
& ~ r1("d1","d23")
& r1("d1","d22")
& r1("d1","d21")
& r1("d1","d20")
& r1("d1","d19")
& r1("d1","d18")
& r1("d1","d17")
& r1("d1","d16")
& r1("d1","d15")
& ~ r1("d1","d14")
& ~ r1("d1","d13")
& ~ r1("d1","d12")
& ~ r1("d1","d11")
& r1("d1","d10")
& r1("d1","d9")
& r1("d1","d8")
& r1("d1","d7")
& ~ r1("d1","d6")
& ~ r1("d1","d5")
& r1("d1","d4")
& r1("d1","d3")
& ~ r1("d1","d2")
& r1("d1","d1")
& ~ r1("d1","d0")
& r1("d0","d62")
& r1("d0","d61")
& r1("d0","d60")
& r1("d0","d59")
& r1("d0","d58")
& r1("d0","d57")
& r1("d0","d56")
& r1("d0","d55")
& r1("d0","d54")
& r1("d0","d53")
& r1("d0","d52")
& r1("d0","d51")
& r1("d0","d50")
& r1("d0","d49")
& r1("d0","d48")
& r1("d0","d47")
& r1("d0","d46")
& r1("d0","d45")
& r1("d0","d44")
& r1("d0","d43")
& r1("d0","d42")
& r1("d0","d41")
& r1("d0","d40")
& r1("d0","d39")
& r1("d0","d38")
& r1("d0","d37")
& r1("d0","d36")
& r1("d0","d35")
& r1("d0","d34")
& r1("d0","d33")
& r1("d0","d32")
& r1("d0","d31")
& r1("d0","d30")
& r1("d0","d29")
& r1("d0","d28")
& r1("d0","d27")
& r1("d0","d26")
& r1("d0","d25")
& r1("d0","d24")
& r1("d0","d23")
& r1("d0","d22")
& r1("d0","d21")
& r1("d0","d20")
& r1("d0","d19")
& r1("d0","d18")
& r1("d0","d17")
& r1("d0","d16")
& r1("d0","d15")
& r1("d0","d14")
& r1("d0","d13")
& r1("d0","d12")
& r1("d0","d11")
& r1("d0","d10")
& r1("d0","d9")
& r1("d0","d8")
& r1("d0","d7")
& r1("d0","d6")
& r1("d0","d5")
& r1("d0","d4")
& r1("d0","d3")
& r1("d0","d2")
& r1("d0","d1")
& r1("d0","d0")
& p6("d62")
& ~ p6("d61")
& p6("d60")
& ~ p6("d59")
& p6("d58")
& ~ p6("d57")
& p6("d56")
& ~ p6("d55")
& p6("d54")
& ~ p6("d53")
& p6("d52")
& ~ p6("d51")
& p6("d50")
& ~ p6("d49")
& p6("d48")
& ~ p6("d47")
& p6("d46")
& ~ p6("d45")
& p6("d44")
& ~ p6("d43")
& p6("d42")
& ~ p6("d41")
& p6("d40")
& ~ p6("d39")
& p6("d38")
& ~ p6("d37")
& p6("d36")
& ~ p6("d35")
& p6("d34")
& ~ p6("d33")
& p6("d32")
& ~ p6("d31")
& ~ p6("d30")
& ~ p6("d29")
& ~ p6("d28")
& ~ p6("d27")
& ~ p6("d26")
& ~ p6("d25")
& ~ p6("d24")
& ~ p6("d23")
& ~ p6("d22")
& ~ p6("d21")
& ~ p6("d20")
& ~ p6("d19")
& ~ p6("d18")
& ~ p6("d17")
& ~ p6("d16")
& ~ p6("d15")
& ~ p6("d14")
& ~ p6("d13")
& ~ p6("d12")
& ~ p6("d11")
& ~ p6("d10")
& ~ p6("d9")
& ~ p6("d8")
& ~ p6("d7")
& ~ p6("d6")
& ~ p6("d5")
& ~ p6("d4")
& ~ p6("d3")
& ~ p6("d2")
& ~ p6("d1")
& ~ p6("d0")
& p5("d62")
& p5("d61")
& ~ p5("d60")
& ~ p5("d59")
& p5("d58")
& p5("d57")
& ~ p5("d56")
& ~ p5("d55")
& p5("d54")
& p5("d53")
& ~ p5("d52")
& ~ p5("d51")
& p5("d50")
& p5("d49")
& ~ p5("d48")
& ~ p5("d47")
& p5("d46")
& p5("d45")
& ~ p5("d44")
& ~ p5("d43")
& p5("d42")
& p5("d41")
& ~ p5("d40")
& ~ p5("d39")
& p5("d38")
& p5("d37")
& ~ p5("d36")
& ~ p5("d35")
& p5("d34")
& p5("d33")
& ~ p5("d32")
& ~ p5("d31")
& p5("d30")
& ~ p5("d29")
& p5("d28")
& ~ p5("d27")
& p5("d26")
& ~ p5("d25")
& p5("d24")
& ~ p5("d23")
& p5("d22")
& ~ p5("d21")
& p5("d20")
& ~ p5("d19")
& p5("d18")
& ~ p5("d17")
& p5("d16")
& ~ p5("d15")
& ~ p5("d14")
& ~ p5("d13")
& ~ p5("d12")
& ~ p5("d11")
& ~ p5("d10")
& ~ p5("d9")
& ~ p5("d8")
& ~ p5("d7")
& ~ p5("d6")
& ~ p5("d5")
& ~ p5("d4")
& ~ p5("d3")
& ~ p5("d2")
& ~ p5("d1")
& ~ p5("d0")
& p4("d62")
& p4("d61")
& p4("d60")
& p4("d59")
& ~ p4("d58")
& ~ p4("d57")
& ~ p4("d56")
& ~ p4("d55")
& p4("d54")
& p4("d53")
& p4("d52")
& p4("d51")
& ~ p4("d50")
& ~ p4("d49")
& ~ p4("d48")
& ~ p4("d47")
& p4("d46")
& p4("d45")
& p4("d44")
& p4("d43")
& ~ p4("d42")
& ~ p4("d41")
& ~ p4("d40")
& ~ p4("d39")
& p4("d38")
& p4("d37")
& p4("d36")
& p4("d35")
& ~ p4("d34")
& ~ p4("d33")
& ~ p4("d32")
& ~ p4("d31")
& p4("d30")
& p4("d29")
& ~ p4("d28")
& ~ p4("d27")
& p4("d26")
& p4("d25")
& ~ p4("d24")
& ~ p4("d23")
& p4("d22")
& p4("d21")
& ~ p4("d20")
& ~ p4("d19")
& p4("d18")
& p4("d17")
& ~ p4("d16")
& ~ p4("d15")
& p4("d14")
& ~ p4("d13")
& p4("d12")
& ~ p4("d11")
& p4("d10")
& ~ p4("d9")
& p4("d8")
& ~ p4("d7")
& ~ p4("d6")
& ~ p4("d5")
& ~ p4("d4")
& ~ p4("d3")
& ~ p4("d2")
& ~ p4("d1")
& ~ p4("d0")
& p3("d62")
& p3("d61")
& p3("d60")
& p3("d59")
& p3("d58")
& p3("d57")
& p3("d56")
& p3("d55")
& ~ p3("d54")
& ~ p3("d53")
& ~ p3("d52")
& ~ p3("d51")
& ~ p3("d50")
& ~ p3("d49")
& ~ p3("d48")
& ~ p3("d47")
& p3("d46")
& p3("d45")
& p3("d44")
& p3("d43")
& p3("d42")
& p3("d41")
& p3("d40")
& p3("d39")
& ~ p3("d38")
& ~ p3("d37")
& ~ p3("d36")
& ~ p3("d35")
& ~ p3("d34")
& ~ p3("d33")
& ~ p3("d32")
& ~ p3("d31")
& p3("d30")
& p3("d29")
& p3("d28")
& p3("d27")
& ~ p3("d26")
& ~ p3("d25")
& ~ p3("d24")
& ~ p3("d23")
& p3("d22")
& p3("d21")
& p3("d20")
& p3("d19")
& ~ p3("d18")
& ~ p3("d17")
& ~ p3("d16")
& ~ p3("d15")
& p3("d14")
& p3("d13")
& ~ p3("d12")
& ~ p3("d11")
& p3("d10")
& p3("d9")
& ~ p3("d8")
& ~ p3("d7")
& p3("d6")
& ~ p3("d5")
& p3("d4")
& ~ p3("d3")
& ~ p3("d2")
& ~ p3("d1")
& ~ p3("d0")
& p2("d62")
& p2("d61")
& p2("d60")
& p2("d59")
& p2("d58")
& p2("d57")
& p2("d56")
& p2("d55")
& p2("d54")
& p2("d53")
& p2("d52")
& p2("d51")
& p2("d50")
& p2("d49")
& p2("d48")
& p2("d47")
& ~ p2("d46")
& ~ p2("d45")
& ~ p2("d44")
& ~ p2("d43")
& ~ p2("d42")
& ~ p2("d41")
& ~ p2("d40")
& ~ p2("d39")
& ~ p2("d38")
& ~ p2("d37")
& ~ p2("d36")
& ~ p2("d35")
& ~ p2("d34")
& ~ p2("d33")
& ~ p2("d32")
& ~ p2("d31")
& p2("d30")
& p2("d29")
& p2("d28")
& p2("d27")
& p2("d26")
& p2("d25")
& p2("d24")
& p2("d23")
& ~ p2("d22")
& ~ p2("d21")
& ~ p2("d20")
& ~ p2("d19")
& ~ p2("d18")
& ~ p2("d17")
& ~ p2("d16")
& ~ p2("d15")
& p2("d14")
& p2("d13")
& p2("d12")
& p2("d11")
& ~ p2("d10")
& ~ p2("d9")
& ~ p2("d8")
& ~ p2("d7")
& p2("d6")
& p2("d5")
& ~ p2("d4")
& ~ p2("d3")
& p2("d2")
& ~ p2("d1")
& ~ p2("d0")
& ~ p106("d62")
& ~ p106("d61")
& ~ p106("d60")
& ~ p106("d59")
& ~ p106("d58")
& ~ p106("d57")
& ~ p106("d56")
& ~ p106("d55")
& ~ p106("d54")
& ~ p106("d53")
& ~ p106("d52")
& ~ p106("d51")
& ~ p106("d50")
& ~ p106("d49")
& ~ p106("d48")
& ~ p106("d47")
& ~ p106("d46")
& ~ p106("d45")
& ~ p106("d44")
& ~ p106("d43")
& ~ p106("d42")
& ~ p106("d41")
& ~ p106("d40")
& ~ p106("d39")
& ~ p106("d38")
& ~ p106("d37")
& ~ p106("d36")
& ~ p106("d35")
& ~ p106("d34")
& ~ p106("d33")
& ~ p106("d32")
& ~ p106("d31")
& ~ p106("d30")
& ~ p106("d29")
& ~ p106("d28")
& ~ p106("d27")
& ~ p106("d26")
& ~ p106("d25")
& ~ p106("d24")
& ~ p106("d23")
& ~ p106("d22")
& ~ p106("d21")
& ~ p106("d20")
& ~ p106("d19")
& ~ p106("d18")
& ~ p106("d17")
& ~ p106("d16")
& ~ p106("d15")
& ~ p106("d14")
& ~ p106("d13")
& ~ p106("d12")
& ~ p106("d11")
& ~ p106("d10")
& ~ p106("d9")
& ~ p106("d8")
& ~ p106("d7")
& ~ p106("d6")
& ~ p106("d5")
& ~ p106("d4")
& ~ p106("d3")
& ~ p106("d2")
& ~ p106("d1")
& ~ p106("d0")
& p105("d62")
& p105("d61")
& p105("d60")
& p105("d59")
& p105("d58")
& p105("d57")
& p105("d56")
& p105("d55")
& p105("d54")
& p105("d53")
& p105("d52")
& p105("d51")
& p105("d50")
& p105("d49")
& p105("d48")
& p105("d47")
& p105("d46")
& p105("d45")
& p105("d44")
& p105("d43")
& p105("d42")
& p105("d41")
& p105("d40")
& p105("d39")
& p105("d38")
& p105("d37")
& p105("d36")
& p105("d35")
& p105("d34")
& p105("d33")
& p105("d32")
& p105("d31")
& ~ p105("d30")
& ~ p105("d29")
& ~ p105("d28")
& ~ p105("d27")
& ~ p105("d26")
& ~ p105("d25")
& ~ p105("d24")
& ~ p105("d23")
& ~ p105("d22")
& ~ p105("d21")
& ~ p105("d20")
& ~ p105("d19")
& ~ p105("d18")
& ~ p105("d17")
& ~ p105("d16")
& ~ p105("d15")
& ~ p105("d14")
& ~ p105("d13")
& ~ p105("d12")
& ~ p105("d11")
& ~ p105("d10")
& ~ p105("d9")
& ~ p105("d8")
& ~ p105("d7")
& ~ p105("d6")
& ~ p105("d5")
& ~ p105("d4")
& ~ p105("d3")
& ~ p105("d2")
& ~ p105("d1")
& ~ p105("d0")
& p104("d62")
& p104("d61")
& p104("d60")
& p104("d59")
& p104("d58")
& p104("d57")
& p104("d56")
& p104("d55")
& p104("d54")
& p104("d53")
& p104("d52")
& p104("d51")
& p104("d50")
& p104("d49")
& p104("d48")
& p104("d47")
& p104("d46")
& p104("d45")
& p104("d44")
& p104("d43")
& p104("d42")
& p104("d41")
& p104("d40")
& p104("d39")
& p104("d38")
& p104("d37")
& p104("d36")
& p104("d35")
& p104("d34")
& p104("d33")
& p104("d32")
& p104("d31")
& p104("d30")
& p104("d29")
& p104("d28")
& p104("d27")
& p104("d26")
& p104("d25")
& p104("d24")
& p104("d23")
& p104("d22")
& p104("d21")
& p104("d20")
& p104("d19")
& p104("d18")
& p104("d17")
& p104("d16")
& p104("d15")
& ~ p104("d14")
& ~ p104("d13")
& ~ p104("d12")
& ~ p104("d11")
& ~ p104("d10")
& ~ p104("d9")
& ~ p104("d8")
& ~ p104("d7")
& ~ p104("d6")
& ~ p104("d5")
& ~ p104("d4")
& ~ p104("d3")
& ~ p104("d2")
& ~ p104("d1")
& ~ p104("d0")
& p103("d62")
& p103("d61")
& p103("d60")
& p103("d59")
& p103("d58")
& p103("d57")
& p103("d56")
& p103("d55")
& p103("d54")
& p103("d53")
& p103("d52")
& p103("d51")
& p103("d50")
& p103("d49")
& p103("d48")
& p103("d47")
& p103("d46")
& p103("d45")
& p103("d44")
& p103("d43")
& p103("d42")
& p103("d41")
& p103("d40")
& p103("d39")
& p103("d38")
& p103("d37")
& p103("d36")
& p103("d35")
& p103("d34")
& p103("d33")
& p103("d32")
& p103("d31")
& p103("d30")
& p103("d29")
& p103("d28")
& p103("d27")
& p103("d26")
& p103("d25")
& p103("d24")
& p103("d23")
& p103("d22")
& p103("d21")
& p103("d20")
& p103("d19")
& p103("d18")
& p103("d17")
& p103("d16")
& p103("d15")
& p103("d14")
& p103("d13")
& p103("d12")
& p103("d11")
& p103("d10")
& p103("d9")
& p103("d8")
& p103("d7")
& ~ p103("d6")
& ~ p103("d5")
& ~ p103("d4")
& ~ p103("d3")
& ~ p103("d2")
& ~ p103("d1")
& ~ p103("d0")
& p102("d62")
& p102("d61")
& p102("d60")
& p102("d59")
& p102("d58")
& p102("d57")
& p102("d56")
& p102("d55")
& p102("d54")
& p102("d53")
& p102("d52")
& p102("d51")
& p102("d50")
& p102("d49")
& p102("d48")
& p102("d47")
& p102("d46")
& p102("d45")
& p102("d44")
& p102("d43")
& p102("d42")
& p102("d41")
& p102("d40")
& p102("d39")
& p102("d38")
& p102("d37")
& p102("d36")
& p102("d35")
& p102("d34")
& p102("d33")
& p102("d32")
& p102("d31")
& p102("d30")
& p102("d29")
& p102("d28")
& p102("d27")
& p102("d26")
& p102("d25")
& p102("d24")
& p102("d23")
& p102("d22")
& p102("d21")
& p102("d20")
& p102("d19")
& p102("d18")
& p102("d17")
& p102("d16")
& p102("d15")
& p102("d14")
& p102("d13")
& p102("d12")
& p102("d11")
& p102("d10")
& p102("d9")
& p102("d8")
& p102("d7")
& p102("d6")
& p102("d5")
& p102("d4")
& p102("d3")
& ~ p102("d2")
& ~ p102("d1")
& ~ p102("d0")
& p101("d62")
& p101("d61")
& p101("d60")
& p101("d59")
& p101("d58")
& p101("d57")
& p101("d56")
& p101("d55")
& p101("d54")
& p101("d53")
& p101("d52")
& p101("d51")
& p101("d50")
& p101("d49")
& p101("d48")
& p101("d47")
& p101("d46")
& p101("d45")
& p101("d44")
& p101("d43")
& p101("d42")
& p101("d41")
& p101("d40")
& p101("d39")
& p101("d38")
& p101("d37")
& p101("d36")
& p101("d35")
& p101("d34")
& p101("d33")
& p101("d32")
& p101("d31")
& p101("d30")
& p101("d29")
& p101("d28")
& p101("d27")
& p101("d26")
& p101("d25")
& p101("d24")
& p101("d23")
& p101("d22")
& p101("d21")
& p101("d20")
& p101("d19")
& p101("d18")
& p101("d17")
& p101("d16")
& p101("d15")
& p101("d14")
& p101("d13")
& p101("d12")
& p101("d11")
& p101("d10")
& p101("d9")
& p101("d8")
& p101("d7")
& p101("d6")
& p101("d5")
& p101("d4")
& p101("d3")
& p101("d2")
& p101("d1")
& ~ p101("d0")
& p100("d62")
& p100("d61")
& p100("d60")
& p100("d59")
& p100("d58")
& p100("d57")
& p100("d56")
& p100("d55")
& p100("d54")
& p100("d53")
& p100("d52")
& p100("d51")
& p100("d50")
& p100("d49")
& p100("d48")
& p100("d47")
& p100("d46")
& p100("d45")
& p100("d44")
& p100("d43")
& p100("d42")
& p100("d41")
& p100("d40")
& p100("d39")
& p100("d38")
& p100("d37")
& p100("d36")
& p100("d35")
& p100("d34")
& p100("d33")
& p100("d32")
& p100("d31")
& p100("d30")
& p100("d29")
& p100("d28")
& p100("d27")
& p100("d26")
& p100("d25")
& p100("d24")
& p100("d23")
& p100("d22")
& p100("d21")
& p100("d20")
& p100("d19")
& p100("d18")
& p100("d17")
& p100("d16")
& p100("d15")
& p100("d14")
& p100("d13")
& p100("d12")
& p100("d11")
& p100("d10")
& p100("d9")
& p100("d8")
& p100("d7")
& p100("d6")
& p100("d5")
& p100("d4")
& p100("d3")
& p100("d2")
& p100("d1")
& p100("d0")
& ~ p1("d62")
& ~ p1("d61")
& ~ p1("d60")
& ~ p1("d59")
& ~ p1("d58")
& ~ p1("d57")
& ~ p1("d56")
& ~ p1("d55")
& ~ p1("d54")
& ~ p1("d53")
& ~ p1("d52")
& ~ p1("d51")
& ~ p1("d50")
& ~ p1("d49")
& ~ p1("d48")
& ~ p1("d47")
& ~ p1("d46")
& ~ p1("d45")
& ~ p1("d44")
& ~ p1("d43")
& ~ p1("d42")
& ~ p1("d41")
& ~ p1("d40")
& ~ p1("d39")
& ~ p1("d38")
& ~ p1("d37")
& ~ p1("d36")
& ~ p1("d35")
& ~ p1("d34")
& ~ p1("d33")
& ~ p1("d32")
& ~ p1("d31")
& ~ p1("d30")
& ~ p1("d29")
& ~ p1("d28")
& ~ p1("d27")
& ~ p1("d26")
& ~ p1("d25")
& ~ p1("d24")
& ~ p1("d23")
& ~ p1("d22")
& ~ p1("d21")
& ~ p1("d20")
& ~ p1("d19")
& ~ p1("d18")
& ~ p1("d17")
& ~ p1("d16")
& ~ p1("d15")
& ~ p1("d14")
& ~ p1("d13")
& ~ p1("d12")
& ~ p1("d11")
& ~ p1("d10")
& ~ p1("d9")
& ~ p1("d8")
& ~ p1("d7")
& ~ p1("d6")
& ~ p1("d5")
& ~ p1("d4")
& ~ p1("d3")
& ~ p1("d2")
& ~ p1("d1")
& ~ p1("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL675+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 23:20:26 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 312060 was started by sandbox2 on n001,
% 0.09/0.38 % Fri Sep 25 23:20:26 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox2/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 17.96/3.13
% 17.96/3.13 % SZS status CounterSatisfiable for theBenchmark
% 17.96/3.13 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------