Vampire-SAT---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 11:48:35 AM UTC 2026

% Result   : Theorem 17.04s 7.66s
% Output   : Refutation 17.04s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   88
%            Number of leaves      :   17
% Syntax   : Number of formulae    :  244 (  49 unt;   7 def)
%            Number of atoms       : 1970 (  38 equ)
%            Maximal formula atoms :   27 (   8 avg)
%            Number of connectives : 3161 (1435   ~;1518   |; 172   &)
%                                         (  10 <=>;  26  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   29 (   9 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of predicates  :   23 (  21 usr;   1 prp; 0-3 aty)
%            Number of functors    :   19 (  19 usr;  11 con; 0-4 aty)
%            Number of variables   :  223 ( 212   !;  11   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,conjecture,
    ! [X0] :
      ( ( v2_orders_2(X0)
        & v3_orders_2(X0)
        & v4_orders_2(X0)
        & v1_lattice3(X0)
        & v2_lattice3(X0)
        & v3_lattice3(X0)
        & l1_orders_2(X0) )
     => ! [X1] :
          ( ( v2_orders_2(X1)
            & v3_orders_2(X1)
            & v4_orders_2(X1)
            & v1_lattice3(X1)
            & v2_lattice3(X1)
            & v3_lattice3(X1)
            & l1_orders_2(X1) )
         => ! [X2] :
              ( ( v1_funct_1(X2)
                & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
                & v18_waybel_0(X2,X1,X0)
                & m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
             => ! [X3] :
                  ( m1_subset_1(X3,u1_struct_0(X0))
                 => k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) = k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3))) ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_waybel34) ).

fof(f2,negated_conjecture,
    ~ ! [X0] :
        ( ( v2_orders_2(X0)
          & v3_orders_2(X0)
          & v4_orders_2(X0)
          & v1_lattice3(X0)
          & v2_lattice3(X0)
          & v3_lattice3(X0)
          & l1_orders_2(X0) )
       => ! [X1] :
            ( ( v2_orders_2(X1)
              & v3_orders_2(X1)
              & v4_orders_2(X1)
              & v1_lattice3(X1)
              & v2_lattice3(X1)
              & v3_lattice3(X1)
              & l1_orders_2(X1) )
           => ! [X2] :
                ( ( v1_funct_1(X2)
                  & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
                  & v18_waybel_0(X2,X1,X0)
                  & m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
               => ! [X3] :
                    ( m1_subset_1(X3,u1_struct_0(X0))
                   => k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) = k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3))) ) ) ) ),
    inference(negated_conjecture,[status(cth)],[f1]) ).

