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

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

% Computer : n020.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:34 AM UTC 2026

% Result   : Theorem 21.30s 4.55s
% Output   : Refutation 21.30s
% 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(X0),u1_struct_0(X1))
                & v17_waybel_0(X2,X0,X1)
                & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
             => ! [X3] :
                  ( m1_subset_1(X3,u1_struct_0(X1))
                 => k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) = k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3))) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_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(X0),u1_struct_0(X1))
                  & v17_waybel_0(X2,X0,X1)
                  & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
               => ! [X3] :
                    ( m1_subset_1(X3,u1_struct_0(X1))
                   => k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) = k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,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/sandbox/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(X0),u1_struct_0(X1))
                & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
             => ( ( v3_lattice3(X0)
                  & v3_lattice3(X1)
                  & v17_waybel_0(X2,X0,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)) )
                   => ( X3 = k1_waybel34(X0,X1,X2)
                    <=> v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_waybel34) ).

fof(f47,axiom,
    ! [X0] :
      ( ( ~ v3_struct_0(X0)
        & l1_orders_2(X0) )
     => ! [X1] :
          ( m1_subset_1(X1,u1_struct_0(X0))
         => ! [X2] :
              ( r3_waybel_1(X0,X1,X2)
            <=> ( r2_yellow_0(X0,X2)
                & X1 = k2_yellow_0(X0,X2)
                & r2_hidden(k2_yellow_0(X0,X2),X2) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_waybel_1) ).

fof(f52,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(X0),u1_struct_0(X1))
        & m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
     => ( v1_funct_1(k1_waybel34(X0,X1,X2))
        & v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
        & m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_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/sandbox/benchmark/theBenchmark.p',dt_k7_yellow_2) ).

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

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

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

fof(f123,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(X2,X0,X1)
                      & ! [X4] :
                          ( m1_subset_1(X4,u1_struct_0(X1))
                         => r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4))) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_waybel_1) ).

fof(f156,plain,
    ? [X0] :
      ( ? [X1] :
          ( ? [X2] :
              ( ? [X3] :
                  ( k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) != k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
                  & m1_subset_1(X3,u1_struct_0(X1)) )
              & v1_funct_1(X2)
              & v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              & v17_waybel_0(X2,X0,X1)
              & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(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) )
      & 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(f157,plain,
    ? [X0] :
      ( ? [X1] :
          ( ? [X2] :
              ( ? [X3] :
                  ( k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) != k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
                  & m1_subset_1(X3,u1_struct_0(X1)) )
              & v1_funct_1(X2)
              & v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
              & v17_waybel_0(X2,X0,X1)
              & m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(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) )
      & 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,[],[f156]) ).

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

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

fof(f220,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( X3 = k1_waybel34(X0,X1,X2)
                  <=> 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)) )
              | ~ v3_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v17_waybel_0(X2,X0,X1)
              | ~ 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)) )
          | ~ 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(f221,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( X3 = k1_waybel34(X0,X1,X2)
                  <=> 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)) )
              | ~ v3_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v17_waybel_0(X2,X0,X1)
              | ~ 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)) )
          | ~ 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,[],[f220]) ).

fof(f222,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( r3_waybel_1(X0,X1,X2)
            <=> ( r2_yellow_0(X0,X2)
                & X1 = k2_yellow_0(X0,X2)
                & r2_hidden(k2_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(f223,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( r3_waybel_1(X0,X1,X2)
            <=> ( r2_yellow_0(X0,X2)
                & X1 = k2_yellow_0(X0,X2)
                & r2_hidden(k2_yellow_0(X0,X2),X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f222]) ).

fof(f226,plain,
    ! [X0,X1,X2] :
      ( ( v1_funct_1(k1_waybel34(X0,X1,X2))
        & v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
        & m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
      | ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
    inference(ennf_transformation,[],[f52]) ).

fof(f227,plain,
    ! [X0,X1,X2] :
      ( ( v1_funct_1(k1_waybel34(X0,X1,X2))
        & v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
        & m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
      | ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
    inference(flattening,[],[f226]) ).

fof(f235,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(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(flattening,[],[f235]) ).

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

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

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

fof(f293,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                  <=> ( v5_orders_3(X2,X0,X1)
                      & ! [X4] :
                          ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                          | ~ m1_subset_1(X4,u1_struct_0(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(ennf_transformation,[],[f123]) ).

fof(f294,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                  <=> ( v5_orders_3(X2,X0,X1)
                      & ! [X4] :
                          ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                          | ~ m1_subset_1(X4,u1_struct_0(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,[],[f293]) ).

fof(f309,plain,
    ( k7_yellow_2(u1_struct_0(sK3),sK2,k1_waybel34(sK2,sK3,sK4),sK5) != k2_yellow_0(sK2,k5_pre_topc(sK2,sK3,sK4,k7_waybel_0(sK3,sK5)))
    & m1_subset_1(sK5,u1_struct_0(sK3))
    & v1_funct_1(sK4)
    & v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    & v17_waybel_0(sK4,sK2,sK3)
    & m2_relset_1(sK4,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)
    & 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)],[f157]) ).

fof(f312,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( X3 = k1_waybel34(X0,X1,X2)
                      | ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) )
                    & ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | k1_waybel34(X0,X1,X2) != 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_lattice3(X0)
              | ~ v3_lattice3(X1)
              | ~ v17_waybel_0(X2,X0,X1)
              | ~ 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)) )
          | ~ 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,[],[f221]) ).

fof(f313,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ( r3_waybel_1(X0,X1,X2)
                | ~ r2_yellow_0(X0,X2)
                | k2_yellow_0(X0,X2) != X1
                | ~ r2_hidden(k2_yellow_0(X0,X2),X2) )
              & ( ( r2_yellow_0(X0,X2)
                  & X1 = k2_yellow_0(X0,X2)
                  & r2_hidden(k2_yellow_0(X0,X2),X2) )
                | ~ r3_waybel_1(X0,X1,X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(nnf_transformation,[],[f223]) ).

fof(f314,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ( r3_waybel_1(X0,X1,X2)
                | ~ r2_yellow_0(X0,X2)
                | k2_yellow_0(X0,X2) != X1
                | ~ r2_hidden(k2_yellow_0(X0,X2),X2) )
              & ( ( r2_yellow_0(X0,X2)
                  & X1 = k2_yellow_0(X0,X2)
                  & r2_hidden(k2_yellow_0(X0,X2),X2) )
                | ~ r3_waybel_1(X0,X1,X2) ) )
          | ~ m1_subset_1(X1,u1_struct_0(X0)) )
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f313]) ).

fof(f337,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,[],[f121]) ).

fof(f338,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X2,X0,X1)
                      | ? [X4] :
                          ( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                          & m1_subset_1(X4,u1_struct_0(X1)) ) )
                    & ( ( v5_orders_3(X2,X0,X1)
                        & ! [X4] :
                            ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                            | ~ m1_subset_1(X4,u1_struct_0(X1)) ) )
                      | ~ 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,[],[f294]) ).

fof(f339,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X2,X0,X1)
                      | ? [X4] :
                          ( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                          & m1_subset_1(X4,u1_struct_0(X1)) ) )
                    & ( ( v5_orders_3(X2,X0,X1)
                        & ! [X4] :
                            ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                            | ~ m1_subset_1(X4,u1_struct_0(X1)) ) )
                      | ~ 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,[],[f338]) ).

