%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN515+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:23 EDT 2022
% Result : CounterSatisfiable 0.78s 1.16s
% Output : Saturation 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SYN515+1 : TPTP v8.1.0. Released v2.1.0.
% 0.03/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n008.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Tue Jul 12 02:23:53 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.73/1.14 *** allocated 10000 integers for termspace/termends
% 0.73/1.14 *** allocated 10000 integers for clauses
% 0.73/1.14 *** allocated 10000 integers for justifications
% 0.73/1.14 Bliksem 1.12
% 0.73/1.14
% 0.73/1.14
% 0.73/1.14 Automatic Strategy Selection
% 0.73/1.14
% 0.73/1.14
% 0.73/1.14 Clauses:
% 0.73/1.14
% 0.73/1.14 { alpha14 }.
% 0.73/1.14 { alpha22, ndr1_0 }.
% 0.73/1.14 { alpha22, ! c5_1( a26 ) }.
% 0.73/1.14 { alpha22, ! ndr1_1( a26 ), c2_2( a26, X ), c4_2( a26, X ), ! c1_2( a26, X
% 0.73/1.14 ) }.
% 0.73/1.14 { ! alpha22, alpha34, alpha48 }.
% 0.73/1.14 { ! alpha34, alpha22 }.
% 0.73/1.14 { ! alpha48, alpha22 }.
% 0.73/1.14 { ! alpha48, alpha66 }.
% 0.73/1.14 { ! alpha48, alpha85 }.
% 0.73/1.14 { ! alpha66, ! alpha85, alpha48 }.
% 0.73/1.14 { ! alpha85, ! ndr1_1( a24 ), alpha103 }.
% 0.73/1.14 { ndr1_1( a24 ), alpha85 }.
% 0.73/1.14 { ! alpha103, alpha85 }.
% 0.73/1.14 { ! alpha103, ! c4_2( a24, X ), c1_2( a24, X ), ! c3_2( a24, X ) }.
% 0.73/1.14 { c4_2( a24, skol1 ), alpha103 }.
% 0.73/1.14 { ! c1_2( a24, skol1 ), alpha103 }.
% 0.73/1.14 { c3_2( a24, skol1 ), alpha103 }.
% 0.73/1.14 { ! alpha66, alpha86 }.
% 0.73/1.14 { ! alpha66, c3_2( a24, a25 ) }.
% 0.73/1.14 { ! alpha86, ! c3_2( a24, a25 ), alpha66 }.
% 0.73/1.14 { ! alpha86, alpha104 }.
% 0.73/1.14 { ! alpha86, c1_2( a24, a25 ) }.
% 0.73/1.14 { ! alpha104, ! c1_2( a24, a25 ), alpha86 }.
% 0.73/1.14 { ! alpha104, alpha117 }.
% 0.73/1.14 { ! alpha104, ndr1_1( a24 ) }.
% 0.73/1.14 { ! alpha117, ! ndr1_1( a24 ), alpha104 }.
% 0.73/1.14 { ! alpha117, ndr1_0 }.
% 0.73/1.14 { ! alpha117, alpha128 }.
% 0.73/1.14 { ! ndr1_0, ! alpha128, alpha117 }.
% 0.73/1.14 { ! alpha128, ! ndr1_1( a24 ), alpha134 }.
% 0.73/1.14 { ndr1_1( a24 ), alpha128 }.
% 0.73/1.14 { ! alpha134, alpha128 }.
% 0.73/1.14 { ! alpha134, ! c1_2( a24, X ), ! c2_2( a24, X ), c4_2( a24, X ) }.
% 0.73/1.14 { c1_2( a24, skol2 ), alpha134 }.
% 0.73/1.14 { c2_2( a24, skol2 ), alpha134 }.
% 0.73/1.14 { ! c4_2( a24, skol2 ), alpha134 }.
% 0.73/1.14 { ! alpha34, ! ndr1_0, alpha49 }.
% 0.73/1.14 { ndr1_0, alpha34 }.
% 0.73/1.14 { ! alpha49, alpha34 }.
% 0.73/1.14 { ! alpha49, alpha67( X ), c5_2( X, Y ), c4_2( X, Y ) }.
% 0.73/1.14 { ! alpha67( skol3 ), alpha49 }.
% 0.73/1.14 { ! c5_2( skol3, skol24 ), alpha49 }.
% 0.73/1.14 { ! c4_2( skol3, skol24 ), alpha49 }.
% 0.73/1.14 { ! alpha67( X ), alpha87( X ), ! ndr1_1( X ) }.
% 0.73/1.14 { ! alpha87( X ), alpha67( X ) }.
% 0.73/1.14 { ndr1_1( X ), alpha67( X ) }.
% 0.73/1.14 { ! alpha87( X ), alpha105( X ), alpha118( X ) }.
% 0.73/1.14 { ! alpha105( X ), alpha87( X ) }.
% 0.73/1.14 { ! alpha118( X ), alpha87( X ) }.
% 0.73/1.14 { ! alpha118( X ), alpha129( X ) }.
% 0.73/1.14 { ! alpha118( X ), ! c5_2( X, a23 ) }.
% 0.73/1.14 { ! alpha129( X ), c5_2( X, a23 ), alpha118( X ) }.
% 0.73/1.14 { ! alpha129( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha129( X ), c2_2( X, a23 ) }.
% 0.73/1.14 { ! alpha129( X ), c4_2( X, a23 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c2_2( X, a23 ), ! c4_2( X, a23 ), alpha129( X ) }.
% 0.73/1.14 { ! alpha105( X ), alpha119( X ) }.
% 0.73/1.14 { ! alpha105( X ), c2_2( X, a22 ) }.
% 0.73/1.14 { ! alpha119( X ), ! c2_2( X, a22 ), alpha105( X ) }.
% 0.73/1.14 { ! alpha119( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha119( X ), c4_2( X, a22 ) }.
% 0.73/1.14 { ! alpha119( X ), c5_2( X, a22 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c4_2( X, a22 ), ! c5_2( X, a22 ), alpha119( X ) }.
% 0.73/1.14 { ! alpha14, alpha23 }.
% 0.73/1.14 { ! alpha14, alpha35 }.
% 0.73/1.14 { ! alpha23, ! alpha35, alpha14 }.
% 0.73/1.14 { ! alpha35, alpha50, c4_0 }.
% 0.73/1.14 { ! alpha50, alpha35 }.
% 0.73/1.14 { ! c4_0, alpha35 }.
% 0.73/1.14 { ! alpha50, alpha68, alpha88 }.
% 0.73/1.14 { ! alpha68, alpha50 }.
% 0.73/1.14 { ! alpha88, alpha50 }.
% 0.73/1.14 { ! alpha88, alpha106( X ), alpha120( X ) }.
% 0.73/1.14 { ! alpha106( skol4 ), alpha88 }.
% 0.73/1.14 { ! alpha120( skol4 ), alpha88 }.
% 0.73/1.14 { ! alpha120( X ), ! c2_2( X, Y ), ! c4_2( X, Y ), ! c1_2( X, Y ) }.
% 0.73/1.14 { c2_2( X, skol5( X ) ), alpha120( X ) }.
% 0.73/1.14 { c4_2( X, skol5( X ) ), alpha120( X ) }.
% 0.73/1.14 { c1_2( X, skol5( X ) ), alpha120( X ) }.
% 0.73/1.14 { ! alpha106( X ), alpha121( X ), ! ndr1_1( X ) }.
% 0.73/1.14 { ! alpha121( X ), alpha106( X ) }.
% 0.73/1.14 { ndr1_1( X ), alpha106( X ) }.
% 0.73/1.14 { ! alpha121( X ), ! c5_1( X ), alpha130( X ) }.
% 0.73/1.14 { c5_1( X ), alpha121( X ) }.
% 0.73/1.14 { ! alpha130( X ), alpha121( X ) }.
% 0.73/1.14 { ! alpha130( X ), alpha135( X ) }.
% 0.73/1.14 { ! alpha130( X ), c5_2( X, a21 ) }.
% 0.73/1.14 { ! alpha135( X ), ! c5_2( X, a21 ), alpha130( X ) }.
% 0.73/1.14 { ! alpha135( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha135( X ), ! c1_2( X, a21 ) }.
% 0.73/1.14 { ! alpha135( X ), ! c4_2( X, a21 ) }.
% 0.73/1.14 { ! ndr1_1( X ), c1_2( X, a21 ), c4_2( X, a21 ), alpha135( X ) }.
% 0.73/1.14 { ! alpha68, ! c3_0, ! ndr1_0 }.
% 0.73/1.14 { c3_0, alpha68 }.
% 0.73/1.14 { ndr1_0, alpha68 }.
% 0.73/1.14 { ! alpha23, alpha8 }.
% 0.73/1.14 { ! alpha23, alpha36 }.
% 0.73/1.14 { ! alpha8, ! alpha36, alpha23 }.
% 0.73/1.14 { ! alpha36, alpha51, alpha69 }.
% 0.73/1.14 { ! alpha51, alpha36 }.
% 0.73/1.14 { ! alpha69, alpha36 }.
% 0.73/1.14 { ! alpha69, alpha89 }.
% 0.73/1.14 { ! alpha69, alpha107 }.
% 0.73/1.14 { ! alpha89, ! alpha107, alpha69 }.
% 0.73/1.14 { ! alpha107, ! ndr1_1( a19 ), ! c3_2( a19, X ), ! c4_2( a19, X ) }.
% 0.73/1.14 { ndr1_1( a19 ), alpha107 }.
% 0.73/1.14 { c3_2( a19, skol6 ), alpha107 }.
% 0.73/1.14 { c4_2( a19, skol6 ), alpha107 }.
% 0.73/1.14 { ! alpha89, alpha108 }.
% 0.73/1.14 { ! alpha89, ! c4_2( a19, a20 ) }.
% 0.73/1.14 { ! alpha108, c4_2( a19, a20 ), alpha89 }.
% 0.73/1.14 { ! alpha108, alpha122 }.
% 0.73/1.14 { ! alpha108, c3_2( a19, a20 ) }.
% 0.73/1.14 { ! alpha122, ! c3_2( a19, a20 ), alpha108 }.
% 0.73/1.14 { ! alpha122, ndr1_0 }.
% 0.73/1.14 { ! alpha122, ! c2_1( a19 ) }.
% 0.73/1.14 { ! alpha122, ndr1_1( a19 ) }.
% 0.73/1.14 { ! ndr1_0, c2_1( a19 ), ! ndr1_1( a19 ), alpha122 }.
% 0.73/1.14 { ! alpha51, alpha70, alpha90 }.
% 0.73/1.14 { ! alpha70, alpha51 }.
% 0.73/1.14 { ! alpha90, alpha51 }.
% 0.73/1.14 { ! alpha90, ! c4_1( X ), ! c3_1( X ), ! c2_1( X ) }.
% 0.73/1.14 { c4_1( skol7 ), alpha90 }.
% 0.73/1.14 { c3_1( skol7 ), alpha90 }.
% 0.73/1.14 { c2_1( skol7 ), alpha90 }.
% 0.73/1.14 { ! alpha70, ! c4_0, ! ndr1_0 }.
% 0.73/1.14 { c4_0, alpha70 }.
% 0.73/1.14 { ndr1_0, alpha70 }.
% 0.73/1.14 { ! alpha8, alpha15 }.
% 0.73/1.14 { ! alpha8, alpha24 }.
% 0.73/1.14 { ! alpha15, ! alpha24, alpha8 }.
% 0.73/1.14 { ! alpha24, alpha37, alpha52 }.
% 0.73/1.14 { ! alpha37, alpha24 }.
% 0.73/1.14 { ! alpha52, alpha24 }.
% 0.73/1.14 { ! alpha52, alpha71( X ), alpha91( X ) }.
% 0.73/1.14 { ! alpha71( skol8 ), alpha52 }.
% 0.73/1.14 { ! alpha91( skol8 ), alpha52 }.
% 0.73/1.14 { ! alpha91( X ), ! c4_2( X, Y ), c3_2( X, Y ), c1_2( X, Y ) }.
% 0.73/1.14 { c4_2( X, skol9( X ) ), alpha91( X ) }.
% 0.73/1.14 { ! c3_2( X, skol9( X ) ), alpha91( X ) }.
% 0.73/1.14 { ! c1_2( X, skol9( X ) ), alpha91( X ) }.
% 0.73/1.14 { ! alpha71( X ), alpha92( X ), ! ndr1_1( X ) }.
% 0.73/1.14 { ! alpha92( X ), alpha71( X ) }.
% 0.73/1.14 { ndr1_1( X ), alpha71( X ) }.
% 0.73/1.14 { ! alpha92( X ), alpha109( X ), c1_1( X ) }.
% 0.73/1.14 { ! alpha109( X ), alpha92( X ) }.
% 0.73/1.14 { ! c1_1( X ), alpha92( X ) }.
% 0.73/1.14 { ! alpha109( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha109( X ), c2_2( X, a18 ) }.
% 0.73/1.14 { ! alpha109( X ), c3_2( X, a18 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c2_2( X, a18 ), ! c3_2( X, a18 ), alpha109( X ) }.
% 0.73/1.14 { ! alpha37, alpha53, ! ndr1_0 }.
% 0.73/1.14 { ! alpha53, alpha37 }.
% 0.73/1.14 { ndr1_0, alpha37 }.
% 0.73/1.14 { ! alpha53, alpha72, ! c5_0 }.
% 0.73/1.14 { ! alpha72, alpha53 }.
% 0.73/1.14 { c5_0, alpha53 }.
% 0.73/1.14 { ! alpha72, ! ndr1_0, alpha93 }.
% 0.73/1.14 { ndr1_0, alpha72 }.
% 0.73/1.14 { ! alpha93, alpha72 }.
% 0.73/1.14 { ! alpha93, alpha110( X ), alpha123( X ) }.
% 0.73/1.14 { ! alpha110( skol10 ), alpha93 }.
% 0.73/1.14 { ! alpha123( skol10 ), alpha93 }.
% 0.73/1.14 { ! alpha123( X ), alpha131( X ) }.
% 0.73/1.14 { ! alpha123( X ), ! c4_2( X, a17 ) }.
% 0.73/1.14 { ! alpha131( X ), c4_2( X, a17 ), alpha123( X ) }.
% 0.73/1.14 { ! alpha131( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha131( X ), c5_2( X, a17 ) }.
% 0.73/1.14 { ! alpha131( X ), c1_2( X, a17 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c5_2( X, a17 ), ! c1_2( X, a17 ), alpha131( X ) }.
% 0.73/1.14 { ! alpha110( X ), ! c5_1( X ), ! c2_1( X ) }.
% 0.73/1.14 { c5_1( X ), alpha110( X ) }.
% 0.73/1.14 { c2_1( X ), alpha110( X ) }.
% 0.73/1.14 { ! alpha15, alpha4 }.
% 0.73/1.14 { ! alpha15, alpha25 }.
% 0.73/1.14 { ! alpha4, ! alpha25, alpha15 }.
% 0.73/1.14 { ! alpha25, alpha38, alpha54 }.
% 0.73/1.14 { ! alpha38, alpha25 }.
% 0.73/1.14 { ! alpha54, alpha25 }.
% 0.73/1.14 { ! alpha54, alpha73 }.
% 0.73/1.14 { ! alpha54, ! c5_1( a16 ) }.
% 0.73/1.14 { ! alpha73, c5_1( a16 ), alpha54 }.
% 0.73/1.14 { ! alpha73, alpha94 }.
% 0.73/1.14 { ! alpha73, ! c3_1( a16 ) }.
% 0.73/1.14 { ! alpha94, c3_1( a16 ), alpha73 }.
% 0.73/1.14 { ! alpha94, ndr1_0 }.
% 0.73/1.14 { ! alpha94, alpha111 }.
% 0.73/1.14 { ! ndr1_0, ! alpha111, alpha94 }.
% 0.73/1.14 { ! alpha111, ! ndr1_1( a16 ), alpha124 }.
% 0.73/1.14 { ndr1_1( a16 ), alpha111 }.
% 0.73/1.14 { ! alpha124, alpha111 }.
% 0.73/1.14 { ! alpha124, ! c4_2( a16, X ), ! c1_2( a16, X ), ! c3_2( a16, X ) }.
% 0.73/1.14 { c4_2( a16, skol11 ), alpha124 }.
% 0.73/1.14 { c1_2( a16, skol11 ), alpha124 }.
% 0.73/1.14 { c3_2( a16, skol11 ), alpha124 }.
% 0.73/1.14 { ! alpha38, alpha55, alpha74 }.
% 0.73/1.14 { ! alpha55, alpha38 }.
% 0.73/1.14 { ! alpha74, alpha38 }.
% 0.73/1.14 { ! alpha74, alpha95 }.
% 0.73/1.14 { ! alpha74, ! c2_2( a14, a15 ) }.
% 0.73/1.14 { ! alpha95, c2_2( a14, a15 ), alpha74 }.
% 0.73/1.14 { ! alpha95, alpha112 }.
% 0.73/1.14 { ! alpha95, c1_2( a14, a15 ) }.
% 0.73/1.14 { ! alpha112, ! c1_2( a14, a15 ), alpha95 }.
% 0.73/1.14 { ! alpha112, alpha125 }.
% 0.73/1.14 { ! alpha112, ! c3_2( a14, a15 ) }.
% 0.73/1.14 { ! alpha125, c3_2( a14, a15 ), alpha112 }.
% 0.73/1.14 { ! alpha125, alpha132 }.
% 0.73/1.14 { ! alpha125, ndr1_1( a14 ) }.
% 0.73/1.14 { ! alpha132, ! ndr1_1( a14 ), alpha125 }.
% 0.73/1.14 { ! alpha132, alpha136 }.
% 0.73/1.14 { ! alpha132, c5_1( a14 ) }.
% 0.73/1.14 { ! alpha136, ! c5_1( a14 ), alpha132 }.
% 0.73/1.14 { ! alpha136, ndr1_0 }.
% 0.73/1.14 { ! alpha136, alpha137 }.
% 0.73/1.14 { ! ndr1_0, ! alpha137, alpha136 }.
% 0.73/1.14 { ! alpha137, ! ndr1_1( a14 ), c5_2( a14, X ), ! c3_2( a14, X ) }.
% 0.73/1.14 { ndr1_1( a14 ), alpha137 }.
% 0.73/1.14 { ! c5_2( a14, skol12 ), alpha137 }.
% 0.73/1.14 { c3_2( a14, skol12 ), alpha137 }.
% 0.73/1.14 { ! alpha55, ! ndr1_0, c2_1( X ), c5_1( X ) }.
% 0.73/1.14 { ndr1_0, alpha55 }.
% 0.73/1.14 { ! c2_1( skol13 ), alpha55 }.
% 0.73/1.14 { ! c5_1( skol13 ), alpha55 }.
% 0.73/1.14 { ! alpha4, alpha9 }.
% 0.73/1.14 { ! alpha4, alpha16 }.
% 0.73/1.14 { ! alpha9, ! alpha16, alpha4 }.
% 0.73/1.14 { ! alpha16, alpha26, alpha39 }.
% 0.73/1.14 { ! alpha26, alpha16 }.
% 0.73/1.14 { ! alpha39, alpha16 }.
% 0.73/1.14 { ! alpha39, alpha56 }.
% 0.73/1.14 { ! alpha39, alpha75 }.
% 0.73/1.14 { ! alpha56, ! alpha75, alpha39 }.
% 0.73/1.14 { ! alpha75, ! ndr1_1( a13 ), c4_2( a13, X ), c3_2( a13, X ) }.
% 0.73/1.14 { ndr1_1( a13 ), alpha75 }.
% 0.73/1.14 { ! c4_2( a13, skol14 ), alpha75 }.
% 0.73/1.14 { ! c3_2( a13, skol14 ), alpha75 }.
% 0.73/1.14 { ! alpha56, alpha76 }.
% 0.73/1.14 { ! alpha56, alpha96 }.
% 0.73/1.14 { ! alpha76, ! alpha96, alpha56 }.
% 0.73/1.14 { ! alpha96, ! ndr1_1( a13 ), alpha113 }.
% 0.73/1.14 { ndr1_1( a13 ), alpha96 }.
% 0.73/1.14 { ! alpha113, alpha96 }.
% 0.73/1.14 { ! alpha113, c1_2( a13, X ), c3_2( a13, X ), ! c5_2( a13, X ) }.
% 0.73/1.14 { ! c1_2( a13, skol15 ), alpha113 }.
% 0.73/1.14 { ! c3_2( a13, skol15 ), alpha113 }.
% 0.73/1.14 { c5_2( a13, skol15 ), alpha113 }.
% 0.73/1.14 { ! alpha76, ndr1_0 }.
% 0.73/1.14 { ! alpha76, ! c4_1( a13 ) }.
% 0.73/1.14 { ! ndr1_0, c4_1( a13 ), alpha76 }.
% 0.73/1.14 { ! alpha26, c4_0, alpha40 }.
% 0.73/1.14 { ! c4_0, alpha26 }.
% 0.73/1.14 { ! alpha40, alpha26 }.
% 0.73/1.14 { ! alpha40, alpha57 }.
% 0.73/1.14 { ! alpha40, ! c5_1( a12 ) }.
% 0.73/1.14 { ! alpha57, c5_1( a12 ), alpha40 }.
% 0.73/1.14 { ! alpha57, ndr1_0 }.
% 0.73/1.14 { ! alpha57, c4_1( a12 ) }.
% 0.73/1.14 { ! alpha57, c3_1( a12 ) }.
% 0.73/1.14 { ! ndr1_0, ! c4_1( a12 ), ! c3_1( a12 ), alpha57 }.
% 0.73/1.14 { ! alpha9, alpha17 }.
% 0.73/1.14 { ! alpha9, alpha27 }.
% 0.73/1.14 { ! alpha17, ! alpha27, alpha9 }.
% 0.73/1.14 { ! alpha27, alpha41, ! c4_0 }.
% 0.73/1.14 { ! alpha41, alpha27 }.
% 0.73/1.14 { c4_0, alpha27 }.
% 0.73/1.14 { ! alpha41, alpha58, alpha77 }.
% 0.73/1.14 { ! alpha58, alpha41 }.
% 0.73/1.14 { ! alpha77, alpha41 }.
% 0.73/1.14 { ! alpha77, alpha97 }.
% 0.73/1.14 { ! alpha77, c1_1( a10 ) }.
% 0.73/1.14 { ! alpha97, ! c1_1( a10 ), alpha77 }.
% 0.73/1.14 { ! alpha97, alpha114 }.
% 0.73/1.14 { ! alpha97, ! c1_2( a10, a11 ) }.
% 0.73/1.14 { ! alpha114, c1_2( a10, a11 ), alpha97 }.
% 0.73/1.14 { ! alpha114, alpha126 }.
% 0.73/1.14 { ! alpha114, c2_2( a10, a11 ) }.
% 0.73/1.14 { ! alpha126, ! c2_2( a10, a11 ), alpha114 }.
% 0.73/1.14 { ! alpha126, alpha133 }.
% 0.73/1.14 { ! alpha126, c5_2( a10, a11 ) }.
% 0.73/1.14 { ! alpha133, ! c5_2( a10, a11 ), alpha126 }.
% 0.73/1.14 { ! alpha133, ndr1_0 }.
% 0.73/1.14 { ! alpha133, c5_1( a10 ) }.
% 0.73/1.14 { ! alpha133, ndr1_1( a10 ) }.
% 0.73/1.14 { ! ndr1_0, ! c5_1( a10 ), ! ndr1_1( a10 ), alpha133 }.
% 0.73/1.14 { ! alpha58, alpha78 }.
% 0.73/1.14 { ! alpha58, c1_2( a8, a9 ) }.
% 0.73/1.14 { ! alpha78, ! c1_2( a8, a9 ), alpha58 }.
% 0.73/1.14 { ! alpha78, alpha98 }.
% 0.73/1.14 { ! alpha78, c3_2( a8, a9 ) }.
% 0.73/1.14 { ! alpha98, ! c3_2( a8, a9 ), alpha78 }.
% 0.73/1.14 { ! alpha98, alpha115 }.
% 0.73/1.14 { ! alpha98, ! c2_2( a8, a9 ) }.
% 0.73/1.14 { ! alpha115, c2_2( a8, a9 ), alpha98 }.
% 0.73/1.14 { ! alpha115, alpha127 }.
% 0.73/1.14 { ! alpha115, ndr1_1( a8 ) }.
% 0.73/1.14 { ! alpha127, ! ndr1_1( a8 ), alpha115 }.
% 0.73/1.14 { ! alpha127, ndr1_0 }.
% 0.73/1.14 { ! alpha127, ! c3_1( a8 ) }.
% 0.73/1.14 { ! alpha127, c1_1( a8 ) }.
% 0.73/1.14 { ! ndr1_0, c3_1( a8 ), ! c1_1( a8 ), alpha127 }.
% 0.73/1.14 { ! alpha17, alpha2 }.
% 0.73/1.14 { ! alpha17, alpha28 }.
% 0.73/1.14 { ! alpha2, ! alpha28, alpha17 }.
% 0.73/1.14 { ! alpha28, alpha42, c2_0 }.
% 0.73/1.14 { ! alpha42, alpha28 }.
% 0.73/1.14 { ! c2_0, alpha28 }.
% 0.73/1.14 { ! alpha42, ! c1_0, alpha59 }.
% 0.73/1.14 { c1_0, alpha42 }.
% 0.73/1.14 { ! alpha59, alpha42 }.
% 0.73/1.14 { ! alpha59, alpha79 }.
% 0.73/1.14 { ! alpha59, c4_1( a7 ) }.
% 0.73/1.14 { ! alpha79, ! c4_1( a7 ), alpha59 }.
% 0.73/1.14 { ! alpha79, ndr1_0 }.
% 0.73/1.14 { ! alpha79, ! c1_1( a7 ) }.
% 0.73/1.14 { ! alpha79, ! c3_1( a7 ) }.
% 0.73/1.14 { ! ndr1_0, c1_1( a7 ), c3_1( a7 ), alpha79 }.
% 0.73/1.14 { ! alpha2, alpha5 }.
% 0.73/1.14 { ! alpha2, alpha10 }.
% 0.73/1.14 { ! alpha5, ! alpha10, alpha2 }.
% 0.73/1.14 { ! alpha10, ! c4_0, ! c1_0, c5_0 }.
% 0.73/1.14 { c4_0, alpha10 }.
% 0.73/1.14 { c1_0, alpha10 }.
% 0.73/1.14 { ! c5_0, alpha10 }.
% 0.73/1.14 { ! alpha5, alpha1 }.
% 0.73/1.14 { ! alpha5, alpha11 }.
% 0.73/1.14 { ! alpha1, ! alpha11, alpha5 }.
% 0.73/1.14 { ! alpha11, alpha18, alpha29 }.
% 0.73/1.14 { ! alpha18, alpha11 }.
% 0.73/1.14 { ! alpha29, alpha11 }.
% 0.73/1.14 { ! alpha29, alpha43( X ), alpha60( X ) }.
% 0.73/1.14 { ! alpha43( skol16 ), alpha29 }.
% 0.73/1.14 { ! alpha60( skol16 ), alpha29 }.
% 0.73/1.14 { ! alpha60( X ), alpha80( X ) }.
% 0.73/1.14 { ! alpha60( X ), ! c5_2( X, a6 ) }.
% 0.73/1.14 { ! alpha80( X ), c5_2( X, a6 ), alpha60( X ) }.
% 0.73/1.14 { ! alpha80( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha80( X ), c3_2( X, a6 ) }.
% 0.73/1.14 { ! alpha80( X ), c2_2( X, a6 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c3_2( X, a6 ), ! c2_2( X, a6 ), alpha80( X ) }.
% 0.73/1.14 { ! alpha43( X ), ! c3_1( X ), alpha61( X ) }.
% 0.73/1.14 { c3_1( X ), alpha43( X ) }.
% 0.73/1.14 { ! alpha61( X ), alpha43( X ) }.
% 0.73/1.14 { ! alpha61( X ), alpha81( X ) }.
% 0.73/1.14 { ! alpha61( X ), ! c1_2( X, a5 ) }.
% 0.73/1.14 { ! alpha81( X ), c1_2( X, a5 ), alpha61( X ) }.
% 0.73/1.14 { ! alpha81( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha81( X ), ! c5_2( X, a5 ) }.
% 0.73/1.14 { ! alpha81( X ), c4_2( X, a5 ) }.
% 0.73/1.14 { ! ndr1_1( X ), c5_2( X, a5 ), ! c4_2( X, a5 ), alpha81( X ) }.
% 0.73/1.14 { ! alpha18, alpha30, ! ndr1_0 }.
% 0.73/1.14 { ! alpha30, alpha18 }.
% 0.73/1.14 { ndr1_0, alpha18 }.
% 0.73/1.14 { ! alpha30, c4_0, alpha44 }.
% 0.73/1.14 { ! c4_0, alpha30 }.
% 0.73/1.14 { ! alpha44, alpha30 }.
% 0.73/1.14 { ! alpha44, alpha62 }.
% 0.73/1.14 { ! alpha44, alpha82 }.
% 0.73/1.14 { ! alpha62, ! alpha82, alpha44 }.
% 0.73/1.14 { ! alpha82, ! ndr1_1( a4 ), alpha99 }.
% 0.73/1.14 { ndr1_1( a4 ), alpha82 }.
% 0.73/1.14 { ! alpha99, alpha82 }.
% 0.73/1.14 { ! alpha99, c4_2( a4, X ), ! c3_2( a4, X ), ! c5_2( a4, X ) }.
% 0.73/1.14 { ! c4_2( a4, skol17 ), alpha99 }.
% 0.73/1.14 { c3_2( a4, skol17 ), alpha99 }.
% 0.73/1.14 { c5_2( a4, skol17 ), alpha99 }.
% 0.73/1.14 { ! alpha62, alpha83 }.
% 0.73/1.14 { ! alpha62, alpha100 }.
% 0.73/1.14 { ! alpha83, ! alpha100, alpha62 }.
% 0.73/1.14 { ! alpha100, ! ndr1_1( a4 ), c3_2( a4, X ), ! c2_2( a4, X ) }.
% 0.73/1.14 { ndr1_1( a4 ), alpha100 }.
% 0.73/1.14 { ! c3_2( a4, skol18 ), alpha100 }.
% 0.73/1.14 { c2_2( a4, skol18 ), alpha100 }.
% 0.73/1.14 { ! alpha83, ndr1_0 }.
% 0.73/1.14 { ! alpha83, alpha101 }.
% 0.73/1.14 { ! ndr1_0, ! alpha101, alpha83 }.
% 0.73/1.14 { ! alpha101, ! ndr1_1( a4 ), alpha116 }.
% 0.73/1.14 { ndr1_1( a4 ), alpha101 }.
% 0.73/1.14 { ! alpha116, alpha101 }.
% 0.73/1.14 { ! alpha116, ! c4_2( a4, X ), ! c5_2( a4, X ), c3_2( a4, X ) }.
% 0.73/1.14 { c4_2( a4, skol19 ), alpha116 }.
% 0.73/1.14 { c5_2( a4, skol19 ), alpha116 }.
% 0.73/1.14 { ! c3_2( a4, skol19 ), alpha116 }.
% 0.73/1.14 { ! alpha1, alpha3 }.
% 0.73/1.14 { ! alpha1, alpha6 }.
% 0.73/1.14 { ! alpha3, ! alpha6, alpha1 }.
% 0.73/1.14 { ! alpha6, alpha12, alpha19 }.
% 0.73/1.14 { ! alpha12, alpha6 }.
% 0.73/1.14 { ! alpha19, alpha6 }.
% 0.73/1.14 { ! alpha19, alpha31( X ), alpha45( X ) }.
% 0.73/1.14 { ! alpha31( skol20 ), alpha19 }.
% 0.73/1.14 { ! alpha45( skol20 ), alpha19 }.
% 0.73/1.14 { ! alpha45( X ), ! c5_2( X, Y ), ! c3_2( X, Y ), ! c4_2( X, Y ) }.
% 0.73/1.14 { c5_2( X, skol21( X ) ), alpha45( X ) }.
% 0.73/1.14 { c3_2( X, skol21( X ) ), alpha45( X ) }.
% 0.73/1.14 { c4_2( X, skol21( X ) ), alpha45( X ) }.
% 0.73/1.14 { ! alpha31( X ), ! c3_1( X ), ! c5_1( X ), ! ndr1_1( X ) }.
% 0.73/1.14 { c3_1( X ), alpha31( X ) }.
% 0.73/1.14 { c5_1( X ), alpha31( X ) }.
% 0.73/1.14 { ndr1_1( X ), alpha31( X ) }.
% 0.73/1.14 { ! alpha12, alpha20, ! ndr1_0 }.
% 0.73/1.14 { ! alpha20, alpha12 }.
% 0.73/1.14 { ndr1_0, alpha12 }.
% 0.73/1.14 { ! alpha20, alpha32, c1_0 }.
% 0.73/1.14 { ! alpha32, alpha20 }.
% 0.73/1.14 { ! c1_0, alpha20 }.
% 0.73/1.14 { ! alpha32, alpha46 }.
% 0.73/1.14 { ! alpha32, ! c3_1( a3 ) }.
% 0.73/1.14 { ! alpha46, c3_1( a3 ), alpha32 }.
% 0.73/1.14 { ! alpha46, alpha63 }.
% 0.73/1.14 { ! alpha46, ! c5_1( a3 ) }.
% 0.73/1.14 { ! alpha63, c5_1( a3 ), alpha46 }.
% 0.73/1.14 { ! alpha63, ndr1_0 }.
% 0.73/1.14 { ! alpha63, alpha84 }.
% 0.73/1.14 { ! ndr1_0, ! alpha84, alpha63 }.
% 0.73/1.14 { ! alpha84, ! ndr1_1( a3 ), alpha102 }.
% 0.73/1.14 { ndr1_1( a3 ), alpha84 }.
% 0.73/1.14 { ! alpha102, alpha84 }.
% 0.73/1.14 { ! alpha102, ! c5_2( a3, X ), ! c1_2( a3, X ), c3_2( a3, X ) }.
% 0.73/1.14 { c5_2( a3, skol22 ), alpha102 }.
% 0.73/1.14 { c1_2( a3, skol22 ), alpha102 }.
% 0.73/1.14 { ! c3_2( a3, skol22 ), alpha102 }.
% 0.73/1.14 { ! alpha3, alpha7, c5_0 }.
% 0.73/1.14 { ! alpha7, alpha3 }.
% 0.73/1.14 { ! c5_0, alpha3 }.
% 0.73/1.14 { ! alpha7, alpha13, ! c3_0 }.
% 0.73/1.14 { ! alpha13, alpha7 }.
% 0.73/1.14 { c3_0, alpha7 }.
% 0.73/1.14 { ! alpha13, ! ndr1_0, alpha21 }.
% 0.73/1.14 { ndr1_0, alpha13 }.
% 0.73/1.14 { ! alpha21, alpha13 }.
% 0.73/1.14 { ! alpha21, alpha33( X ), ! c1_1( X ) }.
% 0.73/1.14 { ! alpha33( skol23 ), alpha21 }.
% 0.73/1.14 { c1_1( skol23 ), alpha21 }.
% 0.73/1.14 { ! alpha33( X ), alpha47( X ), alpha64( X ) }.
% 0.73/1.14 { ! alpha47( X ), alpha33( X ) }.
% 0.73/1.14 { ! alpha64( X ), alpha33( X ) }.
% 0.73/1.14 { ! alpha64( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha64( X ), c3_2( X, a2 ) }.
% 0.73/1.14 { ! alpha64( X ), ! c5_2( X, a2 ) }.
% 0.73/1.14 { ! ndr1_1( X ), ! c3_2( X, a2 ), c5_2( X, a2 ), alpha64( X ) }.
% 0.73/1.14 { ! alpha47( X ), alpha65( X ) }.
% 0.73/1.14 { ! alpha47( X ), ! c1_2( X, a1 ) }.
% 0.73/1.14 { ! alpha65( X ), c1_2( X, a1 ), alpha47( X ) }.
% 0.73/1.14 { ! alpha65( X ), ndr1_1( X ) }.
% 0.73/1.14 { ! alpha65( X ), ! c3_2( X, a1 ) }.
% 0.73/1.14 { ! alpha65( X ), c5_2( X, a1 ) }.
% 0.73/1.14 { ! ndr1_1( X ), c3_2( X, a1 ), ! c5_2( X, a1 ), alpha65( X ) }.
% 0.73/1.14
% 0.73/1.14 *** allocated 15000 integers for clauses
% 0.73/1.14 percentage equality = 0.000000, percentage horn = 0.727069
% 0.73/1.14 This a non-horn, non-equality problem
% 0.73/1.14
% 0.73/1.14
% 0.73/1.14 Options Used:
% 0.73/1.14
% 0.73/1.14 useres = 1
% 0.73/1.14 useparamod = 0
% 0.73/1.14 useeqrefl = 0
% 0.73/1.14 useeqfact = 0
% 0.73/1.14 usefactor = 1
% 0.73/1.14 usesimpsplitting = 0
% 0.73/1.14 usesimpdemod = 0
% 0.73/1.14 usesimpres = 3
% 0.73/1.14
% 0.73/1.14 resimpinuse = 1000
% 0.73/1.14 resimpclauses = 20000
% 0.73/1.14 substype = standard
% 0.73/1.14 backwardsubs = 1
% 0.73/1.14 selectoldest = 5
% 0.73/1.14
% 0.73/1.14 litorderings [0] = split
% 0.73/1.14 litorderings [1] = liftord
% 0.73/1.14
% 0.73/1.14 termordering = none
% 0.73/1.14
% 0.73/1.14 litapriori = 1
% 0.73/1.14 termapriori = 0
% 0.73/1.14 litaposteriori = 0
% 0.73/1.14 termaposteriori = 0
% 0.73/1.14 demodaposteriori = 0
% 0.73/1.14 ordereqreflfact = 0
% 0.73/1.14
% 0.73/1.14 litselect = none
% 0.73/1.14
% 0.73/1.14 maxweight = 15
% 0.73/1.14 maxdepth = 30000
% 0.73/1.14 maxlength = 115
% 0.73/1.14 maxnrvars = 195
% 0.73/1.14 excuselevel = 1
% 0.73/1.14 increasemaxweight = 1
% 0.73/1.14
% 0.73/1.14 maxselected = 10000000
% 0.73/1.14 maxnrclauses = 10000000
% 0.73/1.14
% 0.73/1.14 showgenerated = 0
% 0.73/1.14 showkept = 0
% 0.73/1.14 showselected = 0
% 0.73/1.14 showdeleted = 0
% 0.73/1.14 showresimp = 1
% 0.73/1.14 showstatus = 2000
% 0.73/1.14
% 0.73/1.14 prologoutput = 0
% 0.73/1.14 nrgoals = 5000000
% 0.73/1.14 totalproof = 1
% 0.73/1.14
% 0.73/1.14 Symbols occurring in the translation:
% 0.73/1.14
% 0.73/1.14 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.14 . [1, 2] (w:1, o:235, a:1, s:1, b:0),
% 0.73/1.14 ! [4, 1] (w:0, o:192, a:1, s:1, b:0),
% 0.73/1.14 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.14 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.14 ndr1_0 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.73/1.14 ndr1_1 [37, 1] (w:1, o:197, a:1, s:1, b:0),
% 0.73/1.14 a1 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.73/1.14 c3_2 [39, 2] (w:1, o:260, a:1, s:1, b:0),
% 0.73/1.14 c5_2 [40, 2] (w:1, o:262, a:1, s:1, b:0),
% 0.73/1.14 c1_2 [41, 2] (w:1, o:263, a:1, s:1, b:0),
% 0.73/1.14 a2 [42, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.73/1.14 c1_1 [43, 1] (w:1, o:198, a:1, s:1, b:0),
% 0.73/1.14 c3_0 [44, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.73/1.14 c5_0 [45, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.73/1.14 a3 [47, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.73/1.14 c5_1 [48, 1] (w:1, o:200, a:1, s:1, b:0),
% 0.73/1.14 c3_1 [49, 1] (w:1, o:202, a:1, s:1, b:0),
% 0.73/1.14 c1_0 [50, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.73/1.14 c4_2 [53, 2] (w:1, o:261, a:1, s:1, b:0),
% 0.73/1.14 c4_0 [54, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.73/1.14 a4 [56, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.73/1.14 c2_2 [58, 2] (w:1, o:259, a:1, s:1, b:0),
% 0.73/1.14 a5 [61, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.73/1.14 a6 [62, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.73/1.14 a7 [63, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.73/1.14 c4_1 [64, 1] (w:1, o:199, a:1, s:1, b:0),
% 0.73/1.14 c2_0 [65, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.73/1.14 a8 [66, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.73/1.14 a9 [67, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.73/1.14 a10 [68, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.73/1.14 a11 [69, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.73/1.14 a12 [70, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.14 a13 [71, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.73/1.14 c2_1 [75, 1] (w:1, o:201, a:1, s:1, b:0),
% 0.73/1.14 a14 [77, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.73/1.14 a15 [78, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.73/1.14 a16 [80, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.73/1.14 a17 [82, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.73/1.14 a18 [84, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.73/1.14 a19 [87, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.73/1.14 a20 [88, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.73/1.14 a21 [91, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.73/1.14 a22 [94, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.73/1.14 a23 [95, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.73/1.14 a24 [98, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.73/1.14 a25 [99, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.14 a26 [101, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.73/1.14 alpha1 [103, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.73/1.14 alpha2 [104, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.73/1.14 alpha3 [105, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.73/1.14 alpha4 [106, 0] (w:1, o:119, a:1, s:1, b:0),
% 0.73/1.14 alpha5 [107, 0] (w:1, o:127, a:1, s:1, b:0),
% 0.73/1.14 alpha6 [108, 0] (w:1, o:138, a:1, s:1, b:0),
% 0.73/1.14 alpha7 [109, 0] (w:1, o:144, a:1, s:1, b:0),
% 0.73/1.14 alpha8 [110, 0] (w:1, o:154, a:1, s:1, b:0),
% 0.73/1.14 alpha9 [111, 0] (w:1, o:162, a:1, s:1, b:0),
% 0.73/1.14 alpha10 [112, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.73/1.14 alpha11 [113, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.73/1.14 alpha12 [114, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.73/1.14 alpha13 [115, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.73/1.14 alpha14 [116, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.73/1.14 alpha15 [117, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.73/1.14 alpha16 [118, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.73/1.14 alpha17 [119, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.73/1.14 alpha18 [120, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.73/1.14 alpha19 [121, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.73/1.14 alpha20 [122, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.73/1.14 alpha21 [123, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.73/1.14 alpha22 [124, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.73/1.14 alpha23 [125, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.73/1.14 alpha24 [126, 0] (w:1, o:104, a:1, s:1, b:0),
% 0.73/1.14 alpha25 [127, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.73/1.14 alpha26 [128, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.73/1.14 alpha27 [129, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.73/1.14 alpha28 [130, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.73/1.14 alpha29 [131, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.73/1.14 alpha30 [132, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.73/1.14 alpha31 [133, 1] (w:1, o:203, a:1, s:1, b:0),
% 0.73/1.14 alpha32 [134, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.73/1.14 alpha33 [135, 1] (w:1, o:204, a:1, s:1, b:0),
% 0.73/1.14 alpha34 [136, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.78/1.16 alpha35 [137, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.78/1.16 alpha36 [138, 0] (w:1, o:115, a:1, s:1, b:0),
% 0.78/1.16 alpha37 [139, 0] (w:1, o:116, a:1, s:1, b:0),
% 0.78/1.16 alpha38 [140, 0] (w:1, o:117, a:1, s:1, b:0),
% 0.78/1.16 alpha39 [141, 0] (w:1, o:118, a:1, s:1, b:0),
% 0.78/1.16 alpha40 [142, 0] (w:1, o:120, a:1, s:1, b:0),
% 0.78/1.16 alpha41 [143, 0] (w:1, o:121, a:1, s:1, b:0),
% 0.78/1.16 alpha42 [144, 0] (w:1, o:122, a:1, s:1, b:0),
% 0.78/1.16 alpha43 [145, 1] (w:1, o:205, a:1, s:1, b:0),
% 0.78/1.16 alpha44 [146, 0] (w:1, o:123, a:1, s:1, b:0),
% 0.78/1.16 alpha45 [147, 1] (w:1, o:206, a:1, s:1, b:0),
% 0.78/1.16 alpha46 [148, 0] (w:1, o:124, a:1, s:1, b:0),
% 0.78/1.16 alpha47 [149, 1] (w:1, o:207, a:1, s:1, b:0),
% 0.78/1.16 alpha48 [150, 0] (w:1, o:125, a:1, s:1, b:0),
% 0.78/1.16 alpha49 [151, 0] (w:1, o:126, a:1, s:1, b:0),
% 0.78/1.16 alpha50 [152, 0] (w:1, o:128, a:1, s:1, b:0),
% 0.78/1.16 alpha51 [153, 0] (w:1, o:129, a:1, s:1, b:0),
% 0.78/1.16 alpha52 [154, 0] (w:1, o:130, a:1, s:1, b:0),
% 0.78/1.16 alpha53 [155, 0] (w:1, o:131, a:1, s:1, b:0),
% 0.78/1.16 alpha54 [156, 0] (w:1, o:132, a:1, s:1, b:0),
% 0.78/1.16 alpha55 [157, 0] (w:1, o:133, a:1, s:1, b:0),
% 0.78/1.16 alpha56 [158, 0] (w:1, o:134, a:1, s:1, b:0),
% 0.78/1.16 alpha57 [159, 0] (w:1, o:135, a:1, s:1, b:0),
% 0.78/1.16 alpha58 [160, 0] (w:1, o:136, a:1, s:1, b:0),
% 0.78/1.16 alpha59 [161, 0] (w:1, o:137, a:1, s:1, b:0),
% 0.78/1.16 alpha60 [162, 1] (w:1, o:208, a:1, s:1, b:0),
% 0.78/1.16 alpha61 [163, 1] (w:1, o:209, a:1, s:1, b:0),
% 0.78/1.16 alpha62 [164, 0] (w:1, o:139, a:1, s:1, b:0),
% 0.78/1.16 alpha63 [165, 0] (w:1, o:140, a:1, s:1, b:0),
% 0.78/1.16 alpha64 [166, 1] (w:1, o:210, a:1, s:1, b:0),
% 0.78/1.16 alpha65 [167, 1] (w:1, o:211, a:1, s:1, b:0),
% 0.78/1.16 alpha66 [168, 0] (w:1, o:141, a:1, s:1, b:0),
% 0.78/1.16 alpha67 [169, 1] (w:1, o:212, a:1, s:1, b:0),
% 0.78/1.16 alpha68 [170, 0] (w:1, o:142, a:1, s:1, b:0),
% 0.78/1.16 alpha69 [171, 0] (w:1, o:143, a:1, s:1, b:0),
% 0.78/1.16 alpha70 [172, 0] (w:1, o:145, a:1, s:1, b:0),
% 0.78/1.16 alpha71 [173, 1] (w:1, o:213, a:1, s:1, b:0),
% 0.78/1.16 alpha72 [174, 0] (w:1, o:146, a:1, s:1, b:0),
% 0.78/1.16 alpha73 [175, 0] (w:1, o:147, a:1, s:1, b:0),
% 0.78/1.16 alpha74 [176, 0] (w:1, o:148, a:1, s:1, b:0),
% 0.78/1.16 alpha75 [177, 0] (w:1, o:149, a:1, s:1, b:0),
% 0.78/1.16 alpha76 [178, 0] (w:1, o:150, a:1, s:1, b:0),
% 0.78/1.16 alpha77 [179, 0] (w:1, o:151, a:1, s:1, b:0),
% 0.78/1.16 alpha78 [180, 0] (w:1, o:152, a:1, s:1, b:0),
% 0.78/1.16 alpha79 [181, 0] (w:1, o:153, a:1, s:1, b:0),
% 0.78/1.16 alpha80 [182, 1] (w:1, o:214, a:1, s:1, b:0),
% 0.78/1.16 alpha81 [183, 1] (w:1, o:215, a:1, s:1, b:0),
% 0.78/1.16 alpha82 [184, 0] (w:1, o:155, a:1, s:1, b:0),
% 0.78/1.16 alpha83 [185, 0] (w:1, o:156, a:1, s:1, b:0),
% 0.78/1.16 alpha84 [186, 0] (w:1, o:157, a:1, s:1, b:0),
% 0.78/1.16 alpha85 [187, 0] (w:1, o:158, a:1, s:1, b:0),
% 0.78/1.16 alpha86 [188, 0] (w:1, o:159, a:1, s:1, b:0),
% 0.78/1.16 alpha87 [189, 1] (w:1, o:216, a:1, s:1, b:0),
% 0.78/1.16 alpha88 [190, 0] (w:1, o:160, a:1, s:1, b:0),
% 0.78/1.16 alpha89 [191, 0] (w:1, o:161, a:1, s:1, b:0),
% 0.78/1.16 alpha90 [192, 0] (w:1, o:163, a:1, s:1, b:0),
% 0.78/1.16 alpha91 [193, 1] (w:1, o:217, a:1, s:1, b:0),
% 0.78/1.16 alpha92 [194, 1] (w:1, o:218, a:1, s:1, b:0),
% 0.78/1.16 alpha93 [195, 0] (w:1, o:164, a:1, s:1, b:0),
% 0.78/1.16 alpha94 [196, 0] (w:1, o:165, a:1, s:1, b:0),
% 0.78/1.16 alpha95 [197, 0] (w:1, o:166, a:1, s:1, b:0),
% 0.78/1.16 alpha96 [198, 0] (w:1, o:167, a:1, s:1, b:0),
% 0.78/1.16 alpha97 [199, 0] (w:1, o:168, a:1, s:1, b:0),
% 0.78/1.16 alpha98 [200, 0] (w:1, o:169, a:1, s:1, b:0),
% 0.78/1.16 alpha99 [201, 0] (w:1, o:170, a:1, s:1, b:0),
% 0.78/1.16 alpha100 [202, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.78/1.16 alpha101 [203, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.78/1.16 alpha102 [204, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.78/1.16 alpha103 [205, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.78/1.16 alpha104 [206, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.78/1.16 alpha105 [207, 1] (w:1, o:219, a:1, s:1, b:0),
% 0.78/1.16 alpha106 [208, 1] (w:1, o:220, a:1, s:1, b:0),
% 0.78/1.16 alpha107 [209, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.78/1.16 alpha108 [210, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.78/1.16 alpha109 [211, 1] (w:1, o:221, a:1, s:1, b:0),
% 0.78/1.16 alpha110 [212, 1] (w:1, o:222, a:1, s:1, b:0),
% 0.78/1.16 alpha111 [213, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.78/1.16 alpha112 [214, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.78/1.16 alpha113 [215, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.78/1.16 alpha114 [216, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.78/1.16 alpha115 [217, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.78/1.16 alpha116 [218, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.78/1.16 alpha117 [219, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.78/1.16 alpha118 [220, 1] (w:1, o:223, a:1, s:1, b:0),
% 0.78/1.16 alpha119 [221, 1] (w:1, o:224, a:1, s:1, b:0),
% 0.78/1.16 alpha120 [222, 1] (w:1, o:225, a:1, s:1, b:0),
% 0.78/1.16 alpha121 [223, 1] (w:1, o:226, a:1, s:1, b:0),
% 0.78/1.16 alpha122 [224, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.78/1.16 alpha123 [225, 1] (w:1, o:227, a:1, s:1, b:0),
% 0.78/1.16 alpha124 [226, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.78/1.16 alpha125 [227, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.78/1.16 alpha126 [228, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.78/1.16 alpha127 [229, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.78/1.16 alpha128 [230, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.78/1.16 alpha129 [231, 1] (w:1, o:228, a:1, s:1, b:0),
% 0.78/1.16 alpha130 [232, 1] (w:1, o:229, a:1, s:1, b:0),
% 0.78/1.16 alpha131 [233, 1] (w:1, o:230, a:1, s:1, b:0),
% 0.78/1.16 alpha132 [234, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.78/1.16 alpha133 [235, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.78/1.16 alpha134 [236, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.78/1.16 alpha135 [237, 1] (w:1, o:231, a:1, s:1, b:0),
% 0.78/1.16 alpha136 [238, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.78/1.16 alpha137 [239, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.78/1.16 skol1 [240, 0] (w:1, o:171, a:1, s:1, b:0),
% 0.78/1.16 skol2 [241, 0] (w:1, o:182, a:1, s:1, b:0),
% 0.78/1.16 skol3 [242, 0] (w:1, o:187, a:1, s:1, b:0),
% 0.78/1.16 skol4 [243, 0] (w:1, o:188, a:1, s:1, b:0),
% 0.78/1.16 skol5 [244, 1] (w:1, o:232, a:1, s:1, b:0),
% 0.78/1.16 skol6 [245, 0] (w:1, o:189, a:1, s:1, b:0),
% 0.78/1.16 skol7 [246, 0] (w:1, o:190, a:1, s:1, b:0),
% 0.78/1.16 skol8 [247, 0] (w:1, o:191, a:1, s:1, b:0),
% 0.78/1.16 skol9 [248, 1] (w:1, o:233, a:1, s:1, b:0),
% 0.78/1.16 skol10 [249, 0] (w:1, o:172, a:1, s:1, b:0),
% 0.78/1.16 skol11 [250, 0] (w:1, o:173, a:1, s:1, b:0),
% 0.78/1.16 skol12 [251, 0] (w:1, o:174, a:1, s:1, b:0),
% 0.78/1.16 skol13 [252, 0] (w:1, o:175, a:1, s:1, b:0),
% 0.78/1.16 skol14 [253, 0] (w:1, o:176, a:1, s:1, b:0),
% 0.78/1.16 skol15 [254, 0] (w:1, o:177, a:1, s:1, b:0),
% 0.78/1.16 skol16 [255, 0] (w:1, o:178, a:1, s:1, b:0),
% 0.78/1.16 skol17 [256, 0] (w:1, o:179, a:1, s:1, b:0),
% 0.78/1.16 skol18 [257, 0] (w:1, o:180, a:1, s:1, b:0),
% 0.78/1.16 skol19 [258, 0] (w:1, o:181, a:1, s:1, b:0),
% 0.78/1.16 skol20 [259, 0] (w:1, o:183, a:1, s:1, b:0),
% 0.78/1.16 skol21 [260, 1] (w:1, o:234, a:1, s:1, b:0),
% 0.78/1.16 skol22 [261, 0] (w:1, o:184, a:1, s:1, b:0),
% 0.78/1.16 skol23 [262, 0] (w:1, o:185, a:1, s:1, b:0),
% 0.78/1.16 skol24 [263, 0] (w:1, o:186, a:1, s:1, b:0).
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16 Starting Search:
% 0.78/1.16
% 0.78/1.16 *** allocated 22500 integers for clauses
% 0.78/1.16 *** allocated 33750 integers for clauses
% 0.78/1.16 Resimplifying inuse:
% 0.78/1.16 Done
% 0.78/1.16
% 0.78/1.16 Resimplifying inuse:
% 0.78/1.16 Done
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16 found a saturation!
% 0.78/1.16 % SZS status CounterSatisfiable
% 0.78/1.16 % SZS output start Saturation
% 0.78/1.16
% 0.78/1.16 (580) {G22,W2,D1,L2,V0,M1} S(28);r(448) { alpha117, ! alpha128 }.
% 0.78/1.16 (579) {G22,W2,D1,L2,V0,M1} S(395);r(448) { alpha21, ! alpha13 }.
% 0.78/1.16 (578) {G22,W2,D1,L2,V0,M1} S(383);r(448) { alpha63, ! alpha84 }.
% 0.78/1.16 (577) {G22,W2,D1,L2,V0,M1} S(369);r(448) { alpha20, ! alpha12 }.
% 0.78/1.16 (576) {G22,W2,D1,L2,V0,M1} S(347);r(448) { alpha83, ! alpha101 }.
% 0.78/1.16 (575) {G22,W2,D1,L2,V0,M1} S(322);r(448) { alpha30, ! alpha18 }.
% 0.78/1.16 (574) {G22,W2,D1,L2,V0,M1} S(36);r(448) { alpha49, ! alpha34 }.
% 0.78/1.16 (571) {G10,W12,D2,L6,V0,M1} R(560,141);f;f { ! alpha91( a13 ), ! alpha120(
% 0.78/1.16 a13 ), ! ndr1_1( a13 ), alpha26, alpha109( a13 ), ! c2_2( a13, a18 ) }.
% 0.78/1.16 (570) {G10,W12,D2,L6,V0,M1} R(560,311);f;f { ! alpha91( a13 ), ! alpha120(
% 0.78/1.16 a13 ), ! ndr1_1( a13 ), alpha26, alpha80( a13 ), ! c2_2( a13, a6 ) }.
% 0.78/1.16 (573) {G10,W10,D2,L5,V0,M1} S(566);r(412) { alpha47( a13 ), ! alpha65( a13
% 0.78/1.16 ), ! alpha120( a13 ), alpha26, ! c2_2( a13, a1 ) }.
% 0.78/1.16 (572) {G10,W10,D2,L5,V0,M1} R(560,412);r(411) { ! alpha91( a13 ), !
% 0.78/1.16 alpha120( a13 ), alpha26, ! alpha65( a13 ), ! c2_2( a13, a1 ) }.
% 0.78/1.16 (560) {G9,W13,D2,L6,V1,M1} R(501,517);f { ! alpha91( a13 ), ! alpha120( a13
% 0.78/1.16 ), ! c2_2( a13, X ), ! ndr1_1( a13 ), alpha26, c3_2( a13, X ) }.
% 0.78/1.16 (552) {G1,W12,D2,L5,V1,M1} R(407,361);f { ! ndr1_1( X ), alpha64( X ), !
% 0.78/1.16 alpha45( X ), ! c3_2( X, a2 ), ! c4_2( X, a2 ) }.
% 0.78/1.16 (569) {G5,W10,D2,L6,V1,M1} R(568,469) { ! alpha45( X ), ! alpha91( X ), !
% 0.78/1.16 alpha105( X ), alpha68, c4_0, alpha106( X ) }.
% 0.78/1.16 (544) {G1,W12,D2,L5,V1,M1} R(361,321);f { ! alpha45( X ), ! c3_2( X, a5 ),
% 0.78/1.16 ! ndr1_1( X ), alpha81( X ), ! c4_2( X, a5 ) }.
% 0.78/1.16 (568) {G4,W8,D2,L4,V1,M1} R(567,57);r(56) { ! alpha91( X ), ! alpha45( X )
% 0.78/1.16 , ! alpha105( X ), ! alpha120( X ) }.
% 0.78/1.16 (567) {G3,W11,D2,L5,V1,M1} R(563,548);f { ! alpha91( X ), ! alpha120( X ),
% 0.78/1.16 ! alpha119( X ), ! alpha45( X ), ! c2_2( X, a22 ) }.
% 0.78/1.16 (563) {G2,W12,D2,L5,V1,M1} R(501,60) { ! alpha91( X ), ! alpha120( X ), !
% 0.78/1.16 c2_2( X, a22 ), ! alpha119( X ), c3_2( X, a22 ) }.
% 0.78/1.16 (561) {G2,W12,D2,L5,V1,M1} R(501,320) { ! alpha91( X ), ! alpha120( X ), !
% 0.78/1.16 c2_2( X, a5 ), ! alpha81( X ), c3_2( X, a5 ) }.
% 0.78/1.16 (523) {G1,W12,D2,L5,V1,M1} R(410,72) { alpha47( X ), ! alpha65( X ), !
% 0.78/1.16 alpha120( X ), ! c2_2( X, a1 ), ! c4_2( X, a1 ) }.
% 0.78/1.16 (540) {G24,W11,D2,L8,V0,M1} R(531,515) { alpha70, alpha107, ! c1_1( a8 ),
% 0.78/1.16 alpha127, ! c4_1( a8 ), alpha111, alpha112, c5_1( a8 ) }.
% 0.78/1.16 (541) {G24,W11,D2,L8,V0,M1} R(532,515) { alpha70, alpha107, c1_1( a7 ),
% 0.78/1.16 alpha79, ! c4_1( a7 ), alpha111, alpha112, c5_1( a7 ) }.
% 0.78/1.16 (542) {G24,W11,D2,L8,V0,M1} R(526,515) { alpha70, alpha108, ! c1_1( a8 ),
% 0.78/1.16 alpha127, ! c4_1( a8 ), alpha111, alpha112, c5_1( a8 ) }.
% 0.78/1.16 (543) {G24,W11,D2,L8,V0,M1} R(527,515) { alpha70, alpha108, c1_1( a7 ),
% 0.78/1.16 alpha79, ! c4_1( a7 ), alpha111, alpha112, c5_1( a7 ) }.
% 0.78/1.16 (509) {G1,W15,D2,L6,V1,M1} R(160,128) { ! ndr1_1( X ), alpha131( X ), !
% 0.78/1.16 alpha91( X ), c3_2( X, a17 ), ! c4_2( X, a17 ), ! c5_2( X, a17 ) }.
% 0.78/1.16 (524) {G1,W11,D2,L5,V0,M1} R(410,3);r(411) { alpha47( a26 ), alpha22, !
% 0.78/1.16 alpha65( a26 ), c2_2( a26, a1 ), c4_2( a26, a1 ) }.
% 0.78/1.16 (565) {G3,W10,D2,L5,V1,M1} R(564,549);f { ! alpha91( X ), ! alpha120( X ),
% 0.78/1.16 ! alpha45( X ), alpha118( X ), ! alpha129( X ) }.
% 0.78/1.16 (564) {G2,W9,D2,L4,V1,M1} R(501,54);r(53) { ! alpha91( X ), ! alpha120( X )
% 0.78/1.16 , ! alpha129( X ), c3_2( X, a23 ) }.
% 0.78/1.16 (562) {G2,W8,D2,L4,V0,M1} R(501,352);r(354) { ! alpha91( a4 ), ! alpha120(
% 0.78/1.16 a4 ), alpha116, ! c2_2( a4, skol19 ) }.
% 0.78/1.16 (501) {G1,W13,D2,L5,V2,M1} R(128,72);f { ! alpha91( X ), c3_2( X, Y ), !
% 0.78/1.16 alpha120( X ), ! c2_2( X, Y ), ! c4_2( X, Y ) }.
% 0.78/1.16 (538) {G9,W11,D2,L5,V0,M1} R(517,55);f { ! ndr1_1( a13 ), alpha26, ! c2_2(
% 0.78/1.16 a13, a23 ), alpha129( a13 ), c3_2( a13, a23 ) }.
% 0.78/1.16 (550) {G2,W11,D2,L5,V0,M1} R(546,504);f { ! alpha45( a26 ), ! alpha131( a26
% 0.78/1.16 ), alpha22, c2_2( a26, a17 ), ! c3_2( a26, a17 ) }.
% 0.78/1.16 (553) {G9,W11,D2,L5,V0,M1} R(503,517);r(157) { ! alpha120( a13 ), !
% 0.78/1.16 alpha131( a13 ), ! c2_2( a13, a17 ), alpha26, c3_2( a13, a17 ) }.
% 0.78/1.16 (559) {G11,W6,D2,L4,V0,M1} R(558,498) { alpha26, ! alpha47( a13 ), alpha37
% 0.78/1.16 , alpha71( a13 ) }.
% 0.78/1.16 (488) {G1,W11,D2,L5,V0,M1} R(88,3);f;f { ! ndr1_1( a26 ), alpha135( a26 ),
% 0.78/1.16 alpha22, c2_2( a26, a21 ), c4_2( a26, a21 ) }.
% 0.78/1.16 (558) {G10,W5,D2,L3,V0,M1} R(557,412);r(408) { ! alpha47( a13 ), alpha26, !
% 0.78/1.16 alpha91( a13 ) }.
% 0.78/1.16 (499) {G1,W10,D2,L4,V1,M1} R(128,409) { ! alpha91( X ), c3_2( X, a1 ), !
% 0.78/1.16 alpha47( X ), ! c4_2( X, a1 ) }.
% 0.78/1.16 (414) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c3_2( X, a1 ), alpha65( X ),
% 0.78/1.16 ! c5_2( X, a1 ) }.
% 0.78/1.16 (556) {G2,W7,D2,L3,V1,M1} R(502,320);r(315) { ! alpha61( X ), ! alpha91( X
% 0.78/1.16 ), c3_2( X, a5 ) }.
% 0.78/1.16 (554) {G2,W9,D2,L4,V1,M1} R(503,156);f { ! alpha120( X ), ! alpha131( X ),
% 0.78/1.16 alpha123( X ), ! c2_2( X, a17 ) }.
% 0.78/1.16 (503) {G1,W10,D2,L4,V1,M1} R(159,72) { ! alpha120( X ), ! alpha131( X ), !
% 0.78/1.16 c2_2( X, a17 ), ! c4_2( X, a17 ) }.
% 0.78/1.16 (407) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c3_2( X, a2 ), alpha64( X )
% 0.78/1.16 , c5_2( X, a2 ) }.
% 0.78/1.16 (547) {G1,W10,D2,L4,V1,M1} R(361,83) { ! alpha45( X ), ! c3_2( X, a21 ), !
% 0.78/1.16 alpha130( X ), ! c4_2( X, a21 ) }.
% 0.78/1.16 (551) {G2,W9,D2,L4,V1,M1} R(546,156);f { ! alpha45( X ), ! alpha131( X ),
% 0.78/1.16 alpha123( X ), ! c3_2( X, a17 ) }.
% 0.78/1.16 (546) {G1,W10,D2,L4,V1,M1} R(361,158) { ! alpha45( X ), ! c3_2( X, a17 ), !
% 0.78/1.16 alpha131( X ), ! c4_2( X, a17 ) }.
% 0.78/1.16 (530) {G24,W9,D2,L7,V0,M1} R(528,515) { alpha70, alpha108, alpha29, ! c4_1
% 0.78/1.16 ( skol16 ), alpha111, alpha112, c5_1( skol16 ) }.
% 0.78/1.16 (387) {G0,W10,D2,L4,V1,M1} I { ! c5_2( a3, X ), ! c1_2( a3, X ), c3_2( a3,
% 0.78/1.16 X ), ! alpha102 }.
% 0.78/1.16 (535) {G24,W9,D2,L7,V0,M1} R(533,515) { alpha70, alpha107, alpha29, ! c4_1
% 0.78/1.16 ( skol16 ), alpha111, alpha112, c5_1( skol16 ) }.
% 0.78/1.16 (549) {G1,W9,D2,L4,V1,M1} R(361,51);r(54) { ! alpha45( X ), ! alpha129( X )
% 0.78/1.16 , alpha118( X ), ! c3_2( X, a23 ) }.
% 0.78/1.16 (545) {G1,W9,D2,L4,V1,M1} R(361,307);r(309) { ! alpha45( X ), ! alpha80( X
% 0.78/1.16 ), alpha60( X ), ! c4_2( X, a6 ) }.
% 0.78/1.16 (548) {G1,W7,D2,L3,V1,M1} R(361,61);r(60) { ! alpha45( X ), ! alpha119( X )
% 0.78/1.16 , ! c3_2( X, a22 ) }.
% 0.78/1.16 (361) {G0,W11,D2,L4,V2,M1} I { ! alpha45( X ), ! c3_2( X, Y ), ! c4_2( X, Y
% 0.78/1.16 ), ! c5_2( X, Y ) }.
% 0.78/1.16 (527) {G23,W9,D2,L6,V0,M1} R(496,516) { ! c4_1( a7 ), alpha70, alpha108,
% 0.78/1.16 c1_1( a7 ), alpha79, ! c2_1( a7 ) }.
% 0.78/1.16 (526) {G23,W9,D2,L6,V0,M1} R(496,519) { ! c4_1( a8 ), alpha70, alpha108, !
% 0.78/1.16 c1_1( a8 ), alpha127, ! c2_1( a8 ) }.
% 0.78/1.16 (532) {G23,W9,D2,L6,V0,M1} R(497,516) { ! c4_1( a7 ), alpha70, alpha107,
% 0.78/1.16 c1_1( a7 ), alpha79, ! c2_1( a7 ) }.
% 0.78/1.16 (531) {G23,W9,D2,L6,V0,M1} R(497,519) { ! c4_1( a8 ), alpha70, alpha107, !
% 0.78/1.16 c1_1( a8 ), alpha127, ! c2_1( a8 ) }.
% 0.78/1.16 (351) {G0,W10,D2,L4,V1,M1} I { ! c4_2( a4, X ), ! c5_2( a4, X ), c3_2( a4,
% 0.78/1.16 X ), ! alpha116 }.
% 0.78/1.16 (487) {G1,W9,D2,L4,V0,M1} R(389,72) { alpha102, ! alpha120( a3 ), ! c2_2(
% 0.78/1.16 a3, skol22 ), ! c4_2( a3, skol22 ) }.
% 0.78/1.16 (539) {G2,W6,D2,L3,V0,M1} R(504,155);r(154) { alpha22, ! alpha123( a26 ),
% 0.78/1.16 c2_2( a26, a17 ) }.
% 0.78/1.16 (504) {G1,W9,D2,L4,V0,M1} R(159,3);r(157) { alpha22, ! alpha131( a26 ),
% 0.78/1.16 c2_2( a26, a17 ), c4_2( a26, a17 ) }.
% 0.78/1.16 (537) {G9,W6,D2,L3,V0,M1} R(517,87);r(85) { alpha26, ! alpha135( a13 ),
% 0.78/1.16 c3_2( a13, a21 ) }.
% 0.78/1.16 (341) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a4 ), c3_2( a4, X ), ! c2_2( a4, X
% 0.78/1.16 ), ! alpha100 }.
% 0.78/1.16 (536) {G9,W6,D2,L3,V0,M1} R(517,155);r(478) { alpha26, ! alpha123( a13 ),
% 0.78/1.16 c3_2( a13, a17 ) }.
% 0.78/1.16 (517) {G8,W9,D2,L4,V1,M1} R(218,417) { ! ndr1_1( a13 ), c3_2( a13, X ),
% 0.78/1.16 alpha26, c4_2( a13, X ) }.
% 0.78/1.16 (525) {G1,W9,D2,L4,V1,M1} R(317,72);r(320) { alpha61( X ), ! alpha81( X ),
% 0.78/1.16 ! alpha120( X ), ! c2_2( X, a5 ) }.
% 0.78/1.16 (534) {G7,W7,D2,L5,V0,M1} R(497,472) { ! c4_1( skol20 ), alpha70, alpha107
% 0.78/1.16 , alpha19, ! c2_1( skol20 ) }.
% 0.78/1.16 (334) {G0,W10,D2,L4,V1,M1} I { c4_2( a4, X ), ! c3_2( a4, X ), ! c5_2( a4,
% 0.78/1.16 X ), ! alpha99 }.
% 0.78/1.16 (533) {G7,W7,D2,L5,V0,M1} R(497,474) { ! c4_1( skol16 ), alpha70, alpha107
% 0.78/1.16 , alpha29, ! c2_1( skol16 ) }.
% 0.78/1.16 (497) {G6,W8,D2,L5,V1,M1} R(115,458) { ! c4_1( X ), ! c2_1( X ), alpha70,
% 0.78/1.16 alpha107, ! c3_1( X ) }.
% 0.78/1.16 (529) {G8,W7,D2,L5,V0,M1} R(496,472) { ! c4_1( skol20 ), alpha70, alpha108
% 0.78/1.16 , alpha19, ! c2_1( skol20 ) }.
% 0.78/1.16 (528) {G8,W7,D2,L5,V0,M1} R(496,474) { ! c4_1( skol16 ), alpha70, alpha108
% 0.78/1.16 , alpha29, ! c2_1( skol16 ) }.
% 0.78/1.16 (321) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c4_2( X, a5 ), alpha81( X )
% 0.78/1.16 , c5_2( X, a5 ) }.
% 0.78/1.16 (496) {G7,W8,D2,L5,V1,M1} R(115,459) { ! c4_1( X ), ! c2_1( X ), alpha70,
% 0.78/1.16 alpha108, ! c3_1( X ) }.
% 0.78/1.16 (365) {G0,W8,D2,L4,V1,M1} I { ! c3_1( X ), ! c5_1( X ), ! ndr1_1( X ), !
% 0.78/1.16 alpha31( X ) }.
% 0.78/1.16 (317) {G0,W7,D2,L3,V1,M1} I { ! alpha81( X ), alpha61( X ), c1_2( X, a5 )
% 0.78/1.16 }.
% 0.78/1.16 (410) {G0,W7,D2,L3,V1,M1} I { ! alpha65( X ), alpha47( X ), c1_2( X, a1 )
% 0.78/1.16 }.
% 0.78/1.16 (311) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a6 ), alpha80( X )
% 0.78/1.16 , ! c3_2( X, a6 ) }.
% 0.78/1.16 (362) {G0,W6,D3,L2,V1,M1} I { alpha45( X ), c5_2( X, skol21( X ) ) }.
% 0.78/1.16 (363) {G0,W6,D3,L2,V1,M1} I { alpha45( X ), c3_2( X, skol21( X ) ) }.
% 0.78/1.16 (364) {G0,W6,D3,L2,V1,M1} I { alpha45( X ), c4_2( X, skol21( X ) ) }.
% 0.78/1.16 (522) {G22,W5,D2,L3,V0,M1} S(244);r(448) { ! c4_1( a12 ), alpha57, ! c3_1(
% 0.78/1.16 a12 ) }.
% 0.78/1.16 (307) {G0,W7,D2,L3,V1,M1} I { ! alpha80( X ), alpha60( X ), c5_2( X, a6 )
% 0.78/1.16 }.
% 0.78/1.16 (521) {G22,W5,D2,L3,V0,M1} S(266);r(448) { ! ndr1_1( a10 ), alpha133, !
% 0.78/1.16 c5_1( a10 ) }.
% 0.78/1.16 (520) {G23,W6,D2,L4,V0,M1} R(519,512) { alpha127, ndr1_1( a8 ), alpha18, !
% 0.78/1.16 c1_1( a8 ) }.
% 0.78/1.16 (228) {G0,W10,D2,L4,V1,M1} I { c1_2( a13, X ), c3_2( a13, X ), ! c5_2( a13
% 0.78/1.16 , X ), ! alpha113 }.
% 0.78/1.16 (519) {G22,W5,D2,L3,V0,M1} S(282);r(448) { ! c1_1( a8 ), alpha127, c3_1( a8
% 0.78/1.16 ) }.
% 0.78/1.16 (518) {G23,W6,D2,L4,V0,M1} R(516,512) { alpha79, ndr1_1( a7 ), alpha18,
% 0.78/1.16 c1_1( a7 ) }.
% 0.78/1.16 (516) {G22,W5,D2,L3,V0,M1} S(295);r(448) { c1_1( a7 ), alpha79, c3_1( a7 )
% 0.78/1.16 }.
% 0.78/1.16 (218) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a13 ), c4_2( a13, X ), c3_2( a13, X
% 0.78/1.16 ), ! alpha75 }.
% 0.78/1.16 (515) {G23,W6,D2,L4,V1,M1} R(514,452) { c5_1( X ), alpha111, alpha112, c2_1
% 0.78/1.16 ( X ) }.
% 0.78/1.16 (514) {G22,W5,D2,L3,V1,M1} S(208);r(448) { c5_1( X ), c2_1( X ), ! alpha55
% 0.78/1.16 }.
% 0.78/1.16 (204) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a14 ), c5_2( a14, X ), ! c3_2( a14
% 0.78/1.16 , X ), ! alpha137 }.
% 0.78/1.16 (469) {G4,W6,D2,L4,V1,M1} R(69,461) { alpha106( X ), alpha68, c4_0,
% 0.78/1.16 alpha120( X ) }.
% 0.78/1.16 (491) {G1,W6,D2,L3,V0,M1} R(181,72);r(180) { alpha124, ! alpha120( a16 ), !
% 0.78/1.16 c2_2( a16, skol11 ) }.
% 0.78/1.16 (500) {G1,W6,D2,L3,V0,M1} R(128,229);r(230) { ! alpha91( a13 ), alpha113, !
% 0.78/1.16 c4_2( a13, skol15 ) }.
% 0.78/1.16 (513) {G14,W4,D2,L3,V0,M1} R(512,117) { alpha18, alpha90, ndr1_1( skol7 )
% 0.78/1.16 }.
% 0.78/1.16 (179) {G0,W10,D2,L4,V1,M1} I { ! c4_2( a16, X ), ! c1_2( a16, X ), ! c3_2(
% 0.78/1.16 a16, X ), ! alpha124 }.
% 0.78/1.16 (512) {G13,W5,D2,L3,V1,M1} R(511,507);f { ndr1_1( X ), alpha18, ! c3_1( X )
% 0.78/1.16 }.
% 0.78/1.16 (511) {G2,W6,D2,L3,V1,M1} R(312,473) { ! c3_1( X ), ndr1_1( X ), ! alpha43
% 0.78/1.16 ( X ) }.
% 0.78/1.16 (312) {G0,W6,D2,L3,V1,M1} I { ! c3_1( X ), ! alpha43( X ), alpha61( X ) }.
% 0.78/1.16 (510) {G2,W4,D2,L2,V1,M1} R(401,404);r(468) { ndr1_1( X ), ! alpha33( X )
% 0.78/1.16 }.
% 0.78/1.16 (161) {G0,W6,D2,L3,V1,M1} I { ! c5_1( X ), ! c2_1( X ), ! alpha110( X ) }.
% 0.78/1.16 (401) {G0,W6,D2,L3,V1,M1} I { ! alpha33( X ), alpha47( X ), alpha64( X )
% 0.78/1.16 }.
% 0.78/1.16 (484) {G2,W6,D2,L3,V1,M1} R(483,79) { ndr1_1( X ), ! c5_1( X ), ! alpha121
% 0.78/1.16 ( X ) }.
% 0.78/1.16 (508) {G1,W6,D2,L3,V1,M1} R(135,138) { c1_1( X ), ndr1_1( X ), ! alpha92( X
% 0.78/1.16 ) }.
% 0.78/1.16 (188) {G0,W5,D2,L3,V0,M1} I { c2_2( a14, a15 ), alpha74, ! alpha95 }.
% 0.78/1.16 (160) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c5_2( X, a17 ), alpha131( X
% 0.78/1.16 ), ! c1_2( X, a17 ) }.
% 0.78/1.16 (191) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a14, a15 ), alpha95, ! alpha112 }.
% 0.78/1.16 (194) {G0,W5,D2,L3,V0,M1} I { c3_2( a14, a15 ), alpha112, ! alpha125 }.
% 0.78/1.16 (256) {G0,W5,D2,L3,V0,M1} I { c1_2( a10, a11 ), alpha97, ! alpha114 }.
% 0.78/1.16 (259) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a10, a11 ), alpha114, ! alpha126 }.
% 0.78/1.16 (156) {G0,W7,D2,L3,V1,M1} I { ! alpha131( X ), alpha123( X ), c4_2( X, a17
% 0.78/1.16 ) }.
% 0.78/1.16 (262) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a10, a11 ), alpha126, ! alpha133 }.
% 0.78/1.16 (269) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a8, a9 ), alpha58, ! alpha78 }.
% 0.78/1.16 (272) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a8, a9 ), alpha78, ! alpha98 }.
% 0.78/1.16 (275) {G0,W5,D2,L3,V0,M1} I { c2_2( a8, a9 ), alpha98, ! alpha115 }.
% 0.78/1.16 (141) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a18 ), alpha109( X
% 0.78/1.16 ), ! c3_2( X, a18 ) }.
% 0.78/1.16 (489) {G11,W5,D2,L3,V0,M1} R(190,451) { alpha111, alpha55, c1_2( a14, a15 )
% 0.78/1.16 }.
% 0.78/1.16 (490) {G10,W5,D2,L3,V0,M1} R(187,450) { alpha55, alpha111, ! c2_2( a14, a15
% 0.78/1.16 ) }.
% 0.78/1.16 (493) {G22,W5,D2,L3,V0,M1} S(111);r(448) { ! ndr1_1( a19 ), alpha122, c2_1
% 0.78/1.16 ( a19 ) }.
% 0.78/1.16 (151) {G0,W5,D2,L3,V1,M1} I { alpha110( X ), alpha123( X ), ! alpha93 }.
% 0.78/1.16 (135) {G0,W6,D2,L3,V1,M1} I { ! alpha92( X ), c1_1( X ), alpha109( X ) }.
% 0.78/1.16 (507) {G12,W5,D2,L3,V1,M1} R(506,475) { alpha18, ndr1_1( X ), alpha43( X )
% 0.78/1.16 }.
% 0.78/1.16 (506) {G11,W5,D2,L3,V1,M1} R(302,301) { alpha43( X ), alpha18, alpha60( X )
% 0.78/1.16 }.
% 0.78/1.16 (302) {G0,W5,D2,L3,V1,M1} I { alpha43( X ), alpha60( X ), ! alpha29 }.
% 0.78/1.16 (505) {G12,W5,D2,L3,V1,M1} R(358,357) { alpha31( X ), alpha12, alpha45( X )
% 0.78/1.16 }.
% 0.78/1.16 (132) {G0,W6,D2,L3,V1,M1} I { ! alpha71( X ), ! ndr1_1( X ), alpha92( X )
% 0.78/1.16 }.
% 0.78/1.16 (358) {G0,W5,D2,L3,V1,M1} I { alpha31( X ), alpha45( X ), ! alpha19 }.
% 0.78/1.16 (398) {G0,W5,D2,L3,V1,M1} I { alpha33( X ), ! c1_1( X ), ! alpha21 }.
% 0.78/1.16 (498) {G5,W5,D2,L3,V1,M1} R(125,124) { alpha71( X ), alpha37, alpha91( X )
% 0.78/1.16 }.
% 0.78/1.16 (139) {G0,W5,D2,L2,V1,M1} I { ! alpha109( X ), c2_2( X, a18 ) }.
% 0.78/1.16 (131) {G0,W6,D3,L2,V1,M1} I { alpha91( X ), ! c1_2( X, skol9( X ) ) }.
% 0.78/1.16 (140) {G0,W5,D2,L2,V1,M1} I { ! alpha109( X ), c3_2( X, a18 ) }.
% 0.78/1.16 (155) {G0,W5,D2,L2,V1,M1} I { ! alpha123( X ), ! c4_2( X, a17 ) }.
% 0.78/1.16 (158) {G0,W5,D2,L2,V1,M1} I { ! alpha131( X ), c5_2( X, a17 ) }.
% 0.78/1.16 (159) {G0,W5,D2,L2,V1,M1} I { ! alpha131( X ), c1_2( X, a17 ) }.
% 0.78/1.16 (130) {G0,W6,D3,L2,V1,M1} I { alpha91( X ), ! c3_2( X, skol9( X ) ) }.
% 0.78/1.16 (306) {G0,W5,D2,L2,V1,M1} I { ! alpha60( X ), ! c5_2( X, a6 ) }.
% 0.78/1.16 (309) {G0,W5,D2,L2,V1,M1} I { ! alpha80( X ), c3_2( X, a6 ) }.
% 0.78/1.16 (310) {G0,W5,D2,L2,V1,M1} I { ! alpha80( X ), c2_2( X, a6 ) }.
% 0.78/1.16 (316) {G0,W5,D2,L2,V1,M1} I { ! alpha61( X ), ! c1_2( X, a5 ) }.
% 0.78/1.16 (129) {G0,W6,D3,L2,V1,M1} I { alpha91( X ), c4_2( X, skol9( X ) ) }.
% 0.78/1.16 (319) {G0,W5,D2,L2,V1,M1} I { ! alpha81( X ), ! c5_2( X, a5 ) }.
% 0.78/1.16 (320) {G0,W5,D2,L2,V1,M1} I { ! alpha81( X ), c4_2( X, a5 ) }.
% 0.78/1.16 (405) {G0,W5,D2,L2,V1,M1} I { ! alpha64( X ), c3_2( X, a2 ) }.
% 0.78/1.16 (406) {G0,W5,D2,L2,V1,M1} I { ! alpha64( X ), ! c5_2( X, a2 ) }.
% 0.78/1.16 (128) {G0,W11,D2,L4,V2,M1} I { ! alpha91( X ), c3_2( X, Y ), ! c4_2( X, Y )
% 0.78/1.16 , c1_2( X, Y ) }.
% 0.78/1.16 (409) {G0,W5,D2,L2,V1,M1} I { ! alpha47( X ), ! c1_2( X, a1 ) }.
% 0.78/1.16 (412) {G0,W5,D2,L2,V1,M1} I { ! alpha65( X ), ! c3_2( X, a1 ) }.
% 0.78/1.16 (413) {G0,W5,D2,L2,V1,M1} I { ! alpha65( X ), c5_2( X, a1 ) }.
% 0.78/1.16 (169) {G0,W4,D2,L3,V0,M1} I { c5_1( a16 ), alpha54, ! alpha73 }.
% 0.78/1.16 (125) {G0,W5,D2,L3,V1,M1} I { alpha71( X ), alpha91( X ), ! alpha52 }.
% 0.78/1.16 (172) {G0,W4,D2,L3,V0,M1} I { c3_1( a16 ), alpha73, ! alpha94 }.
% 0.78/1.16 (176) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a16 ), alpha124, ! alpha111 }.
% 0.78/1.16 (197) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a14 ), alpha125, ! alpha132 }.
% 0.78/1.16 (200) {G0,W4,D2,L3,V0,M1} I { ! c5_1( a14 ), alpha132, ! alpha136 }.
% 0.78/1.16 (115) {G0,W7,D2,L4,V1,M1} I { ! c4_1( X ), ! c3_1( X ), ! c2_1( X ), !
% 0.78/1.16 alpha90 }.
% 0.78/1.16 (495) {G9,W4,D2,L3,V0,M1} R(225,419) { alpha113, alpha26, ! ndr1_1( a13 )
% 0.78/1.16 }.
% 0.78/1.16 (225) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a13 ), alpha113, ! alpha96 }.
% 0.78/1.16 (494) {G22,W3,D2,L2,V0,M1} S(234);r(448) { alpha76, c4_1( a13 ) }.
% 0.78/1.16 (240) {G0,W4,D2,L3,V0,M1} I { c5_1( a12 ), alpha40, ! alpha57 }.
% 0.78/1.16 (253) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a10 ), alpha77, ! alpha97 }.
% 0.78/1.16 (278) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a8 ), alpha115, ! alpha127 }.
% 0.78/1.16 (291) {G0,W4,D2,L3,V0,M1} I { ! c4_1( a7 ), alpha59, ! alpha79 }.
% 0.78/1.16 (107) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a19, a20 ), alpha108, ! alpha122 }.
% 0.78/1.16 (331) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a4 ), alpha99, ! alpha82 }.
% 0.78/1.16 (348) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a4 ), alpha116, ! alpha101 }.
% 0.78/1.16 (377) {G0,W4,D2,L3,V0,M1} I { c3_1( a3 ), alpha32, ! alpha46 }.
% 0.78/1.16 (380) {G0,W4,D2,L3,V0,M1} I { c5_1( a3 ), alpha46, ! alpha63 }.
% 0.78/1.16 (104) {G0,W5,D2,L3,V0,M1} I { c4_2( a19, a20 ), alpha89, ! alpha108 }.
% 0.78/1.16 (384) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a3 ), alpha102, ! alpha84 }.
% 0.78/1.16 (492) {G5,W4,D2,L2,V0,M1} R(103,429) { alpha51, ! c4_2( a19, a20 ) }.
% 0.78/1.16 (103) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a19, a20 ), ! alpha89 }.
% 0.78/1.16 (106) {G0,W4,D2,L2,V0,M1} I { c3_2( a19, a20 ), ! alpha108 }.
% 0.78/1.16 (101) {G0,W4,D2,L2,V0,M1} I { alpha107, c4_2( a19, skol6 ) }.
% 0.78/1.16 (180) {G0,W4,D2,L2,V0,M1} I { alpha124, c4_2( a16, skol11 ) }.
% 0.78/1.16 (181) {G0,W4,D2,L2,V0,M1} I { alpha124, c1_2( a16, skol11 ) }.
% 0.78/1.16 (182) {G0,W4,D2,L2,V0,M1} I { alpha124, c3_2( a16, skol11 ) }.
% 0.78/1.16 (187) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a14, a15 ), ! alpha74 }.
% 0.78/1.16 (100) {G0,W4,D2,L2,V0,M1} I { alpha107, c3_2( a19, skol6 ) }.
% 0.78/1.16 (190) {G0,W4,D2,L2,V0,M1} I { c1_2( a14, a15 ), ! alpha95 }.
% 0.78/1.16 (193) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a14, a15 ), ! alpha112 }.
% 0.78/1.16 (206) {G0,W4,D2,L2,V0,M1} I { alpha137, ! c5_2( a14, skol12 ) }.
% 0.78/1.16 (207) {G0,W4,D2,L2,V0,M1} I { alpha137, c3_2( a14, skol12 ) }.
% 0.78/1.16 (98) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a19 ), ! c3_2( a19, X ), ! c4_2( a19
% 0.78/1.16 , X ), ! alpha107 }.
% 0.78/1.16 (220) {G0,W4,D2,L2,V0,M1} I { alpha75, ! c4_2( a13, skol14 ) }.
% 0.78/1.16 (221) {G0,W4,D2,L2,V0,M1} I { alpha75, ! c3_2( a13, skol14 ) }.
% 0.78/1.16 (229) {G0,W4,D2,L2,V0,M1} I { alpha113, ! c1_2( a13, skol15 ) }.
% 0.78/1.16 (230) {G0,W4,D2,L2,V0,M1} I { alpha113, ! c3_2( a13, skol15 ) }.
% 0.78/1.16 (88) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c4_2( X, a21 ), alpha135( X )
% 0.78/1.16 , c1_2( X, a21 ) }.
% 0.78/1.16 (231) {G0,W4,D2,L2,V0,M1} I { alpha113, c5_2( a13, skol15 ) }.
% 0.78/1.16 (255) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a10, a11 ), ! alpha97 }.
% 0.78/1.16 (258) {G0,W4,D2,L2,V0,M1} I { c2_2( a10, a11 ), ! alpha114 }.
% 0.78/1.16 (261) {G0,W4,D2,L2,V0,M1} I { c5_2( a10, a11 ), ! alpha126 }.
% 0.78/1.16 (87) {G0,W5,D2,L2,V1,M1} I { ! alpha135( X ), ! c4_2( X, a21 ) }.
% 0.78/1.16 (268) {G0,W4,D2,L2,V0,M1} I { c1_2( a8, a9 ), ! alpha58 }.
% 0.78/1.16 (271) {G0,W4,D2,L2,V0,M1} I { c3_2( a8, a9 ), ! alpha78 }.
% 0.78/1.16 (274) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a8, a9 ), ! alpha98 }.
% 0.78/1.16 (335) {G0,W4,D2,L2,V0,M1} I { alpha99, ! c4_2( a4, skol17 ) }.
% 0.78/1.16 (86) {G0,W5,D2,L2,V1,M1} I { ! alpha135( X ), ! c1_2( X, a21 ) }.
% 0.78/1.16 (336) {G0,W4,D2,L2,V0,M1} I { alpha99, c3_2( a4, skol17 ) }.
% 0.78/1.16 (337) {G0,W4,D2,L2,V0,M1} I { alpha99, c5_2( a4, skol17 ) }.
% 0.78/1.16 (343) {G0,W4,D2,L2,V0,M1} I { alpha100, ! c3_2( a4, skol18 ) }.
% 0.78/1.16 (344) {G0,W4,D2,L2,V0,M1} I { alpha100, c2_2( a4, skol18 ) }.
% 0.78/1.16 (84) {G0,W7,D2,L3,V1,M1} I { ! alpha135( X ), alpha130( X ), ! c5_2( X, a21
% 0.78/1.16 ) }.
% 0.78/1.16 (352) {G0,W4,D2,L2,V0,M1} I { alpha116, c4_2( a4, skol19 ) }.
% 0.78/1.16 (353) {G0,W4,D2,L2,V0,M1} I { alpha116, c5_2( a4, skol19 ) }.
% 0.78/1.16 (354) {G0,W4,D2,L2,V0,M1} I { alpha116, ! c3_2( a4, skol19 ) }.
% 0.78/1.16 (388) {G0,W4,D2,L2,V0,M1} I { alpha102, c5_2( a3, skol22 ) }.
% 0.78/1.16 (83) {G0,W5,D2,L2,V1,M1} I { ! alpha130( X ), c5_2( X, a21 ) }.
% 0.78/1.16 (389) {G0,W4,D2,L2,V0,M1} I { alpha102, c1_2( a3, skol22 ) }.
% 0.78/1.16 (390) {G0,W4,D2,L2,V0,M1} I { alpha102, ! c3_2( a3, skol22 ) }.
% 0.78/1.16 (486) {G2,W3,D2,L2,V0,M1} R(485,70) { alpha88, c5_1( skol4 ) }.
% 0.78/1.16 (485) {G1,W4,D2,L2,V1,M1} R(80,77) { c5_1( X ), alpha106( X ) }.
% 0.78/1.16 (80) {G0,W4,D2,L2,V1,M1} I { c5_1( X ), alpha121( X ) }.
% 0.78/1.16 (81) {G0,W4,D2,L2,V1,M1} I { alpha121( X ), ! alpha130( X ) }.
% 0.78/1.16 (483) {G1,W4,D2,L2,V1,M1} R(82,85) { ndr1_1( X ), ! alpha130( X ) }.
% 0.78/1.16 (82) {G0,W4,D2,L2,V1,M1} I { ! alpha130( X ), alpha135( X ) }.
% 0.78/1.16 (85) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha135( X ) }.
% 0.78/1.16 (79) {G0,W6,D2,L3,V1,M1} I { ! c5_1( X ), ! alpha121( X ), alpha130( X )
% 0.78/1.16 }.
% 0.78/1.16 (482) {G2,W3,D2,L2,V0,M1} R(481,126) { alpha52, ! c1_1( skol8 ) }.
% 0.78/1.16 (481) {G1,W4,D2,L2,V1,M1} R(133,137) { ! c1_1( X ), alpha71( X ) }.
% 0.78/1.16 (133) {G0,W4,D2,L2,V1,M1} I { alpha71( X ), ! alpha92( X ) }.
% 0.78/1.16 (480) {G1,W3,D2,L2,V0,M1} R(78,70) { alpha88, ndr1_1( skol4 ) }.
% 0.78/1.16 (78) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha106( X ) }.
% 0.78/1.16 (479) {G1,W3,D2,L2,V0,M1} R(134,126) { alpha52, ndr1_1( skol8 ) }.
% 0.78/1.16 (134) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha71( X ) }.
% 0.78/1.16 (136) {G0,W4,D2,L2,V1,M1} I { alpha92( X ), ! alpha109( X ) }.
% 0.78/1.16 (137) {G0,W4,D2,L2,V1,M1} I { ! c1_1( X ), alpha92( X ) }.
% 0.78/1.16 (77) {G0,W4,D2,L2,V1,M1} I { alpha106( X ), ! alpha121( X ) }.
% 0.78/1.16 (138) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha109( X ) }.
% 0.78/1.16 (478) {G1,W4,D2,L2,V1,M1} R(154,157) { ndr1_1( X ), ! alpha123( X ) }.
% 0.78/1.16 (154) {G0,W4,D2,L2,V1,M1} I { ! alpha123( X ), alpha131( X ) }.
% 0.78/1.16 (157) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha131( X ) }.
% 0.78/1.16 (76) {G0,W6,D2,L3,V1,M1} I { ! alpha106( X ), ! ndr1_1( X ), alpha121( X )
% 0.78/1.16 }.
% 0.78/1.16 (477) {G1,W3,D2,L2,V0,M1} R(162,152) { alpha93, c5_1( skol10 ) }.
% 0.78/1.16 (162) {G0,W4,D2,L2,V1,M1} I { c5_1( X ), alpha110( X ) }.
% 0.78/1.16 (476) {G1,W3,D2,L2,V0,M1} R(163,152) { alpha93, c2_1( skol10 ) }.
% 0.78/1.16 (163) {G0,W4,D2,L2,V1,M1} I { c2_1( X ), alpha110( X ) }.
% 0.78/1.16 (75) {G0,W6,D3,L2,V1,M1} I { alpha120( X ), c1_2( X, skol5( X ) ) }.
% 0.78/1.16 (475) {G1,W4,D2,L2,V1,M1} R(305,308) { ndr1_1( X ), ! alpha60( X ) }.
% 0.78/1.16 (305) {G0,W4,D2,L2,V1,M1} I { ! alpha60( X ), alpha80( X ) }.
% 0.78/1.16 (308) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha80( X ) }.
% 0.78/1.16 (474) {G1,W3,D2,L2,V0,M1} R(313,303) { alpha29, c3_1( skol16 ) }.
% 0.78/1.16 (74) {G0,W6,D3,L2,V1,M1} I { alpha120( X ), c4_2( X, skol5( X ) ) }.
% 0.78/1.16 (313) {G0,W4,D2,L2,V1,M1} I { c3_1( X ), alpha43( X ) }.
% 0.78/1.16 (314) {G0,W4,D2,L2,V1,M1} I { alpha43( X ), ! alpha61( X ) }.
% 0.78/1.16 (473) {G1,W4,D2,L2,V1,M1} R(315,318) { ndr1_1( X ), ! alpha61( X ) }.
% 0.78/1.16 (315) {G0,W4,D2,L2,V1,M1} I { ! alpha61( X ), alpha81( X ) }.
% 0.78/1.16 (73) {G0,W6,D3,L2,V1,M1} I { alpha120( X ), c2_2( X, skol5( X ) ) }.
% 0.78/1.16 (318) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha81( X ) }.
% 0.78/1.16 (472) {G1,W3,D2,L2,V0,M1} R(366,359) { alpha19, c3_1( skol20 ) }.
% 0.78/1.16 (366) {G0,W4,D2,L2,V1,M1} I { c3_1( X ), alpha31( X ) }.
% 0.78/1.16 (471) {G1,W3,D2,L2,V0,M1} R(367,359) { alpha19, c5_1( skol20 ) }.
% 0.78/1.16 (72) {G0,W11,D2,L4,V2,M1} I { ! alpha120( X ), ! c2_2( X, Y ), ! c4_2( X, Y
% 0.78/1.16 ), ! c1_2( X, Y ) }.
% 0.78/1.16 (367) {G0,W4,D2,L2,V1,M1} I { c5_1( X ), alpha31( X ) }.
% 0.78/1.16 (470) {G1,W3,D2,L2,V0,M1} R(368,359) { alpha19, ndr1_1( skol20 ) }.
% 0.78/1.16 (368) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha31( X ) }.
% 0.78/1.16 (402) {G0,W4,D2,L2,V1,M1} I { alpha33( X ), ! alpha47( X ) }.
% 0.78/1.16 (69) {G0,W5,D2,L3,V1,M1} I { alpha106( X ), alpha120( X ), ! alpha88 }.
% 0.78/1.16 (403) {G0,W4,D2,L2,V1,M1} I { alpha33( X ), ! alpha64( X ) }.
% 0.78/1.16 (404) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha64( X ) }.
% 0.78/1.16 (468) {G1,W4,D2,L2,V1,M1} R(408,411) { ndr1_1( X ), ! alpha47( X ) }.
% 0.78/1.16 (408) {G0,W4,D2,L2,V1,M1} I { ! alpha47( X ), alpha65( X ) }.
% 0.78/1.16 (62) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c4_2( X, a22 ), alpha119( X
% 0.78/1.16 ), ! c5_2( X, a22 ) }.
% 0.78/1.16 (411) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha65( X ) }.
% 0.78/1.16 (467) {G2,W4,D2,L2,V1,M1} R(462,46);r(466) { ndr1_1( X ), ! alpha87( X )
% 0.78/1.16 }.
% 0.78/1.16 (462) {G1,W4,D2,L2,V1,M1} R(52,49) { ndr1_1( X ), ! alpha118( X ) }.
% 0.78/1.16 (466) {G1,W4,D2,L2,V1,M1} R(59,56) { ndr1_1( X ), ! alpha105( X ) }.
% 0.78/1.16 (61) {G0,W5,D2,L2,V1,M1} I { ! alpha119( X ), c5_2( X, a22 ) }.
% 0.78/1.16 (70) {G0,W3,D2,L2,V0,M1} I { alpha88, ! alpha106( skol4 ) }.
% 0.78/1.16 (71) {G0,W3,D2,L2,V0,M1} I { alpha88, ! alpha120( skol4 ) }.
% 0.78/1.16 (99) {G0,W3,D2,L2,V0,M1} I { alpha107, ndr1_1( a19 ) }.
% 0.78/1.16 (109) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a19 ), ! alpha122 }.
% 0.78/1.16 (60) {G0,W5,D2,L2,V1,M1} I { ! alpha119( X ), c4_2( X, a22 ) }.
% 0.78/1.16 (110) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a19 ), ! alpha122 }.
% 0.78/1.16 (116) {G0,W3,D2,L2,V0,M1} I { alpha90, c4_1( skol7 ) }.
% 0.78/1.16 (117) {G0,W3,D2,L2,V0,M1} I { alpha90, c3_1( skol7 ) }.
% 0.78/1.16 (118) {G0,W3,D2,L2,V0,M1} I { alpha90, c2_1( skol7 ) }.
% 0.78/1.16 (59) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha119( X ) }.
% 0.78/1.16 (126) {G0,W3,D2,L2,V0,M1} I { alpha52, ! alpha71( skol8 ) }.
% 0.78/1.16 (127) {G0,W3,D2,L2,V0,M1} I { alpha52, ! alpha91( skol8 ) }.
% 0.78/1.16 (152) {G0,W3,D2,L2,V0,M1} I { alpha93, ! alpha110( skol10 ) }.
% 0.78/1.16 (153) {G0,W3,D2,L2,V0,M1} I { alpha93, ! alpha123( skol10 ) }.
% 0.78/1.16 (58) {G0,W7,D2,L3,V1,M1} I { ! alpha119( X ), alpha105( X ), ! c2_2( X, a22
% 0.78/1.16 ) }.
% 0.78/1.16 (465) {G6,W3,D2,L2,V0,M1} R(168,166) { alpha38, ! c5_1( a16 ) }.
% 0.78/1.16 (168) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a16 ), ! alpha54 }.
% 0.78/1.16 (464) {G7,W3,D2,L2,V0,M1} R(171,422) { alpha38, ! c3_1( a16 ) }.
% 0.78/1.16 (171) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a16 ), ! alpha73 }.
% 0.78/1.16 (57) {G0,W5,D2,L2,V1,M1} I { ! alpha105( X ), c2_2( X, a22 ) }.
% 0.78/1.16 (177) {G0,W3,D2,L2,V0,M1} I { alpha111, ndr1_1( a16 ) }.
% 0.78/1.16 (196) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a14 ), ! alpha125 }.
% 0.78/1.16 (199) {G0,W3,D2,L2,V0,M1} I { c5_1( a14 ), ! alpha132 }.
% 0.78/1.16 (205) {G0,W3,D2,L2,V0,M1} I { alpha137, ndr1_1( a14 ) }.
% 0.78/1.16 (56) {G0,W4,D2,L2,V1,M1} I { ! alpha105( X ), alpha119( X ) }.
% 0.78/1.16 (210) {G0,W3,D2,L2,V0,M1} I { alpha55, ! c2_1( skol13 ) }.
% 0.78/1.16 (211) {G0,W3,D2,L2,V0,M1} I { alpha55, ! c5_1( skol13 ) }.
% 0.78/1.16 (219) {G0,W3,D2,L2,V0,M1} I { alpha75, ndr1_1( a13 ) }.
% 0.78/1.16 (226) {G0,W3,D2,L2,V0,M1} I { alpha96, ndr1_1( a13 ) }.
% 0.78/1.16 (55) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a23 ), alpha129( X
% 0.78/1.16 ), ! c4_2( X, a23 ) }.
% 0.78/1.16 (463) {G9,W3,D2,L2,V0,M1} R(233,418) { alpha26, ! c4_1( a13 ) }.
% 0.78/1.16 (233) {G0,W3,D2,L2,V0,M1} I { ! c4_1( a13 ), ! alpha76 }.
% 0.78/1.16 (239) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a12 ), ! alpha40 }.
% 0.78/1.16 (242) {G0,W3,D2,L2,V0,M1} I { c4_1( a12 ), ! alpha57 }.
% 0.78/1.16 (54) {G0,W5,D2,L2,V1,M1} I { ! alpha129( X ), c4_2( X, a23 ) }.
% 0.78/1.16 (243) {G0,W3,D2,L2,V0,M1} I { c3_1( a12 ), ! alpha57 }.
% 0.78/1.16 (252) {G0,W3,D2,L2,V0,M1} I { c1_1( a10 ), ! alpha77 }.
% 0.78/1.16 (264) {G0,W3,D2,L2,V0,M1} I { c5_1( a10 ), ! alpha133 }.
% 0.78/1.16 (265) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a10 ), ! alpha133 }.
% 0.78/1.16 (53) {G0,W5,D2,L2,V1,M1} I { ! alpha129( X ), c2_2( X, a23 ) }.
% 0.78/1.16 (277) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a8 ), ! alpha115 }.
% 0.78/1.16 (280) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a8 ), ! alpha127 }.
% 0.78/1.16 (281) {G0,W3,D2,L2,V0,M1} I { c1_1( a8 ), ! alpha127 }.
% 0.78/1.16 (290) {G0,W3,D2,L2,V0,M1} I { c4_1( a7 ), ! alpha59 }.
% 0.78/1.16 (52) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha129( X ) }.
% 0.78/1.16 (293) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a7 ), ! alpha79 }.
% 0.78/1.16 (294) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a7 ), ! alpha79 }.
% 0.78/1.16 (303) {G0,W3,D2,L2,V0,M1} I { alpha29, ! alpha43( skol16 ) }.
% 0.78/1.16 (304) {G0,W3,D2,L2,V0,M1} I { alpha29, ! alpha60( skol16 ) }.
% 0.78/1.16 (51) {G0,W7,D2,L3,V1,M1} I { ! alpha129( X ), alpha118( X ), c5_2( X, a23 )
% 0.78/1.16 }.
% 0.78/1.16 (332) {G0,W3,D2,L2,V0,M1} I { alpha82, ndr1_1( a4 ) }.
% 0.78/1.16 (342) {G0,W3,D2,L2,V0,M1} I { alpha100, ndr1_1( a4 ) }.
% 0.78/1.16 (349) {G0,W3,D2,L2,V0,M1} I { alpha101, ndr1_1( a4 ) }.
% 0.78/1.16 (359) {G0,W3,D2,L2,V0,M1} I { alpha19, ! alpha31( skol20 ) }.
% 0.78/1.16 (50) {G0,W5,D2,L2,V1,M1} I { ! alpha118( X ), ! c5_2( X, a23 ) }.
% 0.78/1.16 (360) {G0,W3,D2,L2,V0,M1} I { alpha19, ! alpha45( skol20 ) }.
% 0.78/1.16 (376) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a3 ), ! alpha32 }.
% 0.78/1.16 (379) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a3 ), ! alpha46 }.
% 0.78/1.16 (385) {G0,W3,D2,L2,V0,M1} I { alpha84, ndr1_1( a3 ) }.
% 0.78/1.16 (49) {G0,W4,D2,L2,V1,M1} I { ! alpha118( X ), alpha129( X ) }.
% 0.78/1.16 (399) {G0,W3,D2,L2,V0,M1} I { alpha21, ! alpha33( skol23 ) }.
% 0.78/1.16 (400) {G0,W3,D2,L2,V0,M1} I { alpha21, c1_1( skol23 ) }.
% 0.78/1.16 (455) {G1,W3,D2,L2,V0,M1} R(45,40) { alpha49, ndr1_1( skol3 ) }.
% 0.78/1.16 (461) {G3,W3,D1,L3,V0,M1} R(66,65) { alpha68, c4_0, alpha88 }.
% 0.78/1.16 (48) {G0,W4,D2,L2,V1,M1} I { alpha87( X ), ! alpha118( X ) }.
% 0.78/1.16 (66) {G0,W3,D1,L3,V0,M1} I { alpha68, alpha88, ! alpha50 }.
% 0.78/1.16 (460) {G22,W2,D1,L2,V0,M1} S(89);r(448) { ! c3_0, ! alpha68 }.
% 0.78/1.16 (97) {G0,W3,D1,L3,V0,M1} I { ! alpha107, alpha69, ! alpha89 }.
% 0.78/1.16 (47) {G0,W4,D2,L2,V1,M1} I { alpha87( X ), ! alpha105( X ) }.
% 0.78/1.16 (459) {G6,W3,D1,L3,V0,M1} R(112,431) { alpha70, alpha108, alpha90 }.
% 0.78/1.16 (458) {G5,W3,D1,L3,V0,M1} R(112,430) { alpha70, alpha107, alpha90 }.
% 0.78/1.16 (112) {G0,W3,D1,L3,V0,M1} I { alpha70, alpha90, ! alpha51 }.
% 0.78/1.16 (457) {G22,W2,D1,L2,V0,M1} S(119);r(448) { ! c4_0, ! alpha70 }.
% 0.78/1.16 (46) {G0,W6,D2,L3,V1,M1} I { ! alpha87( X ), alpha105( X ), alpha118( X )
% 0.78/1.16 }.
% 0.78/1.16 (456) {G2,W2,D1,L2,V0,M1} S(142);r(425) { alpha53, ! alpha37 }.
% 0.78/1.16 (145) {G0,W3,D1,L3,V0,M1} I { alpha72, ! c5_0, ! alpha53 }.
% 0.78/1.16 (45) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha67( X ) }.
% 0.78/1.16 (454) {G22,W2,D1,L2,V0,M1} S(148);r(448) { alpha93, ! alpha72 }.
% 0.78/1.16 (453) {G22,W2,D1,L2,V0,M1} S(175);r(448) { alpha94, ! alpha111 }.
% 0.78/1.16 (44) {G0,W4,D2,L2,V1,M1} I { alpha67( X ), ! alpha87( X ) }.
% 0.78/1.16 (452) {G11,W3,D1,L3,V0,M1} R(451,189) { alpha111, alpha112, alpha55 }.
% 0.78/1.16 (451) {G10,W3,D1,L3,V0,M1} R(450,186) { alpha111, alpha55, alpha95 }.
% 0.78/1.16 (450) {G9,W3,D1,L3,V0,M1} R(183,424) { alpha55, alpha111, alpha74 }.
% 0.78/1.16 (183) {G0,W3,D1,L3,V0,M1} I { alpha55, alpha74, ! alpha38 }.
% 0.78/1.16 (43) {G0,W6,D2,L3,V1,M1} I { ! alpha67( X ), ! ndr1_1( X ), alpha87( X )
% 0.78/1.16 }.
% 0.78/1.16 (449) {G22,W2,D1,L2,V0,M1} S(203);r(448) { alpha136, ! alpha137 }.
% 0.78/1.16 (217) {G0,W3,D1,L3,V0,M1} I { ! alpha56, alpha39, ! alpha75 }.
% 0.78/1.16 (224) {G0,W3,D1,L3,V0,M1} I { ! alpha76, alpha56, ! alpha96 }.
% 0.78/1.16 (42) {G0,W4,D2,L2,V0,M1} I { alpha49, ! c4_2( skol3, skol24 ) }.
% 0.78/1.16 (448) {G21,W1,D1,L1,V0,M1} R(447,260);r(263) { ndr1_0 }.
% 0.78/1.16 (41) {G0,W4,D2,L2,V0,M1} I { alpha49, ! c5_2( skol3, skol24 ) }.
% 0.78/1.16 (40) {G0,W3,D2,L2,V0,M1} I { alpha49, ! alpha67( skol3 ) }.
% 0.78/1.16 (39) {G0,W9,D2,L4,V2,M1} I { alpha67( X ), c5_2( X, Y ), c4_2( X, Y ), !
% 0.78/1.16 alpha49 }.
% 0.78/1.16 (235) {G0,W3,D1,L3,V0,M1} I { c4_0, alpha40, ! alpha26 }.
% 0.78/1.16 (248) {G0,W3,D1,L3,V0,M1} I { alpha58, alpha77, ! alpha41 }.
% 0.78/1.16 (435) {G9,W3,D1,L3,V0,M1} R(286,285) { alpha59, c2_0, ! c1_0 }.
% 0.78/1.16 (286) {G0,W3,D1,L3,V0,M1} I { ! c1_0, alpha59, ! alpha42 }.
% 0.78/1.16 (298) {G9,W3,D1,L3,V0,M1} I;r(297) { ! c4_0, c5_0, ! c1_0 }.
% 0.78/1.16 (325) {G0,W3,D1,L3,V0,M1} I { c4_0, alpha44, ! alpha30 }.
% 0.78/1.16 (35) {G0,W4,D2,L2,V0,M1} I { alpha134, ! c4_2( a24, skol2 ) }.
% 0.78/1.16 (330) {G0,W3,D1,L3,V0,M1} I { ! alpha62, alpha44, ! alpha82 }.
% 0.78/1.16 (340) {G0,W3,D1,L3,V0,M1} I { ! alpha100, alpha62, ! alpha83 }.
% 0.78/1.16 (34) {G0,W4,D2,L2,V0,M1} I { alpha134, c2_2( a24, skol2 ) }.
% 0.78/1.16 (372) {G0,W3,D1,L3,V0,M1} I { alpha32, c1_0, ! alpha20 }.
% 0.78/1.16 (434) {G12,W3,D1,L3,V0,M1} R(392,391) { alpha13, c5_0, ! c3_0 }.
% 0.78/1.16 (392) {G0,W3,D1,L3,V0,M1} I { alpha13, ! c3_0, ! alpha7 }.
% 0.78/1.16 (33) {G0,W4,D2,L2,V0,M1} I { alpha134, c1_2( a24, skol2 ) }.
% 0.78/1.16 (38) {G0,W2,D1,L2,V0,M1} I { alpha34, ! alpha49 }.
% 0.78/1.16 (65) {G2,W2,D1,L2,V0,M1} I;r(64) { c4_0, alpha50 }.
% 0.78/1.16 (32) {G0,W10,D2,L4,V1,M1} I { ! c1_2( a24, X ), ! c2_2( a24, X ), c4_2( a24
% 0.78/1.16 , X ), ! alpha134 }.
% 0.78/1.16 (432) {G1,W2,D1,L2,V0,M1} R(67,90) { c3_0, alpha50 }.
% 0.78/1.16 (67) {G0,W2,D1,L2,V0,M1} I { alpha50, ! alpha68 }.
% 0.78/1.16 (68) {G0,W2,D1,L2,V0,M1} I { alpha50, ! alpha88 }.
% 0.78/1.16 (31) {G0,W2,D1,L2,V0,M1} I { alpha128, ! alpha134 }.
% 0.78/1.16 (90) {G0,W2,D1,L2,V0,M1} I { c3_0, alpha68 }.
% 0.78/1.16 (430) {G4,W2,D1,L2,V0,M1} R(94,96) { alpha107, alpha51 }.
% 0.78/1.16 (431) {G5,W2,D1,L2,V0,M1} R(429,102) { alpha108, alpha51 }.
% 0.78/1.16 (30) {G0,W3,D2,L2,V0,M1} I { alpha128, ndr1_1( a24 ) }.
% 0.78/1.16 (429) {G4,W2,D1,L2,V0,M1} R(94,95) { alpha51, alpha89 }.
% 0.78/1.16 (94) {G3,W2,D1,L2,V0,M1} I;r(93) { alpha51, alpha69 }.
% 0.78/1.16 (95) {G0,W2,D1,L2,V0,M1} I { alpha89, ! alpha69 }.
% 0.78/1.16 (96) {G0,W2,D1,L2,V0,M1} I { alpha107, ! alpha69 }.
% 0.78/1.16 (29) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a24 ), alpha134, ! alpha128 }.
% 0.78/1.16 (102) {G0,W2,D1,L2,V0,M1} I { alpha108, ! alpha89 }.
% 0.78/1.16 (105) {G0,W2,D1,L2,V0,M1} I { alpha122, ! alpha108 }.
% 0.78/1.16 (427) {G1,W2,D1,L2,V0,M1} R(113,120) { c4_0, alpha51 }.
% 0.78/1.16 (113) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha70 }.
% 0.78/1.16 (114) {G0,W2,D1,L2,V0,M1} I { alpha51, ! alpha90 }.
% 0.78/1.16 (120) {G0,W2,D1,L2,V0,M1} I { c4_0, alpha70 }.
% 0.78/1.16 (27) {G0,W2,D1,L2,V0,M1} I { alpha128, ! alpha117 }.
% 0.78/1.16 (124) {G4,W2,D1,L2,V0,M1} I;r(123) { alpha37, alpha52 }.
% 0.78/1.16 (426) {G1,W2,D1,L2,V0,M1} R(143,147) { c5_0, alpha37 }.
% 0.78/1.16 (143) {G0,W2,D1,L2,V0,M1} I { alpha37, ! alpha53 }.
% 0.78/1.16 (146) {G0,W2,D1,L2,V0,M1} I { alpha53, ! alpha72 }.
% 0.78/1.16 (147) {G0,W2,D1,L2,V0,M1} I { c5_0, alpha53 }.
% 0.78/1.16 (25) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a24 ), alpha104, ! alpha117 }.
% 0.78/1.16 (150) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha93 }.
% 0.78/1.16 (424) {G8,W2,D1,L2,V0,M1} R(423,174) { alpha111, alpha38 }.
% 0.78/1.16 (423) {G7,W2,D1,L2,V0,M1} R(422,170) { alpha38, alpha94 }.
% 0.78/1.16 (24) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a24 ), ! alpha104 }.
% 0.78/1.16 (422) {G6,W2,D1,L2,V0,M1} R(166,167) { alpha38, alpha73 }.
% 0.78/1.16 (166) {G5,W2,D1,L2,V0,M1} I;r(165) { alpha38, alpha54 }.
% 0.78/1.16 (167) {G0,W2,D1,L2,V0,M1} I { alpha73, ! alpha54 }.
% 0.78/1.16 (170) {G0,W2,D1,L2,V0,M1} I { alpha94, ! alpha73 }.
% 0.78/1.16 (23) {G0,W2,D1,L2,V0,M1} I { alpha117, ! alpha104 }.
% 0.78/1.16 (174) {G0,W2,D1,L2,V0,M1} I { alpha111, ! alpha94 }.
% 0.78/1.16 (178) {G0,W2,D1,L2,V0,M1} I { alpha111, ! alpha124 }.
% 0.78/1.16 (22) {G0,W5,D2,L3,V0,M1} I { ! c1_2( a24, a25 ), alpha86, ! alpha104 }.
% 0.78/1.16 (184) {G0,W2,D1,L2,V0,M1} I { alpha38, ! alpha55 }.
% 0.78/1.16 (185) {G0,W2,D1,L2,V0,M1} I { alpha38, ! alpha74 }.
% 0.78/1.16 (186) {G0,W2,D1,L2,V0,M1} I { alpha95, ! alpha74 }.
% 0.78/1.16 (189) {G0,W2,D1,L2,V0,M1} I { alpha112, ! alpha95 }.
% 0.78/1.16 (21) {G0,W4,D2,L2,V0,M1} I { c1_2( a24, a25 ), ! alpha86 }.
% 0.78/1.16 (192) {G0,W2,D1,L2,V0,M1} I { alpha125, ! alpha112 }.
% 0.78/1.16 (195) {G0,W2,D1,L2,V0,M1} I { alpha132, ! alpha125 }.
% 0.78/1.16 (198) {G0,W2,D1,L2,V0,M1} I { alpha136, ! alpha132 }.
% 0.78/1.16 (20) {G0,W2,D1,L2,V0,M1} I { alpha104, ! alpha86 }.
% 0.78/1.16 (202) {G0,W2,D1,L2,V0,M1} I { alpha137, ! alpha136 }.
% 0.78/1.16 (417) {G7,W2,D1,L2,V0,M1} R(214,216) { alpha26, alpha75 }.
% 0.78/1.16 (419) {G8,W2,D1,L2,V0,M1} R(416,223) { alpha26, alpha96 }.
% 0.78/1.16 (19) {G0,W5,D2,L3,V0,M1} I { ! c3_2( a24, a25 ), alpha66, ! alpha86 }.
% 0.78/1.16 (418) {G8,W2,D1,L2,V0,M1} R(416,222) { alpha26, alpha76 }.
% 0.78/1.16 (416) {G7,W2,D1,L2,V0,M1} R(214,215) { alpha26, alpha56 }.
% 0.78/1.16 (214) {G6,W2,D1,L2,V0,M1} I;r(213) { alpha26, alpha39 }.
% 0.78/1.16 (18) {G0,W4,D2,L2,V0,M1} I { c3_2( a24, a25 ), ! alpha66 }.
% 0.78/1.16 (215) {G0,W2,D1,L2,V0,M1} I { alpha56, ! alpha39 }.
% 0.78/1.16 (216) {G0,W2,D1,L2,V0,M1} I { alpha75, ! alpha39 }.
% 0.78/1.16 (222) {G0,W2,D1,L2,V0,M1} I { alpha76, ! alpha56 }.
% 0.78/1.16 (223) {G0,W2,D1,L2,V0,M1} I { alpha96, ! alpha56 }.
% 0.78/1.16 (17) {G0,W2,D1,L2,V0,M1} I { alpha86, ! alpha66 }.
% 0.78/1.16 (227) {G0,W2,D1,L2,V0,M1} I { alpha96, ! alpha113 }.
% 0.78/1.16 (236) {G0,W2,D1,L2,V0,M1} I { alpha26, ! c4_0 }.
% 0.78/1.16 (237) {G0,W2,D1,L2,V0,M1} I { alpha26, ! alpha40 }.
% 0.78/1.16 (16) {G0,W4,D2,L2,V0,M1} I { alpha103, c3_2( a24, skol1 ) }.
% 0.78/1.16 (238) {G0,W2,D1,L2,V0,M1} I { alpha57, ! alpha40 }.
% 0.78/1.16 (247) {G7,W2,D1,L2,V0,M1} I;r(246) { alpha41, ! c4_0 }.
% 0.78/1.16 (249) {G0,W2,D1,L2,V0,M1} I { alpha41, ! alpha58 }.
% 0.78/1.16 (15) {G0,W4,D2,L2,V0,M1} I { alpha103, ! c1_2( a24, skol1 ) }.
% 0.78/1.16 (250) {G0,W2,D1,L2,V0,M1} I { alpha41, ! alpha77 }.
% 0.78/1.16 (251) {G0,W2,D1,L2,V0,M1} I { alpha97, ! alpha77 }.
% 0.78/1.16 (254) {G0,W2,D1,L2,V0,M1} I { alpha114, ! alpha97 }.
% 0.78/1.16 (257) {G0,W2,D1,L2,V0,M1} I { alpha126, ! alpha114 }.
% 0.78/1.16 (14) {G0,W4,D2,L2,V0,M1} I { alpha103, c4_2( a24, skol1 ) }.
% 0.78/1.16 (260) {G0,W2,D1,L2,V0,M1} I { alpha133, ! alpha126 }.
% 0.78/1.16 (267) {G0,W2,D1,L2,V0,M1} I { alpha78, ! alpha58 }.
% 0.78/1.16 (270) {G0,W2,D1,L2,V0,M1} I { alpha98, ! alpha78 }.
% 0.78/1.16 (13) {G0,W10,D2,L4,V1,M1} I { ! c4_2( a24, X ), c1_2( a24, X ), ! c3_2( a24
% 0.78/1.16 , X ), ! alpha103 }.
% 0.78/1.16 (273) {G0,W2,D1,L2,V0,M1} I { alpha115, ! alpha98 }.
% 0.78/1.16 (276) {G0,W2,D1,L2,V0,M1} I { alpha127, ! alpha115 }.
% 0.78/1.16 (285) {G8,W2,D1,L2,V0,M1} I;r(284) { c2_0, alpha42 }.
% 0.78/1.16 (12) {G0,W2,D1,L2,V0,M1} I { alpha85, ! alpha103 }.
% 0.78/1.16 (287) {G0,W2,D1,L2,V0,M1} I { c1_0, alpha42 }.
% 0.78/1.16 (288) {G0,W2,D1,L2,V0,M1} I { alpha42, ! alpha59 }.
% 0.78/1.16 (289) {G0,W2,D1,L2,V0,M1} I { alpha79, ! alpha59 }.
% 0.78/1.16 (11) {G0,W3,D2,L2,V0,M1} I { alpha85, ndr1_1( a24 ) }.
% 0.78/1.16 (301) {G10,W2,D1,L2,V0,M1} I;r(300) { alpha18, alpha29 }.
% 0.78/1.16 (323) {G0,W2,D1,L2,V0,M1} I { alpha18, ! alpha30 }.
% 0.78/1.16 (326) {G0,W2,D1,L2,V0,M1} I { alpha30, ! c4_0 }.
% 0.78/1.16 (10) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a24 ), alpha103, ! alpha85 }.
% 0.78/1.16 (327) {G0,W2,D1,L2,V0,M1} I { alpha30, ! alpha44 }.
% 0.78/1.16 (328) {G0,W2,D1,L2,V0,M1} I { alpha62, ! alpha44 }.
% 0.78/1.16 (329) {G0,W2,D1,L2,V0,M1} I { alpha82, ! alpha44 }.
% 0.78/1.16 (333) {G0,W2,D1,L2,V0,M1} I { alpha82, ! alpha99 }.
% 0.78/1.16 (9) {G0,W3,D1,L3,V0,M1} I { ! alpha66, alpha48, ! alpha85 }.
% 0.78/1.16 (338) {G0,W2,D1,L2,V0,M1} I { alpha83, ! alpha62 }.
% 0.78/1.16 (339) {G0,W2,D1,L2,V0,M1} I { alpha100, ! alpha62 }.
% 0.78/1.16 (346) {G0,W2,D1,L2,V0,M1} I { alpha101, ! alpha83 }.
% 0.78/1.16 (8) {G0,W2,D1,L2,V0,M1} I { alpha85, ! alpha48 }.
% 0.78/1.16 (350) {G0,W2,D1,L2,V0,M1} I { alpha101, ! alpha116 }.
% 0.78/1.16 (357) {G11,W2,D1,L2,V0,M1} I;r(356) { alpha12, alpha19 }.
% 0.78/1.16 (370) {G0,W2,D1,L2,V0,M1} I { alpha12, ! alpha20 }.
% 0.78/1.16 (7) {G0,W2,D1,L2,V0,M1} I { alpha66, ! alpha48 }.
% 0.78/1.16 (373) {G0,W2,D1,L2,V0,M1} I { alpha20, ! alpha32 }.
% 0.78/1.16 (374) {G0,W2,D1,L2,V0,M1} I { alpha20, ! c1_0 }.
% 0.78/1.16 (375) {G0,W2,D1,L2,V0,M1} I { alpha46, ! alpha32 }.
% 0.78/1.16 (378) {G0,W2,D1,L2,V0,M1} I { alpha63, ! alpha46 }.
% 0.78/1.16 (6) {G0,W2,D1,L2,V0,M1} I { alpha22, ! alpha48 }.
% 0.78/1.16 (382) {G0,W2,D1,L2,V0,M1} I { alpha84, ! alpha63 }.
% 0.78/1.16 (386) {G0,W2,D1,L2,V0,M1} I { alpha84, ! alpha102 }.
% 0.78/1.16 (391) {G11,W2,D1,L2,V0,M1} I;r(355) { c5_0, alpha7 }.
% 0.78/1.16 (5) {G0,W2,D1,L2,V0,M1} I { alpha22, ! alpha34 }.
% 0.78/1.16 (393) {G0,W2,D1,L2,V0,M1} I { alpha7, ! alpha13 }.
% 0.78/1.16 (394) {G0,W2,D1,L2,V0,M1} I { c3_0, alpha7 }.
% 0.78/1.16 (4) {G0,W3,D1,L3,V0,M1} I { alpha34, alpha48, ! alpha22 }.
% 0.78/1.16 (397) {G0,W2,D1,L2,V0,M1} I { alpha13, ! alpha21 }.
% 0.78/1.16 (63) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha23 }.
% 0.78/1.16 (64) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha35 }.
% 0.78/1.16 (92) {G2,W1,D1,L1,V0,M1} I;r(63) { alpha8 }.
% 0.78/1.16 (3) {G0,W12,D2,L5,V1,M1} I { alpha22, ! ndr1_1( a26 ), c2_2( a26, X ), c4_2
% 0.78/1.16 ( a26, X ), ! c1_2( a26, X ) }.
% 0.78/1.16 (93) {G2,W1,D1,L1,V0,M1} I;r(63) { alpha36 }.
% 0.78/1.16 (122) {G3,W1,D1,L1,V0,M1} I;r(92) { alpha15 }.
% 0.78/1.16 (123) {G3,W1,D1,L1,V0,M1} I;r(92) { alpha24 }.
% 0.78/1.16 (164) {G4,W1,D1,L1,V0,M1} I;r(122) { alpha4 }.
% 0.78/1.16 (2) {G0,W3,D2,L2,V0,M1} I { alpha22, ! c5_1( a26 ) }.
% 0.78/1.16 (165) {G4,W1,D1,L1,V0,M1} I;r(122) { alpha25 }.
% 0.78/1.16 (212) {G5,W1,D1,L1,V0,M1} I;r(164) { alpha9 }.
% 0.78/1.16 (213) {G5,W1,D1,L1,V0,M1} I;r(164) { alpha16 }.
% 0.78/1.16 (245) {G6,W1,D1,L1,V0,M1} I;r(212) { alpha17 }.
% 0.78/1.16 (246) {G6,W1,D1,L1,V0,M1} I;r(212) { alpha27 }.
% 0.78/1.16 (283) {G7,W1,D1,L1,V0,M1} I;r(245) { alpha2 }.
% 0.78/1.16 (284) {G7,W1,D1,L1,V0,M1} I;r(245) { alpha28 }.
% 0.78/1.16 (296) {G8,W1,D1,L1,V0,M1} I;r(283) { alpha5 }.
% 0.78/1.16 (0) {G0,W1,D1,L1,V0,M1} I { alpha14 }.
% 0.78/1.16 (297) {G8,W1,D1,L1,V0,M1} I;r(283) { alpha10 }.
% 0.78/1.16 (299) {G9,W1,D1,L1,V0,M1} I;r(296) { alpha1 }.
% 0.78/1.16 (300) {G9,W1,D1,L1,V0,M1} I;r(296) { alpha11 }.
% 0.78/1.16 (355) {G10,W1,D1,L1,V0,M1} I;r(299) { alpha3 }.
% 0.78/1.16 (356) {G10,W1,D1,L1,V0,M1} I;r(299) { alpha6 }.
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16 % SZS output end Saturation
% 0.78/1.16 end of saturation!
% 0.78/1.16
% 0.78/1.16 Memory use:
% 0.78/1.16
% 0.78/1.16 space for terms: 7592
% 0.78/1.16 space for clauses: 26813
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16 clauses generated: 776
% 0.78/1.16 clauses kept: 581
% 0.78/1.16 clauses selected: 566
% 0.78/1.16 clauses deleted: 63
% 0.78/1.16 clauses inuse deleted: 48
% 0.78/1.16
% 0.78/1.16 subsentry: 288
% 0.78/1.16 literals s-matched: 166
% 0.78/1.16 literals matched: 166
% 0.78/1.16 full subsumption: 0
% 0.78/1.16
% 0.78/1.16 checksum: 2071773944
% 0.78/1.16
% 0.78/1.16
% 0.78/1.16 Bliksem ended
%------------------------------------------------------------------------------