fof(f21,axiom,
    ! [X0] :
      ( l1_orders_2(X0)
     => ( v1_lattice3(X0)
       => ~ v3_struct_0(X0) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattice3) ).

fof(f45,axiom,
    ! [X0] :
      ( ( v2_orders_2(X0)
        & v3_orders_2(X0)
        & v4_orders_2(X0)
        & v1_lattice3(X0)
        & v2_lattice3(X0)
        & l1_orders_2(X0) )
     => ! [X1] :
          ( ( v2_orders_2(X1)
            & v3_orders_2(X1)
            & v4_orders_2(X1)
            & v1_lattice3(X1)
            & v2_lattice3(X1)
            & l1_orders_2(X1) )
         => ! [X2] :
              ( ( v1_funct_1(X2)
                & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
                & m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
             => ( ( v3_lattice3(X0)
                  & v3_lattice3(X1)
                  & v18_waybel_0(X2,X1,X0) )
               => ! [X3] :
                    ( ( v1_funct_1(X3)
                      & v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
                      & m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
                   => ( X3 = k2_waybel34(X0,X1,X2)
                    <=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_waybel34) ).

fof(f47,axiom,
    ! [X0] :
      ( ( ~ v3_struct_0(X0)
        & l1_orders_2(X0) )
     => ! [X1] :
          ( m1_subset_1(X1,u1_struct_0(X0))
         => ! [X2] :
              ( r4_waybel_1(X0,X1,X2)
            <=> ( r1_yellow_0(X0,X2)
                & X1 = k1_yellow_0(X0,X2)
                & r2_hidden(k1_yellow_0(X0,X2),X2) ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_waybel_1) ).

fof(f57,axiom,
    ! [X0,X1,X2] :
      ( ( v2_orders_2(X0)
        & v3_orders_2(X0)
        & v4_orders_2(X0)
        & v1_lattice3(X0)
        & v2_lattice3(X0)
        & l1_orders_2(X0)
        & v2_orders_2(X1)
        & v3_orders_2(X1)
        & v4_orders_2(X1)
        & v1_lattice3(X1)
        & v2_lattice3(X1)
        & l1_orders_2(X1)
        & v1_funct_1(X2)
        & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
        & m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
     => ( v1_funct_1(k2_waybel34(X0,X1,X2))
        & v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
        & m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_waybel34) ).

fof(f63,axiom,
    ! [X0,X1,X2,X3] :
      ( ( ~ v1_xboole_0(X0)
        & ~ v3_struct_0(X1)
        & l1_struct_0(X1)
        & v1_funct_1(X2)
        & v1_funct_2(X2,X0,u1_struct_0(X1))
        & m1_relset_1(X2,X0,u1_struct_0(X1))
        & m1_subset_1(X3,X0) )
     => m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_yellow_2) ).

fof(f64,axiom,
    ! [X0] :
      ( l1_orders_2(X0)
     => l1_struct_0(X0) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).

fof(f89,axiom,
    ! [X0] :
      ( ( ~ v3_struct_0(X0)
        & l1_struct_0(X0) )
     => ~ v1_xboole_0(u1_struct_0(X0)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).

fof(f122,axiom,
    ! [X0,X1,X2] :
      ( m2_relset_1(X2,X0,X1)
    <=> m1_relset_1(X2,X0,X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).

fof(f124,axiom,
    ! [X0] :
      ( ( ~ v3_struct_0(X0)
        & v2_orders_2(X0)
        & v3_orders_2(X0)
        & v4_orders_2(X0)
        & l1_orders_2(X0) )
     => ! [X1] :
          ( ( ~ v3_struct_0(X1)
            & v2_orders_2(X1)
            & v3_orders_2(X1)
            & v4_orders_2(X1)
            & l1_orders_2(X1) )
         => ! [X2] :
              ( ( v1_funct_1(X2)
                & v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
                & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
             => ! [X3] :
                  ( ( v1_funct_1(X3)
                    & v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                    & m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
                 => ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                  <=> ( v5_orders_3(X3,X1,X0)
                      & ! [X4] :
                          ( m1_subset_1(X4,u1_struct_0(X0))
                         => r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4))) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_waybel_1) ).

fof(f157,plain,
    ? [X0] :
      ( ? [X1] :
          ( ? [X2] :
              ( ? [X3] :
                  ( k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) != k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3)))
                  & m1_subset_1(X3,u1_struct_0(X0)) )
              & v1_funct_1(X2)
              & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
              & v18_waybel_0(X2,X1,X0)
              & m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
          & v2_orders_2(X1)
          & v3_orders_2(X1)
          & v4_orders_2(X1)
          & v1_lattice3(X1)
          & v2_lattice3(X1)
          & v3_lattice3(X1)
          & l1_orders_2(X1) )
      & v2_orders_2(X0)
      & v3_orders_2(X0)
      & v4_orders_2(X0)
      & v1_lattice3(X0)
      & v2_lattice3(X0)
      & v3_lattice3(X0)
      & l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f2]) ).

fof(f158,plain,
    ? [X0] :
      ( ? [X1] :
          ( ? [X2] :
              ( ? [X3] :
                  ( k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) != k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3)))
                  & m1_subset_1(X3,u1_struct_0(X0)) )
              & v1_funct_1(X2)
              & v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
              & v18_waybel_0(X2,X1,X0)
              & m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
          & v2_orders_2(X1)
          & v3_orders_2(X1)
          & v4_orders_2(X1)
          & v1_lattice3(X1)
          & v2_lattice3(X1)
          & v3_lattice3(X1)
          & l1_orders_2(X1) )
      & v2_orders_2(X0)
      & v3_orders_2(X0)
      & v4_orders_2(X0)
      & v1_lattice3(X0)
      & v2_lattice3(X0)
      & v3_lattice3(X0)
      & l1_orders_2(X0) ),
    inference(flattening,[],[f157]) ).

fof(f182,plain,
    ! [X0] :
      ( ~ v3_struct_0(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f21]) ).

fof(f183,plain,
    ! [X0] :
      ( ~ v3_struct_0(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f182]) ).

fof(f221,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( X3 = k2_waybel34(X0,X1,X2)
                  <=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
                  | ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
              | ~ v3_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v18_waybel_0(X2,X1,X0)
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
              | ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ v1_lattice3(X1)
          | ~ v2_lattice3(X1)
          | ~ l1_orders_2(X1) )
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f45]) ).

fof(f222,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( X3 = k2_waybel34(X0,X1,X2)
                  <=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
                  | ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
              | ~ v3_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v18_waybel_0(X2,X1,X0)
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
              | ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ v1_lattice3(X1)
          | ~ v2_lattice3(X1)
          | ~ l1_orders_2(X1) )
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f221]) ).

fof(f223,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( r4_waybel_1(X0,X1,X2)
            <=> ( r1_yellow_0(X0,X2)
                & X1 = k1_yellow_0(X0,X2)
                & r2_hidden(k1_yellow_0(X0,X2),X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f47]) ).

fof(f224,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( r4_waybel_1(X0,X1,X2)
            <=> ( r1_yellow_0(X0,X2)
                & X1 = k1_yellow_0(X0,X2)
                & r2_hidden(k1_yellow_0(X0,X2),X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f223]) ).

fof(f228,plain,
    ! [X0,X1,X2] :
      ( ( v1_funct_1(k2_waybel34(X0,X1,X2))
        & v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
        & m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
    inference(ennf_transformation,[],[f57]) ).

fof(f229,plain,
    ! [X0,X1,X2] :
      ( ( v1_funct_1(k2_waybel34(X0,X1,X2))
        & v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
        & m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
    inference(flattening,[],[f228]) ).

fof(f236,plain,
    ! [X0,X1,X2,X3] :
      ( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
      | v1_xboole_0(X0)
      | v3_struct_0(X1)
      | ~ l1_struct_0(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,X0,u1_struct_0(X1))
      | ~ m1_relset_1(X2,X0,u1_struct_0(X1))
      | ~ m1_subset_1(X3,X0) ),
    inference(ennf_transformation,[],[f63]) ).

fof(f237,plain,
    ! [X0,X1,X2,X3] :
      ( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
      | v1_xboole_0(X0)
      | v3_struct_0(X1)
      | ~ l1_struct_0(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,X0,u1_struct_0(X1))
      | ~ m1_relset_1(X2,X0,u1_struct_0(X1))
      | ~ m1_subset_1(X3,X0) ),
    inference(flattening,[],[f236]) ).

fof(f238,plain,
    ! [X0] :
      ( l1_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f64]) ).

fof(f256,plain,
    ! [X0] :
      ( ~ v1_xboole_0(u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ l1_struct_0(X0) ),
    inference(ennf_transformation,[],[f89]) ).

fof(f257,plain,
    ! [X0] :
      ( ~ v1_xboole_0(u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ l1_struct_0(X0) ),
    inference(flattening,[],[f256]) ).

fof(f296,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                  <=> ( v5_orders_3(X3,X1,X0)
                      & ! [X4] :
                          ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                          | ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f124]) ).

fof(f297,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                  <=> ( v5_orders_3(X3,X1,X0)
                      & ! [X4] :
                          ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                          | ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f296]) ).

fof(f312,plain,
    ( k7_yellow_2(u1_struct_0(sK2),sK3,k2_waybel34(sK2,sK3,sK4),sK5) != k1_yellow_0(sK3,k5_pre_topc(sK3,sK2,sK4,k6_waybel_0(sK2,sK5)))
    & m1_subset_1(sK5,u1_struct_0(sK2))
    & v1_funct_1(sK4)
    & v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    & v18_waybel_0(sK4,sK3,sK2)
    & m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    & v2_orders_2(sK3)
    & v3_orders_2(sK3)
    & v4_orders_2(sK3)
    & v1_lattice3(sK3)
    & v2_lattice3(sK3)
    & v3_lattice3(sK3)
    & l1_orders_2(sK3)
    & v2_orders_2(sK2)
    & v3_orders_2(sK2)
    & v4_orders_2(sK2)
    & v1_lattice3(sK2)
    & v2_lattice3(sK2)
    & v3_lattice3(sK2)
    & l1_orders_2(sK2) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f158]) ).

fof(f315,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( X3 = k2_waybel34(X0,X1,X2)
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
                    & ( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
                      | k2_waybel34(X0,X1,X2) != X3 ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
                  | ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
              | ~ v3_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v18_waybel_0(X2,X1,X0)
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
              | ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ v1_lattice3(X1)
          | ~ v2_lattice3(X1)
          | ~ l1_orders_2(X1) )
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(nnf_transformation,[],[f222]) ).

fof(f316,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ( r4_waybel_1(X0,X1,X2)
                | ~ r1_yellow_0(X0,X2)
                | k1_yellow_0(X0,X2) != X1
                | ~ r2_hidden(k1_yellow_0(X0,X2),X2) )
              & ( ( r1_yellow_0(X0,X2)
                  & X1 = k1_yellow_0(X0,X2)
                  & r2_hidden(k1_yellow_0(X0,X2),X2) )
                | ~ r4_waybel_1(X0,X1,X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(nnf_transformation,[],[f224]) ).

fof(f317,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ( r4_waybel_1(X0,X1,X2)
                | ~ r1_yellow_0(X0,X2)
                | k1_yellow_0(X0,X2) != X1
                | ~ r2_hidden(k1_yellow_0(X0,X2),X2) )
              & ( ( r1_yellow_0(X0,X2)
                  & X1 = k1_yellow_0(X0,X2)
                  & r2_hidden(k1_yellow_0(X0,X2),X2) )
                | ~ r4_waybel_1(X0,X1,X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f316]) ).

fof(f341,plain,
    ! [X0,X1,X2] :
      ( ( m2_relset_1(X2,X0,X1)
        | ~ m1_relset_1(X2,X0,X1) )
      & ( m1_relset_1(X2,X0,X1)
        | ~ m2_relset_1(X2,X0,X1) ) ),
    inference(nnf_transformation,[],[f122]) ).

fof(f342,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X3,X1,X0)
                      | ? [X4] :
                          ( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                          & m1_subset_1(X4,u1_struct_0(X0)) ) )
                    & ( ( v5_orders_3(X3,X1,X0)
                        & ! [X4] :
                            ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                            | ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(nnf_transformation,[],[f297]) ).

fof(f343,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X3,X1,X0)
                      | ? [X4] :
                          ( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                          & m1_subset_1(X4,u1_struct_0(X0)) ) )
                    & ( ( v5_orders_3(X3,X1,X0)
                        & ! [X4] :
                            ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                            | ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f342]) ).

fof(f344,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X3,X1,X0)
                      | ? [X4] :
                          ( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
                          & m1_subset_1(X4,u1_struct_0(X0)) ) )
                    & ( ( v5_orders_3(X3,X1,X0)
                        & ! [X5] :
                            ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
                            | ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(rectify,[],[f343]) ).

fof(f345,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X3,X1,X0)
                      | ( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,sK29(X0,X1,X2,X3)),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,sK29(X0,X1,X2,X3))))
                        & m1_subset_1(sK29(X0,X1,X2,X3),u1_struct_0(X0)) ) )
                    & ( ( v5_orders_3(X3,X1,X0)
                        & ! [X5] :
                            ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
                            | ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
                  | ~ v1_funct_1(X3)
                  | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
                  | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
              | ~ v1_funct_1(X2)
              | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
          | v3_struct_0(X1)
          | ~ v2_orders_2(X1)
          | ~ v3_orders_2(X1)
          | ~ v4_orders_2(X1)
          | ~ l1_orders_2(X1) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(X4,sK29(X0,X1,X2,X3))],[f344]) ).

fof(f346,plain,
    l1_orders_2(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f347,plain,
    v3_lattice3(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f348,plain,
    v2_lattice3(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f349,plain,
    v1_lattice3(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f350,plain,
    v4_orders_2(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f351,plain,
    v3_orders_2(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f352,plain,
    v2_orders_2(sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f353,plain,
    l1_orders_2(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f354,plain,
    v3_lattice3(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f355,plain,
    v2_lattice3(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f356,plain,
    v1_lattice3(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f357,plain,
    v4_orders_2(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f358,plain,
    v3_orders_2(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f359,plain,
    v2_orders_2(sK3),
    inference(cnf_transformation,[],[f312]) ).

fof(f360,plain,
    m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)),
    inference(cnf_transformation,[],[f312]) ).

fof(f361,plain,
    v18_waybel_0(sK4,sK3,sK2),
    inference(cnf_transformation,[],[f312]) ).

fof(f362,plain,
    v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2)),
    inference(cnf_transformation,[],[f312]) ).

fof(f363,plain,
    v1_funct_1(sK4),
    inference(cnf_transformation,[],[f312]) ).

fof(f364,plain,
    m1_subset_1(sK5,u1_struct_0(sK2)),
    inference(cnf_transformation,[],[f312]) ).

fof(f365,plain,
    k7_yellow_2(u1_struct_0(sK2),sK3,k2_waybel34(sK2,sK3,sK4),sK5) != k1_yellow_0(sK3,k5_pre_topc(sK3,sK2,sK4,k6_waybel_0(sK2,sK5))),
    inference(cnf_transformation,[],[f312]) ).

fof(f426,plain,
    ! [X0] :
      ( ~ v3_struct_0(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f183]) ).

fof(f487,plain,
    ! [X2,X3,X0,X1] :
      ( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
      | k2_waybel34(X0,X1,X2) != X3
      | ~ v1_funct_1(X3)
      | ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
      | ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
      | ~ v3_lattice3(X0)
      | ~ v3_lattice3(X1)
      | ~ v18_waybel_0(X2,X1,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f315]) ).

fof(f491,plain,
    ! [X2,X0,X1] :
      ( ~ r4_waybel_1(X0,X1,X2)
      | k1_yellow_0(X0,X2) = X1
      | ~ m1_subset_1(X1,u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f317]) ).

fof(f496,plain,
    ! [X2,X0,X1] :
      ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
    inference(cnf_transformation,[],[f229]) ).

fof(f497,plain,
    ! [X2,X0,X1] :
      ( v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
    inference(cnf_transformation,[],[f229]) ).

fof(f498,plain,
    ! [X2,X0,X1] :
      ( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | v1_funct_1(k2_waybel34(X0,X1,X2)) ),
    inference(cnf_transformation,[],[f229]) ).

fof(f502,plain,
    ! [X2,X3,X0,X1] :
      ( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
      | v1_xboole_0(X0)
      | v3_struct_0(X1)
      | ~ l1_struct_0(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,X0,u1_struct_0(X1))
      | ~ m1_relset_1(X2,X0,u1_struct_0(X1))
      | ~ m1_subset_1(X3,X0) ),
    inference(cnf_transformation,[],[f237]) ).

fof(f503,plain,
    ! [X0] :
      ( ~ l1_orders_2(X0)
      | l1_struct_0(X0) ),
    inference(cnf_transformation,[],[f238]) ).

fof(f538,plain,
    ! [X0] :
      ( ~ v1_xboole_0(u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ l1_struct_0(X0) ),
    inference(cnf_transformation,[],[f257]) ).

fof(f642,plain,
    ! [X2,X0,X1] :
      ( ~ m2_relset_1(X2,X0,X1)
      | m1_relset_1(X2,X0,X1) ),
    inference(cnf_transformation,[],[f341]) ).

fof(f645,plain,
    ! [X2,X3,X0,X1,X5] :
      ( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
      | ~ m1_subset_1(X5,u1_struct_0(X0))
      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
      | ~ v1_funct_1(X3)
      | ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
      | v3_struct_0(X1)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ l1_orders_2(X1)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f345]) ).

fof(f658,plain,
    ! [X2,X0,X1] :
      ( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
      | ~ v1_funct_1(k2_waybel34(X0,X1,X2))
      | ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
      | ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
      | ~ v3_lattice3(X0)
      | ~ v3_lattice3(X1)
      | ~ v18_waybel_0(X2,X1,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ v2_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(equality_resolution,[],[f487]) ).

fof(f660,definition,
    sF30 = u1_struct_0(sK2),
    introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).

fof(f661,plain,
    u1_struct_0(sK2) = sF30,
    inference(reorient_equations,[],[f660]) ).

fof(f662,definition,
    sF31 = k2_waybel34(sK2,sK3,sK4),
    introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).

fof(f663,plain,
    k2_waybel34(sK2,sK3,sK4) = sF31,
    inference(reorient_equations,[],[f662]) ).

fof(f664,definition,
    sF32 = k7_yellow_2(sF30,sK3,sF31,sK5),
    introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).

fof(f665,plain,
    k7_yellow_2(sF30,sK3,sF31,sK5) = sF32,
    inference(reorient_equations,[],[f664]) ).

fof(f666,definition,
    sF33 = k6_waybel_0(sK2,sK5),
    introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).

fof(f667,plain,
    k6_waybel_0(sK2,sK5) = sF33,
    inference(reorient_equations,[],[f666]) ).

fof(f668,definition,
    sF34 = k5_pre_topc(sK3,sK2,sK4,sF33),
    introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).

fof(f669,plain,
    k5_pre_topc(sK3,sK2,sK4,sF33) = sF34,
    inference(reorient_equations,[],[f668]) ).

fof(f670,definition,
    sF35 = k1_yellow_0(sK3,sF34),
    introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).

fof(f671,plain,
    k1_yellow_0(sK3,sF34) = sF35,
    inference(reorient_equations,[],[f670]) ).

fof(f672,plain,
    sF32 != sF35,
    inference(definition_folding,[],[f365,f671,f669,f667,f665,f663,f661]) ).

fof(f673,plain,
    m1_subset_1(sK5,sF30),
    inference(definition_folding,[],[f364,f661]) ).

fof(f674,definition,
    sF36 = u1_struct_0(sK3),
    introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).

fof(f675,plain,
    u1_struct_0(sK3) = sF36,
    inference(reorient_equations,[],[f674]) ).

fof(f676,plain,
    v1_funct_2(sK4,sF36,sF30),
    inference(definition_folding,[],[f362,f661,f675]) ).

fof(f677,plain,
    m2_relset_1(sK4,sF36,sF30),
    inference(definition_folding,[],[f360,f661,f675]) ).

fof(f706,plain,
    l1_struct_0(sK2),
    inference(resolution,[],[f503,f346]) ).

fof(f707,plain,
    l1_struct_0(sK3),
    inference(resolution,[],[f503,f353]) ).

fof(f767,plain,
    ( ~ v1_xboole_0(sF30)
    | v3_struct_0(sK2)
    | ~ l1_struct_0(sK2) ),
    inference(superposition,[],[f538,f661]) ).

fof(f770,plain,
    ( ~ v1_xboole_0(sF30)
    | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f767,f706]) ).

fof(f999,plain,
    m1_relset_1(sK4,sF36,sF30),
    inference(resolution,[],[f642,f677]) ).

fof(f1829,plain,
    ( m1_subset_1(sF32,u1_struct_0(sK3))
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ l1_struct_0(sK3)
    | ~ v1_funct_1(sF31)
    | ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_subset_1(sK5,sF30) ),
    inference(superposition,[],[f502,f665]) ).

fof(f1836,plain,
    ( m1_subset_1(sF32,u1_struct_0(sK3))
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31)
    | ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_subset_1(sK5,sF30) ),
    inference(forward_subsumption_resolution,[],[f1829,f707]) ).

fof(f1840,plain,
    ( m1_subset_1(sF32,u1_struct_0(sK3))
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31)
    | ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f1836,f673]) ).

fof(f1841,plain,
    ( m1_subset_1(sF32,sF36)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31)
    | ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
    | ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f1840,f675]) ).

fof(f1842,plain,
    ( ~ v1_funct_2(sF31,sF30,sF36)
    | m1_subset_1(sF32,sF36)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31)
    | ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f1841,f675]) ).

fof(f1843,plain,
    ( ~ m1_relset_1(sF31,sF30,sF36)
    | ~ v1_funct_2(sF31,sF30,sF36)
    | m1_subset_1(sF32,sF36)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31) ),
    inference(forward_demodulation,[],[f1842,f675]) ).

fof(f2209,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v2_orders_2(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(superposition,[],[f498,f661]) ).

fof(f2216,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2209,f352]) ).

fof(f2224,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2216,f351]) ).

fof(f2232,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2224,f350]) ).

fof(f2239,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2232,f349]) ).

fof(f2245,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ l1_orders_2(sK2)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2239,f348]) ).

fof(f2249,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF30)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF30)
      | v1_funct_1(k2_waybel34(sK2,X1,X0)) ),
    inference(forward_subsumption_resolution,[],[f2245,f346]) ).

fof(f2287,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(superposition,[],[f496,f663]) ).

fof(f2296,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2287,f352]) ).