fof(f340,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X2,X0,X1)
                      | ? [X4] :
                          ( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
                          & m1_subset_1(X4,u1_struct_0(X1)) ) )
                    & ( ( v5_orders_3(X2,X0,X1)
                        & ! [X5] :
                            ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
                            | ~ m1_subset_1(X5,u1_struct_0(X1)) ) )
                      | ~ 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,[],[f339]) ).

fof(f341,plain,
    ! [X0] :
      ( ! [X1] :
          ( ! [X2] :
              ( ! [X3] :
                  ( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
                      | ~ v5_orders_3(X2,X0,X1)
                      | ( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,sK28(X0,X1,X2,X3)),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,sK28(X0,X1,X2,X3))))
                        & m1_subset_1(sK28(X0,X1,X2,X3),u1_struct_0(X1)) ) )
                    & ( ( v5_orders_3(X2,X0,X1)
                        & ! [X5] :
                            ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
                            | ~ m1_subset_1(X5,u1_struct_0(X1)) ) )
                      | ~ 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,[sK28]),skolemize(X4,sK28(X0,X1,X2,X3))],[f340]) ).

fof(f342,plain,
    l1_orders_2(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f343,plain,
    v3_lattice3(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f344,plain,
    v2_lattice3(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f345,plain,
    v1_lattice3(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f346,plain,
    v4_orders_2(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f347,plain,
    v3_orders_2(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f348,plain,
    v2_orders_2(sK2),
    inference(cnf_transformation,[],[f309]) ).

fof(f349,plain,
    l1_orders_2(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f350,plain,
    v3_lattice3(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f351,plain,
    v2_lattice3(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f352,plain,
    v1_lattice3(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f353,plain,
    v4_orders_2(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f354,plain,
    v3_orders_2(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f355,plain,
    v2_orders_2(sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f356,plain,
    m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
    inference(cnf_transformation,[],[f309]) ).

fof(f357,plain,
    v17_waybel_0(sK4,sK2,sK3),
    inference(cnf_transformation,[],[f309]) ).

fof(f358,plain,
    v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
    inference(cnf_transformation,[],[f309]) ).

fof(f359,plain,
    v1_funct_1(sK4),
    inference(cnf_transformation,[],[f309]) ).

fof(f360,plain,
    m1_subset_1(sK5,u1_struct_0(sK3)),
    inference(cnf_transformation,[],[f309]) ).

fof(f361,plain,
    k7_yellow_2(u1_struct_0(sK3),sK2,k1_waybel34(sK2,sK3,sK4),sK5) != k2_yellow_0(sK2,k5_pre_topc(sK2,sK3,sK4,k7_waybel_0(sK3,sK5))),
    inference(cnf_transformation,[],[f309]) ).

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

fof(f483,plain,
    ! [X2,X3,X0,X1] :
      ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
      | k1_waybel34(X0,X1,X2) != 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_lattice3(X0)
      | ~ v3_lattice3(X1)
      | ~ v17_waybel_0(X2,X0,X1)
      | ~ 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))
      | ~ 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,[],[f312]) ).

fof(f487,plain,
    ! [X2,X0,X1] :
      ( ~ r3_waybel_1(X0,X1,X2)
      | k2_yellow_0(X0,X2) = X1
      | ~ m1_subset_1(X1,u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f314]) ).

fof(f491,plain,
    ! [X2,X0,X1] :
      ( m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
      | ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
    inference(cnf_transformation,[],[f227]) ).

fof(f492,plain,
    ! [X2,X0,X1] :
      ( v1_funct_2(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
      | ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
    inference(cnf_transformation,[],[f227]) ).

fof(f493,plain,
    ! [X2,X0,X1] :
      ( ~ m1_relset_1(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(X0),u1_struct_0(X1))
      | v1_funct_1(k1_waybel34(X0,X1,X2)) ),
    inference(cnf_transformation,[],[f227]) ).

fof(f498,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,[],[f236]) ).

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

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

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

fof(f637,plain,
    ! [X2,X3,X0,X1,X5] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
      | ~ m1_subset_1(X5,u1_struct_0(X1))
      | ~ 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,[],[f341]) ).

fof(f650,plain,
    ! [X2,X0,X1] :
      ( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
      | ~ v1_funct_1(k1_waybel34(X0,X1,X2))
      | ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
      | ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
      | ~ v3_lattice3(X0)
      | ~ v3_lattice3(X1)
      | ~ v17_waybel_0(X2,X0,X1)
      | ~ 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))
      | ~ 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,[],[f483]) ).

fof(f652,definition,
    sF29 = u1_struct_0(sK3),
    introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).

fof(f653,plain,
    u1_struct_0(sK3) = sF29,
    inference(reorient_equations,[],[f652]) ).

fof(f654,definition,
    sF30 = k1_waybel34(sK2,sK3,sK4),
    introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).

fof(f655,plain,
    k1_waybel34(sK2,sK3,sK4) = sF30,
    inference(reorient_equations,[],[f654]) ).

fof(f656,definition,
    sF31 = k7_yellow_2(sF29,sK2,sF30,sK5),
    introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).

fof(f657,plain,
    k7_yellow_2(sF29,sK2,sF30,sK5) = sF31,
    inference(reorient_equations,[],[f656]) ).

fof(f658,definition,
    sF32 = k7_waybel_0(sK3,sK5),
    introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).

fof(f659,plain,
    k7_waybel_0(sK3,sK5) = sF32,
    inference(reorient_equations,[],[f658]) ).

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

fof(f661,plain,
    k5_pre_topc(sK2,sK3,sK4,sF32) = sF33,
    inference(reorient_equations,[],[f660]) ).

fof(f662,definition,
    sF34 = k2_yellow_0(sK2,sF33),
    introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).

fof(f663,plain,
    k2_yellow_0(sK2,sF33) = sF34,
    inference(reorient_equations,[],[f662]) ).

fof(f664,plain,
    sF31 != sF34,
    inference(definition_folding,[],[f361,f663,f661,f659,f657,f655,f653]) ).

fof(f665,plain,
    m1_subset_1(sK5,sF29),
    inference(definition_folding,[],[f360,f653]) ).

fof(f666,definition,
    sF35 = u1_struct_0(sK2),
    introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).

fof(f667,plain,
    u1_struct_0(sK2) = sF35,
    inference(reorient_equations,[],[f666]) ).

fof(f668,plain,
    v1_funct_2(sK4,sF35,sF29),
    inference(definition_folding,[],[f358,f653,f667]) ).

fof(f669,plain,
    m2_relset_1(sK4,sF35,sF29),
    inference(definition_folding,[],[f356,f653,f667]) ).

fof(f698,plain,
    l1_struct_0(sK2),
    inference(resolution,[],[f499,f342]) ).

fof(f699,plain,
    l1_struct_0(sK3),
    inference(resolution,[],[f499,f349]) ).

fof(f759,plain,
    ( ~ v1_xboole_0(sF29)
    | v3_struct_0(sK3)
    | ~ l1_struct_0(sK3) ),
    inference(superposition,[],[f536,f653]) ).

fof(f762,plain,
    ( ~ v1_xboole_0(sF29)
    | v3_struct_0(sK3) ),
    inference(forward_subsumption_resolution,[],[f759,f699]) ).

fof(f991,plain,
    m1_relset_1(sK4,sF35,sF29),
    inference(resolution,[],[f634,f669]) ).

fof(f1774,plain,
    ( m1_subset_1(sF31,u1_struct_0(sK2))
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ l1_struct_0(sK2)
    | ~ v1_funct_1(sF30)
    | ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_subset_1(sK5,sF29) ),
    inference(superposition,[],[f498,f657]) ).

fof(f1781,plain,
    ( m1_subset_1(sF31,u1_struct_0(sK2))
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30)
    | ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_subset_1(sK5,sF29) ),
    inference(forward_subsumption_resolution,[],[f1774,f698]) ).

fof(f1785,plain,
    ( m1_subset_1(sF31,u1_struct_0(sK2))
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30)
    | ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2)) ),
    inference(forward_subsumption_resolution,[],[f1781,f665]) ).

fof(f1786,plain,
    ( m1_subset_1(sF31,sF35)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30)
    | ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
    | ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f1785,f667]) ).

fof(f1787,plain,
    ( ~ v1_funct_2(sF30,sF29,sF35)
    | m1_subset_1(sF31,sF35)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30)
    | ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2)) ),
    inference(forward_demodulation,[],[f1786,f667]) ).

