%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN534+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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:40 EDT 2022
% Result : CounterSatisfiable 0.96s 1.33s
% Output : Saturation 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN534+1 : TPTP v8.1.0. Released v2.1.0.
% 0.11/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Tue Jul 12 07:34:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.42/1.12 *** allocated 10000 integers for termspace/termends
% 0.42/1.12 *** allocated 10000 integers for clauses
% 0.42/1.12 *** allocated 10000 integers for justifications
% 0.42/1.12 Bliksem 1.12
% 0.42/1.12
% 0.42/1.12
% 0.42/1.12 Automatic Strategy Selection
% 0.42/1.12
% 0.42/1.12
% 0.42/1.12 Clauses:
% 0.42/1.12
% 0.42/1.12 { alpha34 }.
% 0.42/1.12 { ! ndr1_0, c1_1( X ), ! c3_1( X ), ! ndr1_1( X ), ! c1_2( X, Y ), c5_2( X
% 0.42/1.12 , Y ), ! c3_2( X, Y ), ! c5_0, c2_0 }.
% 0.42/1.12 { ! ndr1_0, ! ndr1_1( X ), ! c2_2( X, Y ), ! c5_2( X, Y ), ! c4_2( X, Y ),
% 0.42/1.12 c4_1( X ), c1_1( X ), ! ndr1_0, c2_1( Z ), c4_0 }.
% 0.42/1.12 { c3_0, ! ndr1_0, c1_1( X ), c3_1( X ), c5_0 }.
% 0.42/1.12 { alpha45 }.
% 0.42/1.12 { c3_0, ! c5_0, ! ndr1_0, alpha68( X ), ndr1_1( X ) }.
% 0.42/1.12 { c3_0, ! c5_0, ! ndr1_0, alpha68( X ), c1_2( X, a490 ) }.
% 0.42/1.12 { c3_0, ! c5_0, ! ndr1_0, alpha68( X ), ! c3_2( X, a490 ) }.
% 0.42/1.12 { ! ndr1_0, ! c3_1( X ), c4_1( X ), ! c5_1( X ), c5_0, ! c2_0 }.
% 0.42/1.12 { alpha57 }.
% 0.42/1.12 { ! alpha68( X ), c2_1( X ), alpha83( X ) }.
% 0.42/1.12 { ! c2_1( X ), alpha68( X ) }.
% 0.42/1.12 { ! alpha83( X ), alpha68( X ) }.
% 0.42/1.12 { ! alpha83( X ), alpha93( X ) }.
% 0.42/1.12 { ! alpha83( X ), ! c2_2( X, a489 ) }.
% 0.42/1.12 { ! alpha93( X ), c2_2( X, a489 ), alpha83( X ) }.
% 0.42/1.12 { ! alpha93( X ), ndr1_1( X ) }.
% 0.42/1.12 { ! alpha93( X ), c3_2( X, a489 ) }.
% 0.42/1.12 { ! alpha93( X ), c5_2( X, a489 ) }.
% 0.42/1.12 { ! ndr1_1( X ), ! c3_2( X, a489 ), ! c5_2( X, a489 ), alpha93( X ) }.
% 0.42/1.12 { ! alpha57, alpha69, c3_0 }.
% 0.42/1.12 { ! alpha69, alpha57 }.
% 0.42/1.12 { ! c3_0, alpha57 }.
% 0.42/1.12 { ! alpha69, ndr1_0 }.
% 0.42/1.12 { ! alpha69, c3_1( a491 ) }.
% 0.42/1.12 { ! alpha69, c5_1( a491 ) }.
% 0.42/1.12 { ! ndr1_0, ! c3_1( a491 ), ! c5_1( a491 ), alpha69 }.
% 0.42/1.12 { ! alpha45, alpha58, alpha70 }.
% 0.42/1.12 { ! alpha58, alpha45 }.
% 0.42/1.12 { ! alpha70, alpha45 }.
% 0.42/1.12 { ! alpha70, alpha84 }.
% 0.42/1.12 { ! alpha70, c2_1( a488 ) }.
% 0.42/1.12 { ! alpha84, ! c2_1( a488 ), alpha70 }.
% 0.42/1.12 { ! alpha84, alpha94 }.
% 0.42/1.12 { ! alpha84, alpha103 }.
% 0.42/1.12 { ! alpha94, ! alpha103, alpha84 }.
% 0.42/1.12 { ! alpha103, ! ndr1_1( a488 ), c1_2( a488, X ), c4_2( a488, X ) }.
% 0.42/1.12 { ndr1_1( a488 ), alpha103 }.
% 0.42/1.12 { ! c1_2( a488, skol1 ), alpha103 }.
% 0.42/1.12 { ! c4_2( a488, skol1 ), alpha103 }.
% 0.42/1.12 { ! alpha94, ndr1_0 }.
% 0.42/1.12 { ! alpha94, c4_1( a488 ) }.
% 0.42/1.12 { ! ndr1_0, ! c4_1( a488 ), alpha94 }.
% 0.42/1.12 { ! alpha58, ! c5_0, alpha71 }.
% 0.42/1.12 { c5_0, alpha58 }.
% 0.42/1.12 { ! alpha71, alpha58 }.
% 0.42/1.12 { ! alpha71, alpha85 }.
% 0.42/1.12 { ! alpha71, ! c2_1( a487 ) }.
% 0.42/1.12 { ! alpha85, c2_1( a487 ), alpha71 }.
% 0.42/1.12 { ! alpha85, ndr1_0 }.
% 0.42/1.12 { ! alpha85, alpha95 }.
% 0.42/1.12 { ! ndr1_0, ! alpha95, alpha85 }.
% 0.42/1.12 { ! alpha95, ! ndr1_1( a487 ), alpha104 }.
% 0.42/1.12 { ndr1_1( a487 ), alpha95 }.
% 0.42/1.12 { ! alpha104, alpha95 }.
% 0.42/1.12 { ! alpha104, ! c2_2( a487, X ), c4_2( a487, X ), ! c5_2( a487, X ) }.
% 0.42/1.12 { c2_2( a487, skol2 ), alpha104 }.
% 0.42/1.12 { ! c4_2( a487, skol2 ), alpha104 }.
% 0.42/1.12 { c5_2( a487, skol2 ), alpha104 }.
% 0.42/1.12 { ! alpha34, alpha46 }.
% 0.42/1.12 { ! alpha34, alpha59 }.
% 0.42/1.12 { ! alpha46, ! alpha59, alpha34 }.
% 0.42/1.12 { ! alpha59, alpha72, c2_0 }.
% 0.42/1.12 { ! alpha72, alpha59 }.
% 0.42/1.12 { ! c2_0, alpha59 }.
% 0.42/1.12 { ! alpha72, alpha86, alpha96 }.
% 0.42/1.12 { ! alpha86, alpha72 }.
% 0.42/1.12 { ! alpha96, alpha72 }.
% 0.42/1.12 { ! alpha96, alpha105 }.
% 0.42/1.12 { ! alpha96, c4_1( a485 ) }.
% 0.42/1.12 { ! alpha105, ! c4_1( a485 ), alpha96 }.
% 0.42/1.12 { ! alpha105, alpha110 }.
% 0.42/1.12 { ! alpha105, c2_1( a485 ) }.
% 0.42/1.12 { ! alpha110, ! c2_1( a485 ), alpha105 }.
% 0.42/1.12 { ! alpha110, alpha115 }.
% 0.42/1.12 { ! alpha110, c5_2( a485, a486 ) }.
% 0.42/1.12 { ! alpha115, ! c5_2( a485, a486 ), alpha110 }.
% 0.42/1.12 { ! alpha115, alpha117 }.
% 0.42/1.12 { ! alpha115, c2_2( a485, a486 ) }.
% 0.42/1.12 { ! alpha117, ! c2_2( a485, a486 ), alpha115 }.
% 0.42/1.12 { ! alpha117, ndr1_0 }.
% 0.42/1.12 { ! alpha117, ndr1_1( a485 ) }.
% 0.42/1.12 { ! alpha117, c3_2( a485, a486 ) }.
% 0.42/1.12 { ! ndr1_0, ! ndr1_1( a485 ), ! c3_2( a485, a486 ), alpha117 }.
% 0.42/1.12 { ! alpha86, alpha97 }.
% 0.42/1.12 { ! alpha86, ! c1_1( a484 ) }.
% 0.42/1.12 { ! alpha97, c1_1( a484 ), alpha86 }.
% 0.42/1.12 { ! alpha97, alpha106 }.
% 0.42/1.12 { ! alpha97, ! c3_1( a484 ) }.
% 0.42/1.12 { ! alpha106, c3_1( a484 ), alpha97 }.
% 0.42/1.12 { ! alpha106, ndr1_0 }.
% 0.42/1.12 { ! alpha106, ! ndr1_1( a484 ), c4_2( a484, X ) }.
% 0.42/1.12 { ! ndr1_0, ndr1_1( a484 ), alpha106 }.
% 0.42/1.12 { ! ndr1_0, ! c4_2( a484, skol3 ), alpha106 }.
% 0.42/1.12 { ! alpha46, alpha26 }.
% 0.42/1.12 { ! alpha46, alpha60 }.
% 0.42/1.12 { ! alpha26, ! alpha60, alpha46 }.
% 0.42/1.12 { ! alpha60, alpha73, ! c2_0 }.
% 0.42/1.12 { ! alpha73, alpha60 }.
% 0.42/1.12 { c2_0, alpha60 }.
% 0.42/1.12 { ! alpha73, alpha87, c4_0 }.
% 0.42/1.12 { ! alpha87, alpha73 }.
% 0.42/1.12 { ! c4_0, alpha73 }.
% 0.42/1.12 { ! alpha87, ! ndr1_0, alpha98 }.
% 0.42/1.12 { ndr1_0, alpha87 }.
% 0.42/1.12 { ! alpha98, alpha87 }.
% 0.42/1.12 { ! alpha98, alpha107( X ), ! c2_1( X ) }.
% 0.42/1.12 { ! alpha107( skol4 ), alpha98 }.
% 0.42/1.12 { c2_1( skol4 ), alpha98 }.
% 0.42/1.12 { ! alpha107( X ), alpha111( X ) }.
% 0.42/1.12 { ! alpha107( X ), c1_2( X, a483 ) }.
% 0.42/1.12 { ! alpha111( X ), ! c1_2( X, a483 ), alpha107( X ) }.
% 0.42/1.12 { ! alpha111( X ), ndr1_1( X ) }.
% 0.42/1.12 { ! alpha111( X ), c3_2( X, a483 ) }.
% 0.42/1.12 { ! alpha111( X ), c2_2( X, a483 ) }.
% 0.42/1.12 { ! ndr1_1( X ), ! c3_2( X, a483 ), ! c2_2( X, a483 ), alpha111( X ) }.
% 0.42/1.12 { ! alpha26, alpha35 }.
% 0.42/1.12 { ! alpha26, c5_0, c1_0 }.
% 0.42/1.12 { ! alpha35, ! c5_0, alpha26 }.
% 0.42/1.12 { ! alpha35, ! c1_0, alpha26 }.
% 0.42/1.12 { ! alpha35, alpha19 }.
% 0.42/1.12 { ! alpha35, alpha47 }.
% 0.42/1.12 { ! alpha19, ! alpha47, alpha35 }.
% 0.42/1.12 { ! alpha47, alpha61, ! c3_0 }.
% 0.42/1.12 { ! alpha61, alpha47 }.
% 0.42/1.12 { c3_0, alpha47 }.
% 0.42/1.12 { ! alpha61, alpha74, alpha88 }.
% 0.42/1.12 { ! alpha74, alpha61 }.
% 0.42/1.12 { ! alpha88, alpha61 }.
% 0.42/1.12 { ! alpha88, alpha99( X ), ! c2_1( X ) }.
% 0.42/1.12 { ! alpha99( skol5 ), alpha88 }.
% 0.42/1.12 { c2_1( skol5 ), alpha88 }.
% 0.42/1.12 { ! alpha99( X ), c1_1( X ), alpha108( X ) }.
% 0.42/1.12 { ! c1_1( X ), alpha99( X ) }.
% 0.42/1.12 { ! alpha108( X ), alpha99( X ) }.
% 0.42/1.12 { ! alpha108( X ), alpha112( X ) }.
% 0.42/1.12 { ! alpha108( X ), ! c4_2( X, a482 ) }.
% 0.42/1.12 { ! alpha112( X ), c4_2( X, a482 ), alpha108( X ) }.
% 0.42/1.12 { ! alpha112( X ), ndr1_1( X ) }.
% 0.42/1.12 { ! alpha112( X ), c3_2( X, a482 ) }.
% 0.42/1.12 { ! alpha112( X ), c1_2( X, a482 ) }.
% 0.42/1.12 { ! ndr1_1( X ), ! c3_2( X, a482 ), ! c1_2( X, a482 ), alpha112( X ) }.
% 0.42/1.12 { ! alpha74, alpha89, ! ndr1_0 }.
% 0.42/1.12 { ! alpha89, alpha74 }.
% 0.42/1.12 { ndr1_0, alpha74 }.
% 0.42/1.12 { ! alpha89, ! ndr1_0, alpha100 }.
% 0.42/1.12 { ndr1_0, alpha89 }.
% 0.42/1.12 { ! alpha100, alpha89 }.
% 0.42/1.12 { ! alpha100, alpha109( X ), alpha113( X ) }.
% 0.42/1.12 { ! alpha109( skol6 ), alpha100 }.
% 0.42/1.12 { ! alpha113( skol6 ), alpha100 }.
% 0.42/1.12 { ! alpha113( X ), c1_2( X, Y ), c5_2( X, Y ), ! c4_2( X, Y ) }.
% 0.42/1.12 { ! c1_2( X, skol7( X ) ), alpha113( X ) }.
% 0.42/1.12 { ! c5_2( X, skol7( X ) ), alpha113( X ) }.
% 0.42/1.12 { c4_2( X, skol7( X ) ), alpha113( X ) }.
% 0.42/1.12 { ! alpha109( X ), alpha114( X ), ! ndr1_1( X ) }.
% 0.42/1.12 { ! alpha114( X ), alpha109( X ) }.
% 0.42/1.12 { ndr1_1( X ), alpha109( X ) }.
% 0.42/1.12 { ! alpha114( X ), alpha116( X ), c4_1( X ) }.
% 0.42/1.12 { ! alpha116( X ), alpha114( X ) }.
% 0.42/1.12 { ! c4_1( X ), alpha114( X ) }.
% 0.42/1.12 { ! alpha116( X ), ! ndr1_1( X ), alpha118( X ) }.
% 0.42/1.12 { ndr1_1( X ), alpha116( X ) }.
% 0.42/1.12 { ! alpha118( X ), alpha116( X ) }.
% 0.42/1.12 { ! alpha118( X ), ! c1_2( X, Y ), ! c4_2( X, Y ), ! c2_2( X, Y ) }.
% 0.42/1.12 { c1_2( X, skol8( X ) ), alpha118( X ) }.
% 0.42/1.12 { c4_2( X, skol8( X ) ), alpha118( X ) }.
% 0.42/1.12 { c2_2( X, skol8( X ) ), alpha118( X ) }.
% 0.42/1.12 { ! alpha19, alpha13 }.
% 0.42/1.12 { ! alpha19, alpha27 }.
% 0.42/1.12 { ! alpha13, ! alpha27, alpha19 }.
% 0.42/1.12 { ! alpha27, alpha36, alpha48 }.
% 0.42/1.12 { ! alpha36, alpha27 }.
% 0.42/1.12 { ! alpha48, alpha27 }.
% 0.42/1.12 { ! alpha48, alpha62( X ), alpha75( X ) }.
% 0.42/1.12 { ! alpha62( skol9 ), alpha48 }.
% 0.42/1.12 { ! alpha75( skol9 ), alpha48 }.
% 0.42/1.12 { ! alpha75( X ), ! c5_2( X, Y ), c2_2( X, Y ), ! c4_2( X, Y ) }.
% 0.42/1.12 { c5_2( X, skol10( X ) ), alpha75( X ) }.
% 0.42/1.12 { ! c2_2( X, skol10( X ) ), alpha75( X ) }.
% 0.42/1.12 { c4_2( X, skol10( X ) ), alpha75( X ) }.
% 0.42/1.12 { ! alpha62( X ), alpha76( X ), ! ndr1_1( X ) }.
% 0.42/1.12 { ! alpha76( X ), alpha62( X ) }.
% 0.42/1.12 { ndr1_1( X ), alpha62( X ) }.
% 0.42/1.12 { ! alpha76( X ), alpha90( X ), alpha101( X ) }.
% 0.42/1.12 { ! alpha90( X ), alpha76( X ) }.
% 0.42/1.12 { ! alpha101( X ), alpha76( X ) }.
% 0.42/1.12 { ! alpha101( X ), ! c5_2( X, Y ), ! c3_2( X, Y ), c4_2( X, Y ) }.
% 0.42/1.12 { c5_2( X, skol11( X ) ), alpha101( X ) }.
% 0.42/1.12 { c3_2( X, skol11( X ) ), alpha101( X ) }.
% 0.42/1.12 { ! c4_2( X, skol11( X ) ), alpha101( X ) }.
% 0.42/1.12 { ! alpha90( X ), c2_1( X ), ! ndr1_1( X ) }.
% 0.42/1.12 { ! c2_1( X ), alpha90( X ) }.
% 0.42/1.12 { ndr1_1( X ), alpha90( X ) }.
% 0.42/1.12 { ! alpha36, alpha49, ! ndr1_0 }.
% 0.42/1.12 { ! alpha49, alpha36 }.
% 0.42/1.12 { ndr1_0, alpha36 }.
% 0.42/1.12 { ! alpha49, alpha63, c5_0 }.
% 0.42/1.12 { ! alpha63, alpha49 }.
% 0.42/1.12 { ! c5_0, alpha49 }.
% 0.42/1.12 { ! alpha63, alpha77 }.
% 0.42/1.12 { ! alpha63, ! c5_1( a480 ) }.
% 0.42/1.12 { ! alpha77, c5_1( a480 ), alpha63 }.
% 0.42/1.12 { ! alpha77, alpha91 }.
% 0.42/1.12 { ! alpha77, c2_2( a480, a481 ) }.
% 0.42/1.12 { ! alpha91, ! c2_2( a480, a481 ), alpha77 }.
% 0.42/1.12 { ! alpha91, alpha102 }.
% 0.42/1.12 { ! alpha91, c1_2( a480, a481 ) }.
% 0.42/1.12 { ! alpha102, ! c1_2( a480, a481 ), alpha91 }.
% 0.42/1.12 { ! alpha102, ndr1_0 }.
% 0.42/1.12 { ! alpha102, ndr1_1( a480 ) }.
% 0.42/1.12 { ! alpha102, ! c4_2( a480, a481 ) }.
% 0.42/1.12 { ! ndr1_0, ! ndr1_1( a480 ), c4_2( a480, a481 ), alpha102 }.
% 0.42/1.12 { ! alpha13, alpha8 }.
% 0.42/1.12 { ! alpha13, alpha20 }.
% 0.42/1.12 { ! alpha8, ! alpha20, alpha13 }.
% 0.42/1.12 { ! alpha20, alpha28, ! c3_0 }.
% 0.42/1.12 { ! alpha28, alpha20 }.
% 0.42/1.12 { c3_0, alpha20 }.
% 0.42/1.12 { ! alpha28, c4_0, alpha37 }.
% 0.42/1.12 { ! c4_0, alpha28 }.
% 0.42/1.12 { ! alpha37, alpha28 }.
% 0.42/1.12 { ! alpha37, alpha50 }.
% 0.42/1.12 { ! alpha37, alpha64 }.
% 0.42/1.12 { ! alpha50, ! alpha64, alpha37 }.
% 0.42/1.12 { ! alpha64, ! ndr1_1( a479 ), alpha78 }.
% 0.42/1.12 { ndr1_1( a479 ), alpha64 }.
% 0.42/1.12 { ! alpha78, alpha64 }.
% 0.42/1.12 { ! alpha78, ! c1_2( a479, X ), ! c5_2( a479, X ), ! c2_2( a479, X ) }.
% 0.42/1.12 { c1_2( a479, skol12 ), alpha78 }.
% 0.42/1.12 { c5_2( a479, skol12 ), alpha78 }.
% 0.42/1.12 { c2_2( a479, skol12 ), alpha78 }.
% 0.42/1.12 { ! alpha50, ndr1_0 }.
% 0.42/1.12 { ! alpha50, c5_1( a479 ) }.
% 0.42/1.12 { ! ndr1_0, ! c5_1( a479 ), alpha50 }.
% 0.42/1.12 { ! alpha8, alpha4 }.
% 0.42/1.12 { ! alpha8, alpha14 }.
% 0.42/1.12 { ! alpha4, ! alpha14, alpha8 }.
% 0.42/1.12 { ! alpha14, alpha21, alpha29 }.
% 0.42/1.12 { ! alpha21, alpha14 }.
% 0.42/1.12 { ! alpha29, alpha14 }.
% 0.42/1.12 { ! alpha29, alpha38 }.
% 0.42/1.12 { ! alpha29, c1_1( a478 ) }.
% 0.42/1.12 { ! alpha38, ! c1_1( a478 ), alpha29 }.
% 0.42/1.12 { ! alpha38, alpha51 }.
% 0.42/1.12 { ! alpha38, alpha65 }.
% 0.42/1.12 { ! alpha51, ! alpha65, alpha38 }.
% 0.42/1.12 { ! alpha65, ! ndr1_1( a478 ), alpha79 }.
% 0.42/1.12 { ndr1_1( a478 ), alpha65 }.
% 0.42/1.12 { ! alpha79, alpha65 }.
% 0.42/1.12 { ! alpha79, ! c2_2( a478, X ), ! c1_2( a478, X ), ! c4_2( a478, X ) }.
% 0.42/1.12 { c2_2( a478, skol13 ), alpha79 }.
% 0.42/1.12 { c1_2( a478, skol13 ), alpha79 }.
% 0.42/1.12 { c4_2( a478, skol13 ), alpha79 }.
% 0.42/1.12 { ! alpha51, ndr1_0 }.
% 0.42/1.12 { ! alpha51, ! c2_1( a478 ) }.
% 0.42/1.12 { ! ndr1_0, c2_1( a478 ), alpha51 }.
% 0.42/1.12 { ! alpha21, alpha30, alpha39 }.
% 0.42/1.12 { ! alpha30, alpha21 }.
% 0.42/1.12 { ! alpha39, alpha21 }.
% 0.42/1.12 { ! alpha39, alpha52( X ), ! c2_1( X ) }.
% 0.42/1.12 { ! alpha52( skol14 ), alpha39 }.
% 0.42/1.12 { c2_1( skol14 ), alpha39 }.
% 0.42/1.12 { ! alpha52( X ), c5_1( X ), alpha66( X ) }.
% 0.42/1.12 { ! c5_1( X ), alpha52( X ) }.
% 0.42/1.12 { ! alpha66( X ), alpha52( X ) }.
% 0.42/1.12 { ! alpha66( X ), alpha80( X ) }.
% 0.42/1.12 { ! alpha66( X ), c1_2( X, a477 ) }.
% 0.42/1.12 { ! alpha80( X ), ! c1_2( X, a477 ), alpha66( X ) }.
% 0.42/1.12 { ! alpha80( X ), ndr1_1( X ) }.
% 0.42/1.12 { ! alpha80( X ), ! c2_2( X, a477 ) }.
% 0.42/1.12 { ! alpha80( X ), c5_2( X, a477 ) }.
% 0.42/1.12 { ! ndr1_1( X ), c2_2( X, a477 ), ! c5_2( X, a477 ), alpha80( X ) }.
% 0.42/1.12 { ! alpha30, alpha40, ! ndr1_0 }.
% 0.42/1.12 { ! alpha40, alpha30 }.
% 0.42/1.12 { ndr1_0, alpha30 }.
% 0.42/1.12 { ! alpha40, ! ndr1_0, alpha53 }.
% 0.42/1.12 { ndr1_0, alpha40 }.
% 0.42/1.12 { ! alpha53, alpha40 }.
% 0.42/1.12 { ! alpha53, c2_1( X ), ! c4_1( X ), ! c1_1( X ) }.
% 0.42/1.12 { ! c2_1( skol15 ), alpha53 }.
% 0.42/1.12 { c4_1( skol15 ), alpha53 }.
% 0.42/1.12 { c1_1( skol15 ), alpha53 }.
% 0.42/1.12 { ! alpha4, alpha2 }.
% 0.42/1.12 { ! alpha4, alpha9 }.
% 0.42/1.12 { ! alpha2, ! alpha9, alpha4 }.
% 0.42/1.12 { ! alpha9, alpha15, alpha22 }.
% 0.42/1.12 { ! alpha15, alpha9 }.
% 0.42/1.12 { ! alpha22, alpha9 }.
% 0.42/1.12 { ! alpha22, alpha31( X ), alpha41( X ) }.
% 0.42/1.12 { ! alpha31( skol16 ), alpha22 }.
% 0.42/1.12 { ! alpha41( skol16 ), alpha22 }.
% 0.42/1.12 { ! alpha41( X ), alpha54( X ) }.
% 0.42/1.12 { ! alpha41( X ), ! c5_2( X, a476 ) }.
% 0.42/1.12 { ! alpha54( X ), c5_2( X, a476 ), alpha41( X ) }.
% 0.42/1.12 { ! alpha54( X ), ndr1_1( X ) }.
% 0.42/1.12 { ! alpha54( X ), ! c3_2( X, a476 ) }.
% 0.42/1.12 { ! alpha54( X ), ! c1_2( X, a476 ) }.
% 0.42/1.12 { ! ndr1_1( X ), c3_2( X, a476 ), c1_2( X, a476 ), alpha54( X ) }.
% 0.42/1.12 { ! alpha31( X ), alpha42( X ), ! c3_1( X ) }.
% 0.42/1.12 { ! alpha42( X ), alpha31( X ) }.
% 0.42/1.12 { c3_1( X ), alpha31( X ) }.
% 0.42/1.12 { ! alpha42( X ), ! ndr1_1( X ), alpha55( X ) }.
% 0.42/1.12 { ndr1_1( X ), alpha42( X ) }.
% 0.42/1.12 { ! alpha55( X ), alpha42( X ) }.
% 0.42/1.12 { ! alpha55( X ), c3_2( X, Y ), ! c4_2( X, Y ), c5_2( X, Y ) }.
% 0.42/1.12 { ! c3_2( X, skol17( X ) ), alpha55( X ) }.
% 0.42/1.12 { c4_2( X, skol17( X ) ), alpha55( X ) }.
% 0.42/1.12 { ! c5_2( X, skol17( X ) ), alpha55( X ) }.
% 0.42/1.12 { ! alpha15, c4_0, ! c2_0, ! ndr1_0 }.
% 0.42/1.12 { ! c4_0, alpha15 }.
% 0.42/1.12 { c2_0, alpha15 }.
% 0.42/1.12 { ndr1_0, alpha15 }.
% 0.42/1.12 { ! alpha2, alpha5 }.
% 0.42/1.12 { ! alpha2, ! c2_0, ! c3_0 }.
% 0.42/1.12 { ! alpha5, c2_0, alpha2 }.
% 0.42/1.12 { ! alpha5, c3_0, alpha2 }.
% 0.42/1.12 { ! alpha5, alpha1 }.
% 0.42/1.12 { ! alpha5, alpha10 }.
% 0.42/1.12 { ! alpha1, ! alpha10, alpha5 }.
% 0.42/1.12 { ! alpha10, alpha16, alpha23 }.
% 0.42/1.12 { ! alpha16, alpha10 }.
% 0.42/1.12 { ! alpha23, alpha10 }.
% 0.42/1.12 { ! alpha23, alpha32 }.
% 0.42/1.12 { ! alpha23, c2_2( a474, a475 ) }.
% 0.42/1.12 { ! alpha32, ! c2_2( a474, a475 ), alpha23 }.
% 0.42/1.12 { ! alpha32, alpha43 }.
% 0.42/1.12 { ! alpha32, ! c5_2( a474, a475 ) }.
% 0.42/1.12 { ! alpha43, c5_2( a474, a475 ), alpha32 }.
% 0.42/1.12 { ! alpha43, alpha56 }.
% 0.42/1.12 { ! alpha43, ndr1_1( a474 ) }.
% 0.42/1.12 { ! alpha56, ! ndr1_1( a474 ), alpha43 }.
% 0.42/1.12 { ! alpha56, alpha67 }.
% 0.42/1.12 { ! alpha56, alpha81 }.
% 0.42/1.12 { ! alpha67, ! alpha81, alpha56 }.
% 0.42/1.12 { ! alpha81, ! ndr1_1( a474 ), alpha92 }.
% 0.42/1.12 { ndr1_1( a474 ), alpha81 }.
% 0.42/1.12 { ! alpha92, alpha81 }.
% 0.42/1.12 { ! alpha92, ! c5_2( a474, X ), c1_2( a474, X ), ! c4_2( a474, X ) }.
% 0.42/1.12 { c5_2( a474, skol18 ), alpha92 }.
% 0.42/1.12 { ! c1_2( a474, skol18 ), alpha92 }.
% 0.42/1.12 { c4_2( a474, skol18 ), alpha92 }.
% 0.42/1.12 { ! alpha67, ndr1_0 }.
% 0.42/1.12 { ! alpha67, alpha82 }.
% 0.42/1.12 { ! ndr1_0, ! alpha82, alpha67 }.
% 0.42/1.12 { ! alpha82, ! ndr1_1( a474 ), c4_2( a474, X ), ! c3_2( a474, X ) }.
% 0.42/1.12 { ndr1_1( a474 ), alpha82 }.
% 0.42/1.12 { ! c4_2( a474, skol19 ), alpha82 }.
% 0.42/1.12 { c3_2( a474, skol19 ), alpha82 }.
% 0.42/1.12 { ! alpha16, alpha24 }.
% 0.42/1.12 { ! alpha16, ! c3_2( a472, a473 ) }.
% 0.42/1.12 { ! alpha24, c3_2( a472, a473 ), alpha16 }.
% 0.42/1.12 { ! alpha24, alpha33 }.
% 0.42/1.12 { ! alpha24, ! c5_2( a472, a473 ) }.
% 0.42/1.12 { ! alpha33, c5_2( a472, a473 ), alpha24 }.
% 0.42/1.12 { ! alpha33, alpha44 }.
% 0.42/1.12 { ! alpha33, ndr1_1( a472 ) }.
% 0.42/1.12 { ! alpha44, ! ndr1_1( a472 ), alpha33 }.
% 0.42/1.12 { ! alpha44, ndr1_0 }.
% 0.42/1.12 { ! alpha44, ! c1_1( a472 ) }.
% 0.42/1.12 { ! alpha44, c5_1( a472 ) }.
% 0.42/1.12 { ! ndr1_0, c1_1( a472 ), ! c5_1( a472 ), alpha44 }.
% 0.42/1.12 { ! alpha1, alpha3 }.
% 0.42/1.12 { ! alpha1, alpha6 }.
% 0.42/1.12 { ! alpha3, ! alpha6, alpha1 }.
% 0.42/1.12 { ! alpha6, c3_0, c1_0, ! c5_0 }.
% 0.42/1.12 { ! c3_0, alpha6 }.
% 0.42/1.12 { ! c1_0, alpha6 }.
% 0.42/1.12 { c5_0, alpha6 }.
% 0.42/1.12 { ! alpha3, alpha7 }.
% 0.42/1.12 { ! alpha3, alpha11 }.
% 0.42/1.12 { ! alpha7, ! alpha11, alpha3 }.
% 0.42/1.12 { ! alpha11, alpha17, c1_0 }.
% 0.42/1.12 { ! alpha17, alpha11 }.
% 0.42/1.12 { ! c1_0, alpha11 }.
% 0.42/1.12 { ! alpha17, alpha25, c3_1( X ), c5_1( X ) }.
% 0.42/1.12 { ! alpha25, alpha17 }.
% 0.42/1.12 { ! c3_1( skol20 ), alpha17 }.
% 0.42/1.12 { ! c5_1( skol20 ), alpha17 }.
% 0.42/1.12 { ! alpha25, ! c3_0, ! ndr1_0 }.
% 0.42/1.12 { c3_0, alpha25 }.
% 0.42/1.12 { ndr1_0, alpha25 }.
% 0.42/1.12 { ! alpha7, alpha12, ! c1_0 }.
% 0.42/1.12 { ! alpha12, alpha7 }.
% 0.42/1.12 { c1_0, alpha7 }.
% 0.42/1.12 { ! alpha12, c2_0, alpha18 }.
% 0.42/1.12 { ! c2_0, alpha12 }.
% 0.42/1.12 { ! alpha18, alpha12 }.
% 0.42/1.12 { ! alpha18, ndr1_0 }.
% 0.42/1.12 { ! alpha18, ! c2_1( a471 ) }.
% 0.42/1.12 { ! alpha18, ! c4_1( a471 ) }.
% 0.42/1.12 { ! ndr1_0, c2_1( a471 ), c4_1( a471 ), alpha18 }.
% 0.42/1.12
% 0.42/1.12 *** allocated 15000 integers for clauses
% 0.42/1.12 percentage equality = 0.000000, percentage horn = 0.720930
% 0.42/1.12 This a non-horn, non-equality problem
% 0.42/1.12
% 0.42/1.12
% 0.42/1.12 Options Used:
% 0.42/1.12
% 0.42/1.12 useres = 1
% 0.42/1.12 useparamod = 0
% 0.42/1.12 useeqrefl = 0
% 0.42/1.12 useeqfact = 0
% 0.42/1.12 usefactor = 1
% 0.42/1.12 usesimpsplitting = 0
% 0.42/1.12 usesimpdemod = 0
% 0.42/1.12 usesimpres = 3
% 0.42/1.12
% 0.42/1.12 resimpinuse = 1000
% 0.42/1.12 resimpclauses = 20000
% 0.42/1.12 substype = standard
% 0.42/1.12 backwardsubs = 1
% 0.42/1.12 selectoldest = 5
% 0.42/1.12
% 0.42/1.12 litorderings [0] = split
% 0.42/1.12 litorderings [1] = liftord
% 0.42/1.12
% 0.42/1.12 termordering = none
% 0.42/1.12
% 0.42/1.12 litapriori = 1
% 0.42/1.12 termapriori = 0
% 0.42/1.12 litaposteriori = 0
% 0.42/1.12 termaposteriori = 0
% 0.42/1.12 demodaposteriori = 0
% 0.42/1.12 ordereqreflfact = 0
% 0.42/1.12
% 0.42/1.12 litselect = none
% 0.42/1.12
% 0.42/1.12 maxweight = 15
% 0.42/1.12 maxdepth = 30000
% 0.42/1.12 maxlength = 115
% 0.42/1.12 maxnrvars = 195
% 0.42/1.12 excuselevel = 1
% 0.42/1.12 increasemaxweight = 1
% 0.42/1.12
% 0.42/1.12 maxselected = 10000000
% 0.42/1.12 maxnrclauses = 10000000
% 0.42/1.12
% 0.42/1.12 showgenerated = 0
% 0.42/1.12 showkept = 0
% 0.42/1.12 showselected = 0
% 0.42/1.12 showdeleted = 0
% 0.42/1.12 showresimp = 1
% 0.42/1.12 showstatus = 2000
% 0.42/1.12
% 0.42/1.12 prologoutput = 0
% 0.42/1.12 nrgoals = 5000000
% 0.42/1.12 totalproof = 1
% 0.42/1.12
% 0.42/1.12 Symbols occurring in the translation:
% 0.42/1.12
% 0.42/1.12 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.42/1.12 . [1, 2] (w:1, o:210, a:1, s:1, b:0),
% 0.42/1.12 ! [4, 1] (w:0, o:168, a:1, s:1, b:0),
% 0.42/1.12 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.42/1.12 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.42/1.12 c2_0 [35, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.42/1.12 ndr1_0 [36, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.42/1.12 a471 [37, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.42/1.12 c2_1 [38, 1] (w:1, o:174, a:1, s:1, b:0),
% 0.42/1.12 c4_1 [39, 1] (w:1, o:176, a:1, s:1, b:0),
% 0.42/1.12 c1_0 [40, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.42/1.12 c3_0 [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.42/1.12 c3_1 [43, 1] (w:1, o:175, a:1, s:1, b:0),
% 0.42/1.12 c5_1 [44, 1] (w:1, o:177, a:1, s:1, b:0),
% 0.42/1.12 c5_0 [45, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.42/1.12 a472 [46, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.42/1.12 c1_1 [47, 1] (w:1, o:173, a:1, s:1, b:0),
% 0.42/1.12 ndr1_1 [48, 1] (w:1, o:178, a:1, s:1, b:0),
% 0.42/1.12 a473 [49, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.42/1.12 c5_2 [50, 2] (w:1, o:235, a:1, s:1, b:0),
% 0.42/1.12 c3_2 [51, 2] (w:1, o:237, a:1, s:1, b:0),
% 0.42/1.12 a474 [53, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.42/1.12 c4_2 [54, 2] (w:1, o:234, a:1, s:1, b:0),
% 0.42/1.12 c1_2 [56, 2] (w:1, o:238, a:1, s:1, b:0),
% 0.42/1.12 a475 [57, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.42/1.12 c2_2 [58, 2] (w:1, o:236, a:1, s:1, b:0),
% 0.42/1.12 c4_0 [59, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.42/1.12 a476 [62, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.42/1.12 a477 [65, 0] (w:1, o:46, a:1, s:1, b:0),
% 0.42/1.12 a478 [66, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.42/1.12 a479 [68, 0] (w:1, o:48, a:1, s:1, b:0),
% 0.42/1.12 a480 [70, 0] (w:1, o:49, a:1, s:1, b:0),
% 0.42/1.12 a481 [71, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.42/1.12 a482 [79, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.42/1.16 a483 [81, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.42/1.16 a484 [83, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.42/1.16 a485 [84, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.42/1.16 a486 [85, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.42/1.16 a487 [93, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.42/1.16 a488 [94, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.42/1.16 a489 [97, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.42/1.16 a490 [98, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.42/1.16 a491 [100, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.42/1.16 alpha1 [101, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.42/1.16 alpha2 [102, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.42/1.16 alpha3 [103, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.42/1.16 alpha4 [104, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.42/1.16 alpha5 [105, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.42/1.16 alpha6 [106, 0] (w:1, o:119, a:1, s:1, b:0),
% 0.42/1.16 alpha7 [107, 0] (w:1, o:127, a:1, s:1, b:0),
% 0.42/1.16 alpha8 [108, 0] (w:1, o:136, a:1, s:1, b:0),
% 0.42/1.16 alpha9 [109, 0] (w:1, o:145, a:1, s:1, b:0),
% 0.42/1.16 alpha10 [110, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.42/1.16 alpha11 [111, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.42/1.16 alpha12 [112, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.42/1.16 alpha13 [113, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.42/1.16 alpha14 [114, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.42/1.16 alpha15 [115, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.42/1.16 alpha16 [116, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.42/1.16 alpha17 [117, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.42/1.16 alpha18 [118, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.42/1.16 alpha19 [119, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.42/1.16 alpha20 [120, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.42/1.16 alpha21 [121, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.42/1.16 alpha22 [122, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.42/1.16 alpha23 [123, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.42/1.16 alpha24 [124, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.42/1.16 alpha25 [125, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.42/1.16 alpha26 [126, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.42/1.16 alpha27 [127, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.42/1.16 alpha28 [128, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.42/1.16 alpha29 [129, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.42/1.16 alpha30 [130, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.42/1.16 alpha31 [131, 1] (w:1, o:179, a:1, s:1, b:0),
% 0.42/1.16 alpha32 [132, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.42/1.16 alpha33 [133, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.42/1.16 alpha34 [134, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.42/1.16 alpha35 [135, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.42/1.16 alpha36 [136, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.42/1.16 alpha37 [137, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.42/1.16 alpha38 [138, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.42/1.16 alpha39 [139, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.42/1.16 alpha40 [140, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.42/1.16 alpha41 [141, 1] (w:1, o:180, a:1, s:1, b:0),
% 0.42/1.16 alpha42 [142, 1] (w:1, o:181, a:1, s:1, b:0),
% 0.42/1.16 alpha43 [143, 0] (w:1, o:104, a:1, s:1, b:0),
% 0.42/1.16 alpha44 [144, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.42/1.16 alpha45 [145, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.42/1.16 alpha46 [146, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.42/1.16 alpha47 [147, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.42/1.16 alpha48 [148, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.42/1.16 alpha49 [149, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.42/1.16 alpha50 [150, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.42/1.16 alpha51 [151, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.42/1.16 alpha52 [152, 1] (w:1, o:182, a:1, s:1, b:0),
% 0.42/1.16 alpha53 [153, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.42/1.16 alpha54 [154, 1] (w:1, o:183, a:1, s:1, b:0),
% 0.42/1.16 alpha55 [155, 1] (w:1, o:184, a:1, s:1, b:0),
% 0.42/1.16 alpha56 [156, 0] (w:1, o:115, a:1, s:1, b:0),
% 0.42/1.16 alpha57 [157, 0] (w:1, o:116, a:1, s:1, b:0),
% 0.42/1.16 alpha58 [158, 0] (w:1, o:117, a:1, s:1, b:0),
% 0.42/1.16 alpha59 [159, 0] (w:1, o:118, a:1, s:1, b:0),
% 0.42/1.16 alpha60 [160, 0] (w:1, o:120, a:1, s:1, b:0),
% 0.42/1.16 alpha61 [161, 0] (w:1, o:121, a:1, s:1, b:0),
% 0.42/1.16 alpha62 [162, 1] (w:1, o:185, a:1, s:1, b:0),
% 0.42/1.16 alpha63 [163, 0] (w:1, o:122, a:1, s:1, b:0),
% 0.42/1.16 alpha64 [164, 0] (w:1, o:123, a:1, s:1, b:0),
% 0.42/1.16 alpha65 [165, 0] (w:1, o:124, a:1, s:1, b:0),
% 0.42/1.16 alpha66 [166, 1] (w:1, o:186, a:1, s:1, b:0),
% 0.42/1.16 alpha67 [167, 0] (w:1, o:125, a:1, s:1, b:0),
% 0.42/1.16 alpha68 [168, 1] (w:1, o:187, a:1, s:1, b:0),
% 0.42/1.16 alpha69 [169, 0] (w:1, o:126, a:1, s:1, b:0),
% 0.42/1.16 alpha70 [170, 0] (w:1, o:128, a:1, s:1, b:0),
% 0.96/1.32 alpha71 [171, 0] (w:1, o:129, a:1, s:1, b:0),
% 0.96/1.32 alpha72 [172, 0] (w:1, o:130, a:1, s:1, b:0),
% 0.96/1.32 alpha73 [173, 0] (w:1, o:131, a:1, s:1, b:0),
% 0.96/1.32 alpha74 [174, 0] (w:1, o:132, a:1, s:1, b:0),
% 0.96/1.32 alpha75 [175, 1] (w:1, o:188, a:1, s:1, b:0),
% 0.96/1.32 alpha76 [176, 1] (w:1, o:189, a:1, s:1, b:0),
% 0.96/1.32 alpha77 [177, 0] (w:1, o:133, a:1, s:1, b:0),
% 0.96/1.32 alpha78 [178, 0] (w:1, o:134, a:1, s:1, b:0),
% 0.96/1.32 alpha79 [179, 0] (w:1, o:135, a:1, s:1, b:0),
% 0.96/1.32 alpha80 [180, 1] (w:1, o:190, a:1, s:1, b:0),
% 0.96/1.32 alpha81 [181, 0] (w:1, o:137, a:1, s:1, b:0),
% 0.96/1.32 alpha82 [182, 0] (w:1, o:138, a:1, s:1, b:0),
% 0.96/1.32 alpha83 [183, 1] (w:1, o:191, a:1, s:1, b:0),
% 0.96/1.32 alpha84 [184, 0] (w:1, o:139, a:1, s:1, b:0),
% 0.96/1.32 alpha85 [185, 0] (w:1, o:140, a:1, s:1, b:0),
% 0.96/1.32 alpha86 [186, 0] (w:1, o:141, a:1, s:1, b:0),
% 0.96/1.32 alpha87 [187, 0] (w:1, o:142, a:1, s:1, b:0),
% 0.96/1.32 alpha88 [188, 0] (w:1, o:143, a:1, s:1, b:0),
% 0.96/1.32 alpha89 [189, 0] (w:1, o:144, a:1, s:1, b:0),
% 0.96/1.32 alpha90 [190, 1] (w:1, o:192, a:1, s:1, b:0),
% 0.96/1.32 alpha91 [191, 0] (w:1, o:146, a:1, s:1, b:0),
% 0.96/1.32 alpha92 [192, 0] (w:1, o:147, a:1, s:1, b:0),
% 0.96/1.32 alpha93 [193, 1] (w:1, o:193, a:1, s:1, b:0),
% 0.96/1.32 alpha94 [194, 0] (w:1, o:148, a:1, s:1, b:0),
% 0.96/1.32 alpha95 [195, 0] (w:1, o:149, a:1, s:1, b:0),
% 0.96/1.32 alpha96 [196, 0] (w:1, o:150, a:1, s:1, b:0),
% 0.96/1.32 alpha97 [197, 0] (w:1, o:151, a:1, s:1, b:0),
% 0.96/1.32 alpha98 [198, 0] (w:1, o:152, a:1, s:1, b:0),
% 0.96/1.32 alpha99 [199, 1] (w:1, o:194, a:1, s:1, b:0),
% 0.96/1.32 alpha100 [200, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.96/1.32 alpha101 [201, 1] (w:1, o:195, a:1, s:1, b:0),
% 0.96/1.32 alpha102 [202, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.96/1.32 alpha103 [203, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.96/1.32 alpha104 [204, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.96/1.32 alpha105 [205, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.96/1.32 alpha106 [206, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.96/1.32 alpha107 [207, 1] (w:1, o:196, a:1, s:1, b:0),
% 0.96/1.32 alpha108 [208, 1] (w:1, o:197, a:1, s:1, b:0),
% 0.96/1.32 alpha109 [209, 1] (w:1, o:198, a:1, s:1, b:0),
% 0.96/1.32 alpha110 [210, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.96/1.32 alpha111 [211, 1] (w:1, o:199, a:1, s:1, b:0),
% 0.96/1.32 alpha112 [212, 1] (w:1, o:200, a:1, s:1, b:0),
% 0.96/1.32 alpha113 [213, 1] (w:1, o:201, a:1, s:1, b:0),
% 0.96/1.32 alpha114 [214, 1] (w:1, o:202, a:1, s:1, b:0),
% 0.96/1.32 alpha115 [215, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.96/1.32 alpha116 [216, 1] (w:1, o:203, a:1, s:1, b:0),
% 0.96/1.32 alpha117 [217, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.96/1.32 alpha118 [218, 1] (w:1, o:204, a:1, s:1, b:0),
% 0.96/1.32 skol1 [219, 0] (w:1, o:153, a:1, s:1, b:0),
% 0.96/1.32 skol2 [220, 0] (w:1, o:161, a:1, s:1, b:0),
% 0.96/1.32 skol3 [221, 0] (w:1, o:163, a:1, s:1, b:0),
% 0.96/1.32 skol4 [222, 0] (w:1, o:164, a:1, s:1, b:0),
% 0.96/1.32 skol5 [223, 0] (w:1, o:165, a:1, s:1, b:0),
% 0.96/1.32 skol6 [224, 0] (w:1, o:166, a:1, s:1, b:0),
% 0.96/1.32 skol7 [225, 1] (w:1, o:205, a:1, s:1, b:0),
% 0.96/1.32 skol8 [226, 1] (w:1, o:206, a:1, s:1, b:0),
% 0.96/1.32 skol9 [227, 0] (w:1, o:167, a:1, s:1, b:0),
% 0.96/1.32 skol10 [228, 1] (w:1, o:207, a:1, s:1, b:0),
% 0.96/1.32 skol11 [229, 1] (w:1, o:208, a:1, s:1, b:0),
% 0.96/1.32 skol12 [230, 0] (w:1, o:154, a:1, s:1, b:0),
% 0.96/1.32 skol13 [231, 0] (w:1, o:155, a:1, s:1, b:0),
% 0.96/1.32 skol14 [232, 0] (w:1, o:156, a:1, s:1, b:0),
% 0.96/1.32 skol15 [233, 0] (w:1, o:157, a:1, s:1, b:0),
% 0.96/1.32 skol16 [234, 0] (w:1, o:158, a:1, s:1, b:0),
% 0.96/1.32 skol17 [235, 1] (w:1, o:209, a:1, s:1, b:0),
% 0.96/1.32 skol18 [236, 0] (w:1, o:159, a:1, s:1, b:0),
% 0.96/1.32 skol19 [237, 0] (w:1, o:160, a:1, s:1, b:0),
% 0.96/1.32 skol20 [238, 0] (w:1, o:162, a:1, s:1, b:0).
% 0.96/1.32
% 0.96/1.32
% 0.96/1.32 Starting Search:
% 0.96/1.32
% 0.96/1.32 *** allocated 22500 integers for clauses
% 0.96/1.32 *** allocated 33750 integers for clauses
% 0.96/1.32 Resimplifying inuse:
% 0.96/1.32 Done
% 0.96/1.32
% 0.96/1.32 Resimplifying inuse:
% 0.96/1.32 Done
% 0.96/1.32
% 0.96/1.32 Failed to find proof!
% 0.96/1.32 maxweight = 15
% 0.96/1.32 maxnrclauses = 10000000
% 0.96/1.32 Generated: 805
% 0.96/1.32 Kept: 580
% 0.96/1.32
% 0.96/1.32
% 0.96/1.32 The strategy used was not complete!
% 0.96/1.32
% 0.96/1.32 Increased maxweight to 16
% 0.96/1.32
% 0.96/1.32 Starting Search:
% 0.96/1.32
% 0.96/1.32 Resimplifying inuse:
% 0.96/1.32 Done
% 0.96/1.32
% 0.96/1.32 Resimplifying inuse:
% 0.96/1.32 Done
% 0.96/1.32
% 0.96/1.32 Failed to find proof!
% 0.96/1.32 maxweight = 16
% 0.96/1.32 maxnrclauses = 10000000
% 0.96/1.32 Generated: 805
% 0.96/1.32 Kept: 580
% 0.96/1.32
% 0.96/1.32
% 0.96/1.32 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 17
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Failed to find proof!
% 0.96/1.33 maxweight = 17
% 0.96/1.33 maxnrclauses = 10000000
% 0.96/1.33 Generated: 875
% 0.96/1.33 Kept: 616
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 18
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Failed to find proof!
% 0.96/1.33 maxweight = 18
% 0.96/1.33 maxnrclauses = 10000000
% 0.96/1.33 Generated: 1076
% 0.96/1.33 Kept: 689
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 19
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Failed to find proof!
% 0.96/1.33 maxweight = 19
% 0.96/1.33 maxnrclauses = 10000000
% 0.96/1.33 Generated: 1077
% 0.96/1.33 Kept: 690
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 20
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Failed to find proof!
% 0.96/1.33 maxweight = 20
% 0.96/1.33 maxnrclauses = 10000000
% 0.96/1.33 Generated: 1081
% 0.96/1.33 Kept: 692
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 21
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Failed to find proof!
% 0.96/1.33 maxweight = 21
% 0.96/1.33 maxnrclauses = 10000000
% 0.96/1.33 Generated: 1098
% 0.96/1.33 Kept: 695
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 The strategy used was not complete!
% 0.96/1.33
% 0.96/1.33 Increased maxweight to 22
% 0.96/1.33
% 0.96/1.33 Starting Search:
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33 Resimplifying inuse:
% 0.96/1.33 Done
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 found a saturation!
% 0.96/1.33 % SZS status CounterSatisfiable
% 0.96/1.33 % SZS output start Saturation
% 0.96/1.33
% 0.96/1.33 (694) {G20,W17,D2,L8,V2,M1} S(1);r(362) { c1_1( X ), ! c3_1( X ), ! ndr1_1
% 0.96/1.33 ( X ), c5_2( X, Y ), ! c3_2( X, Y ), c2_0, ! c1_2( X, Y ), ! c5_0 }.
% 0.96/1.33 (692) {G20,W7,D2,L4,V1,M1} S(6);r(362) { c3_0, alpha68( X ), c1_2( X, a490
% 0.96/1.33 ), ! c5_0 }.
% 0.96/1.33 (691) {G20,W7,D2,L4,V1,M1} S(7);r(362) { c3_0, alpha68( X ), ! c3_2( X,
% 0.96/1.33 a490 ), ! c5_0 }.
% 0.96/1.33 (693) {G20,W6,D2,L4,V1,M1} S(5);r(362) { c3_0, ndr1_1( X ), alpha68( X ), !
% 0.96/1.33 c5_0 }.
% 0.96/1.33 (687) {G24,W21,D2,L11,V2,M1} R(665,520);f;f;f { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! ndr1_1( X ), ! alpha113( X ), ! alpha55( X ), c4_1( X ), c2_1( Y )
% 0.96/1.33 , c4_0, alpha80( X ), ! c4_2( X, a477 ) }.
% 0.96/1.33 (690) {G25,W19,D2,L11,V1,M1} R(686,496);f { c1_0, c1_1( a480 ), ! c3_1(
% 0.96/1.33 a480 ), ! ndr1_1( a480 ), ! alpha55( a480 ), c4_1( a480 ), c2_1( X ),
% 0.96/1.33 c4_0, ! alpha75( a480 ), alpha102, ! alpha113( a480 ) }.
% 0.96/1.33 (686) {G24,W21,D2,L11,V3,M1} R(665,522);f;f;f { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! ndr1_1( X ), ! alpha113( X ), ! alpha55( X ), c4_1( X ), c2_1( Z )
% 0.96/1.33 , c4_0, ! alpha75( X ), ! c4_2( X, Y ) }.
% 0.96/1.33 (684) {G24,W17,D2,L9,V0,M1} R(665,571);f;r(412) { c1_0, c1_1( a474 ), !
% 0.96/1.33 c3_1( a474 ), ! alpha113( a474 ), ! alpha55( a474 ), alpha16, ! alpha118
% 0.96/1.33 ( a474 ), alpha80( a474 ), ! c4_2( a474, a477 ) }.
% 0.96/1.33 (685) {G24,W17,D2,L9,V1,M1} R(665,572);f;r(412) { c1_0, c1_1( a474 ), !
% 0.96/1.33 c3_1( a474 ), ! alpha113( a474 ), ! alpha55( a474 ), alpha16, ! alpha118
% 0.96/1.33 ( a474 ), ! alpha75( a474 ), ! c4_2( a474, X ) }.
% 0.96/1.33 (689) {G25,W15,D2,L9,V1,M1} R(667,512);f { c1_0, c1_1( a474 ), ! c3_1( a474
% 0.96/1.33 ), ! alpha111( a474 ), c4_1( a474 ), c2_1( X ), c4_0, alpha16, !
% 0.96/1.33 alpha113( a474 ) }.
% 0.96/1.33 (667) {G24,W17,D2,L9,V2,M1} R(666,526);f;f;f { c1_0, c1_1( X ), ! c3_1( X )
% 0.96/1.33 , ! alpha113( X ), ! alpha111( X ), c4_1( X ), c2_1( Y ), c4_0, ! c4_2( X
% 0.96/1.33 , a483 ) }.
% 0.96/1.33 (671) {G25,W16,D2,L9,V2,M1} R(619,122);f { c1_0, c1_1( X ), ! c3_1( X ),
% 0.96/1.33 c4_1( X ), c2_1( Y ), c4_0, ! alpha75( X ), alpha108( X ), ! alpha112( X
% 0.96/1.33 ) }.
% 0.96/1.33 (688) {G24,W13,D2,L7,V0,M1} R(665,443);r(412) { c1_0, c1_1( a474 ), ! c3_1
% 0.96/1.33 ( a474 ), ! alpha113( a474 ), ! alpha55( a474 ), alpha16, ! c4_2( a474,
% 0.96/1.33 a475 ) }.
% 0.96/1.33 (665) {G23,W17,D2,L8,V2,M1} R(611,278);f;f { c1_0, c1_1( X ), ! c3_1( X ),
% 0.96/1.33 ! ndr1_1( X ), ! alpha113( X ), ! c4_2( X, Y ), ! alpha55( X ), c5_2( X,
% 0.96/1.33 Y ) }.
% 0.96/1.33 (669) {G25,W16,D2,L9,V2,M1} R(619,621);f;f;f;f { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), c4_1( X ), c2_1( Y ), c4_0, ! alpha75( X ), ! alpha101( X ), !
% 0.96/1.33 alpha112( X ) }.
% 0.96/1.33 (683) {G30,W11,D2,L7,V1,M1} R(682,272);f { c1_0, c4_0, c1_1( skol6 ),
% 0.96/1.33 alpha100, c2_1( X ), ! c3_1( skol6 ), ! alpha31( skol6 ) }.
% 0.96/1.33 (682) {G29,W11,D2,L7,V1,M1} R(681,275);r(437) { c1_0, c4_0, c1_1( skol6 ),
% 0.96/1.33 c2_1( X ), alpha100, ! c3_1( skol6 ), ! alpha42( skol6 ) }.
% 0.96/1.33 (681) {G28,W11,D2,L7,V1,M1} R(680,134) { c1_0, c4_0, c1_1( skol6 ), c2_1( X
% 0.96/1.33 ), ! c3_1( skol6 ), alpha100, ! alpha55( skol6 ) }.
% 0.96/1.33 (657) {G23,W17,D2,L10,V1,M1} R(600,431);f;r(418) { ! ndr1_1( a484 ),
% 0.96/1.33 alpha112( a484 ), ! alpha55( a484 ), c4_1( a484 ), c2_1( X ), c4_0, !
% 0.96/1.33 alpha75( a484 ), c2_0, alpha105, ! alpha113( a484 ) }.
% 0.96/1.33 (680) {G27,W12,D2,L7,V2,M1} R(679,141) { c1_0, c1_1( X ), c4_0, c2_1( Y ),
% 0.96/1.33 ! c3_1( X ), ! alpha55( X ), alpha109( X ) }.
% 0.96/1.33 (679) {G26,W12,D2,L7,V2,M1} R(678,144);r(145) { c1_0, c1_1( X ), c2_1( Y )
% 0.96/1.33 , c4_0, ! c3_1( X ), ! alpha55( X ), alpha114( X ) }.
% 0.96/1.33 (678) {G25,W14,D2,L8,V2,M1} R(676,148);r(147) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), c4_1( X ), c2_1( Y ), c4_0, ! alpha55( X ), alpha116( X ) }.
% 0.96/1.33 (676) {G24,W16,D2,L9,V2,M1} R(660,523);f;f;f { c1_0, c1_1( X ), ! c3_1( X )
% 0.96/1.33 , ! ndr1_1( X ), ! alpha55( X ), c4_1( X ), c2_1( Y ), c4_0, alpha118( X
% 0.96/1.33 ) }.
% 0.96/1.33 (652) {G24,W19,D2,L10,V2,M1} R(616,522);f;f;r(426) { c1_0, c1_1( X ), !
% 0.96/1.33 c3_1( X ), ! alpha55( X ), ! alpha66( X ), c4_1( X ), c2_1( Y ), c4_0, !
% 0.96/1.33 alpha75( X ), ! c4_2( X, a477 ) }.
% 0.96/1.33 (660) {G23,W15,D3,L7,V1,M1} R(610,278);f;r(151) { c1_0, c1_1( X ), ! c3_1(
% 0.96/1.33 X ), ! ndr1_1( X ), alpha118( X ), ! alpha55( X ), c5_2( X, skol8( X ) )
% 0.96/1.33 }.
% 0.96/1.33 (675) {G24,W13,D2,L8,V1,M1} S(645);r(268) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 ! alpha54( a484 ), c2_0, alpha105, ! alpha55( a484 ), ! alpha75( a484 )
% 0.96/1.33 }.
% 0.96/1.33 (674) {G24,W13,D2,L8,V1,M1} S(640);r(268) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 ! alpha54( a484 ), c2_0, alpha105, ! alpha75( a484 ), ! alpha113( a484 )
% 0.96/1.33 }.
% 0.96/1.33 (673) {G26,W15,D2,L9,V1,M1} R(672,272);f { c1_0, alpha79, c1_1( a478 ), !
% 0.96/1.33 c3_1( a478 ), c2_1( X ), c4_0, c4_1( a478 ), ! ndr1_1( a478 ), ! alpha31
% 0.96/1.33 ( a478 ) }.
% 0.96/1.33 (672) {G25,W15,D2,L9,V1,M1} R(647,275);f { c1_0, c1_1( a478 ), alpha79, !
% 0.96/1.33 c3_1( a478 ), c4_1( a478 ), c2_1( X ), c4_0, ! ndr1_1( a478 ), ! alpha42
% 0.96/1.33 ( a478 ) }.
% 0.96/1.33 (647) {G24,W15,D2,L9,V1,M1} R(646,525);f;f;f { c1_0, c1_1( a478 ), ! c3_1(
% 0.96/1.33 a478 ), alpha79, ! ndr1_1( a478 ), c4_1( a478 ), c2_1( X ), c4_0, !
% 0.96/1.33 alpha55( a478 ) }.
% 0.96/1.33 (670) {G25,W15,D2,L9,V1,M1} R(619,511);f { c1_0, c1_1( a474 ), ! c3_1( a474
% 0.96/1.33 ), c4_1( a474 ), c2_1( X ), c4_0, ! alpha75( a474 ), alpha16, ! alpha112
% 0.96/1.33 ( a474 ) }.
% 0.96/1.33 (619) {G24,W17,D2,L9,V2,M1} R(617,522);f;r(123) { c1_0, c1_1( X ), ! c3_1(
% 0.96/1.33 X ), ! alpha112( X ), c4_1( X ), c2_1( Y ), c4_0, ! alpha75( X ), ! c4_2
% 0.96/1.33 ( X, a482 ) }.
% 0.96/1.33 (668) {G24,W13,D2,L8,V1,M1} S(649);r(268) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 alpha41( a484 ), c2_0, alpha105, ! alpha54( a484 ), ! alpha75( a484 ) }.
% 0.96/1.33 (666) {G23,W15,D2,L7,V1,M1} R(611,103);r(102) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha113( X ), ! c4_2( X, a483 ), ! alpha111( X ), c5_2( X, a483 )
% 0.96/1.33 }.
% 0.96/1.33 (664) {G27,W13,D2,L8,V1,M1} R(663,458) { c4_0, c2_0, alpha105, c2_1( X ),
% 0.96/1.33 c4_1( a484 ), ! alpha111( a484 ), ! alpha109( a484 ), ! alpha113( a484 )
% 0.96/1.33 }.
% 0.96/1.33 (611) {G22,W18,D2,L8,V2,M1} R(533,136);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 ndr1_1( X ), c5_2( X, Y ), ! alpha113( X ), ! c4_2( X, Y ), ! c3_2( X, Y
% 0.96/1.33 ) }.
% 0.96/1.33 (663) {G26,W13,D2,L8,V1,M1} R(662,143);f { c4_0, c2_1( X ), c2_0, alpha105
% 0.96/1.33 , c4_1( a484 ), ! alpha111( a484 ), ! alpha113( a484 ), ! alpha114( a484
% 0.96/1.33 ) }.
% 0.96/1.33 (662) {G25,W13,D2,L8,V1,M1} R(661,146);r(102) { c4_0, c2_1( X ), c4_1( a484
% 0.96/1.33 ), c2_0, alpha105, ! alpha111( a484 ), ! alpha113( a484 ), ! alpha116(
% 0.96/1.33 a484 ) }.
% 0.96/1.33 (661) {G24,W13,D2,L8,V1,M1} S(651);r(102) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 ! alpha111( a484 ), c2_0, alpha105, ! alpha113( a484 ), ! alpha118( a484
% 0.96/1.33 ) }.
% 0.96/1.33 (610) {G22,W17,D3,L7,V1,M1} R(533,150) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 ndr1_1( X ), c5_2( X, skol8( X ) ), alpha118( X ), ! c3_2( X, skol8( X )
% 0.96/1.33 ) }.
% 0.96/1.33 (659) {G24,W13,D2,L8,V1,M1} S(655);r(102) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 alpha107( a484 ), c2_0, alpha105, ! alpha111( a484 ), ! alpha113( a484 )
% 0.96/1.33 }.
% 0.96/1.33 (658) {G28,W15,D2,L8,V1,M1} R(642,458) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha75( X ), ! alpha101( X ), c4_1( X ), ! alpha109( X ), ! alpha112( X
% 0.96/1.33 ) }.
% 0.96/1.33 (642) {G27,W15,D2,L8,V1,M1} R(641,143) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha75( X ), ! alpha101( X ), ! alpha112( X ), c4_1( X ), ! alpha114( X
% 0.96/1.33 ) }.
% 0.96/1.33 (600) {G22,W20,D2,L10,V2,M1} R(537,522);f;f { ! ndr1_1( X ), ! alpha113( X
% 0.96/1.33 ), alpha112( X ), ! alpha55( X ), c4_1( X ), c1_1( X ), c2_1( Y ), c4_0
% 0.96/1.33 , ! alpha75( X ), ! c4_2( X, a482 ) }.
% 0.96/1.33 (656) {G28,W15,D2,L8,V1,M1} R(644,458) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha75( X ), alpha108( X ), c4_1( X ), ! alpha109( X ), ! alpha112( X )
% 0.96/1.33 }.
% 0.96/1.33 (644) {G27,W15,D2,L8,V1,M1} R(643,143) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha75( X ), alpha108( X ), ! alpha112( X ), c4_1( X ), ! alpha114( X )
% 0.96/1.33 }.
% 0.96/1.33 (604) {G24,W15,D2,L8,V2,M1} R(603,166) { c1_1( X ), c4_0, c2_1( Y ), c4_1(
% 0.96/1.33 X ), ! alpha75( X ), ! alpha76( X ), alpha90( X ), ! alpha93( X ) }.
% 0.96/1.33 (653) {G25,W14,D2,L8,V2,M1} R(630,631);f;f;f;f { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), c4_1( X ), c2_1( Y ), c4_0, ! alpha101( X ), ! alpha107( X ) }.
% 0.96/1.33 (598) {G22,W16,D2,L8,V2,M1} R(526,456);f;f { c4_1( X ), c1_1( X ), c2_1( Y
% 0.96/1.33 ), c4_0, ! alpha111( X ), ! alpha113( X ), alpha107( X ), ! c4_2( X,
% 0.96/1.33 a483 ) }.
% 0.96/1.33 (654) {G25,W13,D2,L8,V1,M1} R(630,512);r(99) { c1_0, c1_1( a474 ), ! c3_1(
% 0.96/1.33 a474 ), c4_1( a474 ), c2_1( X ), c4_0, alpha16, ! alpha107( a474 ) }.
% 0.96/1.33 (630) {G24,W15,D2,L8,V2,M1} R(629,526);f;r(99) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha107( X ), c4_1( X ), c2_1( Y ), c4_0, ! c4_2( X, a483 ) }.
% 0.96/1.33 (635) {G24,W15,D2,L8,V2,M1} R(609,166) { c1_1( X ), c4_0, c2_1( Y ), c4_1(
% 0.96/1.33 X ), alpha83( X ), ! alpha76( X ), alpha90( X ), ! alpha93( X ) }.
% 0.96/1.33 (616) {G23,W15,D2,L7,V1,M1} R(612,278);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha66( X ), ! alpha55( X ), ! c4_2( X, a477 ), c5_2( X, a477 ) }.
% 0.96/1.33 (597) {G22,W16,D2,L8,V2,M1} R(526,549);f;f { c4_1( X ), c1_1( X ), c2_1( Y
% 0.96/1.33 ), c4_0, ! alpha111( X ), ! alpha118( X ), ! alpha113( X ), ! c4_2( X,
% 0.96/1.33 a483 ) }.
% 0.96/1.33 (650) {G29,W14,D2,L9,V1,M1} R(623,166);r(175) { c1_1( a485 ), c2_1( X ),
% 0.96/1.33 c4_0, c2_0, c3_0, c5_0, c4_1( a485 ), ! alpha76( a485 ), alpha90( a485 )
% 0.96/1.33 }.
% 0.96/1.33 (623) {G28,W14,D2,L9,V1,M1} R(578,562);f;f;f { c4_1( a485 ), c1_1( a485 ),
% 0.96/1.33 c2_1( X ), c4_0, c2_0, c3_0, c5_0, ! ndr1_1( a485 ), ! alpha101( a485 )
% 0.96/1.33 }.
% 0.96/1.33 (648) {G27,W14,D2,L8,V0,M1} R(627,458) { c1_0, alpha16, c1_1( a474 ), !
% 0.96/1.33 c3_1( a474 ), ! alpha75( a474 ), c4_1( a474 ), ! alpha109( a474 ), !
% 0.96/1.33 alpha112( a474 ) }.
% 0.96/1.33 (587) {G22,W16,D2,L8,V2,M1} R(522,267);r(268) { c4_1( X ), c1_1( X ), c2_1
% 0.96/1.33 ( Y ), c4_0, ! alpha75( X ), ! alpha54( X ), alpha41( X ), ! c4_2( X,
% 0.96/1.33 a476 ) }.
% 0.96/1.33 (627) {G26,W14,D2,L8,V0,M1} R(626,143) { c1_0, alpha16, c1_1( a474 ), !
% 0.96/1.33 c3_1( a474 ), ! alpha75( a474 ), ! alpha112( a474 ), c4_1( a474 ), !
% 0.96/1.33 alpha114( a474 ) }.
% 0.96/1.33 (599) {G20,W14,D2,L7,V0,M1} R(537,572);f;r(412) { ! alpha113( a474 ),
% 0.96/1.33 alpha112( a474 ), ! alpha55( a474 ), alpha16, ! alpha118( a474 ), !
% 0.96/1.33 alpha75( a474 ), ! c4_2( a474, a482 ) }.
% 0.96/1.33 (646) {G23,W13,D2,L7,V0,M1} R(614,278);f;r(229) { c1_0, c1_1( a478 ), !
% 0.96/1.33 c3_1( a478 ), ! ndr1_1( a478 ), alpha79, ! alpha55( a478 ), c5_2( a478,
% 0.96/1.33 skol13 ) }.
% 0.96/1.33 (614) {G22,W14,D2,L7,V0,M1} R(533,228) { c1_0, c1_1( a478 ), ! c3_1( a478 )
% 0.96/1.33 , ! ndr1_1( a478 ), c5_2( a478, skol13 ), alpha79, ! c3_2( a478, skol13 )
% 0.96/1.33 }.
% 0.96/1.33 (586) {G22,W16,D2,L8,V2,M1} R(522,508);f;r(268) { c4_1( X ), c1_1( X ),
% 0.96/1.33 c2_1( Y ), c4_0, ! alpha75( X ), ! alpha55( X ), ! alpha54( X ), ! c4_2(
% 0.96/1.33 X, a476 ) }.
% 0.96/1.33 (643) {G26,W13,D2,L7,V1,M1} R(639,146);r(123) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha75( X ), alpha108( X ), ! alpha112( X ), ! alpha116( X ) }.
% 0.96/1.33 (639) {G25,W13,D2,L7,V1,M1} R(620,122);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha75( X ), ! alpha112( X ), alpha108( X ), ! alpha118( X ) }.
% 0.96/1.33 (641) {G26,W13,D2,L7,V1,M1} R(638,146);r(123) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha75( X ), ! alpha101( X ), ! alpha112( X ), ! alpha116( X ) }.
% 0.96/1.33 (638) {G25,W13,D2,L7,V1,M1} R(620,621);f;f;f;f { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha75( X ), ! alpha112( X ), ! alpha101( X ), ! alpha118( X ) }.
% 0.96/1.33 (585) {G22,W16,D2,L8,V2,M1} R(522,455);f;r(268) { c4_1( X ), c1_1( X ),
% 0.96/1.33 c2_1( Y ), c4_0, ! alpha75( X ), ! alpha113( X ), ! alpha54( X ), ! c4_2
% 0.96/1.33 ( X, a476 ) }.
% 0.96/1.33 (620) {G24,W14,D2,L7,V1,M1} R(617,557);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha112( X ), ! alpha75( X ), ! alpha118( X ), ! c4_2( X, a482 ) }.
% 0.96/1.33 (637) {G24,W11,D2,L7,V1,M1} S(608);r(16) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 c2_0, alpha105, alpha83( a484 ), ! alpha93( a484 ) }.
% 0.96/1.33 (636) {G28,W13,D2,L7,V1,M1} R(634,458) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha101( X ), c4_1( X ), ! alpha107( X ), ! alpha109( X ) }.
% 0.96/1.33 (634) {G27,W13,D2,L7,V1,M1} R(633,143) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha101( X ), ! alpha107( X ), c4_1( X ), ! alpha114( X ) }.
% 0.96/1.33 (609) {G23,W13,D2,L7,V2,M1} R(605,492);f { c1_1( X ), c2_1( Y ), c4_0, c4_1
% 0.96/1.33 ( X ), alpha83( X ), ! alpha93( X ), ! alpha101( X ) }.
% 0.96/1.33 (633) {G26,W11,D2,L6,V1,M1} R(632,146);r(442) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), ! alpha101( X ), ! alpha107( X ), ! alpha116( X ) }.
% 0.96/1.33 (632) {G25,W11,D2,L6,V1,M1} R(631,559);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha101( X ), ! alpha107( X ), ! alpha118( X ) }.
% 0.96/1.33 (583) {G22,W17,D2,L9,V1,M1} R(522,507);f;f { ! ndr1_1( a485 ), c4_1( a485 )
% 0.96/1.33 , c1_1( a485 ), c2_1( X ), c4_0, ! alpha75( a485 ), ! alpha55( a485 ),
% 0.96/1.33 alpha117, ! c4_2( a485, a486 ) }.
% 0.96/1.33 (631) {G24,W12,D2,L6,V1,M1} R(629,490);r(99) { c1_0, c1_1( X ), ! c3_1( X )
% 0.96/1.33 , ! alpha101( X ), ! alpha107( X ), c4_2( X, a483 ) }.
% 0.96/1.33 (629) {G23,W10,D2,L5,V1,M1} R(615,103);r(99) { c1_0, c1_1( X ), ! c3_1( X )
% 0.96/1.33 , ! alpha107( X ), c5_2( X, a483 ) }.
% 0.96/1.33 (626) {G25,W12,D2,L7,V0,M1} R(618,146);r(123) { c1_0, c1_1( a474 ), alpha16
% 0.96/1.33 , ! c3_1( a474 ), ! alpha75( a474 ), ! alpha112( a474 ), ! alpha116( a474
% 0.96/1.33 ) }.
% 0.96/1.33 (618) {G24,W12,D2,L7,V0,M1} R(617,572);r(511) { c1_0, c1_1( a474 ), ! c3_1
% 0.96/1.33 ( a474 ), alpha16, ! alpha112( a474 ), ! alpha75( a474 ), ! alpha118(
% 0.96/1.33 a474 ) }.
% 0.96/1.33 (625) {G27,W11,D2,L6,V1,M1} R(624,166) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha76( X ), alpha90( X ), ! alpha99( X ) }.
% 0.96/1.33 (624) {G26,W9,D2,L5,V1,M1} R(622,117);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha99( X ), ! alpha101( X ) }.
% 0.96/1.33 (622) {G25,W9,D2,L5,V1,M1} R(621,121);r(120) { c1_0, c1_1( X ), ! c3_1( X )
% 0.96/1.33 , ! alpha101( X ), ! alpha108( X ) }.
% 0.96/1.33 (578) {G26,W15,D2,L9,V1,M1} R(521,474);f;f;f { ! ndr1_1( a485 ), c4_1( a485
% 0.96/1.33 ), c1_1( a485 ), c2_1( X ), c4_0, c2_0, c3_0, c5_0, ! c4_2( a485, a486 )
% 0.96/1.33 }.
% 0.96/1.33 (621) {G24,W12,D2,L6,V1,M1} R(617,489);f { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha101( X ), ! alpha112( X ), c4_2( X, a482 ) }.
% 0.96/1.33 (617) {G23,W10,D2,L5,V1,M1} S(613);r(124) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 alpha112( X ), c5_2( X, a482 ) }.
% 0.96/1.33 (612) {G22,W13,D2,L6,V1,M1} R(533,243);r(426) { c1_0, c1_1( X ), ! c3_1( X
% 0.96/1.33 ), c5_2( X, a477 ), ! alpha66( X ), ! c3_2( X, a477 ) }.
% 0.96/1.33 (533) {G21,W16,D2,L7,V2,M1} S(377);r(387) { c1_0, c1_1( X ), ! c3_1( X ), !
% 0.96/1.33 ndr1_1( X ), c5_2( X, Y ), ! c3_2( X, Y ), ! c1_2( X, Y ) }.
% 0.96/1.33 (607) {G23,W12,D2,L7,V1,M1} R(605,513);f { c1_1( a474 ), c2_1( X ), c4_0,
% 0.96/1.33 c4_1( a474 ), alpha83( a474 ), alpha16, ! alpha93( a474 ) }.
% 0.96/1.33 (605) {G22,W14,D2,L7,V2,M1} S(527);r(18) { c4_1( X ), c1_1( X ), c2_1( Y )
% 0.96/1.33 , c4_0, ! alpha93( X ), alpha83( X ), ! c4_2( X, a489 ) }.
% 0.96/1.33 (606) {G24,W11,D2,L7,V1,M1} S(602);r(16) { c4_0, c2_1( X ), c4_1( a484 ),
% 0.96/1.33 c2_0, alpha105, ! alpha75( a484 ), ! alpha93( a484 ) }.
% 0.96/1.33 (603) {G23,W13,D2,L7,V2,M1} R(589,492);f { c1_1( X ), c2_1( Y ), c4_0, c4_1
% 0.96/1.33 ( X ), ! alpha75( X ), ! alpha93( X ), ! alpha101( X ) }.
% 0.96/1.33 (601) {G23,W12,D2,L7,V1,M1} R(589,513);f { c1_1( a474 ), c2_1( X ), c4_0,
% 0.96/1.33 c4_1( a474 ), ! alpha75( a474 ), alpha16, ! alpha93( a474 ) }.
% 0.96/1.33 (589) {G22,W14,D2,L7,V2,M1} R(522,18);r(16) { c4_1( X ), c1_1( X ), c2_1( Y
% 0.96/1.33 ), c4_0, ! alpha75( X ), ! alpha93( X ), ! c4_2( X, a489 ) }.
% 0.96/1.33 (537) {G2,W14,D2,L6,V1,M1} R(454,278);f;f { ! alpha113( X ), ! ndr1_1( X )
% 0.96/1.33 , ! c4_2( X, a482 ), alpha112( X ), ! alpha55( X ), c5_2( X, a482 ) }.
% 0.96/1.33 (526) {G21,W15,D2,L7,V2,M1} R(365,104);r(102) { ! c4_2( X, a483 ), c4_1( X
% 0.96/1.33 ), c1_1( X ), c2_1( Y ), c4_0, ! alpha111( X ), ! c5_2( X, a483 ) }.
% 0.96/1.33 (525) {G21,W13,D2,L7,V1,M1} R(365,227);r(229) { ! ndr1_1( a478 ), c4_1(
% 0.96/1.33 a478 ), c1_1( a478 ), c2_1( X ), c4_0, alpha79, ! c5_2( a478, skol13 )
% 0.96/1.33 }.
% 0.96/1.33 (596) {G23,W11,D2,L7,V1,M1} R(588,453);r(165) { c1_1( a474 ), c2_1( X ),
% 0.96/1.33 c4_0, alpha92, c4_1( a474 ), alpha36, alpha62( a474 ) }.
% 0.96/1.33 (588) {G22,W12,D2,L7,V1,M1} R(522,307);r(309) { c4_1( a474 ), c1_1( a474 )
% 0.96/1.33 , c2_1( X ), c4_0, ! ndr1_1( a474 ), alpha92, ! alpha75( a474 ) }.
% 0.96/1.33 (571) {G19,W11,D2,L5,V0,M1} R(529,248);f;r(412) { alpha16, ! alpha118( a474
% 0.96/1.33 ), ! c4_2( a474, a477 ), alpha80( a474 ), ! c5_2( a474, a477 ) }.
% 0.96/1.33 (524) {G21,W13,D2,L7,V1,M1} R(365,210);r(209) { ! ndr1_1( a479 ), c4_1(
% 0.96/1.33 a479 ), c1_1( a479 ), c2_1( X ), c4_0, alpha78, ! c4_2( a479, skol12 )
% 0.96/1.33 }.
% 0.96/1.33 (595) {G23,W9,D2,L5,V0,M1} R(594,458) { alpha16, ! alpha75( a474 ), c4_1(
% 0.96/1.33 a474 ), ! alpha93( a474 ), ! alpha109( a474 ) }.
% 0.96/1.33 (594) {G22,W9,D2,L5,V0,M1} R(593,143) { alpha16, ! alpha75( a474 ), !
% 0.96/1.33 alpha93( a474 ), c4_1( a474 ), ! alpha114( a474 ) }.
% 0.96/1.33 (593) {G21,W7,D2,L4,V0,M1} R(592,146);r(16) { alpha16, ! alpha75( a474 ), !
% 0.96/1.33 alpha93( a474 ), ! alpha116( a474 ) }.
% 0.96/1.33 (592) {G20,W7,D2,L4,V0,M1} R(572,18);r(513) { alpha16, ! alpha75( a474 ), !
% 0.96/1.33 alpha93( a474 ), ! alpha118( a474 ) }.
% 0.96/1.33 (523) {G21,W15,D3,L7,V2,M1} R(365,152);r(151) { ! ndr1_1( X ), c4_1( X ),
% 0.96/1.33 c1_1( X ), c2_1( Y ), c4_0, alpha118( X ), ! c5_2( X, skol8( X ) ) }.
% 0.96/1.33 (572) {G19,W11,D2,L5,V1,M1} R(529,159);f;f { alpha16, ! alpha118( a474 ), !
% 0.96/1.33 c4_2( a474, X ), ! alpha75( a474 ), ! c5_2( a474, X ) }.
% 0.96/1.33 (591) {G23,W9,D2,L5,V0,M1} R(590,458) { alpha16, alpha83( a474 ), c4_1(
% 0.96/1.33 a474 ), ! alpha93( a474 ), ! alpha109( a474 ) }.
% 0.96/1.33 (590) {G22,W9,D2,L5,V0,M1} R(581,143) { alpha16, alpha83( a474 ), ! alpha93
% 0.96/1.33 ( a474 ), c4_1( a474 ), ! alpha114( a474 ) }.
% 0.96/1.33 (581) {G21,W7,D2,L4,V0,M1} R(580,146);r(16) { alpha16, alpha83( a474 ), !
% 0.96/1.33 alpha93( a474 ), ! alpha116( a474 ) }.
% 0.96/1.33 (522) {G21,W17,D2,L8,V3,M1} R(365,159);f;f { ! ndr1_1( X ), ! c4_2( X, Y )
% 0.96/1.33 , c4_1( X ), c1_1( X ), c2_1( Z ), c4_0, ! alpha75( X ), ! c5_2( X, Y )
% 0.96/1.33 }.
% 0.96/1.33 (580) {G20,W7,D2,L4,V0,M1} S(574);r(18) { alpha16, ! alpha93( a474 ),
% 0.96/1.33 alpha83( a474 ), ! alpha118( a474 ) }.
% 0.96/1.33 (579) {G23,W9,D2,L5,V0,M1} R(577,458) { alpha16, ! alpha111( a474 ), c4_1(
% 0.96/1.33 a474 ), ! alpha109( a474 ), ! alpha113( a474 ) }.
% 0.96/1.33 (577) {G22,W9,D2,L5,V0,M1} R(576,143) { alpha16, ! alpha111( a474 ), !
% 0.96/1.33 alpha113( a474 ), c4_1( a474 ), ! alpha114( a474 ) }.
% 0.96/1.33 (576) {G21,W7,D2,L4,V0,M1} R(575,146);r(102) { alpha16, ! alpha111( a474 )
% 0.96/1.33 , ! alpha113( a474 ), ! alpha116( a474 ) }.
% 0.96/1.33 (575) {G20,W7,D2,L4,V0,M1} R(573,549);f;f;r(512) { alpha16, ! alpha111(
% 0.96/1.33 a474 ), ! alpha113( a474 ), ! alpha118( a474 ) }.
% 0.96/1.33 (573) {G19,W8,D2,L4,V0,M1} R(529,104);r(512) { alpha16, ! alpha118( a474 )
% 0.96/1.33 , ! alpha111( a474 ), ! c5_2( a474, a483 ) }.
% 0.96/1.33 (529) {G18,W12,D2,L5,V1,M1} R(516,149);f { ! c4_2( a474, X ), alpha16, !
% 0.96/1.33 alpha118( a474 ), ! c5_2( a474, X ), ! c2_2( a474, X ) }.
% 0.96/1.33 (520) {G21,W17,D2,L8,V2,M1} R(365,248);f;f { ! ndr1_1( X ), ! c4_2( X, a477
% 0.96/1.33 ), c4_1( X ), c1_1( X ), c2_1( Y ), c4_0, alpha80( X ), ! c5_2( X, a477
% 0.96/1.33 ) }.
% 0.96/1.33 (549) {G2,W12,D2,L5,V1,M1} R(461,104) { ! alpha118( X ), ! alpha113( X ), !
% 0.96/1.33 c4_2( X, a483 ), ! alpha111( X ), c5_2( X, a483 ) }.
% 0.96/1.33 (570) {G3,W9,D2,L4,V1,M1} R(553,247);r(242) { ! alpha66( X ), ! alpha75( X
% 0.96/1.33 ), ! alpha118( X ), ! c4_2( X, a477 ) }.
% 0.96/1.33 (557) {G2,W12,D2,L5,V1,M1} R(463,159);f { ! alpha118( X ), ! alpha112( X )
% 0.96/1.33 , ! alpha75( X ), ! c4_2( X, a482 ), ! c5_2( X, a482 ) }.
% 0.96/1.33 (509) {G1,W15,D2,L6,V1,M1} R(278,105) { ! alpha55( X ), ! c4_2( X, a483 ),
% 0.96/1.33 ! ndr1_1( X ), c5_2( X, a483 ), alpha111( X ), ! c2_2( X, a483 ) }.
% 0.96/1.33 (569) {G19,W9,D2,L4,V0,M1} S(530);r(412) { alpha16, alpha112( a474 ), !
% 0.96/1.33 c5_2( a474, a482 ), ! c3_2( a474, a482 ) }.
% 0.96/1.33 (562) {G27,W8,D2,L5,V0,M1} R(488,474);f;f;f { ! alpha101( a485 ), c2_0,
% 0.96/1.33 c3_0, c5_0, c4_2( a485, a486 ) }.
% 0.96/1.33 (507) {G21,W11,D2,L5,V0,M1} R(278,425) { ! alpha55( a485 ), ! c4_2( a485,
% 0.96/1.33 a486 ), ! ndr1_1( a485 ), alpha117, c5_2( a485, a486 ) }.
% 0.96/1.33 (568) {G11,W8,D2,L5,V0,M1} R(566,458) { c2_0, alpha105, c4_1( a484 ), !
% 0.96/1.33 alpha107( a484 ), ! alpha109( a484 ) }.
% 0.96/1.33 (566) {G10,W8,D2,L5,V0,M1} R(565,143) { c2_0, alpha105, ! alpha107( a484 )
% 0.96/1.33 , c4_1( a484 ), ! alpha114( a484 ) }.
% 0.96/1.33 (567) {G22,W7,D2,L4,V0,M1} R(564,458) { alpha16, c4_1( a474 ), ! alpha107(
% 0.96/1.33 a474 ), ! alpha109( a474 ) }.
% 0.96/1.33 (564) {G21,W7,D2,L4,V0,M1} R(563,143) { alpha16, ! alpha107( a474 ), c4_1(
% 0.96/1.33 a474 ), ! alpha114( a474 ) }.
% 0.96/1.33 (504) {G1,W15,D2,L6,V1,M1} R(271,149) { ! ndr1_1( X ), alpha54( X ), !
% 0.96/1.33 alpha118( X ), ! c4_2( X, a476 ), ! c2_2( X, a476 ), c3_2( X, a476 ) }.
% 0.96/1.33 (565) {G9,W6,D2,L4,V0,M1} R(561,146);r(442) { c2_0, alpha105, ! alpha107(
% 0.96/1.33 a484 ), ! alpha116( a484 ) }.
% 0.96/1.33 (561) {G8,W6,D2,L4,V0,M1} R(559,431);r(442) { ! alpha107( a484 ), c2_0,
% 0.96/1.33 alpha105, ! alpha118( a484 ) }.
% 0.96/1.33 (563) {G20,W5,D2,L3,V0,M1} R(560,146);r(442) { alpha16, ! alpha107( a474 )
% 0.96/1.33 , ! alpha116( a474 ) }.
% 0.96/1.33 (560) {G19,W5,D2,L3,V0,M1} R(559,512);r(99) { ! alpha107( a474 ), alpha16,
% 0.96/1.33 ! alpha118( a474 ) }.
% 0.96/1.33 (559) {G2,W7,D2,L3,V1,M1} R(466,104);r(99) { ! alpha118( X ), ! alpha107( X
% 0.96/1.33 ), ! c4_2( X, a483 ) }.
% 0.96/1.33 (552) {G9,W8,D2,L5,V0,M1} R(546,10) { c2_0, alpha105, c2_1( a484 ), !
% 0.96/1.33 alpha68( a484 ), ! alpha75( a484 ) }.
% 0.96/1.33 (548) {G14,W8,D2,L4,V0,M1} R(461,444);r(443) { ! alpha118( a474 ), !
% 0.96/1.33 alpha113( a474 ), alpha16, ! c4_2( a474, a475 ) }.
% 0.96/1.33 (463) {G1,W10,D2,L4,V1,M1} R(149,125) { ! alpha118( X ), ! c4_2( X, a482 )
% 0.96/1.33 , ! alpha112( X ), ! c2_2( X, a482 ) }.
% 0.96/1.33 (556) {G7,W8,D2,L4,V1,M1} R(555,459) { c2_1( X ), ! alpha68( X ), ! alpha62
% 0.96/1.33 ( X ), ! alpha75( X ) }.
% 0.96/1.33 (555) {G6,W8,D2,L4,V1,M1} R(554,10);f { ! alpha75( X ), c2_1( X ), !
% 0.96/1.33 alpha68( X ), ! alpha76( X ) }.
% 0.96/1.33 (554) {G5,W8,D2,L4,V1,M1} R(551,173);r(366) { ! alpha75( X ), ! alpha76( X
% 0.96/1.33 ), c2_1( X ), ! alpha83( X ) }.
% 0.96/1.33 (551) {G4,W8,D2,L4,V1,M1} R(547,166) { ! alpha75( X ), ! alpha76( X ), !
% 0.96/1.33 alpha83( X ), alpha90( X ) }.
% 0.96/1.33 (462) {G1,W10,D2,L4,V1,M1} R(149,243) { ! alpha118( X ), ! c4_2( X, a477 )
% 0.96/1.33 , ! alpha66( X ), ! c2_2( X, a477 ) }.
% 0.96/1.33 (550) {G20,W7,D2,L4,V0,M1} R(545,10) { alpha16, c2_1( a474 ), ! alpha68(
% 0.96/1.33 a474 ), ! alpha75( a474 ) }.
% 0.96/1.33 (546) {G8,W6,D2,L4,V0,M1} R(544,431);r(366) { ! alpha75( a484 ), c2_0,
% 0.96/1.33 alpha105, ! alpha83( a484 ) }.
% 0.96/1.33 (547) {G3,W6,D2,L3,V1,M1} R(544,492);r(13) { ! alpha75( X ), ! alpha83( X )
% 0.96/1.33 , ! alpha101( X ) }.
% 0.96/1.33 (545) {G19,W5,D2,L3,V0,M1} R(544,513);r(13) { ! alpha75( a474 ), alpha16, !
% 0.96/1.33 alpha83( a474 ) }.
% 0.96/1.33 (461) {G1,W13,D2,L5,V2,M1} R(149,136);f { ! alpha118( X ), ! c4_2( X, Y ),
% 0.96/1.33 ! alpha113( X ), c5_2( X, Y ), ! c2_2( X, Y ) }.
% 0.96/1.33 (544) {G2,W7,D2,L3,V1,M1} R(484,18);r(13) { ! alpha75( X ), ! alpha83( X )
% 0.96/1.33 , ! c4_2( X, a489 ) }.
% 0.96/1.33 (490) {G1,W10,D2,L4,V1,M1} R(169,103) { ! alpha101( X ), c4_2( X, a483 ), !
% 0.96/1.33 alpha111( X ), ! c5_2( X, a483 ) }.
% 0.96/1.33 (543) {G20,W7,D2,L4,V0,M1} R(456,532);f;f;r(512) { ! alpha111( a474 ),
% 0.96/1.33 alpha107( a474 ), alpha16, ! alpha113( a474 ) }.
% 0.96/1.33 (456) {G1,W12,D2,L5,V1,M1} R(136,101) { ! alpha113( X ), ! c4_2( X, a483 )
% 0.96/1.33 , ! alpha111( X ), alpha107( X ), c5_2( X, a483 ) }.
% 0.96/1.33 (489) {G1,W10,D2,L4,V1,M1} R(169,124) { ! alpha101( X ), c4_2( X, a482 ), !
% 0.96/1.33 alpha112( X ), ! c5_2( X, a482 ) }.
% 0.96/1.33 (540) {G19,W8,D2,L4,V0,M1} R(455,531);f;f { ! alpha113( a474 ), ! alpha54(
% 0.96/1.33 a474 ), alpha16, ! c4_2( a474, a476 ) }.
% 0.96/1.33 (542) {G8,W6,D2,L4,V0,M1} R(541,431);r(424) { ! alpha41( a484 ), c2_0,
% 0.96/1.33 alpha105, ! alpha113( a484 ) }.
% 0.96/1.33 (541) {G2,W7,D2,L3,V1,M1} R(455,266);r(265) { ! alpha113( X ), ! alpha41( X
% 0.96/1.33 ), ! c4_2( X, a476 ) }.
% 0.96/1.33 (455) {G1,W10,D2,L4,V1,M1} R(136,270) { ! alpha113( X ), ! c4_2( X, a476 )
% 0.96/1.33 , ! alpha54( X ), c5_2( X, a476 ) }.
% 0.96/1.33 (535) {G19,W8,D2,L4,V0,M1} R(508,531);f;f { ! alpha55( a474 ), ! alpha54(
% 0.96/1.33 a474 ), alpha16, ! c4_2( a474, a476 ) }.
% 0.96/1.33 (539) {G9,W6,D2,L4,V0,M1} R(538,275);r(424) { c2_0, alpha105, ! alpha41(
% 0.96/1.33 a484 ), ! alpha42( a484 ) }.
% 0.96/1.33 (538) {G8,W6,D2,L4,V0,M1} R(536,431);r(424) { ! alpha41( a484 ), c2_0,
% 0.96/1.33 alpha105, ! alpha55( a484 ) }.
% 0.96/1.33 (536) {G2,W7,D2,L3,V1,M1} R(508,266);r(265) { ! alpha55( X ), ! alpha41( X
% 0.96/1.33 ), ! c4_2( X, a476 ) }.
% 0.96/1.33 (454) {G1,W15,D2,L6,V1,M1} R(136,126) { ! alpha113( X ), ! c4_2( X, a482 )
% 0.96/1.33 , ! ndr1_1( X ), c5_2( X, a482 ), alpha112( X ), ! c3_2( X, a482 ) }.
% 0.96/1.33 (508) {G1,W10,D2,L4,V1,M1} R(278,269) { ! alpha55( X ), ! c4_2( X, a476 ),
% 0.96/1.33 ! alpha54( X ), c5_2( X, a476 ) }.
% 0.96/1.33 (534) {G19,W8,D2,L4,V0,M1} R(531,267);f { alpha16, ! alpha54( a474 ),
% 0.96/1.33 alpha41( a474 ), ! c4_2( a474, a476 ) }.
% 0.96/1.33 (531) {G18,W9,D2,L4,V0,M1} R(516,270) { ! c4_2( a474, a476 ), alpha16, !
% 0.96/1.33 alpha54( a474 ), ! c5_2( a474, a476 ) }.
% 0.96/1.33 (532) {G19,W8,D2,L4,V0,M1} R(516,101);r(512) { alpha16, ! alpha111( a474 )
% 0.96/1.33 , alpha107( a474 ), ! c5_2( a474, a483 ) }.
% 0.96/1.33 (528) {G18,W8,D2,L4,V0,M1} R(516,244);r(247) { alpha16, ! alpha80( a474 ),
% 0.96/1.33 alpha66( a474 ), ! c4_2( a474, a477 ) }.
% 0.96/1.33 (516) {G17,W10,D2,L4,V1,M1} R(306,447) { ! c5_2( a474, X ), ! c4_2( a474, X
% 0.96/1.33 ), alpha16, c1_2( a474, X ) }.
% 0.96/1.33 (519) {G21,W7,D2,L5,V0,M1} R(518,445) { alpha16, c1_1( a474 ), alpha74,
% 0.96/1.33 c1_0, ! c2_1( a474 ) }.
% 0.96/1.33 (513) {G18,W6,D2,L3,V0,M1} R(506,17) { alpha16, ! alpha93( a474 ), c4_2(
% 0.96/1.33 a474, a489 ) }.
% 0.96/1.33 (365) {G20,W18,D2,L8,V3,M1} R(362,2) { ! ndr1_1( X ), ! c5_2( X, Y ), !
% 0.96/1.33 c4_2( X, Y ), c4_1( X ), c1_1( X ), c2_1( Z ), c4_0, ! c2_2( X, Y ) }.
% 0.96/1.33 (512) {G18,W6,D2,L3,V0,M1} R(506,103) { alpha16, ! alpha111( a474 ), c4_2(
% 0.96/1.33 a474, a483 ) }.
% 0.96/1.33 (518) {G20,W5,D2,L3,V0,M1} R(517,117) { alpha16, c1_1( a474 ), ! alpha99(
% 0.96/1.33 a474 ) }.
% 0.96/1.33 (517) {G19,W3,D2,L2,V0,M1} R(511,121);r(120) { alpha16, ! alpha108( a474 )
% 0.96/1.33 }.
% 0.96/1.33 (511) {G18,W6,D2,L3,V0,M1} R(506,124) { alpha16, ! alpha112( a474 ), c4_2(
% 0.96/1.33 a474, a482 ) }.
% 0.96/1.33 (306) {G0,W10,D2,L4,V1,M1} I { ! c5_2( a474, X ), c1_2( a474, X ), ! c4_2(
% 0.96/1.33 a474, X ), ! alpha92 }.
% 0.96/1.33 (515) {G20,W3,D2,L2,V0,M1} R(514,164) { alpha16, alpha62( a474 ) }.
% 0.96/1.33 (514) {G19,W3,D2,L2,V0,M1} R(510,168) { alpha16, alpha76( a474 ) }.
% 0.96/1.33 (510) {G18,W3,D2,L2,V0,M1} R(506,171);r(172) { alpha16, alpha101( a474 )
% 0.96/1.33 }.
% 0.96/1.33 (506) {G17,W7,D2,L3,V1,M1} R(313,359);r(412) { c4_2( a474, X ), alpha16, !
% 0.96/1.33 c3_2( a474, X ) }.
% 0.96/1.33 (278) {G0,W11,D2,L4,V2,M1} I { ! alpha55( X ), ! c4_2( X, Y ), c5_2( X, Y )
% 0.96/1.33 , c3_2( X, Y ) }.
% 0.96/1.33 (313) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a474 ), c4_2( a474, X ), ! c3_2(
% 0.96/1.33 a474, X ), ! alpha82 }.
% 0.96/1.33 (505) {G18,W8,D2,L6,V0,M1} R(460,451);f { c1_0, alpha74, c1_1( a479 ),
% 0.96/1.33 alpha78, c4_0, ! c2_1( a479 ) }.
% 0.96/1.33 (363) {G20,W8,D2,L5,V1,M1} R(362,8) { ! c3_1( X ), c4_1( X ), c5_0, ! c5_1
% 0.96/1.33 ( X ), ! c2_0 }.
% 0.96/1.33 (460) {G17,W8,D2,L5,V1,M1} R(445,446) { alpha74, c1_0, c1_1( X ), ! c2_1( X
% 0.96/1.33 ), ndr1_1( X ) }.
% 0.96/1.33 (271) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c3_2( X, a476 ), alpha54( X )
% 0.96/1.33 , c1_2( X, a476 ) }.
% 0.96/1.33 (487) {G21,W7,D2,L5,V0,M1} R(486,480) { alpha44, alpha25, c1_1( a472 ),
% 0.96/1.33 c1_0, c3_1( a472 ) }.
% 0.96/1.33 (503) {G5,W7,D2,L4,V0,M1} R(469,458) { alpha79, c4_1( a478 ), ! ndr1_1(
% 0.96/1.33 a478 ), ! alpha109( a478 ) }.
% 0.96/1.33 (469) {G4,W7,D2,L4,V0,M1} R(468,143) { alpha79, ! ndr1_1( a478 ), c4_1(
% 0.96/1.33 a478 ), ! alpha114( a478 ) }.
% 0.96/1.33 (248) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c5_2( X, a477 ), alpha80( X
% 0.96/1.33 ), c2_2( X, a477 ) }.
% 0.96/1.33 (255) {G0,W7,D2,L4,V1,M1} I { c2_1( X ), ! c4_1( X ), ! c1_1( X ), !
% 0.96/1.33 alpha53 }.
% 0.96/1.33 (502) {G10,W4,D2,L3,V0,M1} R(501,164) { c2_0, alpha105, alpha62( a484 ) }.
% 0.96/1.33 (226) {G0,W10,D2,L4,V1,M1} I { ! c2_2( a478, X ), ! c1_2( a478, X ), ! c4_2
% 0.96/1.33 ( a478, X ), ! alpha79 }.
% 0.96/1.33 (501) {G9,W4,D2,L3,V0,M1} R(494,168);r(429) { c2_0, alpha105, alpha76( a484
% 0.96/1.33 ) }.
% 0.96/1.33 (494) {G8,W6,D2,L4,V0,M1} R(431,172) { c2_0, alpha105, ! ndr1_1( a484 ),
% 0.96/1.33 alpha101( a484 ) }.
% 0.96/1.33 (499) {G9,W6,D2,L4,V0,M1} R(493,242) { c2_0, alpha105, ! alpha66( a484 ), !
% 0.96/1.33 alpha75( a484 ) }.
% 0.96/1.33 (493) {G8,W6,D2,L4,V0,M1} R(431,483);r(245) { c2_0, alpha105, ! alpha75(
% 0.96/1.33 a484 ), ! alpha80( a484 ) }.
% 0.96/1.33 (207) {G0,W10,D2,L4,V1,M1} I { ! c1_2( a479, X ), ! c5_2( a479, X ), ! c2_2
% 0.96/1.33 ( a479, X ), ! alpha78 }.
% 0.96/1.33 (496) {G20,W6,D2,L3,V0,M1} S(194);r(362) { ! ndr1_1( a480 ), alpha102, c4_2
% 0.96/1.33 ( a480, a481 ) }.
% 0.96/1.33 (498) {G17,W5,D2,L4,V0,M1} R(497,445);r(387) { alpha105, alpha74, c1_0, !
% 0.96/1.33 c2_1( a484 ) }.
% 0.96/1.33 (497) {G9,W4,D2,L3,V0,M1} R(495,117);r(418) { c2_0, alpha105, ! alpha99(
% 0.96/1.33 a484 ) }.
% 0.96/1.33 (495) {G8,W4,D2,L3,V0,M1} R(431,121);r(440) { c2_0, alpha105, ! alpha108(
% 0.96/1.33 a484 ) }.
% 0.96/1.33 (431) {G7,W7,D2,L4,V1,M1} R(84,411) { ! ndr1_1( a484 ), c2_0, alpha105,
% 0.96/1.33 c4_2( a484, X ) }.
% 0.96/1.33 (244) {G0,W7,D2,L3,V1,M1} I { ! alpha80( X ), alpha66( X ), ! c1_2( X, a477
% 0.96/1.33 ) }.
% 0.96/1.33 (492) {G1,W7,D2,L3,V1,M1} R(169,17);r(18) { ! alpha101( X ), ! alpha93( X )
% 0.96/1.33 , c4_2( X, a489 ) }.
% 0.96/1.33 (491) {G1,W6,D2,L3,V0,M1} R(169,316);r(315) { ! alpha101( a474 ), alpha82,
% 0.96/1.33 ! c5_2( a474, skol19 ) }.
% 0.96/1.33 (169) {G0,W11,D2,L4,V2,M1} I { ! alpha101( X ), ! c5_2( X, Y ), c4_2( X, Y
% 0.96/1.33 ), ! c3_2( X, Y ) }.
% 0.96/1.33 (267) {G0,W7,D2,L3,V1,M1} I { ! alpha54( X ), alpha41( X ), c5_2( X, a476 )
% 0.96/1.33 }.
% 0.96/1.33 (483) {G1,W7,D2,L3,V1,M1} R(159,246);r(247) { ! alpha75( X ), ! alpha80( X
% 0.96/1.33 ), ! c4_2( X, a477 ) }.
% 0.96/1.33 (170) {G0,W6,D3,L2,V1,M1} I { alpha101( X ), c5_2( X, skol11( X ) ) }.
% 0.96/1.33 (171) {G0,W6,D3,L2,V1,M1} I { alpha101( X ), c3_2( X, skol11( X ) ) }.
% 0.96/1.33 (162) {G0,W6,D3,L2,V1,M1} I { alpha75( X ), c4_2( X, skol10( X ) ) }.
% 0.96/1.33 (172) {G0,W6,D3,L2,V1,M1} I { alpha101( X ), ! c4_2( X, skol11( X ) ) }.
% 0.96/1.33 (279) {G0,W6,D3,L2,V1,M1} I { alpha55( X ), ! c3_2( X, skol17( X ) ) }.
% 0.96/1.33 (280) {G0,W6,D3,L2,V1,M1} I { alpha55( X ), c4_2( X, skol17( X ) ) }.
% 0.96/1.33 (281) {G0,W6,D3,L2,V1,M1} I { alpha55( X ), ! c5_2( X, skol17( X ) ) }.
% 0.96/1.33 (161) {G0,W6,D3,L2,V1,M1} I { alpha75( X ), ! c2_2( X, skol10( X ) ) }.
% 0.96/1.33 (472) {G22,W6,D2,L5,V0,M1} R(470,63) { c2_0, c3_0, c5_0, alpha96, ! c4_1(
% 0.96/1.33 a485 ) }.
% 0.96/1.33 (486) {G20,W5,D2,L3,V0,M1} S(329);r(362) { c1_1( a472 ), alpha44, ! c5_1(
% 0.96/1.33 a472 ) }.
% 0.96/1.33 (485) {G20,W5,D2,L3,V0,M1} S(350);r(362) { c2_1( a471 ), alpha18, c4_1(
% 0.96/1.33 a471 ) }.
% 0.96/1.33 (160) {G0,W6,D3,L2,V1,M1} I { alpha75( X ), c5_2( X, skol10( X ) ) }.
% 0.96/1.33 (474) {G23,W6,D2,L4,V0,M1} R(473,68) { c2_0, c3_0, c5_0, c5_2( a485, a486 )
% 0.96/1.33 }.
% 0.96/1.33 (476) {G24,W6,D2,L4,V0,M1} R(475,71) { c2_0, c3_0, c5_0, c2_2( a485, a486 )
% 0.96/1.33 }.
% 0.96/1.33 (478) {G25,W6,D2,L4,V0,M1} R(477,75) { c2_0, c3_0, c5_0, c3_2( a485, a486 )
% 0.96/1.33 }.
% 0.96/1.33 (159) {G0,W11,D2,L4,V2,M1} I { ! alpha75( X ), ! c5_2( X, Y ), ! c4_2( X, Y
% 0.96/1.33 ), c2_2( X, Y ) }.
% 0.96/1.33 (482) {G15,W5,D2,L4,V0,M1} R(480,427) { alpha25, c1_0, alpha39, c3_1(
% 0.96/1.33 skol14 ) }.
% 0.96/1.33 (481) {G21,W5,D2,L4,V0,M1} R(480,450) { alpha25, c1_0, alpha50, c3_1( a479
% 0.96/1.33 ) }.
% 0.96/1.33 (480) {G14,W6,D2,L4,V1,M1} R(336,335) { alpha25, c3_1( X ), c1_0, c5_1( X )
% 0.96/1.33 }.
% 0.96/1.33 (336) {G0,W6,D2,L4,V1,M1} I { alpha25, c3_1( X ), c5_1( X ), ! alpha17 }.
% 0.96/1.33 (152) {G0,W6,D3,L2,V1,M1} I { alpha118( X ), c2_2( X, skol8( X ) ) }.
% 0.96/1.33 (471) {G22,W5,D2,L4,V0,M1} R(470,65) { c2_0, c3_0, c5_0, c2_1( a485 ) }.
% 0.96/1.33 (479) {G25,W5,D2,L4,V0,M1} R(477,74) { c2_0, c3_0, c5_0, ndr1_1( a485 ) }.
% 0.96/1.33 (477) {G24,W4,D1,L4,V0,M1} R(475,70) { c2_0, c3_0, c5_0, alpha117 }.
% 0.96/1.33 (475) {G23,W4,D1,L4,V0,M1} R(473,67) { c2_0, c3_0, c5_0, alpha115 }.
% 0.96/1.33 (151) {G0,W6,D3,L2,V1,M1} I { alpha118( X ), c4_2( X, skol8( X ) ) }.
% 0.96/1.33 (473) {G22,W4,D1,L4,V0,M1} R(470,64) { c2_0, c3_0, c5_0, alpha110 }.
% 0.96/1.33 (470) {G21,W4,D1,L4,V0,M1} R(364,417);r(418) { c3_0, c2_0, c5_0, alpha105
% 0.96/1.33 }.
% 0.96/1.33 (364) {G20,W6,D2,L4,V1,M1} R(362,3) { c3_0, c1_1( X ), c5_0, c3_1( X ) }.
% 0.96/1.33 (150) {G0,W6,D3,L2,V1,M1} I { alpha118( X ), c1_2( X, skol8( X ) ) }.
% 0.96/1.33 (468) {G3,W5,D2,L3,V0,M1} R(467,146) { alpha79, ! ndr1_1( a478 ), !
% 0.96/1.33 alpha116( a478 ) }.
% 0.96/1.33 (467) {G2,W3,D2,L2,V0,M1} S(465);r(227) { alpha79, ! alpha118( a478 ) }.
% 0.96/1.33 (464) {G1,W6,D2,L3,V0,M1} R(149,208);r(210) { ! alpha118( a479 ), alpha78,
% 0.96/1.33 ! c4_2( a479, skol12 ) }.
% 0.96/1.33 (149) {G0,W11,D2,L4,V2,M1} I { ! alpha118( X ), ! c4_2( X, Y ), ! c2_2( X,
% 0.96/1.33 Y ), ! c1_2( X, Y ) }.
% 0.96/1.33 (445) {G16,W6,D2,L4,V1,M1} R(114,404) { ! c2_1( X ), alpha74, c1_0, alpha99
% 0.96/1.33 ( X ) }.
% 0.96/1.33 (425) {G20,W6,D2,L3,V0,M1} S(76);r(362) { ! ndr1_1( a485 ), alpha117, !
% 0.96/1.33 c3_2( a485, a486 ) }.
% 0.96/1.33 (146) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha116( X ), alpha118( X )
% 0.96/1.33 }.
% 0.96/1.33 (459) {G2,W4,D2,L2,V1,M1} S(163);r(429) { ! alpha62( X ), alpha76( X ) }.
% 0.96/1.33 (143) {G0,W6,D2,L3,V1,M1} I { ! alpha114( X ), c4_1( X ), alpha116( X ) }.
% 0.96/1.33 (166) {G0,W6,D2,L3,V1,M1} I { ! alpha76( X ), alpha90( X ), alpha101( X )
% 0.96/1.33 }.
% 0.96/1.33 (173) {G0,W6,D2,L3,V1,M1} I { c2_1( X ), ! ndr1_1( X ), ! alpha90( X ) }.
% 0.96/1.33 (458) {G2,W4,D2,L2,V1,M1} S(140);r(436) { ! alpha109( X ), alpha114( X )
% 0.96/1.33 }.
% 0.96/1.33 (457) {G2,W6,D2,L3,V1,M1} R(239,426) { c5_1( X ), ndr1_1( X ), ! alpha52( X
% 0.96/1.33 ) }.
% 0.96/1.33 (239) {G0,W6,D2,L3,V1,M1} I { c5_1( X ), ! alpha52( X ), alpha66( X ) }.
% 0.96/1.33 (272) {G0,W6,D2,L3,V1,M1} I { ! alpha31( X ), ! c3_1( X ), alpha42( X ) }.
% 0.96/1.33 (275) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha42( X ), alpha55( X )
% 0.96/1.33 }.
% 0.96/1.33 (139) {G0,W6,D3,L2,V1,M1} I { alpha113( X ), c4_2( X, skol7( X ) ) }.
% 0.96/1.33 (420) {G2,W6,D2,L3,V1,M1} R(366,10) { c2_1( X ), ndr1_1( X ), ! alpha68( X
% 0.96/1.33 ) }.
% 0.96/1.33 (446) {G2,W6,D2,L3,V1,M1} R(117,440) { c1_1( X ), ndr1_1( X ), ! alpha99( X
% 0.96/1.33 ) }.
% 0.96/1.33 (409) {G8,W5,D2,L4,V0,M1} R(48,400) { alpha104, c1_0, alpha103, ! ndr1_1(
% 0.96/1.33 a487 ) }.
% 0.96/1.33 (451) {G17,W5,D2,L4,V0,M1} R(204,394) { alpha78, c1_0, c4_0, ! ndr1_1( a479
% 0.96/1.33 ) }.
% 0.96/1.33 (138) {G0,W6,D3,L2,V1,M1} I { alpha113( X ), ! c5_2( X, skol7( X ) ) }.
% 0.96/1.33 (187) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a480, a481 ), alpha77, ! alpha91 }.
% 0.96/1.33 (190) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a480, a481 ), alpha91, ! alpha102 }.
% 0.96/1.33 (293) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a474, a475 ), alpha23, ! alpha32 }.
% 0.96/1.33 (296) {G0,W5,D2,L3,V0,M1} I { c5_2( a474, a475 ), alpha32, ! alpha43 }.
% 0.96/1.33 (137) {G0,W6,D3,L2,V1,M1} I { alpha113( X ), ! c1_2( X, skol7( X ) ) }.
% 0.96/1.33 (319) {G0,W5,D2,L3,V0,M1} I { c3_2( a472, a473 ), alpha16, ! alpha24 }.
% 0.96/1.33 (322) {G0,W5,D2,L3,V0,M1} I { c5_2( a472, a473 ), alpha24, ! alpha33 }.
% 0.96/1.33 (372) {G20,W5,D2,L3,V0,M1} S(24);r(362) { ! c3_1( a491 ), alpha69, ! c5_1(
% 0.96/1.33 a491 ) }.
% 0.96/1.33 (453) {G7,W5,D2,L3,V1,M1} R(156,155) { alpha62( X ), alpha36, alpha75( X )
% 0.96/1.33 }.
% 0.96/1.33 (136) {G0,W11,D2,L4,V2,M1} I { ! alpha113( X ), c5_2( X, Y ), ! c4_2( X, Y
% 0.96/1.33 ), c1_2( X, Y ) }.
% 0.96/1.33 (156) {G0,W5,D2,L3,V1,M1} I { alpha62( X ), alpha75( X ), ! alpha48 }.
% 0.96/1.33 (236) {G0,W5,D2,L3,V1,M1} I { alpha52( X ), ! c2_1( X ), ! alpha39 }.
% 0.96/1.33 (452) {G10,W5,D2,L3,V1,M1} R(262,261) { alpha31( X ), alpha15, alpha41( X )
% 0.96/1.33 }.
% 0.96/1.33 (262) {G0,W5,D2,L3,V1,M1} I { alpha31( X ), alpha41( X ), ! alpha22 }.
% 0.96/1.33 (133) {G0,W5,D2,L3,V1,M1} I { alpha109( X ), alpha113( X ), ! alpha100 }.
% 0.96/1.33 (243) {G0,W5,D2,L2,V1,M1} I { ! alpha66( X ), c1_2( X, a477 ) }.
% 0.96/1.33 (246) {G0,W5,D2,L2,V1,M1} I { ! alpha80( X ), ! c2_2( X, a477 ) }.
% 0.96/1.33 (247) {G0,W5,D2,L2,V1,M1} I { ! alpha80( X ), c5_2( X, a477 ) }.
% 0.96/1.33 (266) {G0,W5,D2,L2,V1,M1} I { ! alpha41( X ), ! c5_2( X, a476 ) }.
% 0.96/1.33 (126) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c3_2( X, a482 ), alpha112(
% 0.96/1.33 X ), ! c1_2( X, a482 ) }.
% 0.96/1.33 (269) {G0,W5,D2,L2,V1,M1} I { ! alpha54( X ), ! c3_2( X, a476 ) }.
% 0.96/1.33 (270) {G0,W5,D2,L2,V1,M1} I { ! alpha54( X ), ! c1_2( X, a476 ) }.
% 0.96/1.33 (184) {G0,W4,D2,L3,V0,M1} I { c5_1( a480 ), alpha63, ! alpha77 }.
% 0.96/1.33 (204) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a479 ), alpha78, ! alpha64 }.
% 0.96/1.33 (125) {G0,W5,D2,L2,V1,M1} I { ! alpha112( X ), c1_2( X, a482 ) }.
% 0.96/1.33 (450) {G20,W3,D2,L2,V0,M1} S(213);r(362) { alpha50, ! c5_1( a479 ) }.
% 0.96/1.33 (219) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a478 ), alpha29, ! alpha38 }.
% 0.96/1.33 (449) {G11,W4,D2,L3,V0,M1} R(223,369) { alpha79, alpha21, ! ndr1_1( a478 )
% 0.96/1.33 }.
% 0.96/1.33 (124) {G0,W5,D2,L2,V1,M1} I { ! alpha112( X ), c3_2( X, a482 ) }.
% 0.96/1.33 (223) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a478 ), alpha79, ! alpha65 }.
% 0.96/1.33 (448) {G20,W3,D2,L2,V0,M1} S(232);r(362) { alpha51, c2_1( a478 ) }.
% 0.96/1.33 (299) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a474 ), alpha43, ! alpha56 }.
% 0.96/1.33 (122) {G0,W7,D2,L3,V1,M1} I { ! alpha112( X ), alpha108( X ), c4_2( X, a482
% 0.96/1.33 ) }.
% 0.96/1.33 (447) {G16,W2,D1,L2,V0,M1} R(303,357);r(412) { alpha16, alpha92 }.
% 0.96/1.33 (303) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a474 ), alpha92, ! alpha81 }.
% 0.96/1.33 (325) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a472 ), alpha33, ! alpha44 }.
% 0.96/1.33 (401) {G6,W4,D2,L3,V0,M1} R(43,398) { alpha103, c1_0, ! c2_1( a487 ) }.
% 0.96/1.33 (121) {G0,W5,D2,L2,V1,M1} I { ! alpha108( X ), ! c4_2( X, a482 ) }.
% 0.96/1.33 (413) {G4,W4,D2,L3,V0,M1} R(62,407) { alpha86, c2_0, c4_1( a485 ) }.
% 0.96/1.33 (416) {G17,W4,D2,L3,V0,M1} R(212,393) { c1_0, c4_0, c5_1( a479 ) }.
% 0.96/1.33 (417) {G6,W4,D2,L3,V0,M1} R(81,410) { c2_0, alpha105, ! c3_1( a484 ) }.
% 0.96/1.33 (418) {G5,W4,D2,L3,V0,M1} R(78,408) { c2_0, alpha105, ! c1_1( a484 ) }.
% 0.96/1.33 (117) {G0,W6,D2,L3,V1,M1} I { c1_1( X ), ! alpha99( X ), alpha108( X ) }.
% 0.96/1.33 (186) {G0,W4,D2,L2,V0,M1} I { c2_2( a480, a481 ), ! alpha77 }.
% 0.96/1.33 (189) {G0,W4,D2,L2,V0,M1} I { c1_2( a480, a481 ), ! alpha91 }.
% 0.96/1.33 (193) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a480, a481 ), ! alpha102 }.
% 0.96/1.33 (208) {G0,W4,D2,L2,V0,M1} I { alpha78, c1_2( a479, skol12 ) }.
% 0.96/1.33 (114) {G0,W5,D2,L3,V1,M1} I { alpha99( X ), ! c2_1( X ), ! alpha88 }.
% 0.96/1.33 (209) {G0,W4,D2,L2,V0,M1} I { alpha78, c5_2( a479, skol12 ) }.
% 0.96/1.33 (210) {G0,W4,D2,L2,V0,M1} I { alpha78, c2_2( a479, skol12 ) }.
% 0.96/1.33 (227) {G0,W4,D2,L2,V0,M1} I { alpha79, c2_2( a478, skol13 ) }.
% 0.96/1.33 (228) {G0,W4,D2,L2,V0,M1} I { alpha79, c1_2( a478, skol13 ) }.
% 0.96/1.33 (105) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a483 ), alpha111(
% 0.96/1.33 X ), ! c3_2( X, a483 ) }.
% 0.96/1.33 (229) {G0,W4,D2,L2,V0,M1} I { alpha79, c4_2( a478, skol13 ) }.
% 0.96/1.33 (444) {G12,W4,D2,L2,V0,M1} R(292,290) { alpha16, c2_2( a474, a475 ) }.
% 0.96/1.33 (292) {G0,W4,D2,L2,V0,M1} I { c2_2( a474, a475 ), ! alpha23 }.
% 0.96/1.33 (443) {G13,W4,D2,L2,V0,M1} R(295,353) { alpha16, ! c5_2( a474, a475 ) }.
% 0.96/1.33 (104) {G0,W5,D2,L2,V1,M1} I { ! alpha111( X ), c2_2( X, a483 ) }.
% 0.96/1.33 (295) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a474, a475 ), ! alpha32 }.
% 0.96/1.33 (307) {G0,W4,D2,L2,V0,M1} I { alpha92, c5_2( a474, skol18 ) }.
% 0.96/1.33 (308) {G0,W4,D2,L2,V0,M1} I { alpha92, ! c1_2( a474, skol18 ) }.
% 0.96/1.33 (309) {G0,W4,D2,L2,V0,M1} I { alpha92, c4_2( a474, skol18 ) }.
% 0.96/1.33 (103) {G0,W5,D2,L2,V1,M1} I { ! alpha111( X ), c3_2( X, a483 ) }.
% 0.96/1.33 (315) {G0,W4,D2,L2,V0,M1} I { alpha82, ! c4_2( a474, skol19 ) }.
% 0.96/1.33 (316) {G0,W4,D2,L2,V0,M1} I { alpha82, c3_2( a474, skol19 ) }.
% 0.96/1.33 (318) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a472, a473 ), ! alpha16 }.
% 0.96/1.33 (321) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a472, a473 ), ! alpha24 }.
% 0.96/1.33 (101) {G0,W7,D2,L3,V1,M1} I { ! alpha111( X ), alpha107( X ), ! c1_2( X,
% 0.96/1.33 a483 ) }.
% 0.96/1.33 (435) {G20,W4,D2,L2,V0,M1} S(86);r(362) { alpha106, ! c4_2( a484, skol3 )
% 0.96/1.33 }.
% 0.96/1.33 (442) {G1,W4,D2,L2,V1,M1} R(102,99) { ndr1_1( X ), ! alpha107( X ) }.
% 0.96/1.33 (102) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha111( X ) }.
% 0.96/1.33 (441) {G1,W3,D2,L2,V0,M1} R(118,115) { alpha88, ! c1_1( skol5 ) }.
% 0.96/1.33 (100) {G0,W5,D2,L2,V1,M1} I { ! alpha107( X ), c1_2( X, a483 ) }.
% 0.96/1.33 (118) {G0,W4,D2,L2,V1,M1} I { ! c1_1( X ), alpha99( X ) }.
% 0.96/1.33 (119) {G0,W4,D2,L2,V1,M1} I { alpha99( X ), ! alpha108( X ) }.
% 0.96/1.33 (440) {G1,W4,D2,L2,V1,M1} R(120,123) { ndr1_1( X ), ! alpha108( X ) }.
% 0.96/1.33 (120) {G0,W4,D2,L2,V1,M1} I { ! alpha108( X ), alpha112( X ) }.
% 0.96/1.33 (99) {G0,W4,D2,L2,V1,M1} I { ! alpha107( X ), alpha111( X ) }.
% 0.96/1.33 (123) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha112( X ) }.
% 0.96/1.33 (439) {G2,W3,D2,L2,V0,M1} R(438,134) { alpha100, ! c4_1( skol6 ) }.
% 0.96/1.33 (438) {G1,W4,D2,L2,V1,M1} R(141,145) { ! c4_1( X ), alpha109( X ) }.
% 0.96/1.33 (141) {G0,W4,D2,L2,V1,M1} I { alpha109( X ), ! alpha114( X ) }.
% 0.96/1.33 (96) {G0,W5,D2,L3,V1,M1} I { alpha107( X ), ! c2_1( X ), ! alpha98 }.
% 0.96/1.33 (437) {G1,W3,D2,L2,V0,M1} R(142,134) { alpha100, ndr1_1( skol6 ) }.
% 0.96/1.33 (142) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha109( X ) }.
% 0.96/1.33 (436) {G1,W4,D2,L2,V1,M1} R(144,147) { ndr1_1( X ), alpha114( X ) }.
% 0.96/1.33 (144) {G0,W4,D2,L2,V1,M1} I { alpha114( X ), ! alpha116( X ) }.
% 0.96/1.33 (145) {G0,W4,D2,L2,V1,M1} I { ! c4_1( X ), alpha114( X ) }.
% 0.96/1.33 (147) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha116( X ) }.
% 0.96/1.33 (148) {G0,W4,D2,L2,V1,M1} I { alpha116( X ), ! alpha118( X ) }.
% 0.96/1.33 (434) {G20,W3,D2,L2,V0,M1} S(85);r(362) { alpha106, ndr1_1( a484 ) }.
% 0.96/1.33 (433) {G3,W3,D2,L2,V0,M1} R(432,157) { alpha48, ! c2_1( skol9 ) }.
% 0.96/1.33 (432) {G2,W4,D2,L2,V1,M1} R(164,428) { ! c2_1( X ), alpha62( X ) }.
% 0.96/1.33 (164) {G0,W4,D2,L2,V1,M1} I { alpha62( X ), ! alpha76( X ) }.
% 0.96/1.33 (430) {G1,W3,D2,L2,V0,M1} R(165,157) { alpha48, ndr1_1( skol9 ) }.
% 0.96/1.33 (84) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( a484 ), c4_2( a484, X ), ! alpha106
% 0.96/1.33 }.
% 0.96/1.33 (165) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha62( X ) }.
% 0.96/1.33 (429) {G1,W4,D2,L2,V1,M1} R(167,175) { ndr1_1( X ), alpha76( X ) }.
% 0.96/1.33 (428) {G1,W4,D2,L2,V1,M1} R(167,174) { ! c2_1( X ), alpha76( X ) }.
% 0.96/1.33 (167) {G0,W4,D2,L2,V1,M1} I { alpha76( X ), ! alpha90( X ) }.
% 0.96/1.33 (82) {G0,W4,D2,L3,V0,M1} I { c3_1( a484 ), alpha97, ! alpha106 }.
% 0.96/1.33 (168) {G0,W4,D2,L2,V1,M1} I { alpha76( X ), ! alpha101( X ) }.
% 0.96/1.33 (174) {G0,W4,D2,L2,V1,M1} I { ! c2_1( X ), alpha90( X ) }.
% 0.96/1.33 (175) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha90( X ) }.
% 0.96/1.33 (427) {G1,W3,D2,L2,V0,M1} R(240,237) { alpha39, ! c5_1( skol14 ) }.
% 0.96/1.33 (79) {G0,W4,D2,L3,V0,M1} I { c1_1( a484 ), alpha86, ! alpha97 }.
% 0.96/1.33 (240) {G0,W4,D2,L2,V1,M1} I { ! c5_1( X ), alpha52( X ) }.
% 0.96/1.33 (241) {G0,W4,D2,L2,V1,M1} I { alpha52( X ), ! alpha66( X ) }.
% 0.96/1.33 (426) {G1,W4,D2,L2,V1,M1} R(242,245) { ndr1_1( X ), ! alpha66( X ) }.
% 0.96/1.33 (242) {G0,W4,D2,L2,V1,M1} I { ! alpha66( X ), alpha80( X ) }.
% 0.96/1.33 (245) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha80( X ) }.
% 0.96/1.33 (424) {G1,W4,D2,L2,V1,M1} R(265,268) { ndr1_1( X ), ! alpha41( X ) }.
% 0.96/1.33 (265) {G0,W4,D2,L2,V1,M1} I { ! alpha41( X ), alpha54( X ) }.
% 0.96/1.33 (268) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha54( X ) }.
% 0.96/1.33 (75) {G0,W4,D2,L2,V0,M1} I { c3_2( a485, a486 ), ! alpha117 }.
% 0.96/1.33 (423) {G2,W3,D2,L2,V0,M1} R(422,263) { alpha22, ndr1_1( skol16 ) }.
% 0.96/1.33 (422) {G1,W4,D2,L2,V1,M1} R(273,276) { ndr1_1( X ), alpha31( X ) }.
% 0.96/1.33 (273) {G0,W4,D2,L2,V1,M1} I { alpha31( X ), ! alpha42( X ) }.
% 0.96/1.33 (421) {G1,W3,D2,L2,V0,M1} R(274,263) { alpha22, c3_1( skol16 ) }.
% 0.96/1.33 (72) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a485, a486 ), alpha115, ! alpha117 }.
% 0.96/1.33 (274) {G0,W4,D2,L2,V1,M1} I { c3_1( X ), alpha31( X ) }.
% 0.96/1.33 (276) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha42( X ) }.
% 0.96/1.33 (277) {G0,W4,D2,L2,V1,M1} I { alpha42( X ), ! alpha55( X ) }.
% 0.96/1.33 (366) {G1,W4,D2,L2,V1,M1} R(16,13) { ndr1_1( X ), ! alpha83( X ) }.
% 0.96/1.33 (71) {G0,W4,D2,L2,V0,M1} I { c2_2( a485, a486 ), ! alpha115 }.
% 0.96/1.33 (419) {G20,W3,D1,L3,V0,M1} S(282);r(362) { c4_0, ! c2_0, ! alpha15 }.
% 0.96/1.33 (74) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a485 ), ! alpha117 }.
% 0.96/1.33 (78) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a484 ), ! alpha86 }.
% 0.96/1.33 (69) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a485, a486 ), alpha110, ! alpha115 }.
% 0.96/1.33 (81) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a484 ), ! alpha97 }.
% 0.96/1.33 (97) {G0,W3,D2,L2,V0,M1} I { alpha98, ! alpha107( skol4 ) }.
% 0.96/1.33 (98) {G0,W3,D2,L2,V0,M1} I { alpha98, c2_1( skol4 ) }.
% 0.96/1.33 (115) {G0,W3,D2,L2,V0,M1} I { alpha88, ! alpha99( skol5 ) }.
% 0.96/1.33 (68) {G0,W4,D2,L2,V0,M1} I { c5_2( a485, a486 ), ! alpha110 }.
% 0.96/1.33 (116) {G0,W3,D2,L2,V0,M1} I { alpha88, c2_1( skol5 ) }.
% 0.96/1.33 (134) {G0,W3,D2,L2,V0,M1} I { alpha100, ! alpha109( skol6 ) }.
% 0.96/1.33 (135) {G0,W3,D2,L2,V0,M1} I { alpha100, ! alpha113( skol6 ) }.
% 0.96/1.33 (157) {G0,W3,D2,L2,V0,M1} I { alpha48, ! alpha62( skol9 ) }.
% 0.96/1.33 (66) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a485 ), alpha105, ! alpha110 }.
% 0.96/1.33 (158) {G0,W3,D2,L2,V0,M1} I { alpha48, ! alpha75( skol9 ) }.
% 0.96/1.33 (183) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a480 ), ! alpha63 }.
% 0.96/1.33 (192) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a480 ), ! alpha102 }.
% 0.96/1.33 (205) {G0,W3,D2,L2,V0,M1} I { alpha64, ndr1_1( a479 ) }.
% 0.96/1.33 (65) {G0,W3,D2,L2,V0,M1} I { c2_1( a485 ), ! alpha105 }.
% 0.96/1.33 (212) {G0,W3,D2,L2,V0,M1} I { c5_1( a479 ), ! alpha50 }.
% 0.96/1.33 (415) {G9,W3,D2,L2,V0,M1} R(218,216) { alpha21, c1_1( a478 ) }.
% 0.96/1.33 (218) {G0,W3,D2,L2,V0,M1} I { c1_1( a478 ), ! alpha29 }.
% 0.96/1.33 (224) {G0,W3,D2,L2,V0,M1} I { alpha65, ndr1_1( a478 ) }.
% 0.96/1.33 (63) {G0,W4,D2,L3,V0,M1} I { ! c4_1( a485 ), alpha96, ! alpha105 }.
% 0.96/1.33 (414) {G11,W3,D2,L2,V0,M1} R(231,368) { alpha21, ! c2_1( a478 ) }.
% 0.96/1.33 (231) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a478 ), ! alpha51 }.
% 0.96/1.33 (237) {G0,W3,D2,L2,V0,M1} I { alpha39, ! alpha52( skol14 ) }.
% 0.96/1.33 (238) {G0,W3,D2,L2,V0,M1} I { alpha39, c2_1( skol14 ) }.
% 0.96/1.33 (62) {G0,W3,D2,L2,V0,M1} I { c4_1( a485 ), ! alpha96 }.
% 0.96/1.33 (256) {G0,W3,D2,L2,V0,M1} I { alpha53, ! c2_1( skol15 ) }.
% 0.96/1.33 (257) {G0,W3,D2,L2,V0,M1} I { alpha53, c4_1( skol15 ) }.
% 0.96/1.33 (258) {G0,W3,D2,L2,V0,M1} I { alpha53, c1_1( skol15 ) }.
% 0.96/1.33 (263) {G0,W3,D2,L2,V0,M1} I { alpha22, ! alpha31( skol16 ) }.
% 0.96/1.33 (54) {G0,W4,D2,L2,V0,M1} I { alpha104, c5_2( a487, skol2 ) }.
% 0.96/1.33 (264) {G0,W3,D2,L2,V0,M1} I { alpha22, ! alpha41( skol16 ) }.
% 0.96/1.33 (412) {G14,W3,D2,L2,V0,M1} R(298,354) { alpha16, ndr1_1( a474 ) }.
% 0.96/1.33 (298) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a474 ), ! alpha43 }.
% 0.96/1.33 (304) {G0,W3,D2,L2,V0,M1} I { alpha81, ndr1_1( a474 ) }.
% 0.96/1.33 (53) {G0,W4,D2,L2,V0,M1} I { alpha104, ! c4_2( a487, skol2 ) }.
% 0.96/1.33 (314) {G0,W3,D2,L2,V0,M1} I { alpha82, ndr1_1( a474 ) }.
% 0.96/1.33 (324) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a472 ), ! alpha33 }.
% 0.96/1.33 (327) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a472 ), ! alpha44 }.
% 0.96/1.33 (328) {G0,W3,D2,L2,V0,M1} I { c5_1( a472 ), ! alpha44 }.
% 0.96/1.33 (52) {G0,W4,D2,L2,V0,M1} I { alpha104, c2_2( a487, skol2 ) }.
% 0.96/1.33 (338) {G0,W3,D2,L2,V0,M1} I { alpha17, ! c3_1( skol20 ) }.
% 0.96/1.33 (339) {G0,W3,D2,L2,V0,M1} I { alpha17, ! c5_1( skol20 ) }.
% 0.96/1.33 (348) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a471 ), ! alpha18 }.
% 0.96/1.33 (349) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a471 ), ! alpha18 }.
% 0.96/1.33 (51) {G0,W10,D2,L4,V1,M1} I { ! c2_2( a487, X ), c4_2( a487, X ), ! c5_2(
% 0.96/1.33 a487, X ), ! alpha104 }.
% 0.96/1.33 (370) {G2,W3,D2,L2,V0,M1} R(22,20) { c3_0, c3_1( a491 ) }.
% 0.96/1.33 (371) {G2,W3,D2,L2,V0,M1} R(23,20) { c3_0, c5_1( a491 ) }.
% 0.96/1.33 (380) {G2,W3,D2,L2,V0,M1} R(27,25) { alpha58, c2_1( a488 ) }.
% 0.96/1.33 (391) {G4,W3,D2,L2,V0,M1} R(37,381) { alpha58, c4_1( a488 ) }.
% 0.96/1.33 (49) {G0,W3,D2,L2,V0,M1} I { alpha95, ndr1_1( a487 ) }.
% 0.96/1.33 (395) {G20,W3,D2,L2,V0,M1} S(38);r(362) { alpha94, ! c4_1( a488 ) }.
% 0.96/1.33 (411) {G6,W3,D1,L3,V0,M1} R(410,80) { c2_0, alpha105, alpha106 }.
% 0.96/1.33 (410) {G5,W3,D1,L3,V0,M1} R(408,77) { c2_0, alpha105, alpha97 }.
% 0.96/1.33 (408) {G4,W3,D1,L3,V0,M1} R(407,61) { c2_0, alpha105, alpha86 }.
% 0.96/1.33 (48) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a487 ), alpha104, ! alpha95 }.
% 0.96/1.33 (407) {G3,W3,D1,L3,V0,M1} R(58,57) { alpha86, c2_0, alpha96 }.
% 0.96/1.33 (58) {G0,W3,D1,L3,V0,M1} I { alpha86, alpha96, ! alpha72 }.
% 0.96/1.33 (90) {G0,W3,D1,L3,V0,M1} I { alpha87, c4_0, ! alpha73 }.
% 0.96/1.33 (406) {G20,W2,D1,L2,V0,M1} S(47);r(362) { alpha85, ! alpha95 }.
% 0.96/1.33 (405) {G20,W2,D1,L2,V0,M1} S(93);r(362) { alpha98, ! alpha87 }.
% 0.96/1.33 (404) {G15,W3,D1,L3,V0,M1} R(111,385) { alpha74, c1_0, alpha88 }.
% 0.96/1.33 (111) {G0,W3,D1,L3,V0,M1} I { alpha74, alpha88, ! alpha61 }.
% 0.96/1.33 (44) {G0,W4,D2,L3,V0,M1} I { c2_1( a487 ), alpha71, ! alpha85 }.
% 0.96/1.33 (403) {G20,W2,D1,L2,V0,M1} S(127);r(362) { alpha89, ! alpha74 }.
% 0.96/1.33 (402) {G20,W2,D1,L2,V0,M1} S(130);r(362) { alpha100, ! alpha89 }.
% 0.96/1.33 (43) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a487 ), ! alpha71 }.
% 0.96/1.33 (400) {G7,W3,D1,L3,V0,M1} R(399,46) { c1_0, alpha103, alpha95 }.
% 0.96/1.33 (399) {G6,W3,D1,L3,V0,M1} R(398,42) { c1_0, alpha103, alpha85 }.
% 0.96/1.33 (398) {G5,W3,D1,L3,V0,M1} R(397,107) { alpha103, c1_0, alpha71 }.
% 0.96/1.33 (397) {G4,W3,D1,L3,V0,M1} R(39,382) { alpha71, alpha103, ! c5_0 }.
% 0.96/1.33 (39) {G0,W3,D1,L3,V0,M1} I { ! c5_0, alpha71, ! alpha58 }.
% 0.96/1.33 (396) {G20,W2,D1,L2,V0,M1} S(176);r(362) { alpha49, ! alpha36 }.
% 0.96/1.33 (179) {G0,W3,D1,L3,V0,M1} I { alpha63, c5_0, ! alpha49 }.
% 0.96/1.33 (394) {G16,W3,D1,L3,V0,M1} R(392,202) { c1_0, c4_0, alpha64 }.
% 0.96/1.33 (393) {G16,W3,D1,L3,V0,M1} R(392,201) { c1_0, c4_0, alpha50 }.
% 0.96/1.33 (392) {G15,W3,D1,L3,V0,M1} R(198,386) { c4_0, c1_0, alpha37 }.
% 0.96/1.33 (198) {G0,W3,D1,L3,V0,M1} I { c4_0, alpha37, ! alpha28 }.
% 0.96/1.33 (203) {G0,W3,D1,L3,V0,M1} I { ! alpha50, alpha37, ! alpha64 }.
% 0.96/1.33 (37) {G0,W3,D2,L2,V0,M1} I { c4_1( a488 ), ! alpha94 }.
% 0.96/1.33 (222) {G0,W3,D1,L3,V0,M1} I { ! alpha51, alpha38, ! alpha65 }.
% 0.96/1.33 (233) {G0,W3,D1,L3,V0,M1} I { alpha30, alpha39, ! alpha21 }.
% 0.96/1.33 (390) {G20,W2,D1,L2,V0,M1} S(249);r(362) { alpha40, ! alpha30 }.
% 0.96/1.33 (35) {G0,W4,D2,L2,V0,M1} I { alpha103, ! c4_2( a488, skol1 ) }.
% 0.96/1.33 (389) {G20,W2,D1,L2,V0,M1} S(252);r(362) { alpha53, ! alpha40 }.
% 0.96/1.33 (302) {G0,W3,D1,L3,V0,M1} I { ! alpha67, alpha56, ! alpha81 }.
% 0.96/1.33 (388) {G20,W2,D1,L2,V0,M1} S(312);r(362) { alpha67, ! alpha82 }.
% 0.96/1.33 (34) {G0,W4,D2,L2,V0,M1} I { alpha103, ! c1_2( a488, skol1 ) }.
% 0.96/1.33 (387) {G14,W2,D1,L2,V0,M1} R(384,287) { c1_0, ! c2_0 }.
% 0.96/1.33 (386) {G14,W2,D1,L2,V0,M1} R(384,197) { c1_0, alpha28 }.
% 0.96/1.33 (385) {G14,W2,D1,L2,V0,M1} R(384,110) { c1_0, alpha61 }.
% 0.96/1.33 (33) {G0,W3,D2,L2,V0,M1} I { alpha103, ndr1_1( a488 ) }.
% 0.96/1.33 (384) {G13,W2,D1,L2,V0,M1} S(332);r(107) { c1_0, c3_0 }.
% 0.96/1.33 (383) {G20,W2,D1,L2,V0,M1} S(340);r(362) { ! c3_0, ! alpha25 }.
% 0.96/1.33 (32) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a488 ), c1_2( a488, X ), c4_2( a488
% 0.96/1.33 , X ), ! alpha103 }.
% 0.96/1.33 (344) {G0,W3,D1,L3,V0,M1} I { c2_0, alpha18, ! alpha12 }.
% 0.96/1.33 (40) {G0,W2,D1,L2,V0,M1} I { c5_0, alpha58 }.
% 0.96/1.33 (41) {G0,W2,D1,L2,V0,M1} I { alpha58, ! alpha71 }.
% 0.96/1.33 (31) {G0,W3,D1,L3,V0,M1} I { ! alpha103, alpha84, ! alpha94 }.
% 0.96/1.33 (42) {G0,W2,D1,L2,V0,M1} I { alpha85, ! alpha71 }.
% 0.96/1.33 (46) {G0,W2,D1,L2,V0,M1} I { alpha95, ! alpha85 }.
% 0.96/1.33 (382) {G3,W2,D1,L2,V0,M1} R(30,379) { alpha103, alpha58 }.
% 0.96/1.33 (30) {G0,W2,D1,L2,V0,M1} I { alpha103, ! alpha84 }.
% 0.96/1.33 (50) {G0,W2,D1,L2,V0,M1} I { alpha95, ! alpha104 }.
% 0.96/1.33 (57) {G2,W2,D1,L2,V0,M1} I;r(56) { c2_0, alpha72 }.
% 0.96/1.33 (59) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha86 }.
% 0.96/1.33 (381) {G3,W2,D1,L2,V0,M1} R(29,379) { alpha58, alpha94 }.
% 0.96/1.33 (29) {G0,W2,D1,L2,V0,M1} I { alpha94, ! alpha84 }.
% 0.96/1.33 (60) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha96 }.
% 0.96/1.33 (61) {G0,W2,D1,L2,V0,M1} I { alpha105, ! alpha96 }.
% 0.96/1.33 (64) {G0,W2,D1,L2,V0,M1} I { alpha110, ! alpha105 }.
% 0.96/1.33 (67) {G0,W2,D1,L2,V0,M1} I { alpha115, ! alpha110 }.
% 0.96/1.33 (28) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a488 ), alpha70, ! alpha84 }.
% 0.96/1.33 (70) {G0,W2,D1,L2,V0,M1} I { alpha117, ! alpha115 }.
% 0.96/1.33 (77) {G0,W2,D1,L2,V0,M1} I { alpha97, ! alpha86 }.
% 0.96/1.33 (80) {G0,W2,D1,L2,V0,M1} I { alpha106, ! alpha97 }.
% 0.96/1.33 (27) {G0,W3,D2,L2,V0,M1} I { c2_1( a488 ), ! alpha70 }.
% 0.96/1.33 (89) {G3,W2,D1,L2,V0,M1} I;r(88) { alpha73, ! c2_0 }.
% 0.96/1.33 (91) {G0,W2,D1,L2,V0,M1} I { alpha73, ! alpha87 }.
% 0.96/1.33 (379) {G2,W2,D1,L2,V0,M1} R(26,25) { alpha58, alpha84 }.
% 0.96/1.33 (26) {G0,W2,D1,L2,V0,M1} I { alpha84, ! alpha70 }.
% 0.96/1.33 (92) {G0,W2,D1,L2,V0,M1} I { alpha73, ! c4_0 }.
% 0.96/1.33 (95) {G0,W2,D1,L2,V0,M1} I { alpha87, ! alpha98 }.
% 0.96/1.33 (378) {G5,W2,D1,L2,V0,M1} R(373,177) { c1_0, alpha36 }.
% 0.96/1.33 (25) {G1,W2,D1,L2,V0,M1} I;r(4) { alpha58, alpha70 }.
% 0.96/1.33 (373) {G4,W2,D1,L2,V0,M1} R(107,181) { c1_0, alpha49 }.
% 0.96/1.33 (107) {G3,W2,D1,L2,V0,M1} I;r(87) { c1_0, c5_0 }.
% 0.96/1.33 (110) {G5,W2,D1,L2,V0,M1} I;r(109) { alpha61, ! c3_0 }.
% 0.96/1.33 (112) {G0,W2,D1,L2,V0,M1} I { alpha61, ! alpha74 }.
% 0.96/1.33 (113) {G0,W2,D1,L2,V0,M1} I { alpha61, ! alpha88 }.
% 0.96/1.33 (128) {G0,W2,D1,L2,V0,M1} I { alpha74, ! alpha89 }.
% 0.96/1.33 (23) {G0,W3,D2,L2,V0,M1} I { c5_1( a491 ), ! alpha69 }.
% 0.96/1.33 (132) {G0,W2,D1,L2,V0,M1} I { alpha89, ! alpha100 }.
% 0.96/1.33 (155) {G6,W2,D1,L2,V0,M1} I;r(154) { alpha36, alpha48 }.
% 0.96/1.33 (177) {G0,W2,D1,L2,V0,M1} I { alpha36, ! alpha49 }.
% 0.96/1.33 (22) {G0,W3,D2,L2,V0,M1} I { c3_1( a491 ), ! alpha69 }.
% 0.96/1.33 (180) {G0,W2,D1,L2,V0,M1} I { alpha49, ! alpha63 }.
% 0.96/1.33 (181) {G0,W2,D1,L2,V0,M1} I { alpha49, ! c5_0 }.
% 0.96/1.33 (182) {G0,W2,D1,L2,V0,M1} I { alpha77, ! alpha63 }.
% 0.96/1.33 (185) {G0,W2,D1,L2,V0,M1} I { alpha91, ! alpha77 }.
% 0.96/1.33 (188) {G0,W2,D1,L2,V0,M1} I { alpha102, ! alpha91 }.
% 0.96/1.33 (197) {G7,W2,D1,L2,V0,M1} I;r(196) { alpha28, ! c3_0 }.
% 0.96/1.33 (199) {G0,W2,D1,L2,V0,M1} I { alpha28, ! c4_0 }.
% 0.96/1.33 (20) {G1,W2,D1,L2,V0,M1} I;r(9) { c3_0, alpha69 }.
% 0.96/1.33 (200) {G0,W2,D1,L2,V0,M1} I { alpha28, ! alpha37 }.
% 0.96/1.33 (201) {G0,W2,D1,L2,V0,M1} I { alpha50, ! alpha37 }.
% 0.96/1.33 (202) {G0,W2,D1,L2,V0,M1} I { alpha64, ! alpha37 }.
% 0.96/1.33 (206) {G0,W2,D1,L2,V0,M1} I { alpha64, ! alpha78 }.
% 0.96/1.33 (19) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c5_2( X, a489 ), alpha93( X
% 0.96/1.33 ), ! c3_2( X, a489 ) }.
% 0.96/1.33 (369) {G10,W2,D1,L2,V0,M1} R(367,221) { alpha21, alpha65 }.
% 0.96/1.33 (368) {G10,W2,D1,L2,V0,M1} R(367,220) { alpha21, alpha51 }.
% 0.96/1.33 (367) {G9,W2,D1,L2,V0,M1} R(216,217) { alpha21, alpha38 }.
% 0.96/1.33 (18) {G0,W5,D2,L2,V1,M1} I { ! alpha93( X ), c5_2( X, a489 ) }.
% 0.96/1.33 (216) {G8,W2,D1,L2,V0,M1} I;r(215) { alpha21, alpha29 }.
% 0.96/1.33 (217) {G0,W2,D1,L2,V0,M1} I { alpha38, ! alpha29 }.
% 0.96/1.33 (220) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha38 }.
% 0.96/1.33 (221) {G0,W2,D1,L2,V0,M1} I { alpha65, ! alpha38 }.
% 0.96/1.33 (17) {G0,W5,D2,L2,V1,M1} I { ! alpha93( X ), c3_2( X, a489 ) }.
% 0.96/1.33 (225) {G0,W2,D1,L2,V0,M1} I { alpha65, ! alpha79 }.
% 0.96/1.33 (234) {G0,W2,D1,L2,V0,M1} I { alpha21, ! alpha30 }.
% 0.96/1.33 (235) {G0,W2,D1,L2,V0,M1} I { alpha21, ! alpha39 }.
% 0.96/1.33 (16) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha93( X ) }.
% 0.96/1.33 (250) {G0,W2,D1,L2,V0,M1} I { alpha30, ! alpha40 }.
% 0.96/1.33 (254) {G0,W2,D1,L2,V0,M1} I { alpha40, ! alpha53 }.
% 0.96/1.33 (15) {G0,W7,D2,L3,V1,M1} I { ! alpha93( X ), alpha83( X ), c2_2( X, a489 )
% 0.96/1.33 }.
% 0.96/1.33 (261) {G9,W2,D1,L2,V0,M1} I;r(260) { alpha15, alpha22 }.
% 0.96/1.33 (283) {G0,W2,D1,L2,V0,M1} I { alpha15, ! c4_0 }.
% 0.96/1.33 (284) {G0,W2,D1,L2,V0,M1} I { c2_0, alpha15 }.
% 0.96/1.33 (14) {G0,W5,D2,L2,V1,M1} I { ! alpha83( X ), ! c2_2( X, a489 ) }.
% 0.96/1.33 (287) {G9,W2,D1,L2,V0,M1} I;r(259) { ! c2_0, ! c3_0 }.
% 0.96/1.33 (357) {G15,W2,D1,L2,V0,M1} R(355,301) { alpha16, alpha81 }.
% 0.96/1.33 (359) {G16,W2,D1,L2,V0,M1} R(356,311) { alpha16, alpha82 }.
% 0.96/1.33 (362) {G19,W1,D1,L1,V0,M1} R(361,323);r(326) { ndr1_0 }.
% 0.96/1.33 (13) {G0,W4,D2,L2,V1,M1} I { ! alpha83( X ), alpha93( X ) }.
% 0.96/1.33 (356) {G15,W2,D1,L2,V0,M1} R(355,300) { alpha16, alpha67 }.
% 0.96/1.33 (12) {G0,W4,D2,L2,V1,M1} I { alpha68( X ), ! alpha83( X ) }.
% 0.96/1.33 (355) {G14,W2,D1,L2,V0,M1} R(354,297) { alpha16, alpha56 }.
% 0.96/1.33 (354) {G13,W2,D1,L2,V0,M1} R(353,294) { alpha16, alpha43 }.
% 0.96/1.33 (353) {G12,W2,D1,L2,V0,M1} R(290,291) { alpha16, alpha32 }.
% 0.96/1.33 (290) {G11,W2,D1,L2,V0,M1} I;r(289) { alpha16, alpha23 }.
% 0.96/1.33 (11) {G0,W4,D2,L2,V1,M1} I { ! c2_1( X ), alpha68( X ) }.
% 0.96/1.33 (291) {G0,W2,D1,L2,V0,M1} I { alpha32, ! alpha23 }.
% 0.96/1.33 (294) {G0,W2,D1,L2,V0,M1} I { alpha43, ! alpha32 }.
% 0.96/1.33 (297) {G0,W2,D1,L2,V0,M1} I { alpha56, ! alpha43 }.
% 0.96/1.33 (300) {G0,W2,D1,L2,V0,M1} I { alpha67, ! alpha56 }.
% 0.96/1.33 (10) {G0,W6,D2,L3,V1,M1} I { c2_1( X ), ! alpha68( X ), alpha83( X ) }.
% 0.96/1.33 (301) {G0,W2,D1,L2,V0,M1} I { alpha81, ! alpha56 }.
% 0.96/1.33 (305) {G0,W2,D1,L2,V0,M1} I { alpha81, ! alpha92 }.
% 0.96/1.33 (311) {G0,W2,D1,L2,V0,M1} I { alpha82, ! alpha67 }.
% 0.96/1.33 (317) {G0,W2,D1,L2,V0,M1} I { alpha24, ! alpha16 }.
% 0.96/1.33 (320) {G0,W2,D1,L2,V0,M1} I { alpha33, ! alpha24 }.
% 0.96/1.33 (323) {G0,W2,D1,L2,V0,M1} I { alpha44, ! alpha33 }.
% 0.96/1.33 (335) {G13,W2,D1,L2,V0,M1} I;r(334) { c1_0, alpha17 }.
% 0.96/1.33 (351) {G1,W2,D1,L2,V0,M1} R(337,341) { c3_0, alpha17 }.
% 0.96/1.33 (337) {G0,W2,D1,L2,V0,M1} I { alpha17, ! alpha25 }.
% 0.96/1.33 (341) {G0,W2,D1,L2,V0,M1} I { c3_0, alpha25 }.
% 0.96/1.33 (343) {G13,W2,D1,L2,V0,M1} I;r(333) { alpha12, ! c1_0 }.
% 0.96/1.33 (345) {G0,W2,D1,L2,V0,M1} I { alpha12, ! c2_0 }.
% 0.96/1.33 (346) {G0,W2,D1,L2,V0,M1} I { alpha12, ! alpha18 }.
% 0.96/1.33 (9) {G0,W1,D1,L1,V0,M1} I { alpha57 }.
% 0.96/1.33 (55) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha46 }.
% 0.96/1.33 (4) {G0,W1,D1,L1,V0,M1} I { alpha45 }.
% 0.96/1.33 (56) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha59 }.
% 0.96/1.33 (87) {G2,W1,D1,L1,V0,M1} I;r(55) { alpha26 }.
% 0.96/1.33 (88) {G2,W1,D1,L1,V0,M1} I;r(55) { alpha60 }.
% 0.96/1.33 (106) {G3,W1,D1,L1,V0,M1} I;r(87) { alpha35 }.
% 0.96/1.33 (108) {G4,W1,D1,L1,V0,M1} I;r(106) { alpha19 }.
% 0.96/1.33 (109) {G4,W1,D1,L1,V0,M1} I;r(106) { alpha47 }.
% 0.96/1.33 (153) {G5,W1,D1,L1,V0,M1} I;r(108) { alpha13 }.
% 0.96/1.33 (154) {G5,W1,D1,L1,V0,M1} I;r(108) { alpha27 }.
% 0.96/1.33 (195) {G6,W1,D1,L1,V0,M1} I;r(153) { alpha8 }.
% 0.96/1.33 (196) {G6,W1,D1,L1,V0,M1} I;r(153) { alpha20 }.
% 0.96/1.33 (214) {G7,W1,D1,L1,V0,M1} I;r(195) { alpha4 }.
% 0.96/1.33 (215) {G7,W1,D1,L1,V0,M1} I;r(195) { alpha14 }.
% 0.96/1.33 (259) {G8,W1,D1,L1,V0,M1} I;r(214) { alpha2 }.
% 0.96/1.33 (260) {G8,W1,D1,L1,V0,M1} I;r(214) { alpha9 }.
% 0.96/1.33 (286) {G9,W1,D1,L1,V0,M1} I;r(259) { alpha5 }.
% 0.96/1.33 (288) {G10,W1,D1,L1,V0,M1} I;r(286) { alpha1 }.
% 0.96/1.33 (0) {G0,W1,D1,L1,V0,M1} I { alpha34 }.
% 0.96/1.33 (289) {G10,W1,D1,L1,V0,M1} I;r(286) { alpha10 }.
% 0.96/1.33 (330) {G11,W1,D1,L1,V0,M1} I;r(288) { alpha3 }.
% 0.96/1.33 (331) {G11,W1,D1,L1,V0,M1} I;r(288) { alpha6 }.
% 0.96/1.33 (333) {G12,W1,D1,L1,V0,M1} I;r(330) { alpha7 }.
% 0.96/1.33 (334) {G12,W1,D1,L1,V0,M1} I;r(330) { alpha11 }.
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 % SZS output end Saturation
% 0.96/1.33 end of saturation!
% 0.96/1.33
% 0.96/1.33 Memory use:
% 0.96/1.33
% 0.96/1.33 space for terms: 9366
% 0.96/1.33 space for clauses: 30602
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 clauses generated: 1098
% 0.96/1.33 clauses kept: 695
% 0.96/1.33 clauses selected: 635
% 0.96/1.33 clauses deleted: 81
% 0.96/1.33 clauses inuse deleted: 21
% 0.96/1.33
% 0.96/1.33 subsentry: 560
% 0.96/1.33 literals s-matched: 327
% 0.96/1.33 literals matched: 327
% 0.96/1.33 full subsumption: 0
% 0.96/1.33
% 0.96/1.33 checksum: -480906021
% 0.96/1.33
% 0.96/1.33
% 0.96/1.33 Bliksem ended
%------------------------------------------------------------------------------