Paradox---4.0.SAT-FMo.s

%------------------------------------------------------------------------------
% File     : Paradox---4.0
% Problem  : SYN868-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm  : none
% Format   : tptp:short
% Command  : paradox --no-progress --time %d --tstp --model %s

% Computer : n005.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Thu Jul 21 11:06:20 EDT 2022

% Result   : Satisfiable 0.41s 0.62s
% Output   : FiniteModel 0.41s
% Verified : 
% SZS Type : FiniteModel
%            Domain size           :    2

% Comments : 
%------------------------------------------------------------------------------
% domain size is 2
fof(domain,fi_domain,
    ! [X] :
      ( X = "1"
      | X = "2" ) ).

fof(skc18,fi_functors,
    skc18 = "1" ).

fof(skc19,fi_functors,
    skc19 = "2" ).

fof(skc20,fi_functors,
    skc20 = "1" ).

fof(skc21,fi_functors,
    skc21 = "2" ).

fof(skc22,fi_functors,
    skc22 = "1" ).

fof(skc23,fi_functors,
    skc23 = "2" ).

fof(skc24,fi_functors,
    skc24 = "1" ).

fof(skc25,fi_functors,
    skc25 = "2" ).

fof(skc26,fi_functors,
    skc26 = "1" ).

fof(skc27,fi_functors,
    skc27 = "2" ).

fof(skc28,fi_functors,
    skc28 = "1" ).

fof(skc29,fi_functors,
    skc29 = "2" ).

fof(skc30,fi_functors,
    skc30 = "1" ).

fof(skc31,fi_functors,
    skc31 = "2" ).

fof(skc32,fi_functors,
    skc32 = "1" ).

fof(skc33,fi_functors,
    skc33 = "2" ).

fof(skc34,fi_functors,
    skc34 = "1" ).

fof(skc35,fi_functors,
    skc35 = "2" ).

fof(ssNder1_0,fi_predicates,
    ( ssNder1_0
  <=> $true ) ).

fof(ssNder1_10r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_10r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10)
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
        ( ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2")
      <=> ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1") ) ) ).

fof(ssNder1_11r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11)
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
        ( ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2")
      <=> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1") ) ) ).

fof(ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12)
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
        ( ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2")
      <=> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1") ) ) ).

fof(ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13)
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
        ( ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2")
      <=> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1") ) ) ).

fof(ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14)
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2")
      <=> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1") ) ) ).

fof(ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15)
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2")
      <=> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1") ) ) ).

fof(ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16)
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2")
      <=> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1") ) ) ).

fof(ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17)
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2")
      <=> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1") ) ) ).

fof(ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18)
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
        ( ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2")
      <=> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1") ) ) ).

fof(ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19)
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
        ( ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2")
      <=> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1") ) ) ).

fof(ssNder1_1r1,fi_predicates,
    ( ( ssNder1_1r1("1")
    <=> $true )
    & ( ssNder1_1r1("2")
    <=> ssNder1_1r1("1") ) ) ).

fof(ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19,X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19,X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X20] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2",X20)
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1",X20) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
        ( ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"2")
      <=> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"1") ) ) ).

fof(ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19,X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19,X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X20,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2",X20,X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1",X20,X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X21] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"2",X21)
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"1",X21) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
        ( ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"2")
      <=> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"1") ) ) ).

fof(ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19,X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X20,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2",X20,X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1",X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X21,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"2",X21,X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"1",X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X22] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"2",X22)
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"1",X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
        ( ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,"2")
      <=> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,"1") ) ) ).

fof(ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23] :
      ( ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23)
    <=> $true ) ).

fof(ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
      ( ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
    <=> $true ) ).

fof(ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25] :
      ( ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)
    <=> $true ) ).

fof(ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26] :
      ( ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26)
    <=> $true ) ).

fof(ssNder1_2r1r1,fi_predicates,
    ( ( ssNder1_2r1r1("1","1")
    <=> $true )
    & ! [X2] :
        ( ssNder1_2r1r1("2",X2)
      <=> ssNder1_2r1r1("1",X2) )
    & ! [X1] :
        ( ssNder1_2r1r1(X1,"2")
      <=> ssNder1_2r1r1(X1,"1") ) ) ).

fof(ssNder1_3r1r1r1,fi_predicates,
    ( ( ssNder1_3r1r1r1("1","1","1")
    <=> $true )
    & ! [X2,X3] :
        ( ssNder1_3r1r1r1("2",X2,X3)
      <=> ssNder1_3r1r1r1("1",X2,X3) )
    & ! [X1,X3] :
        ( ssNder1_3r1r1r1(X1,"2",X3)
      <=> ssNder1_3r1r1r1(X1,"1",X3) )
    & ! [X1,X2] :
        ( ssNder1_3r1r1r1(X1,X2,"2")
      <=> ssNder1_3r1r1r1(X1,X2,"1") ) ) ).