fof(f2301,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2296,f351]) ).

fof(f2306,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2301,f350]) ).

fof(f2311,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2306,f349]) ).

fof(f2316,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2311,f348]) ).

fof(f2321,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2316,f346]) ).

fof(f2322,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2321,f359]) ).

fof(f2323,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2322,f358]) ).

fof(f2324,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2323,f357]) ).

fof(f2325,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2324,f356]) ).

fof(f2326,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2325,f355]) ).

fof(f2327,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2326,f353]) ).

fof(f2328,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2327,f363]) ).

fof(f2329,plain,
    ( m2_relset_1(sF31,u1_struct_0(sK2),sF36)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2328,f675]) ).

fof(f2330,plain,
    ( m2_relset_1(sF31,sF30,sF36)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2329,f661]) ).

fof(f2331,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
    | m2_relset_1(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2330,f661]) ).

fof(f2332,plain,
    ( ~ v1_funct_2(sK4,sF36,sF30)
    | m2_relset_1(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2331,f675]) ).

fof(f2333,plain,
    ( m2_relset_1(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2332,f676]) ).

fof(f2334,plain,
    ( ~ m1_relset_1(sK4,u1_struct_0(sK3),sF30)
    | m2_relset_1(sF31,sF30,sF36) ),
    inference(forward_demodulation,[],[f2333,f661]) ).

