%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN495+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.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:58 EDT 2022
% Result : CounterSatisfiable 0.82s 1.18s
% Output : Saturation 0.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SYN495+1 : TPTP v8.1.0. Released v2.1.0.
% 0.08/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Mon Jul 11 23:39:50 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.45/1.11 *** allocated 10000 integers for termspace/termends
% 0.45/1.11 *** allocated 10000 integers for clauses
% 0.45/1.11 *** allocated 10000 integers for justifications
% 0.45/1.11 Bliksem 1.12
% 0.45/1.11
% 0.45/1.11
% 0.45/1.11 Automatic Strategy Selection
% 0.45/1.11
% 0.45/1.11
% 0.45/1.11 Clauses:
% 0.45/1.11
% 0.45/1.11 { alpha26 }.
% 0.45/1.11 { ! hskp16, alpha41 }.
% 0.45/1.11 { ! hskp16, c3_1( a74 ) }.
% 0.45/1.11 { hskp0, ! ndr1_0, c2_1( X ), c1_1( X ), c3_1( X ), hskp8 }.
% 0.45/1.11 { hskp9, ! ndr1_0, c3_1( X ), ! c0_1( X ), ! c1_1( X ), hskp10 }.
% 0.45/1.11 { hskp11, hskp1, hskp12 }.
% 0.45/1.11 { hskp13, hskp2, hskp14 }.
% 0.45/1.11 { hskp3, ! ndr1_0, c0_1( X ), ! c1_1( X ), ! c3_1( X ), hskp15 }.
% 0.45/1.11 { hskp4, ! ndr1_0, c1_1( X ), c0_1( X ), ! c3_1( X ), ! ndr1_0, c1_1( Y ),
% 0.45/1.11 ! c0_1( Y ), ! c2_1( Y ) }.
% 0.45/1.11 { hskp16, hskp5, hskp6 }.
% 0.45/1.11 { hskp7, ! ndr1_0, c0_1( X ), ! c3_1( X ), c1_1( X ), hskp12 }.
% 0.45/1.11 { ! alpha41, ndr1_0 }.
% 0.45/1.11 { ! alpha41, ! c1_1( a74 ) }.
% 0.45/1.11 { ! alpha41, c2_1( a74 ) }.
% 0.45/1.11 { ! ndr1_0, c1_1( a74 ), ! c2_1( a74 ), alpha41 }.
% 0.45/1.11 { ! alpha26, alpha15 }.
% 0.45/1.11 { ! alpha26, alpha42 }.
% 0.45/1.11 { ! alpha15, ! alpha42, alpha26 }.
% 0.45/1.11 { ! alpha42, ! hskp15, alpha55 }.
% 0.45/1.11 { hskp15, alpha42 }.
% 0.45/1.11 { ! alpha55, alpha42 }.
% 0.45/1.11 { ! alpha55, alpha64 }.
% 0.45/1.11 { ! alpha55, c0_1( a72 ) }.
% 0.45/1.11 { ! alpha64, ! c0_1( a72 ), alpha55 }.
% 0.45/1.11 { ! alpha64, ndr1_0 }.
% 0.45/1.11 { ! alpha64, c1_1( a72 ) }.
% 0.45/1.11 { ! alpha64, c3_1( a72 ) }.
% 0.45/1.11 { ! ndr1_0, ! c1_1( a72 ), ! c3_1( a72 ), alpha64 }.
% 0.45/1.11 { ! alpha15, alpha8 }.
% 0.45/1.11 { ! alpha15, alpha27 }.
% 0.45/1.11 { ! alpha8, ! alpha27, alpha15 }.
% 0.45/1.11 { ! alpha27, ! hskp14, alpha43 }.
% 0.45/1.11 { hskp14, alpha27 }.
% 0.45/1.11 { ! alpha43, alpha27 }.
% 0.45/1.11 { ! alpha43, alpha56 }.
% 0.45/1.11 { ! alpha43, c1_1( a70 ) }.
% 0.45/1.11 { ! alpha56, ! c1_1( a70 ), alpha43 }.
% 0.45/1.11 { ! alpha56, ndr1_0 }.
% 0.45/1.11 { ! alpha56, ! c0_1( a70 ) }.
% 0.45/1.11 { ! alpha56, c3_1( a70 ) }.
% 0.45/1.11 { ! ndr1_0, c0_1( a70 ), ! c3_1( a70 ), alpha56 }.
% 0.45/1.11 { ! alpha8, alpha16 }.
% 0.45/1.11 { ! alpha8, alpha28 }.
% 0.45/1.11 { ! alpha16, ! alpha28, alpha8 }.
% 0.45/1.11 { ! alpha28, ! hskp13, alpha44 }.
% 0.45/1.11 { hskp13, alpha28 }.
% 0.45/1.11 { ! alpha44, alpha28 }.
% 0.45/1.11 { ! alpha44, alpha57 }.
% 0.45/1.11 { ! alpha44, c0_1( a68 ) }.
% 0.45/1.11 { ! alpha57, ! c0_1( a68 ), alpha44 }.
% 0.45/1.11 { ! alpha57, ndr1_0 }.
% 0.45/1.11 { ! alpha57, ! c1_1( a68 ) }.
% 0.45/1.11 { ! alpha57, c2_1( a68 ) }.
% 0.45/1.11 { ! ndr1_0, c1_1( a68 ), ! c2_1( a68 ), alpha57 }.
% 0.45/1.11 { ! alpha16, alpha4 }.
% 0.45/1.11 { ! alpha16, alpha29 }.
% 0.45/1.11 { ! alpha4, ! alpha29, alpha16 }.
% 0.45/1.11 { ! alpha29, ! hskp12, alpha45 }.
% 0.45/1.11 { hskp12, alpha29 }.
% 0.45/1.11 { ! alpha45, alpha29 }.
% 0.45/1.11 { ! alpha45, alpha58 }.
% 0.45/1.11 { ! alpha45, c1_1( a67 ) }.
% 0.45/1.11 { ! alpha58, ! c1_1( a67 ), alpha45 }.
% 0.45/1.11 { ! alpha58, ndr1_0 }.
% 0.45/1.11 { ! alpha58, ! c3_1( a67 ) }.
% 0.45/1.11 { ! alpha58, ! c2_1( a67 ) }.
% 0.45/1.11 { ! ndr1_0, c3_1( a67 ), c2_1( a67 ), alpha58 }.
% 0.45/1.11 { ! alpha4, alpha9 }.
% 0.45/1.11 { ! alpha4, alpha17 }.
% 0.45/1.11 { ! alpha9, ! alpha17, alpha4 }.
% 0.45/1.11 { ! alpha17, ! hskp11, alpha30 }.
% 0.45/1.11 { hskp11, alpha17 }.
% 0.45/1.11 { ! alpha30, alpha17 }.
% 0.45/1.11 { ! alpha30, alpha46 }.
% 0.45/1.11 { ! alpha30, c2_1( a65 ) }.
% 0.45/1.11 { ! alpha46, ! c2_1( a65 ), alpha30 }.
% 0.45/1.11 { ! alpha46, ndr1_0 }.
% 0.45/1.11 { ! alpha46, ! c1_1( a65 ) }.
% 0.45/1.11 { ! alpha46, ! c0_1( a65 ) }.
% 0.45/1.11 { ! ndr1_0, c1_1( a65 ), c0_1( a65 ), alpha46 }.
% 0.45/1.11 { ! alpha9, alpha18 }.
% 0.45/1.11 { ! alpha9, alpha31 }.
% 0.45/1.11 { ! alpha18, ! alpha31, alpha9 }.
% 0.45/1.11 { ! alpha31, ! hskp10, alpha47 }.
% 0.45/1.11 { hskp10, alpha31 }.
% 0.45/1.11 { ! alpha47, alpha31 }.
% 0.45/1.11 { ! alpha47, alpha59 }.
% 0.45/1.11 { ! alpha47, c0_1( a64 ) }.
% 0.45/1.11 { ! alpha59, ! c0_1( a64 ), alpha47 }.
% 0.45/1.11 { ! alpha59, ndr1_0 }.
% 0.45/1.11 { ! alpha59, ! c3_1( a64 ) }.
% 0.45/1.11 { ! alpha59, ! c2_1( a64 ) }.
% 0.45/1.11 { ! ndr1_0, c3_1( a64 ), c2_1( a64 ), alpha59 }.
% 0.45/1.11 { ! alpha18, alpha2 }.
% 0.45/1.11 { ! alpha18, alpha32 }.
% 0.45/1.11 { ! alpha2, ! alpha32, alpha18 }.
% 0.45/1.11 { ! alpha32, ! hskp9, alpha48 }.
% 0.45/1.11 { hskp9, alpha32 }.
% 0.45/1.11 { ! alpha48, alpha32 }.
% 0.45/1.11 { ! alpha48, alpha60 }.
% 0.45/1.11 { ! alpha48, c3_1( a63 ) }.
% 0.45/1.11 { ! alpha60, ! c3_1( a63 ), alpha48 }.
% 0.45/1.11 { ! alpha60, ndr1_0 }.
% 0.45/1.11 { ! alpha60, c2_1( a63 ) }.
% 0.45/1.11 { ! alpha60, ! c1_1( a63 ) }.
% 0.45/1.11 { ! ndr1_0, ! c2_1( a63 ), c1_1( a63 ), alpha60 }.
% 0.45/1.11 { ! alpha2, alpha5 }.
% 0.45/1.11 { ! alpha2, alpha10 }.
% 0.45/1.11 { ! alpha5, ! alpha10, alpha2 }.
% 0.45/1.11 { ! alpha10, ! hskp8, alpha19 }.
% 0.45/1.11 { hskp8, alpha10 }.
% 0.45/1.11 { ! alpha19, alpha10 }.
% 0.45/1.11 { ! alpha19, alpha33 }.
% 0.45/1.11 { ! alpha19, c0_1( a62 ) }.
% 0.45/1.11 { ! alpha33, ! c0_1( a62 ), alpha19 }.
% 0.45/1.11 { ! alpha33, ndr1_0 }.
% 0.45/1.11 { ! alpha33, ! c1_1( a62 ) }.
% 0.45/1.11 { ! alpha33, c3_1( a62 ) }.
% 0.45/1.11 { ! ndr1_0, c1_1( a62 ), ! c3_1( a62 ), alpha33 }.
% 0.45/1.11 { ! alpha5, alpha11 }.
% 0.45/1.11 { ! alpha5, alpha20 }.
% 0.45/1.11 { ! alpha11, ! alpha20, alpha5 }.
% 0.45/1.11 { ! alpha20, ! hskp7, alpha34 }.
% 0.45/1.11 { hskp7, alpha20 }.
% 0.45/1.11 { ! alpha34, alpha20 }.
% 0.45/1.11 { ! alpha34, alpha49 }.
% 0.45/1.11 { ! alpha34, ! c0_1( a77 ) }.
% 0.45/1.11 { ! alpha49, c0_1( a77 ), alpha34 }.
% 0.45/1.11 { ! alpha49, ndr1_0 }.
% 0.45/1.11 { ! alpha49, ! c2_1( a77 ) }.
% 0.45/1.11 { ! alpha49, c3_1( a77 ) }.
% 0.45/1.11 { ! ndr1_0, c2_1( a77 ), ! c3_1( a77 ), alpha49 }.
% 0.45/1.11 { ! alpha11, alpha21 }.
% 0.45/1.11 { ! alpha11, alpha35 }.
% 0.45/1.11 { ! alpha21, ! alpha35, alpha11 }.
% 0.45/1.11 { ! alpha35, ! hskp6, alpha50 }.
% 0.45/1.11 { hskp6, alpha35 }.
% 0.45/1.11 { ! alpha50, alpha35 }.
% 0.45/1.11 { ! alpha50, alpha61 }.
% 0.45/1.11 { ! alpha50, ! c2_1( a76 ) }.
% 0.45/1.11 { ! alpha61, c2_1( a76 ), alpha50 }.
% 0.45/1.11 { ! alpha61, ndr1_0 }.
% 0.45/1.11 { ! alpha61, c0_1( a76 ) }.
% 0.45/1.11 { ! alpha61, c1_1( a76 ) }.
% 0.45/1.11 { ! ndr1_0, ! c0_1( a76 ), ! c1_1( a76 ), alpha61 }.
% 0.45/1.11 { ! alpha21, alpha1 }.
% 0.45/1.11 { ! alpha21, alpha36 }.
% 0.45/1.11 { ! alpha1, ! alpha36, alpha21 }.
% 0.45/1.11 { ! alpha36, ! hskp5, alpha51 }.
% 0.45/1.11 { hskp5, alpha36 }.
% 0.45/1.11 { ! alpha51, alpha36 }.
% 0.45/1.11 { ! alpha51, alpha62 }.
% 0.45/1.11 { ! alpha51, ! c1_1( a75 ) }.
% 0.45/1.11 { ! alpha62, c1_1( a75 ), alpha51 }.
% 0.45/1.11 { ! alpha62, ndr1_0 }.
% 0.45/1.11 { ! alpha62, ! c0_1( a75 ) }.
% 0.45/1.11 { ! alpha62, c2_1( a75 ) }.
% 0.45/1.11 { ! ndr1_0, c0_1( a75 ), ! c2_1( a75 ), alpha62 }.
% 0.45/1.11 { ! alpha1, alpha3 }.
% 0.45/1.11 { ! alpha1, alpha6 }.
% 0.45/1.11 { ! alpha3, ! alpha6, alpha1 }.
% 0.45/1.11 { ! alpha6, ! hskp4, alpha12 }.
% 0.45/1.11 { hskp4, alpha6 }.
% 0.45/1.11 { ! alpha12, alpha6 }.
% 0.45/1.11 { ! alpha12, alpha22 }.
% 0.45/1.11 { ! alpha12, ! c2_1( a73 ) }.
% 0.45/1.11 { ! alpha22, c2_1( a73 ), alpha12 }.
% 0.45/1.11 { ! alpha22, ndr1_0 }.
% 0.45/1.11 { ! alpha22, c1_1( a73 ) }.
% 0.45/1.11 { ! alpha22, c0_1( a73 ) }.
% 0.45/1.11 { ! ndr1_0, ! c1_1( a73 ), ! c0_1( a73 ), alpha22 }.
% 0.45/1.11 { ! alpha3, alpha7 }.
% 0.45/1.11 { ! alpha3, alpha13 }.
% 0.45/1.11 { ! alpha7, ! alpha13, alpha3 }.
% 0.45/1.11 { ! alpha13, ! hskp3, alpha23 }.
% 0.45/1.11 { hskp3, alpha13 }.
% 0.45/1.11 { ! alpha23, alpha13 }.
% 0.45/1.11 { ! alpha23, alpha37 }.
% 0.45/1.11 { ! alpha23, ! c1_1( a71 ) }.
% 0.45/1.11 { ! alpha37, c1_1( a71 ), alpha23 }.
% 0.45/1.11 { ! alpha37, ndr1_0 }.
% 0.45/1.11 { ! alpha37, c0_1( a71 ) }.
% 0.45/1.11 { ! alpha37, c3_1( a71 ) }.
% 0.45/1.11 { ! ndr1_0, ! c0_1( a71 ), ! c3_1( a71 ), alpha37 }.
% 0.45/1.11 { ! alpha7, alpha14 }.
% 0.45/1.11 { ! alpha7, alpha24 }.
% 0.45/1.11 { ! alpha14, ! alpha24, alpha7 }.
% 0.45/1.11 { ! alpha24, ! hskp2, alpha38 }.
% 0.45/1.11 { hskp2, alpha24 }.
% 0.45/1.11 { ! alpha38, alpha24 }.
% 0.45/1.11 { ! alpha38, alpha52 }.
% 0.45/1.11 { ! alpha38, ! c2_1( a69 ) }.
% 0.45/1.11 { ! alpha52, c2_1( a69 ), alpha38 }.
% 0.45/1.11 { ! alpha52, ndr1_0 }.
% 0.45/1.11 { ! alpha52, ! c0_1( a69 ) }.
% 0.45/1.11 { ! alpha52, c3_1( a69 ) }.
% 0.45/1.11 { ! ndr1_0, c0_1( a69 ), ! c3_1( a69 ), alpha52 }.
% 0.45/1.11 { ! alpha14, alpha25 }.
% 0.45/1.11 { ! alpha14, alpha39 }.
% 0.45/1.11 { ! alpha25, ! alpha39, alpha14 }.
% 0.45/1.11 { ! alpha39, ! hskp1, alpha53 }.
% 0.45/1.11 { hskp1, alpha39 }.
% 0.45/1.11 { ! alpha53, alpha39 }.
% 0.45/1.11 { ! alpha53, alpha63 }.
% 0.45/1.11 { ! alpha53, ! c3_1( a66 ) }.
% 0.45/1.11 { ! alpha63, c3_1( a66 ), alpha53 }.
% 0.45/1.11 { ! alpha63, ndr1_0 }.
% 0.45/1.11 { ! alpha63, c0_1( a66 ) }.
% 0.45/1.11 { ! alpha63, c1_1( a66 ) }.
% 0.45/1.11 { ! ndr1_0, ! c0_1( a66 ), ! c1_1( a66 ), alpha63 }.
% 0.45/1.11 { ! alpha25, ! hskp0, alpha40 }.
% 0.45/1.11 { hskp0, alpha25 }.
% 0.45/1.11 { ! alpha40, alpha25 }.
% 0.45/1.11 { ! alpha40, alpha54 }.
% 0.45/1.11 { ! alpha40, ! c2_1( a61 ) }.
% 0.45/1.11 { ! alpha54, c2_1( a61 ), alpha40 }.
% 0.45/1.11 { ! alpha54, ndr1_0 }.
% 0.45/1.11 { ! alpha54, c3_1( a61 ) }.
% 0.45/1.11 { ! alpha54, c1_1( a61 ) }.
% 0.45/1.11 { ! ndr1_0, ! c3_1( a61 ), ! c1_1( a61 ), alpha54 }.
% 0.45/1.11
% 0.45/1.11 percentage equality = 0.000000, percentage horn = 0.803653
% 0.45/1.11 This a non-horn, non-equality problem
% 0.45/1.11
% 0.45/1.11
% 0.45/1.11 Options Used:
% 0.45/1.11
% 0.45/1.11 useres = 1
% 0.45/1.11 useparamod = 0
% 0.45/1.11 useeqrefl = 0
% 0.45/1.11 useeqfact = 0
% 0.45/1.11 usefactor = 1
% 0.45/1.11 usesimpsplitting = 0
% 0.45/1.11 usesimpdemod = 0
% 0.45/1.11 usesimpres = 3
% 0.45/1.11
% 0.45/1.11 resimpinuse = 1000
% 0.45/1.11 resimpclauses = 20000
% 0.45/1.11 substype = standard
% 0.45/1.11 backwardsubs = 1
% 0.45/1.11 selectoldest = 5
% 0.45/1.11
% 0.45/1.11 litorderings [0] = split
% 0.45/1.11 litorderings [1] = liftord
% 0.45/1.11
% 0.45/1.11 termordering = none
% 0.45/1.11
% 0.45/1.11 litapriori = 1
% 0.45/1.11 termapriori = 0
% 0.45/1.11 litaposteriori = 0
% 0.45/1.11 termaposteriori = 0
% 0.45/1.11 demodaposteriori = 0
% 0.45/1.11 ordereqreflfact = 0
% 0.45/1.11
% 0.45/1.11 litselect = none
% 0.45/1.11
% 0.45/1.11 maxweight = 15
% 0.45/1.11 maxdepth = 30000
% 0.45/1.11 maxlength = 115
% 0.45/1.11 maxnrvars = 195
% 0.45/1.11 excuselevel = 1
% 0.45/1.11 increasemaxweight = 1
% 0.45/1.11
% 0.45/1.11 maxselected = 10000000
% 0.45/1.11 maxnrclauses = 10000000
% 0.45/1.11
% 0.45/1.11 showgenerated = 0
% 0.45/1.11 showkept = 0
% 0.45/1.11 showselected = 0
% 0.45/1.11 showdeleted = 0
% 0.45/1.11 showresimp = 1
% 0.45/1.11 showstatus = 2000
% 0.45/1.11
% 0.45/1.11 prologoutput = 0
% 0.45/1.11 nrgoals = 5000000
% 0.45/1.11 totalproof = 1
% 0.45/1.11
% 0.45/1.11 Symbols occurring in the translation:
% 0.45/1.11
% 0.45/1.11 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.45/1.11 . [1, 2] (w:1, o:120, a:1, s:1, b:0),
% 0.45/1.11 ! [4, 1] (w:0, o:111, a:1, s:1, b:0),
% 0.45/1.11 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.45/1.11 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.45/1.11 hskp0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.82/1.18 ndr1_0 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.82/1.18 a61 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.82/1.18 c3_1 [38, 1] (w:1, o:117, a:1, s:1, b:0),
% 0.82/1.18 c1_1 [39, 1] (w:1, o:119, a:1, s:1, b:0),
% 0.82/1.18 c2_1 [40, 1] (w:1, o:116, a:1, s:1, b:0),
% 0.82/1.18 hskp1 [41, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.82/1.18 a66 [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.82/1.18 c0_1 [43, 1] (w:1, o:118, a:1, s:1, b:0),
% 0.82/1.18 hskp2 [44, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.82/1.18 a69 [45, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.82/1.18 hskp3 [46, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.82/1.18 a71 [47, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.82/1.18 hskp4 [48, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.82/1.18 a73 [49, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.82/1.18 hskp5 [50, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.82/1.18 a75 [51, 0] (w:1, o:34, a:1, s:1, b:0),
% 0.82/1.18 hskp6 [52, 0] (w:1, o:35, a:1, s:1, b:0),
% 0.82/1.18 a76 [53, 0] (w:1, o:36, a:1, s:1, b:0),
% 0.82/1.18 hskp7 [54, 0] (w:1, o:37, a:1, s:1, b:0),
% 0.82/1.18 a77 [55, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.82/1.18 hskp8 [56, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.82/1.18 a62 [57, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.82/1.18 hskp9 [58, 0] (w:1, o:40, a:1, s:1, b:0),
% 0.82/1.18 a63 [59, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.82/1.18 hskp10 [60, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.82/1.18 a64 [61, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.82/1.18 hskp11 [62, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.82/1.18 a65 [63, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.82/1.18 hskp12 [64, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.82/1.18 a67 [65, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.82/1.18 hskp13 [66, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.82/1.18 a68 [67, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.82/1.18 hskp14 [68, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.82/1.18 a70 [69, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.82/1.18 hskp15 [70, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.82/1.18 a72 [71, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.82/1.18 hskp16 [72, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.82/1.18 a74 [73, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.82/1.18 alpha1 [80, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.82/1.18 alpha2 [81, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.82/1.18 alpha3 [82, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.82/1.18 alpha4 [83, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.82/1.18 alpha5 [84, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.82/1.18 alpha6 [85, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.82/1.18 alpha7 [86, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.82/1.18 alpha8 [87, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.82/1.18 alpha9 [88, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.82/1.18 alpha10 [89, 0] (w:1, o:48, a:1, s:1, b:0),
% 0.82/1.18 alpha11 [90, 0] (w:1, o:49, a:1, s:1, b:0),
% 0.82/1.18 alpha12 [91, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.82/1.18 alpha13 [92, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.82/1.18 alpha14 [93, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.82/1.18 alpha15 [94, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.82/1.18 alpha16 [95, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.82/1.18 alpha17 [96, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.82/1.18 alpha18 [97, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.82/1.18 alpha19 [98, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.82/1.18 alpha20 [99, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.82/1.18 alpha21 [100, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.82/1.18 alpha22 [101, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.82/1.18 alpha23 [102, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.82/1.18 alpha24 [103, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.82/1.18 alpha25 [104, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.82/1.18 alpha26 [105, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.82/1.18 alpha27 [106, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.82/1.18 alpha28 [107, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.82/1.18 alpha29 [108, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.82/1.18 alpha30 [109, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.82/1.18 alpha31 [110, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.82/1.18 alpha32 [111, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.82/1.18 alpha33 [112, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.82/1.18 alpha34 [113, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.82/1.18 alpha35 [114, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.82/1.18 alpha36 [115, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.82/1.18 alpha37 [116, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.82/1.18 alpha38 [117, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.82/1.18 alpha39 [118, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.82/1.18 alpha40 [119, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.82/1.18 alpha41 [120, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.82/1.18 alpha42 [121, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.82/1.18 alpha43 [122, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.82/1.18 alpha44 [123, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.82/1.18 alpha45 [124, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.82/1.18 alpha46 [125, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.82/1.18 alpha47 [126, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.82/1.18 alpha48 [127, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.82/1.18 alpha49 [128, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.82/1.18 alpha50 [129, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.82/1.18 alpha51 [130, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.82/1.18 alpha52 [131, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.82/1.18 alpha53 [132, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.82/1.18 alpha54 [133, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.82/1.18 alpha55 [134, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.82/1.18 alpha56 [135, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.82/1.18 alpha57 [136, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.82/1.18 alpha58 [137, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.82/1.18 alpha59 [138, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.82/1.18 alpha60 [139, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.82/1.18 alpha61 [140, 0] (w:1, o:104, a:1, s:1, b:0),
% 0.82/1.18 alpha62 [141, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.82/1.18 alpha63 [142, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.82/1.18 alpha64 [143, 0] (w:1, o:107, a:1, s:1, b:0).
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 *** allocated 15000 integers for clauses
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 15
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 835
% 0.82/1.18 Kept: 289
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 16
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 16
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 835
% 0.82/1.18 Kept: 293
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 17
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 17
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 835
% 0.82/1.18 Kept: 300
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 18
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 18
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 838
% 0.82/1.18 Kept: 316
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 19
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 19
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 841
% 0.82/1.18 Kept: 319
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 20
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18 Failed to find proof!
% 0.82/1.18 maxweight = 20
% 0.82/1.18 maxnrclauses = 10000000
% 0.82/1.18 Generated: 841
% 0.82/1.18 Kept: 319
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 The strategy used was not complete!
% 0.82/1.18
% 0.82/1.18 Increased maxweight to 21
% 0.82/1.18
% 0.82/1.18 Starting Search:
% 0.82/1.18
% 0.82/1.18 Resimplifying inuse:
% 0.82/1.18 Done
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 found a saturation!
% 0.82/1.18 % SZS status CounterSatisfiable
% 0.82/1.18 % SZS output start Saturation
% 0.82/1.18
% 0.82/1.18 (287) {G22,W14,D2,L10,V1,M1} R(251,211);f { hskp4, ! c2_1( X ), hskp3,
% 0.82/1.18 hskp15, hskp9, hskp10, c3_1( X ), ! c3_1( a71 ), alpha37, ! c0_1( X ) }.
% 0.82/1.18 (318) {G23,W13,D2,L10,V0,M1} R(286,211);f { hskp4, hskp3, hskp15, hskp9,
% 0.82/1.18 hskp10, ! c2_1( a75 ), ! c3_1( a71 ), alpha62, alpha37, c3_1( a75 ) }.
% 0.82/1.18 (286) {G22,W14,D2,L10,V1,M1} R(251,214);f { hskp4, ! c2_1( a75 ), hskp3,
% 0.82/1.18 hskp15, hskp9, hskp10, c3_1( a75 ), ! c3_1( X ), alpha62, c0_1( X ) }.
% 0.82/1.18 (313) {G22,W13,D2,L9,V0,M1} R(260,214);f { hskp4, ! c2_1( a75 ), alpha54,
% 0.82/1.18 hskp9, ! c3_1( a61 ), hskp10, c3_1( a75 ), alpha62, c0_1( a61 ) }.
% 0.82/1.18 (260) {G21,W14,D2,L9,V1,M2} R(228,186);f { hskp4, ! c2_1( X ), ! c3_1( a61
% 0.82/1.18 ), alpha54, hskp9, c3_1( X ), hskp10, c0_1( a61 ), ! c0_1( X ) }.
% 0.82/1.18 (299) {G22,W13,D2,L9,V0,M1} R(263,214);f { hskp4, ! c2_1( a75 ), alpha64,
% 0.82/1.18 hskp9, ! c3_1( a72 ), hskp10, c3_1( a75 ), alpha62, c0_1( a72 ) }.
% 0.82/1.18 (309) {G22,W13,D2,L9,V0,M1} R(255,211);f { hskp4, ! c2_1( a72 ), hskp3,
% 0.82/1.18 hskp15, ! c3_1( a71 ), alpha64, ! c3_1( a72 ), alpha37, ! c0_1( a72 ) }.
% 0.82/1.18 (310) {G22,W12,D2,L9,V0,M1} R(255,192);r(191) { hskp4, hskp3, hskp15, !
% 0.82/1.18 c2_1( a72 ), alpha64, ! c3_1( a72 ), hskp13, hskp14, ! c0_1( a72 ) }.
% 0.82/1.18 (255) {G21,W14,D2,L9,V1,M2} R(223,190) { hskp4, ! c2_1( a72 ), ! c3_1( X )
% 0.82/1.18 , hskp3, hskp15, ! c3_1( a72 ), alpha64, c0_1( X ), ! c0_1( a72 ) }.
% 0.82/1.18 (263) {G21,W14,D2,L9,V1,M2} R(230,186);f { hskp4, ! c2_1( X ), ! c3_1( a72
% 0.82/1.18 ), alpha64, hskp9, c3_1( X ), hskp10, c0_1( a72 ), ! c0_1( X ) }.
% 0.82/1.18 (297) {G22,W13,D2,L9,V0,M1} R(254,211);f { hskp4, ! c2_1( a61 ), hskp3,
% 0.82/1.18 hskp15, ! c3_1( a61 ), alpha54, ! c3_1( a71 ), alpha37, ! c0_1( a61 ) }.
% 0.82/1.18 (298) {G22,W12,D2,L9,V0,M1} R(254,192);r(191) { hskp4, hskp3, hskp15, !
% 0.82/1.18 c2_1( a61 ), alpha54, ! c3_1( a61 ), hskp13, hskp14, ! c0_1( a61 ) }.
% 0.82/1.18 (254) {G21,W14,D2,L9,V1,M2} R(223,206) { hskp4, ! c2_1( a61 ), ! c3_1( X )
% 0.82/1.18 , hskp3, hskp15, ! c3_1( a61 ), alpha54, c0_1( X ), ! c0_1( a61 ) }.
% 0.82/1.18 (289) {G23,W12,D2,L10,V0,M1} R(288,214);f { hskp3, hskp15, hskp4, hskp9,
% 0.82/1.18 hskp10, ! c2_1( a75 ), hskp13, hskp14, alpha62, c3_1( a75 ) }.
% 0.82/1.18 (288) {G22,W13,D2,L10,V1,M1} R(251,192);r(191) { hskp4, hskp3, hskp15,
% 0.82/1.18 hskp9, ! c2_1( X ), hskp10, c3_1( X ), hskp13, hskp14, ! c0_1( X ) }.
% 0.82/1.18 (251) {G21,W15,D2,L10,V2,M2} R(223,186);f { hskp4, ! c2_1( Y ), ! c3_1( X )
% 0.82/1.18 , hskp3, hskp15, hskp9, c3_1( Y ), hskp10, ! c0_1( Y ), c0_1( X ) }.
% 0.82/1.18 (261) {G21,W13,D2,L8,V0,M1} R(228,190) { hskp4, ! c2_1( a72 ), ! c3_1( a61
% 0.82/1.18 ), c0_1( a61 ), alpha54, ! c3_1( a72 ), alpha64, ! c0_1( a72 ) }.
% 0.82/1.18 (262) {G21,W13,D2,L8,V0,M1} R(227,190);f { hskp4, ! c2_1( a61 ), ! c3_1(
% 0.82/1.18 a72 ), ! c0_1( a61 ), ! c3_1( a61 ), alpha54, alpha64, c0_1( a72 ) }.
% 0.82/1.18 (277) {G22,W11,D2,L8,V0,M1} R(248,211);f { hskp4, ! c2_1( a73 ), alpha22,
% 0.82/1.18 hskp3, hskp15, ! c3_1( a71 ), alpha37, ! c0_1( a73 ) }.
% 0.82/1.18 (278) {G22,W10,D2,L8,V0,M1} R(248,192);r(191) { hskp4, alpha22, hskp3,
% 0.82/1.18 hskp15, ! c2_1( a73 ), hskp13, hskp14, ! c0_1( a73 ) }.
% 0.82/1.18 (231) {G20,W15,D2,L9,V2,M1} R(186,184);f { hskp9, c3_1( X ), hskp10, hskp4
% 0.82/1.18 , ! c3_1( Y ), ! c2_1( X ), ! c0_1( X ), c0_1( Y ), c1_1( Y ) }.
% 0.82/1.18 (248) {G21,W12,D2,L8,V1,M2} R(224,185);f;f { hskp4, ! c2_1( a73 ), ! c3_1(
% 0.82/1.18 X ), alpha22, hskp3, hskp15, ! c0_1( a73 ), c0_1( X ) }.
% 0.82/1.18 (270) {G22,W11,D2,L8,V0,M1} R(253,211);f { hskp4, ! c2_1( a66 ), hskp3,
% 0.82/1.18 hskp15, alpha63, ! c3_1( a71 ), alpha37, ! c0_1( a66 ) }.
% 0.82/1.18 (271) {G22,W10,D2,L8,V0,M1} R(253,192);r(191) { hskp4, hskp3, hskp15,
% 0.82/1.18 alpha63, ! c2_1( a66 ), hskp13, hskp14, ! c0_1( a66 ) }.
% 0.82/1.18 (253) {G21,W12,D2,L8,V1,M2} R(223,207);f { hskp4, ! c2_1( a66 ), ! c3_1( X
% 0.82/1.18 ), hskp3, hskp15, alpha63, ! c0_1( a66 ), c0_1( X ) }.
% 0.82/1.18 (229) {G20,W14,D2,L8,V1,M1} R(184,190) { hskp4, ! c3_1( X ), ! c2_1( a72 )
% 0.82/1.18 , ! c0_1( a72 ), c0_1( X ), ! c3_1( a72 ), alpha64, c1_1( X ) }.
% 0.82/1.18 (265) {G22,W11,D2,L8,V0,M1} R(252,211);f { hskp4, ! c2_1( a76 ), hskp3,
% 0.82/1.18 hskp15, alpha61, ! c3_1( a71 ), alpha37, ! c0_1( a76 ) }.
% 0.82/1.18 (266) {G22,W10,D2,L8,V0,M1} R(252,192);r(191) { hskp4, hskp3, hskp15,
% 0.82/1.18 alpha61, ! c2_1( a76 ), hskp13, hskp14, ! c0_1( a76 ) }.
% 0.82/1.18 (252) {G21,W12,D2,L8,V1,M2} R(223,213);f { hskp4, ! c2_1( a76 ), ! c3_1( X
% 0.82/1.18 ), hskp3, hskp15, alpha61, ! c0_1( a76 ), c0_1( X ) }.
% 0.82/1.18 (230) {G20,W12,D2,L7,V1,M1} R(184,190);f { hskp4, ! c3_1( a72 ), ! c2_1( X
% 0.82/1.18 ), ! c0_1( X ), c0_1( a72 ), alpha64, c1_1( X ) }.
% 0.82/1.18 (227) {G20,W14,D2,L8,V1,M1} R(184,206) { hskp4, ! c3_1( X ), ! c2_1( a61 )
% 0.82/1.18 , ! c0_1( a61 ), c0_1( X ), ! c3_1( a61 ), alpha54, c1_1( X ) }.
% 0.82/1.18 (228) {G20,W12,D2,L7,V1,M1} R(184,206);f { hskp4, ! c3_1( a61 ), ! c2_1( X
% 0.82/1.18 ), ! c0_1( X ), c0_1( a61 ), alpha54, c1_1( X ) }.
% 0.82/1.18 (257) {G21,W11,D2,L7,V0,M1} R(225,190);f { hskp4, ! c2_1( a76 ), ! c3_1(
% 0.82/1.18 a72 ), c0_1( a72 ), alpha61, alpha64, ! c0_1( a76 ) }.
% 0.82/1.18 (259) {G21,W11,D2,L7,V0,M1} R(226,190);f { hskp4, ! c2_1( a66 ), ! c3_1(
% 0.82/1.18 a72 ), ! c0_1( a66 ), alpha63, alpha64, c0_1( a72 ) }.
% 0.82/1.18 (258) {G21,W11,D2,L7,V0,M1} R(226,206);f { hskp4, ! c2_1( a66 ), ! c3_1(
% 0.82/1.18 a61 ), c0_1( a61 ), alpha63, alpha54, ! c0_1( a66 ) }.
% 0.82/1.18 (226) {G20,W12,D2,L7,V1,M1} R(184,207);f { hskp4, ! c3_1( X ), ! c2_1( a66
% 0.82/1.18 ), ! c0_1( a66 ), c0_1( X ), alpha63, c1_1( X ) }.
% 0.82/1.18 (256) {G21,W11,D2,L7,V0,M1} R(225,206);f { hskp4, ! c2_1( a76 ), ! c3_1(
% 0.82/1.18 a61 ), c0_1( a61 ), alpha61, alpha54, ! c0_1( a76 ) }.
% 0.82/1.18 (225) {G20,W12,D2,L7,V1,M1} R(184,213);f { hskp4, ! c3_1( X ), ! c2_1( a76
% 0.82/1.18 ), ! c0_1( a76 ), c0_1( X ), alpha61, c1_1( X ) }.
% 0.82/1.18 (250) {G21,W11,D2,L7,V0,M1} R(224,190);f { hskp4, ! c2_1( a73 ), ! c3_1(
% 0.82/1.18 a72 ), c0_1( a72 ), alpha22, alpha64, ! c0_1( a73 ) }.
% 0.82/1.18 (249) {G21,W11,D2,L7,V0,M1} R(224,206);f { hskp4, ! c2_1( a73 ), ! c3_1(
% 0.82/1.18 a61 ), c0_1( a61 ), alpha22, alpha54, ! c0_1( a73 ) }.
% 0.82/1.18 (223) {G20,W13,D2,L8,V2,M1} R(184,185);f;f { hskp4, ! c3_1( X ), ! c2_1( Y
% 0.82/1.18 ), ! c0_1( Y ), c0_1( X ), hskp3, hskp15, c1_1( Y ) }.
% 0.82/1.18 (224) {G20,W12,D2,L7,V1,M1} R(184,212);f { hskp4, ! c3_1( X ), ! c2_1( a73
% 0.82/1.18 ), ! c0_1( a73 ), c0_1( X ), alpha22, c1_1( X ) }.
% 0.82/1.18 (237) {G20,W10,D2,L7,V1,M1} R(187,186);f { hskp0, c2_1( X ), hskp8, hskp9,
% 0.82/1.18 c3_1( X ), hskp10, ! c0_1( X ) }.
% 0.82/1.18 (234) {G20,W9,D2,L6,V0,M1} R(186,201) { hskp9, c3_1( a68 ), hskp10, ! c2_1
% 0.82/1.18 ( a68 ), alpha57, ! c0_1( a68 ) }.
% 0.82/1.18 (233) {G20,W9,D2,L6,V0,M1} R(186,182) { hskp9, c3_1( a74 ), hskp10, ! c2_1
% 0.82/1.18 ( a74 ), alpha41, ! c0_1( a74 ) }.
% 0.82/1.18 (221) {G20,W9,D2,L6,V0,M1} R(185,201) { hskp3, ! c3_1( a68 ), hskp15, !
% 0.82/1.18 c2_1( a68 ), alpha57, c0_1( a68 ) }.
% 0.82/1.18 (232) {G20,W9,D2,L6,V0,M1} R(186,205) { hskp9, c3_1( a63 ), hskp10, ! c2_1
% 0.82/1.18 ( a63 ), alpha60, ! c0_1( a63 ) }.
% 0.82/1.18 (240) {G20,W9,D2,L6,V0,M1} R(187,207) { hskp0, c2_1( a66 ), hskp8, c3_1(
% 0.82/1.18 a66 ), alpha63, ! c0_1( a66 ) }.
% 0.82/1.18 (239) {G20,W9,D2,L6,V0,M1} R(187,213) { hskp0, c2_1( a76 ), hskp8, c3_1(
% 0.82/1.18 a76 ), alpha61, ! c0_1( a76 ) }.
% 0.82/1.18 (238) {G20,W9,D2,L6,V0,M1} R(187,212) { hskp0, c2_1( a73 ), hskp8, c3_1(
% 0.82/1.18 a73 ), alpha22, ! c0_1( a73 ) }.
% 0.82/1.18 (220) {G20,W9,D2,L6,V0,M1} R(185,182) { hskp3, ! c3_1( a74 ), hskp15, !
% 0.82/1.18 c2_1( a74 ), alpha41, c0_1( a74 ) }.
% 0.82/1.18 (241) {G21,W7,D2,L6,V0,M1} R(217,211);f { hskp3, hskp15, hskp7, hskp12,
% 0.82/1.18 alpha37, ! c3_1( a71 ) }.
% 0.82/1.18 (244) {G23,W7,D2,L6,V0,M1} R(243,99) { hskp12, hskp13, hskp14, hskp15,
% 0.82/1.18 hskp3, ! c0_1( a77 ) }.
% 0.82/1.18 (247) {G24,W7,D2,L6,V0,M1} R(245,103) { hskp12, hskp13, hskp14, hskp15,
% 0.82/1.18 hskp3, c3_1( a77 ) }.
% 0.82/1.18 (246) {G24,W7,D2,L6,V0,M1} R(245,102) { hskp12, hskp13, hskp14, hskp15,
% 0.82/1.18 hskp3, ! c2_1( a77 ) }.
% 0.82/1.18 (219) {G20,W9,D2,L6,V0,M1} R(185,205) { hskp3, ! c3_1( a63 ), hskp15, !
% 0.82/1.18 c2_1( a63 ), alpha60, c0_1( a63 ) }.
% 0.82/1.18 (245) {G23,W6,D1,L6,V0,M1} R(243,98) { hskp12, hskp13, hskp14, hskp15,
% 0.82/1.18 hskp3, alpha49 }.
% 0.82/1.18 (243) {G22,W6,D1,L6,V0,M1} R(242,97) { hskp15, hskp12, hskp13, hskp14,
% 0.82/1.18 hskp3, alpha34 }.
% 0.82/1.18 (242) {G21,W6,D1,L6,V0,M1} R(217,192);r(191) { hskp15, hskp3, hskp12,
% 0.82/1.18 hskp13, hskp14, hskp7 }.
% 0.82/1.18 (217) {G20,W8,D2,L6,V1,M1} R(185,183);f;f { hskp3, ! c3_1( X ), hskp15,
% 0.82/1.18 hskp7, hskp12, c0_1( X ) }.
% 0.82/1.18 (187) {G19,W8,D2,L5,V1,M1} R(181,3) { hskp0, c2_1( X ), c3_1( X ), hskp8,
% 0.82/1.18 c1_1( X ) }.
% 0.82/1.18 (236) {G20,W6,D2,L5,V0,M1} R(186,200);r(199) { hskp9, hskp10, hskp1, hskp11
% 0.82/1.18 , ! c0_1( a67 ) }.
% 0.82/1.18 (235) {G20,W6,D2,L5,V0,M1} R(186,194);r(195) { hskp9, hskp10, hskp16, hskp5
% 0.82/1.18 , c3_1( a76 ) }.
% 0.82/1.18 (186) {G19,W8,D2,L5,V1,M1} R(181,4) { hskp9, c3_1( X ), ! c0_1( X ), hskp10
% 0.82/1.18 , ! c1_1( X ) }.
% 0.82/1.18 (222) {G20,W7,D2,L5,V0,M1} R(185,203);f { hskp3, ! c3_1( a65 ), hskp15,
% 0.82/1.18 alpha46, c0_1( a65 ) }.
% 0.82/1.18 (184) {G19,W13,D2,L7,V2,M2} R(181,8) { hskp4, c0_1( X ), ! c3_1( X ), !
% 0.82/1.18 c0_1( Y ), ! c2_1( Y ), c1_1( Y ), c1_1( X ) }.
% 0.82/1.18 (218) {G20,W7,D2,L5,V0,M1} R(185,208);f { hskp3, ! c3_1( a62 ), hskp15,
% 0.82/1.18 alpha33, c0_1( a62 ) }.
% 0.82/1.18 (185) {G19,W8,D2,L5,V1,M1} R(181,7) { hskp3, c0_1( X ), ! c3_1( X ), hskp15
% 0.82/1.18 , ! c1_1( X ) }.
% 0.82/1.18 (216) {G20,W7,D2,L5,V0,M1} R(183,190);f { hskp7, ! c3_1( a72 ), hskp12,
% 0.82/1.18 alpha64, c0_1( a72 ) }.
% 0.82/1.18 (215) {G20,W7,D2,L5,V0,M1} R(183,206);f { hskp7, ! c3_1( a61 ), hskp12,
% 0.82/1.18 alpha54, c0_1( a61 ) }.
% 0.82/1.18 (183) {G19,W8,D2,L5,V1,M1} R(181,10) { hskp7, ! c3_1( X ), c0_1( X ),
% 0.82/1.18 hskp12, c1_1( X ) }.
% 0.82/1.18 (214) {G19,W5,D2,L3,V0,M1} S(124);r(181) { ! c2_1( a75 ), alpha62, c0_1(
% 0.82/1.18 a75 ) }.
% 0.82/1.18 (212) {G19,W5,D2,L3,V0,M1} S(134);r(181) { ! c0_1( a73 ), alpha22, ! c1_1(
% 0.82/1.18 a73 ) }.
% 0.82/1.18 (213) {G19,W5,D2,L3,V0,M1} S(114);r(181) { ! c0_1( a76 ), alpha61, ! c1_1(
% 0.82/1.18 a76 ) }.
% 0.82/1.18 (211) {G19,W5,D2,L3,V0,M1} S(144);r(181) { ! c3_1( a71 ), alpha37, ! c0_1(
% 0.82/1.18 a71 ) }.
% 0.82/1.18 (210) {G19,W5,D2,L3,V0,M1} S(104);r(181) { c2_1( a77 ), alpha49, ! c3_1(
% 0.82/1.18 a77 ) }.
% 0.82/1.18 (209) {G19,W5,D2,L3,V0,M1} S(154);r(181) { ! c3_1( a69 ), alpha52, c0_1(
% 0.82/1.18 a69 ) }.
% 0.82/1.18 (207) {G19,W5,D2,L3,V0,M1} S(164);r(181) { ! c0_1( a66 ), alpha63, ! c1_1(
% 0.82/1.18 a66 ) }.
% 0.82/1.18 (208) {G19,W5,D2,L3,V0,M1} S(94);r(181) { ! c3_1( a62 ), alpha33, c1_1( a62
% 0.82/1.18 ) }.
% 0.82/1.18 (206) {G19,W5,D2,L3,V0,M1} S(172);r(181) { ! c3_1( a61 ), alpha54, ! c1_1(
% 0.82/1.18 a61 ) }.
% 0.82/1.18 (205) {G19,W5,D2,L3,V0,M1} S(84);r(181) { ! c2_1( a63 ), alpha60, c1_1( a63
% 0.82/1.18 ) }.
% 0.82/1.18 (182) {G19,W5,D2,L3,V0,M1} R(181,14) { ! c2_1( a74 ), alpha41, c1_1( a74 )
% 0.82/1.18 }.
% 0.82/1.18 (190) {G19,W5,D2,L3,V0,M1} S(24);r(181) { ! c3_1( a72 ), alpha64, ! c1_1(
% 0.82/1.18 a72 ) }.
% 0.82/1.18 (197) {G19,W5,D2,L3,V0,M1} S(34);r(181) { ! c3_1( a70 ), alpha56, c0_1( a70
% 0.82/1.18 ) }.
% 0.82/1.18 (204) {G19,W5,D2,L3,V0,M1} S(74);r(181) { c2_1( a64 ), alpha59, c3_1( a64 )
% 0.82/1.18 }.
% 0.82/1.18 (201) {G19,W5,D2,L3,V0,M1} S(44);r(181) { ! c2_1( a68 ), alpha57, c1_1( a68
% 0.82/1.18 ) }.
% 0.82/1.18 (202) {G19,W5,D2,L3,V0,M1} S(54);r(181) { c2_1( a67 ), alpha58, c3_1( a67 )
% 0.82/1.18 }.
% 0.82/1.18 (203) {G19,W5,D2,L3,V0,M1} S(64);r(181) { c0_1( a65 ), alpha46, c1_1( a65 )
% 0.82/1.18 }.
% 0.82/1.18 (70) {G0,W4,D2,L3,V0,M1} I { ! c0_1( a64 ), alpha47, ! alpha59 }.
% 0.82/1.18 (80) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a63 ), alpha48, ! alpha60 }.
% 0.82/1.18 (90) {G0,W4,D2,L3,V0,M1} I { ! c0_1( a62 ), alpha19, ! alpha33 }.
% 0.82/1.18 (100) {G0,W4,D2,L3,V0,M1} I { c0_1( a77 ), alpha34, ! alpha49 }.
% 0.82/1.18 (110) {G0,W4,D2,L3,V0,M1} I { c2_1( a76 ), alpha50, ! alpha61 }.
% 0.82/1.18 (60) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a65 ), alpha30, ! alpha46 }.
% 0.82/1.18 (120) {G0,W4,D2,L3,V0,M1} I { c1_1( a75 ), alpha51, ! alpha62 }.
% 0.82/1.18 (130) {G0,W4,D2,L3,V0,M1} I { c2_1( a73 ), alpha12, ! alpha22 }.
% 0.82/1.18 (140) {G0,W4,D2,L3,V0,M1} I { c1_1( a71 ), alpha23, ! alpha37 }.
% 0.82/1.18 (150) {G0,W4,D2,L3,V0,M1} I { c2_1( a69 ), alpha38, ! alpha52 }.
% 0.82/1.18 (160) {G0,W4,D2,L3,V0,M1} I { c3_1( a66 ), alpha53, ! alpha63 }.
% 0.82/1.18 (168) {G0,W4,D2,L3,V0,M1} I { c2_1( a61 ), alpha40, ! alpha54 }.
% 0.82/1.18 (191) {G18,W4,D2,L3,V0,M1} R(153,189) { hskp13, hskp14, c3_1( a69 ) }.
% 0.82/1.18 (192) {G18,W4,D2,L3,V0,M1} R(152,189) { hskp13, hskp14, ! c0_1( a69 ) }.
% 0.82/1.18 (50) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a67 ), alpha45, ! alpha58 }.
% 0.82/1.18 (193) {G17,W4,D2,L3,V0,M1} R(149,173) { hskp13, hskp14, ! c2_1( a69 ) }.
% 0.82/1.18 (194) {G14,W4,D2,L3,V0,M1} R(113,188) { hskp16, hskp5, c1_1( a76 ) }.
% 0.82/1.18 (195) {G14,W4,D2,L3,V0,M1} R(112,188) { hskp16, hskp5, c0_1( a76 ) }.
% 0.82/1.18 (196) {G13,W4,D2,L3,V0,M1} R(109,174) { hskp16, hskp5, ! c2_1( a76 ) }.
% 0.82/1.18 (198) {G8,W4,D2,L3,V0,M1} R(53,176) { hskp1, hskp11, ! c2_1( a67 ) }.
% 0.82/1.18 (199) {G8,W4,D2,L3,V0,M1} R(52,176) { hskp1, hskp11, ! c3_1( a67 ) }.
% 0.82/1.18 (200) {G7,W4,D2,L3,V0,M1} R(49,175) { hskp1, hskp11, c1_1( a67 ) }.
% 0.82/1.18 (49) {G0,W3,D2,L2,V0,M1} I { c1_1( a67 ), ! alpha45 }.
% 0.82/1.18 (43) {G0,W3,D2,L2,V0,M1} I { c2_1( a68 ), ! alpha57 }.
% 0.82/1.18 (52) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a67 ), ! alpha58 }.
% 0.82/1.18 (53) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a67 ), ! alpha58 }.
% 0.82/1.18 (59) {G0,W3,D2,L2,V0,M1} I { c2_1( a65 ), ! alpha30 }.
% 0.82/1.18 (62) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a65 ), ! alpha46 }.
% 0.82/1.18 (42) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a68 ), ! alpha57 }.
% 0.82/1.18 (63) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a65 ), ! alpha46 }.
% 0.82/1.18 (69) {G0,W3,D2,L2,V0,M1} I { c0_1( a64 ), ! alpha47 }.
% 0.82/1.18 (72) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a64 ), ! alpha59 }.
% 0.82/1.18 (73) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a64 ), ! alpha59 }.
% 0.82/1.18 (40) {G0,W4,D2,L3,V0,M1} I { ! c0_1( a68 ), alpha44, ! alpha57 }.
% 0.82/1.18 (79) {G0,W3,D2,L2,V0,M1} I { c3_1( a63 ), ! alpha48 }.
% 0.82/1.18 (82) {G0,W3,D2,L2,V0,M1} I { c2_1( a63 ), ! alpha60 }.
% 0.82/1.18 (83) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a63 ), ! alpha60 }.
% 0.82/1.18 (89) {G0,W3,D2,L2,V0,M1} I { c0_1( a62 ), ! alpha19 }.
% 0.82/1.18 (39) {G0,W3,D2,L2,V0,M1} I { c0_1( a68 ), ! alpha44 }.
% 0.82/1.18 (92) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a62 ), ! alpha33 }.
% 0.82/1.18 (93) {G0,W3,D2,L2,V0,M1} I { c3_1( a62 ), ! alpha33 }.
% 0.82/1.18 (99) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a77 ), ! alpha34 }.
% 0.82/1.18 (102) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a77 ), ! alpha49 }.
% 0.82/1.18 (103) {G0,W3,D2,L2,V0,M1} I { c3_1( a77 ), ! alpha49 }.
% 0.82/1.18 (109) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a76 ), ! alpha50 }.
% 0.82/1.18 (112) {G0,W3,D2,L2,V0,M1} I { c0_1( a76 ), ! alpha61 }.
% 0.82/1.18 (113) {G0,W3,D2,L2,V0,M1} I { c1_1( a76 ), ! alpha61 }.
% 0.82/1.18 (33) {G0,W3,D2,L2,V0,M1} I { c3_1( a70 ), ! alpha56 }.
% 0.82/1.18 (119) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a75 ), ! alpha51 }.
% 0.82/1.18 (122) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a75 ), ! alpha62 }.
% 0.82/1.18 (123) {G0,W3,D2,L2,V0,M1} I { c2_1( a75 ), ! alpha62 }.
% 0.82/1.18 (129) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a73 ), ! alpha12 }.
% 0.82/1.18 (32) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a70 ), ! alpha56 }.
% 0.82/1.18 (132) {G0,W3,D2,L2,V0,M1} I { c1_1( a73 ), ! alpha22 }.
% 0.82/1.18 (133) {G0,W3,D2,L2,V0,M1} I { c0_1( a73 ), ! alpha22 }.
% 0.82/1.18 (139) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a71 ), ! alpha23 }.
% 0.82/1.18 (142) {G0,W3,D2,L2,V0,M1} I { c0_1( a71 ), ! alpha37 }.
% 0.82/1.18 (30) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a70 ), alpha43, ! alpha56 }.
% 0.82/1.18 (143) {G0,W3,D2,L2,V0,M1} I { c3_1( a71 ), ! alpha37 }.
% 0.82/1.18 (149) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a69 ), ! alpha38 }.
% 0.82/1.18 (152) {G0,W3,D2,L2,V0,M1} I { ! c0_1( a69 ), ! alpha52 }.
% 0.82/1.18 (153) {G0,W3,D2,L2,V0,M1} I { c3_1( a69 ), ! alpha52 }.
% 0.82/1.18 (29) {G0,W3,D2,L2,V0,M1} I { c1_1( a70 ), ! alpha43 }.
% 0.82/1.18 (159) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a66 ), ! alpha53 }.
% 0.82/1.18 (162) {G0,W3,D2,L2,V0,M1} I { c0_1( a66 ), ! alpha63 }.
% 0.82/1.18 (163) {G0,W3,D2,L2,V0,M1} I { c1_1( a66 ), ! alpha63 }.
% 0.82/1.18 (167) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a61 ), ! alpha40 }.
% 0.82/1.18 (170) {G0,W3,D2,L2,V0,M1} I { c3_1( a61 ), ! alpha54 }.
% 0.82/1.18 (171) {G0,W3,D2,L2,V0,M1} I { c1_1( a61 ), ! alpha54 }.
% 0.82/1.18 (189) {G17,W3,D1,L3,V0,M1} R(173,148) { hskp13, hskp14, alpha52 }.
% 0.82/1.18 (173) {G16,W3,D1,L3,V0,M1} R(147,6) { hskp13, hskp14, alpha38 }.
% 0.82/1.18 (23) {G0,W3,D2,L2,V0,M1} I { c3_1( a72 ), ! alpha64 }.
% 0.82/1.18 (188) {G13,W3,D1,L3,V0,M1} R(174,108) { hskp16, hskp5, alpha61 }.
% 0.82/1.18 (174) {G12,W3,D1,L3,V0,M1} R(107,9) { hskp16, hskp5, alpha50 }.
% 0.82/1.18 (181) {G18,W1,D1,L1,V0,M1} R(180,158);r(161) { ndr1_0 }.
% 0.82/1.18 (22) {G0,W3,D2,L2,V0,M1} I { c1_1( a72 ), ! alpha64 }.
% 0.82/1.18 (176) {G7,W3,D1,L3,V0,M1} R(175,48) { hskp1, hskp11, alpha58 }.
% 0.82/1.18 (20) {G0,W4,D2,L3,V0,M1} I { ! c0_1( a72 ), alpha55, ! alpha64 }.
% 0.82/1.18 (175) {G6,W3,D1,L3,V0,M1} R(47,5) { hskp1, hskp11, alpha45 }.
% 0.82/1.18 (27) {G3,W2,D1,L2,V0,M1} I;r(26) { alpha43, ! hskp14 }.
% 0.82/1.18 (28) {G0,W2,D1,L2,V0,M1} I { alpha56, ! alpha43 }.
% 0.82/1.18 (19) {G0,W3,D2,L2,V0,M1} I { c0_1( a72 ), ! alpha55 }.
% 0.82/1.18 (37) {G4,W2,D1,L2,V0,M1} I;r(36) { alpha44, ! hskp13 }.
% 0.82/1.18 (38) {G0,W2,D1,L2,V0,M1} I { alpha57, ! alpha44 }.
% 0.82/1.18 (18) {G0,W2,D1,L2,V0,M1} I { alpha64, ! alpha55 }.
% 0.82/1.18 (47) {G5,W2,D1,L2,V0,M1} I;r(46) { alpha45, ! hskp12 }.
% 0.82/1.18 (48) {G0,W2,D1,L2,V0,M1} I { alpha58, ! alpha45 }.
% 0.82/1.18 (57) {G6,W2,D1,L2,V0,M1} I;r(56) { alpha30, ! hskp11 }.
% 0.82/1.18 (17) {G2,W2,D1,L2,V0,M1} I;r(16) { alpha55, ! hskp15 }.
% 0.82/1.18 (58) {G0,W2,D1,L2,V0,M1} I { alpha46, ! alpha30 }.
% 0.82/1.18 (67) {G7,W2,D1,L2,V0,M1} I;r(66) { alpha47, ! hskp10 }.
% 0.82/1.18 (68) {G0,W2,D1,L2,V0,M1} I { alpha59, ! alpha47 }.
% 0.82/1.18 (77) {G8,W2,D1,L2,V0,M1} I;r(76) { alpha48, ! hskp9 }.
% 0.82/1.18 (78) {G0,W2,D1,L2,V0,M1} I { alpha60, ! alpha48 }.
% 0.82/1.18 (13) {G0,W3,D2,L2,V0,M1} I { c2_1( a74 ), ! alpha41 }.
% 0.82/1.18 (87) {G9,W2,D1,L2,V0,M1} I;r(86) { alpha19, ! hskp8 }.
% 0.82/1.18 (88) {G0,W2,D1,L2,V0,M1} I { alpha33, ! alpha19 }.
% 0.82/1.18 (97) {G10,W2,D1,L2,V0,M1} I;r(96) { alpha34, ! hskp7 }.
% 0.82/1.18 (12) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a74 ), ! alpha41 }.
% 0.82/1.18 (98) {G0,W2,D1,L2,V0,M1} I { alpha49, ! alpha34 }.
% 0.82/1.18 (107) {G11,W2,D1,L2,V0,M1} I;r(106) { alpha50, ! hskp6 }.
% 0.82/1.18 (108) {G0,W2,D1,L2,V0,M1} I { alpha61, ! alpha50 }.
% 0.82/1.18 (117) {G12,W2,D1,L2,V0,M1} I;r(116) { alpha51, ! hskp5 }.
% 0.82/1.18 (118) {G0,W2,D1,L2,V0,M1} I { alpha62, ! alpha51 }.
% 0.82/1.18 (127) {G13,W2,D1,L2,V0,M1} I;r(126) { alpha12, ! hskp4 }.
% 0.82/1.18 (128) {G0,W2,D1,L2,V0,M1} I { alpha22, ! alpha12 }.
% 0.82/1.18 (137) {G14,W2,D1,L2,V0,M1} I;r(136) { alpha23, ! hskp3 }.
% 0.82/1.18 (9) {G0,W3,D1,L3,V0,M1} I { hskp16, hskp5, hskp6 }.
% 0.82/1.18 (138) {G0,W2,D1,L2,V0,M1} I { alpha37, ! alpha23 }.
% 0.82/1.18 (147) {G15,W2,D1,L2,V0,M1} I;r(146) { alpha38, ! hskp2 }.
% 0.82/1.18 (148) {G0,W2,D1,L2,V0,M1} I { alpha52, ! alpha38 }.
% 0.82/1.18 (157) {G16,W2,D1,L2,V0,M1} I;r(156) { alpha53, ! hskp1 }.
% 0.82/1.18 (158) {G0,W2,D1,L2,V0,M1} I { alpha63, ! alpha53 }.
% 0.82/1.18 (165) {G16,W2,D1,L2,V0,M1} I;r(155) { alpha40, ! hskp0 }.
% 0.82/1.18 (166) {G0,W2,D1,L2,V0,M1} I { alpha54, ! alpha40 }.
% 0.82/1.18 (15) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha15 }.
% 0.82/1.18 (6) {G0,W3,D1,L3,V0,M1} I { hskp13, hskp14, hskp2 }.
% 0.82/1.18 (16) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha42 }.
% 0.82/1.18 (25) {G2,W1,D1,L1,V0,M1} I;r(15) { alpha8 }.
% 0.82/1.18 (26) {G2,W1,D1,L1,V0,M1} I;r(15) { alpha27 }.
% 0.82/1.18 (35) {G3,W1,D1,L1,V0,M1} I;r(25) { alpha16 }.
% 0.82/1.18 (5) {G0,W3,D1,L3,V0,M1} I { hskp1, hskp11, hskp12 }.
% 0.82/1.18 (36) {G3,W1,D1,L1,V0,M1} I;r(25) { alpha28 }.
% 0.82/1.18 (45) {G4,W1,D1,L1,V0,M1} I;r(35) { alpha4 }.
% 0.82/1.18 (46) {G4,W1,D1,L1,V0,M1} I;r(35) { alpha29 }.
% 0.82/1.18 (55) {G5,W1,D1,L1,V0,M1} I;r(45) { alpha9 }.
% 0.82/1.18 (56) {G5,W1,D1,L1,V0,M1} I;r(45) { alpha17 }.
% 0.82/1.18 (65) {G6,W1,D1,L1,V0,M1} I;r(55) { alpha18 }.
% 0.82/1.18 (66) {G6,W1,D1,L1,V0,M1} I;r(55) { alpha31 }.
% 0.82/1.18 (75) {G7,W1,D1,L1,V0,M1} I;r(65) { alpha2 }.
% 0.82/1.18 (76) {G7,W1,D1,L1,V0,M1} I;r(65) { alpha32 }.
% 0.82/1.18 (85) {G8,W1,D1,L1,V0,M1} I;r(75) { alpha5 }.
% 0.82/1.18 (86) {G8,W1,D1,L1,V0,M1} I;r(75) { alpha10 }.
% 0.82/1.18 (95) {G9,W1,D1,L1,V0,M1} I;r(85) { alpha11 }.
% 0.82/1.18 (2) {G0,W3,D2,L2,V0,M1} I { c3_1( a74 ), ! hskp16 }.
% 0.82/1.18 (96) {G9,W1,D1,L1,V0,M1} I;r(85) { alpha20 }.
% 0.82/1.18 (105) {G10,W1,D1,L1,V0,M1} I;r(95) { alpha21 }.
% 0.82/1.18 (106) {G10,W1,D1,L1,V0,M1} I;r(95) { alpha35 }.
% 0.82/1.18 (115) {G11,W1,D1,L1,V0,M1} I;r(105) { alpha1 }.
% 0.82/1.18 (1) {G0,W2,D1,L2,V0,M1} I { alpha41, ! hskp16 }.
% 0.82/1.18 (116) {G11,W1,D1,L1,V0,M1} I;r(105) { alpha36 }.
% 0.82/1.18 (125) {G12,W1,D1,L1,V0,M1} I;r(115) { alpha3 }.
% 0.82/1.18 (126) {G12,W1,D1,L1,V0,M1} I;r(115) { alpha6 }.
% 0.82/1.18 (135) {G13,W1,D1,L1,V0,M1} I;r(125) { alpha7 }.
% 0.82/1.18 (0) {G0,W1,D1,L1,V0,M1} I { alpha26 }.
% 0.82/1.18 (136) {G13,W1,D1,L1,V0,M1} I;r(125) { alpha13 }.
% 0.82/1.18 (145) {G14,W1,D1,L1,V0,M1} I;r(135) { alpha14 }.
% 0.82/1.18 (146) {G14,W1,D1,L1,V0,M1} I;r(135) { alpha24 }.
% 0.82/1.18 (155) {G15,W1,D1,L1,V0,M1} I;r(145) { alpha25 }.
% 0.82/1.18 (156) {G15,W1,D1,L1,V0,M1} I;r(145) { alpha39 }.
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 % SZS output end Saturation
% 0.82/1.18 end of saturation!
% 0.82/1.18
% 0.82/1.18 Memory use:
% 0.82/1.18
% 0.82/1.18 space for terms: 4710
% 0.82/1.18 space for clauses: 13789
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 clauses generated: 841
% 0.82/1.18 clauses kept: 319
% 0.82/1.18 clauses selected: 265
% 0.82/1.18 clauses deleted: 81
% 0.82/1.18 clauses inuse deleted: 27
% 0.82/1.18
% 0.82/1.18 subsentry: 411
% 0.82/1.18 literals s-matched: 348
% 0.82/1.18 literals matched: 348
% 0.82/1.18 full subsumption: 81
% 0.82/1.18
% 0.82/1.18 checksum: -1013599261
% 0.82/1.18
% 0.82/1.18
% 0.82/1.18 Bliksem ended
%------------------------------------------------------------------------------