fof(ssNder1_4r1r1r1r1,fi_predicates,
    ( ( ssNder1_4r1r1r1r1("1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4] :
        ( ssNder1_4r1r1r1r1("2",X2,X3,X4)
      <=> ssNder1_4r1r1r1r1("1",X2,X3,X4) )
    & ! [X1,X3,X4] :
        ( ssNder1_4r1r1r1r1(X1,"2",X3,X4)
      <=> ssNder1_4r1r1r1r1(X1,"1",X3,X4) )
    & ! [X1,X2,X4] :
        ( ssNder1_4r1r1r1r1(X1,X2,"2",X4)
      <=> ssNder1_4r1r1r1r1(X1,X2,"1",X4) )
    & ! [X1,X2,X3] :
        ( ssNder1_4r1r1r1r1(X1,X2,X3,"2")
      <=> ssNder1_4r1r1r1r1(X1,X2,X3,"1") ) ) ).

fof(ssNder1_5r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_5r1r1r1r1r1("1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5] :
        ( ssNder1_5r1r1r1r1r1("2",X2,X3,X4,X5)
      <=> ssNder1_5r1r1r1r1r1("1",X2,X3,X4,X5) )
    & ! [X1,X3,X4,X5] :
        ( ssNder1_5r1r1r1r1r1(X1,"2",X3,X4,X5)
      <=> ssNder1_5r1r1r1r1r1(X1,"1",X3,X4,X5) )
    & ! [X1,X2,X4,X5] :
        ( ssNder1_5r1r1r1r1r1(X1,X2,"2",X4,X5)
      <=> ssNder1_5r1r1r1r1r1(X1,X2,"1",X4,X5) )
    & ! [X1,X2,X3,X5] :
        ( ssNder1_5r1r1r1r1r1(X1,X2,X3,"2",X5)
      <=> ssNder1_5r1r1r1r1r1(X1,X2,X3,"1",X5) )
    & ! [X1,X2,X3,X4] :
        ( ssNder1_5r1r1r1r1r1(X1,X2,X3,X4,"2")
      <=> ssNder1_5r1r1r1r1r1(X1,X2,X3,X4,"1") ) ) ).

fof(ssNder1_6r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_6r1r1r1r1r1r1("1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6] :
        ( ssNder1_6r1r1r1r1r1r1("2",X2,X3,X4,X5,X6)
      <=> ssNder1_6r1r1r1r1r1r1("1",X2,X3,X4,X5,X6) )
    & ! [X1,X3,X4,X5,X6] :
        ( ssNder1_6r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6)
      <=> ssNder1_6r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6) )
    & ! [X1,X2,X4,X5,X6] :
        ( ssNder1_6r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6)
      <=> ssNder1_6r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6) )
    & ! [X1,X2,X3,X5,X6] :
        ( ssNder1_6r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6)
      <=> ssNder1_6r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6) )
    & ! [X1,X2,X3,X4,X6] :
        ( ssNder1_6r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6)
      <=> ssNder1_6r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6) )
    & ! [X1,X2,X3,X4,X5] :
        ( ssNder1_6r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2")
      <=> ssNder1_6r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1") ) ) ).

fof(ssNder1_7r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_7r1r1r1r1r1r1r1("1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7)
      <=> ssNder1_7r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7) )
    & ! [X1,X3,X4,X5,X6,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7)
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7) )
    & ! [X1,X2,X4,X5,X6,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7)
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7) )
    & ! [X1,X2,X3,X5,X6,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7)
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7) )
    & ! [X1,X2,X3,X4,X6,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7)
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7) )
    & ! [X1,X2,X3,X4,X5,X7] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7)
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7) )
    & ! [X1,X2,X3,X4,X5,X6] :
        ( ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2")
      <=> ssNder1_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1") ) ) ).

fof(ssNder1_8r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_8r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8) )
    & ! [X1,X3,X4,X5,X6,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8) )
    & ! [X1,X2,X4,X5,X6,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8) )
    & ! [X1,X2,X3,X5,X6,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8) )
    & ! [X1,X2,X3,X4,X6,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8) )
    & ! [X1,X2,X3,X4,X5,X7,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8) )
    & ! [X1,X2,X3,X4,X5,X6,X8] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8)
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8) )
    & ! [X1,X2,X3,X4,X5,X6,X7] :
        ( ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2")
      <=> ssNder1_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1") ) ) ).

fof(ssNder1_9r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssNder1_9r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9)
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8] :
        ( ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2")
      <=> ssNder1_9r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1") ) ) ).

fof(ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    <=> $true ) ).

fof(ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    <=> $true ) ).

fof(ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16] :
        ( ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16)
      <=> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16) ) ) ).

fof(ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15] :
        ( ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15)
      <=> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15) ) ) ).

fof(ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14] :
        ( ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14)
      <=> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14) ) ) ).

fof(ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13] :
        ( ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13)
      <=> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13) ) ) ).