fof(f2335,plain,
    ( ~ m1_relset_1(sK4,sF36,sF30)
    | m2_relset_1(sF31,sF30,sF36) ),
    inference(forward_demodulation,[],[f2334,f675]) ).

fof(f2336,plain,
    m2_relset_1(sF31,sF30,sF36),
    inference(forward_subsumption_resolution,[],[f2335,f999]) ).

fof(f2337,plain,
    m1_relset_1(sF31,sF30,sF36),
    inference(resolution,[],[f2336,f642]) ).

fof(f2338,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(superposition,[],[f497,f663]) ).

fof(f2347,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2338,f352]) ).

fof(f2352,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2347,f351]) ).

fof(f2357,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2352,f350]) ).

fof(f2362,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2357,f349]) ).

fof(f2367,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ l1_orders_2(sK2)
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2362,f348]) ).

fof(f2372,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2367,f346]) ).

fof(f2373,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2372,f359]) ).

fof(f2374,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2373,f358]) ).

fof(f2375,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2374,f357]) ).

fof(f2376,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2375,f356]) ).

fof(f2377,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2376,f355]) ).

fof(f2378,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2377,f353]) ).

fof(f2379,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2378,f363]) ).

fof(f2380,plain,
    ( v1_funct_2(sF31,u1_struct_0(sK2),sF36)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2379,f675]) ).

