%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN529+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n018.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:36 EDT 2022
% Result : CounterSatisfiable 0.72s 1.24s
% Output : Saturation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : SYN529+1 : TPTP v8.1.0. Released v2.1.0.
% 0.01/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Tue Jul 12 01:04:14 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.72/1.09 *** allocated 10000 integers for termspace/termends
% 0.72/1.09 *** allocated 10000 integers for clauses
% 0.72/1.09 *** allocated 10000 integers for justifications
% 0.72/1.09 Bliksem 1.12
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Automatic Strategy Selection
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Clauses:
% 0.72/1.09
% 0.72/1.09 { alpha73 }.
% 0.72/1.09 { alpha135 }.
% 0.72/1.09 { alpha151, c2_0, c5_0 }.
% 0.72/1.09 { ! ndr1_1( a355 ), c3_2( a355, X ), ! c1_2( a355, X ), c2_0, c5_0 }.
% 0.72/1.09 { ! c3_1( a355 ), c2_0, c5_0 }.
% 0.72/1.09 { ! alpha151, alpha166 }.
% 0.72/1.09 { ! alpha151, ! c5_2( a355, a356 ) }.
% 0.72/1.09 { ! alpha166, c5_2( a355, a356 ), alpha151 }.
% 0.72/1.09 { ! alpha166, ndr1_0 }.
% 0.72/1.09 { ! alpha166, ndr1_1( a355 ) }.
% 0.72/1.09 { ! alpha166, ! c4_2( a355, a356 ) }.
% 0.72/1.09 { ! ndr1_0, ! ndr1_1( a355 ), c4_2( a355, a356 ), alpha166 }.
% 0.72/1.09 { ! alpha135, alpha96, alpha152 }.
% 0.72/1.09 { ! alpha96, alpha135 }.
% 0.72/1.09 { ! alpha152, alpha135 }.
% 0.72/1.09 { ! alpha152, alpha115 }.
% 0.72/1.09 { ! alpha152, alpha167 }.
% 0.72/1.09 { ! alpha115, ! alpha167, alpha152 }.
% 0.72/1.09 { ! alpha167, ! ndr1_1( a353 ), alpha178 }.
% 0.72/1.09 { ndr1_1( a353 ), alpha167 }.
% 0.72/1.09 { ! alpha178, alpha167 }.
% 0.72/1.09 { ! alpha178, ! c1_2( a353, X ), ! c4_2( a353, X ), c3_2( a353, X ) }.
% 0.72/1.09 { c1_2( a353, skol1 ), alpha178 }.
% 0.72/1.09 { c4_2( a353, skol1 ), alpha178 }.
% 0.72/1.09 { ! c3_2( a353, skol1 ), alpha178 }.
% 0.72/1.09 { ! alpha115, alpha136 }.
% 0.72/1.09 { ! alpha115, c3_2( a353, a354 ) }.
% 0.72/1.09 { ! alpha136, ! c3_2( a353, a354 ), alpha115 }.
% 0.72/1.09 { ! alpha136, alpha153 }.
% 0.72/1.09 { ! alpha136, c2_2( a353, a354 ) }.
% 0.72/1.09 { ! alpha153, ! c2_2( a353, a354 ), alpha136 }.
% 0.72/1.09 { ! alpha153, alpha168 }.
% 0.72/1.09 { ! alpha153, ndr1_1( a353 ) }.
% 0.72/1.09 { ! alpha168, ! ndr1_1( a353 ), alpha153 }.
% 0.72/1.09 { ! alpha168, ndr1_0 }.
% 0.72/1.09 { ! alpha168, alpha179 }.
% 0.72/1.09 { ! ndr1_0, ! alpha179, alpha168 }.
% 0.72/1.09 { ! alpha179, ! ndr1_1( a353 ), alpha184 }.
% 0.72/1.09 { ndr1_1( a353 ), alpha179 }.
% 0.72/1.09 { ! alpha184, alpha179 }.
% 0.72/1.09 { ! alpha184, ! c2_2( a353, X ), c3_2( a353, X ), ! c5_2( a353, X ) }.
% 0.72/1.09 { c2_2( a353, skol2 ), alpha184 }.
% 0.72/1.09 { ! c3_2( a353, skol2 ), alpha184 }.
% 0.72/1.09 { c5_2( a353, skol2 ), alpha184 }.
% 0.72/1.09 { ! alpha96, alpha116, c3_0 }.
% 0.72/1.09 { ! alpha116, alpha96 }.
% 0.72/1.09 { ! c3_0, alpha96 }.
% 0.72/1.09 { ! alpha116, alpha137 }.
% 0.72/1.09 { ! alpha116, c4_1( a351 ) }.
% 0.72/1.09 { ! alpha137, ! c4_1( a351 ), alpha116 }.
% 0.72/1.09 { ! alpha137, alpha154 }.
% 0.72/1.09 { ! alpha137, ! c4_2( a351, a352 ) }.
% 0.72/1.09 { ! alpha154, c4_2( a351, a352 ), alpha137 }.
% 0.72/1.09 { ! alpha154, alpha169 }.
% 0.72/1.09 { ! alpha154, ! c1_2( a351, a352 ) }.
% 0.72/1.09 { ! alpha169, c1_2( a351, a352 ), alpha154 }.
% 0.72/1.09 { ! alpha169, alpha180 }.
% 0.72/1.09 { ! alpha169, c2_2( a351, a352 ) }.
% 0.72/1.09 { ! alpha180, ! c2_2( a351, a352 ), alpha169 }.
% 0.72/1.09 { ! alpha180, ndr1_0 }.
% 0.72/1.09 { ! alpha180, ! c1_1( a351 ) }.
% 0.72/1.09 { ! alpha180, ndr1_1( a351 ) }.
% 0.72/1.09 { ! ndr1_0, c1_1( a351 ), ! ndr1_1( a351 ), alpha180 }.
% 0.72/1.09 { ! alpha73, alpha97 }.
% 0.72/1.09 { ! alpha73, alpha117 }.
% 0.72/1.09 { ! alpha97, ! alpha117, alpha73 }.
% 0.72/1.09 { ! alpha117, c4_0, ! c1_0, ! c5_0 }.
% 0.72/1.09 { ! c4_0, alpha117 }.
% 0.72/1.09 { c1_0, alpha117 }.
% 0.72/1.09 { c5_0, alpha117 }.
% 0.72/1.09 { ! alpha97, alpha54 }.
% 0.72/1.09 { ! alpha97, alpha118 }.
% 0.72/1.09 { ! alpha54, ! alpha118, alpha97 }.
% 0.72/1.09 { ! alpha118, alpha138, alpha155 }.
% 0.72/1.09 { ! alpha138, alpha118 }.
% 0.72/1.09 { ! alpha155, alpha118 }.
% 0.72/1.09 { ! alpha155, alpha170( X ), alpha181( X ) }.
% 0.72/1.09 { ! alpha170( skol3 ), alpha155 }.
% 0.72/1.09 { ! alpha181( skol3 ), alpha155 }.
% 0.72/1.09 { ! alpha181( X ), c1_2( X, Y ), ! c4_2( X, Y ), c5_2( X, Y ) }.
% 0.72/1.09 { ! c1_2( X, skol4( X ) ), alpha181( X ) }.
% 0.72/1.09 { c4_2( X, skol4( X ) ), alpha181( X ) }.
% 0.72/1.09 { ! c5_2( X, skol4( X ) ), alpha181( X ) }.
% 0.72/1.09 { ! alpha170( X ), alpha182( X ), ! ndr1_1( X ) }.
% 0.72/1.09 { ! alpha182( X ), alpha170( X ) }.
% 0.72/1.09 { ndr1_1( X ), alpha170( X ) }.
% 0.72/1.09 { ! alpha182( X ), alpha185( X ), ! c3_1( X ) }.
% 0.72/1.09 { ! alpha185( X ), alpha182( X ) }.
% 0.72/1.09 { c3_1( X ), alpha182( X ) }.
% 0.72/1.09 { ! alpha185( X ), alpha187( X ) }.
% 0.72/1.09 { ! alpha185( X ), ! c1_2( X, a350 ) }.
% 0.72/1.09 { ! alpha187( X ), c1_2( X, a350 ), alpha185( X ) }.
% 0.72/1.09 { ! alpha187( X ), ndr1_1( X ) }.
% 0.72/1.09 { ! alpha187( X ), c2_2( X, a350 ) }.
% 0.72/1.09 { ! alpha187( X ), ! c3_2( X, a350 ) }.
% 0.72/1.09 { ! ndr1_1( X ), ! c2_2( X, a350 ), c3_2( X, a350 ), alpha187( X ) }.
% 0.72/1.09 { ! alpha138, alpha156, ! ndr1_0 }.
% 0.72/1.09 { ! alpha156, alpha138 }.
% 0.72/1.09 { ndr1_0, alpha138 }.
% 0.72/1.09 { ! alpha156, alpha171 }.
% 0.72/1.09 { ! alpha156, c2_2( a348, a349 ) }.
% 0.72/1.09 { ! alpha171, ! c2_2( a348, a349 ), alpha156 }.
% 0.72/1.09 { ! alpha171, alpha183 }.
% 0.72/1.09 { ! alpha171, ! c5_2( a348, a349 ) }.
% 0.72/1.09 { ! alpha183, c5_2( a348, a349 ), alpha171 }.
% 0.72/1.09 { ! alpha183, alpha186 }.
% 0.72/1.09 { ! alpha183, ndr1_1( a348 ) }.
% 0.72/1.09 { ! alpha186, ! ndr1_1( a348 ), alpha183 }.
% 0.72/1.09 { ! alpha186, alpha188 }.
% 0.72/1.09 { ! alpha186, alpha189 }.
% 0.72/1.09 { ! alpha188, ! alpha189, alpha186 }.
% 0.72/1.09 { ! alpha189, ! ndr1_1( a348 ), alpha190 }.
% 0.72/1.09 { ndr1_1( a348 ), alpha189 }.
% 0.72/1.09 { ! alpha190, alpha189 }.
% 0.72/1.09 { ! alpha190, c5_2( a348, X ), ! c4_2( a348, X ), ! c2_2( a348, X ) }.
% 0.72/1.09 { ! c5_2( a348, skol5 ), alpha190 }.
% 0.72/1.09 { c4_2( a348, skol5 ), alpha190 }.
% 0.72/1.09 { c2_2( a348, skol5 ), alpha190 }.
% 0.72/1.09 { ! alpha188, ndr1_0 }.
% 0.72/1.09 { ! alpha188, ! c3_1( a348 ) }.
% 0.72/1.09 { ! ndr1_0, c3_1( a348 ), alpha188 }.
% 0.72/1.09 { ! alpha54, alpha35 }.
% 0.72/1.09 { ! alpha54, alpha74 }.
% 0.72/1.09 { ! alpha35, ! alpha74, alpha54 }.
% 0.72/1.09 { ! alpha74, alpha98, alpha119 }.
% 0.72/1.09 { ! alpha98, alpha74 }.
% 0.72/1.09 { ! alpha119, alpha74 }.
% 0.72/1.09 { ! alpha119, alpha139 }.
% 0.72/1.09 { ! alpha119, c3_1( a346 ) }.
% 0.72/1.09 { ! alpha139, ! c3_1( a346 ), alpha119 }.
% 0.72/1.09 { ! alpha139, alpha157 }.
% 0.72/1.09 { ! alpha139, c1_2( a346, a347 ) }.
% 0.72/1.09 { ! alpha157, ! c1_2( a346, a347 ), alpha139 }.
% 0.72/1.09 { ! alpha157, alpha172 }.
% 0.72/1.09 { ! alpha157, ! c5_2( a346, a347 ) }.
% 0.72/1.09 { ! alpha172, c5_2( a346, a347 ), alpha157 }.
% 0.72/1.09 { ! alpha172, ndr1_0 }.
% 0.72/1.09 { ! alpha172, c4_1( a346 ) }.
% 0.72/1.09 { ! alpha172, ndr1_1( a346 ) }.
% 0.72/1.09 { ! ndr1_0, ! c4_1( a346 ), ! ndr1_1( a346 ), alpha172 }.
% 0.72/1.09 { ! alpha98, alpha120, c5_0 }.
% 0.72/1.09 { ! alpha120, alpha98 }.
% 0.72/1.09 { ! c5_0, alpha98 }.
% 0.72/1.09 { ! alpha120, alpha140 }.
% 0.72/1.09 { ! alpha120, alpha158 }.
% 0.72/1.09 { ! alpha140, ! alpha158, alpha120 }.
% 0.72/1.09 { ! alpha158, ! ndr1_1( a344 ), alpha173 }.
% 0.72/1.09 { ndr1_1( a344 ), alpha158 }.
% 0.72/1.09 { ! alpha173, alpha158 }.
% 0.72/1.09 { ! alpha173, ! c2_2( a344, X ), ! c1_2( a344, X ), ! c5_2( a344, X ) }.
% 0.72/1.09 { c2_2( a344, skol6 ), alpha173 }.
% 0.72/1.09 { c1_2( a344, skol6 ), alpha173 }.
% 0.72/1.09 { c5_2( a344, skol6 ), alpha173 }.
% 0.72/1.09 { ! alpha140, alpha159 }.
% 0.72/1.09 { ! alpha140, ! c2_1( a344 ) }.
% 0.72/1.09 { ! alpha159, c2_1( a344 ), alpha140 }.
% 0.72/1.09 { ! alpha159, alpha174 }.
% 0.72/1.09 { ! alpha159, ! c1_2( a344, a345 ) }.
% 0.72/1.09 { ! alpha174, c1_2( a344, a345 ), alpha159 }.
% 0.72/1.09 { ! alpha174, ndr1_0 }.
% 0.72/1.09 { ! alpha174, ndr1_1( a344 ) }.
% 0.72/1.09 { ! alpha174, c3_2( a344, a345 ) }.
% 0.72/1.09 { ! ndr1_0, ! ndr1_1( a344 ), ! c3_2( a344, a345 ), alpha174 }.
% 0.72/1.09 { ! alpha35, alpha55 }.
% 0.72/1.09 { ! alpha35, alpha75 }.
% 0.72/1.09 { ! alpha55, ! alpha75, alpha35 }.
% 0.72/1.09 { ! alpha75, alpha99, c3_0 }.
% 0.72/1.09 { ! alpha99, alpha75 }.
% 0.72/1.09 { ! c3_0, alpha75 }.
% 0.72/1.09 { ! alpha99, ndr1_0 }.
% 0.72/1.09 { ! alpha99, ! c1_1( a343 ) }.
% 0.72/1.09 { ! alpha99, c2_1( a343 ) }.
% 0.72/1.09 { ! ndr1_0, c1_1( a343 ), ! c2_1( a343 ), alpha99 }.
% 0.72/1.09 { ! alpha55, alpha23 }.
% 0.72/1.09 { ! alpha55, alpha76 }.
% 0.72/1.09 { ! alpha23, ! alpha76, alpha55 }.
% 0.72/1.09 { ! alpha76, alpha100, c5_0 }.
% 0.72/1.09 { ! alpha100, alpha76 }.
% 0.72/1.09 { ! c5_0, alpha76 }.
% 0.72/1.09 { ! alpha100, ! ndr1_0, alpha121 }.
% 0.72/1.09 { ndr1_0, alpha100 }.
% 0.72/1.09 { ! alpha121, alpha100 }.
% 0.72/1.09 { ! alpha121, alpha141( X ), ! c2_1( X ) }.
% 0.72/1.09 { ! alpha141( skol7 ), alpha121 }.
% 0.72/1.09 { c2_1( skol7 ), alpha121 }.
% 0.72/1.09 { ! alpha141( X ), alpha160( X ), c3_1( X ) }.
% 0.72/1.09 { ! alpha160( X ), alpha141( X ) }.
% 0.72/1.09 { ! c3_1( X ), alpha141( X ) }.
% 0.72/1.09 { ! alpha160( X ), ! ndr1_1( X ), alpha175( X ) }.
% 0.72/1.09 { ndr1_1( X ), alpha160( X ) }.
% 0.72/1.09 { ! alpha175( X ), alpha160( X ) }.
% 0.72/1.09 { ! alpha175( X ), c4_2( X, Y ), c3_2( X, Y ), c2_2( X, Y ) }.
% 0.72/1.09 { ! c4_2( X, skol8( X ) ), alpha175( X ) }.
% 0.72/1.09 { ! c3_2( X, skol8( X ) ), alpha175( X ) }.
% 0.72/1.09 { ! c2_2( X, skol8( X ) ), alpha175( X ) }.
% 0.72/1.09 { ! alpha23, alpha36 }.
% 0.72/1.09 { ! alpha23, alpha56 }.
% 0.72/1.09 { ! alpha36, ! alpha56, alpha23 }.
% 0.72/1.09 { ! alpha56, ! c3_0, ! c5_0, c4_0 }.
% 0.72/1.09 { c3_0, alpha56 }.
% 0.72/1.09 { c5_0, alpha56 }.
% 0.72/1.09 { ! c4_0, alpha56 }.
% 0.72/1.09 { ! alpha36, alpha14 }.
% 0.72/1.09 { ! alpha36, alpha57 }.
% 0.72/1.09 { ! alpha14, ! alpha57, alpha36 }.
% 0.72/1.09 { ! alpha57, alpha77, alpha101 }.
% 0.72/1.09 { ! alpha77, alpha57 }.
% 0.72/1.09 { ! alpha101, alpha57 }.
% 0.72/1.09 { ! alpha101, alpha122( X ), c5_1( X ) }.
% 0.72/1.09 { ! alpha122( skol9 ), alpha101 }.
% 0.72/1.09 { ! c5_1( skol9 ), alpha101 }.
% 0.72/1.09 { ! alpha122( X ), alpha142( X ), ! c4_1( X ) }.
% 0.72/1.09 { ! alpha142( X ), alpha122( X ) }.
% 0.72/1.09 { c4_1( X ), alpha122( X ) }.
% 0.72/1.09 { ! alpha142( X ), ndr1_1( X ) }.
% 0.72/1.09 { ! alpha142( X ), c5_2( X, a342 ) }.
% 0.72/1.09 { ! alpha142( X ), c2_2( X, a342 ) }.
% 0.72/1.09 { ! ndr1_1( X ), ! c5_2( X, a342 ), ! c2_2( X, a342 ), alpha142( X ) }.
% 0.72/1.09 { ! alpha77, c4_0, ! ndr1_0 }.
% 0.72/1.09 { ! c4_0, alpha77 }.
% 0.72/1.09 { ndr1_0, alpha77 }.
% 0.72/1.09 { ! alpha14, alpha24 }.
% 0.72/1.09 { ! alpha14, alpha37 }.
% 0.72/1.09 { ! alpha24, ! alpha37, alpha14 }.
% 0.72/1.09 { ! alpha37, c3_0, c5_0, ! c1_0 }.
% 0.72/1.09 { ! c3_0, alpha37 }.
% 0.72/1.09 { ! c5_0, alpha37 }.
% 0.72/1.09 { c1_0, alpha37 }.
% 0.72/1.09 { ! alpha24, alpha8 }.
% 0.72/1.09 { ! alpha24, alpha38 }.
% 0.72/1.09 { ! alpha8, ! alpha38, alpha24 }.
% 0.72/1.09 { ! alpha38, alpha58, alpha78 }.
% 0.72/1.09 { ! alpha58, alpha38 }.
% 0.72/1.09 { ! alpha78, alpha38 }.
% 0.72/1.09 { ! alpha78, alpha102( X ), alpha123( X ) }.
% 0.72/1.09 { ! alpha102( skol10 ), alpha78 }.
% 0.72/1.09 { ! alpha123( skol10 ), alpha78 }.
% 0.72/1.09 { ! alpha123( X ), alpha143( X ) }.
% 0.72/1.09 { ! alpha123( X ), c3_2( X, a341 ) }.
% 0.72/1.09 { ! alpha143( X ), ! c3_2( X, a341 ), alpha123( X ) }.
% 0.72/1.09 { ! alpha143( X ), ndr1_1( X ) }.
% 0.72/1.09 { ! alpha143( X ), c2_2( X, a341 ) }.
% 0.72/1.09 { ! alpha143( X ), c4_2( X, a341 ) }.
% 0.72/1.09 { ! ndr1_1( X ), ! c2_2( X, a341 ), ! c4_2( X, a341 ), alpha143( X ) }.
% 0.72/1.09 { ! alpha102( X ), alpha124( X ), alpha144( X ) }.
% 0.72/1.09 { ! alpha124( X ), alpha102( X ) }.
% 0.72/1.09 { ! alpha144( X ), alpha102( X ) }.
% 0.72/1.09 { ! alpha144( X ), alpha161( X ) }.
% 0.72/1.09 { ! alpha144( X ), c2_2( X, a340 ) }.
% 0.72/1.09 { ! alpha161( X ), ! c2_2( X, a340 ), alpha144( X ) }.
% 0.72/1.09 { ! alpha161( X ), ndr1_1( X ) }.
% 0.72/1.09 { ! alpha161( X ), ! c4_2( X, a340 ) }.
% 0.72/1.09 { ! alpha161( X ), ! c1_2( X, a340 ) }.
% 0.72/1.09 { ! ndr1_1( X ), c4_2( X, a340 ), c1_2( X, a340 ), alpha161( X ) }.
% 0.72/1.09 { ! alpha124( X ), ! ndr1_1( X ), alpha145( X ) }.
% 0.72/1.09 { ndr1_1( X ), alpha124( X ) }.
% 0.72/1.09 { ! alpha145( X ), alpha124( X ) }.
% 0.72/1.09 { ! alpha145( X ), ! c3_2( X, Y ), c2_2( X, Y ), c1_2( X, Y ) }.
% 0.72/1.09 { c3_2( X, skol11( X ) ), alpha145( X ) }.
% 0.72/1.09 { ! c2_2( X, skol11( X ) ), alpha145( X ) }.
% 0.72/1.09 { ! c1_2( X, skol11( X ) ), alpha145( X ) }.
% 0.72/1.09 { ! alpha58, alpha79, ! ndr1_0 }.
% 0.72/1.09 { ! alpha79, alpha58 }.
% 0.72/1.09 { ndr1_0, alpha58 }.
% 0.72/1.09 { ! alpha79, ! c5_0, alpha103 }.
% 0.72/1.09 { c5_0, alpha79 }.
% 0.72/1.09 { ! alpha103, alpha79 }.
% 0.72/1.09 { ! alpha103, alpha125 }.
% 0.72/1.09 { ! alpha103, ! c4_2( a338, a339 ) }.
% 0.72/1.09 { ! alpha125, c4_2( a338, a339 ), alpha103 }.
% 0.72/1.09 { ! alpha125, alpha146 }.
% 0.72/1.09 { ! alpha125, ! c3_2( a338, a339 ) }.
% 0.72/1.09 { ! alpha146, c3_2( a338, a339 ), alpha125 }.
% 0.72/1.09 { ! alpha146, alpha162 }.
% 0.72/1.09 { ! alpha146, c1_2( a338, a339 ) }.
% 0.72/1.09 { ! alpha162, ! c1_2( a338, a339 ), alpha146 }.
% 0.72/1.09 { ! alpha162, alpha176 }.
% 0.72/1.09 { ! alpha162, ndr1_1( a338 ) }.
% 0.72/1.09 { ! alpha176, ! ndr1_1( a338 ), alpha162 }.
% 0.72/1.09 { ! alpha176, ndr1_0 }.
% 0.72/1.09 { ! alpha176, c1_1( a338 ) }.
% 0.72/1.09 { ! alpha176, c4_1( a338 ) }.
% 0.72/1.09 { ! ndr1_0, ! c1_1( a338 ), ! c4_1( a338 ), alpha176 }.
% 0.72/1.09 { ! alpha8, alpha15 }.
% 0.72/1.09 { ! alpha8, alpha25 }.
% 0.72/1.09 { ! alpha15, ! alpha25, alpha8 }.
% 0.72/1.09 { ! alpha25, alpha39, c5_0 }.
% 0.72/1.09 { ! alpha39, alpha25 }.
% 0.72/1.09 { ! c5_0, alpha25 }.
% 0.72/1.09 { ! alpha39, alpha59, c4_0 }.
% 0.72/1.09 { ! alpha59, alpha39 }.
% 0.72/1.09 { ! c4_0, alpha39 }.
% 0.72/1.09 { ! alpha59, alpha80 }.
% 0.72/1.09 { ! alpha59, ! c3_2( a335, a337 ) }.
% 0.72/1.09 { ! alpha80, c3_2( a335, a337 ), alpha59 }.
% 0.72/1.09 { ! alpha80, alpha104 }.
% 0.72/1.09 { ! alpha80, c5_2( a335, a337 ) }.
% 0.72/1.09 { ! alpha104, ! c5_2( a335, a337 ), alpha80 }.
% 0.72/1.09 { ! alpha104, alpha126 }.
% 0.72/1.09 { ! alpha104, c1_2( a335, a337 ) }.
% 0.72/1.09 { ! alpha126, ! c1_2( a335, a337 ), alpha104 }.
% 0.72/1.09 { ! alpha126, alpha147 }.
% 0.72/1.09 { ! alpha126, ndr1_1( a335 ) }.
% 0.72/1.09 { ! alpha147, ! ndr1_1( a335 ), alpha126 }.
% 0.72/1.09 { ! alpha147, alpha163 }.
% 0.72/1.09 { ! alpha147, c2_2( a335, a336 ) }.
% 0.72/1.09 { ! alpha163, ! c2_2( a335, a336 ), alpha147 }.
% 0.72/1.09 { ! alpha163, alpha177 }.
% 0.72/1.09 { ! alpha163, c5_2( a335, a336 ) }.
% 0.72/1.09 { ! alpha177, ! c5_2( a335, a336 ), alpha163 }.
% 0.72/1.09 { ! alpha177, ndr1_0 }.
% 0.72/1.09 { ! alpha177, ndr1_1( a335 ) }.
% 0.72/1.09 { ! alpha177, c4_2( a335, a336 ) }.
% 0.72/1.09 { ! ndr1_0, ! ndr1_1( a335 ), ! c4_2( a335, a336 ), alpha177 }.
% 0.72/1.09 { ! alpha15, alpha26 }.
% 0.72/1.09 { ! alpha15, alpha40 }.
% 0.72/1.09 { ! alpha26, ! alpha40, alpha15 }.
% 0.72/1.09 { ! alpha40, alpha60, c1_0 }.
% 0.72/1.09 { ! alpha60, alpha40 }.
% 0.72/1.09 { ! c1_0, alpha40 }.
% 0.72/1.09 { ! alpha60, ! ndr1_0, alpha81 }.
% 0.72/1.09 { ndr1_0, alpha60 }.
% 0.72/1.09 { ! alpha81, alpha60 }.
% 0.72/1.09 { ! alpha81, alpha105( X ), c5_1( X ) }.
% 0.72/1.09 { ! alpha105( skol12 ), alpha81 }.
% 0.72/1.09 { ! c5_1( skol12 ), alpha81 }.
% 0.72/1.09 { ! alpha105( X ), c3_1( X ), alpha127( X ) }.
% 0.72/1.09 { ! c3_1( X ), alpha105( X ) }.
% 0.72/1.09 { ! alpha127( X ), alpha105( X ) }.
% 0.72/1.09 { ! alpha127( X ), ndr1_1( X ) }.
% 0.72/1.09 { ! alpha127( X ), c4_2( X, a334 ) }.
% 0.72/1.09 { ! alpha127( X ), c2_2( X, a334 ) }.
% 0.72/1.09 { ! ndr1_1( X ), ! c4_2( X, a334 ), ! c2_2( X, a334 ), alpha127( X ) }.
% 0.72/1.09 { ! alpha26, alpha4 }.
% 0.72/1.09 { ! alpha26, alpha41 }.
% 0.72/1.09 { ! alpha4, ! alpha41, alpha26 }.
% 0.72/1.09 { ! alpha41, alpha61, ndr1_0 }.
% 0.72/1.09 { ! alpha41, alpha61, ! c3_1( a333 ) }.
% 0.72/1.09 { ! alpha61, alpha41 }.
% 0.72/1.09 { ! ndr1_0, c3_1( a333 ), alpha41 }.
% 0.72/1.09 { ! alpha61, ! c4_0, alpha82 }.
% 0.72/1.09 { c4_0, alpha61 }.
% 0.72/1.09 { ! alpha82, alpha61 }.
% 0.72/1.09 { ! alpha82, alpha106 }.
% 0.72/1.09 { ! alpha82, c3_1( a331 ) }.
% 0.72/1.09 { ! alpha106, ! c3_1( a331 ), alpha82 }.
% 0.72/1.09 { ! alpha106, alpha128 }.
% 0.72/1.09 { ! alpha106, c5_1( a331 ) }.
% 0.72/1.09 { ! alpha128, ! c5_1( a331 ), alpha106 }.
% 0.72/1.09 { ! alpha128, alpha148 }.
% 0.72/1.09 { ! alpha128, ! c5_2( a331, a332 ) }.
% 0.72/1.09 { ! alpha148, c5_2( a331, a332 ), alpha128 }.
% 0.72/1.09 { ! alpha148, alpha164 }.
% 0.72/1.09 { ! alpha148, c2_2( a331, a332 ) }.
% 0.72/1.09 { ! alpha164, ! c2_2( a331, a332 ), alpha148 }.
% 0.72/1.09 { ! alpha164, ndr1_0 }.
% 0.72/1.09 { ! alpha164, ndr1_1( a331 ) }.
% 0.72/1.09 { ! alpha164, c1_2( a331, a332 ) }.
% 0.72/1.09 { ! ndr1_0, ! ndr1_1( a331 ), ! c1_2( a331, a332 ), alpha164 }.
% 0.72/1.09 { ! alpha4, alpha9 }.
% 0.72/1.09 { ! alpha4, alpha16 }.
% 0.72/1.09 { ! alpha9, ! alpha16, alpha4 }.
% 0.72/1.09 { ! alpha16, alpha27, alpha42 }.
% 0.72/1.09 { ! alpha27, alpha16 }.
% 0.72/1.09 { ! alpha42, alpha16 }.
% 0.72/1.09 { ! alpha42, alpha62 }.
% 0.72/1.09 { ! alpha42, c1_1( a329 ) }.
% 0.72/1.09 { ! alpha62, ! c1_1( a329 ), alpha42 }.
% 0.72/1.09 { ! alpha62, alpha83 }.
% 0.72/1.09 { ! alpha62, alpha107 }.
% 0.72/1.09 { ! alpha83, ! alpha107, alpha62 }.
% 0.72/1.09 { ! alpha107, ! ndr1_1( a329 ), alpha129 }.
% 0.72/1.09 { ndr1_1( a329 ), alpha107 }.
% 0.72/1.09 { ! alpha129, alpha107 }.
% 0.72/1.09 { ! alpha129, ! c4_2( a329, X ), ! c5_2( a329, X ), c1_2( a329, X ) }.
% 0.72/1.09 { c4_2( a329, skol13 ), alpha129 }.
% 0.72/1.09 { c5_2( a329, skol13 ), alpha129 }.
% 0.72/1.09 { ! c1_2( a329, skol13 ), alpha129 }.
% 0.72/1.09 { ! alpha83, ndr1_0 }.
% 0.72/1.09 { ! alpha83, ndr1_1( a329 ) }.
% 0.72/1.09 { ! alpha83, ! c2_2( a329, a330 ) }.
% 0.72/1.09 { ! ndr1_0, ! ndr1_1( a329 ), c2_2( a329, a330 ), alpha83 }.
% 0.72/1.09 { ! alpha27, alpha43, c4_0 }.
% 0.72/1.09 { ! alpha43, alpha27 }.
% 0.72/1.09 { ! c4_0, alpha27 }.
% 0.72/1.09 { ! alpha43, ndr1_0 }.
% 0.72/1.09 { ! alpha43, ! c2_1( a328 ) }.
% 0.72/1.09 { ! alpha43, c5_1( a328 ) }.
% 0.72/1.09 { ! ndr1_0, c2_1( a328 ), ! c5_1( a328 ), alpha43 }.
% 0.72/1.09 { ! alpha9, alpha2 }.
% 0.72/1.09 { ! alpha9, alpha17 }.
% 0.72/1.09 { ! alpha2, ! alpha17, alpha9 }.
% 0.72/1.09 { ! alpha17, alpha28, alpha44 }.
% 0.72/1.09 { ! alpha28, alpha17 }.
% 0.72/1.09 { ! alpha44, alpha17 }.
% 0.72/1.09 { ! alpha44, alpha63 }.
% 0.72/1.09 { ! alpha44, c3_2( a326, a327 ) }.
% 0.72/1.09 { ! alpha63, ! c3_2( a326, a327 ), alpha44 }.
% 0.72/1.09 { ! alpha63, alpha84 }.
% 0.72/1.09 { ! alpha63, ! c5_2( a326, a327 ) }.
% 0.72/1.09 { ! alpha84, c5_2( a326, a327 ), alpha63 }.
% 0.72/1.09 { ! alpha84, alpha108 }.
% 0.72/1.09 { ! alpha84, ! c2_2( a326, a327 ) }.
% 0.72/1.09 { ! alpha108, c2_2( a326, a327 ), alpha84 }.
% 0.72/1.09 { ! alpha108, alpha130 }.
% 0.72/1.09 { ! alpha108, ndr1_1( a326 ) }.
% 0.72/1.09 { ! alpha130, ! ndr1_1( a326 ), alpha108 }.
% 0.72/1.09 { ! alpha130, ndr1_0 }.
% 0.72/1.09 { ! alpha130, c2_1( a326 ) }.
% 0.72/1.09 { ! alpha130, c4_1( a326 ) }.
% 0.72/1.09 { ! ndr1_0, ! c2_1( a326 ), ! c4_1( a326 ), alpha130 }.
% 0.72/1.09 { ! alpha28, c5_0, alpha45 }.
% 0.72/1.09 { ! c5_0, alpha28 }.
% 0.72/1.09 { ! alpha45, alpha28 }.
% 0.72/1.09 { ! alpha45, alpha64 }.
% 0.72/1.09 { ! alpha45, alpha85 }.
% 0.72/1.09 { ! alpha64, ! alpha85, alpha45 }.
% 0.72/1.09 { ! alpha85, ! ndr1_1( a324 ), c3_2( a324, X ), c1_2( a324, X ) }.
% 0.72/1.09 { ndr1_1( a324 ), alpha85 }.
% 0.72/1.09 { ! c3_2( a324, skol14 ), alpha85 }.
% 0.72/1.09 { ! c1_2( a324, skol14 ), alpha85 }.
% 0.72/1.09 { ! alpha64, alpha86 }.
% 0.72/1.09 { ! alpha64, c5_2( a324, a325 ) }.
% 0.72/1.09 { ! alpha86, ! c5_2( a324, a325 ), alpha64 }.
% 0.72/1.09 { ! alpha86, alpha109 }.
% 0.72/1.09 { ! alpha86, c1_2( a324, a325 ) }.
% 0.72/1.09 { ! alpha109, ! c1_2( a324, a325 ), alpha86 }.
% 0.72/1.09 { ! alpha109, alpha131 }.
% 0.72/1.09 { ! alpha109, ndr1_1( a324 ) }.
% 0.72/1.09 { ! alpha131, ! ndr1_1( a324 ), alpha109 }.
% 0.72/1.09 { ! alpha131, ndr1_0 }.
% 0.72/1.09 { ! alpha131, alpha149 }.
% 0.72/1.09 { ! ndr1_0, ! alpha149, alpha131 }.
% 0.72/1.09 { ! alpha149, ! ndr1_1( a324 ), alpha165 }.
% 0.72/1.09 { ndr1_1( a324 ), alpha149 }.
% 0.72/1.09 { ! alpha165, alpha149 }.
% 0.72/1.09 { ! alpha165, c3_2( a324, X ), c2_2( a324, X ), ! c4_2( a324, X ) }.
% 0.72/1.09 { ! c3_2( a324, skol15 ), alpha165 }.
% 0.72/1.09 { ! c2_2( a324, skol15 ), alpha165 }.
% 0.72/1.09 { c4_2( a324, skol15 ), alpha165 }.
% 0.72/1.09 { ! alpha2, alpha5 }.
% 0.72/1.09 { ! alpha2, c2_0, ! c3_0 }.
% 0.72/1.09 { ! alpha5, ! c2_0, alpha2 }.
% 0.72/1.09 { ! alpha5, c3_0, alpha2 }.
% 0.72/1.09 { ! alpha5, alpha10 }.
% 0.72/1.09 { ! alpha5, alpha18 }.
% 0.72/1.09 { ! alpha10, ! alpha18, alpha5 }.
% 0.72/1.09 { ! alpha18, alpha29, alpha46 }.
% 0.72/1.09 { ! alpha29, alpha18 }.
% 0.72/1.09 { ! alpha46, alpha18 }.
% 0.72/1.09 { ! alpha46, alpha65( X ), c2_1( X ) }.
% 0.72/1.09 { ! alpha65( skol16 ), alpha46 }.
% 0.72/1.09 { ! c2_1( skol16 ), alpha46 }.
% 0.72/1.09 { ! alpha65( X ), alpha87( X ), c5_2( X, Y ), c4_2( X, Y ) }.
% 0.72/1.09 { ! alpha87( X ), alpha65( X ) }.
% 0.72/1.09 { ! c5_2( X, skol17( X ) ), alpha65( X ) }.
% 0.72/1.09 { ! c4_2( X, skol17( X ) ), alpha65( X ) }.
% 0.72/1.09 { ! alpha87( X ), c4_1( X ), ! ndr1_1( X ) }.
% 0.72/1.09 { ! c4_1( X ), alpha87( X ) }.
% 0.72/1.09 { ndr1_1( X ), alpha87( X ) }.
% 0.72/1.09 { ! alpha29, alpha47, ! ndr1_0 }.
% 0.72/1.09 { ! alpha47, alpha29 }.
% 0.72/1.09 { ndr1_0, alpha29 }.
% 0.72/1.09 { ! alpha47, alpha66, ! c2_1( X ), c4_1( X ) }.
% 0.72/1.09 { ! alpha66, alpha47 }.
% 0.72/1.09 { c2_1( skol18 ), alpha47 }.
% 0.72/1.09 { ! c4_1( skol18 ), alpha47 }.
% 0.72/1.09 { ! alpha66, alpha88, ! ndr1_0 }.
% 0.72/1.09 { ! alpha88, alpha66 }.
% 0.72/1.09 { ndr1_0, alpha66 }.
% 0.72/1.09 { ! alpha88, ! ndr1_0, c1_1( X ), c5_1( X ) }.
% 0.72/1.09 { ndr1_0, alpha88 }.
% 0.72/1.09 { ! c1_1( skol19 ), alpha88 }.
% 0.72/1.09 { ! c5_1( skol19 ), alpha88 }.
% 0.72/1.10 { ! alpha10, alpha1 }.
% 0.72/1.10 { ! alpha10, alpha19 }.
% 0.72/1.10 { ! alpha1, ! alpha19, alpha10 }.
% 0.72/1.10 { ! alpha19, alpha30, alpha48 }.
% 0.72/1.10 { ! alpha30, alpha19 }.
% 0.72/1.10 { ! alpha48, alpha19 }.
% 0.72/1.10 { ! alpha48, alpha67 }.
% 0.72/1.10 { ! alpha48, ! c1_2( a322, a323 ) }.
% 0.72/1.10 { ! alpha67, c1_2( a322, a323 ), alpha48 }.
% 0.72/1.10 { ! alpha67, alpha89 }.
% 0.72/1.10 { ! alpha67, c5_2( a322, a323 ) }.
% 0.72/1.10 { ! alpha89, ! c5_2( a322, a323 ), alpha67 }.
% 0.72/1.10 { ! alpha89, alpha110 }.
% 0.72/1.10 { ! alpha89, ! c4_2( a322, a323 ) }.
% 0.72/1.10 { ! alpha110, c4_2( a322, a323 ), alpha89 }.
% 0.72/1.10 { ! alpha110, ndr1_0 }.
% 0.72/1.10 { ! alpha110, c3_1( a322 ) }.
% 0.72/1.10 { ! alpha110, ndr1_1( a322 ) }.
% 0.72/1.10 { ! ndr1_0, ! c3_1( a322 ), ! ndr1_1( a322 ), alpha110 }.
% 0.72/1.10 { ! alpha30, alpha49, c4_0 }.
% 0.72/1.10 { ! alpha49, alpha30 }.
% 0.72/1.10 { ! c4_0, alpha30 }.
% 0.72/1.10 { ! alpha49, ! ndr1_0, alpha68 }.
% 0.72/1.10 { ndr1_0, alpha49 }.
% 0.72/1.10 { ! alpha68, alpha49 }.
% 0.72/1.10 { ! alpha68, alpha90( X ), ! c2_1( X ) }.
% 0.72/1.10 { ! alpha90( skol20 ), alpha68 }.
% 0.72/1.10 { c2_1( skol20 ), alpha68 }.
% 0.72/1.10 { ! alpha90( X ), alpha111( X ), alpha132( X ) }.
% 0.72/1.10 { ! alpha111( X ), alpha90( X ) }.
% 0.72/1.10 { ! alpha132( X ), alpha90( X ) }.
% 0.72/1.10 { ! alpha132( X ), alpha150( X ) }.
% 0.72/1.10 { ! alpha132( X ), ! c2_2( X, a321 ) }.
% 0.72/1.10 { ! alpha150( X ), c2_2( X, a321 ), alpha132( X ) }.
% 0.72/1.10 { ! alpha150( X ), ndr1_1( X ) }.
% 0.72/1.10 { ! alpha150( X ), ! c1_2( X, a321 ) }.
% 0.72/1.10 { ! alpha150( X ), c5_2( X, a321 ) }.
% 0.72/1.10 { ! ndr1_1( X ), c1_2( X, a321 ), ! c5_2( X, a321 ), alpha150( X ) }.
% 0.72/1.10 { ! alpha111( X ), ! ndr1_1( X ), alpha133( X ) }.
% 0.72/1.10 { ndr1_1( X ), alpha111( X ) }.
% 0.72/1.10 { ! alpha133( X ), alpha111( X ) }.
% 0.72/1.10 { ! alpha133( X ), ! c4_2( X, Y ), c2_2( X, Y ), ! c3_2( X, Y ) }.
% 0.72/1.10 { c4_2( X, skol21( X ) ), alpha133( X ) }.
% 0.72/1.10 { ! c2_2( X, skol21( X ) ), alpha133( X ) }.
% 0.72/1.10 { c3_2( X, skol21( X ) ), alpha133( X ) }.
% 0.72/1.10 { ! alpha1, alpha3 }.
% 0.72/1.10 { ! alpha1, alpha6 }.
% 0.72/1.10 { ! alpha3, ! alpha6, alpha1 }.
% 0.72/1.10 { ! alpha6, alpha11, ! c4_0 }.
% 0.72/1.10 { ! alpha11, alpha6 }.
% 0.72/1.10 { c4_0, alpha6 }.
% 0.72/1.10 { ! alpha11, alpha20, alpha31 }.
% 0.72/1.10 { ! alpha20, alpha11 }.
% 0.72/1.10 { ! alpha31, alpha11 }.
% 0.72/1.10 { ! alpha31, alpha50 }.
% 0.72/1.10 { ! alpha31, ! c4_2( a318, a320 ) }.
% 0.72/1.10 { ! alpha50, c4_2( a318, a320 ), alpha31 }.
% 0.72/1.10 { ! alpha50, alpha69 }.
% 0.72/1.10 { ! alpha50, c2_2( a318, a320 ) }.
% 0.72/1.10 { ! alpha69, ! c2_2( a318, a320 ), alpha50 }.
% 0.72/1.10 { ! alpha69, alpha91 }.
% 0.72/1.10 { ! alpha69, ndr1_1( a318 ) }.
% 0.72/1.10 { ! alpha91, ! ndr1_1( a318 ), alpha69 }.
% 0.72/1.10 { ! alpha91, alpha112 }.
% 0.72/1.10 { ! alpha91, c2_2( a318, a319 ) }.
% 0.72/1.10 { ! alpha112, ! c2_2( a318, a319 ), alpha91 }.
% 0.72/1.10 { ! alpha112, ndr1_0 }.
% 0.72/1.10 { ! alpha112, ndr1_1( a318 ) }.
% 0.72/1.10 { ! alpha112, c4_2( a318, a319 ) }.
% 0.72/1.10 { ! ndr1_0, ! ndr1_1( a318 ), ! c4_2( a318, a319 ), alpha112 }.
% 0.72/1.10 { ! alpha20, alpha32 }.
% 0.72/1.10 { ! alpha20, c1_1( a316 ) }.
% 0.72/1.10 { ! alpha32, ! c1_1( a316 ), alpha20 }.
% 0.72/1.10 { ! alpha32, alpha51 }.
% 0.72/1.10 { ! alpha32, c2_2( a316, a317 ) }.
% 0.72/1.10 { ! alpha51, ! c2_2( a316, a317 ), alpha32 }.
% 0.72/1.10 { ! alpha51, alpha70 }.
% 0.72/1.10 { ! alpha51, ! c4_2( a316, a317 ) }.
% 0.72/1.10 { ! alpha70, c4_2( a316, a317 ), alpha51 }.
% 0.72/1.10 { ! alpha70, alpha92 }.
% 0.72/1.10 { ! alpha70, c3_2( a316, a317 ) }.
% 0.72/1.10 { ! alpha92, ! c3_2( a316, a317 ), alpha70 }.
% 0.72/1.10 { ! alpha92, ndr1_0 }.
% 0.72/1.10 { ! alpha92, ! c4_1( a316 ) }.
% 0.72/1.10 { ! alpha92, ndr1_1( a316 ) }.
% 0.72/1.10 { ! ndr1_0, c4_1( a316 ), ! ndr1_1( a316 ), alpha92 }.
% 0.72/1.10 { ! alpha3, alpha7 }.
% 0.72/1.10 { ! alpha3, alpha12 }.
% 0.72/1.10 { ! alpha7, ! alpha12, alpha3 }.
% 0.72/1.10 { ! alpha12, alpha21, alpha33 }.
% 0.72/1.10 { ! alpha21, alpha12 }.
% 0.72/1.10 { ! alpha33, alpha12 }.
% 0.72/1.10 { ! alpha33, alpha52( X ), c5_1( X ) }.
% 0.72/1.10 { ! alpha52( skol22 ), alpha33 }.
% 0.72/1.10 { ! c5_1( skol22 ), alpha33 }.
% 0.72/1.10 { ! alpha52( X ), alpha71( X ), ! c4_1( X ) }.
% 0.72/1.10 { ! alpha71( X ), alpha52( X ) }.
% 0.72/1.10 { c4_1( X ), alpha52( X ) }.
% 0.72/1.10 { ! alpha71( X ), ! ndr1_1( X ), alpha93( X ) }.
% 0.72/1.10 { ndr1_1( X ), alpha71( X ) }.
% 0.72/1.10 { ! alpha93( X ), alpha71( X ) }.
% 0.72/1.10 { ! alpha93( X ), c4_2( X, Y ), c3_2( X, Y ), c1_2( X, Y ) }.
% 0.72/1.10 { ! c4_2( X, skol23( X ) ), alpha93( X ) }.
% 0.72/1.10 { ! c3_2( X, skol23( X ) ), alpha93( X ) }.
% 0.72/1.10 { ! c1_2( X, skol23( X ) ), alpha93( X ) }.
% 0.72/1.10 { ! alpha21, alpha34, ! ndr1_0 }.
% 0.72/1.10 { ! alpha34, alpha21 }.
% 0.72/1.10 { ndr1_0, alpha21 }.
% 0.72/1.10 { ! alpha34, c4_0, alpha53 }.
% 0.72/1.10 { ! c4_0, alpha34 }.
% 0.72/1.10 { ! alpha53, alpha34 }.
% 0.72/1.10 { ! alpha53, alpha72 }.
% 0.72/1.10 { ! alpha53, alpha94 }.
% 0.72/1.10 { ! alpha72, ! alpha94, alpha53 }.
% 0.72/1.10 { ! alpha94, ! ndr1_1( a314 ), alpha113 }.
% 0.72/1.10 { ndr1_1( a314 ), alpha94 }.
% 0.72/1.10 { ! alpha113, alpha94 }.
% 0.72/1.10 { ! alpha113, ! c1_2( a314, X ), c4_2( a314, X ), c3_2( a314, X ) }.
% 0.72/1.10 { c1_2( a314, skol24 ), alpha113 }.
% 0.72/1.10 { ! c4_2( a314, skol24 ), alpha113 }.
% 0.72/1.10 { ! c3_2( a314, skol24 ), alpha113 }.
% 0.72/1.10 { ! alpha72, alpha95 }.
% 0.72/1.10 { ! alpha72, c4_1( a314 ) }.
% 0.72/1.10 { ! alpha95, ! c4_1( a314 ), alpha72 }.
% 0.72/1.10 { ! alpha95, alpha114 }.
% 0.72/1.10 { ! alpha95, ! c1_2( a314, a315 ) }.
% 0.72/1.10 { ! alpha114, c1_2( a314, a315 ), alpha95 }.
% 0.72/1.10 { ! alpha114, alpha134 }.
% 0.72/1.10 { ! alpha114, ! c2_2( a314, a315 ) }.
% 0.72/1.10 { ! alpha134, c2_2( a314, a315 ), alpha114 }.
% 0.72/1.10 { ! alpha134, ndr1_0 }.
% 0.72/1.10 { ! alpha134, ndr1_1( a314 ) }.
% 0.72/1.10 { ! alpha134, ! c3_2( a314, a315 ) }.
% 0.72/1.10 { ! ndr1_0, ! ndr1_1( a314 ), c3_2( a314, a315 ), alpha134 }.
% 0.72/1.10 { ! alpha7, alpha13 }.
% 0.72/1.10 { ! alpha7, alpha22 }.
% 0.72/1.10 { ! alpha13, ! alpha22, alpha7 }.
% 0.72/1.10 { ! alpha22, ! c4_0, ! c3_0, ! c2_0 }.
% 0.72/1.10 { c4_0, alpha22 }.
% 0.72/1.10 { c3_0, alpha22 }.
% 0.72/1.10 { c2_0, alpha22 }.
% 0.72/1.10 { ! alpha13, c2_0, ! c5_0 }.
% 0.72/1.10 { ! c2_0, alpha13 }.
% 0.72/1.10 { c5_0, alpha13 }.
% 0.72/1.10
% 0.72/1.10 *** allocated 15000 integers for clauses
% 0.72/1.10 *** allocated 22500 integers for clauses
% 0.72/1.10 percentage equality = 0.000000, percentage horn = 0.772358
% 0.72/1.10 This a non-horn, non-equality problem
% 0.72/1.10
% 0.72/1.10
% 0.72/1.10 Options Used:
% 0.72/1.10
% 0.72/1.10 useres = 1
% 0.72/1.10 useparamod = 0
% 0.72/1.10 useeqrefl = 0
% 0.72/1.10 useeqfact = 0
% 0.72/1.10 usefactor = 1
% 0.72/1.10 usesimpsplitting = 0
% 0.72/1.10 usesimpdemod = 0
% 0.72/1.10 usesimpres = 3
% 0.72/1.10
% 0.72/1.10 resimpinuse = 1000
% 0.72/1.10 resimpclauses = 20000
% 0.72/1.10 substype = standard
% 0.72/1.10 backwardsubs = 1
% 0.72/1.10 selectoldest = 5
% 0.72/1.10
% 0.72/1.10 litorderings [0] = split
% 0.72/1.10 litorderings [1] = liftord
% 0.72/1.10
% 0.72/1.10 termordering = none
% 0.72/1.10
% 0.72/1.10 litapriori = 1
% 0.72/1.10 termapriori = 0
% 0.72/1.10 litaposteriori = 0
% 0.72/1.10 termaposteriori = 0
% 0.72/1.10 demodaposteriori = 0
% 0.72/1.10 ordereqreflfact = 0
% 0.72/1.10
% 0.72/1.10 litselect = none
% 0.72/1.10
% 0.72/1.10 maxweight = 15
% 0.72/1.10 maxdepth = 30000
% 0.72/1.10 maxlength = 115
% 0.72/1.10 maxnrvars = 195
% 0.72/1.10 excuselevel = 1
% 0.72/1.10 increasemaxweight = 1
% 0.72/1.10
% 0.72/1.10 maxselected = 10000000
% 0.72/1.10 maxnrclauses = 10000000
% 0.72/1.10
% 0.72/1.10 showgenerated = 0
% 0.72/1.10 showkept = 0
% 0.72/1.10 showselected = 0
% 0.72/1.10 showdeleted = 0
% 0.72/1.10 showresimp = 1
% 0.72/1.10 showstatus = 2000
% 0.72/1.10
% 0.72/1.10 prologoutput = 0
% 0.72/1.10 nrgoals = 5000000
% 0.72/1.10 totalproof = 1
% 0.72/1.10
% 0.72/1.10 Symbols occurring in the translation:
% 0.72/1.10
% 0.72/1.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.72/1.10 . [1, 2] (w:1, o:305, a:1, s:1, b:0),
% 0.72/1.10 ! [4, 1] (w:0, o:259, a:1, s:1, b:0),
% 0.72/1.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.10 c2_0 [35, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.72/1.10 c5_0 [36, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.72/1.10 c4_0 [37, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.72/1.10 c3_0 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.72/1.10 ndr1_0 [39, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.72/1.10 a314 [40, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.72/1.10 ndr1_1 [41, 1] (w:1, o:264, a:1, s:1, b:0),
% 0.72/1.10 a315 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.72/1.10 c3_2 [43, 2] (w:1, o:331, a:1, s:1, b:0),
% 0.72/1.10 c2_2 [44, 2] (w:1, o:330, a:1, s:1, b:0),
% 0.72/1.10 c1_2 [45, 2] (w:1, o:329, a:1, s:1, b:0),
% 0.72/1.10 c4_1 [46, 1] (w:1, o:266, a:1, s:1, b:0),
% 0.72/1.10 c4_2 [48, 2] (w:1, o:332, a:1, s:1, b:0),
% 0.72/1.10 c5_1 [51, 1] (w:1, o:267, a:1, s:1, b:0),
% 0.72/1.10 a316 [52, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.72/1.10 a317 [53, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.72/1.10 c1_1 [54, 1] (w:1, o:268, a:1, s:1, b:0),
% 0.72/1.10 a318 [55, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.72/1.10 a319 [56, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.72/1.10 a320 [57, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.72/1.10 a321 [60, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.72/1.10 c5_2 [61, 2] (w:1, o:333, a:1, s:1, b:0),
% 0.72/1.10 c2_1 [62, 1] (w:1, o:269, a:1, s:1, b:0),
% 0.72/1.10 a322 [63, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.72/1.10 c3_1 [64, 1] (w:1, o:265, a:1, s:1, b:0),
% 0.72/1.10 a323 [65, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.72/1.10 a324 [71, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.72/1.10 a325 [72, 0] (w:1, o:48, a:1, s:1, b:0),
% 0.72/1.10 a326 [74, 0] (w:1, o:49, a:1, s:1, b:0),
% 0.72/1.10 a327 [75, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.72/1.10 a328 [76, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.72/1.10 a329 [77, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.72/1.10 a330 [78, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.72/1.10 a331 [80, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.72/1.10 a332 [81, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.72/1.10 a333 [82, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.72/1.10 a334 [84, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.72/1.10 c1_0 [85, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.72/1.10 a335 [86, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.72/1.10 a336 [87, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.72/1.10 a337 [88, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.72/1.10 a338 [89, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.72/1.10 a339 [90, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.72/1.10 a340 [93, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.72/1.10 a341 [94, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.72/1.10 a342 [96, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.72/1.10 a343 [99, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.72/1.10 a344 [100, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.72/1.10 a345 [101, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.72/1.10 a346 [103, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.72/1.10 a347 [104, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.72/1.10 a348 [105, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.72/1.10 a349 [107, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.72/1.10 a350 [109, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.72/1.10 a351 [111, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.72/1.10 a352 [112, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.72/1.10 a353 [114, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.72/1.10 a354 [115, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.72/1.10 a355 [117, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.72/1.10 a356 [118, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.72/1.10 alpha1 [120, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.72/1.10 alpha2 [121, 0] (w:1, o:159, a:1, s:1, b:0),
% 0.72/1.10 alpha3 [122, 0] (w:1, o:170, a:1, s:1, b:0),
% 0.72/1.10 alpha4 [123, 0] (w:1, o:181, a:1, s:1, b:0),
% 0.72/1.10 alpha5 [124, 0] (w:1, o:192, a:1, s:1, b:0),
% 0.72/1.10 alpha6 [125, 0] (w:1, o:202, a:1, s:1, b:0),
% 0.72/1.10 alpha7 [126, 0] (w:1, o:212, a:1, s:1, b:0),
% 0.72/1.10 alpha8 [127, 0] (w:1, o:222, a:1, s:1, b:0),
% 0.72/1.10 alpha9 [128, 0] (w:1, o:232, a:1, s:1, b:0),
% 0.72/1.10 alpha10 [129, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.72/1.10 alpha11 [130, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.72/1.10 alpha12 [131, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.72/1.10 alpha13 [132, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.72/1.10 alpha14 [133, 0] (w:1, o:116, a:1, s:1, b:0),
% 0.72/1.10 alpha15 [134, 0] (w:1, o:122, a:1, s:1, b:0),
% 0.72/1.10 alpha16 [135, 0] (w:1, o:132, a:1, s:1, b:0),
% 0.72/1.10 alpha17 [136, 0] (w:1, o:141, a:1, s:1, b:0),
% 0.72/1.10 alpha18 [137, 0] (w:1, o:150, a:1, s:1, b:0),
% 0.72/1.10 alpha19 [138, 0] (w:1, o:157, a:1, s:1, b:0),
% 0.72/1.10 alpha20 [139, 0] (w:1, o:160, a:1, s:1, b:0),
% 0.72/1.10 alpha21 [140, 0] (w:1, o:161, a:1, s:1, b:0),
% 0.72/1.10 alpha22 [141, 0] (w:1, o:162, a:1, s:1, b:0),
% 0.72/1.10 alpha23 [142, 0] (w:1, o:163, a:1, s:1, b:0),
% 0.72/1.10 alpha24 [143, 0] (w:1, o:164, a:1, s:1, b:0),
% 0.72/1.10 alpha25 [144, 0] (w:1, o:165, a:1, s:1, b:0),
% 0.72/1.10 alpha26 [145, 0] (w:1, o:166, a:1, s:1, b:0),
% 0.72/1.10 alpha27 [146, 0] (w:1, o:167, a:1, s:1, b:0),
% 0.72/1.10 alpha28 [147, 0] (w:1, o:168, a:1, s:1, b:0),
% 0.72/1.10 alpha29 [148, 0] (w:1, o:169, a:1, s:1, b:0),
% 0.72/1.10 alpha30 [149, 0] (w:1, o:171, a:1, s:1, b:0),
% 0.72/1.10 alpha31 [150, 0] (w:1, o:172, a:1, s:1, b:0),
% 0.72/1.10 alpha32 [151, 0] (w:1, o:173, a:1, s:1, b:0),
% 0.72/1.10 alpha33 [152, 0] (w:1, o:174, a:1, s:1, b:0),
% 0.72/1.10 alpha34 [153, 0] (w:1, o:175, a:1, s:1, b:0),
% 0.72/1.10 alpha35 [154, 0] (w:1, o:176, a:1, s:1, b:0),
% 0.72/1.10 alpha36 [155, 0] (w:1, o:177, a:1, s:1, b:0),
% 0.72/1.10 alpha37 [156, 0] (w:1, o:178, a:1, s:1, b:0),
% 0.72/1.10 alpha38 [157, 0] (w:1, o:179, a:1, s:1, b:0),
% 0.72/1.10 alpha39 [158, 0] (w:1, o:180, a:1, s:1, b:0),
% 0.72/1.10 alpha40 [159, 0] (w:1, o:182, a:1, s:1, b:0),
% 0.72/1.10 alpha41 [160, 0] (w:1, o:183, a:1, s:1, b:0),
% 0.72/1.10 alpha42 [161, 0] (w:1, o:184, a:1, s:1, b:0),
% 0.72/1.10 alpha43 [162, 0] (w:1, o:185, a:1, s:1, b:0),
% 0.72/1.10 alpha44 [163, 0] (w:1, o:186, a:1, s:1, b:0),
% 0.72/1.10 alpha45 [164, 0] (w:1, o:187, a:1, s:1, b:0),
% 0.72/1.10 alpha46 [165, 0] (w:1, o:188, a:1, s:1, b:0),
% 0.72/1.10 alpha47 [166, 0] (w:1, o:189, a:1, s:1, b:0),
% 0.72/1.10 alpha48 [167, 0] (w:1, o:190, a:1, s:1, b:0),
% 0.72/1.10 alpha49 [168, 0] (w:1, o:191, a:1, s:1, b:0),
% 0.72/1.10 alpha50 [169, 0] (w:1, o:193, a:1, s:1, b:0),
% 0.72/1.10 alpha51 [170, 0] (w:1, o:194, a:1, s:1, b:0),
% 0.72/1.10 alpha52 [171, 1] (w:1, o:270, a:1, s:1, b:0),
% 0.72/1.10 alpha53 [172, 0] (w:1, o:195, a:1, s:1, b:0),
% 0.72/1.10 alpha54 [173, 0] (w:1, o:196, a:1, s:1, b:0),
% 0.72/1.10 alpha55 [174, 0] (w:1, o:197, a:1, s:1, b:0),
% 0.72/1.10 alpha56 [175, 0] (w:1, o:198, a:1, s:1, b:0),
% 0.72/1.10 alpha57 [176, 0] (w:1, o:199, a:1, s:1, b:0),
% 0.72/1.10 alpha58 [177, 0] (w:1, o:200, a:1, s:1, b:0),
% 0.72/1.10 alpha59 [178, 0] (w:1, o:201, a:1, s:1, b:0),
% 0.72/1.10 alpha60 [179, 0] (w:1, o:203, a:1, s:1, b:0),
% 0.72/1.10 alpha61 [180, 0] (w:1, o:204, a:1, s:1, b:0),
% 0.72/1.10 alpha62 [181, 0] (w:1, o:205, a:1, s:1, b:0),
% 0.72/1.10 alpha63 [182, 0] (w:1, o:206, a:1, s:1, b:0),
% 0.72/1.10 alpha64 [183, 0] (w:1, o:207, a:1, s:1, b:0),
% 0.72/1.10 alpha65 [184, 1] (w:1, o:271, a:1, s:1, b:0),
% 0.72/1.10 alpha66 [185, 0] (w:1, o:208, a:1, s:1, b:0),
% 0.72/1.10 alpha67 [186, 0] (w:1, o:209, a:1, s:1, b:0),
% 0.72/1.10 alpha68 [187, 0] (w:1, o:210, a:1, s:1, b:0),
% 0.72/1.10 alpha69 [188, 0] (w:1, o:211, a:1, s:1, b:0),
% 0.72/1.10 alpha70 [189, 0] (w:1, o:213, a:1, s:1, b:0),
% 0.72/1.10 alpha71 [190, 1] (w:1, o:272, a:1, s:1, b:0),
% 0.72/1.10 alpha72 [191, 0] (w:1, o:214, a:1, s:1, b:0),
% 0.72/1.10 alpha73 [192, 0] (w:1, o:215, a:1, s:1, b:0),
% 0.72/1.10 alpha74 [193, 0] (w:1, o:216, a:1, s:1, b:0),
% 0.72/1.10 alpha75 [194, 0] (w:1, o:217, a:1, s:1, b:0),
% 0.72/1.10 alpha76 [195, 0] (w:1, o:218, a:1, s:1, b:0),
% 0.72/1.10 alpha77 [196, 0] (w:1, o:219, a:1, s:1, b:0),
% 0.72/1.10 alpha78 [197, 0] (w:1, o:220, a:1, s:1, b:0),
% 0.72/1.10 alpha79 [198, 0] (w:1, o:221, a:1, s:1, b:0),
% 0.72/1.10 alpha80 [199, 0] (w:1, o:223, a:1, s:1, b:0),
% 0.72/1.10 alpha81 [200, 0] (w:1, o:224, a:1, s:1, b:0),
% 0.72/1.10 alpha82 [201, 0] (w:1, o:225, a:1, s:1, b:0),
% 0.72/1.10 alpha83 [202, 0] (w:1, o:226, a:1, s:1, b:0),
% 0.72/1.10 alpha84 [203, 0] (w:1, o:227, a:1, s:1, b:0),
% 0.72/1.10 alpha85 [204, 0] (w:1, o:228, a:1, s:1, b:0),
% 0.72/1.10 alpha86 [205, 0] (w:1, o:229, a:1, s:1, b:0),
% 0.72/1.10 alpha87 [206, 1] (w:1, o:273, a:1, s:1, b:0),
% 0.72/1.10 alpha88 [207, 0] (w:1, o:230, a:1, s:1, b:0),
% 0.72/1.10 alpha89 [208, 0] (w:1, o:231, a:1, s:1, b:0),
% 0.72/1.10 alpha90 [209, 1] (w:1, o:274, a:1, s:1, b:0),
% 0.72/1.10 alpha91 [210, 0] (w:1, o:233, a:1, s:1, b:0),
% 0.72/1.10 alpha92 [211, 0] (w:1, o:234, a:1, s:1, b:0),
% 0.72/1.10 alpha93 [212, 1] (w:1, o:275, a:1, s:1, b:0),
% 0.72/1.10 alpha94 [213, 0] (w:1, o:235, a:1, s:1, b:0),
% 0.72/1.10 alpha95 [214, 0] (w:1, o:236, a:1, s:1, b:0),
% 0.72/1.10 alpha96 [215, 0] (w:1, o:237, a:1, s:1, b:0),
% 0.72/1.10 alpha97 [216, 0] (w:1, o:238, a:1, s:1, b:0),
% 0.72/1.10 alpha98 [217, 0] (w:1, o:239, a:1, s:1, b:0),
% 0.72/1.10 alpha99 [218, 0] (w:1, o:240, a:1, s:1, b:0),
% 0.72/1.10 alpha100 [219, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.72/1.10 alpha101 [220, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.72/1.10 alpha102 [221, 1] (w:1, o:276, a:1, s:1, b:0),
% 0.72/1.10 alpha103 [222, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.72/1.10 alpha104 [223, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.72/1.10 alpha105 [224, 1] (w:1, o:277, a:1, s:1, b:0),
% 0.72/1.10 alpha106 [225, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.72/1.10 alpha107 [226, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.72/1.10 alpha108 [227, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.72/1.10 alpha109 [228, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.72/1.10 alpha110 [229, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.72/1.10 alpha111 [230, 1] (w:1, o:278, a:1, s:1, b:0),
% 0.72/1.10 alpha112 [231, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.72/1.10 alpha113 [232, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.72/1.10 alpha114 [233, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.72/1.10 alpha115 [234, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.72/1.10 alpha116 [235, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.72/1.10 alpha117 [236, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.72/1.10 alpha118 [237, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.72/1.10 alpha119 [238, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.72/1.10 alpha120 [239, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.72/1.10 alpha121 [240, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.72/1.10 alpha122 [241, 1] (w:1, o:279, a:1, s:1, b:0),
% 0.72/1.10 alpha123 [242, 1] (w:1, o:280, a:1, s:1, b:0),
% 0.72/1.10 alpha124 [243, 1] (w:1, o:281, a:1, s:1, b:0),
% 0.72/1.10 alpha125 [244, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.72/1.10 alpha126 [245, 0] (w:1, o:104, a:1, s:1, b:0),
% 0.72/1.10 alpha127 [246, 1] (w:1, o:282, a:1, s:1, b:0),
% 0.72/1.10 alpha128 [247, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.72/1.10 alpha129 [248, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.72/1.10 alpha130 [249, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.72/1.10 alpha131 [250, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.72/1.10 alpha132 [251, 1] (w:1, o:283, a:1, s:1, b:0),
% 0.72/1.10 alpha133 [252, 1] (w:1, o:284, a:1, s:1, b:0),
% 0.72/1.10 alpha134 [253, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.72/1.10 alpha135 [254, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.72/1.10 alpha136 [255, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.72/1.24 alpha137 [256, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.72/1.24 alpha138 [257, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.72/1.24 alpha139 [258, 0] (w:1, o:115, a:1, s:1, b:0),
% 0.72/1.24 alpha140 [259, 0] (w:1, o:117, a:1, s:1, b:0),
% 0.72/1.24 alpha141 [260, 1] (w:1, o:285, a:1, s:1, b:0),
% 0.72/1.24 alpha142 [261, 1] (w:1, o:286, a:1, s:1, b:0),
% 0.72/1.24 alpha143 [262, 1] (w:1, o:287, a:1, s:1, b:0),
% 0.72/1.24 alpha144 [263, 1] (w:1, o:288, a:1, s:1, b:0),
% 0.72/1.24 alpha145 [264, 1] (w:1, o:289, a:1, s:1, b:0),
% 0.72/1.24 alpha146 [265, 0] (w:1, o:118, a:1, s:1, b:0),
% 0.72/1.24 alpha147 [266, 0] (w:1, o:119, a:1, s:1, b:0),
% 0.72/1.24 alpha148 [267, 0] (w:1, o:120, a:1, s:1, b:0),
% 0.72/1.24 alpha149 [268, 0] (w:1, o:121, a:1, s:1, b:0),
% 0.72/1.24 alpha150 [269, 1] (w:1, o:290, a:1, s:1, b:0),
% 0.72/1.24 alpha151 [270, 0] (w:1, o:123, a:1, s:1, b:0),
% 0.72/1.24 alpha152 [271, 0] (w:1, o:124, a:1, s:1, b:0),
% 0.72/1.24 alpha153 [272, 0] (w:1, o:125, a:1, s:1, b:0),
% 0.72/1.24 alpha154 [273, 0] (w:1, o:126, a:1, s:1, b:0),
% 0.72/1.24 alpha155 [274, 0] (w:1, o:127, a:1, s:1, b:0),
% 0.72/1.24 alpha156 [275, 0] (w:1, o:128, a:1, s:1, b:0),
% 0.72/1.24 alpha157 [276, 0] (w:1, o:129, a:1, s:1, b:0),
% 0.72/1.24 alpha158 [277, 0] (w:1, o:130, a:1, s:1, b:0),
% 0.72/1.24 alpha159 [278, 0] (w:1, o:131, a:1, s:1, b:0),
% 0.72/1.24 alpha160 [279, 1] (w:1, o:291, a:1, s:1, b:0),
% 0.72/1.24 alpha161 [280, 1] (w:1, o:292, a:1, s:1, b:0),
% 0.72/1.24 alpha162 [281, 0] (w:1, o:133, a:1, s:1, b:0),
% 0.72/1.24 alpha163 [282, 0] (w:1, o:134, a:1, s:1, b:0),
% 0.72/1.24 alpha164 [283, 0] (w:1, o:135, a:1, s:1, b:0),
% 0.72/1.24 alpha165 [284, 0] (w:1, o:136, a:1, s:1, b:0),
% 0.72/1.24 alpha166 [285, 0] (w:1, o:137, a:1, s:1, b:0),
% 0.72/1.24 alpha167 [286, 0] (w:1, o:138, a:1, s:1, b:0),
% 0.72/1.24 alpha168 [287, 0] (w:1, o:139, a:1, s:1, b:0),
% 0.72/1.24 alpha169 [288, 0] (w:1, o:140, a:1, s:1, b:0),
% 0.72/1.24 alpha170 [289, 1] (w:1, o:293, a:1, s:1, b:0),
% 0.72/1.24 alpha171 [290, 0] (w:1, o:142, a:1, s:1, b:0),
% 0.72/1.24 alpha172 [291, 0] (w:1, o:143, a:1, s:1, b:0),
% 0.72/1.24 alpha173 [292, 0] (w:1, o:144, a:1, s:1, b:0),
% 0.72/1.24 alpha174 [293, 0] (w:1, o:145, a:1, s:1, b:0),
% 0.72/1.24 alpha175 [294, 1] (w:1, o:294, a:1, s:1, b:0),
% 0.72/1.24 alpha176 [295, 0] (w:1, o:146, a:1, s:1, b:0),
% 0.72/1.24 alpha177 [296, 0] (w:1, o:147, a:1, s:1, b:0),
% 0.72/1.24 alpha178 [297, 0] (w:1, o:148, a:1, s:1, b:0),
% 0.72/1.24 alpha179 [298, 0] (w:1, o:149, a:1, s:1, b:0),
% 0.72/1.24 alpha180 [299, 0] (w:1, o:151, a:1, s:1, b:0),
% 0.72/1.24 alpha181 [300, 1] (w:1, o:295, a:1, s:1, b:0),
% 0.72/1.24 alpha182 [301, 1] (w:1, o:296, a:1, s:1, b:0),
% 0.72/1.24 alpha183 [302, 0] (w:1, o:152, a:1, s:1, b:0),
% 0.72/1.24 alpha184 [303, 0] (w:1, o:153, a:1, s:1, b:0),
% 0.72/1.24 alpha185 [304, 1] (w:1, o:297, a:1, s:1, b:0),
% 0.72/1.24 alpha186 [305, 0] (w:1, o:154, a:1, s:1, b:0),
% 0.72/1.24 alpha187 [306, 1] (w:1, o:298, a:1, s:1, b:0),
% 0.72/1.24 alpha188 [307, 0] (w:1, o:155, a:1, s:1, b:0),
% 0.72/1.24 alpha189 [308, 0] (w:1, o:156, a:1, s:1, b:0),
% 0.72/1.24 alpha190 [309, 0] (w:1, o:158, a:1, s:1, b:0),
% 0.72/1.24 skol1 [310, 0] (w:1, o:241, a:1, s:1, b:0),
% 0.72/1.24 skol2 [311, 0] (w:1, o:250, a:1, s:1, b:0),
% 0.72/1.24 skol3 [312, 0] (w:1, o:254, a:1, s:1, b:0),
% 0.72/1.24 skol4 [313, 1] (w:1, o:299, a:1, s:1, b:0),
% 0.72/1.24 skol5 [314, 0] (w:1, o:255, a:1, s:1, b:0),
% 0.72/1.24 skol6 [315, 0] (w:1, o:256, a:1, s:1, b:0),
% 0.72/1.24 skol7 [316, 0] (w:1, o:257, a:1, s:1, b:0),
% 0.72/1.24 skol8 [317, 1] (w:1, o:300, a:1, s:1, b:0),
% 0.72/1.24 skol9 [318, 0] (w:1, o:258, a:1, s:1, b:0),
% 0.72/1.24 skol10 [319, 0] (w:1, o:242, a:1, s:1, b:0),
% 0.72/1.24 skol11 [320, 1] (w:1, o:301, a:1, s:1, b:0),
% 0.72/1.24 skol12 [321, 0] (w:1, o:243, a:1, s:1, b:0),
% 0.72/1.24 skol13 [322, 0] (w:1, o:244, a:1, s:1, b:0),
% 0.72/1.24 skol14 [323, 0] (w:1, o:245, a:1, s:1, b:0),
% 0.72/1.24 skol15 [324, 0] (w:1, o:246, a:1, s:1, b:0),
% 0.72/1.24 skol16 [325, 0] (w:1, o:247, a:1, s:1, b:0),
% 0.72/1.24 skol17 [326, 1] (w:1, o:302, a:1, s:1, b:0),
% 0.72/1.24 skol18 [327, 0] (w:1, o:248, a:1, s:1, b:0),
% 0.72/1.24 skol19 [328, 0] (w:1, o:249, a:1, s:1, b:0),
% 0.72/1.24 skol20 [329, 0] (w:1, o:251, a:1, s:1, b:0),
% 0.72/1.24 skol21 [330, 1] (w:1, o:303, a:1, s:1, b:0),
% 0.72/1.24 skol22 [331, 0] (w:1, o:252, a:1, s:1, b:0),
% 0.72/1.24 skol23 [332, 1] (w:1, o:304, a:1, s:1, b:0),
% 0.72/1.24 skol24 [333, 0] (w:1, o:253, a:1, s:1, b:0).
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24 Starting Search:
% 0.72/1.24
% 0.72/1.24 *** allocated 33750 integers for clauses
% 0.72/1.24 *** allocated 50625 integers for clauses
% 0.72/1.24 *** allocated 15000 integers for termspace/termends
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Failed to find proof!
% 0.72/1.24 maxweight = 15
% 0.72/1.24 maxnrclauses = 10000000
% 0.72/1.24 Generated: 1139
% 0.72/1.24 Kept: 833
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24 The strategy used was not complete!
% 0.72/1.24
% 0.72/1.24 Increased maxweight to 16
% 0.72/1.24
% 0.72/1.24 Starting Search:
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Failed to find proof!
% 0.72/1.24 maxweight = 16
% 0.72/1.24 maxnrclauses = 10000000
% 0.72/1.24 Generated: 1140
% 0.72/1.24 Kept: 834
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24 The strategy used was not complete!
% 0.72/1.24
% 0.72/1.24 Increased maxweight to 17
% 0.72/1.24
% 0.72/1.24 Starting Search:
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Failed to find proof!
% 0.72/1.24 maxweight = 17
% 0.72/1.24 maxnrclauses = 10000000
% 0.72/1.24 Generated: 1150
% 0.72/1.24 Kept: 839
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24 The strategy used was not complete!
% 0.72/1.24
% 0.72/1.24 Increased maxweight to 18
% 0.72/1.24
% 0.72/1.24 Starting Search:
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24 Resimplifying inuse:
% 0.72/1.24 Done
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24
% 0.72/1.24 found a saturation!
% 0.72/1.24 % SZS status CounterSatisfiable
% 0.72/1.24 % SZS output start Saturation
% 0.72/1.24
% 0.72/1.24 (840) {G24,W2,D1,L2,V0,M1} S(34);r(615) { alpha168, ! alpha179 }.
% 0.72/1.24 (839) {G24,W2,D1,L2,V0,M1} S(518);r(615) { alpha34, ! alpha21 }.
% 0.72/1.24 (838) {G24,W2,D1,L2,V0,M1} S(441);r(615) { alpha68, ! alpha49 }.
% 0.72/1.24 (837) {G24,W2,D1,L2,V0,M1} S(385);r(615) { alpha131, ! alpha149 }.
% 0.72/1.24 (836) {G25,W16,D2,L8,V0,M1} R(820,733);f { ! alpha65( a324 ), alpha87( a324
% 0.72/1.24 ), ! alpha133( a324 ), alpha150( a324 ), c1_2( a324, a321 ), c5_0,
% 0.72/1.24 alpha108, c2_2( a324, a321 ) }.
% 0.72/1.24 (820) {G2,W17,D2,L7,V1,M1} R(745,460) { ! alpha65( X ), alpha87( X ),
% 0.72/1.24 alpha150( X ), ! alpha133( X ), c1_2( X, a321 ), c2_2( X, a321 ), ! c3_2
% 0.72/1.24 ( X, a321 ) }.
% 0.72/1.24 (834) {G3,W16,D2,L7,V1,M1} R(823,225);f;f { ! ndr1_1( X ), alpha150( X ), !
% 0.72/1.24 alpha175( X ), ! alpha181( X ), c1_2( X, a321 ), ! alpha145( X ), c2_2(
% 0.72/1.24 X, a321 ) }.
% 0.72/1.24 (823) {G2,W17,D2,L7,V1,M1} R(746,173) { ! ndr1_1( X ), alpha150( X ), !
% 0.72/1.24 alpha181( X ), ! alpha175( X ), c1_2( X, a321 ), c2_2( X, a321 ), c3_2( X
% 0.72/1.24 , a321 ) }.
% 0.72/1.24 (830) {G3,W16,D2,L7,V1,M1} R(822,225);f { ! ndr1_1( X ), alpha150( X ), !
% 0.72/1.24 alpha93( X ), ! alpha181( X ), ! alpha145( X ), c1_2( X, a321 ), c2_2( X
% 0.72/1.24 , a321 ) }.
% 0.72/1.24 (816) {G9,W18,D2,L9,V0,M1} R(738,719) { ! alpha65( a353 ), alpha87( a353 )
% 0.72/1.24 , alpha142( a353 ), c3_0, alpha116, alpha168, ! c1_2( a353, a342 ), !
% 0.72/1.24 c2_2( a353, a342 ), c3_2( a353, a342 ) }.
% 0.72/1.24 (833) {G26,W15,D2,L8,V0,M1} R(817,770);f { ! alpha65( a324 ), alpha87( a324
% 0.72/1.24 ), alpha142( a324 ), ! alpha181( a324 ), c5_0, alpha108, ! alpha145(
% 0.72/1.24 a324 ), c1_2( a324, a342 ) }.
% 0.72/1.24 (813) {G2,W14,D3,L5,V1,M1} R(737,225);f { alpha65( X ), ! alpha175( X ), !
% 0.72/1.24 alpha145( X ), c1_2( X, skol17( X ) ), c2_2( X, skol17( X ) ) }.
% 0.72/1.24 (826) {G2,W14,D3,L5,V1,M1} R(758,225);f { ! alpha93( X ), alpha65( X ), !
% 0.72/1.24 alpha145( X ), c1_2( X, skol17( X ) ), c2_2( X, skol17( X ) ) }.
% 0.72/1.24 (797) {G2,W17,D2,L7,V1,M1} R(708,514);f { ! ndr1_1( X ), alpha142( X ), !
% 0.72/1.24 alpha181( X ), c1_2( X, a342 ), ! alpha93( X ), ! c2_2( X, a342 ), c3_2(
% 0.72/1.24 X, a342 ) }.
% 0.72/1.24 (832) {G13,W14,D2,L7,V0,M1} R(783,211);f;r(407) { c5_0, alpha119, ! alpha65
% 0.72/1.24 ( a344 ), alpha87( a344 ), ! c1_2( a344, a341 ), alpha143( a344 ), ! c2_2
% 0.72/1.24 ( a344, a341 ) }.
% 0.72/1.24 (831) {G13,W14,D2,L7,V0,M1} R(783,294);f;r(407) { c5_0, alpha119, ! alpha65
% 0.72/1.24 ( a344 ), alpha87( a344 ), ! c1_2( a344, a334 ), alpha127( a344 ), ! c2_2
% 0.72/1.24 ( a344, a334 ) }.
% 0.72/1.24 (806) {G9,W14,D2,L7,V1,M1} R(719,173);f { c3_0, alpha116, alpha168, ! c1_2
% 0.72/1.24 ( a353, X ), ! alpha175( a353 ), c2_2( a353, X ), c3_2( a353, X ) }.
% 0.72/1.24 (817) {G2,W14,D2,L6,V1,M1} R(738,708);f;f;r(407) { ! alpha65( X ), alpha87
% 0.72/1.24 ( X ), alpha142( X ), ! alpha181( X ), c1_2( X, a342 ), ! c2_2( X, a342 )
% 0.72/1.24 }.
% 0.72/1.24 (783) {G12,W15,D2,L7,V1,M1} R(679,401) { ! c1_2( a344, X ), c5_0, alpha119
% 0.72/1.24 , ! alpha65( a344 ), alpha87( a344 ), ! c2_2( a344, X ), c4_2( a344, X )
% 0.72/1.24 }.
% 0.72/1.24 (822) {G2,W14,D2,L6,V1,M1} R(746,514);f { ! ndr1_1( X ), alpha150( X ), !
% 0.72/1.24 alpha181( X ), ! alpha93( X ), c1_2( X, a321 ), c3_2( X, a321 ) }.
% 0.72/1.24 (809) {G26,W13,D2,L6,V0,M1} R(725,225);f { alpha177, ! ndr1_1( a335 ), !
% 0.72/1.24 alpha175( a335 ), ! alpha145( a335 ), c1_2( a335, a336 ), c2_2( a335,
% 0.72/1.24 a336 ) }.
% 0.72/1.24 (814) {G26,W13,D2,L6,V0,M1} R(757,225);f { ! alpha93( a318 ), ! ndr1_1(
% 0.72/1.24 a318 ), alpha112, ! alpha145( a318 ), c1_2( a318, a319 ), c2_2( a318,
% 0.72/1.24 a319 ) }.
% 0.72/1.24 (815) {G26,W13,D2,L6,V0,M1} R(759,225);f { ! alpha93( a335 ), ! ndr1_1(
% 0.72/1.24 a335 ), alpha177, ! alpha145( a335 ), c1_2( a335, a336 ), c2_2( a335,
% 0.72/1.24 a336 ) }.
% 0.72/1.24 (762) {G1,W15,D2,L6,V1,M1} R(514,211) { ! alpha93( X ), c1_2( X, a341 ), !
% 0.72/1.24 ndr1_1( X ), ! c2_2( X, a341 ), alpha143( X ), c3_2( X, a341 ) }.
% 0.72/1.24 (818) {G26,W13,D2,L6,V0,M1} R(754,225);f { alpha112, ! ndr1_1( a318 ), !
% 0.72/1.24 alpha175( a318 ), ! alpha145( a318 ), c1_2( a318, a319 ), c2_2( a318,
% 0.72/1.24 a319 ) }.
% 0.72/1.24 (829) {G28,W10,D3,L5,V0,M1} R(812,225);f;r(71) { c5_0, alpha108, alpha181(
% 0.72/1.24 a324 ), ! alpha145( a324 ), c2_2( a324, skol4( a324 ) ) }.
% 0.72/1.24 (812) {G27,W12,D3,L5,V0,M1} R(736,72) { c2_2( a324, skol4( a324 ) ), c5_0,
% 0.72/1.24 alpha108, alpha181( a324 ), c3_2( a324, skol4( a324 ) ) }.
% 0.72/1.24 (760) {G1,W15,D2,L6,V1,M1} R(514,294) { ! alpha93( X ), c1_2( X, a334 ), !
% 0.72/1.24 ndr1_1( X ), ! c2_2( X, a334 ), alpha127( X ), c3_2( X, a334 ) }.
% 0.72/1.24 (828) {G25,W10,D3,L5,V0,M1} R(752,733);r(71) { ! alpha133( a324 ), alpha181
% 0.72/1.24 ( a324 ), c5_0, alpha108, c2_2( a324, skol4( a324 ) ) }.
% 0.72/1.24 (752) {G1,W12,D3,L4,V1,M1} R(460,72) { ! alpha133( X ), c2_2( X, skol4( X )
% 0.72/1.24 ), alpha181( X ), ! c3_2( X, skol4( X ) ) }.
% 0.72/1.24 (758) {G1,W12,D3,L4,V1,M1} R(514,404) { ! alpha93( X ), c1_2( X, skol17( X
% 0.72/1.24 ) ), alpha65( X ), c3_2( X, skol17( X ) ) }.
% 0.72/1.24 (825) {G25,W12,D2,L6,V0,M1} R(750,733);f;r(642) { ! alpha133( a324 ), c1_2
% 0.72/1.24 ( a324, a340 ), alpha161( a324 ), c5_0, alpha108, c2_2( a324, a340 ) }.
% 0.72/1.24 (750) {G1,W15,D2,L6,V1,M1} R(460,221) { ! alpha133( X ), c2_2( X, a340 ), !
% 0.72/1.24 ndr1_1( X ), c1_2( X, a340 ), alpha161( X ), ! c3_2( X, a340 ) }.
% 0.72/1.24 (821) {G2,W11,D2,L5,V1,M1} R(746,745);f;f;r(407) { alpha150( X ), !
% 0.72/1.24 alpha181( X ), ! alpha65( X ), alpha87( X ), c1_2( X, a321 ) }.
% 0.72/1.24 (746) {G1,W12,D2,L5,V1,M1} R(456,70);f { ! ndr1_1( X ), alpha150( X ), !
% 0.72/1.24 alpha181( X ), c1_2( X, a321 ), ! c4_2( X, a321 ) }.
% 0.72/1.24 (805) {G9,W11,D2,L6,V0,M1} R(719,292) { c3_0, alpha116, alpha168, ! c1_2(
% 0.72/1.24 a353, a334 ), ! alpha127( a353 ), c3_2( a353, a334 ) }.
% 0.72/1.24 (819) {G10,W10,D2,L6,V0,M1} R(804,207);f { c3_0, alpha116, alpha168, !
% 0.72/1.24 alpha143( a353 ), alpha123( a353 ), ! c1_2( a353, a341 ) }.
% 0.72/1.24 (745) {G1,W12,D2,L5,V1,M1} R(456,401);r(407) { alpha150( X ), ! alpha65( X
% 0.72/1.24 ), alpha87( X ), c1_2( X, a321 ), c4_2( X, a321 ) }.
% 0.72/1.24 (804) {G9,W11,D2,L6,V0,M1} R(719,210) { c3_0, alpha116, alpha168, ! c1_2(
% 0.72/1.24 a353, a341 ), ! alpha143( a353 ), c3_2( a353, a341 ) }.
% 0.72/1.24 (749) {G25,W11,D2,L5,V0,M1} R(460,617) { ! alpha133( a355 ), c2_2( a355,
% 0.72/1.24 a356 ), ! ndr1_1( a355 ), alpha166, ! c3_2( a355, a356 ) }.
% 0.72/1.24 (754) {G25,W11,D2,L5,V0,M1} R(753,173) { alpha112, ! ndr1_1( a318 ), !
% 0.72/1.24 alpha175( a318 ), c2_2( a318, a319 ), c3_2( a318, a319 ) }.
% 0.72/1.24 (756) {G25,W11,D2,L5,V0,M1} R(755,225) { alpha134, ! ndr1_1( a314 ), !
% 0.72/1.24 alpha145( a314 ), c1_2( a314, a315 ), c2_2( a314, a315 ) }.
% 0.72/1.24 (738) {G1,W12,D2,L5,V1,M1} R(401,192);r(407) { ! alpha65( X ), alpha87( X )
% 0.72/1.24 , ! c2_2( X, a342 ), alpha142( X ), c4_2( X, a342 ) }.
% 0.72/1.24 (759) {G25,W11,D2,L5,V0,M1} R(514,722) { ! alpha93( a335 ), c1_2( a335,
% 0.72/1.24 a336 ), ! ndr1_1( a335 ), alpha177, c3_2( a335, a336 ) }.
% 0.72/1.24 (757) {G25,W11,D2,L5,V0,M1} R(514,753) { ! alpha93( a318 ), c1_2( a318,
% 0.72/1.24 a319 ), ! ndr1_1( a318 ), alpha112, c3_2( a318, a319 ) }.
% 0.72/1.24 (792) {G26,W11,D2,L5,V0,M1} R(703,225);f { ! alpha175( a355 ), c2_0, !
% 0.72/1.24 alpha145( a355 ), c1_2( a355, a356 ), c2_2( a355, a356 ) }.
% 0.72/1.24 (799) {G27,W11,D2,L5,V0,M1} R(798,225) { c2_0, ! alpha93( a355 ), !
% 0.72/1.24 alpha145( a355 ), c1_2( a355, a356 ), c2_2( a355, a356 ) }.
% 0.72/1.24 (737) {G1,W12,D3,L4,V1,M1} R(404,173) { alpha65( X ), ! alpha175( X ), c2_2
% 0.72/1.24 ( X, skol17( X ) ), c3_2( X, skol17( X ) ) }.
% 0.72/1.24 (811) {G27,W10,D2,L5,V1,M1} R(736,173);f;f { c2_2( a324, X ), c5_0,
% 0.72/1.24 alpha108, ! alpha175( a324 ), c3_2( a324, X ) }.
% 0.72/1.24 (736) {G26,W11,D2,L5,V1,M1} R(389,704) { c2_2( a324, X ), c3_2( a324, X ),
% 0.72/1.24 c5_0, alpha108, ! c4_2( a324, X ) }.
% 0.72/1.24 (810) {G21,W7,D2,L4,V0,M1} R(808,457);r(407) { alpha28, ! alpha65( a326 ),
% 0.72/1.24 alpha87( a326 ), ! alpha111( a326 ) }.
% 0.72/1.24 (808) {G20,W7,D2,L4,V0,M1} S(787);r(691) { alpha28, ! alpha65( a326 ),
% 0.72/1.24 alpha87( a326 ), ! alpha133( a326 ) }.
% 0.72/1.24 (725) {G25,W11,D2,L5,V0,M1} R(722,173) { alpha177, ! ndr1_1( a335 ), !
% 0.72/1.24 alpha175( a335 ), c2_2( a335, a336 ), c3_2( a335, a336 ) }.
% 0.72/1.24 (786) {G19,W10,D2,L5,V0,M1} R(739,689);f { ! alpha65( a326 ), alpha28,
% 0.72/1.24 alpha87( a326 ), ! alpha181( a326 ), c1_2( a326, a327 ) }.
% 0.72/1.24 (807) {G29,W8,D2,L5,V0,M1} R(803,447) { c5_0, alpha108, ! alpha90( a324 ),
% 0.72/1.24 alpha111( a324 ), ! alpha124( a324 ) }.
% 0.72/1.24 (803) {G28,W6,D2,L4,V0,M1} R(802,222);r(660) { c5_0, alpha108, ! alpha124(
% 0.72/1.24 a324 ), ! alpha132( a324 ) }.
% 0.72/1.24 (719) {G8,W12,D2,L6,V1,M1} R(718,19) { c3_0, alpha116, alpha168, ! c1_2(
% 0.72/1.24 a353, X ), c3_2( a353, X ), ! c4_2( a353, X ) }.
% 0.72/1.24 (802) {G27,W6,D2,L4,V0,M1} R(801,454);r(450) { c5_0, alpha108, ! alpha132(
% 0.72/1.24 a324 ), ! alpha145( a324 ) }.
% 0.72/1.24 (800) {G26,W8,D2,L5,V0,M1} R(770,217);r(220) { c5_0, alpha108, ! alpha145(
% 0.72/1.24 a324 ), alpha144( a324 ), ! alpha161( a324 ) }.
% 0.72/1.24 (770) {G25,W10,D2,L5,V1,M1} R(733,225);f { c5_0, alpha108, ! alpha145( a324
% 0.72/1.24 ), c1_2( a324, X ), c2_2( a324, X ) }.
% 0.72/1.24 (715) {G1,W10,D2,L4,V1,M1} R(225,206) { ! alpha145( X ), c1_2( X, a341 ), !
% 0.72/1.24 alpha123( X ), c2_2( X, a341 ) }.
% 0.72/1.24 (771) {G25,W9,D2,L5,V0,M1} R(733,207) { c5_0, alpha108, ! alpha143( a324 )
% 0.72/1.24 , alpha123( a324 ), c1_2( a324, a341 ) }.
% 0.72/1.24 (751) {G1,W9,D2,L4,V0,M1} R(460,331) { ! alpha133( a329 ), c2_2( a329,
% 0.72/1.24 skol13 ), alpha129, ! c3_2( a329, skol13 ) }.
% 0.72/1.24 (798) {G26,W6,D2,L3,V0,M1} S(766);r(777) { c2_0, ! alpha93( a355 ), c3_2(
% 0.72/1.24 a355, a356 ) }.
% 0.72/1.24 (708) {G1,W15,D2,L6,V1,M1} R(192,70) { ! ndr1_1( X ), alpha142( X ), !
% 0.72/1.24 alpha181( X ), c1_2( X, a342 ), ! c2_2( X, a342 ), ! c4_2( X, a342 ) }.
% 0.72/1.24 (796) {G4,W8,D2,L4,V1,M1} R(795,170);r(218) { ! alpha145( X ), alpha144( X
% 0.72/1.24 ), ! alpha160( X ), ! alpha161( X ) }.
% 0.72/1.24 (795) {G3,W8,D2,L4,V1,M1} R(794,217);f { ! alpha161( X ), ! alpha145( X ),
% 0.72/1.24 alpha144( X ), ! alpha175( X ) }.
% 0.72/1.24 (794) {G2,W9,D2,L4,V1,M1} R(707,225);f;r(220) { ! alpha161( X ), ! alpha175
% 0.72/1.24 ( X ), ! alpha145( X ), c2_2( X, a340 ) }.
% 0.72/1.24 (793) {G3,W8,D2,L4,V1,M1} R(768,217);f { ! alpha93( X ), ! alpha145( X ),
% 0.72/1.24 alpha144( X ), ! alpha161( X ) }.
% 0.72/1.24 (707) {G1,W10,D2,L4,V1,M1} R(219,173) { ! alpha161( X ), ! alpha175( X ),
% 0.72/1.24 c2_2( X, a340 ), c3_2( X, a340 ) }.
% 0.72/1.24 (768) {G2,W9,D2,L4,V1,M1} R(763,225);r(220) { ! alpha93( X ), ! alpha145( X
% 0.72/1.24 ), ! alpha161( X ), c2_2( X, a340 ) }.
% 0.72/1.24 (772) {G25,W8,D3,L4,V0,M1} R(733,175) { c5_0, alpha108, alpha175( a324 ),
% 0.72/1.24 c1_2( a324, skol8( a324 ) ) }.
% 0.72/1.24 (734) {G1,W8,D3,L3,V1,M1} R(515,173);r(516) { alpha93( X ), ! alpha175( X )
% 0.72/1.24 , c2_2( X, skol23( X ) ) }.
% 0.72/1.24 (735) {G1,W8,D3,L3,V1,M1} R(463,225);r(462) { alpha133( X ), ! alpha145( X
% 0.72/1.24 ), c1_2( X, skol21( X ) ) }.
% 0.72/1.24 (703) {G25,W9,D2,L4,V0,M1} R(173,558) { ! alpha175( a355 ), c2_2( a355,
% 0.72/1.24 a356 ), c2_0, c3_2( a355, a356 ) }.
% 0.72/1.24 (789) {G23,W8,D2,L4,V0,M1} R(701,225);f;r(682) { ! alpha175( a322 ),
% 0.72/1.24 alpha30, ! alpha145( a322 ), c2_2( a322, a323 ) }.
% 0.72/1.24 (791) {G29,W5,D2,L3,V0,M1} R(790,168) { c2_0, ! alpha93( a355 ), alpha141(
% 0.72/1.24 a355 ) }.
% 0.72/1.24 (790) {G28,W5,D2,L3,V0,M1} R(788,172) { c2_0, ! alpha93( a355 ), alpha160(
% 0.72/1.24 a355 ) }.
% 0.72/1.24 (788) {G27,W5,D2,L3,V0,M1} R(764,781);f { ! alpha93( a355 ), c2_0, alpha175
% 0.72/1.24 ( a355 ) }.
% 0.72/1.24 (701) {G22,W9,D2,L4,V0,M1} R(173,680) { ! alpha175( a322 ), c2_2( a322,
% 0.72/1.24 a323 ), alpha30, c3_2( a322, a323 ) }.
% 0.72/1.24 (764) {G1,W8,D3,L3,V1,M1} R(514,174);r(175) { ! alpha93( X ), alpha175( X )
% 0.72/1.24 , c1_2( X, skol8( X ) ) }.
% 0.72/1.24 (739) {G18,W8,D2,L4,V0,M1} R(401,688) { ! alpha65( a326 ), alpha87( a326 )
% 0.72/1.24 , alpha28, c4_2( a326, a327 ) }.
% 0.72/1.24 (767) {G23,W8,D2,L4,V0,M1} R(765,225);r(682) { alpha30, ! alpha93( a322 ),
% 0.72/1.24 ! alpha145( a322 ), c2_2( a322, a323 ) }.
% 0.72/1.24 (780) {G26,W8,D2,L4,V0,M1} R(777,207) { c2_0, ! alpha143( a355 ), alpha123
% 0.72/1.24 ( a355 ), ! c1_2( a355, a341 ) }.
% 0.72/1.24 (689) {G18,W9,D2,L4,V0,M1} R(688,70) { alpha28, ! alpha181( a326 ), c1_2(
% 0.72/1.24 a326, a327 ), ! c4_2( a326, a327 ) }.
% 0.72/1.24 (781) {G26,W7,D3,L3,V0,M1} R(777,175) { c2_0, alpha175( a355 ), ! c1_2(
% 0.72/1.24 a355, skol8( a355 ) ) }.
% 0.72/1.24 (784) {G12,W7,D2,L4,V0,M1} R(679,190);r(191) { c5_0, alpha119, ! alpha142(
% 0.72/1.24 a344 ), ! c1_2( a344, a342 ) }.
% 0.72/1.24 (785) {G27,W5,D2,L3,V0,M1} R(782,82);f { c2_0, alpha185( a355 ), ! alpha187
% 0.72/1.24 ( a355 ) }.
% 0.72/1.24 (782) {G26,W6,D2,L3,V0,M1} R(777,85) { c2_0, ! alpha187( a355 ), ! c1_2(
% 0.72/1.24 a355, a350 ) }.
% 0.72/1.24 (679) {G11,W11,D2,L5,V1,M1} R(137,676) { ! c1_2( a344, X ), ! c2_2( a344, X
% 0.72/1.24 ), c5_0, alpha119, ! c5_2( a344, X ) }.
% 0.72/1.24 (777) {G25,W7,D2,L3,V1,M1} S(552);r(557) { c2_0, ! c1_2( a355, X ), c3_2(
% 0.72/1.24 a355, X ) }.
% 0.72/1.24 (779) {G28,W6,D2,L4,V0,M1} R(778,74);r(642) { c5_0, alpha108, ! c3_1( a324
% 0.72/1.24 ), ! alpha170( a324 ) }.
% 0.72/1.24 (778) {G27,W6,D2,L4,V0,M1} R(776,77) { c5_0, alpha108, ! c3_1( a324 ), !
% 0.72/1.24 alpha182( a324 ) }.
% 0.72/1.24 (776) {G26,W4,D2,L3,V0,M1} R(773,81);r(80) { c5_0, alpha108, ! alpha185(
% 0.72/1.24 a324 ) }.
% 0.72/1.24 (773) {G25,W7,D2,L4,V0,M1} R(733,85) { c5_0, alpha108, ! alpha187( a324 ),
% 0.72/1.24 c1_2( a324, a350 ) }.
% 0.72/1.24 (775) {G27,W4,D2,L3,V0,M1} R(774,509) { c5_0, alpha108, alpha52( a324 ) }.
% 0.72/1.24 (774) {G26,W4,D2,L3,V0,M1} R(769,513) { c5_0, alpha108, alpha71( a324 ) }.
% 0.72/1.24 (769) {G25,W4,D2,L3,V0,M1} R(733,516);r(517) { c5_0, alpha108, alpha93(
% 0.72/1.24 a324 ) }.
% 0.72/1.24 (530) {G0,W10,D2,L4,V1,M1} I { ! c1_2( a314, X ), c4_2( a314, X ), c3_2(
% 0.72/1.24 a314, X ), ! alpha113 }.
% 0.72/1.24 (733) {G24,W8,D2,L4,V1,M1} R(370,594);r(642) { c1_2( a324, X ), c5_0,
% 0.72/1.24 alpha108, c3_2( a324, X ) }.
% 0.72/1.24 (761) {G7,W7,D2,L4,V0,M1} R(514,584);r(586) { ! alpha93( a351 ), c3_0,
% 0.72/1.24 alpha115, c3_2( a351, a352 ) }.
% 0.72/1.24 (763) {G1,W7,D2,L3,V1,M1} R(514,219);r(220) { ! alpha93( X ), ! alpha161( X
% 0.72/1.24 ), c3_2( X, a340 ) }.
% 0.72/1.24 (765) {G22,W6,D2,L3,V0,M1} R(514,680);r(682) { ! alpha93( a322 ), alpha30,
% 0.72/1.24 c3_2( a322, a323 ) }.
% 0.72/1.24 (514) {G0,W11,D2,L4,V2,M1} I { ! alpha93( X ), c3_2( X, Y ), c1_2( X, Y ),
% 0.72/1.24 c4_2( X, Y ) }.
% 0.72/1.24 (755) {G24,W6,D2,L3,V0,M1} S(546);r(615) { ! ndr1_1( a314 ), alpha134, c3_2
% 0.72/1.24 ( a314, a315 ) }.
% 0.72/1.24 (753) {G24,W6,D2,L3,V0,M1} S(485);r(615) { ! ndr1_1( a318 ), alpha112, !
% 0.72/1.24 c4_2( a318, a319 ) }.
% 0.72/1.24 (714) {G10,W7,D2,L4,V0,M1} R(225,686);r(683) { ! alpha145( a344 ), c5_0,
% 0.72/1.24 alpha119, c2_2( a344, a345 ) }.
% 0.72/1.24 (748) {G23,W6,D2,L4,V0,M1} R(720,421) { ndr1_1( skol19 ), c4_0, alpha88, !
% 0.72/1.24 c4_1( skol19 ) }.
% 0.72/1.24 (460) {G0,W11,D2,L4,V2,M1} I { ! alpha133( X ), c2_2( X, Y ), ! c3_2( X, Y
% 0.72/1.24 ), ! c4_2( X, Y ) }.
% 0.72/1.24 (747) {G23,W6,D2,L4,V0,M1} R(720,287) { ndr1_1( skol12 ), c4_0, alpha81, !
% 0.72/1.24 c4_1( skol12 ) }.
% 0.72/1.24 (720) {G22,W7,D2,L4,V1,M1} R(706,705) { ndr1_1( X ), ! c4_1( X ), c4_0,
% 0.72/1.24 c5_1( X ) }.
% 0.72/1.24 (744) {G28,W6,D2,L4,V0,M1} R(724,421) { ndr1_1( skol19 ), c1_0, alpha88,
% 0.72/1.24 c3_1( skol19 ) }.
% 0.72/1.24 (743) {G28,W6,D2,L4,V0,M1} R(724,185) { ndr1_1( skol9 ), c1_0, alpha101,
% 0.72/1.24 c3_1( skol9 ) }.
% 0.72/1.24 (456) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c1_2( X, a321 ), alpha150( X
% 0.72/1.24 ), ! c5_2( X, a321 ) }.
% 0.72/1.24 (724) {G27,W7,D2,L4,V1,M1} R(723,713) { ndr1_1( X ), c3_1( X ), c1_0, c5_1
% 0.72/1.24 ( X ) }.
% 0.72/1.24 (742) {G27,W6,D2,L4,V0,M1} R(741,712) { c2_0, c4_1( a355 ), alpha29, c2_1(
% 0.72/1.24 a355 ) }.
% 0.72/1.24 (741) {G26,W5,D2,L3,V0,M1} R(740,405);r(557) { c2_0, c4_1( a355 ), !
% 0.72/1.24 alpha65( a355 ) }.
% 0.72/1.24 (740) {G25,W5,D2,L3,V0,M1} R(401,554);r(558) { ! alpha65( a355 ), c2_0,
% 0.72/1.24 alpha87( a355 ) }.
% 0.72/1.24 (401) {G0,W10,D2,L4,V2,M1} I { ! alpha65( X ), alpha87( X ), c4_2( X, Y ),
% 0.72/1.24 c5_2( X, Y ) }.
% 0.72/1.24 (452) {G0,W7,D2,L3,V1,M1} I { ! alpha150( X ), alpha132( X ), c2_2( X, a321
% 0.72/1.24 ) }.
% 0.72/1.24 (403) {G0,W6,D3,L2,V1,M1} I { alpha65( X ), ! c5_2( X, skol17( X ) ) }.
% 0.72/1.24 (404) {G0,W6,D3,L2,V1,M1} I { alpha65( X ), ! c4_2( X, skol17( X ) ) }.
% 0.72/1.24 (461) {G0,W6,D3,L2,V1,M1} I { alpha133( X ), c4_2( X, skol21( X ) ) }.
% 0.72/1.24 (389) {G0,W10,D2,L4,V1,M1} I { c3_2( a324, X ), c2_2( a324, X ), ! c4_2(
% 0.72/1.24 a324, X ), ! alpha165 }.
% 0.72/1.24 (462) {G0,W6,D3,L2,V1,M1} I { alpha133( X ), ! c2_2( X, skol21( X ) ) }.
% 0.72/1.24 (463) {G0,W6,D3,L2,V1,M1} I { alpha133( X ), c3_2( X, skol21( X ) ) }.
% 0.72/1.24 (515) {G0,W6,D3,L2,V1,M1} I { alpha93( X ), ! c4_2( X, skol23( X ) ) }.
% 0.72/1.24 (516) {G0,W6,D3,L2,V1,M1} I { alpha93( X ), ! c3_2( X, skol23( X ) ) }.
% 0.72/1.24 (370) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a324 ), c3_2( a324, X ), c1_2( a324
% 0.72/1.24 , X ), ! alpha85 }.
% 0.72/1.24 (517) {G0,W6,D3,L2,V1,M1} I { alpha93( X ), ! c1_2( X, skol23( X ) ) }.
% 0.72/1.24 (732) {G24,W5,D2,L3,V0,M1} S(437);r(615) { ! ndr1_1( a322 ), alpha110, !
% 0.72/1.24 c3_1( a322 ) }.
% 0.72/1.24 (731) {G24,W5,D2,L3,V0,M1} S(363);r(615) { ! c4_1( a326 ), alpha130, ! c2_1
% 0.72/1.24 ( a326 ) }.
% 0.72/1.24 (730) {G24,W5,D2,L3,V0,M1} S(501);r(615) { ! ndr1_1( a316 ), alpha92, c4_1
% 0.72/1.24 ( a316 ) }.
% 0.72/1.24 (729) {G24,W5,D2,L3,V0,M1} S(344);r(615) { ! c5_1( a328 ), alpha43, c2_1(
% 0.72/1.24 a328 ) }.
% 0.72/1.24 (728) {G24,W6,D2,L3,V0,M1} S(337);r(615) { ! ndr1_1( a329 ), alpha83, c2_2
% 0.72/1.24 ( a329, a330 ) }.
% 0.72/1.24 (411) {G0,W6,D2,L4,V1,M1} I { alpha66, ! c2_1( X ), c4_1( X ), ! alpha47
% 0.72/1.24 }.
% 0.72/1.24 (727) {G24,W5,D2,L3,V1,M1} S(418);r(615) { c5_1( X ), c1_1( X ), ! alpha88
% 0.72/1.24 }.
% 0.72/1.24 (711) {G25,W6,D2,L4,V1,M1} R(444,653) { ! c2_1( X ), c4_0, alpha110,
% 0.72/1.24 alpha90( X ) }.
% 0.72/1.24 (330) {G0,W10,D2,L4,V1,M1} I { ! c4_2( a329, X ), ! c5_2( a329, X ), c1_2(
% 0.72/1.24 a329, X ), ! alpha129 }.
% 0.72/1.24 (617) {G24,W6,D2,L3,V0,M1} R(615,11) { ! ndr1_1( a355 ), alpha166, c4_2(
% 0.72/1.24 a355, a356 ) }.
% 0.72/1.24 (659) {G1,W6,D2,L3,V0,M1} R(106,70);r(107) { alpha190, ! alpha181( a348 ),
% 0.72/1.24 c1_2( a348, skol5 ) }.
% 0.72/1.24 (690) {G24,W6,D2,L3,V0,M1} S(150);r(615) { ! ndr1_1( a344 ), alpha174, !
% 0.72/1.24 c3_2( a344, a345 ) }.
% 0.72/1.24 (726) {G24,W6,D2,L3,V0,M1} S(317);r(615) { ! ndr1_1( a331 ), alpha164, !
% 0.72/1.24 c1_2( a331, a332 ) }.
% 0.72/1.24 (702) {G1,W6,D2,L3,V0,M1} R(173,532);r(533) { ! alpha175( a314 ), alpha113
% 0.72/1.24 , c2_2( a314, skol24 ) }.
% 0.72/1.24 (716) {G19,W6,D2,L3,V0,M1} R(225,691);r(687) { ! alpha145( a326 ), alpha28
% 0.72/1.24 , c1_2( a326, a327 ) }.
% 0.72/1.24 (722) {G24,W6,D2,L3,V0,M1} S(278);r(615) { ! ndr1_1( a335 ), alpha177, !
% 0.72/1.24 c4_2( a335, a336 ) }.
% 0.72/1.24 (723) {G1,W6,D2,L3,V1,M1} R(288,291) { c3_1( X ), ndr1_1( X ), ! alpha105(
% 0.72/1.24 X ) }.
% 0.72/1.24 (294) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a334 ), alpha127(
% 0.72/1.24 X ), ! c4_2( X, a334 ) }.
% 0.72/1.24 (288) {G0,W6,D2,L3,V1,M1} I { c3_1( X ), ! alpha105( X ), alpha127( X ) }.
% 0.72/1.24 (405) {G0,W6,D2,L3,V1,M1} I { c4_1( X ), ! ndr1_1( X ), ! alpha87( X ) }.
% 0.72/1.24 (447) {G0,W6,D2,L3,V1,M1} I { ! alpha90( X ), alpha111( X ), alpha132( X )
% 0.72/1.24 }.
% 0.72/1.24 (457) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha111( X ), alpha133( X )
% 0.72/1.24 }.
% 0.72/1.24 (508) {G0,W6,D2,L3,V1,M1} I { ! alpha52( X ), ! c4_1( X ), alpha71( X ) }.
% 0.72/1.24 (511) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha71( X ), alpha93( X )
% 0.72/1.24 }.
% 0.72/1.24 (654) {G2,W6,D2,L3,V1,M1} R(647,77) { ndr1_1( X ), ! c3_1( X ), ! alpha182
% 0.72/1.24 ( X ) }.
% 0.72/1.24 (721) {G24,W5,D2,L3,V0,M1} S(250);r(615) { ! c4_1( a338 ), alpha176, ! c1_1
% 0.72/1.24 ( a338 ) }.
% 0.72/1.24 (706) {G1,W6,D2,L3,V1,M1} R(186,189) { ! c4_1( X ), ndr1_1( X ), ! alpha122
% 0.72/1.24 ( X ) }.
% 0.72/1.24 (718) {G7,W4,D1,L4,V0,M1} R(717,34);r(572) { c3_0, alpha116, alpha168,
% 0.72/1.24 alpha178 }.
% 0.72/1.24 (717) {G5,W4,D1,L4,V0,M1} R(577,36) { c3_0, alpha116, alpha178, alpha179
% 0.72/1.24 }.
% 0.72/1.24 (577) {G4,W5,D2,L4,V0,M1} R(575,16) { c3_0, alpha116, alpha178, ! ndr1_1(
% 0.72/1.24 a353 ) }.
% 0.72/1.24 (240) {G0,W5,D2,L3,V0,M1} I { c3_2( a338, a339 ), alpha125, ! alpha146 }.
% 0.72/1.24 (243) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a338, a339 ), alpha146, ! alpha162
% 0.72/1.24 }.
% 0.72/1.24 (259) {G0,W5,D2,L3,V0,M1} I { c3_2( a335, a337 ), alpha59, ! alpha80 }.
% 0.72/1.24 (262) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a335, a337 ), alpha80, ! alpha104 }.
% 0.72/1.24 (265) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a335, a337 ), alpha104, ! alpha126
% 0.72/1.24 }.
% 0.72/1.24 (237) {G0,W5,D2,L3,V0,M1} I { c4_2( a338, a339 ), alpha103, ! alpha125 }.
% 0.72/1.24 (271) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a335, a336 ), alpha147, ! alpha163
% 0.72/1.24 }.
% 0.72/1.24 (274) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a335, a336 ), alpha163, ! alpha177
% 0.72/1.24 }.
% 0.72/1.24 (310) {G0,W5,D2,L3,V0,M1} I { c5_2( a331, a332 ), alpha128, ! alpha148 }.
% 0.72/1.24 (313) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a331, a332 ), alpha148, ! alpha164
% 0.72/1.24 }.
% 0.72/1.24 (228) {G0,W6,D3,L2,V1,M1} I { alpha145( X ), ! c1_2( X, skol11( X ) ) }.
% 0.72/1.24 (350) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a326, a327 ), alpha44, ! alpha63 }.
% 0.72/1.24 (353) {G0,W5,D2,L3,V0,M1} I { c5_2( a326, a327 ), alpha63, ! alpha84 }.
% 0.72/1.24 (356) {G0,W5,D2,L3,V0,M1} I { c2_2( a326, a327 ), alpha84, ! alpha108 }.
% 0.72/1.24 (376) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a324, a325 ), alpha64, ! alpha86 }.
% 0.72/1.24 (227) {G0,W6,D3,L2,V1,M1} I { alpha145( X ), ! c2_2( X, skol11( X ) ) }.
% 0.72/1.24 (379) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a324, a325 ), alpha86, ! alpha109 }.
% 0.72/1.24 (427) {G0,W5,D2,L3,V0,M1} I { c1_2( a322, a323 ), alpha48, ! alpha67 }.
% 0.72/1.24 (430) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a322, a323 ), alpha67, ! alpha89 }.
% 0.72/1.24 (433) {G0,W5,D2,L3,V0,M1} I { c4_2( a322, a323 ), alpha89, ! alpha110 }.
% 0.72/1.24 (226) {G0,W6,D3,L2,V1,M1} I { alpha145( X ), c3_2( X, skol11( X ) ) }.
% 0.72/1.24 (472) {G0,W5,D2,L3,V0,M1} I { c4_2( a318, a320 ), alpha31, ! alpha50 }.
% 0.72/1.24 (475) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a318, a320 ), alpha50, ! alpha69 }.
% 0.72/1.24 (481) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a318, a319 ), alpha91, ! alpha112 }.
% 0.72/1.24 (491) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a316, a317 ), alpha32, ! alpha51 }.
% 0.72/1.24 (225) {G0,W11,D2,L4,V2,M1} I { ! alpha145( X ), c2_2( X, Y ), c1_2( X, Y )
% 0.72/1.24 , ! c3_2( X, Y ) }.
% 0.72/1.24 (494) {G0,W5,D2,L3,V0,M1} I { c4_2( a316, a317 ), alpha51, ! alpha70 }.
% 0.72/1.24 (497) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a316, a317 ), alpha70, ! alpha92 }.
% 0.72/1.24 (539) {G0,W5,D2,L3,V0,M1} I { c1_2( a314, a315 ), alpha95, ! alpha114 }.
% 0.72/1.24 (542) {G0,W5,D2,L3,V0,M1} I { c2_2( a314, a315 ), alpha114, ! alpha134 }.
% 0.72/1.24 (222) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha124( X ), alpha145( X )
% 0.72/1.24 }.
% 0.72/1.24 (584) {G5,W5,D2,L3,V0,M1} R(49,579) { c3_0, alpha115, ! c4_2( a351, a352 )
% 0.72/1.24 }.
% 0.72/1.24 (586) {G6,W5,D2,L3,V0,M1} R(52,581) { c3_0, alpha115, ! c1_2( a351, a352 )
% 0.72/1.24 }.
% 0.72/1.24 (591) {G7,W5,D2,L3,V0,M1} R(55,582) { c3_0, alpha115, c2_2( a351, a352 )
% 0.72/1.24 }.
% 0.72/1.24 (616) {G24,W5,D2,L3,V0,M1} R(615,60) { ! ndr1_1( a351 ), alpha180, c1_1(
% 0.72/1.24 a351 ) }.
% 0.72/1.24 (221) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c1_2( X, a340 ), alpha161( X
% 0.72/1.24 ), c4_2( X, a340 ) }.
% 0.72/1.24 (674) {G24,W5,D2,L3,V0,M1} S(127);r(615) { ! ndr1_1( a346 ), alpha172, !
% 0.72/1.24 c4_1( a346 ) }.
% 0.72/1.24 (683) {G8,W5,D2,L3,V0,M1} R(145,637) { c5_0, alpha119, ! c1_2( a344, a345 )
% 0.72/1.24 }.
% 0.72/1.24 (684) {G22,W5,D2,L3,V0,M1} R(378,595) { c5_0, alpha108, c1_2( a324, a325 )
% 0.72/1.24 }.
% 0.72/1.24 (685) {G21,W5,D2,L3,V0,M1} R(375,593) { c5_0, alpha108, c5_2( a324, a325 )
% 0.72/1.24 }.
% 0.72/1.24 (217) {G0,W7,D2,L3,V1,M1} I { ! alpha161( X ), alpha144( X ), ! c2_2( X,
% 0.72/1.24 a340 ) }.
% 0.72/1.24 (686) {G9,W5,D2,L3,V0,M1} R(149,638) { c5_0, alpha119, c3_2( a344, a345 )
% 0.72/1.24 }.
% 0.72/1.24 (693) {G24,W5,D2,L3,V0,M1} S(157);r(615) { c1_1( a343 ), alpha99, ! c2_1(
% 0.72/1.24 a343 ) }.
% 0.72/1.24 (695) {G19,W5,D2,L3,V0,M1} R(277,627) { c4_0, c5_0, c4_2( a335, a336 ) }.
% 0.72/1.24 (696) {G18,W5,D2,L3,V0,M1} R(273,626) { c4_0, c5_0, c5_2( a335, a336 ) }.
% 0.72/1.24 (212) {G0,W6,D2,L3,V1,M1} I { ! alpha102( X ), alpha124( X ), alpha144( X )
% 0.72/1.24 }.
% 0.72/1.24 (697) {G17,W5,D2,L3,V0,M1} R(270,625) { c4_0, c5_0, c2_2( a335, a336 ) }.
% 0.72/1.24 (698) {G15,W5,D2,L3,V0,M1} R(264,623) { c4_0, c5_0, c1_2( a335, a337 ) }.
% 0.72/1.24 (699) {G14,W5,D2,L3,V0,M1} R(261,622) { c4_0, c5_0, c5_2( a335, a337 ) }.
% 0.72/1.24 (700) {G13,W5,D2,L3,V0,M1} R(258,620) { c4_0, c5_0, ! c3_2( a335, a337 )
% 0.72/1.24 }.
% 0.72/1.24 (211) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a341 ), alpha143(
% 0.72/1.24 X ), ! c4_2( X, a341 ) }.
% 0.72/1.24 (713) {G26,W5,D2,L3,V1,M1} R(285,619) { c5_1( X ), c1_0, alpha105( X ) }.
% 0.72/1.24 (285) {G0,W5,D2,L3,V1,M1} I { alpha105( X ), c5_1( X ), ! alpha81 }.
% 0.72/1.24 (712) {G18,W5,D2,L3,V1,M1} R(398,397) { c2_1( X ), alpha29, alpha65( X )
% 0.72/1.24 }.
% 0.72/1.24 (398) {G0,W5,D2,L3,V1,M1} I { alpha65( X ), c2_1( X ), ! alpha46 }.
% 0.72/1.24 (207) {G0,W7,D2,L3,V1,M1} I { ! alpha143( X ), alpha123( X ), ! c3_2( X,
% 0.72/1.24 a341 ) }.
% 0.72/1.24 (444) {G0,W5,D2,L3,V1,M1} I { alpha90( X ), ! c2_1( X ), ! alpha68 }.
% 0.72/1.24 (710) {G21,W5,D2,L3,V1,M1} R(505,504) { c5_1( X ), alpha21, alpha52( X )
% 0.72/1.24 }.
% 0.72/1.24 (505) {G0,W5,D2,L3,V1,M1} I { alpha52( X ), c5_1( X ), ! alpha33 }.
% 0.72/1.24 (709) {G11,W5,D2,L3,V1,M1} R(202,201) { alpha102( X ), alpha58, alpha123( X
% 0.72/1.24 ) }.
% 0.72/1.24 (202) {G0,W5,D2,L3,V1,M1} I { alpha102( X ), alpha123( X ), ! alpha78 }.
% 0.72/1.24 (621) {G4,W5,D2,L3,V1,M1} R(67,66) { alpha170( X ), alpha138, alpha181( X )
% 0.72/1.24 }.
% 0.72/1.24 (694) {G26,W5,D2,L3,V1,M1} R(164,633) { ! c2_1( X ), c5_0, alpha141( X )
% 0.72/1.24 }.
% 0.72/1.24 (705) {G21,W5,D2,L3,V1,M1} R(183,630) { c5_1( X ), c4_0, alpha122( X ) }.
% 0.72/1.24 (206) {G0,W5,D2,L2,V1,M1} I { ! alpha123( X ), c3_2( X, a341 ) }.
% 0.72/1.24 (192) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a342 ), alpha142(
% 0.72/1.24 X ), ! c5_2( X, a342 ) }.
% 0.72/1.24 (209) {G0,W5,D2,L2,V1,M1} I { ! alpha143( X ), c2_2( X, a341 ) }.
% 0.72/1.24 (210) {G0,W5,D2,L2,V1,M1} I { ! alpha143( X ), c4_2( X, a341 ) }.
% 0.72/1.24 (216) {G0,W5,D2,L2,V1,M1} I { ! alpha144( X ), c2_2( X, a340 ) }.
% 0.72/1.24 (219) {G0,W5,D2,L2,V1,M1} I { ! alpha161( X ), ! c4_2( X, a340 ) }.
% 0.72/1.24 (191) {G0,W5,D2,L2,V1,M1} I { ! alpha142( X ), c2_2( X, a342 ) }.
% 0.72/1.24 (220) {G0,W5,D2,L2,V1,M1} I { ! alpha161( X ), ! c1_2( X, a340 ) }.
% 0.72/1.24 (292) {G0,W5,D2,L2,V1,M1} I { ! alpha127( X ), c4_2( X, a334 ) }.
% 0.72/1.24 (293) {G0,W5,D2,L2,V1,M1} I { ! alpha127( X ), c2_2( X, a334 ) }.
% 0.72/1.24 (451) {G0,W5,D2,L2,V1,M1} I { ! alpha132( X ), ! c2_2( X, a321 ) }.
% 0.72/1.24 (190) {G0,W5,D2,L2,V1,M1} I { ! alpha142( X ), c5_2( X, a342 ) }.
% 0.72/1.24 (454) {G0,W5,D2,L2,V1,M1} I { ! alpha150( X ), ! c1_2( X, a321 ) }.
% 0.72/1.24 (455) {G0,W5,D2,L2,V1,M1} I { ! alpha150( X ), c5_2( X, a321 ) }.
% 0.72/1.24 (246) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a338 ), alpha162, ! alpha176 }.
% 0.72/1.24 (268) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a335 ), alpha126, ! alpha147 }.
% 0.72/1.24 (186) {G0,W6,D2,L3,V1,M1} I { ! alpha122( X ), ! c4_1( X ), alpha142( X )
% 0.72/1.24 }.
% 0.72/1.24 (304) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a331 ), alpha82, ! alpha106 }.
% 0.72/1.24 (307) {G0,W4,D2,L3,V0,M1} I { ! c5_1( a331 ), alpha106, ! alpha128 }.
% 0.72/1.24 (323) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a329 ), alpha42, ! alpha62 }.
% 0.72/1.24 (327) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a329 ), alpha129, ! alpha107 }.
% 0.72/1.24 (183) {G0,W5,D2,L3,V1,M1} I { alpha122( X ), c5_1( X ), ! alpha101 }.
% 0.72/1.24 (359) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a326 ), alpha108, ! alpha130 }.
% 0.72/1.24 (382) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a324 ), alpha109, ! alpha131 }.
% 0.72/1.24 (704) {G25,W3,D1,L3,V0,M1} R(386,599);r(642) { c5_0, alpha108, alpha165 }.
% 0.72/1.24 (386) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a324 ), alpha165, ! alpha149 }.
% 0.72/1.24 (176) {G0,W6,D3,L2,V1,M1} I { alpha175( X ), ! c2_2( X, skol8( X ) ) }.
% 0.72/1.24 (478) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a318 ), alpha69, ! alpha91 }.
% 0.72/1.24 (488) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a316 ), alpha20, ! alpha32 }.
% 0.72/1.24 (527) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a314 ), alpha113, ! alpha94 }.
% 0.72/1.24 (536) {G0,W4,D2,L3,V0,M1} I { ! c4_1( a314 ), alpha72, ! alpha95 }.
% 0.72/1.24 (175) {G0,W6,D3,L2,V1,M1} I { alpha175( X ), ! c3_2( X, skol8( X ) ) }.
% 0.72/1.24 (578) {G4,W4,D2,L3,V0,M1} R(576,46) { c3_0, alpha115, c4_1( a351 ) }.
% 0.72/1.24 (602) {G8,W4,D2,L3,V0,M1} R(58,583) { c3_0, alpha115, ! c1_1( a351 ) }.
% 0.72/1.24 (606) {G8,W4,D2,L3,V0,M1} R(59,583) { c3_0, alpha115, ndr1_1( a351 ) }.
% 0.72/1.24 (642) {G23,W4,D2,L3,V0,M1} R(381,596) { c5_0, alpha108, ndr1_1( a324 ) }.
% 0.72/1.24 (174) {G0,W6,D3,L2,V1,M1} I { alpha175( X ), ! c4_2( X, skol8( X ) ) }.
% 0.72/1.24 (643) {G18,W4,D2,L3,V0,M1} R(343,603) { c4_0, alpha107, c5_1( a328 ) }.
% 0.72/1.24 (644) {G18,W4,D2,L3,V0,M1} R(342,603) { c4_0, alpha107, ! c2_1( a328 ) }.
% 0.72/1.24 (648) {G19,W4,D2,L3,V0,M1} R(276,627) { c4_0, c5_0, ndr1_1( a335 ) }.
% 0.72/1.24 (651) {G9,W4,D2,L3,V0,M1} R(148,638) { c5_0, alpha119, ndr1_1( a344 ) }.
% 0.72/1.24 (173) {G0,W11,D2,L4,V2,M1} I { ! alpha175( X ), c3_2( X, Y ), c2_2( X, Y )
% 0.72/1.24 , c4_2( X, Y ) }.
% 0.72/1.24 (652) {G7,W4,D2,L3,V0,M1} R(142,635) { c5_0, alpha119, ! c2_1( a344 ) }.
% 0.72/1.24 (236) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a338, a339 ), ! alpha103 }.
% 0.72/1.24 (239) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a338, a339 ), ! alpha125 }.
% 0.72/1.24 (242) {G0,W4,D2,L2,V0,M1} I { c1_2( a338, a339 ), ! alpha146 }.
% 0.72/1.24 (170) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha160( X ), alpha175( X )
% 0.72/1.24 }.
% 0.72/1.24 (258) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a335, a337 ), ! alpha59 }.
% 0.72/1.24 (261) {G0,W4,D2,L2,V0,M1} I { c5_2( a335, a337 ), ! alpha80 }.
% 0.72/1.24 (264) {G0,W4,D2,L2,V0,M1} I { c1_2( a335, a337 ), ! alpha104 }.
% 0.72/1.24 (270) {G0,W4,D2,L2,V0,M1} I { c2_2( a335, a336 ), ! alpha147 }.
% 0.72/1.24 (167) {G0,W6,D2,L3,V1,M1} I { ! alpha141( X ), c3_1( X ), alpha160( X ) }.
% 0.72/1.24 (273) {G0,W4,D2,L2,V0,M1} I { c5_2( a335, a336 ), ! alpha163 }.
% 0.72/1.24 (277) {G0,W4,D2,L2,V0,M1} I { c4_2( a335, a336 ), ! alpha177 }.
% 0.72/1.24 (309) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a331, a332 ), ! alpha128 }.
% 0.72/1.24 (312) {G0,W4,D2,L2,V0,M1} I { c2_2( a331, a332 ), ! alpha148 }.
% 0.72/1.24 (164) {G0,W5,D2,L3,V1,M1} I { alpha141( X ), ! c2_1( X ), ! alpha121 }.
% 0.72/1.24 (316) {G0,W4,D2,L2,V0,M1} I { c1_2( a331, a332 ), ! alpha164 }.
% 0.72/1.24 (331) {G0,W4,D2,L2,V0,M1} I { alpha129, c4_2( a329, skol13 ) }.
% 0.72/1.24 (332) {G0,W4,D2,L2,V0,M1} I { alpha129, c5_2( a329, skol13 ) }.
% 0.72/1.24 (333) {G0,W4,D2,L2,V0,M1} I { alpha129, ! c1_2( a329, skol13 ) }.
% 0.72/1.24 (692) {G17,W4,D2,L2,V0,M1} R(336,568) { alpha27, ! c2_2( a329, a330 ) }.
% 0.72/1.24 (336) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a329, a330 ), ! alpha83 }.
% 0.72/1.24 (691) {G16,W4,D2,L2,V0,M1} R(349,347) { alpha28, c3_2( a326, a327 ) }.
% 0.72/1.24 (349) {G0,W4,D2,L2,V0,M1} I { c3_2( a326, a327 ), ! alpha44 }.
% 0.72/1.24 (688) {G17,W4,D2,L2,V0,M1} R(352,564) { alpha28, ! c5_2( a326, a327 ) }.
% 0.72/1.24 (352) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a326, a327 ), ! alpha63 }.
% 0.72/1.24 (687) {G18,W4,D2,L2,V0,M1} R(355,565) { alpha28, ! c2_2( a326, a327 ) }.
% 0.72/1.24 (355) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a326, a327 ), ! alpha84 }.
% 0.72/1.24 (149) {G0,W4,D2,L2,V0,M1} I { c3_2( a344, a345 ), ! alpha174 }.
% 0.72/1.24 (372) {G0,W4,D2,L2,V0,M1} I { alpha85, ! c3_2( a324, skol14 ) }.
% 0.72/1.24 (373) {G0,W4,D2,L2,V0,M1} I { alpha85, ! c1_2( a324, skol14 ) }.
% 0.72/1.24 (375) {G0,W4,D2,L2,V0,M1} I { c5_2( a324, a325 ), ! alpha64 }.
% 0.72/1.24 (378) {G0,W4,D2,L2,V0,M1} I { c1_2( a324, a325 ), ! alpha86 }.
% 0.72/1.24 (146) {G0,W5,D2,L3,V0,M1} I { c1_2( a344, a345 ), alpha159, ! alpha174 }.
% 0.72/1.24 (390) {G0,W4,D2,L2,V0,M1} I { alpha165, ! c3_2( a324, skol15 ) }.
% 0.72/1.24 (391) {G0,W4,D2,L2,V0,M1} I { alpha165, ! c2_2( a324, skol15 ) }.
% 0.72/1.24 (392) {G0,W4,D2,L2,V0,M1} I { alpha165, c4_2( a324, skol15 ) }.
% 0.72/1.24 (682) {G19,W4,D2,L2,V0,M1} R(426,424) { alpha30, ! c1_2( a322, a323 ) }.
% 0.72/1.24 (145) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a344, a345 ), ! alpha159 }.
% 0.72/1.24 (426) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a322, a323 ), ! alpha48 }.
% 0.72/1.24 (681) {G20,W4,D2,L2,V0,M1} R(429,560) { alpha30, c5_2( a322, a323 ) }.
% 0.72/1.24 (429) {G0,W4,D2,L2,V0,M1} I { c5_2( a322, a323 ), ! alpha67 }.
% 0.72/1.24 (680) {G21,W4,D2,L2,V0,M1} R(432,561) { alpha30, ! c4_2( a322, a323 ) }.
% 0.72/1.24 (143) {G0,W4,D2,L3,V0,M1} I { c2_1( a344 ), alpha140, ! alpha159 }.
% 0.72/1.24 (432) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a322, a323 ), ! alpha89 }.
% 0.72/1.24 (471) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a318, a320 ), ! alpha31 }.
% 0.72/1.24 (474) {G0,W4,D2,L2,V0,M1} I { c2_2( a318, a320 ), ! alpha50 }.
% 0.72/1.24 (480) {G0,W4,D2,L2,V0,M1} I { c2_2( a318, a319 ), ! alpha91 }.
% 0.72/1.24 (140) {G0,W4,D2,L2,V0,M1} I { alpha173, c5_2( a344, skol6 ) }.
% 0.72/1.24 (484) {G0,W4,D2,L2,V0,M1} I { c4_2( a318, a319 ), ! alpha112 }.
% 0.72/1.24 (490) {G0,W4,D2,L2,V0,M1} I { c2_2( a316, a317 ), ! alpha32 }.
% 0.72/1.24 (493) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a316, a317 ), ! alpha51 }.
% 0.72/1.24 (496) {G0,W4,D2,L2,V0,M1} I { c3_2( a316, a317 ), ! alpha70 }.
% 0.72/1.24 (139) {G0,W4,D2,L2,V0,M1} I { alpha173, c1_2( a344, skol6 ) }.
% 0.72/1.24 (531) {G0,W4,D2,L2,V0,M1} I { alpha113, c1_2( a314, skol24 ) }.
% 0.72/1.24 (532) {G0,W4,D2,L2,V0,M1} I { alpha113, ! c4_2( a314, skol24 ) }.
% 0.72/1.24 (533) {G0,W4,D2,L2,V0,M1} I { alpha113, ! c3_2( a314, skol24 ) }.
% 0.72/1.24 (538) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a314, a315 ), ! alpha95 }.
% 0.72/1.24 (138) {G0,W4,D2,L2,V0,M1} I { alpha173, c2_2( a344, skol6 ) }.
% 0.72/1.24 (541) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a314, a315 ), ! alpha114 }.
% 0.72/1.24 (545) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a314, a315 ), ! alpha134 }.
% 0.72/1.24 (554) {G23,W4,D2,L2,V0,M1} R(551,6) { c2_0, ! c5_2( a355, a356 ) }.
% 0.72/1.24 (558) {G24,W4,D2,L2,V0,M1} R(10,555) { c2_0, ! c4_2( a355, a356 ) }.
% 0.72/1.24 (137) {G0,W10,D2,L4,V1,M1} I { ! c2_2( a344, X ), ! c1_2( a344, X ), ! c5_2
% 0.72/1.24 ( a344, X ), ! alpha173 }.
% 0.72/1.24 (678) {G2,W3,D2,L2,V0,M1} R(677,165) { alpha121, ndr1_1( skol7 ) }.
% 0.72/1.24 (677) {G1,W4,D2,L2,V1,M1} R(168,171) { ndr1_1( X ), alpha141( X ) }.
% 0.72/1.24 (168) {G0,W4,D2,L2,V1,M1} I { alpha141( X ), ! alpha160( X ) }.
% 0.72/1.24 (676) {G10,W3,D1,L3,V0,M1} R(134,636);r(651) { c5_0, alpha119, alpha173 }.
% 0.72/1.24 (134) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a344 ), alpha173, ! alpha158 }.
% 0.72/1.24 (675) {G1,W3,D2,L2,V0,M1} R(169,165) { alpha121, ! c3_1( skol7 ) }.
% 0.72/1.24 (169) {G0,W4,D2,L2,V1,M1} I { ! c3_1( X ), alpha141( X ) }.
% 0.72/1.24 (171) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha160( X ) }.
% 0.72/1.24 (172) {G0,W4,D2,L2,V1,M1} I { alpha160( X ), ! alpha175( X ) }.
% 0.72/1.24 (187) {G0,W4,D2,L2,V1,M1} I { alpha122( X ), ! alpha142( X ) }.
% 0.72/1.24 (673) {G1,W3,D2,L2,V0,M1} R(188,184) { alpha101, c4_1( skol9 ) }.
% 0.72/1.24 (188) {G0,W4,D2,L2,V1,M1} I { c4_1( X ), alpha122( X ) }.
% 0.72/1.24 (189) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha142( X ) }.
% 0.72/1.24 (123) {G0,W5,D2,L3,V0,M1} I { c5_2( a346, a347 ), alpha157, ! alpha172 }.
% 0.72/1.24 (672) {G1,W4,D2,L2,V1,M1} R(205,208) { ndr1_1( X ), ! alpha123( X ) }.
% 0.72/1.24 (205) {G0,W4,D2,L2,V1,M1} I { ! alpha123( X ), alpha143( X ) }.
% 0.72/1.24 (208) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha143( X ) }.
% 0.72/1.24 (671) {G2,W3,D2,L2,V0,M1} R(670,203) { alpha78, ndr1_1( skol10 ) }.
% 0.72/1.24 (122) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a346, a347 ), ! alpha157 }.
% 0.72/1.24 (670) {G1,W4,D2,L2,V1,M1} R(213,223) { ndr1_1( X ), alpha102( X ) }.
% 0.72/1.24 (213) {G0,W4,D2,L2,V1,M1} I { alpha102( X ), ! alpha124( X ) }.
% 0.72/1.24 (214) {G0,W4,D2,L2,V1,M1} I { alpha102( X ), ! alpha144( X ) }.
% 0.72/1.24 (669) {G1,W4,D2,L2,V1,M1} R(215,218) { ndr1_1( X ), ! alpha144( X ) }.
% 0.72/1.24 (120) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a346, a347 ), alpha139, ! alpha157
% 0.72/1.24 }.
% 0.72/1.24 (215) {G0,W4,D2,L2,V1,M1} I { ! alpha144( X ), alpha161( X ) }.
% 0.72/1.24 (218) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha161( X ) }.
% 0.72/1.24 (223) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha124( X ) }.
% 0.72/1.24 (224) {G0,W4,D2,L2,V1,M1} I { alpha124( X ), ! alpha145( X ) }.
% 0.72/1.24 (119) {G0,W4,D2,L2,V0,M1} I { c1_2( a346, a347 ), ! alpha139 }.
% 0.72/1.24 (668) {G1,W3,D2,L2,V0,M1} R(289,286) { alpha81, ! c3_1( skol12 ) }.
% 0.72/1.24 (289) {G0,W4,D2,L2,V1,M1} I { ! c3_1( X ), alpha105( X ) }.
% 0.72/1.24 (290) {G0,W4,D2,L2,V1,M1} I { alpha105( X ), ! alpha127( X ) }.
% 0.72/1.24 (291) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha127( X ) }.
% 0.72/1.24 (117) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a346 ), alpha119, ! alpha139 }.
% 0.72/1.24 (667) {G2,W3,D2,L2,V0,M1} R(664,399) { alpha46, ndr1_1( skol16 ) }.
% 0.72/1.24 (664) {G1,W4,D2,L2,V1,M1} R(402,407) { ndr1_1( X ), alpha65( X ) }.
% 0.72/1.24 (665) {G2,W3,D2,L2,V0,M1} R(663,399) { alpha46, ! c4_1( skol16 ) }.
% 0.72/1.24 (666) {G24,W3,D2,L2,V0,M1} S(111);r(615) { alpha188, c3_1( a348 ) }.
% 0.72/1.24 (663) {G1,W4,D2,L2,V1,M1} R(402,406) { ! c4_1( X ), alpha65( X ) }.
% 0.72/1.24 (402) {G0,W4,D2,L2,V1,M1} I { alpha65( X ), ! alpha87( X ) }.
% 0.72/1.24 (406) {G0,W4,D2,L2,V1,M1} I { ! c4_1( X ), alpha87( X ) }.
% 0.72/1.24 (407) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha87( X ) }.
% 0.72/1.24 (108) {G0,W4,D2,L2,V0,M1} I { alpha190, c2_2( a348, skol5 ) }.
% 0.72/1.24 (662) {G2,W3,D2,L2,V0,M1} R(661,445) { alpha68, ndr1_1( skol20 ) }.
% 0.72/1.24 (661) {G1,W4,D2,L2,V1,M1} R(448,458) { ndr1_1( X ), alpha90( X ) }.
% 0.72/1.24 (448) {G0,W4,D2,L2,V1,M1} I { alpha90( X ), ! alpha111( X ) }.
% 0.72/1.24 (449) {G0,W4,D2,L2,V1,M1} I { alpha90( X ), ! alpha132( X ) }.
% 0.72/1.24 (107) {G0,W4,D2,L2,V0,M1} I { alpha190, c4_2( a348, skol5 ) }.
% 0.72/1.24 (660) {G1,W4,D2,L2,V1,M1} R(450,453) { ndr1_1( X ), ! alpha132( X ) }.
% 0.72/1.24 (450) {G0,W4,D2,L2,V1,M1} I { ! alpha132( X ), alpha150( X ) }.
% 0.72/1.24 (453) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha150( X ) }.
% 0.72/1.24 (458) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha111( X ) }.
% 0.72/1.24 (106) {G0,W4,D2,L2,V0,M1} I { alpha190, ! c5_2( a348, skol5 ) }.
% 0.72/1.24 (459) {G0,W4,D2,L2,V1,M1} I { alpha111( X ), ! alpha133( X ) }.
% 0.72/1.24 (658) {G2,W3,D2,L2,V0,M1} R(657,506) { alpha33, ndr1_1( skol22 ) }.
% 0.72/1.24 (657) {G1,W4,D2,L2,V1,M1} R(509,512) { ndr1_1( X ), alpha52( X ) }.
% 0.72/1.24 (509) {G0,W4,D2,L2,V1,M1} I { alpha52( X ), ! alpha71( X ) }.
% 0.72/1.24 (105) {G0,W10,D2,L4,V1,M1} I { c5_2( a348, X ), ! c4_2( a348, X ), ! c2_2(
% 0.72/1.24 a348, X ), ! alpha190 }.
% 0.72/1.24 (656) {G1,W3,D2,L2,V0,M1} R(510,506) { alpha33, c4_1( skol22 ) }.
% 0.72/1.24 (510) {G0,W4,D2,L2,V1,M1} I { c4_1( X ), alpha52( X ) }.
% 0.72/1.24 (512) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha71( X ) }.
% 0.72/1.24 (513) {G0,W4,D2,L2,V1,M1} I { alpha71( X ), ! alpha93( X ) }.
% 0.72/1.24 (102) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a348 ), alpha190, ! alpha189 }.
% 0.72/1.24 (655) {G2,W3,D2,L2,V0,M1} R(641,68) { alpha155, c3_1( skol3 ) }.
% 0.72/1.24 (641) {G1,W4,D2,L2,V1,M1} R(79,75) { c3_1( X ), alpha170( X ) }.
% 0.72/1.24 (647) {G1,W4,D2,L2,V1,M1} R(83,80) { ndr1_1( X ), ! alpha185( X ) }.
% 0.72/1.24 (653) {G24,W3,D1,L3,V0,M1} S(588);r(604) { c4_0, alpha110, alpha68 }.
% 0.72/1.24 (98) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a348 ), alpha183, ! alpha186 }.
% 0.72/1.24 (97) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a348 ), ! alpha183 }.
% 0.72/1.24 (103) {G0,W3,D2,L2,V0,M1} I { alpha189, ndr1_1( a348 ) }.
% 0.72/1.24 (110) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a348 ), ! alpha188 }.
% 0.72/1.24 (95) {G0,W5,D2,L3,V0,M1} I { c5_2( a348, a349 ), alpha171, ! alpha183 }.
% 0.72/1.24 (116) {G0,W3,D2,L2,V0,M1} I { c3_1( a346 ), ! alpha119 }.
% 0.72/1.24 (125) {G0,W3,D2,L2,V0,M1} I { c4_1( a346 ), ! alpha172 }.
% 0.72/1.24 (126) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a346 ), ! alpha172 }.
% 0.72/1.24 (135) {G0,W3,D2,L2,V0,M1} I { alpha158, ndr1_1( a344 ) }.
% 0.72/1.24 (94) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a348, a349 ), ! alpha171 }.
% 0.72/1.24 (142) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a344 ), ! alpha140 }.
% 0.72/1.24 (148) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a344 ), ! alpha174 }.
% 0.72/1.24 (650) {G6,W3,D2,L2,V0,M1} R(155,153) { c3_0, ! c1_1( a343 ) }.
% 0.72/1.24 (155) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a343 ), ! alpha99 }.
% 0.72/1.24 (92) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a348, a349 ), alpha156, ! alpha171 }.
% 0.72/1.24 (649) {G6,W3,D2,L2,V0,M1} R(156,153) { c3_0, c2_1( a343 ) }.
% 0.72/1.24 (156) {G0,W3,D2,L2,V0,M1} I { c2_1( a343 ), ! alpha99 }.
% 0.72/1.24 (165) {G0,W3,D2,L2,V0,M1} I { alpha121, ! alpha141( skol7 ) }.
% 0.72/1.24 (166) {G0,W3,D2,L2,V0,M1} I { alpha121, c2_1( skol7 ) }.
% 0.72/1.24 (91) {G0,W4,D2,L2,V0,M1} I { c2_2( a348, a349 ), ! alpha156 }.
% 0.72/1.24 (184) {G0,W3,D2,L2,V0,M1} I { alpha101, ! alpha122( skol9 ) }.
% 0.72/1.24 (185) {G0,W3,D2,L2,V0,M1} I { alpha101, ! c5_1( skol9 ) }.
% 0.72/1.24 (203) {G0,W3,D2,L2,V0,M1} I { alpha78, ! alpha102( skol10 ) }.
% 0.72/1.24 (204) {G0,W3,D2,L2,V0,M1} I { alpha78, ! alpha123( skol10 ) }.
% 0.72/1.24 (86) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a350 ), alpha187( X
% 0.72/1.24 ), c3_2( X, a350 ) }.
% 0.72/1.24 (245) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a338 ), ! alpha162 }.
% 0.72/1.24 (248) {G0,W3,D2,L2,V0,M1} I { c1_1( a338 ), ! alpha176 }.
% 0.72/1.24 (249) {G0,W3,D2,L2,V0,M1} I { c4_1( a338 ), ! alpha176 }.
% 0.72/1.24 (267) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a335 ), ! alpha126 }.
% 0.72/1.24 (85) {G0,W5,D2,L2,V1,M1} I { ! alpha187( X ), ! c3_2( X, a350 ) }.
% 0.72/1.24 (276) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a335 ), ! alpha177 }.
% 0.72/1.24 (286) {G0,W3,D2,L2,V0,M1} I { alpha81, ! alpha105( skol12 ) }.
% 0.72/1.24 (287) {G0,W3,D2,L2,V0,M1} I { alpha81, ! c5_1( skol12 ) }.
% 0.72/1.24 (298) {G13,W3,D2,L2,V0,M1} I;r(296) { alpha61, ! c3_1( a333 ) }.
% 0.72/1.24 (84) {G0,W5,D2,L2,V1,M1} I { ! alpha187( X ), c2_2( X, a350 ) }.
% 0.72/1.24 (303) {G0,W3,D2,L2,V0,M1} I { c3_1( a331 ), ! alpha82 }.
% 0.72/1.24 (306) {G0,W3,D2,L2,V0,M1} I { c5_1( a331 ), ! alpha106 }.
% 0.72/1.24 (315) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a331 ), ! alpha164 }.
% 0.72/1.24 (646) {G15,W3,D2,L2,V0,M1} R(322,320) { alpha27, c1_1( a329 ) }.
% 0.72/1.24 (83) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha187( X ) }.
% 0.72/1.24 (322) {G0,W3,D2,L2,V0,M1} I { c1_1( a329 ), ! alpha42 }.
% 0.72/1.24 (328) {G0,W3,D2,L2,V0,M1} I { alpha107, ndr1_1( a329 ) }.
% 0.72/1.24 (645) {G17,W3,D2,L2,V0,M1} R(335,568) { alpha27, ndr1_1( a329 ) }.
% 0.72/1.24 (335) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a329 ), ! alpha83 }.
% 0.72/1.24 (82) {G0,W7,D2,L3,V1,M1} I { ! alpha187( X ), alpha185( X ), c1_2( X, a350
% 0.72/1.24 ) }.
% 0.72/1.24 (342) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a328 ), ! alpha43 }.
% 0.72/1.24 (343) {G0,W3,D2,L2,V0,M1} I { c5_1( a328 ), ! alpha43 }.
% 0.72/1.24 (358) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a326 ), ! alpha108 }.
% 0.72/1.24 (361) {G0,W3,D2,L2,V0,M1} I { c2_1( a326 ), ! alpha130 }.
% 0.72/1.24 (81) {G0,W5,D2,L2,V1,M1} I { ! alpha185( X ), ! c1_2( X, a350 ) }.
% 0.72/1.24 (362) {G0,W3,D2,L2,V0,M1} I { c4_1( a326 ), ! alpha130 }.
% 0.72/1.24 (371) {G0,W3,D2,L2,V0,M1} I { alpha85, ndr1_1( a324 ) }.
% 0.72/1.24 (381) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a324 ), ! alpha109 }.
% 0.72/1.24 (387) {G0,W3,D2,L2,V0,M1} I { alpha149, ndr1_1( a324 ) }.
% 0.72/1.24 (80) {G0,W4,D2,L2,V1,M1} I { ! alpha185( X ), alpha187( X ) }.
% 0.72/1.24 (399) {G0,W3,D2,L2,V0,M1} I { alpha46, ! alpha65( skol16 ) }.
% 0.72/1.24 (400) {G0,W3,D2,L2,V0,M1} I { alpha46, ! c2_1( skol16 ) }.
% 0.72/1.24 (413) {G0,W3,D2,L2,V0,M1} I { alpha47, c2_1( skol18 ) }.
% 0.72/1.24 (414) {G0,W3,D2,L2,V0,M1} I { alpha47, ! c4_1( skol18 ) }.
% 0.72/1.24 (79) {G0,W4,D2,L2,V1,M1} I { c3_1( X ), alpha182( X ) }.
% 0.72/1.24 (420) {G0,W3,D2,L2,V0,M1} I { alpha88, ! c1_1( skol19 ) }.
% 0.72/1.24 (421) {G0,W3,D2,L2,V0,M1} I { alpha88, ! c5_1( skol19 ) }.
% 0.72/1.24 (435) {G0,W3,D2,L2,V0,M1} I { c3_1( a322 ), ! alpha110 }.
% 0.72/1.24 (436) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a322 ), ! alpha110 }.
% 0.72/1.24 (78) {G0,W4,D2,L2,V1,M1} I { alpha182( X ), ! alpha185( X ) }.
% 0.72/1.24 (445) {G0,W3,D2,L2,V0,M1} I { alpha68, ! alpha90( skol20 ) }.
% 0.72/1.24 (446) {G0,W3,D2,L2,V0,M1} I { alpha68, c2_1( skol20 ) }.
% 0.72/1.24 (477) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a318 ), ! alpha69 }.
% 0.72/1.24 (483) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a318 ), ! alpha112 }.
% 0.72/1.24 (77) {G0,W6,D2,L3,V1,M1} I { ! alpha182( X ), ! c3_1( X ), alpha185( X )
% 0.72/1.24 }.
% 0.72/1.24 (487) {G0,W3,D2,L2,V0,M1} I { c1_1( a316 ), ! alpha20 }.
% 0.72/1.24 (499) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a316 ), ! alpha92 }.
% 0.72/1.24 (500) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a316 ), ! alpha92 }.
% 0.72/1.24 (640) {G1,W3,D2,L2,V0,M1} R(76,68) { alpha155, ndr1_1( skol3 ) }.
% 0.72/1.24 (76) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha170( X ) }.
% 0.72/1.24 (506) {G0,W3,D2,L2,V0,M1} I { alpha33, ! alpha52( skol22 ) }.
% 0.72/1.24 (507) {G0,W3,D2,L2,V0,M1} I { alpha33, ! c5_1( skol22 ) }.
% 0.72/1.24 (528) {G0,W3,D2,L2,V0,M1} I { alpha94, ndr1_1( a314 ) }.
% 0.72/1.24 (535) {G0,W3,D2,L2,V0,M1} I { c4_1( a314 ), ! alpha72 }.
% 0.72/1.24 (75) {G0,W4,D2,L2,V1,M1} I { alpha170( X ), ! alpha182( X ) }.
% 0.72/1.24 (544) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a314 ), ! alpha134 }.
% 0.72/1.24 (553) {G22,W3,D2,L2,V0,M1} S(4);r(550) { c2_0, ! c3_1( a355 ) }.
% 0.72/1.24 (557) {G24,W3,D2,L2,V0,M1} R(9,555) { c2_0, ndr1_1( a355 ) }.
% 0.72/1.24 (639) {G24,W2,D1,L2,V0,M1} S(87);r(615) { alpha156, ! alpha138 }.
% 0.72/1.24 (74) {G0,W6,D2,L3,V1,M1} I { ! alpha170( X ), ! ndr1_1( X ), alpha182( X )
% 0.72/1.24 }.
% 0.72/1.24 (101) {G0,W3,D1,L3,V0,M1} I { ! alpha188, alpha186, ! alpha189 }.
% 0.72/1.24 (636) {G6,W3,D1,L3,V0,M1} R(634,132) { c5_0, alpha119, alpha158 }.
% 0.72/1.24 (638) {G8,W3,D1,L3,V0,M1} R(637,144) { c5_0, alpha119, alpha174 }.
% 0.72/1.24 (73) {G0,W6,D3,L2,V1,M1} I { alpha181( X ), ! c5_2( X, skol4( X ) ) }.
% 0.72/1.24 (637) {G7,W3,D1,L3,V0,M1} R(635,141) { c5_0, alpha119, alpha159 }.
% 0.72/1.24 (635) {G6,W3,D1,L3,V0,M1} R(634,131) { c5_0, alpha119, alpha140 }.
% 0.72/1.24 (634) {G5,W3,D1,L3,V0,M1} R(128,114) { c5_0, alpha119, alpha120 }.
% 0.72/1.24 (128) {G0,W3,D1,L3,V0,M1} I { alpha120, c5_0, ! alpha98 }.
% 0.72/1.24 (72) {G0,W6,D3,L2,V1,M1} I { alpha181( X ), c4_2( X, skol4( X ) ) }.
% 0.72/1.24 (133) {G0,W3,D1,L3,V0,M1} I { ! alpha140, alpha120, ! alpha158 }.
% 0.72/1.24 (633) {G25,W2,D1,L2,V0,M1} R(632,160) { c5_0, alpha121 }.
% 0.72/1.24 (632) {G24,W2,D1,L2,V0,M1} S(161);r(615) { alpha121, ! alpha100 }.
% 0.72/1.24 (71) {G0,W6,D3,L2,V1,M1} I { alpha181( X ), ! c1_2( X, skol4( X ) ) }.
% 0.72/1.24 (631) {G23,W2,D1,L2,V0,M1} S(179);r(585) { ! c3_0, ! c5_0 }.
% 0.72/1.24 (630) {G20,W2,D1,L2,V0,M1} R(629,182) { c4_0, alpha101 }.
% 0.72/1.24 (629) {G19,W2,D1,L2,V0,M1} S(193);r(604) { c4_0, ! alpha77 }.
% 0.72/1.24 (70) {G0,W11,D2,L4,V2,M1} I { ! alpha181( X ), c1_2( X, Y ), ! c4_2( X, Y )
% 0.72/1.24 , c5_2( X, Y ) }.
% 0.72/1.24 (198) {G9,W3,D1,L3,V0,M1} I;r(197) { c3_0, c5_0, ! c1_0 }.
% 0.72/1.24 (628) {G24,W2,D1,L2,V0,M1} S(229);r(615) { alpha79, ! alpha58 }.
% 0.72/1.24 (69) {G0,W3,D2,L2,V0,M1} I { alpha155, ! alpha181( skol3 ) }.
% 0.72/1.24 (232) {G0,W3,D1,L3,V0,M1} I { ! c5_0, alpha103, ! alpha79 }.
% 0.72/1.24 (627) {G18,W3,D1,L3,V0,M1} R(626,272) { c4_0, c5_0, alpha177 }.
% 0.72/1.24 (626) {G17,W3,D1,L3,V0,M1} R(625,269) { c4_0, c5_0, alpha163 }.
% 0.72/1.24 (625) {G16,W3,D1,L3,V0,M1} R(624,266) { c4_0, c5_0, alpha147 }.
% 0.72/1.24 (68) {G0,W3,D2,L2,V0,M1} I { alpha155, ! alpha170( skol3 ) }.
% 0.72/1.24 (624) {G15,W3,D1,L3,V0,M1} R(623,263) { c4_0, c5_0, alpha126 }.
% 0.72/1.24 (623) {G14,W3,D1,L3,V0,M1} R(622,260) { c4_0, c5_0, alpha104 }.
% 0.72/1.24 (622) {G13,W3,D1,L3,V0,M1} R(620,257) { c4_0, c5_0, alpha80 }.
% 0.72/1.24 (620) {G12,W3,D1,L3,V0,M1} R(254,253) { c4_0, c5_0, alpha59 }.
% 0.72/1.24 (67) {G0,W5,D2,L3,V1,M1} I { alpha170( X ), alpha181( X ), ! alpha155 }.
% 0.72/1.24 (254) {G0,W3,D1,L3,V0,M1} I { alpha59, c4_0, ! alpha39 }.
% 0.72/1.24 (619) {G25,W2,D1,L2,V0,M1} R(618,281) { c1_0, alpha81 }.
% 0.72/1.24 (618) {G24,W2,D1,L2,V0,M1} S(282);r(615) { alpha81, ! alpha60 }.
% 0.72/1.24 (63) {G2,W3,D1,L3,V0,M1} I;r(62) { c4_0, ! c1_0, ! c5_0 }.
% 0.72/1.24 (615) {G23,W1,D1,L1,V0,M1} R(614,311);r(314) { ndr1_0 }.
% 0.72/1.24 (299) {G0,W3,D1,L3,V0,M1} I { ! c4_0, alpha82, ! alpha61 }.
% 0.72/1.24 (326) {G0,W3,D1,L3,V0,M1} I { ! alpha107, alpha62, ! alpha83 }.
% 0.72/1.24 (603) {G17,W3,D1,L3,V0,M1} R(338,569) { c4_0, alpha107, alpha43 }.
% 0.72/1.24 (59) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a351 ), ! alpha180 }.
% 0.72/1.24 (338) {G0,W3,D1,L3,V0,M1} I { alpha43, c4_0, ! alpha27 }.
% 0.72/1.24 (594) {G20,W3,D1,L3,V0,M1} R(592,368) { c5_0, alpha108, alpha85 }.
% 0.72/1.24 (599) {G24,W3,D1,L3,V0,M1} R(597,384) { c5_0, alpha108, alpha149 }.
% 0.72/1.24 (58) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a351 ), ! alpha180 }.
% 0.72/1.24 (597) {G23,W3,D1,L3,V0,M1} R(596,380) { c5_0, alpha108, alpha131 }.
% 0.72/1.24 (596) {G22,W3,D1,L3,V0,M1} R(595,377) { c5_0, alpha108, alpha109 }.
% 0.72/1.24 (56) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a351, a352 ), alpha169, ! alpha180 }.
% 0.72/1.24 (595) {G21,W3,D1,L3,V0,M1} R(593,374) { c5_0, alpha108, alpha86 }.
% 0.72/1.24 (593) {G20,W3,D1,L3,V0,M1} R(592,367) { c5_0, alpha108, alpha64 }.
% 0.72/1.24 (592) {G19,W3,D1,L3,V0,M1} R(364,566) { c5_0, alpha108, alpha45 }.
% 0.72/1.24 (364) {G0,W3,D1,L3,V0,M1} I { c5_0, alpha45, ! alpha28 }.
% 0.72/1.24 (55) {G0,W4,D2,L2,V0,M1} I { c2_2( a351, a352 ), ! alpha169 }.
% 0.72/1.24 (369) {G0,W3,D1,L3,V0,M1} I { ! alpha64, alpha45, ! alpha85 }.
% 0.72/1.24 (590) {G2,W2,D1,L2,V0,M1} S(408);r(563) { alpha47, ! alpha29 }.
% 0.72/1.24 (53) {G0,W5,D2,L3,V0,M1} I { c1_2( a351, a352 ), alpha154, ! alpha169 }.
% 0.72/1.24 (589) {G1,W2,D1,L2,V0,M1} S(415);r(419) { alpha88, ! alpha66 }.
% 0.72/1.24 (587) {G22,W3,D1,L3,V0,M1} R(438,562) { c4_0, alpha110, alpha49 }.
% 0.72/1.24 (438) {G0,W3,D1,L3,V0,M1} I { alpha49, c4_0, ! alpha30 }.
% 0.72/1.24 (52) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a351, a352 ), ! alpha154 }.
% 0.72/1.24 (467) {G0,W3,D1,L3,V0,M1} I { alpha20, alpha31, ! alpha11 }.
% 0.72/1.24 (521) {G0,W3,D1,L3,V0,M1} I { c4_0, alpha53, ! alpha34 }.
% 0.72/1.24 (50) {G0,W5,D2,L3,V0,M1} I { c4_2( a351, a352 ), alpha137, ! alpha154 }.
% 0.72/1.24 (526) {G0,W3,D1,L3,V0,M1} I { ! alpha72, alpha53, ! alpha94 }.
% 0.72/1.24 (585) {G22,W2,D1,L2,V0,M1} S(549);r(394) { ! c3_0, ! c4_0 }.
% 0.72/1.24 (583) {G7,W3,D1,L3,V0,M1} R(582,54) { c3_0, alpha115, alpha180 }.
% 0.72/1.24 (49) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a351, a352 ), ! alpha137 }.
% 0.72/1.24 (582) {G6,W3,D1,L3,V0,M1} R(581,51) { c3_0, alpha115, alpha169 }.
% 0.72/1.24 (581) {G5,W3,D1,L3,V0,M1} R(579,48) { c3_0, alpha115, alpha154 }.
% 0.72/1.24 (579) {G4,W3,D1,L3,V0,M1} R(576,45) { c3_0, alpha115, alpha137 }.
% 0.72/1.24 (580) {G4,W2,D1,L2,V0,M1} R(576,43);r(44) { alpha115, alpha96 }.
% 0.72/1.24 (47) {G0,W4,D2,L3,V0,M1} I { ! c4_1( a351 ), alpha116, ! alpha137 }.
% 0.72/1.24 (576) {G3,W3,D1,L3,V0,M1} R(574,13) { c3_0, alpha115, alpha116 }.
% 0.72/1.24 (575) {G3,W3,D1,L3,V0,M1} R(574,14) { c3_0, alpha116, alpha167 }.
% 0.72/1.24 (574) {G2,W3,D1,L3,V0,M1} R(42,12) { c3_0, alpha116, alpha152 }.
% 0.72/1.24 (48) {G0,W2,D1,L2,V0,M1} I { alpha154, ! alpha137 }.
% 0.72/1.24 (46) {G0,W3,D2,L2,V0,M1} I { c4_1( a351 ), ! alpha116 }.
% 0.72/1.24 (51) {G0,W2,D1,L2,V0,M1} I { alpha169, ! alpha154 }.
% 0.72/1.24 (54) {G0,W2,D1,L2,V0,M1} I { alpha180, ! alpha169 }.
% 0.72/1.24 (66) {G3,W2,D1,L2,V0,M1} I;r(65) { alpha138, alpha155 }.
% 0.72/1.24 (45) {G0,W2,D1,L2,V0,M1} I { alpha137, ! alpha116 }.
% 0.72/1.24 (88) {G0,W2,D1,L2,V0,M1} I { alpha138, ! alpha156 }.
% 0.72/1.24 (90) {G0,W2,D1,L2,V0,M1} I { alpha171, ! alpha156 }.
% 0.72/1.24 (93) {G0,W2,D1,L2,V0,M1} I { alpha183, ! alpha171 }.
% 0.72/1.24 (44) {G0,W2,D1,L2,V0,M1} I { alpha96, ! c3_0 }.
% 0.72/1.24 (96) {G0,W2,D1,L2,V0,M1} I { alpha186, ! alpha183 }.
% 0.72/1.24 (99) {G0,W2,D1,L2,V0,M1} I { alpha188, ! alpha186 }.
% 0.72/1.24 (100) {G0,W2,D1,L2,V0,M1} I { alpha189, ! alpha186 }.
% 0.72/1.24 (104) {G0,W2,D1,L2,V0,M1} I { alpha189, ! alpha190 }.
% 0.72/1.24 (43) {G0,W2,D1,L2,V0,M1} I { alpha96, ! alpha116 }.
% 0.72/1.24 (114) {G4,W2,D1,L2,V0,M1} I;r(113) { alpha119, alpha98 }.
% 0.72/1.24 (115) {G0,W2,D1,L2,V0,M1} I { alpha139, ! alpha119 }.
% 0.72/1.24 (118) {G0,W2,D1,L2,V0,M1} I { alpha157, ! alpha139 }.
% 0.72/1.24 (42) {G0,W3,D1,L3,V0,M1} I { alpha116, c3_0, ! alpha96 }.
% 0.72/1.24 (121) {G0,W2,D1,L2,V0,M1} I { alpha172, ! alpha157 }.
% 0.72/1.24 (129) {G0,W2,D1,L2,V0,M1} I { alpha98, ! alpha120 }.
% 0.72/1.24 (130) {G0,W2,D1,L2,V0,M1} I { alpha98, ! c5_0 }.
% 0.72/1.24 (41) {G0,W4,D2,L2,V0,M1} I { alpha184, c5_2( a353, skol2 ) }.
% 0.72/1.24 (131) {G0,W2,D1,L2,V0,M1} I { alpha140, ! alpha120 }.
% 0.72/1.24 (132) {G0,W2,D1,L2,V0,M1} I { alpha158, ! alpha120 }.
% 0.72/1.24 (136) {G0,W2,D1,L2,V0,M1} I { alpha158, ! alpha173 }.
% 0.72/1.24 (141) {G0,W2,D1,L2,V0,M1} I { alpha159, ! alpha140 }.
% 0.72/1.24 (40) {G0,W4,D2,L2,V0,M1} I { alpha184, ! c3_2( a353, skol2 ) }.
% 0.72/1.24 (144) {G0,W2,D1,L2,V0,M1} I { alpha174, ! alpha159 }.
% 0.72/1.24 (153) {G5,W2,D1,L2,V0,M1} I;r(152) { c3_0, alpha99 }.
% 0.72/1.24 (39) {G0,W4,D2,L2,V0,M1} I { alpha184, c2_2( a353, skol2 ) }.
% 0.72/1.24 (160) {G6,W2,D1,L2,V0,M1} I;r(159) { c5_0, alpha100 }.
% 0.72/1.25 (163) {G0,W2,D1,L2,V0,M1} I { alpha100, ! alpha121 }.
% 0.72/1.25 (38) {G0,W10,D2,L4,V1,M1} I { ! c2_2( a353, X ), c3_2( a353, X ), ! c5_2(
% 0.72/1.25 a353, X ), ! alpha184 }.
% 0.72/1.25 (182) {G8,W2,D1,L2,V0,M1} I;r(181) { alpha101, alpha77 }.
% 0.72/1.25 (194) {G0,W2,D1,L2,V0,M1} I { alpha77, ! c4_0 }.
% 0.72/1.25 (201) {G10,W2,D1,L2,V0,M1} I;r(200) { alpha58, alpha78 }.
% 0.72/1.25 (37) {G0,W2,D1,L2,V0,M1} I { alpha179, ! alpha184 }.
% 0.72/1.25 (571) {G1,W2,D1,L2,V0,M1} R(230,233) { c5_0, alpha58 }.
% 0.72/1.25 (230) {G0,W2,D1,L2,V0,M1} I { alpha58, ! alpha79 }.
% 0.72/1.25 (233) {G0,W2,D1,L2,V0,M1} I { c5_0, alpha79 }.
% 0.72/1.25 (36) {G0,W3,D2,L2,V0,M1} I { alpha179, ndr1_1( a353 ) }.
% 0.72/1.25 (234) {G0,W2,D1,L2,V0,M1} I { alpha79, ! alpha103 }.
% 0.72/1.25 (235) {G0,W2,D1,L2,V0,M1} I { alpha125, ! alpha103 }.
% 0.72/1.25 (238) {G0,W2,D1,L2,V0,M1} I { alpha146, ! alpha125 }.
% 0.72/1.25 (241) {G0,W2,D1,L2,V0,M1} I { alpha162, ! alpha146 }.
% 0.72/1.25 (35) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a353 ), alpha184, ! alpha179 }.
% 0.72/1.25 (244) {G0,W2,D1,L2,V0,M1} I { alpha176, ! alpha162 }.
% 0.72/1.25 (253) {G11,W2,D1,L2,V0,M1} I;r(252) { c5_0, alpha39 }.
% 0.72/1.25 (255) {G0,W2,D1,L2,V0,M1} I { alpha39, ! alpha59 }.
% 0.72/1.25 (256) {G0,W2,D1,L2,V0,M1} I { alpha39, ! c4_0 }.
% 0.72/1.25 (257) {G0,W2,D1,L2,V0,M1} I { alpha80, ! alpha59 }.
% 0.72/1.25 (260) {G0,W2,D1,L2,V0,M1} I { alpha104, ! alpha80 }.
% 0.72/1.25 (263) {G0,W2,D1,L2,V0,M1} I { alpha126, ! alpha104 }.
% 0.72/1.25 (33) {G0,W2,D1,L2,V0,M1} I { alpha179, ! alpha168 }.
% 0.72/1.25 (266) {G0,W2,D1,L2,V0,M1} I { alpha147, ! alpha126 }.
% 0.72/1.25 (269) {G0,W2,D1,L2,V0,M1} I { alpha163, ! alpha147 }.
% 0.72/1.25 (272) {G0,W2,D1,L2,V0,M1} I { alpha177, ! alpha163 }.
% 0.72/1.25 (281) {G12,W2,D1,L2,V0,M1} I;r(280) { c1_0, alpha60 }.
% 0.72/1.25 (284) {G0,W2,D1,L2,V0,M1} I { alpha60, ! alpha81 }.
% 0.72/1.25 (31) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a353 ), alpha153, ! alpha168 }.
% 0.72/1.25 (300) {G0,W2,D1,L2,V0,M1} I { c4_0, alpha61 }.
% 0.72/1.25 (301) {G0,W2,D1,L2,V0,M1} I { alpha61, ! alpha82 }.
% 0.72/1.25 (302) {G0,W2,D1,L2,V0,M1} I { alpha106, ! alpha82 }.
% 0.72/1.25 (305) {G0,W2,D1,L2,V0,M1} I { alpha128, ! alpha106 }.
% 0.72/1.25 (30) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a353 ), ! alpha153 }.
% 0.72/1.25 (308) {G0,W2,D1,L2,V0,M1} I { alpha148, ! alpha128 }.
% 0.72/1.25 (311) {G0,W2,D1,L2,V0,M1} I { alpha164, ! alpha148 }.
% 0.72/1.25 (569) {G16,W2,D1,L2,V0,M1} R(567,325) { alpha107, alpha27 }.
% 0.72/1.25 (29) {G0,W2,D1,L2,V0,M1} I { alpha168, ! alpha153 }.
% 0.72/1.25 (568) {G16,W2,D1,L2,V0,M1} R(567,324) { alpha27, alpha83 }.
% 0.72/1.25 (567) {G15,W2,D1,L2,V0,M1} R(320,321) { alpha27, alpha62 }.
% 0.72/1.25 (320) {G14,W2,D1,L2,V0,M1} I;r(319) { alpha27, alpha42 }.
% 0.72/1.25 (28) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a353, a354 ), alpha136, ! alpha153 }.
% 0.72/1.25 (321) {G0,W2,D1,L2,V0,M1} I { alpha62, ! alpha42 }.
% 0.72/1.25 (324) {G0,W2,D1,L2,V0,M1} I { alpha83, ! alpha62 }.
% 0.72/1.25 (325) {G0,W2,D1,L2,V0,M1} I { alpha107, ! alpha62 }.
% 0.72/1.25 (329) {G0,W2,D1,L2,V0,M1} I { alpha107, ! alpha129 }.
% 0.72/1.25 (27) {G0,W4,D2,L2,V0,M1} I { c2_2( a353, a354 ), ! alpha136 }.
% 0.72/1.25 (339) {G0,W2,D1,L2,V0,M1} I { alpha27, ! alpha43 }.
% 0.72/1.25 (340) {G0,W2,D1,L2,V0,M1} I { alpha27, ! c4_0 }.
% 0.72/1.25 (26) {G0,W2,D1,L2,V0,M1} I { alpha153, ! alpha136 }.
% 0.72/1.25 (566) {G18,W2,D1,L2,V0,M1} R(565,354) { alpha108, alpha28 }.
% 0.72/1.25 (565) {G17,W2,D1,L2,V0,M1} R(564,351) { alpha28, alpha84 }.
% 0.72/1.25 (564) {G16,W2,D1,L2,V0,M1} R(347,348) { alpha28, alpha63 }.
% 0.72/1.25 (347) {G15,W2,D1,L2,V0,M1} I;r(346) { alpha28, alpha44 }.
% 0.72/1.25 (25) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a353, a354 ), alpha115, ! alpha136 }.
% 0.72/1.25 (348) {G0,W2,D1,L2,V0,M1} I { alpha63, ! alpha44 }.
% 0.72/1.25 (351) {G0,W2,D1,L2,V0,M1} I { alpha84, ! alpha63 }.
% 0.72/1.25 (354) {G0,W2,D1,L2,V0,M1} I { alpha108, ! alpha84 }.
% 0.72/1.25 (357) {G0,W2,D1,L2,V0,M1} I { alpha130, ! alpha108 }.
% 0.72/1.25 (24) {G0,W4,D2,L2,V0,M1} I { c3_2( a353, a354 ), ! alpha115 }.
% 0.72/1.25 (365) {G0,W2,D1,L2,V0,M1} I { alpha28, ! c5_0 }.
% 0.72/1.25 (366) {G0,W2,D1,L2,V0,M1} I { alpha28, ! alpha45 }.
% 0.72/1.25 (367) {G0,W2,D1,L2,V0,M1} I { alpha64, ! alpha45 }.
% 0.72/1.25 (23) {G0,W2,D1,L2,V0,M1} I { alpha136, ! alpha115 }.
% 0.72/1.25 (368) {G0,W2,D1,L2,V0,M1} I { alpha85, ! alpha45 }.
% 0.72/1.25 (374) {G0,W2,D1,L2,V0,M1} I { alpha86, ! alpha64 }.
% 0.72/1.25 (377) {G0,W2,D1,L2,V0,M1} I { alpha109, ! alpha86 }.
% 0.72/1.25 (380) {G0,W2,D1,L2,V0,M1} I { alpha131, ! alpha109 }.
% 0.72/1.25 (22) {G0,W4,D2,L2,V0,M1} I { alpha178, ! c3_2( a353, skol1 ) }.
% 0.72/1.25 (384) {G0,W2,D1,L2,V0,M1} I { alpha149, ! alpha131 }.
% 0.72/1.25 (388) {G0,W2,D1,L2,V0,M1} I { alpha149, ! alpha165 }.
% 0.72/1.25 (394) {G15,W2,D1,L2,V0,M1} I;r(345) { c2_0, ! c3_0 }.
% 0.72/1.25 (21) {G0,W4,D2,L2,V0,M1} I { alpha178, c4_2( a353, skol1 ) }.
% 0.72/1.25 (397) {G17,W2,D1,L2,V0,M1} I;r(396) { alpha29, alpha46 }.
% 0.72/1.25 (409) {G0,W2,D1,L2,V0,M1} I { alpha29, ! alpha47 }.
% 0.72/1.25 (20) {G0,W4,D2,L2,V0,M1} I { alpha178, c1_2( a353, skol1 ) }.
% 0.72/1.25 (412) {G0,W2,D1,L2,V0,M1} I { alpha47, ! alpha66 }.
% 0.72/1.25 (416) {G0,W2,D1,L2,V0,M1} I { alpha66, ! alpha88 }.
% 0.72/1.25 (19) {G0,W10,D2,L4,V1,M1} I { ! c1_2( a353, X ), ! c4_2( a353, X ), c3_2(
% 0.72/1.25 a353, X ), ! alpha178 }.
% 0.72/1.25 (562) {G21,W2,D1,L2,V0,M1} R(561,431) { alpha110, alpha30 }.
% 0.72/1.25 (561) {G20,W2,D1,L2,V0,M1} R(560,428) { alpha30, alpha89 }.
% 0.72/1.25 (560) {G19,W2,D1,L2,V0,M1} R(424,425) { alpha30, alpha67 }.
% 0.72/1.25 (424) {G18,W2,D1,L2,V0,M1} I;r(423) { alpha30, alpha48 }.
% 0.72/1.25 (18) {G0,W2,D1,L2,V0,M1} I { alpha167, ! alpha178 }.
% 0.72/1.25 (425) {G0,W2,D1,L2,V0,M1} I { alpha67, ! alpha48 }.
% 0.72/1.25 (428) {G0,W2,D1,L2,V0,M1} I { alpha89, ! alpha67 }.
% 0.72/1.25 (431) {G0,W2,D1,L2,V0,M1} I { alpha110, ! alpha89 }.
% 0.72/1.25 (17) {G0,W3,D2,L2,V0,M1} I { alpha167, ndr1_1( a353 ) }.
% 0.72/1.25 (439) {G0,W2,D1,L2,V0,M1} I { alpha30, ! alpha49 }.
% 0.72/1.25 (440) {G0,W2,D1,L2,V0,M1} I { alpha30, ! c4_0 }.
% 0.72/1.25 (16) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a353 ), alpha178, ! alpha167 }.
% 0.72/1.25 (443) {G0,W2,D1,L2,V0,M1} I { alpha49, ! alpha68 }.
% 0.72/1.25 (466) {G19,W2,D1,L2,V0,M1} I;r(465) { alpha11, ! c4_0 }.
% 0.72/1.25 (468) {G0,W2,D1,L2,V0,M1} I { alpha11, ! alpha20 }.
% 0.72/1.25 (469) {G0,W2,D1,L2,V0,M1} I { alpha11, ! alpha31 }.
% 0.72/1.25 (15) {G0,W3,D1,L3,V0,M1} I { ! alpha115, alpha152, ! alpha167 }.
% 0.72/1.25 (470) {G0,W2,D1,L2,V0,M1} I { alpha50, ! alpha31 }.
% 0.72/1.25 (473) {G0,W2,D1,L2,V0,M1} I { alpha69, ! alpha50 }.
% 0.72/1.25 (476) {G0,W2,D1,L2,V0,M1} I { alpha91, ! alpha69 }.
% 0.72/1.25 (479) {G0,W2,D1,L2,V0,M1} I { alpha112, ! alpha91 }.
% 0.72/1.25 (14) {G0,W2,D1,L2,V0,M1} I { alpha167, ! alpha152 }.
% 0.72/1.25 (486) {G0,W2,D1,L2,V0,M1} I { alpha32, ! alpha20 }.
% 0.72/1.25 (489) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha32 }.
% 0.72/1.25 (492) {G0,W2,D1,L2,V0,M1} I { alpha70, ! alpha51 }.
% 0.72/1.25 (13) {G0,W2,D1,L2,V0,M1} I { alpha115, ! alpha152 }.
% 0.72/1.25 (495) {G0,W2,D1,L2,V0,M1} I { alpha92, ! alpha70 }.
% 0.72/1.25 (504) {G20,W2,D1,L2,V0,M1} I;r(503) { alpha21, alpha33 }.
% 0.72/1.25 (519) {G0,W2,D1,L2,V0,M1} I { alpha21, ! alpha34 }.
% 0.72/1.25 (12) {G1,W2,D1,L2,V0,M1} I;r(1) { alpha152, alpha96 }.
% 0.72/1.25 (522) {G0,W2,D1,L2,V0,M1} I { alpha34, ! c4_0 }.
% 0.72/1.25 (523) {G0,W2,D1,L2,V0,M1} I { alpha34, ! alpha53 }.
% 0.72/1.25 (524) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha53 }.
% 0.72/1.25 (525) {G0,W2,D1,L2,V0,M1} I { alpha94, ! alpha53 }.
% 0.72/1.25 (529) {G0,W2,D1,L2,V0,M1} I { alpha94, ! alpha113 }.
% 0.72/1.25 (534) {G0,W2,D1,L2,V0,M1} I { alpha95, ! alpha72 }.
% 0.72/1.25 (537) {G0,W2,D1,L2,V0,M1} I { alpha114, ! alpha95 }.
% 0.72/1.25 (10) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a355, a356 ), ! alpha166 }.
% 0.72/1.25 (540) {G0,W2,D1,L2,V0,M1} I { alpha134, ! alpha114 }.
% 0.72/1.25 (550) {G21,W2,D1,L2,V0,M1} I;r(547) { c2_0, ! c5_0 }.
% 0.72/1.25 (9) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a355 ), ! alpha166 }.
% 0.72/1.25 (555) {G23,W2,D1,L2,V0,M1} R(551,5) { c2_0, alpha166 }.
% 0.72/1.25 (551) {G22,W2,D1,L2,V0,M1} S(2);r(550) { c2_0, alpha151 }.
% 0.72/1.25 (61) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha97 }.
% 0.72/1.25 (62) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha117 }.
% 0.72/1.25 (64) {G2,W1,D1,L1,V0,M1} I;r(61) { alpha54 }.
% 0.72/1.25 (65) {G2,W1,D1,L1,V0,M1} I;r(61) { alpha118 }.
% 0.72/1.25 (112) {G3,W1,D1,L1,V0,M1} I;r(64) { alpha35 }.
% 0.72/1.25 (113) {G3,W1,D1,L1,V0,M1} I;r(64) { alpha74 }.
% 0.72/1.25 (7) {G0,W5,D2,L3,V0,M1} I { c5_2( a355, a356 ), alpha151, ! alpha166 }.
% 0.72/1.25 (151) {G4,W1,D1,L1,V0,M1} I;r(112) { alpha55 }.
% 0.72/1.25 (152) {G4,W1,D1,L1,V0,M1} I;r(112) { alpha75 }.
% 0.72/1.25 (158) {G5,W1,D1,L1,V0,M1} I;r(151) { alpha23 }.
% 0.72/1.25 (159) {G5,W1,D1,L1,V0,M1} I;r(151) { alpha76 }.
% 0.72/1.25 (6) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a355, a356 ), ! alpha151 }.
% 0.72/1.25 (177) {G6,W1,D1,L1,V0,M1} I;r(158) { alpha36 }.
% 0.72/1.25 (178) {G6,W1,D1,L1,V0,M1} I;r(158) { alpha56 }.
% 0.72/1.25 (180) {G7,W1,D1,L1,V0,M1} I;r(177) { alpha14 }.
% 0.72/1.25 (181) {G7,W1,D1,L1,V0,M1} I;r(177) { alpha57 }.
% 0.72/1.25 (5) {G0,W2,D1,L2,V0,M1} I { alpha166, ! alpha151 }.
% 0.72/1.25 (196) {G8,W1,D1,L1,V0,M1} I;r(180) { alpha24 }.
% 0.72/1.25 (197) {G8,W1,D1,L1,V0,M1} I;r(180) { alpha37 }.
% 0.72/1.25 (199) {G9,W1,D1,L1,V0,M1} I;r(196) { alpha8 }.
% 0.72/1.25 (200) {G9,W1,D1,L1,V0,M1} I;r(196) { alpha38 }.
% 0.72/1.25 (251) {G10,W1,D1,L1,V0,M1} I;r(199) { alpha15 }.
% 0.72/1.25 (252) {G10,W1,D1,L1,V0,M1} I;r(199) { alpha25 }.
% 0.72/1.25 (279) {G11,W1,D1,L1,V0,M1} I;r(251) { alpha26 }.
% 0.72/1.25 (280) {G11,W1,D1,L1,V0,M1} I;r(251) { alpha40 }.
% 0.72/1.25 (295) {G12,W1,D1,L1,V0,M1} I;r(279) { alpha4 }.
% 0.72/1.25 (296) {G12,W1,D1,L1,V0,M1} I;r(279) { alpha41 }.
% 0.72/1.25 (318) {G13,W1,D1,L1,V0,M1} I;r(295) { alpha9 }.
% 0.72/1.25 (319) {G13,W1,D1,L1,V0,M1} I;r(295) { alpha16 }.
% 0.72/1.25 (345) {G14,W1,D1,L1,V0,M1} I;r(318) { alpha2 }.
% 0.72/1.25 (346) {G14,W1,D1,L1,V0,M1} I;r(318) { alpha17 }.
% 0.72/1.25 (393) {G15,W1,D1,L1,V0,M1} I;r(345) { alpha5 }.
% 0.72/1.25 (395) {G16,W1,D1,L1,V0,M1} I;r(393) { alpha10 }.
% 0.72/1.25 (1) {G0,W1,D1,L1,V0,M1} I { alpha135 }.
% 0.72/1.25 (396) {G16,W1,D1,L1,V0,M1} I;r(393) { alpha18 }.
% 0.72/1.25 (422) {G17,W1,D1,L1,V0,M1} I;r(395) { alpha1 }.
% 0.72/1.25 (423) {G17,W1,D1,L1,V0,M1} I;r(395) { alpha19 }.
% 0.72/1.25 (464) {G18,W1,D1,L1,V0,M1} I;r(422) { alpha3 }.
% 0.72/1.25 (0) {G0,W1,D1,L1,V0,M1} I { alpha73 }.
% 0.72/1.25 (465) {G18,W1,D1,L1,V0,M1} I;r(422) { alpha6 }.
% 0.72/1.25 (502) {G19,W1,D1,L1,V0,M1} I;r(464) { alpha7 }.
% 0.72/1.25 (503) {G19,W1,D1,L1,V0,M1} I;r(464) { alpha12 }.
% 0.72/1.25 (547) {G20,W1,D1,L1,V0,M1} I;r(502) { alpha13 }.
% 0.72/1.25 (548) {G20,W1,D1,L1,V0,M1} I;r(502) { alpha22 }.
% 0.72/1.25
% 0.72/1.25
% 0.72/1.25 % SZS output end Saturation
% 0.72/1.25 end of saturation!
% 0.72/1.25
% 0.72/1.25 Memory use:
% 0.72/1.25
% 0.72/1.25 space for terms: 10598
% 0.72/1.25 space for clauses: 38751
% 0.72/1.25
% 0.72/1.25
% 0.72/1.25 clauses generated: 1151
% 0.72/1.25 clauses kept: 841
% 0.72/1.25 clauses selected: 800
% 0.72/1.25 clauses deleted: 89
% 0.72/1.25 clauses inuse deleted: 48
% 0.72/1.25
% 0.72/1.25 subsentry: 621
% 0.72/1.25 literals s-matched: 278
% 0.72/1.25 literals matched: 278
% 0.72/1.25 full subsumption: 0
% 0.72/1.25
% 0.72/1.25 checksum: -22123390
% 0.72/1.25
% 0.72/1.25
% 0.72/1.25 Bliksem ended
%------------------------------------------------------------------------------