fof(f1788,plain,
    ( ~ m1_relset_1(sF30,sF29,sF35)
    | ~ v1_funct_2(sF30,sF29,sF35)
    | m1_subset_1(sF31,sF35)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30) ),
    inference(forward_demodulation,[],[f1787,f667]) ).

fof(f2158,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ 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(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,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(superposition,[],[f493,f653]) ).

fof(f2165,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ 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,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2158,f355]) ).

fof(f2173,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v4_orders_2(sK3)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2165,f354]) ).

fof(f2181,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_lattice3(sK3)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2173,f353]) ).

fof(f2188,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v2_lattice3(sK3)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2181,f352]) ).

fof(f2194,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ l1_orders_2(sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,u1_struct_0(X1),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2188,f351]) ).

fof(f2198,plain,
    ! [X0,X1] :
      ( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
      | ~ 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),sF29)
      | v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f2194,f349]) ).

fof(f2236,plain,
    ( m2_relset_1(sF30,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)
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(superposition,[],[f491,f655]) ).

fof(f2245,plain,
    ( m2_relset_1(sF30,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)
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2236,f348]) ).

fof(f2250,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2245,f347]) ).

fof(f2255,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2250,f346]) ).

fof(f2260,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2255,f345]) ).

fof(f2265,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2260,f344]) ).

fof(f2270,plain,
    ( m2_relset_1(sF30,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)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2265,f342]) ).

fof(f2271,plain,
    ( m2_relset_1(sF30,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)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2270,f355]) ).

fof(f2272,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2271,f354]) ).

fof(f2273,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_lattice3(sK3)
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2272,f353]) ).

fof(f2274,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v2_lattice3(sK3)
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2273,f352]) ).

fof(f2275,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ l1_orders_2(sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2274,f351]) ).

fof(f2276,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2275,f349]) ).

fof(f2277,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2276,f359]) ).

fof(f2278,plain,
    ( m2_relset_1(sF30,u1_struct_0(sK3),sF35)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2277,f667]) ).

fof(f2279,plain,
    ( m2_relset_1(sF30,sF29,sF35)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2278,f653]) ).