fof(f2381,plain,
    ( v1_funct_2(sF31,sF30,sF36)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2380,f661]) ).

fof(f2382,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
    | v1_funct_2(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2381,f661]) ).

fof(f2383,plain,
    ( ~ v1_funct_2(sK4,sF36,sF30)
    | v1_funct_2(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f2382,f675]) ).

fof(f2384,plain,
    ( v1_funct_2(sF31,sF30,sF36)
    | ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f2383,f676]) ).

fof(f2385,plain,
    ( ~ m1_relset_1(sK4,u1_struct_0(sK3),sF30)
    | v1_funct_2(sF31,sF30,sF36) ),
    inference(forward_demodulation,[],[f2384,f661]) ).

fof(f2386,plain,
    ( ~ m1_relset_1(sK4,sF36,sF30)
    | v1_funct_2(sF31,sF30,sF36) ),
    inference(forward_demodulation,[],[f2385,f675]) ).

fof(f2387,plain,
    v1_funct_2(sF31,sF30,sF36),
    inference(forward_subsumption_resolution,[],[f2386,f999]) ).

fof(f2650,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2)
      | ~ v2_orders_2(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(superposition,[],[f645,f667]) ).

fof(f2654,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f2650,f352]) ).

fof(f2657,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f2654,f351]) ).

fof(f2660,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f2657,f350]) ).

fof(f2663,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f2660,f346]) ).

fof(f2666,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ m1_subset_1(sK5,u1_struct_0(sK2))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2663,f661]) ).

fof(f2667,plain,
    ! [X2,X0,X1] :
      ( ~ m1_subset_1(sK5,sF30)
      | r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2666,f661]) ).

fof(f2668,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f2667,f673]) ).

fof(f2669,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
      | r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2668,f661]) ).

fof(f2670,plain,
    ! [X2,X0,X1] :
      ( ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
      | ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
      | r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2669,f661]) ).

fof(f2671,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X1,sF30,u1_struct_0(X0))
      | ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
      | ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
      | r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_1(X1)
      | ~ m2_relset_1(X1,u1_struct_0(sK2),u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2670,f661]) ).

fof(f2672,plain,
    ! [X2,X0,X1] :
      ( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
      | ~ v1_funct_2(X1,sF30,u1_struct_0(X0))
      | ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
      | ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
      | ~ m2_relset_1(X1,sF30,u1_struct_0(X0))
      | ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_1(X1)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f2671,f661]) ).

fof(f3281,plain,
    ( ~ v1_funct_2(sF31,sF30,sF36)
    | m1_subset_1(sF32,sF36)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31) ),
    inference(resolution,[],[f1843,f2337]) ).

fof(f3282,plain,
    ( m1_subset_1(sF32,sF36)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31) ),
    inference(forward_subsumption_resolution,[],[f3281,f2387]) ).

fof(f4028,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ v2_orders_2(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(superposition,[],[f2249,f675]) ).

fof(f4033,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f4028,f359]) ).

fof(f4039,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ v4_orders_2(sK3)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f4033,f358]) ).

fof(f4043,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f4039,f357]) ).

fof(f4045,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f4043,f356]) ).

fof(f4047,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF36,sF30)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f4045,f355]) ).

fof(f4049,plain,
    ! [X0] :
      ( v1_funct_1(k2_waybel34(sK2,sK3,X0))
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF36,sF30)
      | ~ m1_relset_1(X0,sF36,sF30) ),
    inference(forward_subsumption_resolution,[],[f4047,f353]) ).

fof(f4822,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(sK4)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | ~ v2_orders_2(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(sK2) ),
    inference(superposition,[],[f2672,f669]) ).

fof(f4826,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | ~ v2_orders_2(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4822,f363]) ).

fof(f4828,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4826,f359]) ).

fof(f4830,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4828,f358]) ).

fof(f4832,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4830,f357]) ).

fof(f4834,plain,
    ! [X0] :
      ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(X0,sF30,u1_struct_0(sK3))
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4832,f353]) ).

fof(f4836,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4834,f675]) ).

fof(f4838,plain,
    ! [X0] :
      ( ~ m2_relset_1(sK4,sF36,sF30)
      | ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4836,f675]) ).

fof(f4840,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4838,f677]) ).

fof(f4842,plain,
    ! [X0] :
      ( ~ v1_funct_2(sK4,sF36,sF30)
      | ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4840,f675]) ).

fof(f4844,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4842,f676]) ).

fof(f4846,plain,
    ! [X0] :
      ( ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
      | ~ v1_funct_2(X0,sF30,sF36)
      | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
      | ~ m2_relset_1(X0,sF30,sF36)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4844,f675]) ).

fof(f10619,plain,
    ( v1_funct_1(sF31)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,sF36,sF30)
    | ~ m1_relset_1(sK4,sF36,sF30) ),
    inference(superposition,[],[f4049,f663]) ).

fof(f10620,plain,
    ( v1_funct_1(sF31)
    | ~ v1_funct_2(sK4,sF36,sF30)
    | ~ m1_relset_1(sK4,sF36,sF30) ),
    inference(forward_subsumption_resolution,[],[f10619,f363]) ).

fof(f10621,plain,
    ( v1_funct_1(sF31)
    | ~ m1_relset_1(sK4,sF36,sF30) ),
    inference(forward_subsumption_resolution,[],[f10620,f676]) ).

fof(f10622,plain,
    v1_funct_1(sF31),
    inference(forward_subsumption_resolution,[],[f10621,f999]) ).

fof(f13490,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK3)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(resolution,[],[f4846,f658]) ).

fof(f13491,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK3)
    | v3_struct_0(sK2)
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(duplicate_literal_removal,[],[f13490]) ).

fof(f13494,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK2)
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13491,f426]) ).

fof(f13497,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13494,f426]) ).

fof(f13500,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v3_lattice3(sK3)
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13497,f347]) ).

fof(f13503,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v18_waybel_0(sK4,sK3,sK2)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13500,f354]) ).

fof(f13506,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13503,f361]) ).

fof(f13508,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK3)
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13506,f363]) ).

fof(f13510,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_orders_2(sK3)
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13508,f359]) ).

fof(f13512,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v4_orders_2(sK3)
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13510,f358]) ).

fof(f13514,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13512,f357]) ).

fof(f13516,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13514,f356]) ).

fof(f13518,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ l1_orders_2(sK3)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13516,f355]) ).

fof(f13520,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13518,f353]) ).

fof(f13522,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13520,f352]) ).

fof(f13524,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13522,f351]) ).

fof(f13526,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13524,f350]) ).

