%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN490+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 02:51:54 EDT 2022
% Result : CounterSatisfiable 1.84s 2.21s
% Output : Saturation 1.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN490+1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Mon Jul 11 22:12:12 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.82/1.20 *** allocated 10000 integers for termspace/termends
% 0.82/1.20 *** allocated 10000 integers for clauses
% 0.82/1.20 *** allocated 10000 integers for justifications
% 0.82/1.20 Bliksem 1.12
% 0.82/1.20
% 0.82/1.20
% 0.82/1.20 Automatic Strategy Selection
% 0.82/1.20
% 0.82/1.20
% 0.82/1.20 Clauses:
% 0.82/1.20
% 0.82/1.20 { alpha15 }.
% 0.82/1.20 { ! hskp13, alpha26 }.
% 0.82/1.20 { ! hskp13, c2_1( a15 ) }.
% 0.82/1.20 { hskp7, hskp0, hskp8 }.
% 0.82/1.20 { ! ndr1_0, ! c1_1( X ), c0_1( X ), ! c2_1( X ), hskp1, ! ndr1_0, ! c2_1( Y
% 0.82/1.20 ), c1_1( Y ), c3_1( Y ) }.
% 0.82/1.20 { ! ndr1_0, ! c3_1( X ), ! c2_1( X ), c1_1( X ), hskp2, hskp9 }.
% 0.82/1.20 { hskp10, hskp3, hskp11 }.
% 0.82/1.20 { ! ndr1_0, ! c3_1( X ), ! c1_1( X ), ! c2_1( X ), hskp12, ! ndr1_0, c2_1(
% 0.82/1.20 Y ), ! c3_1( Y ), c0_1( Y ) }.
% 0.82/1.20 { hskp4, ! ndr1_0, ! c0_1( X ), ! c1_1( X ), c2_1( X ), ! ndr1_0, ! c0_1( Y
% 0.82/1.20 ), c1_1( Y ), ! c3_1( Y ) }.
% 0.82/1.20 { hskp5, ! ndr1_0, c2_1( X ), c0_1( X ), c1_1( X ), hskp3 }.
% 0.82/1.20 { ! ndr1_0, c0_1( X ), c2_1( X ), c3_1( X ), hskp6, hskp13 }.
% 0.82/1.20 { ! alpha26, ndr1_0 }.
% 0.82/1.20 { ! alpha26, c3_1( a15 ) }.
% 0.82/1.20 { ! alpha26, c1_1( a15 ) }.
% 0.82/1.20 { ! ndr1_0, ! c3_1( a15 ), ! c1_1( a15 ), alpha26 }.
% 0.82/1.20 { ! alpha15, alpha8 }.
% 0.82/1.20 { ! alpha15, alpha27 }.
% 0.82/1.20 { ! alpha8, ! alpha27, alpha15 }.
% 0.82/1.20 { ! alpha27, ! hskp12, alpha39 }.
% 0.82/1.20 { hskp12, alpha27 }.
% 0.82/1.20 { ! alpha39, alpha27 }.
% 0.82/1.20 { ! alpha39, alpha48 }.
% 0.82/1.20 { ! alpha39, c3_1( a10 ) }.
% 0.82/1.20 { ! alpha48, ! c3_1( a10 ), alpha39 }.
% 0.82/1.20 { ! alpha48, ndr1_0 }.
% 0.82/1.20 { ! alpha48, ! c1_1( a10 ) }.
% 0.82/1.20 { ! alpha48, ! c2_1( a10 ) }.
% 0.82/1.20 { ! ndr1_0, c1_1( a10 ), c2_1( a10 ), alpha48 }.
% 0.82/1.20 { ! alpha8, alpha16 }.
% 0.82/1.20 { ! alpha8, alpha28 }.
% 0.82/1.20 { ! alpha16, ! alpha28, alpha8 }.
% 0.82/1.20 { ! alpha28, ! hskp11, alpha40 }.
% 0.82/1.20 { hskp11, alpha28 }.
% 0.82/1.20 { ! alpha40, alpha28 }.
% 0.82/1.20 { ! alpha40, alpha49 }.
% 0.82/1.20 { ! alpha40, c3_1( a9 ) }.
% 0.82/1.20 { ! alpha49, ! c3_1( a9 ), alpha40 }.
% 0.82/1.20 { ! alpha49, ndr1_0 }.
% 0.82/1.20 { ! alpha49, c1_1( a9 ) }.
% 0.82/1.20 { ! alpha49, c2_1( a9 ) }.
% 0.82/1.20 { ! ndr1_0, ! c1_1( a9 ), ! c2_1( a9 ), alpha49 }.
% 0.82/1.20 { ! alpha16, alpha4 }.
% 0.82/1.20 { ! alpha16, alpha29 }.
% 0.82/1.20 { ! alpha4, ! alpha29, alpha16 }.
% 0.82/1.20 { ! alpha29, ! hskp10, alpha41 }.
% 0.82/1.20 { hskp10, alpha29 }.
% 0.82/1.20 { ! alpha41, alpha29 }.
% 0.82/1.20 { ! alpha41, alpha50 }.
% 0.82/1.20 { ! alpha41, c3_1( a7 ) }.
% 0.82/1.20 { ! alpha50, ! c3_1( a7 ), alpha41 }.
% 0.82/1.20 { ! alpha50, ndr1_0 }.
% 0.82/1.20 { ! alpha50, ! c2_1( a7 ) }.
% 0.82/1.20 { ! alpha50, ! c1_1( a7 ) }.
% 0.82/1.20 { ! ndr1_0, c2_1( a7 ), c1_1( a7 ), alpha50 }.
% 0.82/1.20 { ! alpha4, alpha9 }.
% 0.82/1.20 { ! alpha4, alpha17 }.
% 0.82/1.20 { ! alpha9, ! alpha17, alpha4 }.
% 0.82/1.20 { ! alpha17, ! hskp9, alpha30 }.
% 0.82/1.20 { hskp9, alpha17 }.
% 0.82/1.20 { ! alpha30, alpha17 }.
% 0.82/1.20 { ! alpha30, alpha42 }.
% 0.82/1.20 { ! alpha30, c2_1( a6 ) }.
% 0.82/1.20 { ! alpha42, ! c2_1( a6 ), alpha30 }.
% 0.82/1.20 { ! alpha42, ndr1_0 }.
% 0.82/1.20 { ! alpha42, c1_1( a6 ) }.
% 0.82/1.20 { ! alpha42, c3_1( a6 ) }.
% 0.82/1.20 { ! ndr1_0, ! c1_1( a6 ), ! c3_1( a6 ), alpha42 }.
% 0.82/1.20 { ! alpha9, alpha18 }.
% 0.82/1.20 { ! alpha9, alpha31 }.
% 0.82/1.20 { ! alpha18, ! alpha31, alpha9 }.
% 0.82/1.20 { ! alpha31, ! hskp8, alpha43 }.
% 0.82/1.20 { hskp8, alpha31 }.
% 0.82/1.20 { ! alpha43, alpha31 }.
% 0.82/1.20 { ! alpha43, alpha51 }.
% 0.82/1.20 { ! alpha43, c2_1( a3 ) }.
% 0.82/1.20 { ! alpha51, ! c2_1( a3 ), alpha43 }.
% 0.82/1.20 { ! alpha51, ndr1_0 }.
% 0.82/1.20 { ! alpha51, ! c3_1( a3 ) }.
% 0.82/1.20 { ! alpha51, ! c1_1( a3 ) }.
% 0.82/1.20 { ! ndr1_0, c3_1( a3 ), c1_1( a3 ), alpha51 }.
% 0.82/1.20 { ! alpha18, alpha2 }.
% 0.82/1.20 { ! alpha18, alpha32 }.
% 0.82/1.20 { ! alpha2, ! alpha32, alpha18 }.
% 0.82/1.20 { ! alpha32, ! hskp7, alpha44 }.
% 0.82/1.20 { hskp7, alpha32 }.
% 0.82/1.20 { ! alpha44, alpha32 }.
% 0.82/1.20 { ! alpha44, alpha52 }.
% 0.82/1.20 { ! alpha44, c1_1( a1 ) }.
% 0.82/1.20 { ! alpha52, ! c1_1( a1 ), alpha44 }.
% 0.82/1.20 { ! alpha52, ndr1_0 }.
% 0.82/1.20 { ! alpha52, c3_1( a1 ) }.
% 0.82/1.20 { ! alpha52, c0_1( a1 ) }.
% 0.82/1.20 { ! ndr1_0, ! c3_1( a1 ), ! c0_1( a1 ), alpha52 }.
% 0.82/1.20 { ! alpha2, alpha5 }.
% 0.82/1.20 { ! alpha2, alpha10 }.
% 0.82/1.20 { ! alpha5, ! alpha10, alpha2 }.
% 0.82/1.20 { ! alpha10, ! hskp6, alpha19 }.
% 0.82/1.20 { hskp6, alpha10 }.
% 0.82/1.20 { ! alpha19, alpha10 }.
% 0.82/1.20 { ! alpha19, alpha33 }.
% 0.82/1.20 { ! alpha19, ! c2_1( a14 ) }.
% 0.82/1.20 { ! alpha33, c2_1( a14 ), alpha19 }.
% 0.82/1.20 { ! alpha33, ndr1_0 }.
% 0.82/1.20 { ! alpha33, ! c0_1( a14 ) }.
% 0.82/1.20 { ! alpha33, c1_1( a14 ) }.
% 0.82/1.20 { ! ndr1_0, c0_1( a14 ), ! c1_1( a14 ), alpha33 }.
% 0.82/1.20 { ! alpha5, alpha11 }.
% 0.82/1.20 { ! alpha5, alpha20 }.
% 0.82/1.20 { ! alpha11, ! alpha20, alpha5 }.
% 0.82/1.20 { ! alpha20, ! hskp5, alpha34 }.
% 0.82/1.20 { hskp5, alpha20 }.
% 0.82/1.20 { ! alpha34, alpha20 }.
% 0.82/1.20 { ! alpha34, alpha45 }.
% 0.82/1.20 { ! alpha34, ! c2_1( a12 ) }.
% 0.82/1.20 { ! alpha45, c2_1( a12 ), alpha34 }.
% 0.82/1.20 { ! alpha45, ndr1_0 }.
% 0.82/1.20 { ! alpha45, ! c1_1( a12 ) }.
% 0.82/1.20 { ! alpha45, ! c0_1( a12 ) }.
% 0.82/1.20 { ! ndr1_0, c1_1( a12 ), c0_1( a12 ), alpha45 }.
% 0.82/1.20 { ! alpha11, alpha1 }.
% 0.82/1.20 { ! alpha11, alpha21 }.
% 0.82/1.20 { ! alpha1, ! alpha21, alpha11 }.
% 0.82/1.20 { ! alpha21, ! hskp4, alpha35 }.
% 0.82/1.20 { hskp4, alpha21 }.
% 0.87/1.29 { ! alpha35, alpha21 }.
% 0.87/1.29 { ! alpha35, alpha46 }.
% 0.87/1.29 { ! alpha35, ! c0_1( a11 ) }.
% 0.87/1.29 { ! alpha46, c0_1( a11 ), alpha35 }.
% 0.87/1.29 { ! alpha46, ndr1_0 }.
% 0.87/1.29 { ! alpha46, c1_1( a11 ) }.
% 0.87/1.29 { ! alpha46, c2_1( a11 ) }.
% 0.87/1.29 { ! ndr1_0, ! c1_1( a11 ), ! c2_1( a11 ), alpha46 }.
% 0.87/1.29 { ! alpha1, alpha3 }.
% 0.87/1.29 { ! alpha1, alpha6 }.
% 0.87/1.29 { ! alpha3, ! alpha6, alpha1 }.
% 0.87/1.29 { ! alpha6, ! hskp3, alpha12 }.
% 0.87/1.29 { hskp3, alpha6 }.
% 0.87/1.29 { ! alpha12, alpha6 }.
% 0.87/1.29 { ! alpha12, alpha22 }.
% 0.87/1.29 { ! alpha12, ! c0_1( a8 ) }.
% 0.87/1.29 { ! alpha22, c0_1( a8 ), alpha12 }.
% 0.87/1.29 { ! alpha22, ndr1_0 }.
% 0.87/1.29 { ! alpha22, c1_1( a8 ) }.
% 0.87/1.29 { ! alpha22, c3_1( a8 ) }.
% 0.87/1.29 { ! ndr1_0, ! c1_1( a8 ), ! c3_1( a8 ), alpha22 }.
% 0.87/1.29 { ! alpha3, alpha7 }.
% 0.87/1.29 { ! alpha3, alpha13 }.
% 0.87/1.29 { ! alpha7, ! alpha13, alpha3 }.
% 0.87/1.29 { ! alpha13, ! hskp2, alpha23 }.
% 0.87/1.29 { hskp2, alpha13 }.
% 0.87/1.29 { ! alpha23, alpha13 }.
% 0.87/1.29 { ! alpha23, alpha36 }.
% 0.87/1.29 { ! alpha23, ! c2_1( a5 ) }.
% 0.87/1.29 { ! alpha36, c2_1( a5 ), alpha23 }.
% 0.87/1.29 { ! alpha36, ndr1_0 }.
% 0.87/1.29 { ! alpha36, c1_1( a5 ) }.
% 0.87/1.29 { ! alpha36, c0_1( a5 ) }.
% 0.87/1.29 { ! ndr1_0, ! c1_1( a5 ), ! c0_1( a5 ), alpha36 }.
% 0.87/1.29 { ! alpha7, alpha14 }.
% 0.87/1.29 { ! alpha7, alpha24 }.
% 0.87/1.29 { ! alpha14, ! alpha24, alpha7 }.
% 0.87/1.29 { ! alpha24, ! hskp1, alpha37 }.
% 0.87/1.29 { hskp1, alpha24 }.
% 0.87/1.29 { ! alpha37, alpha24 }.
% 0.87/1.29 { ! alpha37, alpha47 }.
% 0.87/1.29 { ! alpha37, ! c2_1( a4 ) }.
% 0.87/1.29 { ! alpha47, c2_1( a4 ), alpha37 }.
% 0.87/1.29 { ! alpha47, ndr1_0 }.
% 0.87/1.29 { ! alpha47, ! c3_1( a4 ) }.
% 0.87/1.29 { ! alpha47, c1_1( a4 ) }.
% 0.87/1.29 { ! ndr1_0, c3_1( a4 ), ! c1_1( a4 ), alpha47 }.
% 0.87/1.29 { ! alpha14, ! hskp0, alpha25 }.
% 0.87/1.29 { hskp0, alpha14 }.
% 0.87/1.29 { ! alpha25, alpha14 }.
% 0.87/1.29 { ! alpha25, alpha38 }.
% 0.87/1.29 { ! alpha25, ! c1_1( a2 ) }.
% 0.87/1.29 { ! alpha38, c1_1( a2 ), alpha25 }.
% 0.87/1.29 { ! alpha38, ndr1_0 }.
% 0.87/1.29 { ! alpha38, ! c3_1( a2 ) }.
% 0.87/1.29 { ! alpha38, c0_1( a2 ) }.
% 0.87/1.29 { ! ndr1_0, c3_1( a2 ), ! c0_1( a2 ), alpha38 }.
% 0.87/1.29
% 0.87/1.29 percentage equality = 0.000000, percentage horn = 0.805556
% 0.87/1.29 This a non-horn, non-equality problem
% 0.87/1.29
% 0.87/1.29
% 0.87/1.29 Options Used:
% 0.87/1.29
% 0.87/1.29 useres = 1
% 0.87/1.29 useparamod = 0
% 0.87/1.29 useeqrefl = 0
% 0.87/1.29 useeqfact = 0
% 0.87/1.29 usefactor = 1
% 0.87/1.29 usesimpsplitting = 0
% 0.87/1.29 usesimpdemod = 0
% 0.87/1.29 usesimpres = 3
% 0.87/1.29
% 0.87/1.29 resimpinuse = 1000
% 0.87/1.29 resimpclauses = 20000
% 0.87/1.29 substype = standard
% 0.87/1.29 backwardsubs = 1
% 0.87/1.29 selectoldest = 5
% 0.87/1.29
% 0.87/1.29 litorderings [0] = split
% 0.87/1.29 litorderings [1] = liftord
% 0.87/1.29
% 0.87/1.29 termordering = none
% 0.87/1.29
% 0.87/1.29 litapriori = 1
% 0.87/1.29 termapriori = 0
% 0.87/1.29 litaposteriori = 0
% 0.87/1.29 termaposteriori = 0
% 0.87/1.29 demodaposteriori = 0
% 0.87/1.29 ordereqreflfact = 0
% 0.87/1.29
% 0.87/1.29 litselect = none
% 0.87/1.29
% 0.87/1.29 maxweight = 15
% 0.87/1.29 maxdepth = 30000
% 0.87/1.29 maxlength = 115
% 0.87/1.29 maxnrvars = 195
% 0.87/1.29 excuselevel = 1
% 0.87/1.29 increasemaxweight = 1
% 0.87/1.29
% 0.87/1.29 maxselected = 10000000
% 0.87/1.29 maxnrclauses = 10000000
% 0.87/1.29
% 0.87/1.29 showgenerated = 0
% 0.87/1.29 showkept = 0
% 0.87/1.29 showselected = 0
% 0.87/1.29 showdeleted = 0
% 0.87/1.29 showresimp = 1
% 0.87/1.29 showstatus = 2000
% 0.87/1.29
% 0.87/1.29 prologoutput = 0
% 0.87/1.29 nrgoals = 5000000
% 0.87/1.29 totalproof = 1
% 0.87/1.29
% 0.87/1.29 Symbols occurring in the translation:
% 0.87/1.29
% 0.87/1.29 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.87/1.29 . [1, 2] (w:1, o:105, a:1, s:1, b:0),
% 0.87/1.29 ! [4, 1] (w:0, o:96, a:1, s:1, b:0),
% 0.87/1.29 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.87/1.29 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.87/1.29 hskp0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.87/1.29 ndr1_0 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.87/1.29 a2 [37, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.87/1.29 c3_1 [38, 1] (w:1, o:102, a:1, s:1, b:0),
% 0.87/1.29 c0_1 [39, 1] (w:1, o:103, a:1, s:1, b:0),
% 0.87/1.29 c1_1 [40, 1] (w:1, o:104, a:1, s:1, b:0),
% 0.87/1.29 hskp1 [41, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.87/1.29 a4 [42, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.87/1.29 c2_1 [43, 1] (w:1, o:101, a:1, s:1, b:0),
% 0.87/1.29 hskp2 [44, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.87/1.29 a5 [45, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.87/1.29 hskp3 [46, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.87/1.29 a8 [47, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.87/1.29 hskp4 [48, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.87/1.29 a11 [49, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.87/1.29 hskp5 [50, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.87/1.29 a12 [51, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.87/1.29 hskp6 [52, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.87/1.29 a14 [53, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.87/1.29 hskp7 [54, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.87/1.29 a1 [55, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.87/1.29 hskp8 [56, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.87/1.29 a3 [57, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.87/1.29 hskp9 [58, 0] (w:1, o:32, a:1, s:1, b:0),
% 1.84/2.20 a6 [59, 0] (w:1, o:33, a:1, s:1, b:0),
% 1.84/2.20 hskp10 [60, 0] (w:1, o:18, a:1, s:1, b:0),
% 1.84/2.20 a7 [61, 0] (w:1, o:25, a:1, s:1, b:0),
% 1.84/2.20 hskp11 [62, 0] (w:1, o:19, a:1, s:1, b:0),
% 1.84/2.20 a9 [63, 0] (w:1, o:34, a:1, s:1, b:0),
% 1.84/2.20 hskp12 [64, 0] (w:1, o:20, a:1, s:1, b:0),
% 1.84/2.20 a10 [65, 0] (w:1, o:8, a:1, s:1, b:0),
% 1.84/2.20 hskp13 [66, 0] (w:1, o:21, a:1, s:1, b:0),
% 1.84/2.20 a15 [67, 0] (w:1, o:13, a:1, s:1, b:0),
% 1.84/2.20 alpha1 [77, 0] (w:1, o:44, a:1, s:1, b:0),
% 1.84/2.20 alpha2 [78, 0] (w:1, o:55, a:1, s:1, b:0),
% 1.84/2.20 alpha3 [79, 0] (w:1, o:66, a:1, s:1, b:0),
% 1.84/2.20 alpha4 [80, 0] (w:1, o:77, a:1, s:1, b:0),
% 1.84/2.20 alpha5 [81, 0] (w:1, o:88, a:1, s:1, b:0),
% 1.84/2.20 alpha6 [82, 0] (w:1, o:92, a:1, s:1, b:0),
% 1.84/2.20 alpha7 [83, 0] (w:1, o:93, a:1, s:1, b:0),
% 1.84/2.20 alpha8 [84, 0] (w:1, o:94, a:1, s:1, b:0),
% 1.84/2.20 alpha9 [85, 0] (w:1, o:95, a:1, s:1, b:0),
% 1.84/2.20 alpha10 [86, 0] (w:1, o:45, a:1, s:1, b:0),
% 1.84/2.20 alpha11 [87, 0] (w:1, o:46, a:1, s:1, b:0),
% 1.84/2.20 alpha12 [88, 0] (w:1, o:47, a:1, s:1, b:0),
% 1.84/2.20 alpha13 [89, 0] (w:1, o:48, a:1, s:1, b:0),
% 1.84/2.20 alpha14 [90, 0] (w:1, o:49, a:1, s:1, b:0),
% 1.84/2.20 alpha15 [91, 0] (w:1, o:50, a:1, s:1, b:0),
% 1.84/2.20 alpha16 [92, 0] (w:1, o:51, a:1, s:1, b:0),
% 1.84/2.20 alpha17 [93, 0] (w:1, o:52, a:1, s:1, b:0),
% 1.84/2.20 alpha18 [94, 0] (w:1, o:53, a:1, s:1, b:0),
% 1.84/2.20 alpha19 [95, 0] (w:1, o:54, a:1, s:1, b:0),
% 1.84/2.20 alpha20 [96, 0] (w:1, o:56, a:1, s:1, b:0),
% 1.84/2.20 alpha21 [97, 0] (w:1, o:57, a:1, s:1, b:0),
% 1.84/2.20 alpha22 [98, 0] (w:1, o:58, a:1, s:1, b:0),
% 1.84/2.20 alpha23 [99, 0] (w:1, o:59, a:1, s:1, b:0),
% 1.84/2.20 alpha24 [100, 0] (w:1, o:60, a:1, s:1, b:0),
% 1.84/2.20 alpha25 [101, 0] (w:1, o:61, a:1, s:1, b:0),
% 1.84/2.20 alpha26 [102, 0] (w:1, o:62, a:1, s:1, b:0),
% 1.84/2.20 alpha27 [103, 0] (w:1, o:63, a:1, s:1, b:0),
% 1.84/2.20 alpha28 [104, 0] (w:1, o:64, a:1, s:1, b:0),
% 1.84/2.20 alpha29 [105, 0] (w:1, o:65, a:1, s:1, b:0),
% 1.84/2.20 alpha30 [106, 0] (w:1, o:67, a:1, s:1, b:0),
% 1.84/2.20 alpha31 [107, 0] (w:1, o:68, a:1, s:1, b:0),
% 1.84/2.20 alpha32 [108, 0] (w:1, o:69, a:1, s:1, b:0),
% 1.84/2.20 alpha33 [109, 0] (w:1, o:70, a:1, s:1, b:0),
% 1.84/2.20 alpha34 [110, 0] (w:1, o:71, a:1, s:1, b:0),
% 1.84/2.20 alpha35 [111, 0] (w:1, o:72, a:1, s:1, b:0),
% 1.84/2.20 alpha36 [112, 0] (w:1, o:73, a:1, s:1, b:0),
% 1.84/2.20 alpha37 [113, 0] (w:1, o:74, a:1, s:1, b:0),
% 1.84/2.20 alpha38 [114, 0] (w:1, o:75, a:1, s:1, b:0),
% 1.84/2.20 alpha39 [115, 0] (w:1, o:76, a:1, s:1, b:0),
% 1.84/2.20 alpha40 [116, 0] (w:1, o:78, a:1, s:1, b:0),
% 1.84/2.20 alpha41 [117, 0] (w:1, o:79, a:1, s:1, b:0),
% 1.84/2.20 alpha42 [118, 0] (w:1, o:80, a:1, s:1, b:0),
% 1.84/2.20 alpha43 [119, 0] (w:1, o:81, a:1, s:1, b:0),
% 1.84/2.20 alpha44 [120, 0] (w:1, o:82, a:1, s:1, b:0),
% 1.84/2.20 alpha45 [121, 0] (w:1, o:83, a:1, s:1, b:0),
% 1.84/2.20 alpha46 [122, 0] (w:1, o:84, a:1, s:1, b:0),
% 1.84/2.20 alpha47 [123, 0] (w:1, o:85, a:1, s:1, b:0),
% 1.84/2.20 alpha48 [124, 0] (w:1, o:86, a:1, s:1, b:0),
% 1.84/2.20 alpha49 [125, 0] (w:1, o:87, a:1, s:1, b:0),
% 1.84/2.20 alpha50 [126, 0] (w:1, o:89, a:1, s:1, b:0),
% 1.84/2.20 alpha51 [127, 0] (w:1, o:90, a:1, s:1, b:0),
% 1.84/2.20 alpha52 [128, 0] (w:1, o:91, a:1, s:1, b:0).
% 1.84/2.20
% 1.84/2.20
% 1.84/2.20 Starting Search:
% 1.84/2.20
% 1.84/2.20 *** allocated 15000 integers for clauses
% 1.84/2.20 Resimplifying inuse:
% 1.84/2.20 Done
% 1.84/2.20
% 1.84/2.20 Failed to find proof!
% 1.84/2.20 maxweight = 15
% 1.84/2.20 maxnrclauses = 10000000
% 1.84/2.20 Generated: 963
% 1.84/2.20 Kept: 302
% 1.84/2.20
% 1.84/2.20
% 1.84/2.20 The strategy used was not complete!
% 1.84/2.20
% 1.84/2.20 Increased maxweight to 16
% 1.84/2.20
% 1.84/2.20 Starting Search:
% 1.84/2.20
% 1.84/2.20 Resimplifying inuse:
% 1.84/2.20 Done
% 1.84/2.20
% 1.84/2.20 Failed to find proof!
% 1.84/2.20 maxweight = 16
% 1.84/2.20 maxnrclauses = 10000000
% 1.84/2.20 Generated: 1124
% 1.84/2.20 Kept: 320
% 1.84/2.20
% 1.84/2.20
% 1.84/2.20 The strategy used was not complete!
% 1.84/2.20
% 1.84/2.20 Increased maxweight to 17
% 1.84/2.20
% 1.84/2.20 Starting Search:
% 1.84/2.20
% 1.84/2.20 Resimplifying inuse:
% 1.84/2.20 Done
% 1.84/2.20
% 1.84/2.20 Failed to find proof!
% 1.84/2.20 maxweight = 17
% 1.84/2.20 maxnrclauses = 10000000
% 1.84/2.20 Generated: 1131
% 1.84/2.20 Kept: 324
% 1.84/2.20
% 1.84/2.20
% 1.84/2.20 The strategy used was not complete!
% 1.84/2.20
% 1.84/2.20 Increased maxweight to 18
% 1.84/2.20
% 1.84/2.20 Starting Search:
% 1.84/2.20
% 1.84/2.20 Resimplifying inuse:
% 1.84/2.20 Done
% 1.84/2.20
% 1.84/2.20 Failed to find proof!
% 1.84/2.20 maxweight = 18
% 1.84/2.20 maxnrclauses = 10000000
% 1.84/2.20 Generated: 1264
% 1.84/2.20 Kept: 342
% 1.84/2.20
% 1.84/2.20
% 1.84/2.20 The strategy used was not complete!
% 1.84/2.20
% 1.84/2.20 Increased maxweight to 19
% 1.84/2.20
% 1.84/2.20 Starting Search:
% 1.84/2.20
% 1.84/2.20 *** allocated 22500 integers for clauses
% 1.84/2.20 Resimplifying inuse:
% 1.84/2.20 Done
% 1.84/2.20
% 1.84/2.20 Failed to find proof!
% 1.84/2.20 maxweight = 19
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 2480
% 1.84/2.21 Kept: 397
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 20
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 20
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 3277
% 1.84/2.21 Kept: 433
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 21
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 21
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 5556
% 1.84/2.21 Kept: 491
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 22
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 *** allocated 33750 integers for clauses
% 1.84/2.21 *** allocated 15000 integers for termspace/termends
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 22
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 5772
% 1.84/2.21 Kept: 546
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 23
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 23
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6149
% 1.84/2.21 Kept: 599
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 24
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 24
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6112
% 1.84/2.21 Kept: 614
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 25
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 25
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6444
% 1.84/2.21 Kept: 660
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 26
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 26
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6667
% 1.84/2.21 Kept: 634
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 27
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 27
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6758
% 1.84/2.21 Kept: 642
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 28
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 28
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6758
% 1.84/2.21 Kept: 645
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 29
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 29
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6868
% 1.84/2.21 Kept: 656
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 30
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 30
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6917
% 1.84/2.21 Kept: 662
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 31
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 31
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6917
% 1.84/2.21 Kept: 666
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 32
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 32
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 33
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 33
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 34
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 34
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 35
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 35
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 36
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 36
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 37
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21 Failed to find proof!
% 1.84/2.21 maxweight = 37
% 1.84/2.21 maxnrclauses = 10000000
% 1.84/2.21 Generated: 6922
% 1.84/2.21 Kept: 667
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 The strategy used was not complete!
% 1.84/2.21
% 1.84/2.21 Increased maxweight to 38
% 1.84/2.21
% 1.84/2.21 Starting Search:
% 1.84/2.21
% 1.84/2.21 Resimplifying inuse:
% 1.84/2.21 Done
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 found a saturation!
% 1.84/2.21 % SZS status CounterSatisfiable
% 1.84/2.21 % SZS output start Saturation
% 1.84/2.21
% 1.84/2.21 (659) {G23,W25,D2,L16,V1,M2} R(423,244);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a3 ), c2_1( a7 ), hskp6, c3_1( a3 ), hskp13, ! c3_1( X )
% 1.84/2.21 , ! c3_1( a7 ), ! c3_1( a5 ), alpha36, alpha50, ! c0_1( a5 ), ! c0_1( X )
% 1.84/2.21 }.
% 1.84/2.21 (662) {G23,W25,D2,L16,V1,M2} R(399,244);f;f { hskp4, alpha48, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a10 ), c2_1( a7 ), hskp6, c3_1( a10 ), hskp13, ! c3_1( X
% 1.84/2.21 ), ! c3_1( a7 ), ! c3_1( a5 ), alpha36, alpha50, ! c0_1( a5 ), ! c0_1( X
% 1.84/2.21 ) }.
% 1.84/2.21 (542) {G24,W25,D2,L15,V1,M2} F(538);f;f { hskp4, hskp12, alpha48, alpha26,
% 1.84/2.21 c2_1( a10 ), c2_1( a15 ), ! c2_1( X ), c2_1( a3 ), alpha51, ! c3_1( a15 )
% 1.84/2.21 , ! c3_1( a10 ), ! c3_1( X ), c3_1( a3 ), ! c0_1( X ), ! c0_1( a3 ) }.
% 1.84/2.21 (631) {G25,W24,D2,L16,V0,M1} R(616,244);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a3 ), alpha45, c2_1( a7 ), ! c3_1( a12 ), c3_1( a3 ),
% 1.84/2.21 hskp6, hskp13, ! c3_1( a5 ), ! c3_1( a7 ), alpha36, alpha50, ! c0_1( a5 )
% 1.84/2.21 }.
% 1.84/2.21 (634) {G25,W24,D2,L16,V0,M1} R(503,244);f;f { hskp4, hskp12, alpha48,
% 1.84/2.21 alpha45, c2_1( a10 ), ! c2_1( a12 ), c2_1( a7 ), ! c3_1( a12 ), c3_1( a10
% 1.84/2.21 ), hskp6, hskp13, ! c3_1( a5 ), ! c3_1( a7 ), alpha36, alpha50, ! c0_1(
% 1.84/2.21 a5 ) }.
% 1.84/2.21 (606) {G25,W24,D2,L15,V0,M1} R(426,500);f;f;f;f;f;f { hskp4, alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a10 ), c2_1( a3 ), alpha45, ! c3_1( a10 ), !
% 1.84/2.21 c3_1( a12 ), c3_1( a3 ), alpha48, c2_1( a15 ), ! c3_1( a15 ), alpha26, !
% 1.84/2.21 c0_1( a3 ) }.
% 1.84/2.21 (663) {G23,W24,D2,L15,V1,M2} R(399,251);f;f;r(1) { hskp4, alpha48, hskp12,
% 1.84/2.21 ! c2_1( X ), c2_1( a10 ), c2_1( a7 ), hskp6, c3_1( a10 ), ! c3_1( a7 ), !
% 1.84/2.21 c3_1( X ), ! c3_1( a15 ), alpha26, alpha50, ! c0_1( a15 ), ! c0_1( X )
% 1.84/2.21 }.
% 1.84/2.21 (635) {G25,W23,D2,L15,V0,M1} R(503,251);f;f;r(1) { hskp4, hskp12, alpha48,
% 1.84/2.21 alpha45, c2_1( a10 ), ! c2_1( a12 ), c2_1( a7 ), ! c3_1( a12 ), c3_1( a10
% 1.84/2.21 ), hskp6, ! c3_1( a15 ), ! c3_1( a7 ), alpha26, alpha50, ! c0_1( a15 )
% 1.84/2.21 }.
% 1.84/2.21 (543) {G24,W23,D2,L14,V1,M2} F(537);f;f { hskp4, hskp12, alpha48, alpha26,
% 1.84/2.21 c2_1( a10 ), c2_1( a15 ), ! c2_1( X ), c2_1( a7 ), alpha50, ! c3_1( a10 )
% 1.84/2.21 , ! c3_1( X ), ! c3_1( a15 ), ! c0_1( a7 ), ! c0_1( X ) }.
% 1.84/2.21 (548) {G24,W23,D2,L14,V1,M2} F(544);f;f { hskp4, hskp12, alpha48, alpha36,
% 1.84/2.21 c2_1( a10 ), c2_1( a5 ), ! c2_1( X ), c2_1( a7 ), alpha50, ! c3_1( a10 )
% 1.84/2.21 , ! c3_1( X ), ! c3_1( a5 ), ! c0_1( a7 ), ! c0_1( X ) }.
% 1.84/2.21 (507) {G25,W22,D2,L14,V0,M1} R(500,441);f;f;f;f;f;f { hskp4, hskp12,
% 1.84/2.21 alpha48, c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a15 ), ! c3_1( a12 )
% 1.84/2.21 , alpha26, alpha50, c2_1( a7 ), ! c3_1( a10 ), ! c3_1( a15 ), ! c0_1( a7
% 1.84/2.21 ) }.
% 1.84/2.21 (519) {G25,W22,D2,L14,V0,M1} R(501,441);f;f;f;f;f;f { hskp4, hskp12,
% 1.84/2.21 alpha48, c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a5 ), ! c3_1( a12 ),
% 1.84/2.21 alpha36, alpha50, c2_1( a7 ), ! c3_1( a10 ), ! c3_1( a5 ), ! c0_1( a7 )
% 1.84/2.21 }.
% 1.84/2.21 (660) {G24,W21,D2,L14,V0,M1} F(659);f { hskp4, hskp12, alpha51, c2_1( a3 )
% 1.84/2.21 , ! c2_1( a5 ), hskp6, c2_1( a7 ), hskp13, c3_1( a3 ), ! c3_1( a5 ),
% 1.84/2.21 alpha36, alpha50, ! c3_1( a7 ), ! c0_1( a5 ) }.
% 1.84/2.21 (665) {G24,W21,D2,L14,V0,M1} F(662);f { hskp4, hskp12, alpha48, c2_1( a10 )
% 1.84/2.21 , ! c2_1( a5 ), hskp6, c2_1( a7 ), hskp13, c3_1( a10 ), ! c3_1( a5 ),
% 1.84/2.21 alpha36, alpha50, ! c3_1( a7 ), ! c0_1( a5 ) }.
% 1.84/2.21 (666) {G24,W21,D2,L14,V0,M1} F(661);f;f { hskp4, hskp12, alpha48, c2_1( a10
% 1.84/2.21 ), ! c2_1( a11 ), hskp6, c2_1( a7 ), hskp13, c3_1( a10 ), ! c3_1( a11 )
% 1.84/2.21 , alpha46, alpha50, ! c3_1( a7 ), ! c0_1( a11 ) }.
% 1.84/2.21 (664) {G24,W20,D2,L13,V0,M1} F(663);f { hskp4, hskp12, alpha48, c2_1( a10 )
% 1.84/2.21 , ! c2_1( a15 ), hskp6, c2_1( a7 ), c3_1( a10 ), ! c3_1( a15 ), alpha26,
% 1.84/2.21 alpha50, ! c3_1( a7 ), ! c0_1( a15 ) }.
% 1.84/2.21 (399) {G22,W21,D2,L13,V2,M2} R(261,163);f { hskp4, c2_1( a10 ), alpha48, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( Y ), ! c3_1( X ), ! c3_1( Y ), c3_1( a10 ),
% 1.84/2.21 hskp6, hskp13, ! c0_1( X ), c0_1( Y ) }.
% 1.84/2.21 (658) {G23,W19,D2,L12,V1,M1} R(423,319);f;f;f;f;f;f;r(1) { hskp4, alpha51,
% 1.84/2.21 hskp12, ! c2_1( X ), c2_1( a15 ), c2_1( a3 ), hskp6, ! c3_1( a15 ), c3_1
% 1.84/2.21 ( a3 ), ! c3_1( X ), alpha26, ! c0_1( X ) }.
% 1.84/2.21 (423) {G22,W21,D2,L13,V2,M2} R(269,163);f;f { hskp4, c2_1( a3 ), alpha51, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( Y ), ! c3_1( X ), c3_1( a3 ), ! c3_1( Y ),
% 1.84/2.21 hskp6, hskp13, ! c0_1( X ), c0_1( Y ) }.
% 1.84/2.21 (654) {G23,W20,D2,L13,V1,M1} R(438,257);f;f;f;f;f;f;f { hskp4, alpha50,
% 1.84/2.21 hskp12, ! c2_1( X ), c2_1( a5 ), c2_1( a7 ), hskp6, ! c3_1( a5 ), hskp13
% 1.84/2.21 , ! c3_1( X ), c3_1( a7 ), alpha36, ! c0_1( X ) }.
% 1.84/2.21 (656) {G23,W19,D2,L12,V1,M1} R(438,255);f;f;f;f;f;f;r(1) { hskp4, alpha50,
% 1.84/2.21 hskp12, ! c2_1( X ), c2_1( a15 ), c2_1( a7 ), hskp6, ! c3_1( a15 ), c3_1
% 1.84/2.21 ( a7 ), ! c3_1( X ), alpha26, ! c0_1( X ) }.
% 1.84/2.21 (438) {G22,W21,D2,L13,V2,M2} R(281,163);f { hskp4, c2_1( a7 ), alpha50, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( Y ), ! c3_1( X ), ! c3_1( Y ), c3_1( a7 ), hskp6
% 1.84/2.21 , hskp13, ! c0_1( X ), c0_1( Y ) }.
% 1.84/2.21 (474) {G23,W20,D2,L14,V1,M2} R(288,163);f { hskp12, hskp2, hskp9, hskp4,
% 1.84/2.21 c2_1( a7 ), ! c2_1( X ), c2_1( a6 ), alpha50, alpha42, hskp6, c3_1( a7 )
% 1.84/2.21 , hskp13, ! c3_1( a6 ), ! c3_1( X ) }.
% 1.84/2.21 (487) {G23,W20,D2,L14,V1,M2} R(289,163);f { hskp12, hskp2, hskp9, hskp4,
% 1.84/2.21 c2_1( a10 ), ! c2_1( X ), c2_1( a6 ), alpha48, alpha42, hskp6, c3_1( a10
% 1.84/2.21 ), hskp13, ! c3_1( a6 ), ! c3_1( X ) }.
% 1.84/2.21 (560) {G23,W20,D2,L14,V1,M2} R(293,163);f { hskp12, hskp2, hskp9, hskp4,
% 1.84/2.21 c2_1( a10 ), ! c2_1( X ), c2_1( a5 ), alpha36, alpha48, hskp6, c3_1( a10
% 1.84/2.21 ), hskp13, ! c3_1( a5 ), ! c3_1( X ) }.
% 1.84/2.21 (563) {G23,W20,D2,L14,V1,M2} R(294,163);f { hskp12, hskp2, hskp9, hskp4,
% 1.84/2.21 c2_1( a7 ), ! c2_1( X ), c2_1( a8 ), alpha22, alpha50, hskp6, c3_1( a7 )
% 1.84/2.21 , hskp13, ! c3_1( a8 ), ! c3_1( X ) }.
% 1.84/2.21 (566) {G23,W20,D2,L14,V1,M2} R(295,163);f { hskp12, hskp2, hskp9, hskp4,
% 1.84/2.21 c2_1( a10 ), ! c2_1( X ), c2_1( a8 ), alpha22, alpha48, hskp6, c3_1( a10
% 1.84/2.21 ), hskp13, ! c3_1( a8 ), ! c3_1( X ) }.
% 1.84/2.21 (568) {G23,W20,D2,L14,V1,M2} R(298,163);f;f { hskp4, c2_1( a3 ), alpha22,
% 1.84/2.21 c3_1( a3 ), alpha51, ! c2_1( X ), hskp12, c2_1( a8 ), hskp2, hskp9, hskp6
% 1.84/2.21 , hskp13, ! c3_1( X ), ! c3_1( a8 ) }.
% 1.84/2.21 (571) {G23,W20,D2,L14,V1,M2} R(300,163);f;f { hskp4, c2_1( a3 ), c3_1( a3 )
% 1.84/2.21 , alpha51, alpha42, ! c2_1( X ), hskp12, c2_1( a6 ), hskp2, hskp9, hskp6
% 1.84/2.21 , hskp13, ! c3_1( X ), ! c3_1( a6 ) }.
% 1.84/2.21 (592) {G23,W20,D2,L14,V1,M2} R(325,163);f;f { hskp4, c2_1( a3 ), alpha36,
% 1.84/2.21 c3_1( a3 ), alpha51, ! c2_1( X ), hskp12, c2_1( a5 ), hskp2, hskp9, hskp6
% 1.84/2.21 , hskp13, ! c3_1( X ), ! c3_1( a5 ) }.
% 1.84/2.21 (646) {G25,W19,D2,L13,V0,M1} R(467,257);f;f;f;f;f;f;f { hskp4, hskp12,
% 1.84/2.21 alpha50, alpha45, ! c2_1( a12 ), c2_1( a5 ), c2_1( a7 ), ! c3_1( a12 ), !
% 1.84/2.21 c3_1( a5 ), hskp6, hskp13, alpha36, c3_1( a7 ) }.
% 1.84/2.21 (651) {G26,W18,D2,L13,V1,M2} F(650);f { hskp4, alpha36, alpha50, hskp6,
% 1.84/2.21 hskp13, hskp12, hskp2, c2_1( a5 ), hskp9, ! c2_1( X ), c2_1( a7 ), ! c3_1
% 1.84/2.21 ( X ), ! c3_1( a5 ) }.
% 1.84/2.21 (647) {G25,W18,D2,L12,V0,M1} R(467,255);f;f;f;f;f;f;r(1) { hskp4, hskp12,
% 1.84/2.21 alpha50, alpha45, ! c2_1( a12 ), c2_1( a15 ), c2_1( a7 ), ! c3_1( a12 ),
% 1.84/2.21 ! c3_1( a15 ), hskp6, alpha26, c3_1( a7 ) }.
% 1.84/2.21 (467) {G24,W20,D2,L13,V1,M1} R(441,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( a12 ), alpha45, c2_1( X ), c2_1( a7 ), ! c3_1( X ), ! c3_1( a12 ), c3_1
% 1.84/2.21 ( a7 ), hskp6, hskp13, c0_1( X ) }.
% 1.84/2.21 (481) {G23,W20,D2,L13,V1,M1} R(435,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a7 ), c2_1( a6 ), alpha42, ! c3_1( a6 ), ! c3_1( X ), c3_1(
% 1.84/2.21 a7 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (483) {G23,W20,D2,L13,V1,M1} R(437,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a7 ), c2_1( a8 ), alpha22, ! c3_1( a8 ), ! c3_1( X ), c3_1(
% 1.84/2.21 a7 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (489) {G23,W20,D2,L13,V1,M1} R(439,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a1 ), c2_1( a7 ), alpha52, ! c3_1( a1 ), ! c3_1( X ), c3_1(
% 1.84/2.21 a7 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (503) {G24,W20,D2,L13,V1,M1} R(402,163);f { hskp4, alpha48, hskp12, c2_1(
% 1.84/2.21 a10 ), alpha45, c2_1( X ), ! c2_1( a12 ), ! c3_1( X ), ! c3_1( a12 ),
% 1.84/2.21 c3_1( a10 ), hskp6, hskp13, c0_1( X ) }.
% 1.84/2.21 (529) {G23,W20,D2,L13,V1,M1} R(393,163);f { hskp4, alpha48, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a10 ), c2_1( a6 ), alpha42, ! c3_1( a6 ), ! c3_1( X ), c3_1
% 1.84/2.21 ( a10 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (546) {G23,W20,D2,L13,V1,M1} R(395,163);f { hskp4, alpha48, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a10 ), c2_1( a5 ), alpha36, ! c3_1( a5 ), ! c3_1( X ), c3_1
% 1.84/2.21 ( a10 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (550) {G23,W20,D2,L13,V1,M1} R(398,163);f { hskp4, alpha48, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a10 ), c2_1( a8 ), alpha22, ! c3_1( a8 ), ! c3_1( X ), c3_1
% 1.84/2.21 ( a10 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (552) {G23,W20,D2,L13,V1,M1} R(400,163);f { hskp4, alpha48, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a10 ), c2_1( a1 ), alpha52, ! c3_1( a1 ), ! c3_1( X ), c3_1
% 1.84/2.21 ( a10 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (603) {G23,W20,D2,L13,V1,M1} R(416,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a3 ), c2_1( a5 ), alpha36, c3_1( a3 ), ! c3_1( a5 ), !
% 1.84/2.21 c3_1( X ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (630) {G25,W18,D2,L12,V0,M1} R(616,319);f;f;f;f;f;f;r(1) { hskp4, alpha51,
% 1.84/2.21 hskp12, ! c2_1( a12 ), c2_1( a15 ), alpha45, c2_1( a3 ), ! c3_1( a12 ), !
% 1.84/2.21 c3_1( a15 ), hskp6, alpha26, c3_1( a3 ) }.
% 1.84/2.21 (616) {G24,W20,D2,L13,V1,M1} R(426,163);f;f { hskp4, alpha51, ! c2_1( a12 )
% 1.84/2.21 , hskp12, c2_1( a3 ), c2_1( X ), alpha45, ! c3_1( a12 ), ! c3_1( X ),
% 1.84/2.21 c3_1( a3 ), hskp6, hskp13, c0_1( X ) }.
% 1.84/2.21 (622) {G23,W20,D2,L13,V1,M1} R(421,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a3 ), c2_1( a6 ), alpha42, c3_1( a3 ), ! c3_1( a6 ), !
% 1.84/2.21 c3_1( X ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (623) {G23,W20,D2,L13,V1,M1} R(422,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a3 ), c2_1( a8 ), alpha22, c3_1( a3 ), ! c3_1( a8 ), !
% 1.84/2.21 c3_1( X ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (624) {G23,W20,D2,L13,V1,M1} R(424,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a1 ), c2_1( a3 ), alpha52, ! c3_1( a1 ), c3_1( a3 ), !
% 1.84/2.21 c3_1( X ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (424) {G22,W20,D2,L12,V1,M2} R(269,180);f { hskp4, c2_1( a3 ), alpha51, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( a1 ), ! c3_1( X ), ! c3_1( a1 ), c3_1( a3 ),
% 1.84/2.21 alpha52, ! c0_1( a3 ), ! c0_1( X ) }.
% 1.84/2.21 (422) {G22,W20,D2,L12,V1,M2} R(269,211);f;f;f;f;f;f { hskp4, c2_1( a3 ),
% 1.84/2.21 alpha51, ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), c3_1( a3 ), ! c3_1
% 1.84/2.21 ( a8 ), alpha22, ! c0_1( a3 ), ! c0_1( X ) }.
% 1.84/2.21 (421) {G22,W20,D2,L12,V1,M2} R(269,271);f;f;f;f;f;f { hskp4, c2_1( a3 ),
% 1.84/2.21 alpha51, ! c2_1( X ), hskp12, c2_1( a6 ), ! c3_1( X ), c3_1( a3 ), ! c3_1
% 1.84/2.21 ( a6 ), alpha42, ! c0_1( a3 ), ! c0_1( X ) }.
% 1.84/2.21 (618) {G25,W19,D2,L13,V0,M1} R(612,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a3 ), alpha45, c2_1( a5 ), ! c3_1( a12 ), c3_1( a3 ),
% 1.84/2.21 alpha36, hskp6, hskp13, ! c3_1( a5 ) }.
% 1.84/2.21 (330) {G22,W21,D2,L13,V0,M1} R(240,215);f { hskp4, c2_1( a7 ), ! c3_1( a11
% 1.84/2.21 ), ! c2_1( a11 ), alpha46, alpha50, ! c2_1( a12 ), hskp12, ! c3_1( a12 )
% 1.84/2.21 , ! c3_1( a7 ), alpha45, ! c0_1( a11 ), c0_1( a12 ) }.
% 1.84/2.21 (619) {G25,W19,D2,L13,V0,M1} R(614,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a3 ), alpha45, c2_1( a6 ), ! c3_1( a12 ), c3_1( a3 ),
% 1.84/2.21 alpha42, hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (620) {G25,W19,D2,L13,V0,M1} R(615,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a3 ), alpha45, c2_1( a8 ), ! c3_1( a12 ), c3_1( a3 ),
% 1.84/2.21 alpha22, hskp6, hskp13, ! c3_1( a8 ) }.
% 1.84/2.21 (621) {G25,W19,D2,L13,V0,M1} R(617,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a1 ), alpha45, c2_1( a3 ), ! c3_1( a12 ), ! c3_1( a1 )
% 1.84/2.21 , alpha52, hskp6, hskp13, c3_1( a3 ) }.
% 1.84/2.21 (617) {G24,W19,D2,L12,V0,M1} R(426,180);f { hskp4, alpha51, ! c2_1( a12 ),
% 1.84/2.21 hskp12, c2_1( a1 ), c2_1( a3 ), alpha45, ! c3_1( a12 ), ! c3_1( a1 ),
% 1.84/2.21 c3_1( a3 ), alpha52, ! c0_1( a3 ) }.
% 1.84/2.21 (615) {G24,W19,D2,L12,V0,M1} R(426,211);f;f;f;f;f;f { hskp4, alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a3 ), c2_1( a8 ), alpha45, ! c3_1( a12 ), c3_1
% 1.84/2.21 ( a3 ), ! c3_1( a8 ), alpha22, ! c0_1( a3 ) }.
% 1.84/2.21 (614) {G24,W19,D2,L12,V0,M1} R(426,271);f;f;f;f;f;f { hskp4, alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a3 ), c2_1( a6 ), alpha45, ! c3_1( a12 ), c3_1
% 1.84/2.21 ( a3 ), ! c3_1( a6 ), alpha42, ! c0_1( a3 ) }.
% 1.84/2.21 (612) {G24,W19,D2,L12,V0,M1} R(426,243);f;f;f;f;f;f { hskp4, alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a3 ), c2_1( a5 ), alpha45, ! c3_1( a12 ), c3_1
% 1.84/2.21 ( a3 ), ! c3_1( a5 ), alpha36, ! c0_1( a3 ) }.
% 1.84/2.21 (426) {G23,W20,D2,L12,V1,M2} F(420);f;f { hskp4, c2_1( a3 ), alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( X ), ! c3_1( a12 ), alpha45, ! c3_1( X ), c3_1
% 1.84/2.21 ( a3 ), c0_1( X ), ! c0_1( a3 ) }.
% 1.84/2.21 (416) {G22,W20,D2,L12,V1,M2} R(269,243);f;f;f;f;f;f { hskp4, c2_1( a3 ),
% 1.84/2.21 alpha51, ! c2_1( X ), hskp12, c2_1( a5 ), ! c3_1( X ), c3_1( a3 ), ! c3_1
% 1.84/2.21 ( a5 ), alpha36, ! c0_1( a3 ), ! c0_1( X ) }.
% 1.84/2.21 (325) {G22,W20,D2,L13,V1,M1} R(243,214);f { hskp4, c2_1( a3 ), ! c3_1( a5 )
% 1.84/2.21 , alpha36, c3_1( a3 ), alpha51, ! c2_1( X ), hskp12, c2_1( a5 ), ! c3_1(
% 1.84/2.21 X ), hskp2, hskp9, ! c0_1( a3 ) }.
% 1.84/2.21 (471) {G25,W19,D2,L13,V0,M1} R(463,163);f { hskp4, hskp12, alpha50, ! c2_1
% 1.84/2.21 ( a12 ), alpha45, c2_1( a7 ), c2_1( a6 ), ! c3_1( a12 ), alpha42, c3_1(
% 1.84/2.21 a7 ), hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (478) {G25,W19,D2,L13,V0,M1} R(466,163);f { hskp4, hskp12, alpha50, ! c2_1
% 1.84/2.21 ( a12 ), alpha45, c2_1( a7 ), c2_1( a8 ), ! c3_1( a12 ), alpha22, c3_1(
% 1.84/2.21 a7 ), hskp6, hskp13, ! c3_1( a8 ) }.
% 1.84/2.21 (480) {G25,W19,D2,L13,V0,M1} R(468,163);f { hskp4, hskp12, alpha50, ! c2_1
% 1.84/2.21 ( a12 ), alpha45, c2_1( a1 ), c2_1( a7 ), ! c3_1( a12 ), alpha52, ! c3_1
% 1.84/2.21 ( a1 ), hskp6, hskp13, c3_1( a7 ) }.
% 1.84/2.21 (506) {G25,W19,D2,L13,V0,M1} R(499,163);f { hskp4, hskp12, alpha48, c2_1(
% 1.84/2.21 a10 ), alpha45, ! c2_1( a12 ), c2_1( a6 ), ! c3_1( a12 ), alpha42, c3_1(
% 1.84/2.21 a10 ), hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (522) {G25,W19,D2,L13,V0,M1} R(501,163);f { hskp4, hskp12, alpha48, c2_1(
% 1.84/2.21 a10 ), alpha45, ! c2_1( a12 ), c2_1( a5 ), ! c3_1( a12 ), alpha36, c3_1(
% 1.84/2.21 a10 ), hskp6, hskp13, ! c3_1( a5 ) }.
% 1.84/2.21 (526) {G25,W19,D2,L13,V0,M1} R(502,163);f { hskp4, hskp12, alpha48, c2_1(
% 1.84/2.21 a10 ), alpha45, ! c2_1( a12 ), c2_1( a8 ), ! c3_1( a12 ), alpha22, c3_1(
% 1.84/2.21 a10 ), hskp6, hskp13, ! c3_1( a8 ) }.
% 1.84/2.21 (528) {G25,W19,D2,L13,V0,M1} R(504,163);f { hskp4, hskp12, alpha48, c2_1(
% 1.84/2.21 a10 ), alpha45, ! c2_1( a12 ), c2_1( a1 ), ! c3_1( a12 ), alpha52, c3_1(
% 1.84/2.21 a10 ), hskp6, hskp13, ! c3_1( a1 ) }.
% 1.84/2.21 (321) {G23,W19,D2,L13,V1,M2} R(319,214);f { hskp4, c2_1( a3 ), alpha26, !
% 1.84/2.21 c3_1( a15 ), alpha51, hskp6, ! c2_1( X ), hskp12, c2_1( a15 ), hskp2,
% 1.84/2.21 hskp9, ! c3_1( X ), c3_1( a3 ) }.
% 1.84/2.21 (449) {G23,W19,D2,L13,V1,M1} R(440,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a7 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( X ), c3_1( a7 ),
% 1.84/2.21 hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (454) {G23,W19,D2,L13,V1,M1} R(401,163);f { hskp4, alpha48, hskp12, ! c2_1
% 1.84/2.21 ( X ), c2_1( a10 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( X ), c3_1( a10 )
% 1.84/2.21 , hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (554) {G23,W19,D2,L13,V1,M2} R(292,163);f;r(1) { hskp12, hskp2, hskp9,
% 1.84/2.21 hskp4, c2_1( a10 ), ! c2_1( X ), c2_1( a15 ), alpha26, alpha48, hskp6,
% 1.84/2.21 c3_1( a10 ), ! c3_1( X ), ! c3_1( a15 ) }.
% 1.84/2.21 (578) {G23,W19,D2,L13,V1,M1} R(425,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a3 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( X ), c3_1( a3
% 1.84/2.21 ), hskp6, hskp13, ! c0_1( X ) }.
% 1.84/2.21 (584) {G23,W19,D2,L12,V0,M1} R(309,215);f;f;f;f;f;f { hskp12, ! c2_1( a12 )
% 1.84/2.21 , c2_1( a7 ), alpha45, ! c3_1( a12 ), hskp4, ! c3_1( a15 ), ! c3_1( a7 )
% 1.84/2.21 , alpha26, alpha50, c2_1( a15 ), c0_1( a12 ) }.
% 1.84/2.21 (309) {G22,W19,D2,L12,V0,M1} R(215,251);f { hskp12, ! c2_1( a12 ), c2_1( a7
% 1.84/2.21 ), ! c3_1( a12 ), alpha45, ! c3_1( a7 ), hskp4, ! c3_1( a15 ), c0_1( a12
% 1.84/2.21 ), alpha26, alpha50, ! c0_1( a15 ) }.
% 1.84/2.21 (581) {G23,W19,D2,L12,V0,M1} R(308,215);f;f;f;f;f;f { hskp12, ! c2_1( a12 )
% 1.84/2.21 , c2_1( a7 ), alpha45, ! c3_1( a12 ), hskp4, ! c3_1( a5 ), ! c3_1( a7 ),
% 1.84/2.21 alpha36, alpha50, c2_1( a5 ), c0_1( a12 ) }.
% 1.84/2.21 (308) {G22,W19,D2,L12,V0,M1} R(215,244);f { hskp12, ! c2_1( a12 ), c2_1( a7
% 1.84/2.21 ), ! c3_1( a12 ), alpha45, ! c3_1( a7 ), hskp4, ! c3_1( a5 ), c0_1( a12
% 1.84/2.21 ), alpha36, alpha50, ! c0_1( a5 ) }.
% 1.84/2.21 (469) {G25,W19,D2,L12,V0,M1} R(463,215);f;f;f;f;f { hskp4, hskp12, alpha50
% 1.84/2.21 , ! c2_1( a12 ), alpha45, c2_1( a7 ), c2_1( a6 ), ! c3_1( a12 ), alpha42
% 1.84/2.21 , ! c3_1( a7 ), ! c3_1( a6 ), c0_1( a12 ) }.
% 1.84/2.21 (476) {G25,W19,D2,L12,V0,M1} R(466,215);f;f;f;f;f { hskp4, hskp12, alpha50
% 1.84/2.21 , ! c2_1( a12 ), alpha45, c2_1( a7 ), c2_1( a8 ), ! c3_1( a12 ), alpha22
% 1.84/2.21 , ! c3_1( a7 ), ! c3_1( a8 ), c0_1( a12 ) }.
% 1.84/2.21 (505) {G25,W19,D2,L12,V0,M1} R(499,215);f;f;f;f;f { hskp4, hskp12, alpha48
% 1.84/2.21 , c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a6 ), ! c3_1( a12 ), alpha42
% 1.84/2.21 , ! c3_1( a10 ), ! c3_1( a6 ), c0_1( a12 ) }.
% 1.84/2.21 (509) {G25,W19,D2,L12,V0,M1} R(500,215);f;f;f;f;f { hskp4, hskp12, alpha48
% 1.84/2.21 , c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a15 ), ! c3_1( a12 ),
% 1.84/2.21 alpha26, ! c3_1( a10 ), ! c3_1( a15 ), c0_1( a12 ) }.
% 1.84/2.21 (520) {G25,W19,D2,L12,V0,M1} R(501,215);f;f;f;f;f { hskp4, hskp12, alpha48
% 1.84/2.21 , c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a5 ), ! c3_1( a12 ), alpha36
% 1.84/2.21 , ! c3_1( a10 ), ! c3_1( a5 ), c0_1( a12 ) }.
% 1.84/2.21 (524) {G25,W19,D2,L12,V0,M1} R(502,215);f;f;f;f;f { hskp4, hskp12, alpha48
% 1.84/2.21 , c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a8 ), ! c3_1( a12 ), alpha22
% 1.84/2.21 , ! c3_1( a10 ), ! c3_1( a8 ), c0_1( a12 ) }.
% 1.84/2.21 (579) {G24,W18,D2,L13,V0,M1} R(577,163);f;f { hskp4, alpha51, hskp12, !
% 1.84/2.21 c2_1( a12 ), c2_1( a3 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( a12 ),
% 1.84/2.21 alpha45, hskp6, hskp13, c3_1( a3 ) }.
% 1.84/2.21 (577) {G23,W18,D2,L12,V0,M1} R(425,315);f;f;f;f;f;f { hskp4, alpha51, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a3 ), c2_1( a8 ), ! c3_1( a12 ), hskp10,
% 1.84/2.21 hskp11, c3_1( a3 ), alpha45, ! c0_1( a3 ) }.
% 1.84/2.21 (425) {G22,W19,D2,L12,V1,M2} R(269,172);r(170) { hskp4, c2_1( a3 ), alpha51
% 1.84/2.21 , ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), c3_1( a3 ), hskp10,
% 1.84/2.21 hskp11, ! c0_1( X ), ! c0_1( a3 ) }.
% 1.84/2.21 (540) {G23,W19,D2,L12,V1,M1} R(394,163);f;r(1) { hskp4, alpha48, hskp12, !
% 1.84/2.21 c2_1( X ), c2_1( a10 ), c2_1( a15 ), alpha26, ! c3_1( a15 ), ! c3_1( X )
% 1.84/2.21 , c3_1( a10 ), hskp6, ! c0_1( X ) }.
% 1.84/2.21 (574) {G24,W16,D2,L12,V0,M1} R(341,380);f;f;f;f;f;f;f;f;f;f { hskp4,
% 1.84/2.21 alpha36, alpha50, c2_1( a7 ), hskp6, hskp13, hskp12, ! c2_1( a8 ), c2_1(
% 1.84/2.21 a5 ), hskp10, hskp11, ! c3_1( a5 ) }.
% 1.84/2.21 (360) {G23,W18,D2,L13,V0,M1} R(248,163);f { hskp4, c2_1( a10 ), alpha36,
% 1.84/2.21 alpha48, hskp12, ! c2_1( a8 ), c2_1( a5 ), hskp10, hskp11, c3_1( a10 ),
% 1.84/2.21 hskp6, hskp13, ! c3_1( a5 ) }.
% 1.84/2.21 (408) {G23,W18,D2,L13,V0,M1} R(264,163);f { hskp4, c2_1( a10 ), alpha48,
% 1.84/2.21 alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, c3_1( a10 ),
% 1.84/2.21 hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (446) {G23,W18,D2,L13,V0,M1} R(283,163);f { hskp4, c2_1( a7 ), alpha50,
% 1.84/2.21 alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, c3_1( a7 ),
% 1.84/2.21 hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (451) {G24,W18,D2,L13,V0,M1} R(448,163);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( a12 ), c2_1( a7 ), hskp10, hskp11, c2_1( a8 ), alpha45, ! c3_1( a12 ),
% 1.84/2.21 hskp6, hskp13, c3_1( a7 ) }.
% 1.84/2.21 (455) {G24,W18,D2,L13,V0,M1} R(453,163);f { hskp4, alpha48, hskp12, c2_1(
% 1.84/2.21 a10 ), ! c2_1( a12 ), hskp10, hskp11, c2_1( a8 ), alpha45, c3_1( a10 ),
% 1.84/2.21 hskp6, hskp13, ! c3_1( a12 ) }.
% 1.84/2.21 (569) {G23,W18,D2,L13,V0,M1} R(326,163);f;f { hskp4, c2_1( a3 ), alpha36,
% 1.84/2.21 c3_1( a3 ), alpha51, hskp12, ! c2_1( a8 ), c2_1( a5 ), hskp10, hskp11,
% 1.84/2.21 hskp6, hskp13, ! c3_1( a5 ) }.
% 1.84/2.21 (570) {G23,W18,D2,L13,V0,M1} R(301,163);f;f { hskp4, c2_1( a3 ), c3_1( a3 )
% 1.84/2.21 , alpha51, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11,
% 1.84/2.21 hskp6, hskp13, ! c3_1( a6 ) }.
% 1.84/2.21 (300) {G22,W20,D2,L13,V1,M1} R(271,214);f { hskp4, c2_1( a3 ), ! c3_1( a6 )
% 1.84/2.21 , c3_1( a3 ), alpha51, alpha42, ! c2_1( X ), hskp12, c2_1( a6 ), ! c3_1(
% 1.84/2.21 X ), hskp2, hskp9, ! c0_1( a3 ) }.
% 1.84/2.21 (301) {G22,W18,D2,L12,V0,M1} R(271,216);f { hskp4, c2_1( a3 ), ! c3_1( a6 )
% 1.84/2.21 , c3_1( a3 ), alpha51, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10
% 1.84/2.21 , hskp11, ! c0_1( a3 ) }.
% 1.84/2.21 (326) {G22,W18,D2,L12,V0,M1} R(243,216);f { hskp4, c2_1( a3 ), ! c3_1( a5 )
% 1.84/2.21 , alpha36, c3_1( a3 ), alpha51, hskp12, ! c2_1( a8 ), c2_1( a5 ), hskp10
% 1.84/2.21 , hskp11, ! c0_1( a3 ) }.
% 1.84/2.21 (331) {G22,W18,D2,L12,V0,M1} R(240,216);f { hskp4, c2_1( a7 ), ! c3_1( a11
% 1.84/2.21 ), ! c2_1( a11 ), alpha46, alpha50, hskp12, ! c2_1( a8 ), ! c3_1( a7 ),
% 1.84/2.21 hskp10, hskp11, ! c0_1( a11 ) }.
% 1.84/2.21 (298) {G22,W20,D2,L13,V1,M1} R(211,214);f { hskp4, c2_1( a3 ), ! c3_1( a8 )
% 1.84/2.21 , alpha22, c3_1( a3 ), alpha51, ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1(
% 1.84/2.21 X ), hskp2, hskp9, ! c0_1( a3 ) }.
% 1.84/2.21 (511) {G25,W18,D2,L12,V0,M1} R(500,163);f;r(1) { hskp4, hskp12, alpha48,
% 1.84/2.21 c2_1( a10 ), alpha45, ! c2_1( a12 ), c2_1( a15 ), ! c3_1( a12 ), alpha26
% 1.84/2.21 , c3_1( a10 ), hskp6, ! c3_1( a15 ) }.
% 1.84/2.21 (564) {G24,W18,D2,L12,V1,M2} F(562);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a7 ), alpha22, alpha50, ! c2_1( X ), c2_1( a8 ), ! c3_1( a7 ), ! c3_1( a8
% 1.84/2.21 ), ! c3_1( X ) }.
% 1.84/2.21 (567) {G24,W18,D2,L12,V1,M2} F(565);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a10 ), alpha22, alpha48, ! c2_1( X ), c2_1( a8 ), ! c3_1( a10 ), ! c3_1(
% 1.84/2.21 a8 ), ! c3_1( X ) }.
% 1.84/2.21 (295) {G22,W18,D2,L12,V1,M1} R(214,210);f { hskp12, ! c2_1( X ), c2_1( a8 )
% 1.84/2.21 , hskp2, hskp9, hskp4, c2_1( a10 ), ! c3_1( X ), ! c3_1( a8 ), alpha22,
% 1.84/2.21 alpha48, ! c0_1( a10 ) }.
% 1.84/2.21 (294) {G22,W18,D2,L12,V1,M1} R(214,212);f { hskp12, ! c2_1( X ), c2_1( a8 )
% 1.84/2.21 , hskp2, hskp9, hskp4, c2_1( a7 ), ! c3_1( X ), ! c3_1( a8 ), alpha22,
% 1.84/2.21 alpha50, ! c0_1( a7 ) }.
% 1.84/2.21 (475) {G24,W18,D2,L12,V1,M2} F(473);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a7 ), alpha50, alpha42, ! c2_1( X ), c2_1( a6 ), ! c3_1( a7 ), ! c3_1( a6
% 1.84/2.21 ), ! c3_1( X ) }.
% 1.84/2.21 (488) {G24,W18,D2,L12,V1,M2} F(486);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a10 ), alpha48, alpha42, ! c2_1( X ), c2_1( a6 ), ! c3_1( a10 ), ! c3_1(
% 1.84/2.21 a6 ), ! c3_1( X ) }.
% 1.84/2.21 (561) {G24,W18,D2,L12,V1,M2} F(559);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a10 ), alpha36, alpha48, ! c2_1( X ), c2_1( a5 ), ! c3_1( a10 ), ! c3_1(
% 1.84/2.21 a5 ), ! c3_1( X ) }.
% 1.84/2.21 (293) {G22,W18,D2,L12,V1,M1} R(214,242);f { hskp12, ! c2_1( X ), c2_1( a5 )
% 1.84/2.21 , hskp2, hskp9, hskp4, c2_1( a10 ), ! c3_1( X ), ! c3_1( a5 ), alpha36,
% 1.84/2.21 alpha48, ! c0_1( a10 ) }.
% 1.84/2.21 (518) {G24,W18,D2,L12,V1,M2} F(517);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a7 ), ! c2_1( X ), alpha36, alpha50, c2_1( a5 ), ! c3_1( a5 ), ! c3_1( X
% 1.84/2.21 ), ! c3_1( a7 ) }.
% 1.84/2.21 (558) {G26,W17,D2,L12,V1,M2} F(556);f { hskp12, hskp2, hskp4, hskp9,
% 1.84/2.21 alpha26, alpha50, c2_1( a15 ), hskp6, c2_1( a7 ), ! c2_1( X ), ! c3_1(
% 1.84/2.21 a15 ), ! c3_1( X ) }.
% 1.84/2.21 (536) {G24,W18,D2,L12,V1,M2} F(534);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a7 ), ! c2_1( X ), alpha26, alpha50, c2_1( a15 ), ! c3_1( a15 ), ! c3_1(
% 1.84/2.21 X ), ! c3_1( a7 ) }.
% 1.84/2.21 (555) {G24,W18,D2,L12,V1,M2} F(553);f { hskp12, hskp2, hskp4, hskp9, c2_1(
% 1.84/2.21 a10 ), alpha26, alpha48, ! c2_1( X ), c2_1( a15 ), ! c3_1( a10 ), ! c3_1
% 1.84/2.21 ( a15 ), ! c3_1( X ) }.
% 1.84/2.21 (292) {G22,W18,D2,L12,V1,M1} R(214,249);f { hskp12, ! c2_1( X ), c2_1( a15
% 1.84/2.21 ), hskp2, hskp9, hskp4, c2_1( a10 ), ! c3_1( X ), ! c3_1( a15 ), alpha26
% 1.84/2.21 , alpha48, ! c0_1( a10 ) }.
% 1.84/2.21 (400) {G22,W18,D2,L11,V1,M2} R(261,180);f { hskp4, c2_1( a10 ), alpha48, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( a1 ), ! c3_1( X ), ! c3_1( a1 ), alpha52, ! c0_1
% 1.84/2.21 ( X ), ! c0_1( a10 ) }.
% 1.84/2.21 (398) {G22,W18,D2,L11,V1,M2} R(261,210);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), ! c3_1( a8 ),
% 1.84/2.21 alpha22, ! c0_1( X ), ! c0_1( a10 ) }.
% 1.84/2.21 (395) {G22,W18,D2,L11,V1,M2} R(261,242);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, ! c2_1( X ), hskp12, c2_1( a5 ), ! c3_1( X ), ! c3_1( a5 ),
% 1.84/2.21 alpha36, ! c0_1( X ), ! c0_1( a10 ) }.
% 1.84/2.21 (394) {G22,W18,D2,L11,V1,M2} R(261,249);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, ! c2_1( X ), hskp12, c2_1( a15 ), ! c3_1( X ), ! c3_1( a15 ),
% 1.84/2.21 alpha26, ! c0_1( X ), ! c0_1( a10 ) }.
% 1.84/2.21 (291) {G22,W18,D2,L12,V1,M1} R(214,251);f { hskp12, ! c2_1( X ), c2_1( a7 )
% 1.84/2.21 , hskp2, hskp9, hskp4, ! c3_1( a15 ), ! c3_1( X ), ! c3_1( a7 ), alpha26
% 1.84/2.21 , alpha50, ! c0_1( a15 ) }.
% 1.84/2.21 (393) {G22,W18,D2,L11,V1,M2} R(261,263);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, ! c2_1( X ), hskp12, c2_1( a6 ), ! c3_1( X ), ! c3_1( a6 ),
% 1.84/2.21 alpha42, ! c0_1( X ), ! c0_1( a10 ) }.
% 1.84/2.21 (504) {G24,W17,D2,L11,V0,M1} R(402,180);f { hskp4, alpha48, hskp12, c2_1(
% 1.84/2.21 a10 ), ! c2_1( a12 ), alpha45, c2_1( a1 ), ! c3_1( a12 ), ! c3_1( a1 ),
% 1.84/2.21 alpha52, ! c0_1( a10 ) }.
% 1.84/2.21 (502) {G24,W17,D2,L11,V0,M1} R(402,210);f;f;f;f;f { hskp4, alpha48, hskp12
% 1.84/2.21 , c2_1( a10 ), ! c2_1( a12 ), alpha45, c2_1( a8 ), ! c3_1( a12 ), ! c3_1
% 1.84/2.21 ( a8 ), alpha22, ! c0_1( a10 ) }.
% 1.84/2.21 (501) {G24,W17,D2,L11,V0,M1} R(402,242);f;f;f;f;f { hskp4, alpha48, hskp12
% 1.84/2.21 , c2_1( a10 ), ! c2_1( a12 ), alpha45, c2_1( a5 ), ! c3_1( a12 ), ! c3_1
% 1.84/2.21 ( a5 ), alpha36, ! c0_1( a10 ) }.
% 1.84/2.21 (290) {G22,W18,D2,L12,V1,M1} R(214,244);f { hskp12, ! c2_1( X ), c2_1( a7 )
% 1.84/2.21 , hskp2, hskp9, hskp4, ! c3_1( a5 ), ! c3_1( X ), ! c3_1( a7 ), alpha36,
% 1.84/2.21 alpha50, ! c0_1( a5 ) }.
% 1.84/2.21 (500) {G24,W17,D2,L11,V0,M1} R(402,249);f;f;f;f;f { hskp4, alpha48, hskp12
% 1.84/2.21 , c2_1( a10 ), ! c2_1( a12 ), alpha45, c2_1( a15 ), ! c3_1( a12 ), ! c3_1
% 1.84/2.21 ( a15 ), alpha26, ! c0_1( a10 ) }.
% 1.84/2.21 (499) {G24,W17,D2,L11,V0,M1} R(402,263);f;f;f;f;f { hskp4, alpha48, hskp12
% 1.84/2.21 , c2_1( a10 ), ! c2_1( a12 ), alpha45, c2_1( a6 ), ! c3_1( a12 ), ! c3_1
% 1.84/2.21 ( a6 ), alpha42, ! c0_1( a10 ) }.
% 1.84/2.21 (402) {G23,W18,D2,L11,V1,M2} F(388);f;f { hskp4, alpha48, c2_1( a10 ),
% 1.84/2.21 hskp12, ! c2_1( a12 ), c2_1( X ), alpha45, ! c3_1( X ), ! c3_1( a12 ), !
% 1.84/2.21 c0_1( a10 ), c0_1( X ) }.
% 1.84/2.21 (439) {G22,W18,D2,L11,V1,M2} R(281,180);f { hskp4, c2_1( a7 ), alpha50, !
% 1.84/2.21 c2_1( X ), hskp12, c2_1( a1 ), ! c3_1( X ), ! c3_1( a1 ), alpha52, ! c0_1
% 1.84/2.21 ( X ), ! c0_1( a7 ) }.
% 1.84/2.21 (289) {G22,W18,D2,L12,V1,M1} R(214,263);f { hskp12, ! c2_1( X ), c2_1( a6 )
% 1.84/2.21 , hskp2, hskp9, hskp4, c2_1( a10 ), ! c3_1( X ), ! c3_1( a6 ), alpha48,
% 1.84/2.21 alpha42, ! c0_1( a10 ) }.
% 1.84/2.21 (437) {G22,W18,D2,L11,V1,M2} R(281,212);f;f;f;f;f { hskp4, c2_1( a7 ),
% 1.84/2.21 alpha50, ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), ! c3_1( a8 ),
% 1.84/2.21 alpha22, ! c0_1( X ), ! c0_1( a7 ) }.
% 1.84/2.21 (435) {G22,W18,D2,L11,V1,M2} R(281,282);f;f;f;f;f { hskp4, c2_1( a7 ),
% 1.84/2.21 alpha50, ! c2_1( X ), hskp12, c2_1( a6 ), ! c3_1( X ), ! c3_1( a6 ),
% 1.84/2.21 alpha42, ! c0_1( X ), ! c0_1( a7 ) }.
% 1.84/2.21 (468) {G24,W17,D2,L11,V0,M1} R(441,180);f { hskp4, alpha50, hskp12, ! c2_1
% 1.84/2.21 ( a12 ), c2_1( a1 ), alpha45, c2_1( a7 ), ! c3_1( a12 ), ! c3_1( a1 ),
% 1.84/2.21 alpha52, ! c0_1( a7 ) }.
% 1.84/2.21 (466) {G24,W17,D2,L11,V0,M1} R(441,212);f;f;f;f;f { hskp4, alpha50, hskp12
% 1.84/2.21 , ! c2_1( a12 ), c2_1( a7 ), alpha45, c2_1( a8 ), ! c3_1( a12 ), ! c3_1(
% 1.84/2.21 a8 ), alpha22, ! c0_1( a7 ) }.
% 1.84/2.21 (288) {G22,W18,D2,L12,V1,M1} R(214,282);f { hskp12, ! c2_1( X ), c2_1( a6 )
% 1.84/2.21 , hskp2, hskp9, hskp4, c2_1( a7 ), ! c3_1( X ), ! c3_1( a6 ), alpha50,
% 1.84/2.21 alpha42, ! c0_1( a7 ) }.
% 1.84/2.21 (463) {G24,W17,D2,L11,V0,M1} R(441,282);f;f;f;f;f { hskp4, alpha50, hskp12
% 1.84/2.21 , ! c2_1( a12 ), c2_1( a7 ), alpha45, c2_1( a6 ), ! c3_1( a12 ), ! c3_1(
% 1.84/2.21 a6 ), alpha42, ! c0_1( a7 ) }.
% 1.84/2.21 (441) {G23,W18,D2,L11,V1,M2} F(433);f;f { hskp4, alpha50, ! c2_1( a12 ),
% 1.84/2.21 hskp12, c2_1( a7 ), c2_1( X ), alpha45, ! c3_1( X ), ! c3_1( a12 ), !
% 1.84/2.21 c0_1( a7 ), c0_1( X ) }.
% 1.84/2.21 (322) {G23,W17,D2,L12,V0,M1} R(319,216);f { hskp4, c2_1( a3 ), alpha26, !
% 1.84/2.21 c3_1( a15 ), alpha51, hskp6, hskp12, ! c2_1( a8 ), c2_1( a15 ), hskp10,
% 1.84/2.21 hskp11, c3_1( a3 ) }.
% 1.84/2.21 (369) {G23,W17,D2,L12,V0,M1} R(252,163);f;r(1) { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha26, alpha48, hskp12, ! c2_1( a8 ), c2_1( a15 ), hskp10, hskp11, c3_1
% 1.84/2.21 ( a10 ), hskp6, ! c3_1( a15 ) }.
% 1.84/2.21 (453) {G23,W16,D2,L11,V0,M1} R(401,315);f;f;f;f;f;f { hskp4, alpha48, c2_1
% 1.84/2.21 ( a10 ), hskp12, ! c2_1( a12 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( a12 )
% 1.84/2.21 , alpha45, ! c0_1( a10 ) }.
% 1.84/2.21 (401) {G22,W17,D2,L11,V1,M2} R(261,172);r(170) { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), hskp10, hskp11, !
% 1.84/2.21 c0_1( a10 ), ! c0_1( X ) }.
% 1.84/2.21 (448) {G23,W16,D2,L11,V0,M1} R(440,315);f;f;f;f;f;f { hskp4, alpha50, !
% 1.84/2.21 c2_1( a12 ), hskp12, c2_1( a7 ), c2_1( a8 ), hskp10, hskp11, ! c3_1( a12
% 1.84/2.21 ), alpha45, ! c0_1( a7 ) }.
% 1.84/2.21 (450) {G24,W15,D2,L11,V0,M1} R(285,377);f;f;f;f;f;f;f;f;f;f { hskp4,
% 1.84/2.21 alpha26, alpha50, c2_1( a7 ), hskp6, hskp12, ! c2_1( a8 ), c2_1( a15 ),
% 1.84/2.21 hskp10, hskp11, ! c3_1( a15 ) }.
% 1.84/2.21 (440) {G22,W17,D2,L11,V1,M2} R(281,172);r(170) { hskp4, c2_1( a7 ), alpha50
% 1.84/2.21 , ! c2_1( X ), hskp12, c2_1( a8 ), ! c3_1( X ), hskp10, hskp11, ! c0_1(
% 1.84/2.21 a7 ), ! c0_1( X ) }.
% 1.84/2.21 (445) {G23,W16,D2,L11,V0,M1} R(283,216);f;f;f;f;f { hskp4, c2_1( a7 ),
% 1.84/2.21 alpha50, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, !
% 1.84/2.21 c3_1( a7 ), ! c3_1( a6 ) }.
% 1.84/2.21 (283) {G22,W16,D2,L11,V0,M1} R(282,216);f { hskp4, c2_1( a7 ), ! c3_1( a6 )
% 1.84/2.21 , alpha50, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, !
% 1.84/2.21 c0_1( a7 ) }.
% 1.84/2.21 (359) {G23,W16,D2,L11,V0,M1} R(248,216);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha36, alpha48, hskp12, ! c2_1( a8 ), c2_1( a5 ), hskp10, hskp11, !
% 1.84/2.21 c3_1( a10 ), ! c3_1( a5 ) }.
% 1.84/2.21 (281) {G21,W19,D2,L11,V2,M3} R(208,166);f { hskp4, c2_1( a7 ), ! c3_1( X )
% 1.84/2.21 , alpha50, ! c2_1( X ), hskp12, c2_1( Y ), ! c3_1( Y ), ! c0_1( X ), c0_1
% 1.84/2.21 ( Y ), ! c0_1( a7 ) }.
% 1.84/2.21 (368) {G23,W16,D2,L11,V0,M1} R(252,216);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha26, alpha48, hskp12, ! c2_1( a8 ), c2_1( a15 ), hskp10, hskp11, !
% 1.84/2.21 c3_1( a10 ), ! c3_1( a15 ) }.
% 1.84/2.21 (377) {G23,W16,D2,L11,V0,M1} R(254,216);f;f;f;f;f { hskp4, c2_1( a7 ),
% 1.84/2.21 alpha26, alpha50, hskp12, ! c2_1( a8 ), ! c3_1( a15 ), hskp10, hskp11,
% 1.84/2.21 c2_1( a15 ), ! c3_1( a7 ) }.
% 1.84/2.21 (380) {G23,W16,D2,L11,V0,M1} R(256,216);f;f;f;f;f { hskp4, c2_1( a7 ),
% 1.84/2.21 alpha36, alpha50, hskp12, ! c2_1( a8 ), ! c3_1( a5 ), hskp10, hskp11,
% 1.84/2.21 c2_1( a5 ), ! c3_1( a7 ) }.
% 1.84/2.21 (407) {G23,W16,D2,L11,V0,M1} R(264,216);f;f;f;f;f { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha48, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, !
% 1.84/2.21 c3_1( a10 ), ! c3_1( a6 ) }.
% 1.84/2.21 (269) {G21,W21,D2,L12,V2,M3} R(206,166);f { hskp4, c2_1( a3 ), ! c3_1( X )
% 1.84/2.21 , c3_1( a3 ), alpha51, ! c2_1( X ), hskp12, c2_1( Y ), ! c3_1( Y ), !
% 1.84/2.21 c0_1( a3 ), c0_1( Y ), ! c0_1( X ) }.
% 1.84/2.21 (413) {G22,W15,D2,L10,V0,M1} R(343,180);f { hskp1, ! c2_1( a14 ), ! c2_1(
% 1.84/2.21 a1 ), c3_1( a14 ), hskp2, hskp9, alpha33, ! c3_1( a1 ), alpha52, c0_1(
% 1.84/2.21 a14 ) }.
% 1.84/2.21 (412) {G22,W15,D2,L10,V0,M1} R(343,196);f;f;f;f { hskp1, ! c2_1( a14 ), !
% 1.84/2.21 c2_1( a5 ), c3_1( a14 ), hskp2, hskp9, alpha33, ! c3_1( a5 ), alpha36,
% 1.84/2.21 c0_1( a14 ) }.
% 1.84/2.21 (343) {G21,W16,D2,L10,V1,M2} R(220,183) { hskp1, ! c2_1( X ), ! c2_1( a14 )
% 1.84/2.21 , c3_1( a14 ), ! c3_1( X ), hskp2, hskp9, alpha33, c0_1( X ), c0_1( a14 )
% 1.84/2.21 }.
% 1.84/2.21 (404) {G22,W15,D2,L10,V0,M1} R(342,180);f { hskp1, ! c2_1( a1 ), ! c2_1( a5
% 1.84/2.21 ), ! c3_1( a1 ), hskp2, hskp9, alpha36, c3_1( a5 ), alpha52, ! c0_1( a5
% 1.84/2.21 ) }.
% 1.84/2.21 (264) {G22,W16,D2,L11,V0,M1} R(263,216);f { hskp4, c2_1( a10 ), ! c3_1( a6
% 1.84/2.21 ), alpha48, alpha42, hskp12, ! c2_1( a8 ), c2_1( a6 ), hskp10, hskp11, !
% 1.84/2.21 c0_1( a10 ) }.
% 1.84/2.21 (342) {G21,W16,D2,L10,V1,M2} R(220,184) { hskp1, ! c2_1( X ), ! c2_1( a5 )
% 1.84/2.21 , c3_1( a5 ), ! c3_1( X ), hskp2, hskp9, alpha36, c0_1( X ), ! c0_1( a5 )
% 1.84/2.21 }.
% 1.84/2.21 (318) {G23,W15,D2,L11,V0,M1} R(218,163);f { hskp4, c2_1( a10 ), alpha22,
% 1.84/2.21 alpha48, hskp5, c2_1( a8 ), hskp3, c3_1( a10 ), hskp6, hskp13, ! c3_1( a8
% 1.84/2.21 ) }.
% 1.84/2.21 (329) {G23,W15,D2,L11,V0,M1} R(219,163);f { hskp4, c2_1( a7 ), alpha22,
% 1.84/2.21 alpha50, hskp5, c2_1( a8 ), hskp3, c3_1( a7 ), hskp6, hskp13, ! c3_1( a8
% 1.84/2.21 ) }.
% 1.84/2.21 (335) {G23,W15,D2,L11,V0,M1} R(284,163);f { hskp4, c2_1( a7 ), alpha50,
% 1.84/2.21 alpha42, hskp5, c2_1( a6 ), hskp3, c3_1( a7 ), hskp6, hskp13, ! c3_1( a6
% 1.84/2.21 ) }.
% 1.84/2.21 (261) {G21,W19,D2,L11,V2,M3} R(205,166);f { hskp4, c2_1( a10 ), ! c3_1( X )
% 1.84/2.21 , alpha48, ! c2_1( X ), hskp12, c2_1( Y ), ! c3_1( Y ), ! c0_1( X ), c0_1
% 1.84/2.21 ( Y ), ! c0_1( a10 ) }.
% 1.84/2.21 (338) {G23,W15,D2,L11,V0,M1} R(265,163);f { hskp4, c2_1( a10 ), alpha48,
% 1.84/2.21 alpha42, hskp5, c2_1( a6 ), hskp3, c3_1( a10 ), hskp6, hskp13, ! c3_1( a6
% 1.84/2.21 ) }.
% 1.84/2.21 (381) {G23,W15,D2,L11,V0,M1} R(302,163);f;f { hskp4, c2_1( a3 ), c3_1( a3 )
% 1.84/2.21 , alpha51, alpha42, hskp5, c2_1( a6 ), hskp3, hskp6, hskp13, ! c3_1( a6 )
% 1.84/2.21 }.
% 1.84/2.21 (382) {G23,W15,D2,L11,V0,M1} R(299,163);f;f { hskp4, c2_1( a3 ), alpha22,
% 1.84/2.21 c3_1( a3 ), alpha51, hskp5, c2_1( a8 ), hskp3, hskp6, hskp13, ! c3_1( a8
% 1.84/2.21 ) }.
% 1.84/2.21 (299) {G22,W15,D2,L10,V0,M1} R(211,189);f;f { hskp4, c2_1( a3 ), ! c3_1( a8
% 1.84/2.21 ), alpha22, c3_1( a3 ), alpha51, hskp5, c2_1( a8 ), hskp3, ! c0_1( a3 )
% 1.84/2.21 }.
% 1.84/2.21 (302) {G22,W15,D2,L10,V0,M1} R(271,193);f;f { hskp4, c2_1( a3 ), ! c3_1( a6
% 1.84/2.21 ), c3_1( a3 ), alpha51, alpha42, hskp5, c2_1( a6 ), hskp3, ! c0_1( a3 )
% 1.84/2.21 }.
% 1.84/2.21 (332) {G22,W15,D2,L10,V0,M1} R(240,163);f { hskp4, c2_1( a7 ), ! c3_1( a11
% 1.84/2.21 ), ! c2_1( a11 ), alpha46, alpha50, c3_1( a7 ), hskp6, hskp13, ! c0_1(
% 1.84/2.21 a11 ) }.
% 1.84/2.21 (349) {G22,W15,D2,L10,V0,M1} R(239,163);f;f { hskp4, c2_1( a3 ), ! c3_1(
% 1.84/2.21 a11 ), ! c2_1( a11 ), alpha46, c3_1( a3 ), alpha51, hskp6, hskp13, ! c0_1
% 1.84/2.21 ( a11 ) }.
% 1.84/2.21 (270) {G21,W15,D2,L9,V0,M1} R(206,175) { hskp4, c2_1( a3 ), ! c3_1( a9 ), !
% 1.84/2.21 c0_1( a3 ), c3_1( a3 ), alpha51, ! c2_1( a9 ), alpha49, ! c0_1( a9 ) }.
% 1.84/2.21 (256) {G22,W16,D2,L11,V0,M1} R(244,216);f { hskp4, c2_1( a7 ), ! c3_1( a5 )
% 1.84/2.21 , alpha36, alpha50, hskp12, ! c2_1( a8 ), ! c3_1( a7 ), hskp10, hskp11, !
% 1.84/2.21 c0_1( a5 ) }.
% 1.84/2.21 (347) {G21,W15,D2,L9,V0,M1} R(223,179) { hskp1, ! c2_1( a3 ), ! c2_1( a5 )
% 1.84/2.21 , c3_1( a5 ), c0_1( a3 ), alpha36, c3_1( a3 ), alpha51, ! c0_1( a5 ) }.
% 1.84/2.21 (348) {G21,W15,D2,L9,V0,M1} R(225,179) { hskp1, ! c2_1( a14 ), ! c2_1( a3 )
% 1.84/2.21 , c3_1( a14 ), c0_1( a14 ), alpha33, c3_1( a3 ), alpha51, c0_1( a3 ) }.
% 1.84/2.21 (286) {G23,W14,D2,L10,V0,M1} R(255,192);f;f { hskp4, c2_1( a7 ), alpha26,
% 1.84/2.21 alpha50, ! c3_1( a15 ), hskp6, hskp5, c2_1( a15 ), hskp3, c3_1( a7 ) }.
% 1.84/2.21 (323) {G23,W14,D2,L10,V0,M1} R(319,192);f;f { hskp4, c2_1( a3 ), alpha26, !
% 1.84/2.21 c3_1( a15 ), alpha51, hskp6, hskp5, c2_1( a15 ), hskp3, c3_1( a3 ) }.
% 1.84/2.21 (254) {G22,W16,D2,L11,V0,M1} R(251,216);f { hskp4, c2_1( a7 ), ! c3_1( a15
% 1.84/2.21 ), alpha26, alpha50, hskp12, ! c2_1( a8 ), ! c3_1( a7 ), hskp10, hskp11
% 1.84/2.21 , ! c0_1( a15 ) }.
% 1.84/2.21 (346) {G23,W14,D2,L10,V0,M1} R(253,163);f;r(1) { hskp4, c2_1( a10 ),
% 1.84/2.21 alpha26, alpha48, hskp5, c2_1( a15 ), hskp3, c3_1( a10 ), hskp6, ! c3_1(
% 1.84/2.21 a15 ) }.
% 1.84/2.21 (374) {G22,W13,D2,L9,V0,M1} R(266,180);f { hskp1, ! c2_1( a11 ), ! c2_1( a1
% 1.84/2.21 ), alpha46, c3_1( a11 ), hskp2, hskp9, alpha52, ! c3_1( a1 ) }.
% 1.84/2.21 (373) {G22,W13,D2,L9,V0,M1} R(266,196);f;f;f;f { hskp1, ! c2_1( a11 ), !
% 1.84/2.21 c2_1( a5 ), alpha46, c3_1( a11 ), hskp2, hskp9, alpha36, ! c3_1( a5 ) }.
% 1.84/2.21 (266) {G21,W14,D2,L9,V1,M1} R(221,167);f { hskp1, ! c2_1( X ), ! c2_1( a11
% 1.84/2.21 ), c3_1( a11 ), alpha46, ! c3_1( X ), hskp2, hskp9, c0_1( X ) }.
% 1.84/2.21 (252) {G22,W16,D2,L11,V0,M1} R(249,216);f { hskp4, c2_1( a10 ), ! c3_1( a15
% 1.84/2.21 ), alpha26, alpha48, hskp12, ! c2_1( a8 ), c2_1( a15 ), hskp10, hskp11,
% 1.84/2.21 ! c0_1( a10 ) }.
% 1.84/2.21 (365) {G22,W13,D2,L9,V0,M1} R(277,180);f { hskp1, ! c2_1( a1 ), ! c2_1( a4
% 1.84/2.21 ), alpha47, ! c3_1( a1 ), hskp2, hskp9, alpha52, c3_1( a4 ) }.
% 1.84/2.21 (364) {G22,W13,D2,L9,V0,M1} R(277,196);f;f;f;f { hskp1, ! c2_1( a4 ), !
% 1.84/2.21 c2_1( a5 ), alpha47, c3_1( a4 ), hskp2, hskp9, alpha36, ! c3_1( a5 ) }.
% 1.84/2.21 (277) {G21,W14,D2,L9,V1,M1} R(224,167);f { hskp1, ! c2_1( X ), ! c2_1( a4 )
% 1.84/2.21 , c3_1( a4 ), alpha47, ! c3_1( X ), hskp2, hskp9, c0_1( X ) }.
% 1.84/2.21 (356) {G23,W11,D2,L8,V0,M1} R(354,199);f;f;f;f { hskp1, ! c2_1( a1 ),
% 1.84/2.21 alpha49, ! c2_1( a9 ), hskp2, hskp9, alpha52, ! c3_1( a1 ) }.
% 1.84/2.21 (248) {G22,W16,D2,L11,V0,M1} R(242,216);f { hskp4, c2_1( a10 ), ! c3_1( a5
% 1.84/2.21 ), alpha36, alpha48, hskp12, ! c2_1( a8 ), c2_1( a5 ), hskp10, hskp11, !
% 1.84/2.21 c0_1( a10 ) }.
% 1.84/2.21 (355) {G23,W11,D2,L8,V0,M1} R(353,199);f;f;f;f { hskp1, ! c2_1( a5 ),
% 1.84/2.21 alpha49, ! c2_1( a9 ), hskp2, hskp9, alpha36, ! c3_1( a5 ) }.
% 1.84/2.21 (279) {G21,W14,D2,L9,V1,M1} R(227,167);f { hskp1, ! c2_1( X ), ! c2_1( a9 )
% 1.84/2.21 , c3_1( a9 ), alpha49, ! c3_1( X ), hskp2, hskp9, c0_1( X ) }.
% 1.84/2.21 (239) {G21,W15,D2,L9,V0,M1} R(201,179) { hskp4, c2_1( a3 ), ! c3_1( a11 ),
% 1.84/2.21 ! c0_1( a11 ), ! c2_1( a11 ), alpha46, c3_1( a3 ), alpha51, ! c0_1( a3 )
% 1.84/2.21 }.
% 1.84/2.21 (226) {G20,W14,D2,L8,V1,M1} R(168,179) { ! c2_1( a3 ), hskp1, ! c2_1( X ),
% 1.84/2.21 c3_1( X ), c0_1( a3 ), c3_1( a3 ), alpha51, c1_1( X ) }.
% 1.84/2.21 (225) {G20,W14,D2,L8,V1,M1} R(168,183) { ! c2_1( X ), hskp1, ! c2_1( a14 )
% 1.84/2.21 , c3_1( a14 ), c0_1( X ), c0_1( a14 ), alpha33, ! c1_1( X ) }.
% 1.84/2.21 (223) {G20,W14,D2,L8,V1,M1} R(168,184) { ! c2_1( X ), hskp1, ! c2_1( a5 ),
% 1.84/2.21 c3_1( a5 ), c0_1( X ), ! c0_1( a5 ), alpha36, ! c1_1( X ) }.
% 1.84/2.21 (253) {G22,W13,D2,L9,V0,M1} R(249,192);f;f { hskp4, c2_1( a10 ), ! c3_1(
% 1.84/2.21 a15 ), alpha26, alpha48, hskp5, c2_1( a15 ), hskp3, ! c0_1( a10 ) }.
% 1.84/2.21 (220) {G20,W15,D2,L9,V2,M1} R(168,167);f { ! c2_1( X ), hskp1, ! c2_1( Y )
% 1.84/2.21 , c3_1( Y ), c0_1( X ), ! c3_1( X ), hskp2, hskp9, c1_1( Y ) }.
% 1.84/2.21 (257) {G22,W13,D2,L9,V0,M1} R(244,163);f { hskp4, c2_1( a7 ), ! c3_1( a5 )
% 1.84/2.21 , alpha36, alpha50, c3_1( a7 ), hskp6, hskp13, ! c0_1( a5 ) }.
% 1.84/2.21 (265) {G22,W13,D2,L9,V0,M1} R(263,193);f;f { hskp4, c2_1( a10 ), ! c3_1( a6
% 1.84/2.21 ), alpha48, alpha42, hskp5, c2_1( a6 ), hskp3, ! c0_1( a10 ) }.
% 1.84/2.21 (284) {G22,W13,D2,L9,V0,M1} R(282,193);f;f { hskp4, c2_1( a7 ), ! c3_1( a6
% 1.84/2.21 ), alpha50, alpha42, hskp5, c2_1( a6 ), hskp3, ! c0_1( a7 ) }.
% 1.84/2.21 (240) {G21,W13,D2,L8,V0,M1} R(201,177);f { hskp4, c2_1( a7 ), ! c3_1( a11 )
% 1.84/2.21 , ! c0_1( a11 ), ! c2_1( a11 ), alpha46, alpha50, ! c0_1( a7 ) }.
% 1.84/2.21 (219) {G22,W13,D2,L9,V0,M1} R(212,189);f;f { hskp4, c2_1( a7 ), ! c3_1( a8
% 1.84/2.21 ), alpha22, alpha50, hskp5, c2_1( a8 ), hskp3, ! c0_1( a7 ) }.
% 1.84/2.21 (238) {G21,W13,D2,L8,V0,M1} R(201,169);f { hskp4, c2_1( a10 ), ! c3_1( a11
% 1.84/2.21 ), ! c0_1( a10 ), ! c2_1( a11 ), alpha46, alpha48, ! c0_1( a11 ) }.
% 1.84/2.21 (243) {G21,W13,D2,L8,V0,M1} R(203,179) { hskp4, c2_1( a3 ), ! c3_1( a5 ), !
% 1.84/2.21 c0_1( a3 ), alpha36, c3_1( a3 ), alpha51, ! c0_1( a5 ) }.
% 1.84/2.21 (319) {G22,W12,D2,L8,V0,M1} R(250,163);f;f;r(1) { hskp4, c2_1( a3 ), ! c3_1
% 1.84/2.21 ( a15 ), alpha26, c3_1( a3 ), alpha51, hskp6, ! c0_1( a15 ) }.
% 1.84/2.21 (250) {G21,W13,D2,L8,V0,M1} R(204,179) { hskp4, c2_1( a3 ), ! c3_1( a15 ),
% 1.84/2.21 ! c0_1( a15 ), alpha26, c3_1( a3 ), alpha51, ! c0_1( a3 ) }.
% 1.84/2.21 (218) {G22,W13,D2,L9,V0,M1} R(210,189);f;f { hskp4, c2_1( a10 ), ! c3_1( a8
% 1.84/2.21 ), alpha22, alpha48, hskp5, c2_1( a8 ), hskp3, ! c0_1( a10 ) }.
% 1.84/2.21 (262) {G21,W13,D2,L8,V0,M1} R(205,175) { hskp4, c2_1( a10 ), ! c3_1( a9 ),
% 1.84/2.21 ! c0_1( a10 ), alpha48, ! c2_1( a9 ), alpha49, ! c0_1( a9 ) }.
% 1.84/2.21 (268) {G21,W13,D2,L8,V0,M1} R(221,179) { hskp1, ! c2_1( a11 ), ! c2_1( a3 )
% 1.84/2.21 , c3_1( a11 ), alpha46, c3_1( a3 ), alpha51, c0_1( a3 ) }.
% 1.84/2.21 (314) {G21,W13,D2,L8,V0,M1} R(215,180);f { hskp12, ! c2_1( a12 ), c2_1( a1
% 1.84/2.21 ), ! c3_1( a12 ), alpha45, ! c3_1( a1 ), alpha52, c0_1( a12 ) }.
% 1.84/2.21 (315) {G21,W12,D2,L8,V0,M1} R(215,172);r(170) { hskp12, ! c2_1( a12 ), c2_1
% 1.84/2.21 ( a8 ), alpha45, ! c3_1( a12 ), hskp10, hskp11, c0_1( a12 ) }.
% 1.84/2.21 (215) {G20,W14,D2,L8,V1,M2} R(166,185) { ! c2_1( a12 ), hskp12, c2_1( X ),
% 1.84/2.21 ! c3_1( a12 ), ! c3_1( X ), alpha45, c0_1( X ), c0_1( a12 ) }.
% 1.84/2.21 (271) {G21,W13,D2,L8,V0,M1} R(206,178);f { hskp4, c2_1( a3 ), ! c3_1( a6 )
% 1.84/2.21 , ! c0_1( a3 ), c3_1( a3 ), alpha51, alpha42, ! c0_1( a6 ) }.
% 1.84/2.21 (274) {G21,W13,D2,L8,V0,M1} R(222,183) { hskp1, ! c2_1( a12 ), ! c2_1( a14
% 1.84/2.21 ), c3_1( a14 ), alpha45, c0_1( a12 ), alpha33, c0_1( a14 ) }.
% 1.84/2.21 (272) {G21,W13,D2,L8,V0,M1} R(222,184) { hskp1, ! c2_1( a12 ), ! c2_1( a5 )
% 1.84/2.21 , c3_1( a5 ), alpha45, c0_1( a12 ), alpha36, ! c0_1( a5 ) }.
% 1.84/2.21 (276) {G21,W13,D2,L8,V0,M1} R(207,177);f { hskp4, c2_1( a7 ), ! c3_1( a9 )
% 1.84/2.21 , ! c0_1( a7 ), ! c2_1( a9 ), alpha49, alpha50, ! c0_1( a9 ) }.
% 1.84/2.21 (213) {G20,W20,D2,L11,V3,M1} R(166,165);f { ! c2_1( X ), hskp12, c2_1( Y )
% 1.84/2.21 , ! c3_1( X ), ! c3_1( Y ), hskp4, c2_1( Z ), ! c0_1( Z ), c0_1( Y ), !
% 1.84/2.21 c0_1( X ), ! c1_1( Z ) }.
% 1.84/2.21 (278) {G21,W13,D2,L8,V0,M1} R(224,179) { hskp1, ! c2_1( a3 ), ! c2_1( a4 )
% 1.84/2.21 , c3_1( a4 ), alpha47, c3_1( a3 ), alpha51, c0_1( a3 ) }.
% 1.84/2.21 (280) {G21,W13,D2,L8,V0,M1} R(227,179) { hskp1, ! c2_1( a3 ), ! c2_1( a9 )
% 1.84/2.21 , c3_1( a9 ), alpha49, c3_1( a3 ), alpha51, c0_1( a3 ) }.
% 1.84/2.21 (296) {G21,W12,D2,L8,V1,M2} R(214,180);f { hskp12, ! c2_1( X ), c2_1( a1 )
% 1.84/2.21 , hskp2, hskp9, alpha52, ! c3_1( X ), ! c3_1( a1 ) }.
% 1.84/2.21 (297) {G21,W11,D2,L8,V1,M1} R(214,172);r(170) { hskp12, ! c2_1( X ), c2_1(
% 1.84/2.21 a8 ), hskp2, hskp9, hskp10, hskp11, ! c3_1( X ) }.
% 1.84/2.21 (211) {G21,W13,D2,L8,V0,M1} R(202,179) { hskp4, c2_1( a3 ), ! c3_1( a8 ), !
% 1.84/2.21 c0_1( a3 ), alpha22, c3_1( a3 ), alpha51, ! c0_1( a8 ) }.
% 1.84/2.21 (214) {G20,W13,D2,L8,V2,M1} R(166,167);f;f { ! c2_1( X ), hskp12, c2_1( Y )
% 1.84/2.21 , ! c3_1( X ), ! c3_1( Y ), hskp2, hskp9, c0_1( Y ) }.
% 1.84/2.21 (233) {G21,W12,D2,L8,V0,M1} R(228,183) { hskp1, ! c2_1( a14 ), ! c2_1( a8 )
% 1.84/2.21 , hskp10, hskp11, c3_1( a14 ), alpha33, c0_1( a14 ) }.
% 1.84/2.21 (231) {G21,W12,D2,L8,V0,M1} R(228,184) { hskp1, ! c2_1( a5 ), ! c2_1( a8 )
% 1.84/2.21 , hskp10, hskp11, c3_1( a5 ), alpha36, ! c0_1( a5 ) }.
% 1.84/2.21 (255) {G22,W12,D2,L8,V0,M1} R(251,163);f;r(1) { hskp4, c2_1( a7 ), ! c3_1(
% 1.84/2.21 a15 ), alpha26, alpha50, c3_1( a7 ), hskp6, ! c0_1( a15 ) }.
% 1.84/2.21 (209) {G20,W12,D2,L7,V1,M1} R(165,178);f { hskp4, c2_1( X ), ! c3_1( a6 ),
% 1.84/2.21 ! c0_1( a6 ), ! c0_1( X ), alpha42, ! c1_1( X ) }.
% 1.84/2.21 (282) {G21,W11,D2,L7,V0,M1} R(208,178);f { hskp4, c2_1( a7 ), ! c3_1( a6 )
% 1.84/2.21 , ! c0_1( a7 ), alpha50, alpha42, ! c0_1( a6 ) }.
% 1.84/2.21 (208) {G20,W12,D2,L7,V1,M1} R(165,177);f { hskp4, c2_1( a7 ), ! c3_1( X ),
% 1.84/2.21 ! c0_1( X ), ! c0_1( a7 ), alpha50, c1_1( X ) }.
% 1.84/2.21 (227) {G20,W12,D2,L7,V1,M1} R(168,175);f { ! c2_1( X ), hskp1, ! c2_1( a9 )
% 1.84/2.21 , c3_1( a9 ), c0_1( X ), alpha49, ! c1_1( X ) }.
% 1.84/2.21 (224) {G20,W12,D2,L7,V1,M1} R(168,182);f { ! c2_1( X ), hskp1, ! c2_1( a4 )
% 1.84/2.21 , c3_1( a4 ), c0_1( X ), alpha47, ! c1_1( X ) }.
% 1.84/2.21 (207) {G20,W14,D2,L8,V1,M1} R(165,175) { hskp4, c2_1( X ), ! c3_1( a9 ), !
% 1.84/2.21 c0_1( a9 ), ! c0_1( X ), ! c2_1( a9 ), alpha49, ! c1_1( X ) }.
% 1.84/2.21 (275) {G21,W11,D2,L7,V0,M1} R(222,175);f { hskp1, ! c2_1( a12 ), ! c2_1( a9
% 1.84/2.21 ), c3_1( a9 ), alpha45, alpha49, c0_1( a12 ) }.
% 1.84/2.21 (273) {G21,W11,D2,L7,V0,M1} R(222,182);f { hskp1, ! c2_1( a12 ), ! c2_1( a4
% 1.84/2.21 ), c3_1( a4 ), alpha45, alpha47, c0_1( a12 ) }.
% 1.84/2.21 (222) {G20,W12,D2,L7,V1,M1} R(168,185);f { ! c2_1( a12 ), hskp1, ! c2_1( X
% 1.84/2.21 ), c3_1( X ), c0_1( a12 ), alpha45, c1_1( X ) }.
% 1.84/2.21 (267) {G21,W11,D2,L7,V0,M1} R(221,185);f { hskp1, ! c2_1( a11 ), ! c2_1(
% 1.84/2.21 a12 ), c3_1( a11 ), alpha46, alpha45, c0_1( a12 ) }.
% 1.84/2.21 (206) {G20,W14,D2,L8,V1,M1} R(165,179) { hskp4, c2_1( a3 ), ! c3_1( X ), !
% 1.84/2.21 c0_1( X ), ! c0_1( a3 ), c3_1( a3 ), alpha51, c1_1( X ) }.
% 1.84/2.21 (221) {G20,W12,D2,L7,V1,M1} R(168,187);f { ! c2_1( X ), hskp1, ! c2_1( a11
% 1.84/2.21 ), c3_1( a11 ), c0_1( X ), alpha46, ! c1_1( X ) }.
% 1.84/2.21 (263) {G21,W11,D2,L7,V0,M1} R(205,178);f { hskp4, c2_1( a10 ), ! c3_1( a6 )
% 1.84/2.21 , ! c0_1( a10 ), alpha48, alpha42, ! c0_1( a6 ) }.
% 1.84/2.21 (260) {G23,W10,D2,L8,V0,M1} R(246,180);f { hskp0, hskp1, hskp7, ! c2_1( a1
% 1.84/2.21 ), hskp2, hskp9, alpha52, ! c3_1( a1 ) }.
% 1.84/2.21 (259) {G23,W10,D2,L8,V0,M1} R(246,196);f;f;f;f { hskp0, hskp1, hskp7, !
% 1.84/2.21 c2_1( a5 ), hskp2, hskp9, alpha36, ! c3_1( a5 ) }.
% 1.84/2.21 (205) {G20,W12,D2,L7,V1,M1} R(165,169);f { hskp4, c2_1( a10 ), ! c3_1( X )
% 1.84/2.21 , ! c0_1( X ), ! c0_1( a10 ), alpha48, c1_1( X ) }.
% 1.84/2.21 (246) {G22,W11,D2,L8,V1,M1} R(245,167);f { hskp1, hskp0, hskp7, ! c2_1( X )
% 1.84/2.21 , ! c3_1( X ), hskp2, hskp9, c0_1( X ) }.
% 1.84/2.21 (244) {G21,W11,D2,L7,V0,M1} R(203,177);f { hskp4, c2_1( a7 ), ! c3_1( a5 )
% 1.84/2.21 , ! c0_1( a5 ), alpha36, alpha50, ! c0_1( a7 ) }.
% 1.84/2.21 (251) {G21,W11,D2,L7,V0,M1} R(204,177);f { hskp4, c2_1( a7 ), ! c3_1( a15 )
% 1.84/2.21 , ! c0_1( a15 ), alpha26, alpha50, ! c0_1( a7 ) }.
% 1.84/2.21 (249) {G21,W11,D2,L7,V0,M1} R(204,169);f { hskp4, c2_1( a10 ), ! c3_1( a15
% 1.84/2.21 ), ! c0_1( a10 ), alpha26, alpha48, ! c0_1( a15 ) }.
% 1.84/2.21 (204) {G20,W12,D2,L7,V1,M1} R(165,162);f { hskp4, c2_1( X ), ! c3_1( a15 )
% 1.84/2.21 , ! c0_1( a15 ), ! c0_1( X ), alpha26, ! c1_1( X ) }.
% 1.84/2.21 (242) {G21,W11,D2,L7,V0,M1} R(203,169);f { hskp4, c2_1( a10 ), ! c3_1( a5 )
% 1.84/2.21 , ! c0_1( a10 ), alpha36, alpha48, ! c0_1( a5 ) }.
% 1.84/2.21 (247) {G22,W8,D2,L6,V0,M1} R(245,185);f { hskp1, hskp0, hskp7, ! c2_1( a12
% 1.84/2.21 ), alpha45, c0_1( a12 ) }.
% 1.84/2.21 (245) {G21,W9,D2,L6,V1,M1} S(229);r(174) { hskp1, ! c2_1( X ), hskp0, hskp7
% 1.84/2.21 , c0_1( X ), ! c1_1( X ) }.
% 1.84/2.21 (203) {G20,W12,D2,L7,V1,M1} R(165,184);f { hskp4, c2_1( X ), ! c3_1( a5 ),
% 1.84/2.21 ! c0_1( a5 ), ! c0_1( X ), alpha36, ! c1_1( X ) }.
% 1.84/2.21 (237) {G22,W10,D2,L8,V0,M1} R(230,194);f;f { hskp1, ! c2_1( a11 ), hskp10,
% 1.84/2.21 hskp11, alpha46, hskp2, hskp9, ! c2_1( a8 ) }.
% 1.84/2.21 (241) {G22,W10,D2,L8,V0,M1} R(234,199);f;f { hskp1, ! c2_1( a8 ), hskp10,
% 1.84/2.21 hskp11, alpha49, hskp2, hskp9, ! c2_1( a9 ) }.
% 1.84/2.21 (234) {G21,W10,D2,L7,V0,M1} R(228,175);f { hskp1, ! c2_1( a8 ), ! c2_1( a9
% 1.84/2.21 ), hskp10, hskp11, alpha49, c3_1( a9 ) }.
% 1.84/2.21 (232) {G21,W10,D2,L7,V0,M1} R(228,182);f { hskp1, ! c2_1( a4 ), ! c2_1( a8
% 1.84/2.21 ), hskp10, hskp11, alpha47, c3_1( a4 ) }.
% 1.84/2.21 (201) {G20,W14,D2,L8,V1,M1} R(165,187) { hskp4, c2_1( X ), ! c3_1( a11 ), !
% 1.84/2.21 c0_1( a11 ), ! c0_1( X ), ! c2_1( a11 ), alpha46, ! c1_1( X ) }.
% 1.84/2.21 (230) {G21,W10,D2,L7,V0,M1} R(228,187);f { hskp1, ! c2_1( a11 ), ! c2_1( a8
% 1.84/2.21 ), hskp10, hskp11, alpha46, c3_1( a11 ) }.
% 1.84/2.21 (236) {G22,W7,D2,L6,V0,M1} S(235);r(174) { hskp1, hskp10, hskp11, hskp0,
% 1.84/2.21 hskp7, ! c2_1( a8 ) }.
% 1.84/2.21 (228) {G20,W11,D2,L7,V1,M1} R(168,171);r(172) { hskp1, ! c2_1( a8 ), ! c2_1
% 1.84/2.21 ( X ), c3_1( X ), hskp10, hskp11, c1_1( X ) }.
% 1.84/2.21 (168) {G19,W13,D2,L7,V2,M2} R(161,4) { c0_1( X ), ! c2_1( X ), hskp1, !
% 1.84/2.21 c2_1( Y ), c3_1( Y ), ! c1_1( X ), c1_1( Y ) }.
% 1.84/2.21 (212) {G21,W11,D2,L7,V0,M1} R(202,177);f { hskp4, c2_1( a7 ), ! c3_1( a8 )
% 1.84/2.21 , ! c0_1( a7 ), alpha22, alpha50, ! c0_1( a8 ) }.
% 1.84/2.21 (210) {G21,W11,D2,L7,V0,M1} R(202,169);f { hskp4, c2_1( a10 ), ! c3_1( a8 )
% 1.84/2.21 , ! c0_1( a10 ), alpha22, alpha48, ! c0_1( a8 ) }.
% 1.84/2.21 (217) {G21,W10,D2,L7,V0,M1} R(216,180);f { hskp12, c2_1( a1 ), ! c2_1( a8 )
% 1.84/2.21 , hskp10, hskp11, alpha52, ! c3_1( a1 ) }.
% 1.84/2.21 (216) {G20,W11,D2,L7,V1,M1} R(166,171);r(170) { hskp12, ! c2_1( a8 ), c2_1
% 1.84/2.21 ( X ), ! c3_1( X ), hskp10, hskp11, c0_1( X ) }.
% 1.84/2.21 (166) {G19,W13,D2,L7,V2,M1} R(161,7) { ! c3_1( X ), ! c2_1( X ), hskp12,
% 1.84/2.21 c2_1( Y ), ! c3_1( Y ), c0_1( Y ), ! c1_1( X ) }.
% 1.84/2.21 (202) {G20,W12,D2,L7,V1,M1} R(165,186);f { hskp4, c2_1( X ), ! c3_1( a8 ),
% 1.84/2.21 ! c0_1( a8 ), ! c0_1( X ), alpha22, ! c1_1( X ) }.
% 1.84/2.21 (165) {G19,W13,D2,L7,V2,M2} R(161,8) { hskp4, ! c0_1( X ), c2_1( X ), !
% 1.84/2.21 c0_1( Y ), ! c3_1( Y ), ! c1_1( X ), c1_1( Y ) }.
% 1.84/2.21 (193) {G20,W9,D2,L6,V0,M1} R(164,178) { hskp5, c2_1( a6 ), hskp3, ! c3_1(
% 1.84/2.21 a6 ), alpha42, c0_1( a6 ) }.
% 1.84/2.21 (192) {G20,W9,D2,L6,V0,M1} R(164,162) { hskp5, c2_1( a15 ), hskp3, ! c3_1(
% 1.84/2.21 a15 ), alpha26, c0_1( a15 ) }.
% 1.84/2.21 (190) {G20,W9,D2,L6,V0,M1} R(164,182) { hskp5, c2_1( a4 ), hskp3, c3_1( a4
% 1.84/2.21 ), alpha47, c0_1( a4 ) }.
% 1.84/2.21 (189) {G20,W9,D2,L6,V0,M1} R(164,186) { hskp5, c2_1( a8 ), hskp3, ! c3_1(
% 1.84/2.21 a8 ), alpha22, c0_1( a8 ) }.
% 1.84/2.21 (197) {G20,W9,D2,L6,V0,M1} R(167,183) { ! c2_1( a14 ), hskp2, hskp9, ! c3_1
% 1.84/2.21 ( a14 ), alpha33, c0_1( a14 ) }.
% 1.84/2.21 (196) {G20,W9,D2,L6,V0,M1} R(167,184) { ! c2_1( a5 ), hskp2, hskp9, ! c3_1
% 1.84/2.21 ( a5 ), alpha36, ! c0_1( a5 ) }.
% 1.84/2.21 (200) {G20,W7,D2,L5,V0,M1} R(167,178);f { ! c2_1( a6 ), hskp2, hskp9,
% 1.84/2.21 alpha42, ! c3_1( a6 ) }.
% 1.84/2.21 (199) {G20,W7,D2,L5,V0,M1} R(167,175);f { ! c2_1( a9 ), hskp2, hskp9,
% 1.84/2.21 alpha49, ! c3_1( a9 ) }.
% 1.84/2.21 (198) {G20,W7,D2,L5,V0,M1} R(167,162);f { ! c2_1( a15 ), hskp2, hskp9,
% 1.84/2.21 alpha26, ! c3_1( a15 ) }.
% 1.84/2.21 (195) {G20,W7,D2,L5,V0,M1} R(167,186);f { ! c2_1( a8 ), hskp2, hskp9,
% 1.84/2.21 alpha22, ! c3_1( a8 ) }.
% 1.84/2.21 (194) {G20,W7,D2,L5,V0,M1} R(167,187);f { ! c2_1( a11 ), hskp2, hskp9,
% 1.84/2.21 alpha46, ! c3_1( a11 ) }.
% 1.84/2.21 (167) {G19,W8,D2,L5,V1,M1} R(161,5) { ! c2_1( X ), ! c3_1( X ), hskp2,
% 1.84/2.21 hskp9, c1_1( X ) }.
% 1.84/2.21 (191) {G20,W7,D2,L5,V0,M1} R(164,183);f { hskp5, c2_1( a14 ), hskp3,
% 1.84/2.21 alpha33, c0_1( a14 ) }.
% 1.84/2.21 (164) {G19,W8,D2,L5,V1,M1} R(161,9) { hskp5, c2_1( X ), c0_1( X ), hskp3,
% 1.84/2.21 c1_1( X ) }.
% 1.84/2.21 (188) {G20,W7,D2,L5,V0,M1} R(163,181);f { c2_1( a2 ), hskp6, hskp13,
% 1.84/2.21 alpha38, c3_1( a2 ) }.
% 1.84/2.21 (163) {G19,W8,D2,L5,V1,M1} R(161,10) { c2_1( X ), c3_1( X ), hskp6, hskp13
% 1.84/2.21 , c0_1( X ) }.
% 1.84/2.21 (187) {G19,W5,D2,L3,V0,M1} S(104);r(161) { ! c2_1( a11 ), alpha46, ! c1_1(
% 1.84/2.21 a11 ) }.
% 1.84/2.21 (186) {G19,W5,D2,L3,V0,M1} S(114);r(161) { ! c3_1( a8 ), alpha22, ! c1_1(
% 1.84/2.21 a8 ) }.
% 1.84/2.21 (185) {G19,W5,D2,L3,V0,M1} S(94);r(161) { c0_1( a12 ), alpha45, c1_1( a12 )
% 1.84/2.21 }.
% 1.84/2.21 (184) {G19,W5,D2,L3,V0,M1} S(124);r(161) { ! c0_1( a5 ), alpha36, ! c1_1(
% 1.84/2.21 a5 ) }.
% 1.84/2.21 (182) {G19,W5,D2,L3,V0,M1} S(134);r(161) { c3_1( a4 ), alpha47, ! c1_1( a4
% 1.84/2.21 ) }.
% 1.84/2.21 (183) {G19,W5,D2,L3,V0,M1} S(84);r(161) { c0_1( a14 ), alpha33, ! c1_1( a14
% 1.84/2.21 ) }.
% 1.84/2.21 (181) {G19,W5,D2,L3,V0,M1} S(142);r(161) { c3_1( a2 ), alpha38, ! c0_1( a2
% 1.84/2.21 ) }.
% 1.84/2.21 (180) {G19,W5,D2,L3,V0,M1} S(74);r(161) { ! c3_1( a1 ), alpha52, ! c0_1( a1
% 1.84/2.21 ) }.
% 1.84/2.21 (162) {G19,W5,D2,L3,V0,M1} R(161,14) { ! c3_1( a15 ), alpha26, ! c1_1( a15
% 1.84/2.21 ) }.
% 1.84/2.21 (169) {G19,W5,D2,L3,V0,M1} S(24);r(161) { c2_1( a10 ), alpha48, c1_1( a10 )
% 1.84/2.21 }.
% 1.84/2.21 (179) {G19,W5,D2,L3,V0,M1} S(64);r(161) { c3_1( a3 ), alpha51, c1_1( a3 )
% 1.84/2.21 }.
% 1.84/2.21 (175) {G19,W5,D2,L3,V0,M1} S(34);r(161) { ! c2_1( a9 ), alpha49, ! c1_1( a9
% 1.84/2.21 ) }.
% 1.84/2.21 (177) {G19,W5,D2,L3,V0,M1} S(44);r(161) { c2_1( a7 ), alpha50, c1_1( a7 )
% 1.84/2.21 }.
% 1.84/2.21 (178) {G19,W5,D2,L3,V0,M1} S(54);r(161) { ! c3_1( a6 ), alpha42, ! c1_1( a6
% 1.84/2.21 ) }.
% 1.84/2.21 (60) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a3 ), alpha43, ! alpha51 }.
% 1.84/2.21 (70) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a1 ), alpha44, ! alpha52 }.
% 1.84/2.21 (80) {G0,W4,D2,L3,V0,M1} I { c2_1( a14 ), alpha19, ! alpha33 }.
% 1.84/2.21 (90) {G0,W4,D2,L3,V0,M1} I { c2_1( a12 ), alpha34, ! alpha45 }.
% 1.84/2.21 (100) {G0,W4,D2,L3,V0,M1} I { c0_1( a11 ), alpha35, ! alpha46 }.
% 1.84/2.21 (50) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a6 ), alpha30, ! alpha42 }.
% 1.84/2.21 (110) {G0,W4,D2,L3,V0,M1} I { c0_1( a8 ), alpha12, ! alpha22 }.
% 1.84/2.21 (120) {G0,W4,D2,L3,V0,M1} I { c2_1( a5 ), alpha23, ! alpha36 }.
% 1.84/2.21 (130) {G0,W4,D2,L3,V0,M1} I { c2_1( a4 ), alpha37, ! alpha47 }.
% 1.84/2.21 (138) {G0,W4,D2,L3,V0,M1} I { c1_1( a2 ), alpha25, ! alpha38 }.
% 1.84/2.21 (170) {G14,W4,D2,L3,V0,M1} R(113,156) { hskp10, hskp11, c3_1( a8 ) }.
% 1.84/2.21 (171) {G14,W4,D2,L3,V0,M1} R(112,156) { hskp10, hskp11, c1_1( a8 ) }.
% 1.84/2.21 (172) {G13,W4,D2,L3,V0,M1} R(109,143) { hskp10, hskp11, ! c0_1( a8 ) }.
% 1.84/2.21 (173) {G9,W4,D2,L3,V0,M1} R(63,145) { hskp0, hskp7, ! c1_1( a3 ) }.
% 1.84/2.21 (40) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a7 ), alpha41, ! alpha50 }.
% 1.84/2.21 (174) {G9,W4,D2,L3,V0,M1} R(62,145) { hskp0, hskp7, ! c3_1( a3 ) }.
% 1.84/2.21 (176) {G8,W4,D2,L3,V0,M1} R(59,144) { hskp0, hskp7, c2_1( a3 ) }.
% 1.84/2.21 (42) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a7 ), ! alpha50 }.
% 1.84/2.21 (43) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a7 ), ! alpha50 }.
% 1.84/2.21 (39) {G0,W3,D2,L2,V0,M1} I { c3_1( a7 ), ! alpha41 }.
% 1.84/2.21 (49) {G0,W3,D2,L2,V0,M1} I { c2_1( a6 ), ! alpha30 }.
% 1.84/2.21 (52) {G0,W3,D2,L2,V0,M1} I { c1_1( a6 ), ! alpha42 }.
% 1.84/2.21 (53) {G0,W3,D2,L2,V0,M1} I { c3_1( a6 ), ! alpha42 }.
% 1.84/2.21 (59) {G0,W3,D2,L2,V0,M1} I { c2_1( a3 ), ! alpha43 }.
% 1.84/2.21 (62) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a3 ), ! alpha51 }.
% 1.84/2.21 (63) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a3 ), ! alpha51 }.
% 1.84/2.21 (69) {G0,W3,D2,L2,V0,M1} I { c1_1( a1 ), ! alpha44 }.
% 1.84/2.21 (72) {G0,W3,D2,L2,V0,M1} I { c3_1( a1 ), ! alpha52 }.
% 1.84/2.21 (33) {G0,W3,D2,L2,V0,M1} I { c2_1( a9 ), ! alpha49 }.
% 1.84/2.21 (73) {G0,W3,D2,L2,V0,M1} I { c0_1( a1 ), ! alpha52 }.
% 1.84/2.21 (79) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a14 ), ! alpha19 }.
% 1.84/2.21 (82) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a14 ), ! alpha33 }.
% 1.84/2.21 (83) {G0,W3,D2,L2,V0,M1} I { c1_1( a14 ), ! alpha33 }.
% 1.84/2.21 (32) {G0,W3,D2,L2,V0,M1} I { c1_1( a9 ), ! alpha49 }.
% 1.84/2.21 (89) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a12 ), ! alpha34 }.
% 1.84/2.21 (92) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a12 ), ! alpha45 }.
% 1.84/2.21 (93) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a12 ), ! alpha45 }.
% 1.84/2.21 (99) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a11 ), ! alpha35 }.
% 1.84/2.21 (30) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a9 ), alpha40, ! alpha49 }.
% 1.84/2.21 (102) {G0,W3,D2,L2,V0,M1} I { c1_1( a11 ), ! alpha46 }.
% 1.84/2.21 (103) {G0,W3,D2,L2,V0,M1} I { c2_1( a11 ), ! alpha46 }.
% 1.84/2.21 (109) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a8 ), ! alpha12 }.
% 1.84/2.21 (112) {G0,W3,D2,L2,V0,M1} I { c1_1( a8 ), ! alpha22 }.
% 1.84/2.21 (29) {G0,W3,D2,L2,V0,M1} I { c3_1( a9 ), ! alpha40 }.
% 1.84/2.21 (113) {G0,W3,D2,L2,V0,M1} I { c3_1( a8 ), ! alpha22 }.
% 1.84/2.21 (119) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a5 ), ! alpha23 }.
% 1.84/2.21 (122) {G0,W3,D2,L2,V0,M1} I { c1_1( a5 ), ! alpha36 }.
% 1.84/2.21 (123) {G0,W3,D2,L2,V0,M1} I { c0_1( a5 ), ! alpha36 }.
% 1.84/2.21 (129) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a4 ), ! alpha37 }.
% 1.84/2.21 (132) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a4 ), ! alpha47 }.
% 1.84/2.21 (133) {G0,W3,D2,L2,V0,M1} I { c1_1( a4 ), ! alpha47 }.
% 1.84/2.21 (137) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a2 ), ! alpha25 }.
% 1.84/2.21 (23) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a10 ), ! alpha48 }.
% 1.84/2.21 (140) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a2 ), ! alpha38 }.
% 1.84/2.21 (141) {G0,W3,D2,L2,V0,M1} I { c0_1( a2 ), ! alpha38 }.
% 1.84/2.21 (161) {G18,W1,D1,L1,V0,M1} R(160,38);r(41) { ndr1_0 }.
% 1.84/2.21 (22) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a10 ), ! alpha48 }.
% 1.84/2.21 (156) {G13,W3,D1,L3,V0,M1} R(143,108) { hskp10, hskp11, alpha22 }.
% 1.84/2.21 (20) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a10 ), alpha39, ! alpha48 }.
% 1.84/2.21 (143) {G12,W3,D1,L3,V0,M1} R(107,6) { hskp10, hskp11, alpha12 }.
% 1.84/2.21 (19) {G0,W3,D2,L2,V0,M1} I { c3_1( a10 ), ! alpha39 }.
% 1.84/2.21 (145) {G8,W3,D1,L3,V0,M1} R(144,58) { hskp0, hskp7, alpha51 }.
% 1.84/2.21 (144) {G7,W3,D1,L3,V0,M1} R(57,3) { hskp0, hskp7, alpha43 }.
% 1.84/2.21 (17) {G2,W2,D1,L2,V0,M1} I;r(16) { alpha39, ! hskp12 }.
% 1.84/2.21 (18) {G0,W2,D1,L2,V0,M1} I { alpha48, ! alpha39 }.
% 1.84/2.21 (27) {G3,W2,D1,L2,V0,M1} I;r(26) { alpha40, ! hskp11 }.
% 1.84/2.21 (28) {G0,W2,D1,L2,V0,M1} I { alpha49, ! alpha40 }.
% 1.84/2.21 (13) {G0,W3,D2,L2,V0,M1} I { c1_1( a15 ), ! alpha26 }.
% 1.84/2.21 (37) {G4,W2,D1,L2,V0,M1} I;r(36) { alpha41, ! hskp10 }.
% 1.84/2.21 (38) {G0,W2,D1,L2,V0,M1} I { alpha50, ! alpha41 }.
% 1.84/2.21 (47) {G5,W2,D1,L2,V0,M1} I;r(46) { alpha30, ! hskp9 }.
% 1.84/2.21 (12) {G0,W3,D2,L2,V0,M1} I { c3_1( a15 ), ! alpha26 }.
% 1.84/2.21 (48) {G0,W2,D1,L2,V0,M1} I { alpha42, ! alpha30 }.
% 1.84/2.21 (57) {G6,W2,D1,L2,V0,M1} I;r(56) { alpha43, ! hskp8 }.
% 1.84/2.21 (58) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha43 }.
% 1.84/2.21 (67) {G7,W2,D1,L2,V0,M1} I;r(66) { alpha44, ! hskp7 }.
% 1.84/2.21 (68) {G0,W2,D1,L2,V0,M1} I { alpha52, ! alpha44 }.
% 1.84/2.21 (77) {G8,W2,D1,L2,V0,M1} I;r(76) { alpha19, ! hskp6 }.
% 1.84/2.21 (78) {G0,W2,D1,L2,V0,M1} I { alpha33, ! alpha19 }.
% 1.84/2.21 (87) {G9,W2,D1,L2,V0,M1} I;r(86) { alpha34, ! hskp5 }.
% 1.84/2.21 (88) {G0,W2,D1,L2,V0,M1} I { alpha45, ! alpha34 }.
% 1.84/2.21 (97) {G10,W2,D1,L2,V0,M1} I;r(96) { alpha35, ! hskp4 }.
% 1.84/2.21 (98) {G0,W2,D1,L2,V0,M1} I { alpha46, ! alpha35 }.
% 1.84/2.21 (107) {G11,W2,D1,L2,V0,M1} I;r(106) { alpha12, ! hskp3 }.
% 1.84/2.21 (108) {G0,W2,D1,L2,V0,M1} I { alpha22, ! alpha12 }.
% 1.84/2.21 (117) {G12,W2,D1,L2,V0,M1} I;r(116) { alpha23, ! hskp2 }.
% 1.84/2.21 (118) {G0,W2,D1,L2,V0,M1} I { alpha36, ! alpha23 }.
% 1.84/2.21 (127) {G13,W2,D1,L2,V0,M1} I;r(126) { alpha37, ! hskp1 }.
% 1.84/2.21 (6) {G0,W3,D1,L3,V0,M1} I { hskp10, hskp11, hskp3 }.
% 1.84/2.21 (128) {G0,W2,D1,L2,V0,M1} I { alpha47, ! alpha37 }.
% 1.84/2.21 (135) {G13,W2,D1,L2,V0,M1} I;r(125) { alpha25, ! hskp0 }.
% 1.84/2.21 (136) {G0,W2,D1,L2,V0,M1} I { alpha38, ! alpha25 }.
% 1.84/2.21 (15) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha8 }.
% 1.84/2.21 (16) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha27 }.
% 1.84/2.21 (25) {G2,W1,D1,L1,V0,M1} I;r(15) { alpha16 }.
% 1.84/2.21 (26) {G2,W1,D1,L1,V0,M1} I;r(15) { alpha28 }.
% 1.84/2.21 (35) {G3,W1,D1,L1,V0,M1} I;r(25) { alpha4 }.
% 1.84/2.21 (36) {G3,W1,D1,L1,V0,M1} I;r(25) { alpha29 }.
% 1.84/2.21 (45) {G4,W1,D1,L1,V0,M1} I;r(35) { alpha9 }.
% 1.84/2.21 (3) {G0,W3,D1,L3,V0,M1} I { hskp0, hskp7, hskp8 }.
% 1.84/2.21 (46) {G4,W1,D1,L1,V0,M1} I;r(35) { alpha17 }.
% 1.84/2.21 (55) {G5,W1,D1,L1,V0,M1} I;r(45) { alpha18 }.
% 1.84/2.21 (56) {G5,W1,D1,L1,V0,M1} I;r(45) { alpha31 }.
% 1.84/2.21 (65) {G6,W1,D1,L1,V0,M1} I;r(55) { alpha2 }.
% 1.84/2.21 (2) {G0,W3,D2,L2,V0,M1} I { c2_1( a15 ), ! hskp13 }.
% 1.84/2.21 (66) {G6,W1,D1,L1,V0,M1} I;r(55) { alpha32 }.
% 1.84/2.21 (75) {G7,W1,D1,L1,V0,M1} I;r(65) { alpha5 }.
% 1.84/2.21 (76) {G7,W1,D1,L1,V0,M1} I;r(65) { alpha10 }.
% 1.84/2.21 (85) {G8,W1,D1,L1,V0,M1} I;r(75) { alpha11 }.
% 1.84/2.21 (1) {G0,W2,D1,L2,V0,M1} I { alpha26, ! hskp13 }.
% 1.84/2.21 (86) {G8,W1,D1,L1,V0,M1} I;r(75) { alpha20 }.
% 1.84/2.21 (95) {G9,W1,D1,L1,V0,M1} I;r(85) { alpha1 }.
% 1.84/2.21 (96) {G9,W1,D1,L1,V0,M1} I;r(85) { alpha21 }.
% 1.84/2.21 (105) {G10,W1,D1,L1,V0,M1} I;r(95) { alpha3 }.
% 1.84/2.21 (0) {G0,W1,D1,L1,V0,M1} I { alpha15 }.
% 1.84/2.21 (106) {G10,W1,D1,L1,V0,M1} I;r(95) { alpha6 }.
% 1.84/2.21 (115) {G11,W1,D1,L1,V0,M1} I;r(105) { alpha7 }.
% 1.84/2.21 (116) {G11,W1,D1,L1,V0,M1} I;r(105) { alpha13 }.
% 1.84/2.21 (125) {G12,W1,D1,L1,V0,M1} I;r(115) { alpha14 }.
% 1.84/2.21 (126) {G12,W1,D1,L1,V0,M1} I;r(115) { alpha24 }.
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 % SZS output end Saturation
% 1.84/2.21 end of saturation!
% 1.84/2.21
% 1.84/2.21 Memory use:
% 1.84/2.21
% 1.84/2.21 space for terms: 13707
% 1.84/2.21 space for clauses: 28516
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 clauses generated: 6922
% 1.84/2.21 clauses kept: 667
% 1.84/2.21 clauses selected: 456
% 1.84/2.21 clauses deleted: 251
% 1.84/2.21 clauses inuse deleted: 40
% 1.84/2.21
% 1.84/2.21 subsentry: 5923
% 1.84/2.21 literals s-matched: 3435
% 1.84/2.21 literals matched: 3435
% 1.84/2.21 full subsumption: 1406
% 1.84/2.21
% 1.84/2.21 checksum: -898004171
% 1.84/2.21
% 1.84/2.21
% 1.84/2.21 Bliksem ended
%------------------------------------------------------------------------------