fof(ssPv18_11r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
      ( ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
    <=> $false ) ).

fof(ssPv19_10r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
      ( ssPv19_10r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
    <=> $false ) ).

fof(ssPv21_8r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv21_8r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv21_8r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8) )
    & ! [X1,X3,X4,X5,X6,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8) )
    & ! [X1,X2,X4,X5,X6,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8) )
    & ! [X1,X2,X3,X5,X6,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8) )
    & ! [X1,X2,X3,X4,X6,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8) )
    & ! [X1,X2,X3,X4,X5,X7,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8) )
    & ! [X1,X2,X3,X4,X5,X6,X8] :
        ( ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8)
      <=> ssPv21_8r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8) ) ) ).

fof(ssPv22_7r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv22_7r1r1r1r1r1r1r1("1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv22_7r1r1r1r1r1r1r1("1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7)
      <=> ssPv22_7r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7) )
    & ! [X1,X3,X4,X5,X6,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7)
      <=> ssPv22_7r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7) )
    & ! [X1,X2,X4,X5,X6,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7)
      <=> ssPv22_7r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7) )
    & ! [X1,X2,X3,X5,X6,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7)
      <=> ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7) )
    & ! [X1,X2,X3,X4,X6,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7)
      <=> ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7) )
    & ! [X1,X2,X3,X4,X5,X7] :
        ( ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7)
      <=> ssPv22_7r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7) ) ) ).

fof(ssPv24_5r1r1r1r1r1,fi_predicates,
    ( ( ssPv24_5r1r1r1r1r1("1","1","1","1","1")
    <=> $true )
    & ( ssPv24_5r1r1r1r1r1("1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5] :
        ( ssPv24_5r1r1r1r1r1("2",X2,X3,X4,X5)
      <=> ssPv24_5r1r1r1r1r1("1",X2,X3,X4,X5) )
    & ! [X1,X3,X4,X5] :
        ( ssPv24_5r1r1r1r1r1(X1,"2",X3,X4,X5)
      <=> ssPv24_5r1r1r1r1r1(X1,"1",X3,X4,X5) )
    & ! [X1,X2,X4,X5] :
        ( ssPv24_5r1r1r1r1r1(X1,X2,"2",X4,X5)
      <=> ssPv24_5r1r1r1r1r1(X1,X2,"1",X4,X5) )
    & ! [X1,X2,X3,X5] :
        ( ssPv24_5r1r1r1r1r1(X1,X2,X3,"2",X5)
      <=> ssPv24_5r1r1r1r1r1(X1,X2,X3,"1",X5) ) ) ).

fof(ssPv25_4r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4] :
      ( ssPv25_4r1r1r1r1(X1,X2,X3,X4)
    <=> $false ) ).

fof(ssPv26_3r1r1r1,fi_predicates,
    ! [X1,X2,X3] :
      ( ssPv26_3r1r1r1(X1,X2,X3)
    <=> $false ) ).

fof(ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27] :
      ( ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27)
    <=> $true ) ).

fof(ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26] :
      ( ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26)
    <=> $true ) ).

fof(ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25] :
      ( ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)
    <=> $false ) ).

fof(ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19,X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19,X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X20,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2",X20,X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1",X20,X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X21,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"2",X21,X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"1",X21,X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X22,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"2",X22,X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"1",X22,X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X23,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,"2",X23,X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,"1",X23,X24) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X24] :
        ( ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,"2",X24)
      <=> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,"1",X24) ) ) ).

fof(ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ( ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1")
    <=> $true )
    & ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","1","2")
    <=> $false )
    & ! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("2",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1("1",X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"2",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,"1",X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"2",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,"1",X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"2",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,"1",X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"2",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,"1",X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"2",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,"1",X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"2",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,"1",X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"2",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,"1",X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"2",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,"1",X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"2",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,"1",X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"2",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,"1",X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"2",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,"1",X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X14,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"2",X14,X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,"1",X14,X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"2",X15,X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,"1",X15,X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X16,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"2",X16,X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,"1",X16,X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X17,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"2",X17,X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,"1",X17,X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X18,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"2",X18,X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,"1",X18,X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"2",X19,X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,"1",X19,X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X20,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"2",X20,X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,"1",X20,X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X21,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"2",X21,X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,"1",X21,X22) )
    & ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X22] :
        ( ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"2",X22)
      <=> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,"1",X22) ) ) ).

fof(ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1,fi_predicates,
    ! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20] :
      ( ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
    <=> $false ) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYN868-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.13  % Command  : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.34  % Computer : n005.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Tue Jul 12 04:12:51 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  Paradox, version 4.0, 2010-06-29.
% 0.13/0.34  +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34  Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK
% 0.20/0.47  +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.60  +++ BEGIN MODEL
% 0.41/0.60  SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.41/0.62  +++ END MODEL
% 0.41/0.62  +++ RESULT: Satisfiable
% 0.41/0.62  SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------