fof(f13528,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13526,f349]) ).

fof(f13530,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13528,f348]) ).

fof(f13532,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13530,f346]) ).

fof(f13534,plain,
    ( ~ v1_funct_2(sF31,sF30,sF36)
    | r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13532,f663]) ).

fof(f13537,plain,
    ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13534,f2387]) ).

fof(f13539,plain,
    ( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,sF31,sK5),sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13537,f663]) ).

fof(f13542,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13539,f665]) ).

fof(f13543,plain,
    ( ~ m2_relset_1(sF31,sF30,sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13542,f663]) ).

fof(f13544,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13543,f2336]) ).

fof(f13545,plain,
    ( ~ v1_funct_1(sF31)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13544,f663]) ).

fof(f13546,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13545,f10622]) ).

fof(f13547,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13546,f675]) ).

fof(f13548,plain,
    ( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13547,f661]) ).

fof(f13549,plain,
    ( ~ v1_funct_2(sF31,sF30,sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13548,f663]) ).

fof(f13550,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13549,f2387]) ).

fof(f13551,plain,
    ( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13550,f675]) ).

fof(f13552,plain,
    ( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13551,f661]) ).

fof(f13553,plain,
    ( ~ m2_relset_1(sF31,sF30,sF36)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13552,f663]) ).

fof(f13554,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13553,f2336]) ).

fof(f13555,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13554,f661]) ).

fof(f13556,plain,
    ( ~ v1_funct_2(sK4,sF36,sF30)
    | r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f13555,f675]) ).

fof(f13557,plain,
    ( r4_waybel_1(sK3,sF32,sF34)
    | ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f13556,f676]) ).

fof(f13558,plain,
    ( ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
    | r4_waybel_1(sK3,sF32,sF34) ),
    inference(forward_demodulation,[],[f13557,f661]) ).

fof(f13559,plain,
    ( ~ m2_relset_1(sK4,sF36,sF30)
    | r4_waybel_1(sK3,sF32,sF34) ),
    inference(forward_demodulation,[],[f13558,f675]) ).

fof(f13560,plain,
    r4_waybel_1(sK3,sF32,sF34),
    inference(forward_subsumption_resolution,[],[f13559,f677]) ).

fof(f13561,plain,
    ( sF32 = k1_yellow_0(sK3,sF34)
    | ~ m1_subset_1(sF32,u1_struct_0(sK3))
    | v3_struct_0(sK3)
    | ~ l1_orders_2(sK3) ),
    inference(resolution,[],[f13560,f491]) ).

fof(f13566,plain,
    ( sF32 = k1_yellow_0(sK3,sF34)
    | ~ m1_subset_1(sF32,u1_struct_0(sK3))
    | v3_struct_0(sK3) ),
    inference(forward_subsumption_resolution,[],[f13561,f353]) ).

fof(f13569,plain,
    ( sF32 = sF35
    | ~ m1_subset_1(sF32,u1_struct_0(sK3))
    | v3_struct_0(sK3) ),
    inference(forward_demodulation,[],[f13566,f671]) ).

fof(f13571,plain,
    ( ~ m1_subset_1(sF32,u1_struct_0(sK3))
    | v3_struct_0(sK3) ),
    inference(forward_subsumption_resolution,[],[f13569,f672]) ).

fof(f13572,plain,
    ( ~ m1_subset_1(sF32,sF36)
    | v3_struct_0(sK3) ),
    inference(forward_demodulation,[],[f13571,f675]) ).

fof(f13573,plain,
    ( v3_struct_0(sK3)
    | v1_xboole_0(sF30)
    | v3_struct_0(sK3)
    | ~ v1_funct_1(sF31) ),
    inference(resolution,[],[f13572,f3282]) ).

fof(f13574,plain,
    ( v3_struct_0(sK3)
    | v1_xboole_0(sF30)
    | ~ v1_funct_1(sF31) ),
    inference(duplicate_literal_removal,[],[f13573]) ).

fof(f13575,plain,
    ( v1_xboole_0(sF30)
    | v3_struct_0(sK3) ),
    inference(forward_subsumption_resolution,[],[f13574,f10622]) ).

fof(f13580,plain,
    ( v3_struct_0(sK2)
    | v3_struct_0(sK3) ),
    inference(resolution,[],[f13575,f770]) ).

fof(f13593,plain,
    ( v3_struct_0(sK3)
    | ~ v1_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(resolution,[],[f13580,f426]) ).

fof(f13594,plain,
    ( v3_struct_0(sK3)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13593,f349]) ).

fof(f13596,plain,
    v3_struct_0(sK3),
    inference(forward_subsumption_resolution,[],[f13594,f346]) ).

fof(f13602,plain,
    ( ~ v1_lattice3(sK3)
    | ~ l1_orders_2(sK3) ),
    inference(resolution,[],[f13596,f426]) ).

fof(f13603,plain,
    ~ l1_orders_2(sK3),
    inference(forward_subsumption_resolution,[],[f13602,f356]) ).

