%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN516+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n003.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:24 EDT 2022
% Result : CounterSatisfiable 0.71s 1.11s
% Output : Saturation 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN516+1 : TPTP v8.1.0. Released v2.1.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Mon Jul 11 23:22:15 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.71/1.10 *** allocated 10000 integers for termspace/termends
% 0.71/1.10 *** allocated 10000 integers for clauses
% 0.71/1.10 *** allocated 10000 integers for justifications
% 0.71/1.10 Bliksem 1.12
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Automatic Strategy Selection
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Clauses:
% 0.71/1.10
% 0.71/1.10 { alpha22 }.
% 0.71/1.10 { alpha34, alpha46, c1_0 }.
% 0.71/1.10 { alpha34, ! c5_2( a48, a49 ), c1_0 }.
% 0.71/1.10 { ! alpha46, alpha59 }.
% 0.71/1.10 { ! alpha46, ! c1_2( a48, a49 ) }.
% 0.71/1.10 { ! alpha59, c1_2( a48, a49 ), alpha46 }.
% 0.71/1.10 { ! alpha59, ndr1_0 }.
% 0.71/1.10 { ! alpha59, c4_1( a48 ) }.
% 0.71/1.10 { ! alpha59, ndr1_1( a48 ) }.
% 0.71/1.10 { ! ndr1_0, ! c4_1( a48 ), ! ndr1_1( a48 ), alpha59 }.
% 0.71/1.10 { ! alpha34, ndr1_0 }.
% 0.71/1.10 { ! alpha34, ! c3_1( a47 ) }.
% 0.71/1.10 { ! ndr1_0, c3_1( a47 ), alpha34 }.
% 0.71/1.10 { ! alpha22, alpha35 }.
% 0.71/1.10 { ! alpha22, alpha47 }.
% 0.71/1.10 { ! alpha35, ! alpha47, alpha22 }.
% 0.71/1.10 { ! alpha47, ! c2_0, ndr1_0 }.
% 0.71/1.10 { ! alpha47, ! c2_0, ! c3_1( a46 ) }.
% 0.71/1.10 { c2_0, alpha47 }.
% 0.71/1.10 { ! ndr1_0, c3_1( a46 ), alpha47 }.
% 0.71/1.10 { ! alpha35, alpha14 }.
% 0.71/1.10 { ! alpha35, alpha48 }.
% 0.71/1.10 { ! alpha14, ! alpha48, alpha35 }.
% 0.71/1.10 { ! alpha48, alpha60, alpha69 }.
% 0.71/1.10 { ! alpha60, alpha48 }.
% 0.71/1.10 { ! alpha69, alpha48 }.
% 0.71/1.10 { ! alpha69, alpha79 }.
% 0.71/1.10 { ! alpha69, c4_1( a44 ) }.
% 0.71/1.10 { ! alpha79, ! c4_1( a44 ), alpha69 }.
% 0.71/1.10 { ! alpha79, alpha86 }.
% 0.71/1.10 { ! alpha79, c3_1( a44 ) }.
% 0.71/1.10 { ! alpha86, ! c3_1( a44 ), alpha79 }.
% 0.71/1.10 { ! alpha86, alpha89 }.
% 0.71/1.10 { ! alpha86, ! c2_2( a44, a45 ) }.
% 0.71/1.10 { ! alpha89, c2_2( a44, a45 ), alpha86 }.
% 0.71/1.10 { ! alpha89, alpha91 }.
% 0.71/1.10 { ! alpha89, ! c4_2( a44, a45 ) }.
% 0.71/1.10 { ! alpha91, c4_2( a44, a45 ), alpha89 }.
% 0.71/1.10 { ! alpha91, ndr1_0 }.
% 0.71/1.10 { ! alpha91, ndr1_1( a44 ) }.
% 0.71/1.10 { ! alpha91, c1_2( a44, a45 ) }.
% 0.71/1.10 { ! ndr1_0, ! ndr1_1( a44 ), ! c1_2( a44, a45 ), alpha91 }.
% 0.71/1.10 { ! alpha60, ! c5_0, alpha70 }.
% 0.71/1.10 { c5_0, alpha60 }.
% 0.71/1.10 { ! alpha70, alpha60 }.
% 0.71/1.10 { ! alpha70, ndr1_0 }.
% 0.71/1.10 { ! alpha70, ! c5_1( a43 ) }.
% 0.71/1.10 { ! alpha70, ! c2_1( a43 ) }.
% 0.71/1.10 { ! ndr1_0, c5_1( a43 ), c2_1( a43 ), alpha70 }.
% 0.71/1.10 { ! alpha14, alpha8 }.
% 0.71/1.10 { ! alpha14, alpha23 }.
% 0.71/1.10 { ! alpha8, ! alpha23, alpha14 }.
% 0.71/1.10 { ! alpha23, alpha36, alpha49 }.
% 0.71/1.10 { ! alpha36, alpha23 }.
% 0.71/1.10 { ! alpha49, alpha23 }.
% 0.71/1.10 { ! alpha49, alpha61 }.
% 0.71/1.10 { ! alpha49, ! c2_1( a41 ) }.
% 0.71/1.10 { ! alpha61, c2_1( a41 ), alpha49 }.
% 0.71/1.10 { ! alpha61, alpha71 }.
% 0.71/1.10 { ! alpha61, c4_2( a41, a42 ) }.
% 0.71/1.10 { ! alpha71, ! c4_2( a41, a42 ), alpha61 }.
% 0.71/1.10 { ! alpha71, alpha80 }.
% 0.71/1.10 { ! alpha71, ! c3_2( a41, a42 ) }.
% 0.71/1.10 { ! alpha80, c3_2( a41, a42 ), alpha71 }.
% 0.71/1.10 { ! alpha80, ndr1_0 }.
% 0.71/1.10 { ! alpha80, ndr1_1( a41 ) }.
% 0.71/1.10 { ! alpha80, c5_2( a41, a42 ) }.
% 0.71/1.10 { ! ndr1_0, ! ndr1_1( a41 ), ! c5_2( a41, a42 ), alpha80 }.
% 0.71/1.10 { ! alpha36, c3_0, alpha50 }.
% 0.71/1.10 { ! c3_0, alpha36 }.
% 0.71/1.10 { ! alpha50, alpha36 }.
% 0.71/1.10 { ! alpha50, alpha62 }.
% 0.71/1.10 { ! alpha50, alpha72 }.
% 0.71/1.10 { ! alpha62, ! alpha72, alpha50 }.
% 0.71/1.10 { ! alpha72, ! ndr1_1( a39 ), ! c5_2( a39, X ), c1_2( a39, X ) }.
% 0.71/1.10 { ndr1_1( a39 ), alpha72 }.
% 0.71/1.10 { c5_2( a39, skol1 ), alpha72 }.
% 0.71/1.10 { ! c1_2( a39, skol1 ), alpha72 }.
% 0.71/1.10 { ! alpha62, alpha73 }.
% 0.71/1.10 { ! alpha62, c2_1( a39 ) }.
% 0.71/1.10 { ! alpha73, ! c2_1( a39 ), alpha62 }.
% 0.71/1.10 { ! alpha73, alpha81 }.
% 0.71/1.10 { ! alpha73, c2_2( a39, a40 ) }.
% 0.71/1.10 { ! alpha81, ! c2_2( a39, a40 ), alpha73 }.
% 0.71/1.10 { ! alpha81, ndr1_0 }.
% 0.71/1.10 { ! alpha81, ndr1_1( a39 ) }.
% 0.71/1.10 { ! alpha81, c1_2( a39, a40 ) }.
% 0.71/1.10 { ! ndr1_0, ! ndr1_1( a39 ), ! c1_2( a39, a40 ), alpha81 }.
% 0.71/1.10 { ! alpha8, alpha15 }.
% 0.71/1.10 { ! alpha8, alpha24 }.
% 0.71/1.10 { ! alpha15, ! alpha24, alpha8 }.
% 0.71/1.10 { ! alpha24, alpha37, alpha51 }.
% 0.71/1.10 { ! alpha37, alpha24 }.
% 0.71/1.10 { ! alpha51, alpha24 }.
% 0.71/1.10 { ! alpha51, alpha63( X ), c4_1( X ) }.
% 0.71/1.10 { ! alpha63( skol2 ), alpha51 }.
% 0.71/1.10 { ! c4_1( skol2 ), alpha51 }.
% 0.71/1.10 { ! alpha63( X ), ! c5_1( X ), alpha74( X ) }.
% 0.71/1.10 { c5_1( X ), alpha63( X ) }.
% 0.71/1.10 { ! alpha74( X ), alpha63( X ) }.
% 0.71/1.10 { ! alpha74( X ), alpha82( X ) }.
% 0.71/1.10 { ! alpha74( X ), c3_2( X, a38 ) }.
% 0.71/1.10 { ! alpha82( X ), ! c3_2( X, a38 ), alpha74( X ) }.
% 0.71/1.10 { ! alpha82( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha82( X ), ! c5_2( X, a38 ) }.
% 0.71/1.10 { ! alpha82( X ), c1_2( X, a38 ) }.
% 0.71/1.10 { ! ndr1_1( X ), c5_2( X, a38 ), ! c1_2( X, a38 ), alpha82( X ) }.
% 0.71/1.10 { ! alpha37, ! c3_0, ! ndr1_0 }.
% 0.71/1.10 { c3_0, alpha37 }.
% 0.71/1.10 { ndr1_0, alpha37 }.
% 0.71/1.10 { ! alpha15, alpha4 }.
% 0.71/1.10 { ! alpha15, alpha25 }.
% 0.71/1.10 { ! alpha4, ! alpha25, alpha15 }.
% 0.71/1.10 { ! alpha25, ! c4_0, ! c2_0, c5_0 }.
% 0.71/1.10 { c4_0, alpha25 }.
% 0.71/1.10 { c2_0, alpha25 }.
% 0.71/1.10 { ! c5_0, alpha25 }.
% 0.71/1.10 { ! alpha4, alpha9 }.
% 0.71/1.10 { ! alpha4, alpha16 }.
% 0.71/1.10 { ! alpha9, ! alpha16, alpha4 }.
% 0.71/1.10 { ! alpha16, alpha26, alpha38 }.
% 0.71/1.10 { ! alpha26, alpha16 }.
% 0.71/1.10 { ! alpha38, alpha16 }.
% 0.71/1.10 { ! alpha38, alpha52( X ), c4_1( X ) }.
% 0.71/1.10 { ! alpha52( skol3 ), alpha38 }.
% 0.71/1.10 { ! c4_1( skol3 ), alpha38 }.
% 0.71/1.10 { ! alpha52( X ), c5_1( X ), alpha64( X ) }.
% 0.71/1.10 { ! c5_1( X ), alpha52( X ) }.
% 0.71/1.10 { ! alpha64( X ), alpha52( X ) }.
% 0.71/1.10 { ! alpha64( X ), alpha75( X ) }.
% 0.71/1.10 { ! alpha64( X ), ! c2_2( X, a37 ) }.
% 0.71/1.10 { ! alpha75( X ), c2_2( X, a37 ), alpha64( X ) }.
% 0.71/1.10 { ! alpha75( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha75( X ), c4_2( X, a37 ) }.
% 0.71/1.10 { ! alpha75( X ), c3_2( X, a37 ) }.
% 0.71/1.10 { ! ndr1_1( X ), ! c4_2( X, a37 ), ! c3_2( X, a37 ), alpha75( X ) }.
% 0.71/1.10 { ! alpha26, alpha39, ! ndr1_0 }.
% 0.71/1.10 { ! alpha39, alpha26 }.
% 0.71/1.10 { ndr1_0, alpha26 }.
% 0.71/1.10 { ! alpha39, ! ndr1_0, alpha53 }.
% 0.71/1.10 { ndr1_0, alpha39 }.
% 0.71/1.10 { ! alpha53, alpha39 }.
% 0.71/1.10 { ! alpha53, alpha65( X ), c5_1( X ) }.
% 0.71/1.10 { ! alpha65( skol4 ), alpha53 }.
% 0.71/1.10 { ! c5_1( skol4 ), alpha53 }.
% 0.71/1.10 { ! alpha65( X ), alpha76( X ), c3_2( X, Y ), c2_2( X, Y ) }.
% 0.71/1.10 { ! alpha76( X ), alpha65( X ) }.
% 0.71/1.10 { ! c3_2( X, skol5( X ) ), alpha65( X ) }.
% 0.71/1.10 { ! c2_2( X, skol5( X ) ), alpha65( X ) }.
% 0.71/1.10 { ! alpha76( X ), alpha83( X ), ! ndr1_1( X ) }.
% 0.71/1.10 { ! alpha83( X ), alpha76( X ) }.
% 0.71/1.10 { ndr1_1( X ), alpha76( X ) }.
% 0.71/1.10 { ! alpha83( X ), alpha87( X ) }.
% 0.71/1.10 { ! alpha83( X ), c3_2( X, a36 ) }.
% 0.71/1.10 { ! alpha87( X ), ! c3_2( X, a36 ), alpha83( X ) }.
% 0.71/1.10 { ! alpha87( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha87( X ), ! c5_2( X, a36 ) }.
% 0.71/1.10 { ! alpha87( X ), ! c1_2( X, a36 ) }.
% 0.71/1.10 { ! ndr1_1( X ), c5_2( X, a36 ), c1_2( X, a36 ), alpha87( X ) }.
% 0.71/1.10 { ! alpha9, alpha2 }.
% 0.71/1.10 { ! alpha9, alpha17 }.
% 0.71/1.10 { ! alpha2, ! alpha17, alpha9 }.
% 0.71/1.10 { ! alpha17, alpha27, ! c1_0 }.
% 0.71/1.10 { ! alpha27, alpha17 }.
% 0.71/1.10 { c1_0, alpha17 }.
% 0.71/1.10 { ! alpha27, alpha40, ! c4_0 }.
% 0.71/1.10 { ! alpha40, alpha27 }.
% 0.71/1.10 { c4_0, alpha27 }.
% 0.71/1.10 { ! alpha40, alpha54 }.
% 0.71/1.10 { ! alpha40, ! c1_1( a34 ) }.
% 0.71/1.10 { ! alpha54, c1_1( a34 ), alpha40 }.
% 0.71/1.10 { ! alpha54, alpha66 }.
% 0.71/1.10 { ! alpha54, ! c2_1( a34 ) }.
% 0.71/1.10 { ! alpha66, c2_1( a34 ), alpha54 }.
% 0.71/1.10 { ! alpha66, alpha77 }.
% 0.71/1.10 { ! alpha66, ! c4_2( a34, a35 ) }.
% 0.71/1.10 { ! alpha77, c4_2( a34, a35 ), alpha66 }.
% 0.71/1.10 { ! alpha77, alpha84 }.
% 0.71/1.10 { ! alpha77, ! c5_2( a34, a35 ) }.
% 0.71/1.10 { ! alpha84, c5_2( a34, a35 ), alpha77 }.
% 0.71/1.10 { ! alpha84, ndr1_0 }.
% 0.71/1.10 { ! alpha84, ndr1_1( a34 ) }.
% 0.71/1.10 { ! alpha84, c1_2( a34, a35 ) }.
% 0.71/1.10 { ! ndr1_0, ! ndr1_1( a34 ), ! c1_2( a34, a35 ), alpha84 }.
% 0.71/1.10 { ! alpha2, alpha5 }.
% 0.71/1.10 { ! alpha2, alpha10 }.
% 0.71/1.10 { ! alpha5, ! alpha10, alpha2 }.
% 0.71/1.10 { ! alpha10, alpha18, c5_0 }.
% 0.71/1.10 { ! alpha18, alpha10 }.
% 0.71/1.10 { ! c5_0, alpha10 }.
% 0.71/1.10 { ! alpha18, alpha28, alpha41 }.
% 0.71/1.10 { ! alpha28, alpha18 }.
% 0.71/1.10 { ! alpha41, alpha18 }.
% 0.71/1.10 { ! alpha41, alpha55 }.
% 0.71/1.10 { ! alpha41, c1_1( a31 ) }.
% 0.71/1.10 { ! alpha55, ! c1_1( a31 ), alpha41 }.
% 0.71/1.10 { ! alpha55, alpha67 }.
% 0.71/1.10 { ! alpha55, c2_2( a31, a33 ) }.
% 0.71/1.10 { ! alpha67, ! c2_2( a31, a33 ), alpha55 }.
% 0.71/1.10 { ! alpha67, alpha78 }.
% 0.71/1.10 { ! alpha67, ! c5_2( a31, a33 ) }.
% 0.71/1.10 { ! alpha78, c5_2( a31, a33 ), alpha67 }.
% 0.71/1.10 { ! alpha78, alpha85 }.
% 0.71/1.10 { ! alpha78, ! c4_2( a31, a33 ) }.
% 0.71/1.10 { ! alpha85, c4_2( a31, a33 ), alpha78 }.
% 0.71/1.10 { ! alpha85, alpha88 }.
% 0.71/1.10 { ! alpha85, ndr1_1( a31 ) }.
% 0.71/1.10 { ! alpha88, ! ndr1_1( a31 ), alpha85 }.
% 0.71/1.10 { ! alpha88, alpha90 }.
% 0.71/1.10 { ! alpha88, c5_2( a31, a32 ) }.
% 0.71/1.10 { ! alpha90, ! c5_2( a31, a32 ), alpha88 }.
% 0.71/1.10 { ! alpha90, alpha92 }.
% 0.71/1.10 { ! alpha90, ! c4_2( a31, a32 ) }.
% 0.71/1.10 { ! alpha92, c4_2( a31, a32 ), alpha90 }.
% 0.71/1.10 { ! alpha92, ndr1_0 }.
% 0.71/1.10 { ! alpha92, ndr1_1( a31 ) }.
% 0.71/1.10 { ! alpha92, c3_2( a31, a32 ) }.
% 0.71/1.10 { ! ndr1_0, ! ndr1_1( a31 ), ! c3_2( a31, a32 ), alpha92 }.
% 0.71/1.10 { ! alpha28, ndr1_0 }.
% 0.71/1.10 { ! alpha28, ! c1_1( a30 ) }.
% 0.71/1.10 { ! alpha28, c3_1( a30 ) }.
% 0.71/1.10 { ! ndr1_0, c1_1( a30 ), ! c3_1( a30 ), alpha28 }.
% 0.71/1.10 { ! alpha5, alpha1 }.
% 0.71/1.10 { ! alpha5, alpha11 }.
% 0.71/1.10 { ! alpha1, ! alpha11, alpha5 }.
% 0.71/1.10 { ! alpha11, alpha19, alpha29 }.
% 0.71/1.10 { ! alpha19, alpha11 }.
% 0.71/1.10 { ! alpha29, alpha11 }.
% 0.71/1.10 { ! alpha29, alpha42( X ), alpha56( X ) }.
% 0.71/1.10 { ! alpha42( skol6 ), alpha29 }.
% 0.71/1.10 { ! alpha56( skol6 ), alpha29 }.
% 0.71/1.10 { ! alpha56( X ), ! c3_2( X, Y ), ! c5_2( X, Y ), ! c1_2( X, Y ) }.
% 0.71/1.10 { c3_2( X, skol7( X ) ), alpha56( X ) }.
% 0.71/1.10 { c5_2( X, skol7( X ) ), alpha56( X ) }.
% 0.71/1.10 { c1_2( X, skol7( X ) ), alpha56( X ) }.
% 0.71/1.10 { ! alpha42( X ), alpha57( X ), ! ndr1_1( X ) }.
% 0.71/1.10 { ! alpha57( X ), alpha42( X ) }.
% 0.71/1.10 { ndr1_1( X ), alpha42( X ) }.
% 0.71/1.10 { ! alpha57( X ), c3_1( X ), alpha68( X ) }.
% 0.71/1.10 { ! c3_1( X ), alpha57( X ) }.
% 0.71/1.10 { ! alpha68( X ), alpha57( X ) }.
% 0.71/1.10 { ! alpha68( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha68( X ), ! c1_2( X, a29 ) }.
% 0.71/1.10 { ! alpha68( X ), c2_2( X, a29 ) }.
% 0.71/1.10 { ! ndr1_1( X ), c1_2( X, a29 ), ! c2_2( X, a29 ), alpha68( X ) }.
% 0.71/1.10 { ! alpha19, alpha30, ! ndr1_0 }.
% 0.71/1.10 { ! alpha30, alpha19 }.
% 0.71/1.10 { ndr1_0, alpha19 }.
% 0.71/1.10 { ! alpha30, ! ndr1_0, alpha43 }.
% 0.71/1.10 { ndr1_0, alpha30 }.
% 0.71/1.10 { ! alpha43, alpha30 }.
% 0.71/1.10 { ! alpha43, c2_1( X ), alpha58( X ) }.
% 0.71/1.10 { ! c2_1( skol8 ), alpha43 }.
% 0.71/1.10 { ! alpha58( skol8 ), alpha43 }.
% 0.71/1.10 { ! alpha58( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha58( X ), ! c5_2( X, a28 ) }.
% 0.71/1.10 { ! alpha58( X ), ! c3_2( X, a28 ) }.
% 0.71/1.10 { ! ndr1_1( X ), c5_2( X, a28 ), c3_2( X, a28 ), alpha58( X ) }.
% 0.71/1.10 { ! alpha1, alpha3 }.
% 0.71/1.10 { ! alpha1, alpha6 }.
% 0.71/1.10 { ! alpha3, ! alpha6, alpha1 }.
% 0.71/1.10 { ! alpha6, alpha12, alpha20 }.
% 0.71/1.10 { ! alpha12, alpha6 }.
% 0.71/1.10 { ! alpha20, alpha6 }.
% 0.71/1.10 { ! alpha20, alpha31( X ), ! c4_1( X ) }.
% 0.71/1.10 { ! alpha31( skol9 ), alpha20 }.
% 0.71/1.10 { c4_1( skol9 ), alpha20 }.
% 0.71/1.10 { ! alpha31( X ), ! ndr1_1( X ), alpha44( X ) }.
% 0.71/1.10 { ndr1_1( X ), alpha31( X ) }.
% 0.71/1.10 { ! alpha44( X ), alpha31( X ) }.
% 0.71/1.10 { ! alpha44( X ), c2_2( X, Y ), ! c5_2( X, Y ), c4_2( X, Y ) }.
% 0.71/1.10 { ! c2_2( X, skol10( X ) ), alpha44( X ) }.
% 0.71/1.10 { c5_2( X, skol10( X ) ), alpha44( X ) }.
% 0.71/1.10 { ! c4_2( X, skol10( X ) ), alpha44( X ) }.
% 0.71/1.10 { ! alpha12, c1_0, ! ndr1_0 }.
% 0.71/1.10 { ! c1_0, alpha12 }.
% 0.71/1.10 { ndr1_0, alpha12 }.
% 0.71/1.10 { ! alpha3, alpha7, alpha13 }.
% 0.71/1.10 { ! alpha7, alpha3 }.
% 0.71/1.10 { ! alpha13, alpha3 }.
% 0.71/1.10 { ! alpha13, alpha21( X ), alpha32( X ) }.
% 0.71/1.10 { ! alpha21( skol11 ), alpha13 }.
% 0.71/1.10 { ! alpha32( skol11 ), alpha13 }.
% 0.71/1.10 { ! alpha32( X ), alpha45( X ) }.
% 0.71/1.10 { ! alpha32( X ), c4_2( X, a27 ) }.
% 0.71/1.10 { ! alpha45( X ), ! c4_2( X, a27 ), alpha32( X ) }.
% 0.71/1.10 { ! alpha45( X ), ndr1_1( X ) }.
% 0.71/1.10 { ! alpha45( X ), ! c1_2( X, a27 ) }.
% 0.71/1.10 { ! alpha45( X ), ! c5_2( X, a27 ) }.
% 0.71/1.10 { ! ndr1_1( X ), c1_2( X, a27 ), c5_2( X, a27 ), alpha45( X ) }.
% 0.71/1.10 { ! alpha21( X ), ! ndr1_1( X ), alpha33( X ) }.
% 0.71/1.10 { ndr1_1( X ), alpha21( X ) }.
% 0.71/1.10 { ! alpha33( X ), alpha21( X ) }.
% 0.71/1.10 { ! alpha33( X ), c3_2( X, Y ), ! c4_2( X, Y ), c5_2( X, Y ) }.
% 0.71/1.10 { ! c3_2( X, skol12( X ) ), alpha33( X ) }.
% 0.71/1.10 { c4_2( X, skol12( X ) ), alpha33( X ) }.
% 0.71/1.10 { ! c5_2( X, skol12( X ) ), alpha33( X ) }.
% 0.71/1.10 { ! alpha7, c4_0, c5_0, ! ndr1_0 }.
% 0.71/1.10 { ! c4_0, alpha7 }.
% 0.71/1.10 { ! c5_0, alpha7 }.
% 0.71/1.10 { ndr1_0, alpha7 }.
% 0.71/1.10
% 0.71/1.10 percentage equality = 0.000000, percentage horn = 0.756667
% 0.71/1.10 This a non-horn, non-equality problem
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Options Used:
% 0.71/1.10
% 0.71/1.10 useres = 1
% 0.71/1.10 useparamod = 0
% 0.71/1.10 useeqrefl = 0
% 0.71/1.10 useeqfact = 0
% 0.71/1.10 usefactor = 1
% 0.71/1.10 usesimpsplitting = 0
% 0.71/1.10 usesimpdemod = 0
% 0.71/1.10 usesimpres = 3
% 0.71/1.10
% 0.71/1.10 resimpinuse = 1000
% 0.71/1.10 resimpclauses = 20000
% 0.71/1.10 substype = standard
% 0.71/1.10 backwardsubs = 1
% 0.71/1.10 selectoldest = 5
% 0.71/1.10
% 0.71/1.10 litorderings [0] = split
% 0.71/1.10 litorderings [1] = liftord
% 0.71/1.10
% 0.71/1.10 termordering = none
% 0.71/1.10
% 0.71/1.10 litapriori = 1
% 0.71/1.10 termapriori = 0
% 0.71/1.10 litaposteriori = 0
% 0.71/1.10 termaposteriori = 0
% 0.71/1.10 demodaposteriori = 0
% 0.71/1.10 ordereqreflfact = 0
% 0.71/1.10
% 0.71/1.10 litselect = none
% 0.71/1.10
% 0.71/1.10 maxweight = 15
% 0.71/1.10 maxdepth = 30000
% 0.71/1.10 maxlength = 115
% 0.71/1.10 maxnrvars = 195
% 0.71/1.10 excuselevel = 1
% 0.71/1.10 increasemaxweight = 1
% 0.71/1.10
% 0.71/1.10 maxselected = 10000000
% 0.71/1.10 maxnrclauses = 10000000
% 0.71/1.10
% 0.71/1.10 showgenerated = 0
% 0.71/1.10 showkept = 0
% 0.71/1.10 showselected = 0
% 0.71/1.10 showdeleted = 0
% 0.71/1.10 showresimp = 1
% 0.71/1.10 showstatus = 2000
% 0.71/1.10
% 0.71/1.10 prologoutput = 0
% 0.71/1.10 nrgoals = 5000000
% 0.71/1.10 totalproof = 1
% 0.71/1.10
% 0.71/1.10 Symbols occurring in the translation:
% 0.71/1.10
% 0.71/1.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.71/1.10 . [1, 2] (w:1, o:162, a:1, s:1, b:0),
% 0.71/1.10 ! [4, 1] (w:0, o:126, a:1, s:1, b:0),
% 0.71/1.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.10 c4_0 [35, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.71/1.10 c5_0 [36, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.71/1.10 ndr1_0 [38, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.71/1.10 ndr1_1 [40, 1] (w:1, o:131, a:1, s:1, b:0),
% 0.71/1.10 c3_2 [41, 2] (w:1, o:187, a:1, s:1, b:0),
% 0.71/1.10 c4_2 [42, 2] (w:1, o:188, a:1, s:1, b:0),
% 0.71/1.10 c5_2 [43, 2] (w:1, o:189, a:1, s:1, b:0),
% 0.71/1.10 a27 [44, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.71/1.10 c1_2 [45, 2] (w:1, o:190, a:1, s:1, b:0),
% 0.71/1.10 c1_0 [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.71/1.10 c2_2 [49, 2] (w:1, o:186, a:1, s:1, b:0),
% 0.71/1.10 c4_1 [50, 1] (w:1, o:133, a:1, s:1, b:0),
% 0.71/1.10 c2_1 [52, 1] (w:1, o:135, a:1, s:1, b:0),
% 0.71/1.10 a28 [53, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.71/1.10 c3_1 [55, 1] (w:1, o:132, a:1, s:1, b:0),
% 0.71/1.10 a29 [56, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.71/1.10 a30 [58, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.71/1.11 c1_1 [59, 1] (w:1, o:134, a:1, s:1, b:0),
% 0.71/1.11 a31 [60, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.71/1.11 a32 [61, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.71/1.11 a33 [62, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.71/1.11 a34 [63, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.71/1.11 a35 [64, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.71/1.11 a36 [66, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.71/1.11 c5_1 [68, 1] (w:1, o:136, a:1, s:1, b:0),
% 0.71/1.11 a37 [70, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.71/1.11 c2_0 [71, 0] (w:1, o:34, a:1, s:1, b:0),
% 0.71/1.11 c3_0 [72, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.71/1.11 a38 [74, 0] (w:1, o:35, a:1, s:1, b:0),
% 0.71/1.11 a39 [75, 0] (w:1, o:36, a:1, s:1, b:0),
% 0.71/1.11 a40 [76, 0] (w:1, o:37, a:1, s:1, b:0),
% 0.71/1.11 a41 [78, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.71/1.11 a42 [79, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.71/1.11 a43 [80, 0] (w:1, o:40, a:1, s:1, b:0),
% 0.71/1.11 a44 [81, 0] (w:1, o:41, a:1, s:1, b:0),
% 0.71/1.11 a45 [82, 0] (w:1, o:42, a:1, s:1, b:0),
% 0.71/1.11 a46 [83, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.71/1.11 a47 [84, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.71/1.11 a48 [85, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.71/1.11 a49 [86, 0] (w:1, o:46, a:1, s:1, b:0),
% 0.71/1.11 alpha1 [87, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.71/1.11 alpha2 [88, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.71/1.11 alpha3 [89, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.71/1.11 alpha4 [90, 0] (w:1, o:76, a:1, s:1, b:0),
% 0.71/1.11 alpha5 [91, 0] (w:1, o:84, a:1, s:1, b:0),
% 0.71/1.11 alpha6 [92, 0] (w:1, o:91, a:1, s:1, b:0),
% 0.71/1.11 alpha7 [93, 0] (w:1, o:98, a:1, s:1, b:0),
% 0.71/1.11 alpha8 [94, 0] (w:1, o:106, a:1, s:1, b:0),
% 0.71/1.11 alpha9 [95, 0] (w:1, o:114, a:1, s:1, b:0),
% 0.71/1.11 alpha10 [96, 0] (w:1, o:48, a:1, s:1, b:0),
% 0.71/1.11 alpha11 [97, 0] (w:1, o:49, a:1, s:1, b:0),
% 0.71/1.11 alpha12 [98, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.71/1.11 alpha13 [99, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.71/1.11 alpha14 [100, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.71/1.11 alpha15 [101, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.71/1.11 alpha16 [102, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.71/1.11 alpha17 [103, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.71/1.11 alpha18 [104, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.71/1.11 alpha19 [105, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.71/1.11 alpha20 [106, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.71/1.11 alpha21 [107, 1] (w:1, o:137, a:1, s:1, b:0),
% 0.71/1.11 alpha22 [108, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.71/1.11 alpha23 [109, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.71/1.11 alpha24 [110, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.71/1.11 alpha25 [111, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.71/1.11 alpha26 [112, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.71/1.11 alpha27 [113, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.71/1.11 alpha28 [114, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.71/1.11 alpha29 [115, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.71/1.11 alpha30 [116, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.71/1.11 alpha31 [117, 1] (w:1, o:138, a:1, s:1, b:0),
% 0.71/1.11 alpha32 [118, 1] (w:1, o:139, a:1, s:1, b:0),
% 0.71/1.11 alpha33 [119, 1] (w:1, o:140, a:1, s:1, b:0),
% 0.71/1.11 alpha34 [120, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.71/1.11 alpha35 [121, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.71/1.11 alpha36 [122, 0] (w:1, o:72, a:1, s:1, b:0),
% 0.71/1.11 alpha37 [123, 0] (w:1, o:73, a:1, s:1, b:0),
% 0.71/1.11 alpha38 [124, 0] (w:1, o:74, a:1, s:1, b:0),
% 0.71/1.11 alpha39 [125, 0] (w:1, o:75, a:1, s:1, b:0),
% 0.71/1.11 alpha40 [126, 0] (w:1, o:77, a:1, s:1, b:0),
% 0.71/1.11 alpha41 [127, 0] (w:1, o:78, a:1, s:1, b:0),
% 0.71/1.11 alpha42 [128, 1] (w:1, o:141, a:1, s:1, b:0),
% 0.71/1.11 alpha43 [129, 0] (w:1, o:79, a:1, s:1, b:0),
% 0.71/1.11 alpha44 [130, 1] (w:1, o:142, a:1, s:1, b:0),
% 0.71/1.11 alpha45 [131, 1] (w:1, o:143, a:1, s:1, b:0),
% 0.71/1.11 alpha46 [132, 0] (w:1, o:80, a:1, s:1, b:0),
% 0.71/1.11 alpha47 [133, 0] (w:1, o:81, a:1, s:1, b:0),
% 0.71/1.11 alpha48 [134, 0] (w:1, o:82, a:1, s:1, b:0),
% 0.71/1.11 alpha49 [135, 0] (w:1, o:83, a:1, s:1, b:0),
% 0.71/1.11 alpha50 [136, 0] (w:1, o:85, a:1, s:1, b:0),
% 0.71/1.11 alpha51 [137, 0] (w:1, o:86, a:1, s:1, b:0),
% 0.71/1.11 alpha52 [138, 1] (w:1, o:144, a:1, s:1, b:0),
% 0.71/1.11 alpha53 [139, 0] (w:1, o:87, a:1, s:1, b:0),
% 0.71/1.11 alpha54 [140, 0] (w:1, o:88, a:1, s:1, b:0),
% 0.71/1.11 alpha55 [141, 0] (w:1, o:89, a:1, s:1, b:0),
% 0.71/1.11 alpha56 [142, 1] (w:1, o:145, a:1, s:1, b:0),
% 0.71/1.11 alpha57 [143, 1] (w:1, o:146, a:1, s:1, b:0),
% 0.71/1.11 alpha58 [144, 1] (w:1, o:147, a:1, s:1, b:0),
% 0.71/1.11 alpha59 [145, 0] (w:1, o:90, a:1, s:1, b:0),
% 0.71/1.11 alpha60 [146, 0] (w:1, o:92, a:1, s:1, b:0),
% 0.71/1.11 alpha61 [147, 0] (w:1, o:93, a:1, s:1, b:0),
% 0.71/1.11 alpha62 [148, 0] (w:1, o:94, a:1, s:1, b:0),
% 0.71/1.11 alpha63 [149, 1] (w:1, o:148, a:1, s:1, b:0),
% 0.71/1.11 alpha64 [150, 1] (w:1, o:149, a:1, s:1, b:0),
% 0.71/1.11 alpha65 [151, 1] (w:1, o:150, a:1, s:1, b:0),
% 0.71/1.11 alpha66 [152, 0] (w:1, o:95, a:1, s:1, b:0),
% 0.71/1.11 alpha67 [153, 0] (w:1, o:96, a:1, s:1, b:0),
% 0.71/1.11 alpha68 [154, 1] (w:1, o:151, a:1, s:1, b:0),
% 0.71/1.11 alpha69 [155, 0] (w:1, o:97, a:1, s:1, b:0),
% 0.71/1.11 alpha70 [156, 0] (w:1, o:99, a:1, s:1, b:0),
% 0.71/1.11 alpha71 [157, 0] (w:1, o:100, a:1, s:1, b:0),
% 0.71/1.11 alpha72 [158, 0] (w:1, o:101, a:1, s:1, b:0),
% 0.71/1.11 alpha73 [159, 0] (w:1, o:102, a:1, s:1, b:0),
% 0.71/1.11 alpha74 [160, 1] (w:1, o:152, a:1, s:1, b:0),
% 0.71/1.11 alpha75 [161, 1] (w:1, o:153, a:1, s:1, b:0),
% 0.71/1.11 alpha76 [162, 1] (w:1, o:154, a:1, s:1, b:0),
% 0.71/1.11 alpha77 [163, 0] (w:1, o:103, a:1, s:1, b:0),
% 0.71/1.11 alpha78 [164, 0] (w:1, o:104, a:1, s:1, b:0),
% 0.71/1.11 alpha79 [165, 0] (w:1, o:105, a:1, s:1, b:0),
% 0.71/1.11 alpha80 [166, 0] (w:1, o:107, a:1, s:1, b:0),
% 0.71/1.11 alpha81 [167, 0] (w:1, o:108, a:1, s:1, b:0),
% 0.71/1.11 alpha82 [168, 1] (w:1, o:155, a:1, s:1, b:0),
% 0.71/1.11 alpha83 [169, 1] (w:1, o:156, a:1, s:1, b:0),
% 0.71/1.11 alpha84 [170, 0] (w:1, o:109, a:1, s:1, b:0),
% 0.71/1.11 alpha85 [171, 0] (w:1, o:110, a:1, s:1, b:0),
% 0.71/1.11 alpha86 [172, 0] (w:1, o:111, a:1, s:1, b:0),
% 0.71/1.11 alpha87 [173, 1] (w:1, o:157, a:1, s:1, b:0),
% 0.71/1.11 alpha88 [174, 0] (w:1, o:112, a:1, s:1, b:0),
% 0.71/1.11 alpha89 [175, 0] (w:1, o:113, a:1, s:1, b:0),
% 0.71/1.11 alpha90 [176, 0] (w:1, o:115, a:1, s:1, b:0),
% 0.71/1.11 alpha91 [177, 0] (w:1, o:116, a:1, s:1, b:0),
% 0.71/1.11 alpha92 [178, 0] (w:1, o:117, a:1, s:1, b:0),
% 0.71/1.11 skol1 [179, 0] (w:1, o:118, a:1, s:1, b:0),
% 0.71/1.11 skol2 [180, 0] (w:1, o:120, a:1, s:1, b:0),
% 0.71/1.11 skol3 [181, 0] (w:1, o:121, a:1, s:1, b:0),
% 0.71/1.11 skol4 [182, 0] (w:1, o:122, a:1, s:1, b:0),
% 0.71/1.11 skol5 [183, 1] (w:1, o:158, a:1, s:1, b:0),
% 0.71/1.11 skol6 [184, 0] (w:1, o:123, a:1, s:1, b:0),
% 0.71/1.11 skol7 [185, 1] (w:1, o:159, a:1, s:1, b:0),
% 0.71/1.11 skol8 [186, 0] (w:1, o:124, a:1, s:1, b:0),
% 0.71/1.11 skol9 [187, 0] (w:1, o:125, a:1, s:1, b:0),
% 0.71/1.11 skol10 [188, 1] (w:1, o:160, a:1, s:1, b:0),
% 0.71/1.11 skol11 [189, 0] (w:1, o:119, a:1, s:1, b:0),
% 0.71/1.11 skol12 [190, 1] (w:1, o:161, a:1, s:1, b:0).
% 0.71/1.11
% 0.71/1.11
% 0.71/1.11 Starting Search:
% 0.71/1.11
% 0.71/1.11 *** allocated 15000 integers for clauses
% 0.71/1.11 *** allocated 22500 integers for clauses
% 0.71/1.11 Resimplifying inuse:
% 0.71/1.11 Done
% 0.71/1.11
% 0.71/1.11 Resimplifying inuse:
% 0.71/1.11 Done
% 0.71/1.11
% 0.71/1.11
% 0.71/1.11
% 0.71/1.11 found a saturation!
% 0.71/1.11 % SZS status CounterSatisfiable
% 0.71/1.11 % SZS output start Saturation
% 0.71/1.11
% 0.71/1.11 (385) {G21,W2,D1,L2,V0,M1} S(220);r(314) { alpha43, ! alpha30 }.
% 0.71/1.11 (384) {G21,W2,D1,L2,V0,M1} S(120);r(314) { alpha53, ! alpha39 }.
% 0.71/1.11 (383) {G21,W2,D1,L2,V0,M1} S(95);r(314) { ! c3_0, ! alpha37 }.
% 0.71/1.11 (372) {G1,W15,D2,L6,V1,M1} R(239,229) { ! alpha44( X ), c2_2( X, a28 ), !
% 0.71/1.11 ndr1_1( X ), c3_2( X, a28 ), alpha58( X ), c4_2( X, a28 ) }.
% 0.71/1.11 (373) {G1,W12,D3,L4,V1,M1} R(239,205) { ! alpha44( X ), c2_2( X, skol7( X )
% 0.71/1.11 ), alpha56( X ), c4_2( X, skol7( X ) ) }.
% 0.71/1.11 (371) {G1,W15,D2,L6,V1,M1} R(216,203) { ! ndr1_1( X ), alpha68( X ), !
% 0.71/1.11 alpha56( X ), ! c2_2( X, a29 ), ! c3_2( X, a29 ), ! c5_2( X, a29 ) }.
% 0.71/1.11 (376) {G22,W11,D2,L5,V0,M1} R(260,329) { ! alpha33( a41 ), c3_2( a41, a42 )
% 0.71/1.11 , ! ndr1_1( a41 ), alpha80, ! c4_2( a41, a42 ) }.
% 0.71/1.11 (367) {G1,W10,D3,L4,V1,M1} R(261,126) { alpha33( X ), ! alpha65( X ),
% 0.71/1.11 alpha76( X ), c2_2( X, skol12( X ) ) }.
% 0.71/1.11 (381) {G1,W10,D2,L5,V0,M1} R(260,2) { ! alpha33( a48 ), c3_2( a48, a49 ),
% 0.71/1.11 alpha34, c1_0, ! c4_2( a48, a49 ) }.
% 0.71/1.11 (380) {G1,W10,D2,L4,V1,M1} R(260,92) { ! alpha33( X ), c3_2( X, a38 ), !
% 0.71/1.11 alpha82( X ), ! c4_2( X, a38 ) }.
% 0.71/1.11 (357) {G1,W11,D2,L5,V1,M1} R(126,90) { ! alpha65( X ), alpha76( X ), !
% 0.71/1.11 alpha82( X ), alpha74( X ), c2_2( X, a38 ) }.
% 0.71/1.11 (382) {G2,W7,D2,L3,V1,M1} R(379,251);r(250) { ! alpha33( X ), ! alpha32( X
% 0.71/1.11 ), c3_2( X, a27 ) }.
% 0.71/1.11 (379) {G1,W10,D2,L4,V1,M1} R(260,255) { ! alpha33( X ), c3_2( X, a27 ), !
% 0.71/1.11 alpha45( X ), ! c4_2( X, a27 ) }.
% 0.71/1.11 (377) {G1,W10,D2,L4,V1,M1} R(260,137) { ! alpha33( X ), c3_2( X, a36 ), !
% 0.71/1.11 alpha87( X ), ! c4_2( X, a36 ) }.
% 0.71/1.11 (378) {G1,W7,D2,L3,V1,M1} R(260,227);r(228) { ! alpha33( X ), ! alpha58( X
% 0.71/1.11 ), ! c4_2( X, a28 ) }.
% 0.71/1.11 (260) {G0,W11,D2,L4,V2,M1} I { ! alpha33( X ), c3_2( X, Y ), ! c4_2( X, Y )
% 0.71/1.11 , c5_2( X, Y ) }.
% 0.71/1.11 (256) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c5_2( X, a27 ), alpha45( X )
% 0.71/1.11 , c1_2( X, a27 ) }.
% 0.71/1.11 (368) {G9,W9,D2,L4,V0,M1} R(203,303) { ! alpha56( a44 ), ! c3_2( a44, a45 )
% 0.71/1.11 , alpha60, ! c5_2( a44, a45 ) }.
% 0.71/1.11 (375) {G1,W9,D2,L4,V0,M1} R(239,67) { ! alpha44( a39 ), c2_2( a39, skol1 )
% 0.71/1.11 , alpha72, c4_2( a39, skol1 ) }.
% 0.71/1.11 (374) {G18,W7,D2,L4,V0,M1} R(239,347);r(346) { ! alpha44( a31 ), c5_0,
% 0.71/1.11 alpha28, c2_2( a31, a32 ) }.
% 0.71/1.11 (239) {G0,W11,D2,L4,V2,M1} I { ! alpha44( X ), c2_2( X, Y ), c4_2( X, Y ),
% 0.71/1.11 ! c5_2( X, Y ) }.
% 0.71/1.11 (356) {G1,W9,D2,L4,V1,M1} R(126,228) { ! alpha65( X ), alpha76( X ), !
% 0.71/1.11 alpha58( X ), c2_2( X, a28 ) }.
% 0.71/1.11 (361) {G1,W9,D2,L4,V1,M1} R(135,126);r(131) { ! alpha65( X ), alpha76( X )
% 0.71/1.11 , ! alpha87( X ), c2_2( X, a36 ) }.
% 0.71/1.11 (369) {G22,W8,D2,L5,V0,M1} R(360,318) { ndr1_1( a43 ), alpha37, c4_1( a43 )
% 0.71/1.11 , alpha70, c2_1( a43 ) }.
% 0.71/1.11 (358) {G8,W8,D2,L4,V0,M1} R(126,323) { ! alpha65( a41 ), alpha76( a41 ),
% 0.71/1.11 alpha36, c2_2( a41, a42 ) }.
% 0.71/1.11 (229) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c3_2( X, a28 ), alpha58( X )
% 0.71/1.11 , c5_2( X, a28 ) }.
% 0.71/1.11 (366) {G22,W8,D2,L4,V0,M1} R(365,126);r(132) { alpha92, ! alpha65( a31 ),
% 0.71/1.11 alpha76( a31 ), c2_2( a31, a32 ) }.
% 0.71/1.11 (370) {G10,W6,D2,L4,V1,M1} R(359,360);f;f { ndr1_1( X ), alpha26, alpha37,
% 0.71/1.11 c4_1( X ) }.
% 0.71/1.11 (216) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c2_2( X, a29 ), alpha68( X
% 0.71/1.11 ), c1_2( X, a29 ) }.
% 0.71/1.11 (359) {G9,W7,D2,L4,V1,M1} R(352,351) { ndr1_1( X ), c4_1( X ), alpha26,
% 0.71/1.11 c5_1( X ) }.
% 0.71/1.11 (360) {G7,W7,D2,L4,V1,M1} R(344,343) { ndr1_1( X ), c4_1( X ), alpha37, !
% 0.71/1.11 c5_1( X ) }.
% 0.71/1.11 (252) {G0,W7,D2,L3,V1,M1} I { ! alpha45( X ), alpha32( X ), ! c4_2( X, a27
% 0.71/1.11 ) }.
% 0.71/1.11 (205) {G0,W6,D3,L2,V1,M1} I { alpha56( X ), c5_2( X, skol7( X ) ) }.
% 0.71/1.11 (204) {G0,W6,D3,L2,V1,M1} I { alpha56( X ), c3_2( X, skol7( X ) ) }.
% 0.71/1.11 (206) {G0,W6,D3,L2,V1,M1} I { alpha56( X ), c1_2( X, skol7( X ) ) }.
% 0.71/1.11 (240) {G0,W6,D3,L2,V1,M1} I { alpha44( X ), ! c2_2( X, skol10( X ) ) }.
% 0.71/1.11 (241) {G0,W6,D3,L2,V1,M1} I { alpha44( X ), c5_2( X, skol10( X ) ) }.
% 0.71/1.11 (242) {G0,W6,D3,L2,V1,M1} I { alpha44( X ), ! c4_2( X, skol10( X ) ) }.
% 0.71/1.11 (203) {G0,W11,D2,L4,V2,M1} I { ! alpha56( X ), ! c3_2( X, Y ), ! c5_2( X, Y
% 0.71/1.11 ), ! c1_2( X, Y ) }.
% 0.71/1.11 (261) {G0,W6,D3,L2,V1,M1} I { alpha33( X ), ! c3_2( X, skol12( X ) ) }.
% 0.71/1.11 (262) {G0,W6,D3,L2,V1,M1} I { alpha33( X ), c4_2( X, skol12( X ) ) }.
% 0.71/1.11 (263) {G0,W6,D3,L2,V1,M1} I { alpha33( X ), ! c5_2( X, skol12( X ) ) }.
% 0.71/1.11 (365) {G21,W6,D2,L3,V0,M1} S(192);r(314) { ! ndr1_1( a31 ), alpha92, ! c3_2
% 0.71/1.11 ( a31, a32 ) }.
% 0.71/1.11 (364) {G21,W5,D2,L3,V0,M1} S(196);r(314) { ! c3_1( a30 ), alpha28, c1_1(
% 0.71/1.11 a30 ) }.
% 0.71/1.11 (363) {G21,W6,D2,L3,V0,M1} S(161);r(314) { ! ndr1_1( a34 ), alpha84, ! c1_2
% 0.71/1.11 ( a34, a35 ) }.
% 0.71/1.11 (353) {G21,W6,D2,L4,V1,M1} R(247,326) { alpha21( X ), c4_0, c5_0, alpha32(
% 0.71/1.11 X ) }.
% 0.71/1.11 (315) {G21,W6,D2,L3,V0,M1} R(314,35) { ! ndr1_1( a44 ), alpha91, ! c1_2(
% 0.71/1.11 a44, a45 ) }.
% 0.71/1.11 (329) {G21,W6,D2,L3,V0,M1} S(58);r(314) { ! ndr1_1( a41 ), alpha80, ! c5_2
% 0.71/1.11 ( a41, a42 ) }.
% 0.71/1.11 (139) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c5_2( X, a36 ), alpha87( X )
% 0.71/1.11 , c1_2( X, a36 ) }.
% 0.71/1.11 (341) {G21,W6,D2,L3,V0,M1} S(78);r(314) { ! ndr1_1( a39 ), alpha81, ! c1_2
% 0.71/1.11 ( a39, a40 ) }.
% 0.71/1.11 (207) {G0,W6,D2,L3,V1,M1} I { ! alpha42( X ), ! ndr1_1( X ), alpha57( X )
% 0.71/1.11 }.
% 0.71/1.11 (362) {G1,W6,D2,L3,V1,M1} R(210,213) { c3_1( X ), ndr1_1( X ), ! alpha57( X
% 0.71/1.11 ) }.
% 0.71/1.11 (210) {G0,W6,D2,L3,V1,M1} I { c3_1( X ), ! alpha57( X ), alpha68( X ) }.
% 0.71/1.11 (135) {G0,W7,D2,L3,V1,M1} I { ! alpha87( X ), alpha83( X ), ! c3_2( X, a36
% 0.71/1.11 ) }.
% 0.71/1.11 (236) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha31( X ), alpha44( X )
% 0.71/1.11 }.
% 0.71/1.11 (257) {G0,W6,D2,L3,V1,M1} I { ! ndr1_1( X ), ! alpha21( X ), alpha33( X )
% 0.71/1.11 }.
% 0.71/1.11 (344) {G2,W6,D2,L3,V1,M1} R(85,340) { ! c5_1( X ), ndr1_1( X ), ! alpha63(
% 0.71/1.11 X ) }.
% 0.71/1.11 (352) {G2,W6,D2,L3,V1,M1} R(107,338) { c5_1( X ), ndr1_1( X ), ! alpha52( X
% 0.71/1.11 ) }.
% 0.71/1.11 (130) {G0,W6,D2,L3,V1,M1} I { ! alpha76( X ), ! ndr1_1( X ), alpha83( X )
% 0.71/1.11 }.
% 0.71/1.11 (154) {G0,W5,D2,L3,V0,M1} I { c4_2( a34, a35 ), alpha66, ! alpha77 }.
% 0.71/1.11 (157) {G0,W5,D2,L3,V0,M1} I { c5_2( a34, a35 ), alpha77, ! alpha84 }.
% 0.71/1.11 (173) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a31, a33 ), alpha55, ! alpha67 }.
% 0.71/1.11 (176) {G0,W5,D2,L3,V0,M1} I { c5_2( a31, a33 ), alpha67, ! alpha78 }.
% 0.71/1.11 (129) {G0,W6,D3,L2,V1,M1} I { alpha65( X ), ! c2_2( X, skol5( X ) ) }.
% 0.71/1.11 (179) {G0,W5,D2,L3,V0,M1} I { c4_2( a31, a33 ), alpha78, ! alpha85 }.
% 0.71/1.11 (185) {G0,W5,D2,L3,V0,M1} I { ! c5_2( a31, a32 ), alpha88, ! alpha90 }.
% 0.71/1.11 (188) {G0,W5,D2,L3,V0,M1} I { c4_2( a31, a32 ), alpha90, ! alpha92 }.
% 0.71/1.11 (269) {G1,W5,D2,L3,V0,M1} R(4,1) { alpha34, c1_0, ! c1_2( a48, a49 ) }.
% 0.71/1.11 (128) {G0,W6,D3,L2,V1,M1} I { alpha65( X ), ! c3_2( X, skol5( X ) ) }.
% 0.71/1.11 (317) {G21,W5,D2,L3,V0,M1} R(314,9) { ! ndr1_1( a48 ), alpha59, ! c4_1( a48
% 0.71/1.11 ) }.
% 0.71/1.11 (318) {G21,W5,D2,L3,V0,M1} S(42);r(314) { c2_1( a43 ), alpha70, c5_1( a43 )
% 0.71/1.11 }.
% 0.71/1.11 (345) {G18,W5,D2,L3,V0,M1} R(191,296) { c5_0, alpha28, c3_2( a31, a32 ) }.
% 0.71/1.11 (346) {G17,W5,D2,L3,V0,M1} R(187,295) { c5_0, alpha28, ! c4_2( a31, a32 )
% 0.71/1.11 }.
% 0.71/1.11 (126) {G0,W10,D2,L4,V2,M1} I { ! alpha65( X ), alpha76( X ), c2_2( X, Y ),
% 0.71/1.11 c3_2( X, Y ) }.
% 0.71/1.11 (347) {G16,W5,D2,L3,V0,M1} R(184,293) { c5_0, alpha28, c5_2( a31, a32 ) }.
% 0.71/1.11 (348) {G14,W5,D2,L3,V0,M1} R(178,291) { c5_0, alpha28, ! c4_2( a31, a33 )
% 0.71/1.11 }.
% 0.71/1.11 (349) {G13,W5,D2,L3,V0,M1} R(175,290) { c5_0, alpha28, ! c5_2( a31, a33 )
% 0.71/1.11 }.
% 0.71/1.11 (350) {G12,W5,D2,L3,V0,M1} R(172,289) { c5_0, alpha28, c2_2( a31, a33 ) }.
% 0.71/1.11 (123) {G0,W5,D2,L3,V1,M1} I { alpha65( X ), c5_1( X ), ! alpha53 }.
% 0.71/1.11 (355) {G11,W5,D2,L3,V1,M1} R(200,199) { alpha42( X ), alpha19, alpha56( X )
% 0.71/1.11 }.
% 0.71/1.11 (200) {G0,W5,D2,L3,V1,M1} I { alpha42( X ), alpha56( X ), ! alpha29 }.
% 0.71/1.11 (223) {G0,W5,D2,L3,V1,M1} I { c2_1( X ), alpha58( X ), ! alpha43 }.
% 0.71/1.11 (354) {G12,W5,D2,L3,V1,M1} R(233,232) { ! c4_1( X ), alpha12, alpha31( X )
% 0.71/1.11 }.
% 0.71/1.11 (116) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), ! c3_2( X, a37 ), alpha75( X
% 0.71/1.11 ), ! c4_2( X, a37 ) }.
% 0.71/1.11 (233) {G0,W5,D2,L3,V1,M1} I { alpha31( X ), ! c4_1( X ), ! alpha20 }.
% 0.71/1.11 (247) {G0,W5,D2,L3,V1,M1} I { alpha21( X ), alpha32( X ), ! alpha13 }.
% 0.71/1.11 (343) {G6,W5,D2,L3,V1,M1} R(82,81) { c4_1( X ), alpha37, alpha63( X ) }.
% 0.71/1.11 (351) {G8,W5,D2,L3,V1,M1} R(104,103) { c4_1( X ), alpha26, alpha52( X ) }.
% 0.71/1.11 (112) {G0,W7,D2,L3,V1,M1} I { ! alpha75( X ), alpha64( X ), c2_2( X, a37 )
% 0.71/1.11 }.
% 0.71/1.11 (111) {G0,W5,D2,L2,V1,M1} I { ! alpha64( X ), ! c2_2( X, a37 ) }.
% 0.71/1.11 (114) {G0,W5,D2,L2,V1,M1} I { ! alpha75( X ), c4_2( X, a37 ) }.
% 0.71/1.11 (115) {G0,W5,D2,L2,V1,M1} I { ! alpha75( X ), c3_2( X, a37 ) }.
% 0.71/1.11 (134) {G0,W5,D2,L2,V1,M1} I { ! alpha83( X ), c3_2( X, a36 ) }.
% 0.71/1.11 (107) {G0,W6,D2,L3,V1,M1} I { c5_1( X ), ! alpha52( X ), alpha64( X ) }.
% 0.71/1.11 (137) {G0,W5,D2,L2,V1,M1} I { ! alpha87( X ), ! c5_2( X, a36 ) }.
% 0.71/1.11 (138) {G0,W5,D2,L2,V1,M1} I { ! alpha87( X ), ! c1_2( X, a36 ) }.
% 0.71/1.11 (214) {G0,W5,D2,L2,V1,M1} I { ! alpha68( X ), ! c1_2( X, a29 ) }.
% 0.71/1.11 (215) {G0,W5,D2,L2,V1,M1} I { ! alpha68( X ), c2_2( X, a29 ) }.
% 0.71/1.11 (104) {G0,W5,D2,L3,V1,M1} I { alpha52( X ), c4_1( X ), ! alpha38 }.
% 0.71/1.11 (227) {G0,W5,D2,L2,V1,M1} I { ! alpha58( X ), ! c5_2( X, a28 ) }.
% 0.71/1.11 (228) {G0,W5,D2,L2,V1,M1} I { ! alpha58( X ), ! c3_2( X, a28 ) }.
% 0.71/1.11 (251) {G0,W5,D2,L2,V1,M1} I { ! alpha32( X ), c4_2( X, a27 ) }.
% 0.71/1.11 (254) {G0,W5,D2,L2,V1,M1} I { ! alpha45( X ), ! c1_2( X, a27 ) }.
% 0.71/1.11 (94) {G0,W10,D2,L4,V1,M1} I { ! ndr1_1( X ), c5_2( X, a38 ), alpha82( X ),
% 0.71/1.11 ! c1_2( X, a38 ) }.
% 0.71/1.11 (255) {G0,W5,D2,L2,V1,M1} I { ! alpha45( X ), ! c5_2( X, a27 ) }.
% 0.71/1.11 (148) {G0,W4,D2,L3,V0,M1} I { c1_1( a34 ), alpha40, ! alpha54 }.
% 0.71/1.11 (151) {G0,W4,D2,L3,V0,M1} I { c2_1( a34 ), alpha54, ! alpha66 }.
% 0.71/1.11 (170) {G0,W4,D2,L3,V0,M1} I { ! c1_1( a31 ), alpha41, ! alpha55 }.
% 0.71/1.11 (93) {G0,W5,D2,L2,V1,M1} I { ! alpha82( X ), c1_2( X, a38 ) }.
% 0.71/1.11 (182) {G0,W4,D2,L3,V0,M1} I { ! ndr1_1( a31 ), alpha85, ! alpha88 }.
% 0.71/1.11 (282) {G2,W4,D2,L3,V0,M1} R(268,7) { c1_0, alpha34, c4_1( a48 ) }.
% 0.71/1.11 (281) {G2,W4,D2,L3,V0,M1} R(268,8) { c1_0, alpha34, ndr1_1( a48 ) }.
% 0.71/1.11 (92) {G0,W5,D2,L2,V1,M1} I { ! alpha82( X ), ! c5_2( X, a38 ) }.
% 0.71/1.11 (320) {G18,W4,D2,L3,V0,M1} R(190,296) { c5_0, alpha28, ndr1_1( a31 ) }.
% 0.71/1.11 (321) {G11,W4,D2,L3,V0,M1} R(169,288) { alpha28, c5_0, c1_1( a31 ) }.
% 0.71/1.11 (153) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a34, a35 ), ! alpha66 }.
% 0.71/1.11 (90) {G0,W7,D2,L3,V1,M1} I { ! alpha82( X ), alpha74( X ), ! c3_2( X, a38 )
% 0.71/1.11 }.
% 0.71/1.11 (156) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a34, a35 ), ! alpha77 }.
% 0.71/1.11 (160) {G0,W4,D2,L2,V0,M1} I { c1_2( a34, a35 ), ! alpha84 }.
% 0.71/1.11 (172) {G0,W4,D2,L2,V0,M1} I { c2_2( a31, a33 ), ! alpha55 }.
% 0.71/1.11 (175) {G0,W4,D2,L2,V0,M1} I { ! c5_2( a31, a33 ), ! alpha67 }.
% 0.71/1.11 (89) {G0,W5,D2,L2,V1,M1} I { ! alpha74( X ), c3_2( X, a38 ) }.
% 0.71/1.11 (178) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a31, a33 ), ! alpha78 }.
% 0.71/1.11 (184) {G0,W4,D2,L2,V0,M1} I { c5_2( a31, a32 ), ! alpha88 }.
% 0.71/1.11 (187) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a31, a32 ), ! alpha90 }.
% 0.71/1.11 (191) {G0,W4,D2,L2,V0,M1} I { c3_2( a31, a32 ), ! alpha92 }.
% 0.71/1.11 (85) {G0,W6,D2,L3,V1,M1} I { ! c5_1( X ), ! alpha63( X ), alpha74( X ) }.
% 0.71/1.11 (286) {G6,W4,D2,L2,V0,M1} R(27,276) { alpha60, ! c2_2( a44, a45 ) }.
% 0.71/1.11 (294) {G7,W4,D2,L2,V0,M1} R(30,277) { alpha60, ! c4_2( a44, a45 ) }.
% 0.71/1.11 (303) {G8,W4,D2,L2,V0,M1} R(34,278) { alpha60, c1_2( a44, a45 ) }.
% 0.71/1.11 (322) {G6,W4,D2,L2,V0,M1} R(50,271) { alpha36, c4_2( a41, a42 ) }.
% 0.71/1.11 (82) {G0,W5,D2,L3,V1,M1} I { alpha63( X ), c4_1( X ), ! alpha51 }.
% 0.71/1.11 (323) {G7,W4,D2,L2,V0,M1} R(53,273) { alpha36, ! c3_2( a41, a42 ) }.
% 0.71/1.11 (327) {G8,W4,D2,L2,V0,M1} R(57,274) { alpha36, c5_2( a41, a42 ) }.
% 0.71/1.11 (342) {G1,W3,D2,L2,V0,M1} R(86,83) { alpha51, c5_1( skol2 ) }.
% 0.71/1.11 (86) {G0,W4,D2,L2,V1,M1} I { c5_1( X ), alpha63( X ) }.
% 0.71/1.11 (87) {G0,W4,D2,L2,V1,M1} I { alpha63( X ), ! alpha74( X ) }.
% 0.71/1.11 (340) {G1,W4,D2,L2,V1,M1} R(88,91) { ndr1_1( X ), ! alpha74( X ) }.
% 0.71/1.11 (88) {G0,W4,D2,L2,V1,M1} I { ! alpha74( X ), alpha82( X ) }.
% 0.71/1.11 (91) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha82( X ) }.
% 0.71/1.11 (77) {G0,W4,D2,L2,V0,M1} I { c1_2( a39, a40 ), ! alpha81 }.
% 0.71/1.11 (339) {G1,W3,D2,L2,V0,M1} R(108,105) { alpha38, ! c5_1( skol3 ) }.
% 0.71/1.11 (108) {G0,W4,D2,L2,V1,M1} I { ! c5_1( X ), alpha52( X ) }.
% 0.71/1.11 (109) {G0,W4,D2,L2,V1,M1} I { alpha52( X ), ! alpha64( X ) }.
% 0.71/1.11 (338) {G1,W4,D2,L2,V1,M1} R(110,113) { ndr1_1( X ), ! alpha64( X ) }.
% 0.71/1.11 (74) {G0,W5,D2,L3,V0,M1} I { ! c2_2( a39, a40 ), alpha73, ! alpha81 }.
% 0.71/1.11 (110) {G0,W4,D2,L2,V1,M1} I { ! alpha64( X ), alpha75( X ) }.
% 0.71/1.11 (113) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha75( X ) }.
% 0.71/1.11 (337) {G2,W3,D2,L2,V0,M1} R(336,124) { alpha53, ndr1_1( skol4 ) }.
% 0.71/1.11 (336) {G1,W4,D2,L2,V1,M1} R(127,132) { ndr1_1( X ), alpha65( X ) }.
% 0.71/1.11 (73) {G0,W4,D2,L2,V0,M1} I { c2_2( a39, a40 ), ! alpha73 }.
% 0.71/1.11 (127) {G0,W4,D2,L2,V1,M1} I { alpha65( X ), ! alpha76( X ) }.
% 0.71/1.11 (131) {G0,W4,D2,L2,V1,M1} I { alpha76( X ), ! alpha83( X ) }.
% 0.71/1.11 (132) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha76( X ) }.
% 0.71/1.11 (335) {G1,W4,D2,L2,V1,M1} R(133,136) { ndr1_1( X ), ! alpha83( X ) }.
% 0.71/1.11 (71) {G0,W4,D2,L3,V0,M1} I { ! c2_1( a39 ), alpha62, ! alpha73 }.
% 0.71/1.11 (133) {G0,W4,D2,L2,V1,M1} I { ! alpha83( X ), alpha87( X ) }.
% 0.71/1.11 (136) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha87( X ) }.
% 0.71/1.11 (334) {G2,W3,D2,L2,V0,M1} R(333,201) { alpha29, ! c3_1( skol6 ) }.
% 0.71/1.11 (333) {G1,W4,D2,L2,V1,M1} R(208,211) { ! c3_1( X ), alpha42( X ) }.
% 0.71/1.11 (68) {G0,W4,D2,L2,V0,M1} I { alpha72, ! c1_2( a39, skol1 ) }.
% 0.71/1.11 (208) {G0,W4,D2,L2,V1,M1} I { alpha42( X ), ! alpha57( X ) }.
% 0.71/1.11 (332) {G1,W3,D2,L2,V0,M1} R(209,201) { alpha29, ndr1_1( skol6 ) }.
% 0.71/1.11 (209) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha42( X ) }.
% 0.71/1.11 (211) {G0,W4,D2,L2,V1,M1} I { ! c3_1( X ), alpha57( X ) }.
% 0.71/1.11 (67) {G0,W4,D2,L2,V0,M1} I { alpha72, c5_2( a39, skol1 ) }.
% 0.71/1.11 (212) {G0,W4,D2,L2,V1,M1} I { alpha57( X ), ! alpha68( X ) }.
% 0.71/1.11 (213) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha68( X ) }.
% 0.71/1.11 (226) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha58( X ) }.
% 0.71/1.11 (331) {G1,W3,D2,L2,V0,M1} R(237,234) { alpha20, ndr1_1( skol9 ) }.
% 0.71/1.11 (65) {G0,W9,D2,L4,V1,M1} I { ! ndr1_1( a39 ), ! c5_2( a39, X ), c1_2( a39,
% 0.71/1.11 X ), ! alpha72 }.
% 0.71/1.11 (237) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha31( X ) }.
% 0.71/1.11 (238) {G0,W4,D2,L2,V1,M1} I { alpha31( X ), ! alpha44( X ) }.
% 0.71/1.11 (330) {G1,W4,D2,L2,V1,M1} R(250,253) { ndr1_1( X ), ! alpha32( X ) }.
% 0.71/1.11 (250) {G0,W4,D2,L2,V1,M1} I { ! alpha32( X ), alpha45( X ) }.
% 0.71/1.11 (253) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), ! alpha45( X ) }.
% 0.71/1.11 (328) {G1,W3,D2,L2,V0,M1} R(258,248) { alpha13, ndr1_1( skol11 ) }.
% 0.71/1.11 (258) {G0,W4,D2,L2,V1,M1} I { ndr1_1( X ), alpha21( X ) }.
% 0.71/1.11 (259) {G0,W4,D2,L2,V1,M1} I { alpha21( X ), ! alpha33( X ) }.
% 0.71/1.11 (57) {G0,W4,D2,L2,V0,M1} I { c5_2( a41, a42 ), ! alpha80 }.
% 0.71/1.11 (326) {G20,W3,D1,L3,V0,M1} R(325,246) { c4_0, c5_0, alpha13 }.
% 0.71/1.11 (325) {G19,W3,D1,L3,V0,M1} S(264);r(297) { c4_0, c5_0, ! alpha7 }.
% 0.71/1.11 (324) {G8,W3,D2,L2,V0,M1} R(56,274) { alpha36, ndr1_1( a41 ) }.
% 0.71/1.11 (54) {G0,W5,D2,L3,V0,M1} I { c3_2( a41, a42 ), alpha71, ! alpha80 }.
% 0.71/1.11 (56) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a41 ), ! alpha80 }.
% 0.71/1.11 (66) {G0,W3,D2,L2,V0,M1} I { alpha72, ndr1_1( a39 ) }.
% 0.71/1.11 (70) {G0,W3,D2,L2,V0,M1} I { c2_1( a39 ), ! alpha62 }.
% 0.71/1.11 (76) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a39 ), ! alpha81 }.
% 0.71/1.11 (53) {G0,W4,D2,L2,V0,M1} I { ! c3_2( a41, a42 ), ! alpha71 }.
% 0.71/1.11 (83) {G0,W3,D2,L2,V0,M1} I { alpha51, ! alpha63( skol2 ) }.
% 0.71/1.11 (84) {G0,W3,D2,L2,V0,M1} I { alpha51, ! c4_1( skol2 ) }.
% 0.71/1.11 (105) {G0,W3,D2,L2,V0,M1} I { alpha38, ! alpha52( skol3 ) }.
% 0.71/1.11 (106) {G0,W3,D2,L2,V0,M1} I { alpha38, ! c4_1( skol3 ) }.
% 0.71/1.11 (51) {G0,W5,D2,L3,V0,M1} I { ! c4_2( a41, a42 ), alpha61, ! alpha71 }.
% 0.71/1.11 (124) {G0,W3,D2,L2,V0,M1} I { alpha53, ! alpha65( skol4 ) }.
% 0.71/1.11 (125) {G0,W3,D2,L2,V0,M1} I { alpha53, ! c5_1( skol4 ) }.
% 0.71/1.11 (147) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a34 ), ! alpha40 }.
% 0.71/1.11 (150) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a34 ), ! alpha54 }.
% 0.71/1.11 (50) {G0,W4,D2,L2,V0,M1} I { c4_2( a41, a42 ), ! alpha61 }.
% 0.71/1.11 (159) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a34 ), ! alpha84 }.
% 0.71/1.11 (169) {G0,W3,D2,L2,V0,M1} I { c1_1( a31 ), ! alpha41 }.
% 0.71/1.11 (181) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a31 ), ! alpha85 }.
% 0.71/1.11 (190) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a31 ), ! alpha92 }.
% 0.71/1.11 (48) {G0,W4,D2,L3,V0,M1} I { c2_1( a41 ), alpha49, ! alpha61 }.
% 0.71/1.11 (194) {G0,W3,D2,L2,V0,M1} I { ! c1_1( a30 ), ! alpha28 }.
% 0.71/1.11 (195) {G0,W3,D2,L2,V0,M1} I { c3_1( a30 ), ! alpha28 }.
% 0.71/1.11 (201) {G0,W3,D2,L2,V0,M1} I { alpha29, ! alpha42( skol6 ) }.
% 0.71/1.11 (319) {G5,W3,D2,L2,V0,M1} R(47,45) { alpha36, ! c2_1( a41 ) }.
% 0.71/1.11 (47) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a41 ), ! alpha49 }.
% 0.71/1.11 (202) {G0,W3,D2,L2,V0,M1} I { alpha29, ! alpha56( skol6 ) }.
% 0.71/1.11 (224) {G0,W3,D2,L2,V0,M1} I { alpha43, ! c2_1( skol8 ) }.
% 0.71/1.11 (225) {G0,W3,D2,L2,V0,M1} I { alpha43, ! alpha58( skol8 ) }.
% 0.71/1.11 (234) {G0,W3,D2,L2,V0,M1} I { alpha20, ! alpha31( skol9 ) }.
% 0.71/1.11 (235) {G0,W3,D2,L2,V0,M1} I { alpha20, c4_1( skol9 ) }.
% 0.71/1.11 (248) {G0,W3,D2,L2,V0,M1} I { alpha13, ! alpha21( skol11 ) }.
% 0.71/1.11 (249) {G0,W3,D2,L2,V0,M1} I { alpha13, ! alpha32( skol11 ) }.
% 0.71/1.11 (272) {G4,W3,D2,L2,V0,M1} R(21,19) { alpha60, c4_1( a44 ) }.
% 0.71/1.11 (41) {G0,W3,D2,L2,V0,M1} I { ! c2_1( a43 ), ! alpha70 }.
% 0.71/1.11 (279) {G5,W3,D2,L2,V0,M1} R(24,270) { alpha60, c3_1( a44 ) }.
% 0.71/1.11 (302) {G8,W3,D2,L2,V0,M1} R(33,278) { alpha60, ndr1_1( a44 ) }.
% 0.71/1.11 (316) {G21,W3,D2,L2,V0,M1} R(314,12) { alpha34, c3_1( a47 ) }.
% 0.71/1.11 (314) {G20,W1,D1,L1,V0,M1} S(313);r(39) { ndr1_0 }.
% 0.71/1.11 (40) {G0,W3,D2,L2,V0,M1} I { ! c5_1( a43 ), ! alpha70 }.
% 0.71/1.11 (36) {G0,W3,D1,L3,V0,M1} I { ! c5_0, alpha70, ! alpha60 }.
% 0.71/1.11 (59) {G0,W3,D1,L3,V0,M1} I { c3_0, alpha50, ! alpha36 }.
% 0.71/1.11 (34) {G0,W4,D2,L2,V0,M1} I { c1_2( a44, a45 ), ! alpha91 }.
% 0.71/1.11 (64) {G0,W3,D1,L3,V0,M1} I { ! alpha62, alpha50, ! alpha72 }.
% 0.71/1.11 (100) {G6,W3,D1,L3,V0,M1} I;r(99) { ! c4_0, c5_0, ! c2_0 }.
% 0.71/1.11 (301) {G1,W2,D1,L2,V0,M1} S(117);r(121) { alpha39, ! alpha26 }.
% 0.71/1.11 (33) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a44 ), ! alpha91 }.
% 0.71/1.11 (143) {G0,W3,D1,L3,V0,M1} I { alpha40, ! c4_0, ! alpha27 }.
% 0.71/1.11 (31) {G0,W5,D2,L3,V0,M1} I { c4_2( a44, a45 ), alpha89, ! alpha91 }.
% 0.71/1.11 (296) {G17,W3,D1,L3,V0,M1} R(295,186) { c5_0, alpha28, alpha92 }.
% 0.71/1.11 (295) {G16,W3,D1,L3,V0,M1} R(293,183) { c5_0, alpha28, alpha90 }.
% 0.71/1.11 (293) {G15,W3,D1,L3,V0,M1} R(292,180) { c5_0, alpha28, alpha88 }.
% 0.71/1.11 (30) {G0,W4,D2,L2,V0,M1} I { ! c4_2( a44, a45 ), ! alpha89 }.
% 0.71/1.11 (292) {G14,W3,D1,L3,V0,M1} R(291,177) { c5_0, alpha28, alpha85 }.
% 0.71/1.11 (291) {G13,W3,D1,L3,V0,M1} R(290,174) { c5_0, alpha28, alpha78 }.
% 0.71/1.11 (290) {G12,W3,D1,L3,V0,M1} R(289,171) { c5_0, alpha28, alpha67 }.
% 0.71/1.11 (289) {G11,W3,D1,L3,V0,M1} R(288,168) { c5_0, alpha28, alpha55 }.
% 0.71/1.11 (28) {G0,W5,D2,L3,V0,M1} I { c2_2( a44, a45 ), alpha86, ! alpha89 }.
% 0.71/1.11 (288) {G10,W3,D1,L3,V0,M1} R(165,164) { alpha28, c5_0, alpha41 }.
% 0.71/1.11 (165) {G0,W3,D1,L3,V0,M1} I { alpha28, alpha41, ! alpha18 }.
% 0.71/1.11 (287) {G1,W2,D1,L2,V0,M1} S(217);r(221) { alpha30, ! alpha19 }.
% 0.71/1.11 (27) {G0,W4,D2,L2,V0,M1} I { ! c2_2( a44, a45 ), ! alpha86 }.
% 0.71/1.11 (285) {G3,W2,D1,L2,V0,M1} S(243);r(283) { c1_0, ! alpha12 }.
% 0.71/1.11 (25) {G0,W4,D2,L3,V0,M1} I { ! c3_1( a44 ), alpha79, ! alpha86 }.
% 0.71/1.11 (268) {G1,W3,D1,L3,V0,M1} R(3,1) { alpha34, c1_0, alpha59 }.
% 0.71/1.11 (278) {G7,W2,D1,L2,V0,M1} R(277,29) { alpha60, alpha91 }.
% 0.71/1.11 (24) {G0,W3,D2,L2,V0,M1} I { c3_1( a44 ), ! alpha79 }.
% 0.71/1.11 (277) {G6,W2,D1,L2,V0,M1} R(26,276) { alpha60, alpha89 }.
% 0.71/1.11 (26) {G0,W2,D1,L2,V0,M1} I { alpha89, ! alpha86 }.
% 0.71/1.11 (29) {G0,W2,D1,L2,V0,M1} I { alpha91, ! alpha89 }.
% 0.71/1.11 (276) {G5,W2,D1,L2,V0,M1} R(23,270) { alpha60, alpha86 }.
% 0.71/1.11 (23) {G0,W2,D1,L2,V0,M1} I { alpha86, ! alpha79 }.
% 0.71/1.11 (37) {G0,W2,D1,L2,V0,M1} I { c5_0, alpha60 }.
% 0.71/1.11 (38) {G0,W2,D1,L2,V0,M1} I { alpha60, ! alpha70 }.
% 0.71/1.11 (22) {G0,W4,D2,L3,V0,M1} I { ! c4_1( a44 ), alpha69, ! alpha79 }.
% 0.71/1.11 (274) {G7,W2,D1,L2,V0,M1} R(273,52) { alpha36, alpha80 }.
% 0.71/1.11 (273) {G6,W2,D1,L2,V0,M1} R(271,49) { alpha36, alpha71 }.
% 0.71/1.11 (271) {G5,W2,D1,L2,V0,M1} R(45,46) { alpha36, alpha61 }.
% 0.71/1.11 (21) {G0,W3,D2,L2,V0,M1} I { c4_1( a44 ), ! alpha69 }.
% 0.71/1.11 (45) {G4,W2,D1,L2,V0,M1} I;r(44) { alpha36, alpha49 }.
% 0.71/1.11 (46) {G0,W2,D1,L2,V0,M1} I { alpha61, ! alpha49 }.
% 0.71/1.11 (49) {G0,W2,D1,L2,V0,M1} I { alpha71, ! alpha61 }.
% 0.71/1.11 (270) {G4,W2,D1,L2,V0,M1} R(20,19) { alpha60, alpha79 }.
% 0.71/1.11 (20) {G0,W2,D1,L2,V0,M1} I { alpha79, ! alpha69 }.
% 0.71/1.11 (52) {G0,W2,D1,L2,V0,M1} I { alpha80, ! alpha71 }.
% 0.71/1.11 (60) {G0,W2,D1,L2,V0,M1} I { alpha36, ! c3_0 }.
% 0.71/1.11 (61) {G0,W2,D1,L2,V0,M1} I { alpha36, ! alpha50 }.
% 0.71/1.11 (19) {G3,W2,D1,L2,V0,M1} I;r(18) { alpha60, alpha69 }.
% 0.71/1.11 (62) {G0,W2,D1,L2,V0,M1} I { alpha62, ! alpha50 }.
% 0.71/1.11 (63) {G0,W2,D1,L2,V0,M1} I { alpha72, ! alpha50 }.
% 0.71/1.11 (69) {G0,W2,D1,L2,V0,M1} I { alpha73, ! alpha62 }.
% 0.71/1.11 (72) {G0,W2,D1,L2,V0,M1} I { alpha81, ! alpha73 }.
% 0.71/1.11 (16) {G2,W3,D2,L2,V0,M1} I;r(14) { ! c3_1( a46 ), ! c2_0 }.
% 0.71/1.11 (81) {G5,W2,D1,L2,V0,M1} I;r(80) { alpha37, alpha51 }.
% 0.71/1.11 (96) {G0,W2,D1,L2,V0,M1} I { c3_0, alpha37 }.
% 0.71/1.11 (103) {G7,W2,D1,L2,V0,M1} I;r(102) { alpha26, alpha38 }.
% 0.71/1.11 (118) {G0,W2,D1,L2,V0,M1} I { alpha26, ! alpha39 }.
% 0.71/1.11 (122) {G0,W2,D1,L2,V0,M1} I { alpha39, ! alpha53 }.
% 0.71/1.11 (142) {G8,W2,D1,L2,V0,M1} I;r(141) { alpha27, ! c1_0 }.
% 0.71/1.11 (144) {G0,W2,D1,L2,V0,M1} I { alpha27, ! alpha40 }.
% 0.71/1.11 (145) {G0,W2,D1,L2,V0,M1} I { c4_0, alpha27 }.
% 0.71/1.11 (11) {G0,W3,D2,L2,V0,M1} I { ! c3_1( a47 ), ! alpha34 }.
% 0.71/1.12 (146) {G0,W2,D1,L2,V0,M1} I { alpha54, ! alpha40 }.
% 0.71/1.12 (149) {G0,W2,D1,L2,V0,M1} I { alpha66, ! alpha54 }.
% 0.71/1.12 (152) {G0,W2,D1,L2,V0,M1} I { alpha77, ! alpha66 }.
% 0.71/1.12 (155) {G0,W2,D1,L2,V0,M1} I { alpha84, ! alpha77 }.
% 0.71/1.12 (164) {G9,W2,D1,L2,V0,M1} I;r(163) { c5_0, alpha18 }.
% 0.71/1.12 (166) {G0,W2,D1,L2,V0,M1} I { alpha18, ! alpha28 }.
% 0.71/1.12 (167) {G0,W2,D1,L2,V0,M1} I { alpha18, ! alpha41 }.
% 0.71/1.12 (168) {G0,W2,D1,L2,V0,M1} I { alpha55, ! alpha41 }.
% 0.71/1.12 (171) {G0,W2,D1,L2,V0,M1} I { alpha67, ! alpha55 }.
% 0.71/1.12 (174) {G0,W2,D1,L2,V0,M1} I { alpha78, ! alpha67 }.
% 0.71/1.12 (177) {G0,W2,D1,L2,V0,M1} I { alpha85, ! alpha78 }.
% 0.71/1.12 (8) {G0,W3,D2,L2,V0,M1} I { ndr1_1( a48 ), ! alpha59 }.
% 0.71/1.12 (180) {G0,W2,D1,L2,V0,M1} I { alpha88, ! alpha85 }.
% 0.71/1.12 (183) {G0,W2,D1,L2,V0,M1} I { alpha90, ! alpha88 }.
% 0.71/1.12 (186) {G0,W2,D1,L2,V0,M1} I { alpha92, ! alpha90 }.
% 0.71/1.12 (7) {G0,W3,D2,L2,V0,M1} I { c4_1( a48 ), ! alpha59 }.
% 0.71/1.12 (199) {G10,W2,D1,L2,V0,M1} I;r(198) { alpha19, alpha29 }.
% 0.71/1.12 (218) {G0,W2,D1,L2,V0,M1} I { alpha19, ! alpha30 }.
% 0.71/1.12 (222) {G0,W2,D1,L2,V0,M1} I { alpha30, ! alpha43 }.
% 0.71/1.12 (232) {G11,W2,D1,L2,V0,M1} I;r(231) { alpha12, alpha20 }.
% 0.71/1.12 (244) {G0,W2,D1,L2,V0,M1} I { alpha12, ! c1_0 }.
% 0.71/1.12 (5) {G0,W5,D2,L3,V0,M1} I { c1_2( a48, a49 ), alpha46, ! alpha59 }.
% 0.71/1.12 (246) {G11,W2,D1,L2,V0,M1} I;r(230) { alpha13, alpha7 }.
% 0.71/1.12 (265) {G0,W2,D1,L2,V0,M1} I { alpha7, ! c4_0 }.
% 0.71/1.12 (266) {G0,W2,D1,L2,V0,M1} I { alpha7, ! c5_0 }.
% 0.71/1.12 (4) {G0,W4,D2,L2,V0,M1} I { ! c1_2( a48, a49 ), ! alpha46 }.
% 0.71/1.12 (13) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha35 }.
% 0.71/1.12 (14) {G1,W1,D1,L1,V0,M1} I;r(0) { alpha47 }.
% 0.71/1.12 (17) {G2,W1,D1,L1,V0,M1} I;r(13) { alpha14 }.
% 0.71/1.12 (3) {G0,W2,D1,L2,V0,M1} I { alpha59, ! alpha46 }.
% 0.71/1.12 (18) {G2,W1,D1,L1,V0,M1} I;r(13) { alpha48 }.
% 0.71/1.12 (43) {G3,W1,D1,L1,V0,M1} I;r(17) { alpha8 }.
% 0.71/1.12 (44) {G3,W1,D1,L1,V0,M1} I;r(17) { alpha23 }.
% 0.71/1.12 (79) {G4,W1,D1,L1,V0,M1} I;r(43) { alpha15 }.
% 0.71/1.12 (2) {G0,W5,D2,L3,V0,M1} I { alpha34, c1_0, ! c5_2( a48, a49 ) }.
% 0.71/1.12 (80) {G4,W1,D1,L1,V0,M1} I;r(43) { alpha24 }.
% 0.71/1.12 (98) {G5,W1,D1,L1,V0,M1} I;r(79) { alpha4 }.
% 0.71/1.12 (99) {G5,W1,D1,L1,V0,M1} I;r(79) { alpha25 }.
% 0.71/1.12 (101) {G6,W1,D1,L1,V0,M1} I;r(98) { alpha9 }.
% 0.71/1.12 (1) {G0,W3,D1,L3,V0,M1} I { alpha34, c1_0, alpha46 }.
% 0.71/1.12 (102) {G6,W1,D1,L1,V0,M1} I;r(98) { alpha16 }.
% 0.71/1.12 (140) {G7,W1,D1,L1,V0,M1} I;r(101) { alpha2 }.
% 0.71/1.12 (141) {G7,W1,D1,L1,V0,M1} I;r(101) { alpha17 }.
% 0.71/1.12 (162) {G8,W1,D1,L1,V0,M1} I;r(140) { alpha5 }.
% 0.71/1.12 (0) {G0,W1,D1,L1,V0,M1} I { alpha22 }.
% 0.71/1.12 (163) {G8,W1,D1,L1,V0,M1} I;r(140) { alpha10 }.
% 0.71/1.12 (197) {G9,W1,D1,L1,V0,M1} I;r(162) { alpha1 }.
% 0.71/1.12 (198) {G9,W1,D1,L1,V0,M1} I;r(162) { alpha11 }.
% 0.71/1.12 (230) {G10,W1,D1,L1,V0,M1} I;r(197) { alpha3 }.
% 0.71/1.12 (231) {G10,W1,D1,L1,V0,M1} I;r(197) { alpha6 }.
% 0.71/1.12
% 0.71/1.12
% 0.71/1.12 % SZS output end Saturation
% 0.71/1.12 end of saturation!
% 0.71/1.12
% 0.71/1.12 Memory use:
% 0.71/1.12
% 0.71/1.12 space for terms: 4897
% 0.71/1.12 space for clauses: 18130
% 0.71/1.12
% 0.71/1.12
% 0.71/1.12 clauses generated: 506
% 0.71/1.12 clauses kept: 386
% 0.71/1.12 clauses selected: 368
% 0.71/1.12 clauses deleted: 51
% 0.71/1.12 clauses inuse deleted: 33
% 0.71/1.12
% 0.71/1.12 subsentry: 137
% 0.71/1.12 literals s-matched: 117
% 0.71/1.12 literals matched: 117
% 0.71/1.12 full subsumption: 0
% 0.71/1.12
% 0.71/1.12 checksum: -2144042719
% 0.71/1.12
% 0.71/1.12
% 0.71/1.12 Bliksem ended
%------------------------------------------------------------------------------