%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN523+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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:52:30 EDT 2022
% Result : CounterSatisfiable 0.73s 1.11s
% Output : Saturation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN523+1 : TPTP v8.1.0. Released v2.1.0.
% 0.04/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Mon Jul 11 16:03:34 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.73/1.09 *** allocated 10000 integers for termspace/termends
% 0.73/1.09 *** allocated 10000 integers for clauses
% 0.73/1.09 *** allocated 10000 integers for justifications
% 0.73/1.09 Bliksem 1.12
% 0.73/1.09
% 0.73/1.09
% 0.73/1.09 Automatic Strategy Selection
% 0.73/1.09
% 0.73/1.09
% 0.73/1.09 Clauses:
% 0.73/1.09
% 0.73/1.09 { alpha28 }.
% 0.73/1.09 { ! c4_0, ! ndr1_0, c4_1( X ), c5_1( X ), c1_1( X ), alpha39 }.
% 0.73/1.09 { ! c4_0, ! ndr1_0, c4_1( X ), c5_1( X ), c1_1( X ), ! ndr1_1( a155 ), !
% 0.73/1.09 c4_2( a155, Y ), ! c2_2( a155, Y ), c5_2( a155, Y ) }.
% 0.73/1.09 { ! alpha39, alpha51 }.
% 0.73/1.09 { ! alpha39, c2_2( a155, a156 ) }.
% 0.73/1.09 { ! alpha51, ! c2_2( a155, a156 ), alpha39 }.
% 0.73/1.09 { ! alpha51, alpha58 }.
% 0.73/1.09 { ! alpha51, c5_2( a155, a156 ) }.
% 0.73/1.09 { ! alpha58, ! c5_2( a155, a156 ), alpha51 }.
% 0.73/1.09 { ! alpha58, alpha64 }.
% 0.73/1.09 { ! alpha58, c1_2( a155, a156 ) }.
% 0.73/1.09 { ! alpha64, ! c1_2( a155, a156 ), alpha58 }.
% 0.73/1.09 { ! alpha64, ndr1_0 }.
% 0.73/1.09 { ! alpha64, ! c4_1( a155 ) }.
% 0.73/1.09 { ! alpha64, ndr1_1( a155 ) }.
% 0.73/1.09 { ! ndr1_0, c4_1( a155 ), ! ndr1_1( a155 ), alpha64 }.
% 0.73/1.09 { ! alpha28, alpha20 }.
% 0.73/1.09 { ! alpha28, alpha40 }.
% 0.73/1.09 { ! alpha20, ! alpha40, alpha28 }.
% 0.73/1.09 { ! alpha40, alpha52, c3_0 }.
% 0.73/1.09 { ! alpha52, alpha40 }.
% 0.73/1.09 { ! c3_0, alpha40 }.
% 0.73/1.09 { ! alpha52, alpha59, alpha65 }.
% 0.73/1.09 { ! alpha59, alpha52 }.
% 0.73/1.09 { ! alpha65, alpha52 }.
% 0.73/1.09 { ! alpha65, alpha69 }.
% 0.73/1.09 { ! alpha65, alpha72 }.
% 0.73/1.09 { ! alpha69, ! alpha72, alpha65 }.
% 0.73/1.09 { ! alpha72, ! ndr1_1( a154 ), ! c5_2( a154, X ), ! c1_2( a154, X ) }.
% 0.73/1.09 { ndr1_1( a154 ), alpha72 }.
% 0.73/1.09 { c5_2( a154, skol1 ), alpha72 }.
% 0.73/1.09 { c1_2( a154, skol1 ), alpha72 }.
% 0.73/1.09 { ! alpha69, ndr1_0 }.
% 0.73/1.09 { ! alpha69, ! c5_1( a154 ) }.
% 0.73/1.09 { ! alpha69, c1_1( a154 ) }.
% 0.73/1.09 { ! ndr1_0, c5_1( a154 ), ! c1_1( a154 ), alpha69 }.
% 0.73/1.09 { ! alpha59, ndr1_0 }.
% 0.73/1.09 { ! alpha59, ! c1_1( a153 ) }.
% 0.73/1.09 { ! alpha59, ! c5_1( a153 ) }.
% 0.73/1.09 { ! ndr1_0, c1_1( a153 ), c5_1( a153 ), alpha59 }.
% 0.73/1.09 { ! alpha20, alpha13 }.
% 0.73/1.09 { ! alpha20, alpha29 }.
% 0.73/1.09 { ! alpha13, ! alpha29, alpha20 }.
% 0.73/1.09 { ! alpha29, alpha41, c5_1( X ), c4_1( X ) }.
% 0.73/1.09 { ! alpha41, alpha29 }.
% 0.73/1.09 { ! c5_1( skol2 ), alpha29 }.
% 0.73/1.09 { ! c4_1( skol2 ), alpha29 }.
% 0.73/1.09 { ! alpha41, alpha53, ! ndr1_0 }.
% 0.73/1.09 { ! alpha53, alpha41 }.
% 0.73/1.09 { ndr1_0, alpha41 }.
% 0.73/1.09 { ! alpha53, alpha60, c2_0 }.
% 0.73/1.09 { ! alpha60, alpha53 }.
% 0.73/1.09 { ! c2_0, alpha53 }.
% 0.73/1.09 { ! alpha60, alpha66 }.
% 0.73/1.09 { ! alpha60, c3_1( a152 ) }.
% 0.73/1.09 { ! alpha66, ! c3_1( a152 ), alpha60 }.
% 0.73/1.09 { ! alpha66, ndr1_0 }.
% 0.73/1.09 { ! alpha66, ! c4_1( a152 ) }.
% 0.73/1.09 { ! alpha66, ! c1_1( a152 ) }.
% 0.73/1.09 { ! ndr1_0, c4_1( a152 ), c1_1( a152 ), alpha66 }.
% 0.73/1.09 { ! alpha13, alpha21 }.
% 0.73/1.09 { ! alpha13, alpha30 }.
% 0.73/1.09 { ! alpha21, ! alpha30, alpha13 }.
% 0.73/1.09 { ! alpha30, ! c3_0, alpha42 }.
% 0.73/1.09 { c3_0, alpha30 }.
% 0.73/1.09 { ! alpha42, alpha30 }.
% 0.73/1.09 { ! alpha42, ndr1_0 }.
% 0.73/1.09 { ! alpha42, ! c2_1( a151 ) }.
% 0.73/1.09 { ! alpha42, ! c3_1( a151 ) }.
% 0.73/1.09 { ! ndr1_0, c2_1( a151 ), c3_1( a151 ), alpha42 }.
% 0.73/1.09 { ! alpha21, alpha8 }.
% 0.73/1.09 { ! alpha21, alpha31 }.
% 0.73/1.09 { ! alpha8, ! alpha31, alpha21 }.
% 0.73/1.09 { ! alpha31, alpha43, c3_0 }.
% 0.73/1.09 { ! alpha43, alpha31 }.
% 0.73/1.09 { ! c3_0, alpha31 }.
% 0.73/1.09 { ! alpha43, alpha54, alpha61 }.
% 0.73/1.09 { ! alpha54, alpha43 }.
% 0.73/1.09 { ! alpha61, alpha43 }.
% 0.73/1.09 { ! alpha61, alpha67 }.
% 0.73/1.09 { ! alpha61, ! c4_1( a150 ) }.
% 0.73/1.09 { ! alpha67, c4_1( a150 ), alpha61 }.
% 0.73/1.09 { ! alpha67, ndr1_0 }.
% 0.73/1.09 { ! alpha67, alpha70 }.
% 0.73/1.09 { ! ndr1_0, ! alpha70, alpha67 }.
% 0.73/1.09 { ! alpha70, ! ndr1_1( a150 ), c5_2( a150, X ), ! c4_2( a150, X ) }.
% 0.73/1.09 { ndr1_1( a150 ), alpha70 }.
% 0.73/1.09 { ! c5_2( a150, skol3 ), alpha70 }.
% 0.73/1.09 { c4_2( a150, skol3 ), alpha70 }.
% 0.73/1.09 { ! alpha54, ! ndr1_0, alpha62 }.
% 0.73/1.09 { ndr1_0, alpha54 }.
% 0.73/1.09 { ! alpha62, alpha54 }.
% 0.73/1.09 { ! alpha62, alpha68( X ), c3_1( X ) }.
% 0.73/1.09 { ! alpha68( skol4 ), alpha62 }.
% 0.73/1.09 { ! c3_1( skol4 ), alpha62 }.
% 0.73/1.09 { ! alpha68( X ), alpha71( X ), c4_1( X ) }.
% 0.73/1.09 { ! alpha71( X ), alpha68( X ) }.
% 0.73/1.09 { ! c4_1( X ), alpha68( X ) }.
% 0.73/1.09 { ! alpha71( X ), ndr1_1( X ) }.
% 0.73/1.09 { ! alpha71( X ), c5_2( X, a149 ) }.
% 0.73/1.09 { ! alpha71( X ), c4_2( X, a149 ) }.
% 0.73/1.09 { ! ndr1_1( X ), ! c5_2( X, a149 ), ! c4_2( X, a149 ), alpha71( X ) }.
% 0.73/1.09 { ! alpha8, alpha4 }.
% 0.73/1.09 { ! alpha8, alpha14 }.
% 0.73/1.09 { ! alpha4, ! alpha14, alpha8 }.
% 0.73/1.09 { ! alpha14, alpha22, alpha32 }.
% 0.73/1.09 { ! alpha22, alpha14 }.
% 0.73/1.09 { ! alpha32, alpha14 }.
% 0.73/1.09 { ! alpha32, alpha44 }.
% 0.73/1.09 { ! alpha32, ! c2_1( a148 ) }.
% 0.73/1.09 { ! alpha44, c2_1( a148 ), alpha32 }.
% 0.73/1.09 { ! alpha44, ndr1_0 }.
% 0.73/1.09 { ! alpha44, c5_1( a148 ) }.
% 0.73/1.09 { ! alpha44, ! c3_1( a148 ) }.
% 0.73/1.09 { ! ndr1_0, ! c5_1( a148 ), c3_1( a148 ), alpha44 }.
% 0.73/1.09 { ! alpha22, ! c5_0, ! c1_0 }.
% 0.73/1.09 { c5_0, alpha22 }.
% 0.73/1.09 { c1_0, alpha22 }.
% 0.73/1.09 { ! alpha4, alpha9 }.
% 0.73/1.09 { ! alpha4, alpha15 }.
% 0.73/1.09 { ! alpha9, ! alpha15, alpha4 }.
% 0.73/1.09 { ! alpha15, alpha23, alpha33 }.
% 0.73/1.09 { ! alpha23, alpha15 }.
% 0.73/1.09 { ! alpha33, alpha15 }.
% 0.73/1.09 { ! alpha33, c5_1( X ), alpha45( X ) }.
% 0.73/1.09 { ! c5_1( skol5 ), alpha33 }.
% 0.73/1.09 { ! alpha45( skol5 ), alpha33 }.
% 0.73/1.09 { ! alpha45( X ), alpha55( X ) }.
% 0.73/1.09 { ! alpha45( X ), ! c5_2( X, a147 ) }.
% 0.73/1.09 { ! alpha55( X ), c5_2( X, a147 ), alpha45( X ) }.
% 0.73/1.09 { ! alpha55( X ), ndr1_1( X ) }.
% 0.73/1.09 { ! alpha55( X ), c3_2( X, a147 ) }.
% 0.73/1.09 { ! alpha55( X ), ! c1_2( X, a147 ) }.
% 0.73/1.09 { ! ndr1_1( X ), ! c3_2( X, a147 ), c1_2( X, a147 ), alpha55( X ) }.
% 0.73/1.09 { ! alpha23, alpha34, ! ndr1_0 }.
% 0.73/1.09 { ! alpha34, alpha23 }.
% 0.73/1.09 { ndr1_0, alpha23 }.
% 0.73/1.09 { ! alpha34, alpha46, c4_0 }.
% 0.73/1.09 { ! alpha46, alpha34 }.
% 0.73/1.09 { ! c4_0, alpha34 }.
% 0.73/1.09 { ! alpha46, ndr1_0 }.
% 0.73/1.09 { ! alpha46, ! c3_1( a146 ) }.
% 0.73/1.09 { ! alpha46, c4_1( a146 ) }.
% 0.73/1.09 { ! ndr1_0, c3_1( a146 ), ! c4_1( a146 ), alpha46 }.
% 0.73/1.09 { ! alpha9, alpha2 }.
% 0.73/1.09 { ! alpha9, alpha16 }.
% 0.73/1.09 { ! alpha2, ! alpha16, alpha9 }.
% 0.73/1.09 { ! alpha16, alpha24, c2_0 }.
% 0.73/1.09 { ! alpha24, alpha16 }.
% 0.73/1.09 { ! c2_0, alpha16 }.
% 0.73/1.09 { ! alpha24, alpha35 }.
% 0.73/1.09 { ! alpha24, ! c5_1( a145 ) }.
% 0.73/1.09 { ! alpha35, c5_1( a145 ), alpha24 }.
% 0.73/1.09 { ! alpha35, alpha47 }.
% 0.73/1.09 { ! alpha35, c3_1( a145 ) }.
% 0.73/1.09 { ! alpha47, ! c3_1( a145 ), alpha35 }.
% 0.73/1.09 { ! alpha47, ndr1_0 }.
% 0.73/1.09 { ! alpha47, alpha56 }.
% 0.73/1.09 { ! ndr1_0, ! alpha56, alpha47 }.
% 0.73/1.09 { ! alpha56, ! ndr1_1( a145 ), alpha63 }.
% 0.73/1.09 { ndr1_1( a145 ), alpha56 }.
% 0.73/1.09 { ! alpha63, alpha56 }.
% 0.73/1.09 { ! alpha63, ! c2_2( a145, X ), ! c5_2( a145, X ), ! c1_2( a145, X ) }.
% 0.73/1.09 { c2_2( a145, skol6 ), alpha63 }.
% 0.73/1.09 { c5_2( a145, skol6 ), alpha63 }.
% 0.73/1.09 { c1_2( a145, skol6 ), alpha63 }.
% 0.73/1.09 { ! alpha2, alpha5 }.
% 0.73/1.09 { ! alpha2, alpha10 }.
% 0.73/1.09 { ! alpha5, ! alpha10, alpha2 }.
% 0.73/1.09 { ! alpha10, alpha17, alpha25 }.
% 0.73/1.09 { ! alpha17, alpha10 }.
% 0.73/1.09 { ! alpha25, alpha10 }.
% 0.73/1.09 { ! alpha25, alpha36( X ), c4_2( X, Y ), c1_2( X, Y ) }.
% 0.73/1.09 { ! alpha36( skol7 ), alpha25 }.
% 0.73/1.09 { ! c4_2( skol7, skol10 ), alpha25 }.
% 0.73/1.09 { ! c1_2( skol7, skol10 ), alpha25 }.
% 0.73/1.09 { ! alpha36( X ), ! c5_1( X ), ! c3_1( X ), ! ndr1_1( X ) }.
% 0.73/1.09 { c5_1( X ), alpha36( X ) }.
% 0.73/1.09 { c3_1( X ), alpha36( X ) }.
% 0.73/1.09 { ndr1_1( X ), alpha36( X ) }.
% 0.73/1.09 { ! alpha17, ! c1_0, ! ndr1_0 }.
% 0.73/1.09 { c1_0, alpha17 }.
% 0.73/1.09 { ndr1_0, alpha17 }.
% 0.73/1.09 { ! alpha5, alpha1 }.
% 0.73/1.09 { ! alpha5, alpha11 }.
% 0.73/1.09 { ! alpha1, ! alpha11, alpha5 }.
% 0.73/1.09 { ! alpha11, ! c4_0, alpha18 }.
% 0.73/1.09 { c4_0, alpha11 }.
% 0.73/1.09 { ! alpha18, alpha11 }.
% 0.73/1.09 { ! alpha18, alpha26 }.
% 0.73/1.09 { ! alpha18, ! c4_1( a144 ) }.
% 0.73/1.09 { ! alpha26, c4_1( a144 ), alpha18 }.
% 0.73/1.09 { ! alpha26, alpha37 }.
% 0.73/1.09 { ! alpha26, c5_1( a144 ) }.
% 0.73/1.09 { ! alpha37, ! c5_1( a144 ), alpha26 }.
% 0.73/1.09 { ! alpha37, ndr1_0 }.
% 0.73/1.09 { ! alpha37, alpha48 }.
% 0.73/1.09 { ! ndr1_0, ! alpha48, alpha37 }.
% 0.73/1.09 { ! alpha48, ! ndr1_1( a144 ), alpha57 }.
% 0.73/1.09 { ndr1_1( a144 ), alpha48 }.
% 0.73/1.09 { ! alpha57, alpha48 }.
% 0.73/1.09 { ! alpha57, c3_2( a144, X ), c4_2( a144, X ), ! c5_2( a144, X ) }.
% 0.73/1.09 { ! c3_2( a144, skol8 ), alpha57 }.
% 0.73/1.09 { ! c4_2( a144, skol8 ), alpha57 }.
% 0.73/1.09 { c5_2( a144, skol8 ), alpha57 }.
% 0.73/1.09 { ! alpha1, alpha3 }.
% 0.73/1.09 { ! alpha1, alpha6 }.
% 0.73/1.09 { ! alpha3, ! alpha6, alpha1 }.
% 0.73/1.09 { ! alpha6, c5_0, c2_0, c1_0 }.
% 0.73/1.09 { ! c5_0, alpha6 }.
% 0.73/1.09 { ! c2_0, alpha6 }.
% 0.73/1.09 { ! c1_0, alpha6 }.
% 0.73/1.09 { ! alpha3, alpha7, ! c2_0 }.
% 0.73/1.09 { ! alpha7, alpha3 }.
% 0.73/1.09 { c2_0, alpha3 }.
% 0.73/1.09 { ! alpha7, alpha12, ndr1_0 }.
% 0.73/1.09 { ! alpha7, alpha12, ! c1_1( a143 ) }.
% 0.73/1.09 { ! alpha12, alpha7 }.
% 0.73/1.09 { ! ndr1_0, c1_1( a143 ), alpha7 }.
% 0.73/1.09 { ! alpha12, ! ndr1_0, alpha19 }.
% 0.73/1.09 { ndr1_0, alpha12 }.
% 0.73/1.09 { ! alpha19, alpha12 }.
% 0.73/1.09 { ! alpha19, alpha27( X ), ! c1_1( X ) }.
% 0.73/1.09 { ! alpha27( skol9 ), alpha19 }.
% 0.73/1.09 { c1_1( skol9 ), alpha19 }.
% 0.73/1.09 { ! alpha27( X ), alpha38( X ), alpha49( X ) }.
% 0.73/1.09 { ! alpha38( X ), alpha27( X ) }.
% 0.73/1.09 { ! alpha49( X ), alpha27( X ) }.
% 0.73/1.09 { ! alpha49( X ), ndr1_1( X ) }.
% 0.73/1.09 { ! alpha49( X ), c3_2( X, a142 ) }.
% 0.73/1.09 { ! alpha49( X ), ! c4_2( X, a142 ) }.
% 0.73/1.09 { ! ndr1_1( X ), ! c3_2( X, a142 ), c4_2( X, a142 ), alpha49( X ) }.
% 0.73/1.09 { ! alpha38( X ), alpha50( X ) }.
% 0.73/1.09 { ! alpha38( X ), ! c1_2( X, a141 ) }.
% 0.73/1.09 { ! alpha50( X ), c1_2( X, a141 ), alpha38( X ) }.
% 0.73/1.09 { ! alpha50( X ), ndr1_1( X ) }.
% 0.73/1.09 { ! alpha50( X ), ! c2_2( X, a141 ) }.
% 0.73/1.09 { ! alpha50( X ), ! c5_2( X, a141 ) }.
% 0.73/1.09 { ! ndr1_1( X ), c2_2( X, a141 ), c5_2( X, a141 ), alpha50( X ) }.
% 0.73/1.09
% 0.73/1.09 percentage equality = 0.000000, percentage horn = 0.731092
% 0.73/1.09 This a non-horn, non-equality problem
% 0.73/1.09
% 0.73/1.09
% 0.73/1.09 Options Used:
% 0.73/1.09
% 0.73/1.09 useres = 1
% 0.73/1.09 useparamod = 0
% 0.73/1.09 useeqrefl = 0
% 0.73/1.09 useeqfact = 0
% 0.73/1.09 usefactor = 1
% 0.73/1.09 usesimpsplitting = 0
% 0.73/1.09 usesimpdemod = 0
% 0.73/1.11 usesimpres = 3
% 0.73/1.11
% 0.73/1.11 resimpinuse = 1000
% 0.73/1.11 resimpclauses = 20000
% 0.73/1.11 substype = standard
% 0.73/1.11 backwardsubs = 1
% 0.73/1.11 selectoldest = 5
% 0.73/1.11
% 0.73/1.11 litorderings [0] = split
% 0.73/1.11 litorderings [1] = liftord
% 0.73/1.11
% 0.73/1.11 termordering = none
% 0.73/1.11
% 0.73/1.11 litapriori = 1
% 0.73/1.11 termapriori = 0
% 0.73/1.11 litaposteriori = 0
% 0.73/1.11 termaposteriori = 0
% 0.73/1.11 demodaposteriori = 0
% 0.73/1.11 ordereqreflfact = 0
% 0.73/1.11
% 0.73/1.11 litselect = none
% 0.73/1.11
% 0.73/1.11 maxweight = 15
% 0.73/1.11 maxdepth = 30000
% 0.73/1.11 maxlength = 115
% 0.73/1.11 maxnrvars = 195
% 0.73/1.11 excuselevel = 1
% 0.73/1.11 increasemaxweight = 1
% 0.73/1.11
% 0.73/1.11 maxselected = 10000000
% 0.73/1.11 maxnrclauses = 10000000
% 0.73/1.11
% 0.73/1.11 showgenerated = 0
% 0.73/1.11 showkept = 0
% 0.73/1.11 showselected = 0
% 0.73/1.11 showdeleted = 0
% 0.73/1.11 showresimp = 1
% 0.73/1.11 showstatus = 2000
% 0.73/1.11
% 0.73/1.11 prologoutput = 0
% 0.73/1.11 nrgoals = 5000000
% 0.73/1.11 totalproof = 1
% 0.73/1.11
% 0.73/1.11 Symbols occurring in the translation:
% 0.73/1.11
% 0.73/1.11 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.11 . [1, 2] (w:1, o:133, a:1, s:1, b:0),
% 0.73/1.11 ! [4, 1] (w:0, o:113, a:1, s:1, b:0),
% 0.73/1.11 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.11 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.11 ndr1_0 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.73/1.11 ndr1_1 [37, 1] (w:1, o:118, a:1, s:1, b:0),
% 0.73/1.11 a141 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.73/1.11 c2_2 [39, 2] (w:1, o:158, a:1, s:1, b:0),
% 0.73/1.11 c5_2 [40, 2] (w:1, o:160, a:1, s:1, b:0),
% 0.73/1.11 c1_2 [41, 2] (w:1, o:157, a:1, s:1, b:0),
% 0.73/1.11 a142 [42, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.73/1.11 c3_2 [43, 2] (w:1, o:161, a:1, s:1, b:0),
% 0.73/1.11 c4_2 [44, 2] (w:1, o:159, a:1, s:1, b:0),
% 0.73/1.11 c1_1 [45, 1] (w:1, o:119, a:1, s:1, b:0),
% 0.73/1.11 a143 [46, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.73/1.11 c2_0 [47, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.73/1.11 c5_0 [48, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.73/1.11 c1_0 [49, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.11 c4_0 [50, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.73/1.11 a144 [52, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.73/1.11 c5_1 [53, 1] (w:1, o:123, a:1, s:1, b:0),
% 0.73/1.11 c4_1 [54, 1] (w:1, o:122, a:1, s:1, b:0),
% 0.73/1.11 c3_1 [56, 1] (w:1, o:121, a:1, s:1, b:0),
% 0.73/1.11 a145 [59, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.73/1.11 a146 [60, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.73/1.11 a147 [62, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.11 a148 [63, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.73/1.11 c2_1 [64, 1] (w:1, o:120, a:1, s:1, b:0),
% 0.73/1.11 a149 [66, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.73/1.11 a150 [68, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.73/1.11 c3_0 [69, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.73/1.11 a151 [70, 0] (w:1, o:34, a:1, s:1, b:0),
% 0.73/1.11 a152 [71, 0] (w:1, o:35, a:1, s:1, b:0),
% 0.73/1.11 a153 [73, 0] (w:1, o:36, a:1, s:1, b:0),
% 0.73/1.11 a154 [74, 0] (w:1, o:37, a:1, s:1, b:0),
% 0.73/1.11 a155 [77, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.73/1.11 a156 [78, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.73/1.11 alpha1 [80, 0] (w:1, o:40, a:1, s:1, b:0),
% 0.73/1.11 alpha2 [81, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.73/1.11 alpha3 [82, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.73/1.11 alpha4 [83, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.73/1.11 alpha5 [84, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.73/1.11 alpha6 [85, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.73/1.11 alpha7 [86, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.73/1.11 alpha8 [87, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.73/1.11 alpha9 [88, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.73/1.11 alpha10 [89, 0] (w:1, o:41, a:1, s:1, b:0),
% 0.73/1.11 alpha11 [90, 0] (w:1, o:42, a:1, s:1, b:0),
% 0.73/1.11 alpha12 [91, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.73/1.11 alpha13 [92, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.73/1.11 alpha14 [93, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.73/1.11 alpha15 [94, 0] (w:1, o:46, a:1, s:1, b:0),
% 0.73/1.11 alpha16 [95, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.73/1.11 alpha17 [96, 0] (w:1, o:48, a:1, s:1, b:0),
% 0.73/1.11 alpha18 [97, 0] (w:1, o:49, a:1, s:1, b:0),
% 0.73/1.11 alpha19 [98, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.73/1.11 alpha20 [99, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.73/1.11 alpha21 [100, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.73/1.11 alpha22 [101, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.73/1.11 alpha23 [102, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.73/1.11 alpha24 [103, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.73/1.11 alpha25 [104, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.73/1.11 alpha26 [105, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.73/1.11 alpha27 [106, 1] (w:1, o:124, a:1, s:1, b:0),
% 0.73/1.11 alpha28 [107, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.73/1.11 alpha29 [108, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.73/1.11 alpha30 [109, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.73/1.11 alpha31 [110, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.73/1.11 alpha32 [111, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.73/1.11 alpha33 [112, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.73/1.11 alpha34 [113, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.73/1.11 alpha35 [114, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.73/1.11 alpha36 [115, 1] (w:1, o:125, a:1, s:1, b:0),
% 0.73/1.11 alpha37 [116, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.73/1.11 alpha38 [117, 1] (w:1, o:126, a:1, s:1, b:0),
% 0.73/1.11 alpha39 [118, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.73/1.11 alpha40 [119, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.73/1.11 alpha41 [120, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.73/1.11 alpha42 [121, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.73/1.11 alpha43 [122, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.73/1.11 alpha44 [123, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.73/1.11 alpha45 [124, 1] (w:1, o:127, a:1, s:1, b:0),
% 0.73/1.11 alpha46 [125, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.73/1.11 alpha47 [126, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.73/1.11 alpha48 [127, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.73/1.11 alpha49 [128, 1] (w:1, o:128, a:1, s:1, b:0),
% 0.73/1.11 alpha50 [129, 1] (w:1, o:129, a:1, s:1, b:0),
% 0.73/1.11 alpha51 [130, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.73/1.11 alpha52 [131, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.73/1.11 alpha53 [132, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.73/1.11 alpha54 [133, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.73/1.11 alpha55 [134, 1] (w:1, o:130, a:1, s:1, b:0),
% 0.73/1.11 alpha56 [135, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.73/1.11 alpha57 [136, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.73/1.11 alpha58 [137, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.73/1.11 alpha59 [138, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.73/1.11 alpha60 [139, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.73/1.11 alpha61 [140, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.73/1.11 alpha62 [141, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.73/1.11 alpha63 [142, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.73/1.11 alpha64 [143, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.73/1.11 alpha65 [144, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.73/1.11 alpha66 [145, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.73/1.11 alpha67 [146, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.73/1.11 alpha68 [147, 1] (w:1, o:131, a:1, s:1, b:0),
% 0.73/1.11 alpha69 [148, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.73/1.11 alpha70 [149, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.73/1.11 alpha71 [150, 1] (w:1, o:132, a:1, s:1, b:0),
% 0.73/1.11 alpha72 [151, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.73/1.11 skol1 [152, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.73/1.11 skol2 [153, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.73/1.11 skol3 [154, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.73/1.11 skol4 [155, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.73/1.11 skol5 [156, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.73/1.11 skol6 [157, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.73/1.11 skol7 [158, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.73/1.11 skol8 [159, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.73/1.11 skol9 [160, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.73/1.11 skol10 [161, 0] (w:1, o:104, a:1, s:1, b:0).
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 Starting Search:
% 0.73/1.11
% 0.73/1.11 *** allocated 15000 integers for clauses
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Failed to find proof!
% 0.73/1.11 maxweight = 15
% 0.73/1.11 maxnrclauses = 10000000
% 0.73/1.11 Generated: 371
% 0.73/1.11 Kept: 283
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 The strategy used was not complete!
% 0.73/1.11
% 0.73/1.11 Increased maxweight to 16
% 0.73/1.11
% 0.73/1.11 Starting Search:
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Failed to find proof!
% 0.73/1.11 maxweight = 16
% 0.73/1.11 maxnrclauses = 10000000
% 0.73/1.11 Generated: 371
% 0.73/1.11 Kept: 283
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 The strategy used was not complete!
% 0.73/1.11
% 0.73/1.11 Increased maxweight to 17
% 0.73/1.11
% 0.73/1.11 Starting Search:
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Failed to find proof!
% 0.73/1.11 maxweight = 17
% 0.73/1.11 maxnrclauses = 10000000
% 0.73/1.11 Generated: 371
% 0.73/1.11 Kept: 283
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 The strategy used was not complete!
% 0.73/1.11
% 0.73/1.11 Increased maxweight to 18
% 0.73/1.11
% 0.73/1.11 Starting Search:
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11 Resimplifying inuse:
% 0.73/1.11 Done
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 found a saturation!
% 0.73/1.11 % SZS status CounterSatisfiable
% 0.73/1.11 % SZS output start Saturation
% 0.73/1.11
% 0.73/1.11 (282) {G7,W18,D2,L8,V2,M1} S(2);r(218) { c4_1( X ), c1_1( X ), ! ndr1_1(
% 0.73/1.11 a155 ), c5_1( X ), ! c2_2( a155, Y ), ! c4_2( a155, Y ), c5_2( a155, Y )
% 0.73/1.11 , ! c4_0 }.
% 0.73/1.11 (283) {G7,W8,D2,L5,V1,M1} S(1);r(218) { c4_1( X ), c1_1( X ), alpha39, c5_1
% 0.73/1.11 ( X ), ! c4_0 }.
% 0.73/1.11 (281) {G12,W7,D2,L5,V0,M1} R(274,113);r(108) { c3_0, alpha54, alpha36( a150
% 0.73/1.11 ), alpha17, ! alpha45( a150 ) }.
% 0.73/1.11 (275) {G6,W12,D2,L6,V0,M1} R(220,204);f { ! ndr1_1( a154 ), c3_0, alpha59,
% 0.73/1.11 ! c1_2( a154, a141 ), alpha50( a154 ), c2_2( a154, a141 ) }.
% 0.73/1.11 (280) {G12,W7,D2,L5,V0,M1} R(277,199);r(198) { c3_0, alpha54, alpha17,
% 0.73/1.11 alpha36( a150 ), ! alpha38( a150 ) }.
% 0.73/1.11 (277) {G11,W10,D2,L6,V0,M1} R(272,268) { c3_0, alpha54, alpha36( a150 ), !
% 0.73/1.11 alpha50( a150 ), alpha17, c1_2( a150, a141 ) }.
% 0.73/1.11 (279) {G15,W10,D2,L5,V0,M1} R(267,86) { ! c1_2( a145, a149 ), c2_0, alpha23
% 0.73/1.11 , ! alpha71( a145 ), ! c2_2( a145, a149 ) }.
% 0.73/1.11 (267) {G14,W11,D2,L5,V1,M1} R(140,262) { ! c2_2( a145, X ), ! c1_2( a145, X
% 0.73/1.11 ), c2_0, alpha23, ! c5_2( a145, X ) }.
% 0.73/1.11 (278) {G11,W10,D2,L6,V0,M1} R(273,268);r(154) { c3_0, alpha54, alpha36(
% 0.73/1.11 a150 ), alpha71( a150 ), alpha17, c1_2( a150, a149 ) }.
% 0.73/1.11 (273) {G10,W9,D2,L5,V0,M1} R(251,88);f;f { ! ndr1_1( a150 ), c3_0, alpha54
% 0.73/1.11 , alpha71( a150 ), ! c4_2( a150, a149 ) }.
% 0.73/1.11 (272) {G10,W7,D2,L4,V0,M1} R(251,203);r(201) { c3_0, alpha54, ! alpha50(
% 0.73/1.11 a150 ), ! c4_2( a150, a141 ) }.
% 0.73/1.11 (276) {G6,W7,D2,L4,V0,M1} R(220,86);r(85) { c3_0, alpha59, ! alpha71( a154
% 0.73/1.11 ), ! c1_2( a154, a149 ) }.
% 0.73/1.11 (220) {G5,W10,D2,L5,V1,M1} R(25,216) { ! ndr1_1( a154 ), ! c1_2( a154, X )
% 0.73/1.11 , c3_0, alpha59, ! c5_2( a154, X ) }.
% 0.73/1.11 (271) {G10,W7,D2,L4,V0,M1} R(251,109);r(250) { c3_0, alpha54, ! alpha45(
% 0.73/1.11 a150 ), ! c4_2( a150, a147 ) }.
% 0.73/1.11 (251) {G9,W10,D2,L5,V1,M1} R(72,232) { ! ndr1_1( a150 ), ! c4_2( a150, X )
% 0.73/1.11 , c3_0, alpha54, c5_2( a150, X ) }.
% 0.73/1.11 (197) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c4_2( X, a142 ), alpha49( X )
% 0.73/1.11 , ! c3_2( X, a142 ) }.
% 0.73/1.11 (204) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c2_2( X, a141 ), alpha50( X )
% 0.73/1.11 , c5_2( X, a141 ) }.
% 0.73/1.11 (173) {G0,W10,D2,L4,V1,M1} I { c3_2( a144, X ), c4_2( a144, X ), ! c5_2(
% 0.73/1.11 a144, X ), ! alpha57 }.
% 0.73/1.11 (269) {G11,W8,D2,L4,V1,M1} R(268,196) { alpha36( X ), alpha17, ! alpha49( X
% 0.73/1.11 ), c1_2( X, a142 ) }.
% 0.73/1.11 (270) {G11,W7,D2,L4,V0,M1} R(268,175) { alpha36( a144 ), alpha17, alpha57,
% 0.73/1.11 c1_2( a144, skol8 ) }.
% 0.73/1.11 (268) {G10,W9,D2,L4,V2,M1} R(147,146) { alpha36( X ), c1_2( X, Y ), alpha17
% 0.73/1.11 , c4_2( X, Y ) }.
% 0.73/1.11 (151) {G0,W8,D2,L4,V1,M1} I { ! c5_1( X ), ! c3_1( X ), ! ndr1_1( X ), !
% 0.73/1.11 alpha36( X ) }.
% 0.73/1.11 (147) {G0,W9,D2,L4,V2,M1} I { alpha36( X ), c4_2( X, Y ), c1_2( X, Y ), !
% 0.73/1.11 alpha25 }.
% 0.73/1.11 (200) {G0,W7,D2,L3,V1,M1} I { ! alpha50( X ), alpha38( X ), c1_2( X, a141 )
% 0.73/1.11 }.
% 0.73/1.11 (264) {G8,W6,D2,L4,V0,M1} R(257,39) { alpha44, alpha41, c3_1( a148 ), c4_1
% 0.73/1.11 ( a148 ) }.
% 0.73/1.11 (263) {G10,W6,D2,L4,V0,M1} R(257,259) { alpha44, alpha23, ndr1_1( a148 ),
% 0.73/1.11 c3_1( a148 ) }.
% 0.73/1.11 (266) {G2,W4,D2,L2,V1,M1} R(191,194);r(244) { ndr1_1( X ), ! alpha27( X )
% 0.73/1.11 }.
% 0.73/1.11 (140) {G0,W10,D2,L4,V1,M1} I { ! c2_2( a145, X ), ! c5_2( a145, X ), ! c1_2
% 0.73/1.11 ( a145, X ), ! alpha63 }.
% 0.73/1.11 (191) {G0,W6,D2,L3,V1,M1} I { ! alpha27( X ), alpha38( X ), alpha49( X )
% 0.73/1.11 }.
% 0.73/1.11 (253) {G1,W6,D2,L3,V1,M1} R(82,85) { c4_1( X ), ndr1_1( X ), ! alpha68( X )
% 0.73/1.11 }.
% 0.73/1.11 (254) {G6,W5,D2,L4,V0,M1} R(227,39) { c3_0, alpha41, alpha59, c4_1( a154 )
% 0.73/1.11 }.
% 0.73/1.11 (265) {G7,W5,D2,L3,V0,M1} S(124);r(218) { c3_1( a146 ), alpha46, ! c4_1(
% 0.73/1.11 a146 ) }.
% 0.73/1.11 (260) {G10,W5,D2,L4,V0,M1} R(259,227) { alpha23, c3_0, alpha59, ndr1_1(
% 0.73/1.11 a154 ) }.
% 0.73/1.11 (219) {G7,W5,D2,L3,V0,M1} R(218,15) { ! ndr1_1( a155 ), alpha64, c4_1( a155
% 0.73/1.11 ) }.
% 0.73/1.11 (234) {G7,W5,D2,L3,V0,M1} S(32);r(218) { ! c1_1( a154 ), alpha69, c5_1(
% 0.73/1.11 a154 ) }.
% 0.73/1.11 (237) {G7,W5,D2,L3,V0,M1} S(36);r(218) { c1_1( a153 ), alpha59, c5_1( a153
% 0.73/1.11 ) }.
% 0.73/1.11 (114) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c1_2( X, a147 ), alpha55( X )
% 0.73/1.11 , ! c3_2( X, a147 ) }.
% 0.73/1.11 (245) {G7,W5,D2,L3,V0,M1} S(52);r(218) { c1_1( a152 ), alpha66, c4_1( a152
% 0.73/1.11 ) }.
% 0.73/1.11 (247) {G7,W5,D2,L3,V0,M1} S(59);r(218) { c2_1( a151 ), alpha42, c3_1( a151
% 0.73/1.11 ) }.
% 0.73/1.11 (257) {G7,W5,D2,L3,V0,M1} S(98);r(218) { c3_1( a148 ), alpha44, ! c5_1(
% 0.73/1.11 a148 ) }.
% 0.73/1.11 (188) {G0,W5,D2,L3,V1,M1} I { alpha27( X ), ! c1_1( X ), ! alpha19 }.
% 0.73/1.11 (110) {G0,W7,D2,L3,V1,M1} I { ! alpha55( X ), alpha45( X ), c5_2( X, a147 )
% 0.73/1.11 }.
% 0.73/1.11 (262) {G13,W3,D1,L3,V0,M1} R(261,256);f { c2_0, alpha23, alpha63 }.
% 0.73/1.11 (261) {G10,W4,D2,L3,V0,M1} R(259,236) { alpha23, c2_0, ndr1_1( a145 ) }.
% 0.73/1.11 (259) {G9,W5,D2,L3,V1,M1} R(258,250) { alpha23, ndr1_1( X ), c5_1( X ) }.
% 0.73/1.11 (258) {G8,W5,D2,L3,V1,M1} R(105,104) { c5_1( X ), alpha23, alpha45( X ) }.
% 0.73/1.11 (105) {G0,W5,D2,L3,V1,M1} I { c5_1( X ), alpha45( X ), ! alpha33 }.
% 0.73/1.11 (109) {G0,W5,D2,L2,V1,M1} I { ! alpha45( X ), ! c5_2( X, a147 ) }.
% 0.73/1.11 (112) {G0,W5,D2,L2,V1,M1} I { ! alpha55( X ), c3_2( X, a147 ) }.
% 0.73/1.11 (113) {G0,W5,D2,L2,V1,M1} I { ! alpha55( X ), ! c1_2( X, a147 ) }.
% 0.73/1.11 (195) {G0,W5,D2,L2,V1,M1} I { ! alpha49( X ), c3_2( X, a142 ) }.
% 0.73/1.11 (196) {G0,W5,D2,L2,V1,M1} I { ! alpha49( X ), ! c4_2( X, a142 ) }.
% 0.73/1.11 (199) {G0,W5,D2,L2,V1,M1} I { ! alpha38( X ), ! c1_2( X, a141 ) }.
% 0.73/1.11 (202) {G0,W5,D2,L2,V1,M1} I { ! alpha50( X ), ! c2_2( X, a141 ) }.
% 0.73/1.11 (203) {G0,W5,D2,L2,V1,M1} I { ! alpha50( X ), ! c5_2( X, a141 ) }.
% 0.73/1.11 (88) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c4_2( X, a149 ), alpha71( X
% 0.73/1.11 ), ! c5_2( X, a149 ) }.
% 0.73/1.11 (94) {G0,W4,D2,L3,V0,M1} I { c2_1( a148 ), alpha32, ! alpha44 }.
% 0.73/1.11 (130) {G0,W4,D2,L3,V0,M1} I { c5_1( a145 ), alpha24, ! alpha35 }.
% 0.73/1.11 (133) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a145 ), alpha35, ! alpha47 }.
% 0.73/1.11 (256) {G12,W4,D2,L3,V0,M1} R(137,209) { alpha63, c2_0, ! ndr1_1( a145 ) }.
% 0.73/1.11 (87) {G0,W5,D2,L2,V1,M1} I { ! alpha71( X ), c4_2( X, a149 ) }.
% 0.73/1.11 (137) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a145 ), alpha63, ! alpha56 }.
% 0.73/1.11 (163) {G0,W4,D2,L3,V0,M1} I { c4_1( a144 ), alpha18, ! alpha26 }.
% 0.73/1.11 (166) {G0,W4,D2,L3,V0,M1} I { ! c5_1( a144 ), alpha26, ! alpha37 }.
% 0.73/1.11 (170) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a144 ), alpha57, ! alpha48 }.
% 0.73/1.11 (86) {G0,W5,D2,L2,V1,M1} I { ! alpha71( X ), c5_2( X, a149 ) }.
% 0.73/1.11 (182) {G0,W4,D2,L3,V0,M1} I { alpha12, ! c1_1( a143 ), ! alpha7 }.
% 0.73/1.11 (255) {G2,W3,D2,L2,V0,M1} S(184);r(205) { alpha7, c1_1( a143 ) }.
% 0.73/1.11 (227) {G5,W4,D2,L3,V0,M1} R(30,215) { c3_0, alpha59, ! c5_1( a154 ) }.
% 0.73/1.11 (82) {G0,W6,D2,L3,V1,M1} I { ! alpha68( X ), c4_1( X ), alpha71( X ) }.
% 0.73/1.11 (231) {G5,W4,D2,L3,V0,M1} R(31,215) { c3_0, alpha59, c1_1( a154 ) }.
% 0.73/1.11 (239) {G10,W4,D2,L3,V0,M1} R(39,236) { alpha41, c2_0, c4_1( a145 ) }.
% 0.73/1.11 (238) {G4,W4,D2,L3,V0,M1} R(39,106) { alpha41, alpha33, c4_1( skol5 ) }.
% 0.73/1.11 (243) {G7,W4,D2,L3,V0,M1} R(67,229) { alpha54, c3_0, ! c4_1( a150 ) }.
% 0.73/1.11 (79) {G0,W5,D2,L3,V1,M1} I { alpha68( X ), c3_1( X ), ! alpha62 }.
% 0.73/1.11 (141) {G0,W4,D2,L2,V0,M1} I { alpha63, c2_2( a145, skol6 ) }.
% 0.73/1.11 (142) {G0,W4,D2,L2,V0,M1} I { alpha63, c5_2( a145, skol6 ) }.
% 0.73/1.11 (143) {G0,W4,D2,L2,V0,M1} I { alpha63, c1_2( a145, skol6 ) }.
% 0.73/1.11 (149) {G0,W4,D2,L2,V0,M1} I { alpha25, ! c4_2( skol7, skol10 ) }.
% 0.73/1.11 (75) {G0,W4,D2,L2,V0,M1} I { alpha70, c4_2( a150, skol3 ) }.
% 0.73/1.11 (150) {G0,W4,D2,L2,V0,M1} I { alpha25, ! c1_2( skol7, skol10 ) }.
% 0.73/1.11 (174) {G0,W4,D2,L2,V0,M1} I { alpha57, ! c3_2( a144, skol8 ) }.
% 0.73/1.11 (175) {G0,W4,D2,L2,V0,M1} I { alpha57, ! c4_2( a144, skol8 ) }.
% 0.73/1.11 (176) {G0,W4,D2,L2,V0,M1} I { alpha57, c5_2( a144, skol8 ) }.
% 0.73/1.11 (74) {G0,W4,D2,L2,V0,M1} I { alpha70, ! c5_2( a150, skol3 ) }.
% 0.73/1.11 (83) {G0,W4,D2,L2,V1,M1} I { alpha68( X ), ! alpha71( X ) }.
% 0.73/1.11 (252) {G1,W3,D2,L2,V0,M1} R(84,80) { alpha62, ! c4_1( skol4 ) }.
% 0.73/1.11 (84) {G0,W4,D2,L2,V1,M1} I { ! c4_1( X ), alpha68( X ) }.
% 0.73/1.11 (85) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha71( X ) }.
% 0.73/1.11 (72) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a150 ), c5_2( a150, X ), ! c4_2(
% 0.73/1.11 a150, X ), ! alpha70 }.
% 0.73/1.11 (250) {G1,W4,D2,L2,V1,M1} R(108,111) { ndr1_1( X ), ! alpha45( X ) }.
% 0.73/1.11 (108) {G0,W4,D2,L2,V1,M1} I { ! alpha45( X ), alpha55( X ) }.
% 0.73/1.11 (111) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha55( X ) }.
% 0.73/1.11 (249) {G1,W3,D2,L2,V0,M1} R(152,148) { alpha25, c5_1( skol7 ) }.
% 0.73/1.11 (68) {G0,W4,D2,L3,V0,M1} I { c4_1( a150 ), alpha61, ! alpha67 }.
% 0.73/1.11 (152) {G0,W4,D2,L2,V1,M1} I { c5_1( X ), alpha36( X ) }.
% 0.73/1.11 (248) {G1,W3,D2,L2,V0,M1} R(153,148) { alpha25, c3_1( skol7 ) }.
% 0.73/1.11 (153) {G0,W4,D2,L2,V1,M1} I { c3_1( X ), alpha36( X ) }.
% 0.73/1.11 (246) {G1,W3,D2,L2,V0,M1} R(154,148) { alpha25, ndr1_1( skol7 ) }.
% 0.73/1.11 (154) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha36( X ) }.
% 0.73/1.11 (192) {G0,W4,D2,L2,V1,M1} I { alpha27( X ), ! alpha38( X ) }.
% 0.73/1.11 (193) {G0,W4,D2,L2,V1,M1} I { alpha27( X ), ! alpha49( X ) }.
% 0.73/1.11 (194) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha49( X ) }.
% 0.73/1.11 (244) {G1,W4,D2,L2,V1,M1} R(198,201) { ndr1_1( X ), ! alpha38( X ) }.
% 0.73/1.11 (198) {G0,W4,D2,L2,V1,M1} I { ! alpha38( X ), alpha50( X ) }.
% 0.73/1.11 (201) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha50( X ) }.
% 0.73/1.11 (51) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a152 ), ! alpha66 }.
% 0.73/1.11 (50) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a152 ), ! alpha66 }.
% 0.73/1.11 (57) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a151 ), ! alpha42 }.
% 0.73/1.11 (58) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a151 ), ! alpha42 }.
% 0.73/1.11 (67) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a150 ), ! alpha61 }.
% 0.73/1.11 (73) {G0,W3,D2,L2,V0,M1} I { alpha70, ndr1_1( a150 ) }.
% 0.73/1.11 (48) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a152 ), alpha60, ! alpha66 }.
% 0.73/1.11 (80) {G0,W3,D2,L2,V0,M1} I { alpha62, ! alpha68( skol4 ) }.
% 0.73/1.11 (81) {G0,W3,D2,L2,V0,M1} I { alpha62, ! c3_1( skol4 ) }.
% 0.73/1.11 (242) {G7,W3,D2,L2,V0,M1} R(93,91) { alpha22, ! c2_1( a148 ) }.
% 0.73/1.11 (93) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a148 ), ! alpha32 }.
% 0.73/1.11 (47) {G0,W3,D2,L2,V0,M1} I { c3_1( a152 ), ! alpha60 }.
% 0.73/1.11 (241) {G8,W3,D2,L2,V0,M1} R(96,210) { alpha22, c5_1( a148 ) }.
% 0.73/1.11 (96) {G0,W3,D2,L2,V0,M1} I { c5_1( a148 ), ! alpha44 }.
% 0.73/1.11 (240) {G8,W3,D2,L2,V0,M1} R(97,210) { alpha22, ! c3_1( a148 ) }.
% 0.73/1.11 (97) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a148 ), ! alpha44 }.
% 0.73/1.11 (39) {G3,W5,D2,L3,V1,M1} I;r(38) { alpha41, c4_1( X ), c5_1( X ) }.
% 0.73/1.11 (106) {G0,W3,D2,L2,V0,M1} I { alpha33, ! c5_1( skol5 ) }.
% 0.73/1.11 (107) {G0,W3,D2,L2,V0,M1} I { alpha33, ! alpha45( skol5 ) }.
% 0.73/1.11 (122) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a146 ), ! alpha46 }.
% 0.73/1.11 (123) {G0,W3,D2,L2,V0,M1} I { c4_1( a146 ), ! alpha46 }.
% 0.73/1.11 (236) {G9,W3,D2,L2,V0,M1} R(129,127) { c2_0, ! c5_1( a145 ) }.
% 0.73/1.11 (129) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a145 ), ! alpha24 }.
% 0.73/1.11 (235) {G10,W3,D2,L2,V0,M1} R(132,206) { c2_0, c3_1( a145 ) }.
% 0.73/1.11 (132) {G0,W3,D2,L2,V0,M1} I { c3_1( a145 ), ! alpha35 }.
% 0.73/1.11 (35) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a153 ), ! alpha59 }.
% 0.73/1.11 (138) {G0,W3,D2,L2,V0,M1} I { alpha56, ndr1_1( a145 ) }.
% 0.73/1.11 (148) {G0,W3,D2,L2,V0,M1} I { alpha25, ! alpha36( skol7 ) }.
% 0.73/1.11 (162) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a144 ), ! alpha18 }.
% 0.73/1.11 (165) {G0,W3,D2,L2,V0,M1} I { c5_1( a144 ), ! alpha26 }.
% 0.73/1.11 (34) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a153 ), ! alpha59 }.
% 0.73/1.11 (171) {G0,W3,D2,L2,V0,M1} I { alpha48, ndr1_1( a144 ) }.
% 0.73/1.11 (189) {G0,W3,D2,L2,V0,M1} I { alpha19, ! alpha27( skol9 ) }.
% 0.73/1.11 (190) {G0,W3,D2,L2,V0,M1} I { alpha19, c1_1( skol9 ) }.
% 0.73/1.11 (233) {G13,W2,D1,L2,V0,M1} S(40);r(213) { alpha53, ! alpha41 }.
% 0.73/1.11 (43) {G0,W3,D1,L3,V0,M1} I { alpha60, c2_0, ! alpha53 }.
% 0.73/1.11 (232) {G8,W3,D1,L3,V0,M1} R(230,70) { c3_0, alpha54, alpha70 }.
% 0.73/1.11 (230) {G7,W3,D1,L3,V0,M1} R(229,66) { c3_0, alpha54, alpha67 }.
% 0.73/1.11 (31) {G0,W3,D2,L2,V0,M1} I { c1_1( a154 ), ! alpha69 }.
% 0.73/1.11 (229) {G6,W3,D1,L3,V0,M1} R(63,62) { alpha54, c3_0, alpha61 }.
% 0.73/1.11 (63) {G0,W3,D1,L3,V0,M1} I { alpha54, alpha61, ! alpha43 }.
% 0.73/1.11 (228) {G7,W2,D1,L2,V0,M1} S(71);r(218) { alpha67, ! alpha70 }.
% 0.73/1.11 (30) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a154 ), ! alpha69 }.
% 0.73/1.11 (226) {G7,W2,D1,L2,V0,M1} S(76);r(218) { alpha62, ! alpha54 }.
% 0.73/1.11 (99) {G0,W3,D1,L3,V0,M1} I { ! c5_0, ! c1_0, ! alpha22 }.
% 0.73/1.11 (225) {G7,W2,D1,L2,V0,M1} S(115);r(218) { alpha34, ! alpha23 }.
% 0.73/1.11 (28) {G0,W4,D2,L2,V0,M1} I { alpha72, c1_2( a154, skol1 ) }.
% 0.73/1.11 (118) {G0,W3,D1,L3,V0,M1} I { alpha46, c4_0, ! alpha34 }.
% 0.73/1.11 (224) {G7,W2,D1,L2,V0,M1} S(136);r(218) { alpha47, ! alpha56 }.
% 0.73/1.11 (27) {G0,W4,D2,L2,V0,M1} I { alpha72, c5_2( a154, skol1 ) }.
% 0.73/1.11 (223) {G7,W2,D1,L2,V0,M1} S(155);r(218) { ! c1_0, ! alpha17 }.
% 0.73/1.11 (222) {G7,W2,D1,L2,V0,M1} S(169);r(218) { alpha37, ! alpha48 }.
% 0.73/1.11 (26) {G0,W3,D2,L2,V0,M1} I { alpha72, ndr1_1( a154 ) }.
% 0.73/1.11 (179) {G11,W3,D1,L3,V0,M1} I;r(178) { c2_0, c1_0, c5_0 }.
% 0.73/1.11 (221) {G7,W2,D1,L2,V0,M1} S(185);r(218) { alpha19, ! alpha12 }.
% 0.73/1.11 (25) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a154 ), ! c5_2( a154, X ), ! c1_2(
% 0.73/1.11 a154, X ), ! alpha72 }.
% 0.73/1.11 (216) {G4,W3,D1,L3,V0,M1} R(214,23) { c3_0, alpha59, alpha72 }.
% 0.73/1.11 (218) {G6,W1,D1,L1,V0,M1} R(217,55);r(56) { ndr1_0 }.
% 0.73/1.11 (215) {G4,W3,D1,L3,V0,M1} R(214,22) { c3_0, alpha59, alpha69 }.
% 0.73/1.11 (24) {G0,W3,D1,L3,V0,M1} I { ! alpha69, alpha65, ! alpha72 }.
% 0.73/1.11 (214) {G3,W3,D1,L3,V0,M1} R(19,18) { alpha59, c3_0, alpha65 }.
% 0.73/1.11 (21) {G0,W2,D1,L2,V0,M1} I { alpha52, ! alpha65 }.
% 0.73/1.11 (22) {G0,W2,D1,L2,V0,M1} I { alpha69, ! alpha65 }.
% 0.73/1.11 (23) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha65 }.
% 0.73/1.11 (20) {G0,W2,D1,L2,V0,M1} I { alpha52, ! alpha59 }.
% 0.73/1.11 (41) {G0,W2,D1,L2,V0,M1} I { alpha41, ! alpha53 }.
% 0.73/1.11 (19) {G0,W3,D1,L3,V0,M1} I { alpha59, alpha65, ! alpha52 }.
% 0.73/1.11 (44) {G0,W2,D1,L2,V0,M1} I { alpha53, ! alpha60 }.
% 0.73/1.11 (45) {G0,W2,D1,L2,V0,M1} I { alpha53, ! c2_0 }.
% 0.73/1.11 (46) {G0,W2,D1,L2,V0,M1} I { alpha66, ! alpha60 }.
% 0.73/1.11 (18) {G2,W2,D1,L2,V0,M1} I;r(17) { c3_0, alpha52 }.
% 0.73/1.11 (55) {G4,W2,D1,L2,V0,M1} I;r(54) { alpha42, ! c3_0 }.
% 0.73/1.11 (62) {G5,W2,D1,L2,V0,M1} I;r(61) { c3_0, alpha43 }.
% 0.73/1.11 (64) {G0,W2,D1,L2,V0,M1} I { alpha43, ! alpha54 }.
% 0.73/1.11 (65) {G0,W2,D1,L2,V0,M1} I { alpha43, ! alpha61 }.
% 0.73/1.11 (66) {G0,W2,D1,L2,V0,M1} I { alpha67, ! alpha61 }.
% 0.73/1.11 (14) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a155 ), ! alpha64 }.
% 0.73/1.11 (70) {G0,W2,D1,L2,V0,M1} I { alpha70, ! alpha67 }.
% 0.73/1.11 (78) {G0,W2,D1,L2,V0,M1} I { alpha54, ! alpha62 }.
% 0.73/1.11 (13) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a155 ), ! alpha64 }.
% 0.73/1.11 (210) {G7,W2,D1,L2,V0,M1} R(91,92) { alpha22, alpha44 }.
% 0.73/1.11 (91) {G6,W2,D1,L2,V0,M1} I;r(90) { alpha22, alpha32 }.
% 0.73/1.11 (92) {G0,W2,D1,L2,V0,M1} I { alpha44, ! alpha32 }.
% 0.73/1.11 (100) {G0,W2,D1,L2,V0,M1} I { c5_0, alpha22 }.
% 0.73/1.11 (101) {G0,W2,D1,L2,V0,M1} I { c1_0, alpha22 }.
% 0.73/1.11 (104) {G7,W2,D1,L2,V0,M1} I;r(103) { alpha23, alpha33 }.
% 0.73/1.11 (11) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a155, a156 ), alpha58, ! alpha64 }.
% 0.73/1.11 (116) {G0,W2,D1,L2,V0,M1} I { alpha23, ! alpha34 }.
% 0.73/1.11 (119) {G0,W2,D1,L2,V0,M1} I { alpha34, ! alpha46 }.
% 0.73/1.11 (120) {G0,W2,D1,L2,V0,M1} I { alpha34, ! c4_0 }.
% 0.73/1.11 (10) {G0,W4,D2,L2,V0,M1} I { c1_2( a155, a156 ), ! alpha58 }.
% 0.73/1.11 (209) {G11,W2,D1,L2,V0,M1} R(207,135) { c2_0, alpha56 }.
% 0.73/1.11 (207) {G10,W2,D1,L2,V0,M1} R(206,131) { c2_0, alpha47 }.
% 0.73/1.11 (9) {G0,W2,D1,L2,V0,M1} I { alpha64, ! alpha58 }.
% 0.73/1.11 (206) {G9,W2,D1,L2,V0,M1} R(127,128) { c2_0, alpha35 }.
% 0.73/1.11 (127) {G8,W2,D1,L2,V0,M1} I;r(126) { c2_0, alpha24 }.
% 0.73/1.11 (128) {G0,W2,D1,L2,V0,M1} I { alpha35, ! alpha24 }.
% 0.73/1.11 (131) {G0,W2,D1,L2,V0,M1} I { alpha47, ! alpha35 }.
% 0.73/1.11 (8) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a155, a156 ), alpha51, ! alpha58 }.
% 0.73/1.11 (135) {G0,W2,D1,L2,V0,M1} I { alpha56, ! alpha47 }.
% 0.73/1.11 (139) {G0,W2,D1,L2,V0,M1} I { alpha56, ! alpha63 }.
% 0.73/1.11 (146) {G9,W2,D1,L2,V0,M1} I;r(145) { alpha17, alpha25 }.
% 0.73/1.11 (7) {G0,W4,D2,L2,V0,M1} I { c5_2( a155, a156 ), ! alpha51 }.
% 0.73/1.11 (156) {G0,W2,D1,L2,V0,M1} I { c1_0, alpha17 }.
% 0.73/1.11 (160) {G10,W2,D1,L2,V0,M1} I;r(159) { alpha18, ! c4_0 }.
% 0.73/1.11 (161) {G0,W2,D1,L2,V0,M1} I { alpha26, ! alpha18 }.
% 0.73/1.11 (6) {G0,W2,D1,L2,V0,M1} I { alpha58, ! alpha51 }.
% 0.73/1.11 (164) {G0,W2,D1,L2,V0,M1} I { alpha37, ! alpha26 }.
% 0.73/1.11 (168) {G0,W2,D1,L2,V0,M1} I { alpha48, ! alpha37 }.
% 0.73/1.11 (172) {G0,W2,D1,L2,V0,M1} I { alpha48, ! alpha57 }.
% 0.73/1.11 (5) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a155, a156 ), alpha39, ! alpha51 }.
% 0.73/1.11 (180) {G11,W2,D1,L2,V0,M1} I;r(177) { alpha7, ! c2_0 }.
% 0.73/1.11 (183) {G0,W2,D1,L2,V0,M1} I { alpha7, ! alpha12 }.
% 0.73/1.11 (4) {G0,W4,D2,L2,V0,M1} I { c2_2( a155, a156 ), ! alpha39 }.
% 0.73/1.11 (187) {G0,W2,D1,L2,V0,M1} I { alpha12, ! alpha19 }.
% 0.73/1.11 (16) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha20 }.
% 0.73/1.11 (17) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha40 }.
% 0.73/1.11 (37) {G2,W1,D1,L1,V0,M1} I;r(16) { alpha13 }.
% 0.73/1.11 (3) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha39 }.
% 0.73/1.11 (38) {G2,W1,D1,L1,V0,M1} I;r(16) { alpha29 }.
% 0.73/1.11 (53) {G3,W1,D1,L1,V0,M1} I;r(37) { alpha21 }.
% 0.73/1.11 (54) {G3,W1,D1,L1,V0,M1} I;r(37) { alpha30 }.
% 0.73/1.11 (60) {G4,W1,D1,L1,V0,M1} I;r(53) { alpha8 }.
% 0.73/1.11 (61) {G4,W1,D1,L1,V0,M1} I;r(53) { alpha31 }.
% 0.73/1.11 (89) {G5,W1,D1,L1,V0,M1} I;r(60) { alpha4 }.
% 0.73/1.11 (90) {G5,W1,D1,L1,V0,M1} I;r(60) { alpha14 }.
% 0.73/1.11 (102) {G6,W1,D1,L1,V0,M1} I;r(89) { alpha9 }.
% 0.73/1.11 (103) {G6,W1,D1,L1,V0,M1} I;r(89) { alpha15 }.
% 0.73/1.11 (125) {G7,W1,D1,L1,V0,M1} I;r(102) { alpha2 }.
% 0.73/1.11 (126) {G7,W1,D1,L1,V0,M1} I;r(102) { alpha16 }.
% 0.73/1.11 (144) {G8,W1,D1,L1,V0,M1} I;r(125) { alpha5 }.
% 0.73/1.11 (0) {G0,W1,D1,L1,V0,M1} I { alpha28 }.
% 0.73/1.11 (145) {G8,W1,D1,L1,V0,M1} I;r(125) { alpha10 }.
% 0.73/1.11 (158) {G9,W1,D1,L1,V0,M1} I;r(144) { alpha1 }.
% 0.73/1.11 (159) {G9,W1,D1,L1,V0,M1} I;r(144) { alpha11 }.
% 0.73/1.11 (177) {G10,W1,D1,L1,V0,M1} I;r(158) { alpha3 }.
% 0.73/1.11 (178) {G10,W1,D1,L1,V0,M1} I;r(158) { alpha6 }.
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 % SZS output end Saturation
% 0.73/1.11 end of saturation!
% 0.73/1.11
% 0.73/1.11 Memory use:
% 0.73/1.11
% 0.73/1.11 space for terms: 3669
% 0.73/1.11 space for clauses: 13089
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 clauses generated: 371
% 0.73/1.11 clauses kept: 284
% 0.73/1.11 clauses selected: 268
% 0.73/1.11 clauses deleted: 41
% 0.73/1.11 clauses inuse deleted: 25
% 0.73/1.11
% 0.73/1.11 subsentry: 101
% 0.73/1.11 literals s-matched: 93
% 0.73/1.11 literals matched: 93
% 0.73/1.11 full subsumption: 0
% 0.73/1.11
% 0.73/1.11 checksum: 1014296556
% 0.73/1.11
% 0.73/1.11
% 0.73/1.11 Bliksem ended
%------------------------------------------------------------------------------