fof(f13605,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f13603,f353]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42  % Computer : n010.cluster.edu
% 0.15/0.42  % Model    : x86_64 x86_64
% 0.15/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42  % Memory   : 8046.5625MB
% 0.15/0.42  % OS       : Linux 6.8.0-71-generic
% 0.15/0.42  % CPULimit : 300
% 0.15/0.42  % WCLimit  : 300
% 0.15/0.42  % DateTime : Sun Sep 27 14:56:46 UTC 2026
% 0.15/0.43  % CPUTime  : 
% 0.15/0.43  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.48  Running first-order model finding
% 0.23/0.48  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.12/4.35  % (1054125)Will run a generic schedule for satisfiability detection.
% 27.12/4.35  % (1054131)% WARNING: option uhcvi not known.
% 27.12/4.35  % (1054132)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4007761278:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.12/4.35  % (1054131)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1742172670:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.12/4.35  % (1054133)dis+10_1_sil=32000:sp=arity:random_seed=2024089579:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.12/4.35  % (1054130)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3189721060_2999 on theBenchmark for (2999ds/0Mi)
% 27.12/4.35  % (1054136)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3621826522:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.12/4.35  % (1054135)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3479342951:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.12/4.35  % (1054134)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3016323097:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.12/4.35  % TRYING [1]
% 27.12/4.35  % TRYING [2]
% 27.12/4.35  % TRYING [3]
% 27.12/4.35  % (1054133)Instruction limit reached! 
% 27.12/4.35  % (1054133)------------------------------
% 27.12/4.35  % (1054133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.12/4.35  % (1054133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.12/4.35  % (1054133)CaDiCaL version: 2.1.3
% 27.12/4.35  % (1054133)Termination reason: Instruction limit
% 27.12/4.35  % (1054133)Termination phase: Saturation
% 27.12/4.35  % (1054133)Time elapsed: 0.091 s
% 27.12/4.35  % (1054133)Peak memory usage: 13 MB
% 27.12/4.35  % (1054133)Instructions burned: 104 (million)
% 27.12/4.35  % (1054134)Instruction limit reached! 
% 27.12/4.35  % (1054134)------------------------------
% 27.12/4.35  % (1054134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.12/4.35  % (1054134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.12/4.35  % (1054134)CaDiCaL version: 2.1.3
% 27.12/4.35  % (1054134)Termination reason: Instruction limit
% 27.12/4.35  % (1054134)Termination phase: Saturation
% 27.12/4.35  % (1054134)Time elapsed: 0.108 s
% 27.12/4.35  % (1054134)Peak memory usage: 13 MB
% 27.12/4.35  % (1054134)Instructions burned: 116 (million)
% 27.12/4.35  % (1054144)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=668386010:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.12/4.35  % (1054135)Instruction limit reached! 
% 27.12/4.35  % (1054135)------------------------------
% 27.12/4.35  % (1054135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.12/4.35  % (1054135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.12/4.35  % (1054135)CaDiCaL version: 2.1.3
% 27.12/4.35  % (1054135)Termination reason: Instruction limit
% 27.12/4.35  % (1054135)Termination phase: Saturation
% 27.12/4.35  % (1054135)Time elapsed: 0.114 s
% 27.12/4.35  % (1054135)Peak memory usage: 13 MB
% 27.12/4.35  % (1054135)Instructions burned: 132 (million)
% 27.12/4.35  % (1054147)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3323398666:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.12/4.35  % TRYING [1]
% 27.12/4.35  % (1054145)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3594558577:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.12/4.35  % TRYING [2]
% 27.12/4.35  % (1054136)Instruction limit reached! 
% 27.12/4.35  % (1054136)------------------------------
% 27.12/4.35  % (1054136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.12/4.35  % (1054136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.12/4.35  % (1054136)CaDiCaL version: 2.1.3
% 27.12/4.35  % (1054136)Termination reason: Instruction limit
% 27.12/4.35  % (1054136)Termination phase: Saturation
% 27.12/4.35  % (1054136)Time elapsed: 0.153 s
% 27.12/4.35  % (1054136)Peak memory usage: 13 MB
% 27.12/4.35  % (1054136)Instructions burned: 159 (million)
% 27.12/4.35  % TRYING [3]
% 27.12/4.35  % TRYING [4]
% 27.12/4.35  % (1054150)ott-21_1_sil=16000:fs=off:random_seed=3388752809:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.12/4.35  % (1054145)Instruction limit reached! 
% 27.12/4.35  % (1054145)------------------------------
% 27.12/4.35  % (1054145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.12/4.35  % (1054145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054145)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054145)Termination reason: Instruction limit
% 17.04/7.66  % (1054145)Termination phase: Saturation
% 17.04/7.66  % (1054145)Time elapsed: 0.125 s
% 17.04/7.66  % (1054145)Peak memory usage: 13 MB
% 17.04/7.66  % (1054145)Instructions burned: 132 (million)
% 17.04/7.66  % (1054152)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2304620178:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 17.04/7.66  % TRYING [4]
% 17.04/7.66  % (1054150)Instruction limit reached! 
% 17.04/7.66  % (1054150)------------------------------
% 17.04/7.66  % (1054150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054150)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054150)Termination reason: Instruction limit
% 17.04/7.66  % (1054150)Termination phase: Saturation
% 17.04/7.66  % (1054150)Time elapsed: 0.161 s
% 17.04/7.66  % (1054150)Peak memory usage: 13 MB
% 17.04/7.66  % (1054150)Instructions burned: 180 (million)
% 17.04/7.66  % (1054154)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1718215600:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 17.04/7.66  % TRYING [1]
% 17.04/7.66  % TRYING [2]
% 17.04/7.66  % TRYING [3]
% 17.04/7.66  % (1054144)Instruction limit reached! 
% 17.04/7.66  % (1054144)------------------------------
% 17.04/7.66  % (1054144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054144)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054144)Termination reason: Instruction limit
% 17.04/7.66  % (1054144)Termination phase: Finite model building SAT solving
% 17.04/7.66  % (1054144)Time elapsed: 0.522 s
% 17.04/7.66  % (1054144)Peak memory usage: 33 MB
% 17.04/7.66  % (1054144)Instructions burned: 714 (million)
% 17.04/7.66  % (1054156)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2540151387:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 17.04/7.66  % (1054152)Instruction limit reached! 
% 17.04/7.66  % (1054152)------------------------------
% 17.04/7.66  % (1054152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054152)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054152)Termination reason: Instruction limit
% 17.04/7.66  % (1054152)Termination phase: Saturation
% 17.04/7.66  % (1054152)Time elapsed: 0.484 s
% 17.04/7.66  % (1054152)Peak memory usage: 15 MB
% 17.04/7.66  % (1054152)Instructions burned: 478 (million)
% 17.04/7.66  % TRYING [5]
% 17.04/7.66  % (1054158)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=964082347:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 17.04/7.66  % (1054147)Instruction limit reached! 
% 17.04/7.66  % (1054147)------------------------------
% 17.04/7.66  % (1054147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054147)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054147)Termination reason: Instruction limit
% 17.04/7.66  % (1054147)Termination phase: Saturation
% 17.04/7.66  % (1054147)Time elapsed: 0.708 s
% 17.04/7.66  % (1054147)Peak memory usage: 20 MB
% 17.04/7.66  % (1054147)Instructions burned: 684 (million)
% 17.04/7.66  % (1054160)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3261130835:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 17.04/7.66  % TRYING [4]
% 17.04/7.66  % (1054154)Instruction limit reached! 
% 17.04/7.66  % (1054154)------------------------------
% 17.04/7.66  % (1054154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054154)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054154)Termination reason: Instruction limit
% 17.04/7.66  % (1054154)Termination phase: Finite model building constraint generation
% 17.04/7.66  % (1054154)Time elapsed: 0.616 s
% 17.04/7.66  % (1054154)Peak memory usage: 22 MB
% 17.04/7.66  % (1054154)Instructions burned: 865 (million)
% 17.04/7.66  % (1054162)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2379066120:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 17.04/7.66  % (1054158)Instruction limit reached! 
% 17.04/7.66  % (1054158)------------------------------
% 17.04/7.66  % (1054158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054158)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054158)Termination reason: Instruction limit
% 17.04/7.66  % (1054158)Termination phase: Finite model building constraint generation
% 17.04/7.66  % (1054158)Time elapsed: 0.633 s
% 17.04/7.66  % (1054158)Peak memory usage: 102 MB
% 17.04/7.66  % (1054158)Instructions burned: 889 (million)
% 17.04/7.66  % (1054164)fmb+10_1_sil=64000:random_seed=2761604668:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 17.04/7.66  % TRYING [1]
% 17.04/7.66  % TRYING [2]
% 17.04/7.66  % TRYING [3]
% 17.04/7.66  % (1054160)Instruction limit reached! 
% 17.04/7.66  % (1054160)------------------------------
% 17.04/7.66  % (1054160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054160)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054160)Termination reason: Instruction limit
% 17.04/7.66  % (1054160)Termination phase: Saturation
% 17.04/7.66  % (1054160)Time elapsed: 0.718 s
% 17.04/7.66  % (1054160)Peak memory usage: 25 MB
% 17.04/7.66  % (1054160)Instructions burned: 693 (million)
% 17.04/7.66  % (1054166)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3522531385:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 17.04/7.66  % TRYING [20]
% 17.04/7.66  % (1054156)Instruction limit reached! 
% 17.04/7.66  % (1054156)------------------------------
% 17.04/7.66  % (1054156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054156)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054156)Termination reason: Instruction limit
% 17.04/7.66  % (1054156)Termination phase: Saturation
% 17.04/7.66  % (1054156)Time elapsed: 1.065 s
% 17.04/7.66  % (1054156)Peak memory usage: 27 MB
% 17.04/7.66  % (1054156)Instructions burned: 1179 (million)
% 17.04/7.66  % (1054168)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=128940003:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 17.04/7.66  % TRYING [8]
% 17.04/7.66  % TRYING [4]
% 17.04/7.66  % (1054162)Instruction limit reached! 
% 17.04/7.66  % (1054162)------------------------------
% 17.04/7.66  % (1054162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054162)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054162)Termination reason: Instruction limit
% 17.04/7.66  % (1054162)Termination phase: Saturation
% 17.04/7.66  % (1054162)Time elapsed: 0.829 s
% 17.04/7.66  % (1054162)Peak memory usage: 20 MB
% 17.04/7.66  % (1054162)Instructions burned: 880 (million)
% 17.04/7.66  % (1054170)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=386550872:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 17.04/7.66  % (1054168)Instruction limit reached! 
% 17.04/7.66  % (1054168)------------------------------
% 17.04/7.66  % (1054168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054168)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054168)Termination reason: Instruction limit
% 17.04/7.66  % (1054168)Termination phase: Finite model building constraint generation
% 17.04/7.66  % (1054168)Time elapsed: 0.564 s
% 17.04/7.66  % (1054168)Peak memory usage: 53 MB
% 17.04/7.66  % (1054168)Instructions burned: 920 (million)
% 17.04/7.66  % (1054172)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3476557223:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi)
% 17.04/7.66  % TRYING [5]
% 17.04/7.66  % (1054172)Instruction limit reached! 
% 17.04/7.66  % (1054172)------------------------------
% 17.04/7.66  % (1054172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054172)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054172)Termination reason: Instruction limit
% 17.04/7.66  % (1054172)Termination phase: Saturation
% 17.04/7.66  % (1054172)Time elapsed: 1.359 s
% 17.04/7.66  % (1054172)Peak memory usage: 26 MB
% 17.04/7.66  % (1054172)Instructions burned: 1473 (million)
% 17.04/7.66  % (1054174)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1400607565:i=6324_2962 on theBenchmark for (2962ds/6324Mi)
% 17.04/7.66  % (1054174)Cannot represent all propositional literals internally
% 17.04/7.66  % (1054174)Refutation not found, incomplete strategy
% 17.04/7.66  % (1054174)------------------------------
% 17.04/7.66  % (1054174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054174)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054174)Termination reason: Refutation not found, incomplete strategy
% 17.04/7.66  % (1054174)Time elapsed: 0.034 s
% 17.04/7.66  % (1054174)Peak memory usage: 11 MB
% 17.04/7.66  % (1054174)Instructions burned: 55 (million)
% 17.04/7.66  % (1054174)------------------------------
% 17.04/7.66  % (1054174)------------------------------
% 17.04/7.66  % (1054176)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3886667624:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 17.04/7.66  % TRYING [16]
% 17.04/7.66  % (1054176)Instruction limit reached! 
% 17.04/7.66  % (1054176)------------------------------
% 17.04/7.66  % (1054176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054176)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054176)Termination reason: Instruction limit
% 17.04/7.66  % (1054176)Termination phase: Finite model building constraint generation
% 17.04/7.66  % (1054176)Time elapsed: 1.486 s
% 17.04/7.66  % (1054176)Peak memory usage: 119 MB
% 17.04/7.66  % (1054176)Instructions burned: 2174 (million)
% 17.04/7.66  % (1054182)ott-2_1_sil=16000:newcnf=on:random_seed=1747516337:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi)
% 17.04/7.66  % TRYING [6]
% 17.04/7.66  % (1054182)Instruction limit reached! 
% 17.04/7.66  % (1054182)------------------------------
% 17.04/7.66  % (1054182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054182)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054182)Termination reason: Instruction limit
% 17.04/7.66  % (1054182)Termination phase: Saturation
% 17.04/7.66  % (1054182)Time elapsed: 0.845 s
% 17.04/7.66  % (1054182)Peak memory usage: 19 MB
% 17.04/7.66  % (1054182)Instructions burned: 869 (million)
% 17.04/7.66  % (1054184)ott+10_1_sil=32000:tgt=ground:random_seed=2332271222:i=5114:av=off_2937 on theBenchmark for (2937ds/5114Mi)
% 17.04/7.66  % (1054170)Instruction limit reached! 
% 17.04/7.66  % (1054170)------------------------------
% 17.04/7.66  % (1054170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.66  % (1054170)CaDiCaL version: 2.1.3
% 17.04/7.66  % (1054170)Termination reason: Instruction limit
% 17.04/7.66  % (1054170)Termination phase: Saturation
% 17.04/7.66  % (1054170)Time elapsed: 4.513 s
% 17.04/7.66  % (1054170)Peak memory usage: 38 MB
% 17.04/7.66  % (1054170)Instructions burned: 5132 (million)
% 17.04/7.66  % (1054186)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2719726728:i=54282_2935 on theBenchmark for (2935ds/54282Mi)
% 17.04/7.66  % TRYING [1]
% 17.04/7.66  % TRYING [2]
% 17.04/7.66  % TRYING [3]
% 17.04/7.66  % TRYING [4]
% 17.04/7.66  % (1054184) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1054125-1054184"...
% 17.04/7.66  % (1054184)...printing done.
% 17.04/7.66  % (1054184)Refutation found. Thanks to Tanya!
% 17.04/7.66  % SZS status Theorem for theBenchmark
% 17.04/7.66  % SZS output start Proof for theBenchmark
% See solution above
% 17.04/7.66  % (1054184)------------------------------
% 17.04/7.66  % (1054184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.04/7.66  % (1054184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.04/7.67  % (1054184)CaDiCaL version: 2.1.3
% 17.04/7.67  % (1054184)Termination reason: Refutation
% 17.04/7.67  % (1054184)Time elapsed: 0.768 s
% 17.04/7.67  % (1054184)Peak memory usage: 19 MB
% 17.04/7.67  % (1054184)Instructions burned: 851 (million)
% 17.04/7.67  % (1054125)Success in time 7.171 s
% 17.04/7.67  % Vampire exiting
%------------------------------------------------------------------------------