fof(f2280,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
    | m2_relset_1(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2279,f653]) ).

fof(f2281,plain,
    ( ~ v1_funct_2(sK4,sF35,sF29)
    | m2_relset_1(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2280,f667]) ).

fof(f2282,plain,
    ( m2_relset_1(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2281,f668]) ).

fof(f2283,plain,
    ( ~ m1_relset_1(sK4,u1_struct_0(sK2),sF29)
    | m2_relset_1(sF30,sF29,sF35) ),
    inference(forward_demodulation,[],[f2282,f653]) ).

fof(f2284,plain,
    ( ~ m1_relset_1(sK4,sF35,sF29)
    | m2_relset_1(sF30,sF29,sF35) ),
    inference(forward_demodulation,[],[f2283,f667]) ).

fof(f2285,plain,
    m2_relset_1(sF30,sF29,sF35),
    inference(forward_subsumption_resolution,[],[f2284,f991]) ).

fof(f2286,plain,
    m1_relset_1(sF30,sF29,sF35),
    inference(resolution,[],[f2285,f634]) ).

fof(f2287,plain,
    ( v1_funct_2(sF30,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)
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(superposition,[],[f492,f655]) ).

fof(f2296,plain,
    ( v1_funct_2(sF30,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)
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2287,f348]) ).

fof(f2301,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2296,f347]) ).

fof(f2306,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2301,f346]) ).

fof(f2311,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2306,f345]) ).

fof(f2316,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2311,f344]) ).

fof(f2321,plain,
    ( v1_funct_2(sF30,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)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2316,f342]) ).

fof(f2322,plain,
    ( v1_funct_2(sF30,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)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2321,f355]) ).

fof(f2323,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ 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(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2322,f354]) ).

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

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

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

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

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

fof(f2329,plain,
    ( v1_funct_2(sF30,u1_struct_0(sK3),sF35)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2328,f667]) ).

fof(f2330,plain,
    ( v1_funct_2(sF30,sF29,sF35)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2329,f653]) ).

fof(f2331,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
    | v1_funct_2(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2330,f653]) ).

fof(f2332,plain,
    ( ~ v1_funct_2(sK4,sF35,sF29)
    | v1_funct_2(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f2331,f667]) ).

fof(f2333,plain,
    ( v1_funct_2(sF30,sF29,sF35)
    | ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f2332,f668]) ).

fof(f2334,plain,
    ( ~ m1_relset_1(sK4,u1_struct_0(sK2),sF29)
    | v1_funct_2(sF30,sF29,sF35) ),
    inference(forward_demodulation,[],[f2333,f653]) ).

fof(f2335,plain,
    ( ~ m1_relset_1(sK4,sF35,sF29)
    | v1_funct_2(sF30,sF29,sF35) ),
    inference(forward_demodulation,[],[f2334,f667]) ).

fof(f2336,plain,
    v1_funct_2(sF30,sF29,sF35),
    inference(forward_subsumption_resolution,[],[f2335,f991]) ).

fof(f2599,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | ~ v2_orders_2(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(superposition,[],[f637,f659]) ).

fof(f2603,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | ~ v3_orders_2(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f2599,f355]) ).

fof(f2606,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | ~ v4_orders_2(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f2603,f354]) ).

fof(f2609,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | ~ l1_orders_2(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f2606,f353]) ).

fof(f2612,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f2609,f349]) ).

fof(f2615,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ m1_subset_1(sK5,u1_struct_0(sK3))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2612,f653]) ).

fof(f2616,plain,
    ! [X2,X0,X1] :
      ( ~ m1_subset_1(sK5,sF29)
      | r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2615,f653]) ).

fof(f2617,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f2616,f665]) ).

fof(f2618,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2617,f653]) ).

fof(f2619,plain,
    ! [X2,X0,X1] :
      ( ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2618,f653]) ).

fof(f2620,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X2,u1_struct_0(X0),sF29)
      | ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2619,f653]) ).

fof(f2621,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
      | ~ v1_funct_2(X2,u1_struct_0(X0),sF29)
      | ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
      | ~ m2_relset_1(X2,u1_struct_0(X0),sF29)
      | ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | v3_struct_0(sK3)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f2620,f653]) ).

fof(f3155,plain,
    ( ~ v1_funct_2(sF30,sF29,sF35)
    | m1_subset_1(sF31,sF35)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30) ),
    inference(resolution,[],[f1788,f2286]) ).

fof(f3156,plain,
    ( m1_subset_1(sF31,sF35)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30) ),
    inference(forward_subsumption_resolution,[],[f3155,f2336]) ).

fof(f3903,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ v2_orders_2(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(superposition,[],[f2198,f667]) ).

fof(f3908,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f3903,f348]) ).

fof(f3914,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ v4_orders_2(sK2)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f3908,f347]) ).

fof(f3918,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ v1_lattice3(sK2)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f3914,f346]) ).

fof(f3920,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ v2_lattice3(sK2)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f3918,f345]) ).

fof(f3922,plain,
    ! [X0] :
      ( ~ m1_relset_1(X0,sF35,sF29)
      | ~ l1_orders_2(sK2)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
    inference(forward_subsumption_resolution,[],[f3920,f344]) ).

fof(f3924,plain,
    ! [X0] :
      ( v1_funct_1(k1_waybel34(sK2,sK3,X0))
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF35,sF29)
      | ~ m1_relset_1(X0,sF35,sF29) ),
    inference(forward_subsumption_resolution,[],[f3922,f342]) ).

fof(f4693,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | ~ v1_funct_1(sK4)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2)
      | ~ v2_orders_2(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(superposition,[],[f2621,f661]) ).

fof(f4697,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2)
      | ~ v2_orders_2(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f4693,f359]) ).

fof(f4699,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2)
      | ~ v3_orders_2(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f4697,f348]) ).

fof(f4701,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2)
      | ~ v4_orders_2(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f4699,f347]) ).

fof(f4703,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2)
      | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f4701,f346]) ).

fof(f4705,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4703,f342]) ).

