%--------------------------------------------------------------------------
% Syntax   : Number of clauses    : 3104 ( 108 non-Horn;   1 unit; 1593 RR)
%            Number of literals   : 121400 (   0 equality)
%            Maximal clause size  :   60 (  39 average)
%            Number of predicates : 1742 (   1 propositional; 0-56 arity)
%            Number of functors   :   48 (  48 constant; 0-0 arity)
%            Number of variables  : 114976 (2943 singleton)
%            Maximal term depth   :    1 (   1 average)
%--------------------------------------------------------------------------
input_clause(clause1,conjecture,
    [++ssNder1_0]).

input_clause(clause2,conjecture,
    [--ssNder1_0,
     ++ssNder1_1r1(U)]).

input_clause(clause3,conjecture,
    [--ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_2r1r1(U,V)]).

input_clause(clause4,conjecture,
    [--ssPv56_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause5,conjecture,
    [--ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_2r1r1(U,V)]).

input_clause(clause6,conjecture,
    [--ssPv56_1r1(U),
     --ssNder1_0,
     ++ssPv15_1r1(U),
     ++ssPv31_1r1(U),
     ++ssPv53_1r1(U)]).

input_clause(clause7,conjecture,
    [--ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_3r1r1r1(U,V,W)]).

input_clause(clause8,conjecture,
    [--ssPv13_1r1(U),
     --ssPv16_1r1(U),
     --ssPv56_1r1(U),
     --ssNder1_0,
     ++ssPv55_1r1(U)]).

input_clause(clause9,conjecture,
    [--ssPv56_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause10,conjecture,
    [--ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_3r1r1r1(U,V,W)]).

input_clause(clause11,conjecture,
    [--ssPv55_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause12,conjecture,
    [--ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_3r1r1r1(U,V,W)]).

input_clause(clause13,conjecture,
    [--ssPv15_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_2r1r1(U,V),
     ++ssPv53_2r1r1(U,V),
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause14,conjecture,
    [--ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_4r1r1r1r1(U,V,W,X)]).

input_clause(clause15,conjecture,
    [--ssPv1_2r1r1(U,V),
     --ssPv55_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv25_2r1r1(U,V),
     ++ssPv29_2r1r1(U,V)]).

input_clause(clause16,conjecture,
    [--ssPv25_2r1r1(U,V),
     --ssPv45_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv5_2r1r1(U,V),
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause17,conjecture,
    [--ssPv13_2r1r1(U,V),
     --ssPv16_2r1r1(U,V),
     --ssPv56_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause18,conjecture,
    [--ssPv12_2r1r1(U,V),
     --ssPv24_2r1r1(U,V),
     --ssPv29_2r1r1(U,V),
     --ssPv55_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause19,conjecture,
    [--ssPv56_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause20,conjecture,
    [--ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_4r1r1r1r1(U,V,W,X)]).

input_clause(clause21,conjecture,
    [--ssPv55_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause22,conjecture,
    [--ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_4r1r1r1r1(U,V,W,X)]).

input_clause(clause23,conjecture,
    [--ssPv54_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause24,conjecture,
    [--ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_4r1r1r1r1(U,V,W,X)]).

input_clause(clause25,conjecture,
    [--ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause26,conjecture,
    [--ssPv23_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv29_3r1r1r1(U,V,W),
     ++ssPv32_3r1r1r1(U,V,W),
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause27,conjecture,
    [--ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause28,conjecture,
    [--ssPv56_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause29,conjecture,
    [--ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause30,conjecture,
    [--ssPv55_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause31,conjecture,
    [--ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause32,conjecture,
    [--ssPv54_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause33,conjecture,
    [--ssPv53_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause34,conjecture,
    [--ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause35,conjecture,
    [--ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv10_4r1r1r1r1(U,V,W,X),
     ++ssPv14_4r1r1r1r1(U,V,W,X),
     ++ssPv22_4r1r1r1r1(U,V,W,X),
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause36,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause37,conjecture,
    [--ssPv56_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv15_4r1r1r1r1(U,V,W,X),
     ++ssPv31_4r1r1r1r1(U,V,W,X),
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause38,conjecture,
    [--ssPv15_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_4r1r1r1r1(U,V,W,X),
     ++ssPv53_4r1r1r1r1(U,V,W,X),
     ++ssPv55_4r1r1r1r1(U,V,W,X)]).

input_clause(clause39,conjecture,
    [--ssPv9_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv7_4r1r1r1r1(U,V,W,X),
     ++ssPv14_4r1r1r1r1(U,V,W,X),
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause40,conjecture,
    [--ssPv10_4r1r1r1r1(U,V,W,X),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv17_4r1r1r1r1(U,V,W,X),
     ++ssPv45_4r1r1r1r1(U,V,W,X)]).

input_clause(clause41,conjecture,
    [--ssPv56_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause42,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause43,conjecture,
    [--ssPv14_4r1r1r1r1(U,V,W,X),
     --ssPv21_4r1r1r1r1(U,V,W,X),
     --ssPv31_4r1r1r1r1(U,V,W,X),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause44,conjecture,
    [--ssPv55_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause45,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause46,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause47,conjecture,
    [--ssPv54_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause48,conjecture,
    [--ssPv53_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause49,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause50,conjecture,
    [--ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause51,conjecture,
    [--ssPv52_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause52,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause53,conjecture,
    [--ssPv36_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv32_5r1r1r1r1r1(U,V,W,X,Y),
     ++ssPv42_5r1r1r1r1r1(U,V,W,X,Y),
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause54,conjecture,
    [--ssPv56_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause55,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause56,conjecture,
    [--ssPv55_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause57,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause58,conjecture,
    [--ssPv54_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause59,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause60,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause61,conjecture,
    [--ssPv53_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause62,conjecture,
    [--ssPv52_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause63,conjecture,
    [--ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause64,conjecture,
    [--ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1)]).

input_clause(clause65,conjecture,
    [--ssPv51_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause66,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause67,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,skc94)]).

input_clause(clause68,conjecture,
    [--ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,skc95),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause69,conjecture,
    [--ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv4_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     ++ssPv12_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     ++ssPv14_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause70,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause71,conjecture,
    [--ssPv56_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause72,conjecture,
    [--ssPv5_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv25_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     ++ssPv47_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause73,conjecture,
    [--ssPv55_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause74,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause75,conjecture,
    [--ssPv24_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv46_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv30_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause76,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause77,conjecture,
    [--ssPv5_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv43_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv46_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause78,conjecture,
    [--ssPv54_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause79,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause80,conjecture,
    [--ssPv53_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause81,conjecture,
    [--ssPv52_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause82,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause83,conjecture,
    [--ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause84,conjecture,
    [--ssPv51_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause85,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause86,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,skc92)]).

input_clause(clause87,conjecture,
    [--ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,skc93),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause88,conjecture,
    [--ssPv56_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause89,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause90,conjecture,
    [--ssPv55_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause91,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause92,conjecture,
    [--ssPv54_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause93,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause94,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause95,conjecture,
    [--ssPv53_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause96,conjecture,
    [--ssPv52_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause97,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause98,conjecture,
    [--ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause99,conjecture,
    [--ssPv51_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause100,conjecture,
    [--ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause101,conjecture,
    [--ssPv49_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause102,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause103,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,skc90)]).

input_clause(clause104,conjecture,
    [--ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,skc91),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause105,conjecture,
    [--ssPv56_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause106,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause107,conjecture,
    [--ssPv55_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause108,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause109,conjecture,
    [--ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv26_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     ++ssPv38_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     ++ssPv41_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause110,conjecture,
    [--ssPv54_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause111,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause112,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause113,conjecture,
    [--ssPv53_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause114,conjecture,
    [--ssPv5_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssPv29_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv44_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause115,conjecture,
    [--ssPv13_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssPv48_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv37_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause116,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause117,conjecture,
    [--ssPv52_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause118,conjecture,
    [--ssPv17_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssPv45_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv41_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause119,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause120,conjecture,
    [--ssPv51_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause121,conjecture,
    [--ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause122,conjecture,
    [--ssPv49_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause123,conjecture,
    [--ssPv48_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause124,conjecture,
    [--ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause125,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause126,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,skc88)]).

input_clause(clause127,conjecture,
    [--ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,skc89),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause128,conjecture,
    [--ssPv56_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause129,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause130,conjecture,
    [--ssPv55_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause131,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause132,conjecture,
    [--ssPv54_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause133,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause134,conjecture,
    [--ssPv8_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv13_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     ++ssPv17_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause135,conjecture,
    [--ssPv37_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv7_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     ++ssPv46_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause136,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause137,conjecture,
    [--ssPv53_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause138,conjecture,
    [--ssPv30_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv20_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     ++ssPv34_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause139,conjecture,
    [--ssPv52_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause140,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause141,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause142,conjecture,
    [--ssPv51_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause143,conjecture,
    [--ssPv13_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv37_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause144,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause145,conjecture,
    [--ssPv49_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause146,conjecture,
    [--ssPv48_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause147,conjecture,
    [--ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause148,conjecture,
    [--ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause149,conjecture,
    [--ssPv47_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause150,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause151,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,skc86)]).

input_clause(clause152,conjecture,
    [--ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,skc87),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause153,conjecture,
    [--ssPv56_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause154,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause155,conjecture,
    [--ssPv55_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause156,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause157,conjecture,
    [--ssPv54_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause158,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause159,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause160,conjecture,
    [--ssPv53_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause161,conjecture,
    [--ssPv52_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause162,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause163,conjecture,
    [--ssPv51_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause164,conjecture,
    [--ssPv5_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssPv51_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv25_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause165,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause166,conjecture,
    [--ssPv49_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause167,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause168,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause169,conjecture,
    [--ssPv48_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause170,conjecture,
    [--ssPv47_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause171,conjecture,
    [--ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause172,conjecture,
    [--ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause173,conjecture,
    [--ssPv46_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause174,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause175,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,skc84)]).

input_clause(clause176,conjecture,
    [--ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,skc85),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause177,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause178,conjecture,
    [--ssPv56_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause179,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause180,conjecture,
    [--ssPv55_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause181,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause182,conjecture,
    [--ssPv54_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause183,conjecture,
    [--ssPv53_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause184,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause185,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause186,conjecture,
    [--ssPv52_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause187,conjecture,
    [--ssPv37_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv7_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     ++ssPv48_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause188,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause189,conjecture,
    [--ssPv51_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause190,conjecture,
    [--ssPv15_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     ++ssPv53_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     ++ssPv55_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause191,conjecture,
    [--ssPv24_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     ++ssPv51_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause192,conjecture,
    [--ssPv5_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv43_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause193,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause194,conjecture,
    [--ssPv49_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause195,conjecture,
    [--ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv34_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv17_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause196,conjecture,
    [--ssPv48_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause197,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause198,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause199,conjecture,
    [--ssPv47_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause200,conjecture,
    [--ssPv46_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause201,conjecture,
    [--ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause202,conjecture,
    [--ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv45_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause203,conjecture,
    [--ssPv45_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause204,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause205,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,skc82)]).

input_clause(clause206,conjecture,
    [--ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,skc83),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause207,conjecture,
    [--ssPv56_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause208,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause209,conjecture,
    [--ssPv55_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause210,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause211,conjecture,
    [--ssPv54_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause212,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause213,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause214,conjecture,
    [--ssPv53_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause215,conjecture,
    [--ssPv52_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_5r1r1r1r1r1(U,V,W,X,Y)]).

input_clause(clause216,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause217,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause218,conjecture,
    [--ssPv51_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv51_6r1r1r1r1r1r1(U,V,W,X,Y,Z)]).

input_clause(clause219,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause220,conjecture,
    [--ssPv49_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv49_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2)]).

input_clause(clause221,conjecture,
    [--ssPv10_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv53_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     ++ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause222,conjecture,
    [--ssPv25_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv5_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     ++ssPv55_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause223,conjecture,
    [--ssPv48_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3)]).

input_clause(clause224,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssPv48_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv48_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause225,conjecture,
    [--ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv49_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv41_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause226,conjecture,
    [--ssPv47_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4)]).

input_clause(clause227,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssPv47_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv47_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause228,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause229,conjecture,
    [--ssPv46_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5)]).

input_clause(clause230,conjecture,
    [--ssPv45_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6)]).

input_clause(clause231,conjecture,
    [--ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv45_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause232,conjecture,
    [--ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv44_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8)]).

input_clause(clause233,conjecture,
    [--ssPv44_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7)]).

input_clause(clause234,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause235,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,skc80)]).

input_clause(clause236,conjecture,
    [--ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,skc81),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0]).

input_clause(clause237,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssPv56_1r1(U),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause238,conjecture,
    [--ssPv56_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv56_1r1(U)]).

input_clause(clause239,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssPv55_2r1r1(U,V),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause240,conjecture,
    [--ssPv55_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv55_2r1r1(U,V)]).

input_clause(clause241,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssPv54_3r1r1r1(U,V,W),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause242,conjecture,
    [--ssPv54_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv54_3r1r1r1(U,V,W)]).

input_clause(clause243,conjecture,
    [--ssPv53_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_4r1r1r1r1(U,V,W,X)]).

input_clause(clause244,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssPv53_4r1r1r1r1(U,V,W,X),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv53_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause245,conjecture,
    [--ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6),
     --ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5),
     --ssNder1_10r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4),
     --ssNder1_9r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3),
     --ssNder1_8r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2),
     --ssNder1_7r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1),
     --ssNder1_6r1r1r1r1r1r1(U,V,W,X,Y,Z),
     --ssPv52_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_5r1r1r1r1r1(U,V,W,X,Y),
     --ssNder1_4r1r1r1r1(U,V,W,X),
     --ssNder1_3r1r1r1(U,V,W),
     --ssNder1_2r1r1(U,V),
     --ssNder1_1r1(U),
     --ssNder1_0,
     ++ssPv52_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9)]).

input_clause(clause246,conjecture,
    [--ssPv52_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9),
     --ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8),
     --ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7),
     --ss