fof(f4707,plain,
    ! [X0] :
      ( ~ v1_funct_2(sK4,sF35,sF29)
      | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4705,f667]) ).

fof(f4709,plain,
    ! [X0] :
      ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4707,f668]) ).

fof(f4711,plain,
    ! [X0] :
      ( ~ m2_relset_1(X0,sF29,sF35)
      | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4709,f667]) ).

fof(f4713,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF29,sF35)
      | ~ m2_relset_1(X0,sF29,sF35)
      | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4711,f667]) ).

fof(f4715,plain,
    ! [X0] :
      ( ~ m2_relset_1(sK4,sF35,sF29)
      | ~ v1_funct_2(X0,sF29,sF35)
      | ~ m2_relset_1(X0,sF29,sF35)
      | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f4713,f667]) ).

fof(f4717,plain,
    ! [X0] :
      ( ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
      | ~ m2_relset_1(X0,sF29,sF35)
      | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
      | ~ v1_funct_2(X0,sF29,sF35)
      | ~ v1_funct_1(X0)
      | v3_struct_0(sK3)
      | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f4715,f669]) ).

fof(f10259,plain,
    ( v1_funct_1(sF30)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,sF35,sF29)
    | ~ m1_relset_1(sK4,sF35,sF29) ),
    inference(superposition,[],[f3924,f655]) ).

fof(f10260,plain,
    ( v1_funct_1(sF30)
    | ~ v1_funct_2(sK4,sF35,sF29)
    | ~ m1_relset_1(sK4,sF35,sF29) ),
    inference(forward_subsumption_resolution,[],[f10259,f359]) ).

fof(f10261,plain,
    ( v1_funct_1(sF30)
    | ~ m1_relset_1(sK4,sF35,sF29) ),
    inference(forward_subsumption_resolution,[],[f10260,f668]) ).

fof(f10262,plain,
    v1_funct_1(sF30),
    inference(forward_subsumption_resolution,[],[f10261,f991]) ).

fof(f13076,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK3)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ v2_orders_2(sK2)
    | ~ v3_orders_2(sK2)
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(resolution,[],[f4717,f650]) ).

fof(f13077,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK3)
    | v3_struct_0(sK2)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13076]) ).

fof(f13080,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | v3_struct_0(sK2)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13077,f422]) ).

fof(f13083,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_lattice3(sK2)
    | ~ v3_lattice3(sK3)
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13080,f422]) ).

fof(f13086,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v3_lattice3(sK3)
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13083,f343]) ).

fof(f13089,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v17_waybel_0(sK4,sK2,sK3)
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13086,f350]) ).

fof(f13092,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_1(sK4)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13089,f357]) ).

fof(f13094,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13092,f359]) ).

fof(f13096,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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)
    | ~ 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,[],[f13094,f355]) ).

fof(f13098,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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,[],[f13096,f354]) ).

fof(f13100,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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,[],[f13098,f353]) ).

fof(f13102,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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,[],[f13100,f352]) ).

fof(f13104,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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,[],[f13102,f351]) ).

fof(f13106,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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) ),
    inference(forward_subsumption_resolution,[],[f13104,f349]) ).

fof(f13108,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,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) ),
    inference(forward_subsumption_resolution,[],[f13106,f348]) ).

fof(f13111,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v4_orders_2(sK2)
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13108,f347]) ).

fof(f13113,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v1_lattice3(sK2)
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13111,f346]) ).

fof(f13116,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ v2_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13113,f345]) ).

fof(f13118,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ l1_orders_2(sK2) ),
    inference(forward_subsumption_resolution,[],[f13116,f344]) ).

fof(f13120,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13118,f342]) ).

fof(f13122,plain,
    ( ~ m2_relset_1(sF30,sF29,sF35)
    | r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13120,f655]) ).

fof(f13124,plain,
    ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13122,f2285]) ).

fof(f13126,plain,
    ( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,sF30,sK5),sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13124,f655]) ).

fof(f13128,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13126,f657]) ).

fof(f13129,plain,
    ( ~ v1_funct_2(sF30,sF29,sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13128,f655]) ).

fof(f13130,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13129,f2336]) ).

fof(f13131,plain,
    ( ~ v1_funct_1(sF30)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13130,f655]) ).

fof(f13132,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13131,f10262]) ).

fof(f13133,plain,
    ( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13132,f667]) ).

fof(f13134,plain,
    ( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13133,f653]) ).

fof(f13135,plain,
    ( ~ v1_funct_2(sF30,sF29,sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13134,f655]) ).

fof(f13136,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13135,f2336]) ).

fof(f13137,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13136,f667]) ).

fof(f13138,plain,
    ( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13137,f653]) ).

fof(f13139,plain,
    ( ~ m2_relset_1(sF30,sF29,sF35)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13138,f655]) ).

fof(f13140,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13139,f2285]) ).

fof(f13141,plain,
    ( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13140,f653]) ).

fof(f13142,plain,
    ( ~ v1_funct_2(sK4,sF35,sF29)
    | r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_demodulation,[],[f13141,f667]) ).

fof(f13143,plain,
    ( r3_waybel_1(sK2,sF31,sF33)
    | ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
    inference(forward_subsumption_resolution,[],[f13142,f668]) ).

fof(f13144,plain,
    ( ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
    | r3_waybel_1(sK2,sF31,sF33) ),
    inference(forward_demodulation,[],[f13143,f653]) ).

fof(f13145,plain,
    ( ~ m2_relset_1(sK4,sF35,sF29)
    | r3_waybel_1(sK2,sF31,sF33) ),
    inference(forward_demodulation,[],[f13144,f667]) ).

fof(f13146,plain,
    r3_waybel_1(sK2,sF31,sF33),
    inference(forward_subsumption_resolution,[],[f13145,f669]) ).

fof(f13147,plain,
    ( sF31 = k2_yellow_0(sK2,sF33)
    | ~ m1_subset_1(sF31,u1_struct_0(sK2))
    | v3_struct_0(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(resolution,[],[f13146,f487]) ).

fof(f13152,plain,
    ( sF31 = k2_yellow_0(sK2,sF33)
    | ~ m1_subset_1(sF31,u1_struct_0(sK2))
    | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f13147,f342]) ).

fof(f13155,plain,
    ( sF31 = sF34
    | ~ m1_subset_1(sF31,u1_struct_0(sK2))
    | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f13152,f663]) ).

fof(f13157,plain,
    ( ~ m1_subset_1(sF31,u1_struct_0(sK2))
    | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f13155,f664]) ).

fof(f13158,plain,
    ( ~ m1_subset_1(sF31,sF35)
    | v3_struct_0(sK2) ),
    inference(forward_demodulation,[],[f13157,f667]) ).

fof(f13159,plain,
    ( v3_struct_0(sK2)
    | v1_xboole_0(sF29)
    | v3_struct_0(sK2)
    | ~ v1_funct_1(sF30) ),
    inference(resolution,[],[f13158,f3156]) ).

fof(f13160,plain,
    ( v3_struct_0(sK2)
    | v1_xboole_0(sF29)
    | ~ v1_funct_1(sF30) ),
    inference(duplicate_literal_removal,[],[f13159]) ).

fof(f13161,plain,
    ( v1_xboole_0(sF29)
    | v3_struct_0(sK2) ),
    inference(forward_subsumption_resolution,[],[f13160,f10262]) ).

fof(f13166,plain,
    ( v3_struct_0(sK3)
    | v3_struct_0(sK2) ),
    inference(resolution,[],[f13161,f762]) ).

fof(f13179,plain,
    ( v3_struct_0(sK2)
    | ~ v1_lattice3(sK3)
    | ~ l1_orders_2(sK3) ),
    inference(resolution,[],[f13166,f422]) ).

fof(f13180,plain,
    ( v3_struct_0(sK2)
    | ~ l1_orders_2(sK3) ),
    inference(forward_subsumption_resolution,[],[f13179,f352]) ).

fof(f13182,plain,
    v3_struct_0(sK2),
    inference(forward_subsumption_resolution,[],[f13180,f349]) ).

fof(f13188,plain,
    ( ~ v1_lattice3(sK2)
    | ~ l1_orders_2(sK2) ),
    inference(resolution,[],[f13182,f422]) ).

fof(f13189,plain,
    ~ l1_orders_2(sK2),
    inference(forward_subsumption_resolution,[],[f13188,f345]) ).

fof(f13191,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f13189,f342]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LAT352+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42  % Computer : n020.cluster.edu
% 0.12/0.42  % Model    : x86_64 x86_64
% 0.12/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.42  % Memory   : 8046.5625MB
% 0.12/0.42  % OS       : Linux 6.8.0-71-generic
% 0.12/0.42  % CPULimit : 300
% 0.12/0.42  % WCLimit  : 300
% 0.12/0.42  % DateTime : Sun Sep 27 14:56:34 UTC 2026
% 0.12/0.43  % CPUTime  : 
% 0.12/0.43  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.45  Running first-order model finding
% 0.12/0.45  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.07/2.60  % (3466401)Will run a generic schedule for satisfiability detection.
% 15.07/2.60  % (3466409)dis+10_1_sil=32000:sp=arity:random_seed=3701112405:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.07/2.60  % (3466407)% WARNING: option uhcvi not known.
% 15.07/2.60  % (3466406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=190317862_2999 on theBenchmark for (2999ds/0Mi)
% 15.07/2.60  % (3466407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3898579787:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.07/2.60  % (3466408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=892621373:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.07/2.60  % (3466410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1282153166:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.07/2.60  % (3466411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2576128430:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.07/2.60  % (3466412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3099621016:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.07/2.60  % TRYING [1]
% 15.07/2.60  % (3466409)Instruction limit reached! 
% 15.07/2.60  % (3466409)------------------------------
% 15.07/2.60  % (3466409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.07/2.60  % (3466409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.07/2.60  % (3466409)CaDiCaL version: 2.1.3
% 15.07/2.60  % (3466409)Termination reason: Instruction limit
% 15.07/2.60  % (3466409)Termination phase: Saturation
% 15.07/2.60  % (3466409)Time elapsed: 0.034 s
% 15.07/2.60  % (3466409)Peak memory usage: 13 MB
% 15.07/2.60  % (3466409)Instructions burned: 106 (million)
% 15.07/2.60  % TRYING [2]
% 15.07/2.60  % TRYING [3]
% 15.07/2.60  % (3466420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3422250813:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.07/2.60  % TRYING [1]
% 15.07/2.60  % TRYING [2]
% 15.07/2.60  % TRYING [3]
% 15.07/2.60  % (3466410)Instruction limit reached! 
% 15.07/2.60  % (3466410)------------------------------
% 15.07/2.60  % (3466410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.07/2.60  % (3466410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.07/2.60  % (3466410)CaDiCaL version: 2.1.3
% 15.07/2.60  % (3466410)Termination reason: Instruction limit
% 15.07/2.60  % (3466410)Termination phase: Saturation
% 15.07/2.60  % (3466410)Time elapsed: 0.065 s
% 15.07/2.60  % (3466410)Peak memory usage: 13 MB
% 15.07/2.60  % (3466410)Instructions burned: 116 (million)
% 15.07/2.60  % (3466411)Instruction limit reached! 
% 15.07/2.60  % (3466411)------------------------------
% 15.07/2.60  % (3466411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.07/2.60  % (3466411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.07/2.60  % (3466411)CaDiCaL version: 2.1.3
% 15.07/2.60  % (3466411)Termination reason: Instruction limit
% 15.07/2.60  % (3466411)Termination phase: Saturation
% 15.07/2.60  % (3466411)Time elapsed: 0.069 s
% 15.07/2.60  % (3466411)Peak memory usage: 13 MB
% 15.07/2.60  % (3466411)Instructions burned: 133 (million)
% 15.07/2.60  % (3466422)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1163681234:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.07/2.60  % (3466423)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=793245707:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.07/2.60  % (3466412)Instruction limit reached! 
% 15.07/2.60  % (3466412)------------------------------
% 15.07/2.60  % (3466412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.07/2.60  % (3466412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.07/2.60  % (3466412)CaDiCaL version: 2.1.3
% 15.07/2.60  % (3466412)Termination reason: Instruction limit
% 15.07/2.60  % (3466412)Termination phase: Saturation
% 15.07/2.60  % (3466412)Time elapsed: 0.100 s
% 15.07/2.60  % (3466412)Peak memory usage: 15 MB
% 15.07/2.60  % (3466412)Instructions burned: 159 (million)
% 15.07/2.60  % TRYING [4]
% 15.07/2.60  % (3466426)ott-21_1_sil=16000:fs=off:random_seed=4248815672:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.07/2.60  % TRYING [4]
% 15.07/2.60  % (3466422)Instruction limit reached! 
% 15.07/2.60  % (3466422)------------------------------
% 15.07/2.60  % (3466422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.07/2.60  % (3466422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466422)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466422)Termination reason: Instruction limit
% 21.30/4.55  % (3466422)Termination phase: Saturation
% 21.30/4.55  % (3466422)Time elapsed: 0.077 s
% 21.30/4.55  % (3466422)Peak memory usage: 14 MB
% 21.30/4.55  % (3466422)Instructions burned: 133 (million)
% 21.30/4.55  % (3466428)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3956889715:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 21.30/4.55  % (3466420)Instruction limit reached! 
% 21.30/4.55  % (3466420)------------------------------
% 21.30/4.55  % (3466420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466420)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466420)Termination reason: Instruction limit
% 21.30/4.55  % (3466420)Termination phase: Finite model building SAT solving
% 21.30/4.55  % (3466420)Time elapsed: 0.173 s
% 21.30/4.55  % (3466420)Peak memory usage: 33 MB
% 21.30/4.55  % (3466420)Instructions burned: 715 (million)
% 21.30/4.55  % (3466426)Instruction limit reached! 
% 21.30/4.55  % (3466426)------------------------------
% 21.30/4.55  % (3466426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466426)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466426)Termination reason: Instruction limit
% 21.30/4.55  % (3466426)Termination phase: Saturation
% 21.30/4.55  % (3466426)Time elapsed: 0.091 s
% 21.30/4.55  % (3466426)Peak memory usage: 13 MB
% 21.30/4.55  % (3466426)Instructions burned: 181 (million)
% 21.30/4.55  % (3466431)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=405649140:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 21.30/4.55  % (3466430)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1078408187:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 21.30/4.55  % TRYING [1]
% 21.30/4.55  % TRYING [2]
% 21.30/4.55  % TRYING [3]
% 21.30/4.55  % (3466428)Instruction limit reached! 
% 21.30/4.55  % (3466428)------------------------------
% 21.30/4.55  % (3466428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466428)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466428)Termination reason: Instruction limit
% 21.30/4.55  % (3466428)Termination phase: Saturation
% 21.30/4.55  % (3466428)Time elapsed: 0.299 s
% 21.30/4.55  % (3466428)Peak memory usage: 15 MB
% 21.30/4.55  % (3466428)Instructions burned: 478 (million)
% 21.30/4.55  % (3466434)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1324422546:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 21.30/4.55  % (3466423)Instruction limit reached! 
% 21.30/4.55  % (3466423)------------------------------
% 21.30/4.55  % (3466423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466423)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466423)Termination reason: Instruction limit
% 21.30/4.55  % (3466423)Termination phase: Saturation
% 21.30/4.55  % (3466423)Time elapsed: 0.426 s
% 21.30/4.55  % (3466423)Peak memory usage: 19 MB
% 21.30/4.55  % (3466423)Instructions burned: 685 (million)
% 21.30/4.55  % (3466436)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=1048315886:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 21.30/4.55  % TRYING [4]
% 21.30/4.55  % (3466430)Instruction limit reached! 
% 21.30/4.55  % (3466430)------------------------------
% 21.30/4.55  % (3466430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466430)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466430)Termination reason: Instruction limit
% 21.30/4.55  % (3466430)Termination phase: Finite model building constraint generation
% 21.30/4.55  % (3466430)Time elapsed: 0.336 s
% 21.30/4.55  % (3466430)Peak memory usage: 22 MB
% 21.30/4.55  % (3466430)Instructions burned: 869 (million)
% 21.30/4.55  % (3466438)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4253332819:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 21.30/4.55  % (3466431)Instruction limit reached! 
% 21.30/4.55  % (3466431)------------------------------
% 21.30/4.55  % (3466431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466431)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466431)Termination reason: Instruction limit
% 21.30/4.55  % (3466431)Termination phase: Saturation
% 21.30/4.55  % (3466431)Time elapsed: 0.370 s
% 21.30/4.55  % (3466431)Peak memory usage: 26 MB
% 21.30/4.55  % (3466431)Instructions burned: 1180 (million)
% 21.30/4.55  % (3466440)fmb+10_1_sil=64000:random_seed=4205348117:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 21.30/4.55  % TRYING [1]
% 21.30/4.55  % TRYING [2]
% 21.30/4.55  % TRYING [3]
% 21.30/4.55  % TRYING [4]
% 21.30/4.55  % TRYING [5]
% 21.30/4.55  % (3466434)Instruction limit reached! 
% 21.30/4.55  % (3466434)------------------------------
% 21.30/4.55  % (3466434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466434)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466434)Termination reason: Instruction limit
% 21.30/4.55  % (3466434)Termination phase: Finite model building constraint generation
% 21.30/4.55  % (3466434)Time elapsed: 0.410 s
% 21.30/4.55  % (3466434)Peak memory usage: 104 MB
% 21.30/4.55  % (3466434)Instructions burned: 891 (million)
% 21.30/4.55  % (3466436)Instruction limit reached! 
% 21.30/4.55  % (3466436)------------------------------
% 21.30/4.55  % (3466436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466436)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466436)Termination reason: Instruction limit
% 21.30/4.55  % (3466436)Termination phase: Saturation
% 21.30/4.55  % (3466436)Time elapsed: 0.404 s
% 21.30/4.55  % (3466436)Peak memory usage: 21 MB
% 21.30/4.55  % (3466436)Instructions burned: 693 (million)
% 21.30/4.55  % (3466442)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2635414156:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 21.30/4.55  % (3466443)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3342011005:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 21.30/4.55  % TRYING [20]
% 21.30/4.55  % TRYING [8]
% 21.30/4.55  % TRYING [5]
% 21.30/4.55  % (3466438)Instruction limit reached! 
% 21.30/4.55  % (3466438)------------------------------
% 21.30/4.55  % (3466438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466438)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466438)Termination reason: Instruction limit
% 21.30/4.55  % (3466438)Termination phase: Saturation
% 21.30/4.55  % (3466438)Time elapsed: 0.502 s
% 21.30/4.55  % (3466438)Peak memory usage: 20 MB
% 21.30/4.55  % (3466438)Instructions burned: 880 (million)
% 21.30/4.55  % (3466446)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4294104621:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 21.30/4.55  % (3466443)Instruction limit reached! 
% 21.30/4.55  % (3466443)------------------------------
% 21.30/4.55  % (3466443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466443)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466443)Termination reason: Instruction limit
% 21.30/4.55  % (3466443)Termination phase: Finite model building constraint generation
% 21.30/4.55  % (3466443)Time elapsed: 0.298 s
% 21.30/4.55  % (3466443)Peak memory usage: 53 MB
% 21.30/4.55  % (3466443)Instructions burned: 922 (million)
% 21.30/4.55  % (3466448)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3412267828:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 21.30/4.55  % (3466448)Instruction limit reached! 
% 21.30/4.55  % (3466448)------------------------------
% 21.30/4.55  % (3466448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466448)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466448)Termination reason: Instruction limit
% 21.30/4.55  % (3466448)Termination phase: Saturation
% 21.30/4.55  % (3466448)Time elapsed: 0.760 s
% 21.30/4.55  % (3466448)Peak memory usage: 26 MB
% 21.30/4.55  % (3466448)Instructions burned: 1473 (million)
% 21.30/4.55  % (3466450)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1971439663:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 21.30/4.55  % (3466450)Cannot represent all propositional literals internally
% 21.30/4.55  % (3466450)Refutation not found, incomplete strategy
% 21.30/4.55  % (3466450)------------------------------
% 21.30/4.55  % (3466450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466450)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466450)Termination reason: Refutation not found, incomplete strategy
% 21.30/4.55  % (3466450)Time elapsed: 0.026 s
% 21.30/4.55  % (3466450)Peak memory usage: 12 MB
% 21.30/4.55  % (3466450)Instructions burned: 54 (million)
% 21.30/4.55  % (3466450)------------------------------
% 21.30/4.55  % (3466450)------------------------------
% 21.30/4.55  % (3466452)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3582739104:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 21.30/4.55  % TRYING [16]
% 21.30/4.55  % TRYING [6]
% 21.30/4.55  % (3466452)Instruction limit reached! 
% 21.30/4.55  % (3466452)------------------------------
% 21.30/4.55  % (3466452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466452)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466452)Termination reason: Instruction limit
% 21.30/4.55  % (3466452)Termination phase: Finite model building constraint generation
% 21.30/4.55  % (3466452)Time elapsed: 0.763 s
% 21.30/4.55  % (3466452)Peak memory usage: 119 MB
% 21.30/4.55  % (3466452)Instructions burned: 2174 (million)
% 21.30/4.55  % (3466454)ott-2_1_sil=16000:newcnf=on:random_seed=2925308825:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 21.30/4.55  % (3466454)Instruction limit reached! 
% 21.30/4.55  % (3466454)------------------------------
% 21.30/4.55  % (3466454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466454)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466454)Termination reason: Instruction limit
% 21.30/4.55  % (3466454)Termination phase: Saturation
% 21.30/4.55  % (3466454)Time elapsed: 0.562 s
% 21.30/4.55  % (3466454)Peak memory usage: 19 MB
% 21.30/4.55  % (3466454)Instructions burned: 869 (million)
% 21.30/4.55  % (3466456)ott+10_1_sil=32000:tgt=ground:random_seed=2428084956:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 21.30/4.55  % (3466446)Instruction limit reached! 
% 21.30/4.55  % (3466446)------------------------------
% 21.30/4.55  % (3466446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466446)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466446)Termination reason: Instruction limit
% 21.30/4.55  % (3466446)Termination phase: Saturation
% 21.30/4.55  % (3466446)Time elapsed: 2.773 s
% 21.30/4.55  % (3466446)Peak memory usage: 38 MB
% 21.30/4.55  % (3466446)Instructions burned: 5133 (million)
% 21.30/4.55  % (3466458)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4244321955:i=54282_2960 on theBenchmark for (2960ds/54282Mi)
% 21.30/4.55  % TRYING [1]
% 21.30/4.55  % TRYING [2]
% 21.30/4.55  % TRYING [3]
% 21.30/4.55  % (3466456) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3466401-3466456"...
% 21.30/4.55  % (3466456)...printing done.
% 21.30/4.55  % (3466456)Refutation found. Thanks to Tanya!
% 21.30/4.55  % SZS status Theorem for theBenchmark
% 21.30/4.55  % SZS output start Proof for theBenchmark
% See solution above
% 21.30/4.55  % (3466456)------------------------------
% 21.30/4.55  % (3466456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.30/4.55  % (3466456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.30/4.55  % (3466456)CaDiCaL version: 2.1.3
% 21.30/4.55  % (3466456)Termination reason: Refutation
% 21.30/4.55  % (3466456)Time elapsed: 0.460 s
% 21.30/4.55  % (3466456)Peak memory usage: 19 MB
% 21.30/4.55  % (3466456)Instructions burned: 831 (million)
% 21.30/4.55  % (3466401)Success in time 4.09 s
% 21.30/4.55  % Vampire exiting
%------------------------------------------------------------------------------