Vampire---5.0.1.THM-Ref.s

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

% Computer : n003.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:47:13 AM UTC 2026

% Result   : Theorem 71.59s 17.74s
% Output   : Refutation 112.97s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   68
%            Number of leaves      :   24
% Syntax   : Number of formulae    :  283 (  56 unt;  14 def)
%            Number of atoms       : 2245 (  39 equ)
%            Maximal formula atoms :   27 (   7 avg)
%            Number of connectives : 3590 (1628   ~;1735   |; 184   &)
%                                         (  17 <=>;  26  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   29 (   9 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of predicates  :   32 (  30 usr;   8 prp; 0-3 aty)
%            Number of functors    :   20 (  20 usr;  11 con; 0-4 aty)
%            Number of variables   :  230 (   0 sgn 219   !;  11   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1394,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(f7885,axiom,
    ! [X0] :
      ( l1_orders_2(X0)
     => l1_struct_0(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).

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

fof(f15209,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(f15254,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(f15265,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(f16826,axiom,
    ! [X0] :
      ( ( ~ v3_struct_0(X0)
        & v2_orders_2(X0)
        & v3_orders_2(X0)
        & v1_lattice3(X0)
        & l1_orders_2(X0) )
     => ( ~ v1_xboole_0(u1_struct_0(X0))
        & v1_waybel_0(u1_struct_0(X0),X0)
        & v12_waybel_0(u1_struct_0(X0),X0)
        & m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_waybel13) ).

fof(f18893,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(f18906,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(f18912,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(f18913,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)],[f18912]) ).

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

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

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

fof(f40672,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,[],[f15209]) ).

fof(f40673,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,[],[f40672]) ).

fof(f40751,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,[],[f15254]) ).

fof(f40752,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,[],[f40751]) ).

fof(f40771,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,[],[f15265]) ).

fof(f40772,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,[],[f40771]) ).

fof(f43645,plain,
    ! [X0] :
      ( ( ~ v1_xboole_0(u1_struct_0(X0))
        & v1_waybel_0(u1_struct_0(X0),X0)
        & v12_waybel_0(u1_struct_0(X0),X0)
        & m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(ennf_transformation,[],[f16826]) ).

fof(f43646,plain,
    ! [X0] :
      ( ( ~ v1_xboole_0(u1_struct_0(X0))
        & v1_waybel_0(u1_struct_0(X0),X0)
        & v12_waybel_0(u1_struct_0(X0),X0)
        & m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(flattening,[],[f43645]) ).

fof(f47387,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,[],[f18893]) ).

fof(f47388,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,[],[f47387]) ).

fof(f47405,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,[],[f18906]) ).

fof(f47406,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,[],[f47405]) ).

fof(f47417,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,[],[f18913]) ).

fof(f47418,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,[],[f47417]) ).

fof(f50040,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,[],[f1394]) ).

fof(f58574,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,[],[f40752]) ).

fof(f58575,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,[],[f58574]) ).

fof(f58601,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,[],[f40772]) ).

fof(f58602,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,[],[f58601]) ).

fof(f58603,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,[],[f58602]) ).

fof(f58604,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,sK6405(X0,X1,X2,X3)),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,sK6405(X0,X1,X2,X3))))
                        & m1_subset_1(sK6405(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,[sK6405]),skolemize(X4,sK6405(X0,X1,X2,X3))],[f58603]) ).

fof(f62294,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,[],[f47406]) ).

fof(f62300,plain,
    ( k7_yellow_2(u1_struct_0(sK8408),sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410) != k2_yellow_0(sK8407,k5_pre_topc(sK8407,sK8408,sK8409,k7_waybel_0(sK8408,sK8410)))
    & m1_subset_1(sK8410,u1_struct_0(sK8408))
    & v1_funct_1(sK8409)
    & v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    & v17_waybel_0(sK8409,sK8407,sK8408)
    & m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    & v2_orders_2(sK8408)
    & v3_orders_2(sK8408)
    & v4_orders_2(sK8408)
    & v1_lattice3(sK8408)
    & v2_lattice3(sK8408)
    & v3_lattice3(sK8408)
    & l1_orders_2(sK8408)
    & v2_orders_2(sK8407)
    & v3_orders_2(sK8407)
    & v4_orders_2(sK8407)
    & v1_lattice3(sK8407)
    & v2_lattice3(sK8407)
    & v3_lattice3(sK8407)
    & l1_orders_2(sK8407) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK8407,sK8408,sK8409,sK8410]),skolemize(X0,sK8407),skolemize(X1,sK8408),skolemize(X2,sK8409),skolemize(X3,sK8410)],[f47418]) ).

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

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

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

fof(f95490,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,[],[f40673]) ).

fof(f95763,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,[],[f58575]) ).

fof(f95822,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,[],[f58604]) ).

fof(f100844,plain,
    ! [X0] :
      ( ~ v1_xboole_0(u1_struct_0(X0))
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v1_lattice3(X0)
      | ~ l1_orders_2(X0) ),
    inference(cnf_transformation,[],[f43646]) ).

fof(f109170,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,[],[f47388]) ).

fof(f109171,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,[],[f47388]) ).

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

fof(f109224,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,[],[f62294]) ).

fof(f109256,plain,
    l1_orders_2(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109257,plain,
    v3_lattice3(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109258,plain,
    v2_lattice3(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109259,plain,
    v1_lattice3(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109260,plain,
    v4_orders_2(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109261,plain,
    v3_orders_2(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109262,plain,
    v2_orders_2(sK8407),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109263,plain,
    l1_orders_2(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109264,plain,
    v3_lattice3(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109265,plain,
    v2_lattice3(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109266,plain,
    v1_lattice3(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109267,plain,
    v4_orders_2(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109268,plain,
    v3_orders_2(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109269,plain,
    v2_orders_2(sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109270,plain,
    m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109271,plain,
    v17_waybel_0(sK8409,sK8407,sK8408),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109272,plain,
    v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109273,plain,
    v1_funct_1(sK8409),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109274,plain,
    m1_subset_1(sK8410,u1_struct_0(sK8408)),
    inference(cnf_transformation,[],[f62300]) ).

fof(f109275,plain,
    k7_yellow_2(u1_struct_0(sK8408),sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410) != k2_yellow_0(sK8407,k5_pre_topc(sK8407,sK8408,sK8409,k7_waybel_0(sK8408,sK8410))),
    inference(cnf_transformation,[],[f62300]) ).

fof(f128415,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,[],[f109224]) ).

fof(f128417,definition,
    sF8411 = u1_struct_0(sK8408),
    introduced(definition,[new_symbols(definition,[sF8411])],[function_definition]) ).

fof(f128418,plain,
    u1_struct_0(sK8408) = sF8411,
    inference(reorient_equations,[],[f128417]) ).

fof(f128419,definition,
    sF8412 = k1_waybel34(sK8407,sK8408,sK8409),
    introduced(definition,[new_symbols(definition,[sF8412])],[function_definition]) ).

fof(f128420,plain,
    k1_waybel34(sK8407,sK8408,sK8409) = sF8412,
    inference(reorient_equations,[],[f128419]) ).

fof(f128421,definition,
    sF8413 = k7_yellow_2(sF8411,sK8407,sF8412,sK8410),
    introduced(definition,[new_symbols(definition,[sF8413])],[function_definition]) ).

fof(f128422,plain,
    k7_yellow_2(sF8411,sK8407,sF8412,sK8410) = sF8413,
    inference(reorient_equations,[],[f128421]) ).

fof(f128423,definition,
    sF8414 = k7_waybel_0(sK8408,sK8410),
    introduced(definition,[new_symbols(definition,[sF8414])],[function_definition]) ).

fof(f128424,plain,
    k7_waybel_0(sK8408,sK8410) = sF8414,
    inference(reorient_equations,[],[f128423]) ).

fof(f128425,definition,
    sF8415 = k5_pre_topc(sK8407,sK8408,sK8409,sF8414),
    introduced(definition,[new_symbols(definition,[sF8415])],[function_definition]) ).

fof(f128426,plain,
    k5_pre_topc(sK8407,sK8408,sK8409,sF8414) = sF8415,
    inference(reorient_equations,[],[f128425]) ).

fof(f128427,definition,
    sF8416 = k2_yellow_0(sK8407,sF8415),
    introduced(definition,[new_symbols(definition,[sF8416])],[function_definition]) ).

fof(f128428,plain,
    k2_yellow_0(sK8407,sF8415) = sF8416,
    inference(reorient_equations,[],[f128427]) ).

fof(f128429,plain,
    sF8413 != sF8416,
    inference(definition_folding,[],[f109275,f128428,f128426,f128424,f128422,f128420,f128418]) ).

fof(f128430,plain,
    m1_subset_1(sK8410,sF8411),
    inference(definition_folding,[],[f109274,f128418]) ).

fof(f128431,definition,
    sF8417 = u1_struct_0(sK8407),
    introduced(definition,[new_symbols(definition,[sF8417])],[function_definition]) ).

fof(f128432,plain,
    u1_struct_0(sK8407) = sF8417,
    inference(reorient_equations,[],[f128431]) ).

fof(f128433,plain,
    v1_funct_2(sK8409,sF8417,sF8411),
    inference(definition_folding,[],[f109272,f128418,f128432]) ).

fof(f128434,plain,
    m2_relset_1(sK8409,sF8417,sF8411),
    inference(definition_folding,[],[f109270,f128418,f128432]) ).

fof(f147112,plain,
    ( ~ v3_struct_0(sK8407)
    | ~ l1_orders_2(sK8407) ),
    inference(resolution,[],[f84944,f109259]) ).

fof(f147113,plain,
    ( ~ v3_struct_0(sK8408)
    | ~ l1_orders_2(sK8408) ),
    inference(resolution,[],[f84944,f109266]) ).

fof(f147114,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(superposition,[],[f109170,f128420]) ).

fof(f147125,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(superposition,[],[f109171,f128420]) ).

fof(f147131,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | v1_xboole_0(sF8411)
    | v3_struct_0(sK8407)
    | ~ l1_struct_0(sK8407)
    | ~ v1_funct_1(sF8412)
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_subset_1(sK8410,sF8411) ),
    inference(superposition,[],[f95490,f128422]) ).

fof(f147139,plain,
    l1_struct_0(sK8407),
    inference(resolution,[],[f77297,f109256]) ).

fof(f147144,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ 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(sK8408)
      | ~ v3_orders_2(sK8408)
      | ~ v4_orders_2(sK8408)
      | ~ v1_lattice3(sK8408)
      | ~ v2_lattice3(sK8408)
      | ~ l1_orders_2(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(superposition,[],[f109172,f128418]) ).

fof(f147166,definition,
    ( spl8418_2245
  <=> m1_relset_1(sK8409,sF8417,sF8411) ),
    introduced(definition,[new_symbols(definition,[spl8418_2245])],[avatar_definition]) ).

fof(f147167,plain,
    ( m1_relset_1(sK8409,sF8417,sF8411)
    | ~ spl8418_2245 ),
    inference(avatar_component_clause,[],[f147166]) ).

fof(f147168,plain,
    ( ~ m1_relset_1(sK8409,sF8417,sF8411)
    | spl8418_2245 ),
    inference(avatar_component_clause,[],[f147166]) ).

fof(f147190,plain,
    m1_relset_1(sK8409,sF8417,sF8411),
    inference(resolution,[],[f64334,f128434]) ).

fof(f147192,plain,
    ( $false
    | spl8418_2245 ),
    inference(forward_subsumption_resolution,[],[f147190,f147168]) ).

fof(f147193,plain,
    spl8418_2245,
    inference(avatar_contradiction_clause,[],[f147192]) ).

fof(f147229,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8408),X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | ~ v2_orders_2(sK8408)
      | ~ v3_orders_2(sK8408)
      | ~ v4_orders_2(sK8408)
      | ~ l1_orders_2(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(superposition,[],[f95822,f128424]) ).

fof(f147263,plain,
    ( ~ v1_xboole_0(sF8411)
    | v3_struct_0(sK8408)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ l1_orders_2(sK8408) ),
    inference(superposition,[],[f100844,f128418]) ).

fof(f147896,definition,
    ( spl8418_2273
  <=> v1_funct_2(sF8412,sF8411,sF8417) ),
    introduced(definition,[new_symbols(definition,[spl8418_2273])],[avatar_definition]) ).

fof(f147898,plain,
    ( v1_funct_2(sF8412,sF8411,sF8417)
    | ~ spl8418_2273 ),
    inference(avatar_component_clause,[],[f147896]) ).

fof(f148025,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f147114,f109262]) ).

fof(f148032,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f147125,f109262]) ).

fof(f148035,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ 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(sK8408)
      | ~ v4_orders_2(sK8408)
      | ~ v1_lattice3(sK8408)
      | ~ v2_lattice3(sK8408)
      | ~ l1_orders_2(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f147144,f109269]) ).

fof(f148719,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148025,f109261]) ).

fof(f148728,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148032,f109261]) ).

fof(f148731,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ 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(sK8408)
      | ~ v1_lattice3(sK8408)
      | ~ v2_lattice3(sK8408)
      | ~ l1_orders_2(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f148035,f109268]) ).

fof(f148815,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148719,f109260]) ).

fof(f148820,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148728,f109260]) ).

fof(f148823,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v1_lattice3(sK8408)
      | ~ v2_lattice3(sK8408)
      | ~ l1_orders_2(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f148731,f109267]) ).

fof(f148879,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148815,f109259]) ).

fof(f148884,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148820,f109259]) ).

fof(f148887,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ v2_orders_2(X1)
      | ~ v3_orders_2(X1)
      | ~ v4_orders_2(X1)
      | ~ v1_lattice3(X1)
      | ~ v2_lattice3(X1)
      | ~ l1_orders_2(X1)
      | ~ v2_lattice3(sK8408)
      | ~ l1_orders_2(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f148823,f109266]) ).

fof(f148940,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148879,f109258]) ).

fof(f148945,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ l1_orders_2(sK8407)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148884,f109258]) ).

fof(f148948,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ 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(sK8408)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f148887,f109265]) ).

fof(f148995,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148940,f109256]) ).

fof(f149000,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148945,f109256]) ).

fof(f149003,plain,
    ! [X0,X1] :
      ( ~ v1_funct_2(X0,u1_struct_0(X1),sF8411)
      | ~ 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_1(k1_waybel34(X1,sK8408,X0))
      | ~ m1_relset_1(X0,u1_struct_0(X1),sF8411) ),
    inference(forward_subsumption_resolution,[],[f148948,f109263]) ).

fof(f149039,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f148995,f109269]) ).

fof(f149040,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149000,f109269]) ).

fof(f149074,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149039,f109268]) ).

fof(f149075,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149040,f109268]) ).

fof(f149083,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149074,f109267]) ).

fof(f149084,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149075,f109267]) ).

fof(f149090,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149083,f109266]) ).

fof(f149091,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149084,f109266]) ).

fof(f149096,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149090,f109265]) ).

fof(f149097,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ l1_orders_2(sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149091,f109265]) ).

fof(f149102,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149096,f109263]) ).

fof(f149103,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149097,f109263]) ).

fof(f149108,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149102,f109273]) ).

fof(f149109,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149103,f109273]) ).

fof(f149114,plain,
    ( m2_relset_1(sF8412,u1_struct_0(sK8408),sF8417)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149108,f128432]) ).

fof(f149115,plain,
    ( v1_funct_2(sF8412,u1_struct_0(sK8408),sF8417)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149109,f128432]) ).

fof(f149120,plain,
    ( m2_relset_1(sF8412,sF8411,sF8417)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149114,f128418]) ).

fof(f149121,plain,
    ( v1_funct_2(sF8412,sF8411,sF8417)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149115,f128418]) ).

fof(f149126,plain,
    ( ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411)
    | m2_relset_1(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149120,f128418]) ).

fof(f149127,plain,
    ( ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411)
    | v1_funct_2(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149121,f128418]) ).

fof(f149132,plain,
    ( ~ v1_funct_2(sK8409,sF8417,sF8411)
    | m2_relset_1(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149126,f128432]) ).

fof(f149133,plain,
    ( ~ v1_funct_2(sK8409,sF8417,sF8411)
    | v1_funct_2(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_demodulation,[],[f149127,f128432]) ).

fof(f149138,plain,
    ( m2_relset_1(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149132,f128433]) ).

fof(f149139,plain,
    ( v1_funct_2(sF8412,sF8411,sF8417)
    | ~ m1_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408)) ),
    inference(forward_subsumption_resolution,[],[f149133,f128433]) ).

fof(f149144,plain,
    ( ~ m1_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
    | m2_relset_1(sF8412,sF8411,sF8417) ),
    inference(forward_demodulation,[],[f149138,f128418]) ).

fof(f149145,plain,
    ( ~ m1_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
    | v1_funct_2(sF8412,sF8411,sF8417) ),
    inference(forward_demodulation,[],[f149139,f128418]) ).

fof(f149150,plain,
    ( ~ m1_relset_1(sK8409,sF8417,sF8411)
    | m2_relset_1(sF8412,sF8411,sF8417) ),
    inference(forward_demodulation,[],[f149144,f128432]) ).

fof(f149151,plain,
    ( ~ m1_relset_1(sK8409,sF8417,sF8411)
    | v1_funct_2(sF8412,sF8411,sF8417) ),
    inference(forward_demodulation,[],[f149145,f128432]) ).

fof(f149156,plain,
    ( m2_relset_1(sF8412,sF8411,sF8417)
    | ~ spl8418_2245 ),
    inference(forward_subsumption_resolution,[],[f149150,f147167]) ).

fof(f149157,plain,
    ( v1_funct_2(sF8412,sF8411,sF8417)
    | ~ spl8418_2245 ),
    inference(forward_subsumption_resolution,[],[f149151,f147167]) ).

fof(f149162,plain,
    ( spl8418_2273
    | ~ spl8418_2245 ),
    inference(avatar_split_clause,[],[f149157,f147166,f147896]) ).

fof(f149171,definition,
    ( spl8418_2418
  <=> v1_funct_1(sF8412) ),
    introduced(definition,[new_symbols(definition,[spl8418_2418])],[avatar_definition]) ).

fof(f149172,plain,
    ( v1_funct_1(sF8412)
    | ~ spl8418_2418 ),
    inference(avatar_component_clause,[],[f149171]) ).

fof(f149173,plain,
    ( ~ v1_funct_1(sF8412)
    | spl8418_2418 ),
    inference(avatar_component_clause,[],[f149171]) ).

fof(f149188,definition,
    ( spl8418_2420
  <=> v3_struct_0(sK8407) ),
    introduced(definition,[new_symbols(definition,[spl8418_2420])],[avatar_definition]) ).

fof(f149189,plain,
    ( ~ v3_struct_0(sK8407)
    | spl8418_2420 ),
    inference(avatar_component_clause,[],[f149188]) ).

fof(f149196,definition,
    ( spl8418_2422
  <=> v3_struct_0(sK8408) ),
    introduced(definition,[new_symbols(definition,[spl8418_2422])],[avatar_definition]) ).

fof(f149206,plain,
    ( ~ v1_xboole_0(sF8411)
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ l1_orders_2(sK8408) ),
    inference(forward_subsumption_resolution,[],[f147263,f84944]) ).

fof(f149224,definition,
    ( spl8418_2424
  <=> v1_xboole_0(sF8411) ),
    introduced(definition,[new_symbols(definition,[spl8418_2424])],[avatar_definition]) ).

fof(f149225,plain,
    ( ~ v1_xboole_0(sF8411)
    | spl8418_2424 ),
    inference(avatar_component_clause,[],[f149224]) ).

fof(f149351,plain,
    ~ v3_struct_0(sK8408),
    inference(forward_subsumption_resolution,[],[f147113,f109263]) ).

fof(f149352,plain,
    ~ v3_struct_0(sK8407),
    inference(forward_subsumption_resolution,[],[f147112,f109256]) ).

fof(f149358,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8408),X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | ~ v3_orders_2(sK8408)
      | ~ v4_orders_2(sK8408)
      | ~ l1_orders_2(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f147229,f109269]) ).

fof(f149399,plain,
    ( ~ v1_xboole_0(sF8411)
    | ~ v3_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ l1_orders_2(sK8408) ),
    inference(forward_subsumption_resolution,[],[f149206,f109269]) ).

fof(f149629,plain,
    ~ spl8418_2422,
    inference(avatar_split_clause,[],[f149351,f149196]) ).

fof(f149630,plain,
    ~ spl8418_2420,
    inference(avatar_split_clause,[],[f149352,f149188]) ).

fof(f149634,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8408),X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | ~ v4_orders_2(sK8408)
      | ~ l1_orders_2(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f149358,f109268]) ).

fof(f149661,plain,
    ( ~ v1_xboole_0(sF8411)
    | ~ v1_lattice3(sK8408)
    | ~ l1_orders_2(sK8408) ),
    inference(forward_subsumption_resolution,[],[f149399,f109268]) ).

fof(f149776,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8408),X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | ~ l1_orders_2(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f149634,f109267]) ).

fof(f149785,plain,
    ( ~ v1_xboole_0(sF8411)
    | ~ l1_orders_2(sK8408) ),
    inference(forward_subsumption_resolution,[],[f149661,f109266]) ).

fof(f149883,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8408),X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f149776,f109263]) ).

fof(f149887,plain,
    ~ v1_xboole_0(sF8411),
    inference(forward_subsumption_resolution,[],[f149785,f109263]) ).

fof(f150032,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ m1_subset_1(sK8410,u1_struct_0(sK8408))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f149883,f128418]) ).

fof(f150042,plain,
    ~ spl8418_2424,
    inference(avatar_split_clause,[],[f149887,f149224]) ).

fof(f150115,plain,
    ! [X2,X0,X1] :
      ( ~ m1_subset_1(sK8410,sF8411)
      | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f150032,f128418]) ).

fof(f150139,plain,
    ! [X2,X0,X1] :
      ( r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_2(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_subsumption_resolution,[],[f150115,f128430]) ).

fof(f150145,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ m2_relset_1(X1,u1_struct_0(sK8408),u1_struct_0(X0))
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f150139,f128418]) ).

fof(f150151,plain,
    ! [X2,X0,X1] :
      ( ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f150145,f128418]) ).

fof(f150164,plain,
    ! [X2,X0,X1] :
      ( ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
      | ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8408))
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f150151,f128418]) ).

fof(f150168,plain,
    ! [X2,X0,X1] :
      ( ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
      | ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
      | ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
      | ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
      | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
      | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
      | ~ v1_funct_1(X1)
      | ~ v1_funct_1(X2)
      | v3_struct_0(sK8408)
      | v3_struct_0(X0)
      | ~ v2_orders_2(X0)
      | ~ v3_orders_2(X0)
      | ~ v4_orders_2(X0)
      | ~ l1_orders_2(X0) ),
    inference(forward_demodulation,[],[f150164,f128418]) ).

fof(f150173,definition,
    ( spl8418_2550
  <=> ! [X2,X0,X1] :
        ( ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
        | ~ l1_orders_2(X0)
        | ~ v4_orders_2(X0)
        | ~ v3_orders_2(X0)
        | ~ v2_orders_2(X0)
        | v3_struct_0(X0)
        | ~ v1_funct_1(X2)
        | ~ v1_funct_1(X1)
        | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
        | r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
        | ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
        | ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
        | ~ v1_funct_2(X2,u1_struct_0(X0),sF8411) ) ),
    introduced(definition,[new_symbols(definition,[spl8418_2550])],[avatar_definition]) ).

fof(f150174,plain,
    ( ! [X2,X0,X1] :
        ( r3_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8408,X2,sF8414))
        | ~ l1_orders_2(X0)
        | ~ v4_orders_2(X0)
        | ~ v3_orders_2(X0)
        | ~ v2_orders_2(X0)
        | v3_struct_0(X0)
        | ~ v1_funct_1(X2)
        | ~ v1_funct_1(X1)
        | ~ v3_waybel_1(k1_waybel_1(X0,sK8408,X2,X1),X0,sK8408)
        | ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
        | ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
        | ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
        | ~ v1_funct_2(X2,u1_struct_0(X0),sF8411) )
    | ~ spl8418_2550 ),
    inference(avatar_component_clause,[],[f150173]) ).

fof(f150175,plain,
    ( spl8418_2422
    | spl8418_2550 ),
    inference(avatar_split_clause,[],[f150168,f150173,f149196]) ).

fof(f150222,plain,
    ( m1_relset_1(sF8412,sF8411,sF8417)
    | ~ spl8418_2245 ),
    inference(resolution,[],[f149156,f64334]) ).

fof(f150342,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ l1_orders_2(sK8407)
        | ~ v4_orders_2(sK8407)
        | ~ v3_orders_2(sK8407)
        | ~ v2_orders_2(sK8407)
        | v3_struct_0(sK8407)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | ~ spl8418_2550 ),
    inference(superposition,[],[f150174,f128426]) ).

fof(f150346,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v4_orders_2(sK8407)
        | ~ v3_orders_2(sK8407)
        | ~ v2_orders_2(sK8407)
        | v3_struct_0(sK8407)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150342,f109256]) ).

fof(f150348,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v3_orders_2(sK8407)
        | ~ v2_orders_2(sK8407)
        | v3_struct_0(sK8407)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150346,f109260]) ).

fof(f150350,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v2_orders_2(sK8407)
        | v3_struct_0(sK8407)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150348,f109261]) ).

fof(f150352,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | v3_struct_0(sK8407)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150350,f109262]) ).

fof(f150354,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(sK8409)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150352,f149189]) ).

fof(f150356,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150354,f109273]) ).

fof(f150358,plain,
    ( ! [X0] :
        ( ~ m2_relset_1(sK8409,sF8417,sF8411)
        | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150356,f128432]) ).

fof(f150360,plain,
    ( ! [X0] :
        ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8407))
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150358,f128434]) ).

fof(f150362,plain,
    ( ! [X0] :
        ( ~ v1_funct_2(X0,sF8411,sF8417)
        | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8407))
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150360,f128432]) ).

fof(f150364,plain,
    ( ! [X0] :
        ( ~ m2_relset_1(X0,sF8411,sF8417)
        | ~ v1_funct_2(X0,sF8411,sF8417)
        | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150362,f128432]) ).

fof(f150366,plain,
    ( ! [X0] :
        ( ~ v1_funct_2(sK8409,sF8417,sF8411)
        | ~ m2_relset_1(X0,sF8411,sF8417)
        | ~ v1_funct_2(X0,sF8411,sF8417)
        | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150364,f128432]) ).

fof(f150368,plain,
    ( ! [X0] :
        ( ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,sK8409,X0),sK8407,sK8408)
        | ~ v1_funct_2(X0,sF8411,sF8417)
        | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,X0,sK8410),sF8415)
        | ~ v1_funct_1(X0)
        | ~ m2_relset_1(X0,sF8411,sF8417) )
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150366,f128433]) ).

fof(f150371,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_lattice3(sK8407)
    | ~ v3_lattice3(sK8408)
    | ~ v17_waybel_0(sK8409,sK8407,sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(resolution,[],[f150368,f128415]) ).

fof(f150373,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_lattice3(sK8407)
    | ~ v3_lattice3(sK8408)
    | ~ v17_waybel_0(sK8409,sK8407,sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(duplicate_literal_removal,[],[f150371]) ).

fof(f150374,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v3_lattice3(sK8408)
    | ~ v17_waybel_0(sK8409,sK8407,sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150373,f109257]) ).

fof(f150375,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v17_waybel_0(sK8409,sK8407,sK8408)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150374,f109264]) ).

fof(f150376,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150375,f109271]) ).

fof(f150377,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8408)
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150376,f109273]) ).

fof(f150378,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v3_orders_2(sK8408)
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150377,f109269]) ).

fof(f150379,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v4_orders_2(sK8408)
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150378,f109268]) ).

fof(f150380,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v1_lattice3(sK8408)
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150379,f109267]) ).

fof(f150381,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_lattice3(sK8408)
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150380,f109266]) ).

fof(f150382,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ l1_orders_2(sK8408)
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150381,f109265]) ).

fof(f150383,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_orders_2(sK8407)
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150382,f109263]) ).

fof(f150384,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v3_orders_2(sK8407)
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150383,f109262]) ).

fof(f150385,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v4_orders_2(sK8407)
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150384,f109261]) ).

fof(f150386,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v1_lattice3(sK8407)
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150385,f109260]) ).

fof(f150387,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ v2_lattice3(sK8407)
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150386,f109259]) ).

fof(f150388,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ l1_orders_2(sK8407)
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150387,f109258]) ).

fof(f150389,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150388,f109256]) ).

fof(f150390,plain,
    ( ~ v1_funct_2(sF8412,sF8411,sF8417)
    | r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150389,f128420]) ).

fof(f150391,plain,
    ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,k1_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150390,f147898]) ).

fof(f150392,plain,
    ( r3_waybel_1(sK8407,k7_yellow_2(sF8411,sK8407,sF8412,sK8410),sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150391,f128420]) ).

fof(f150393,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_1(k1_waybel34(sK8407,sK8408,sK8409))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150392,f128422]) ).

fof(f150394,plain,
    ( ~ v1_funct_1(sF8412)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150393,f128420]) ).

fof(f150590,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ v2_orders_2(sK8407)
      | ~ v3_orders_2(sK8407)
      | ~ v4_orders_2(sK8407)
      | ~ v1_lattice3(sK8407)
      | ~ v2_lattice3(sK8407)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(superposition,[],[f149003,f128432]) ).

fof(f150593,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ v3_orders_2(sK8407)
      | ~ v4_orders_2(sK8407)
      | ~ v1_lattice3(sK8407)
      | ~ v2_lattice3(sK8407)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150590,f109262]) ).

fof(f150595,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ v4_orders_2(sK8407)
      | ~ v1_lattice3(sK8407)
      | ~ v2_lattice3(sK8407)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150593,f109261]) ).

fof(f150597,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ v1_lattice3(sK8407)
      | ~ v2_lattice3(sK8407)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150595,f109260]) ).

fof(f150599,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ v2_lattice3(sK8407)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150597,f109259]) ).

fof(f150601,plain,
    ! [X0] :
      ( ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ l1_orders_2(sK8407)
      | ~ v1_funct_1(X0)
      | v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150599,f109258]) ).

fof(f150603,plain,
    ! [X0] :
      ( v1_funct_1(k1_waybel34(sK8407,sK8408,X0))
      | ~ v1_funct_1(X0)
      | ~ v1_funct_2(X0,sF8417,sF8411)
      | ~ m1_relset_1(X0,sF8417,sF8411) ),
    inference(forward_subsumption_resolution,[],[f150601,f109256]) ).

fof(f150605,plain,
    ( v1_funct_1(sF8412)
    | ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,sF8417,sF8411)
    | ~ m1_relset_1(sK8409,sF8417,sF8411) ),
    inference(superposition,[],[f150603,f128420]) ).

fof(f150606,plain,
    ( ~ v1_funct_1(sK8409)
    | ~ v1_funct_2(sK8409,sF8417,sF8411)
    | ~ m1_relset_1(sK8409,sF8417,sF8411)
    | spl8418_2418 ),
    inference(forward_subsumption_resolution,[],[f150605,f149173]) ).

fof(f150607,plain,
    ( ~ v1_funct_2(sK8409,sF8417,sF8411)
    | ~ m1_relset_1(sK8409,sF8417,sF8411)
    | spl8418_2418 ),
    inference(forward_subsumption_resolution,[],[f150606,f109273]) ).

fof(f150608,plain,
    ( ~ m1_relset_1(sK8409,sF8417,sF8411)
    | spl8418_2418 ),
    inference(forward_subsumption_resolution,[],[f150607,f128433]) ).

fof(f150609,plain,
    ( $false
    | ~ spl8418_2245
    | spl8418_2418 ),
    inference(forward_subsumption_resolution,[],[f150608,f147167]) ).

fof(f150610,plain,
    ( ~ spl8418_2245
    | spl8418_2418 ),
    inference(avatar_contradiction_clause,[],[f150609]) ).

fof(f150611,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | v3_struct_0(sK8407)
    | ~ l1_struct_0(sK8407)
    | ~ v1_funct_1(sF8412)
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_subset_1(sK8410,sF8411)
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f147131,f149225]) ).

fof(f150613,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150394,f149172]) ).

fof(f150617,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ l1_struct_0(sK8407)
    | ~ v1_funct_1(sF8412)
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_subset_1(sK8410,sF8411)
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150611,f149189]) ).

fof(f150619,plain,
    ( ~ m2_relset_1(sF8412,sF8411,sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150613,f128420]) ).

fof(f150623,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ v1_funct_1(sF8412)
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_subset_1(sK8410,sF8411)
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150617,f147139]) ).

fof(f150625,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150619,f149156]) ).

fof(f150628,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_subset_1(sK8410,sF8411)
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150623,f149172]) ).

fof(f150630,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150625,f128432]) ).

fof(f150631,plain,
    ( m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150628,f128430]) ).

fof(f150633,plain,
    ( ~ v1_funct_2(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150630,f128418]) ).

fof(f150634,plain,
    ( m1_subset_1(sF8413,sF8417)
    | ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_demodulation,[],[f150631,f128432]) ).

fof(f150636,plain,
    ( ~ v1_funct_2(sF8412,sF8411,sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150633,f128420]) ).

fof(f150637,plain,
    ( ~ v1_funct_2(sF8412,sF8411,sF8417)
    | m1_subset_1(sF8413,sF8417)
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_demodulation,[],[f150634,f128432]) ).

fof(f150639,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),u1_struct_0(sK8407))
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150636,f147898]) ).

fof(f150640,plain,
    ( m1_subset_1(sF8413,sF8417)
    | ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8407))
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150637,f147898]) ).

fof(f150642,plain,
    ( ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8408),sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150639,f128432]) ).

fof(f150643,plain,
    ( ~ m1_relset_1(sF8412,sF8411,sF8417)
    | m1_subset_1(sF8413,sF8417)
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_demodulation,[],[f150640,f128432]) ).

fof(f150645,plain,
    ( ~ m2_relset_1(k1_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150642,f128418]) ).

fof(f150646,plain,
    ( m1_subset_1(sF8413,sF8417)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424 ),
    inference(forward_subsumption_resolution,[],[f150643,f150222]) ).

fof(f150648,plain,
    ( ~ m2_relset_1(sF8412,sF8411,sF8417)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150645,f128420]) ).

fof(f150650,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ v1_funct_2(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150648,f149156]) ).

fof(f150652,plain,
    ( ~ v1_funct_2(sK8409,u1_struct_0(sK8407),sF8411)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150650,f128418]) ).

fof(f150653,plain,
    ( ~ v1_funct_2(sK8409,sF8417,sF8411)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150652,f128432]) ).

fof(f150654,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ m2_relset_1(sK8409,u1_struct_0(sK8407),u1_struct_0(sK8408))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150653,f128433]) ).

fof(f150655,plain,
    ( ~ m2_relset_1(sK8409,u1_struct_0(sK8407),sF8411)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150654,f128418]) ).

fof(f150656,plain,
    ( ~ m2_relset_1(sK8409,sF8417,sF8411)
    | r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150655,f128432]) ).

fof(f150657,plain,
    ( r3_waybel_1(sK8407,sF8413,sF8415)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150656,f128434]) ).

fof(f150664,plain,
    ( sF8413 = k2_yellow_0(sK8407,sF8415)
    | ~ m1_subset_1(sF8413,u1_struct_0(sK8407))
    | v3_struct_0(sK8407)
    | ~ l1_orders_2(sK8407)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(resolution,[],[f150657,f95763]) ).

fof(f150665,plain,
    ( sF8413 = k2_yellow_0(sK8407,sF8415)
    | ~ m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ l1_orders_2(sK8407)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150664,f149189]) ).

fof(f150666,plain,
    ( sF8413 = k2_yellow_0(sK8407,sF8415)
    | ~ m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150665,f109256]) ).

fof(f150667,plain,
    ( sF8413 = sF8416
    | ~ m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150666,f128428]) ).

fof(f150668,plain,
    ( ~ m1_subset_1(sF8413,u1_struct_0(sK8407))
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150667,f128429]) ).

fof(f150669,plain,
    ( ~ m1_subset_1(sF8413,sF8417)
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | ~ spl8418_2550 ),
    inference(forward_demodulation,[],[f150668,f128432]) ).

fof(f150670,plain,
    ( $false
    | ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424
    | ~ spl8418_2550 ),
    inference(forward_subsumption_resolution,[],[f150669,f150646]) ).

fof(f150671,plain,
    ( ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424
    | ~ spl8418_2550 ),
    inference(avatar_contradiction_clause,[],[f150670]) ).

cnf(s1894,plain,
    spl8418_2245,
    inference(sat_conversion,[],[f147193]) ).

cnf(s2063,plain,
    ( ~ spl8418_2245
    | spl8418_2273 ),
    inference(sat_conversion,[],[f149162]) ).

cnf(s2114,plain,
    ~ spl8418_2422,
    inference(sat_conversion,[],[f149629]) ).

cnf(s2115,plain,
    ~ spl8418_2420,
    inference(sat_conversion,[],[f149630]) ).

cnf(s2175,plain,
    ~ spl8418_2424,
    inference(sat_conversion,[],[f150042]) ).

cnf(s2200,plain,
    ( spl8418_2422
    | spl8418_2550 ),
    inference(sat_conversion,[],[f150175]) ).

cnf(s2211,plain,
    ( ~ spl8418_2245
    | spl8418_2418 ),
    inference(sat_conversion,[],[f150610]) ).

cnf(s2212,plain,
    ( ~ spl8418_2245
    | ~ spl8418_2273
    | ~ spl8418_2418
    | spl8418_2420
    | spl8418_2424
    | ~ spl8418_2550 ),
    inference(sat_conversion,[],[f150671]) ).

cnf(s2245,plain,
    spl8418_2550,
    inference(rat,[],[s2200,s2114]) ).

cnf(s2330,plain,
    spl8418_2418,
    inference(rat,[],[s2211,s1894]) ).

cnf(s2334,plain,
    spl8418_2273,
    inference(rat,[],[s2063,s1894]) ).

cnf(s2335,plain,
    $false,
    inference(rat,[],[s2212,s2245,s2175,s2115,s1894,s2330,s2334]) ).

fof(f150672,plain,
    $false,
    inference(avatar_sat_refutation,[],[s2335]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LAT352+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38  % Computer : n003.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Sun Sep 27 14:58:14 UTC 2026
% 0.12/0.38  % CPUTime  : 
% 0.12/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42  Running first-order theorem proving
% 0.12/0.42  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.32/4.10  % (646558)Detected formulas, will run a generic FOF schedule.
% 16.32/4.10  % (646565)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3487271236:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 16.32/4.10  % (646564)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=947425193:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 16.32/4.10  % (646563)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1885692361:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 16.32/4.10  % (646566)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3303159146:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 16.32/4.10  % (646568)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1476800831:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 16.32/4.10  % (646567)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2674250326:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 16.32/4.10  % (646569)dis-21_1_sil=8000:lcm=predicate:random_seed=3017578822:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 16.32/4.10  % (646568)Instruction limit reached! 
% 16.32/4.10  % (646568)------------------------------
% 16.32/4.10  % (646568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/4.10  % (646568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/4.10  % (646568)CaDiCaL version: 2.1.3
% 16.32/4.10  % (646568)Termination reason: Instruction limit
% 16.32/4.10  % (646568)Termination phase: Property scanning
% 16.32/4.10  % (646568)Time elapsed: 0.062 s
% 16.32/4.10  % (646568)Peak memory usage: 112 MB
% 16.32/4.10  % (646568)Instructions burned: 141 (million)
% 16.32/4.10  % (646566)Instruction limit reached! 
% 16.32/4.10  % (646566)------------------------------
% 16.32/4.10  % (646566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/4.10  % (646566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/4.10  % (646566)CaDiCaL version: 2.1.3
% 16.32/4.10  % (646566)Termination reason: Instruction limit
% 16.32/4.10  % (646566)Termination phase: SInE selection
% 16.32/4.10  % (646566)Time elapsed: 0.083 s
% 16.32/4.10  % (646566)Peak memory usage: 112 MB
% 16.32/4.10  % (646566)Instructions burned: 109 (million)
% 16.32/4.10  % (646569)Instruction limit reached! 
% 16.32/4.10  % (646569)------------------------------
% 16.32/4.10  % (646569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/4.10  % (646569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/4.10  % (646569)CaDiCaL version: 2.1.3
% 16.32/4.10  % (646569)Termination reason: Instruction limit
% 16.32/4.10  % (646569)Termination phase: SInE selection
% 16.32/4.10  % (646569)Time elapsed: 0.086 s
% 16.32/4.10  % (646569)Peak memory usage: 112 MB
% 16.32/4.10  % (646569)Instructions burned: 129 (million)
% 16.32/4.10  % (646567)Instruction limit reached! 
% 16.32/4.10  % (646567)------------------------------
% 16.32/4.10  % (646567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/4.10  % (646567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/4.10  % (646567)CaDiCaL version: 2.1.3
% 16.32/4.10  % (646567)Termination reason: Instruction limit
% 16.32/4.10  % (646567)Termination phase: Preprocessing 1
% 16.32/4.10  % (646567)Time elapsed: 0.100 s
% 16.32/4.10  % (646567)Peak memory usage: 112 MB
% 16.32/4.10  % (646567)Instructions burned: 119 (million)
% 16.32/4.10  % (646577)lrs+10_1_sil=8000:sp=occurrence:random_seed=1864561830:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 16.32/4.10  % (646578)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2935494795:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 16.32/4.10  % (646579)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3448989571:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 16.32/4.10  % (646580)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1854371357:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 16.32/4.10  % (646578)Instruction limit reached! 
% 16.32/4.10  % (646578)------------------------------
% 23.41/5.09  % (646578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646578)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646578)Termination reason: Instruction limit
% 23.41/5.09  % (646578)Termination phase: Property scanning
% 23.41/5.09  % (646578)Time elapsed: 0.068 s
% 23.41/5.09  % (646578)Peak memory usage: 112 MB
% 23.41/5.09  % (646578)Instructions burned: 158 (million)
% 23.41/5.09  % (646580)Instruction limit reached! 
% 23.41/5.09  % (646580)------------------------------
% 23.41/5.09  % (646580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646580)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646580)Termination reason: Instruction limit
% 23.41/5.09  % (646580)Termination phase: Property scanning
% 23.41/5.09  % (646580)Time elapsed: 0.108 s
% 23.41/5.09  % (646580)Peak memory usage: 112 MB
% 23.41/5.09  % (646580)Instructions burned: 250 (million)
% 23.41/5.09  % (646577)Instruction limit reached! 
% 23.41/5.09  % (646577)------------------------------
% 23.41/5.09  % (646577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646577)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646577)Termination reason: Instruction limit
% 23.41/5.09  % (646577)Termination phase: Saturation
% 23.41/5.09  % (646577)Time elapsed: 0.197 s
% 23.41/5.09  % (646577)Peak memory usage: 119 MB
% 23.41/5.09  % (646577)Instructions burned: 286 (million)
% 23.41/5.09  % (646579)Instruction limit reached! 
% 23.41/5.09  % (646579)------------------------------
% 23.41/5.09  % (646579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646579)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646579)Termination reason: Instruction limit
% 23.41/5.09  % (646579)Termination phase: Saturation
% 23.41/5.09  % (646579)Time elapsed: 0.233 s
% 23.41/5.09  % (646579)Peak memory usage: 119 MB
% 23.41/5.09  % (646579)Instructions burned: 325 (million)
% 23.41/5.09  % (646585)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2055425428:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.41/5.09  % (646586)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=33595915:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 23.41/5.09  % (646587)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3889797310:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 23.41/5.09  % (646589)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3176824438:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 23.41/5.09  % (646587)Instruction limit reached! 
% 23.41/5.09  % (646587)------------------------------
% 23.41/5.09  % (646587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646587)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646587)Termination reason: Instruction limit
% 23.41/5.09  % (646587)Termination phase: SInE selection
% 23.41/5.09  % (646587)Time elapsed: 0.089 s
% 23.41/5.09  % (646587)Peak memory usage: 112 MB
% 23.41/5.09  % (646587)Instructions burned: 114 (million)
% 23.41/5.09  % (646585)Instruction limit reached! 
% 23.41/5.09  % (646585)------------------------------
% 23.41/5.09  % (646585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646585)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646585)Termination reason: Instruction limit
% 23.41/5.09  % (646585)Termination phase: Preprocessing 3
% 23.41/5.09  % (646585)Time elapsed: 0.223 s
% 23.41/5.09  % (646585)Peak memory usage: 119 MB
% 23.41/5.09  % (646585)Instructions burned: 295 (million)
% 23.41/5.09  % (646589)Instruction limit reached! 
% 23.41/5.09  % (646589)------------------------------
% 23.41/5.09  % (646589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.41/5.09  % (646589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.41/5.09  % (646589)CaDiCaL version: 2.1.3
% 23.41/5.09  % (646589)Termination reason: Instruction limit
% 23.41/5.09  % (646589)Termination phase: Preprocessing 1
% 23.41/5.09  % (646589)Time elapsed: 0.089 s
% 62.21/10.51  % (646589)Peak memory usage: 112 MB
% 62.21/10.51  % (646589)Instructions burned: 128 (million)
% 62.21/10.51  % (646593)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4279933253:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 62.21/10.51  % (646594)lrs+10_1_sil=8000:sp=occurrence:random_seed=3535882583:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 62.21/10.51  % (646595)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3235397260:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 62.21/10.51  % (646593)Instruction limit reached! 
% 62.21/10.51  % (646593)------------------------------
% 62.21/10.51  % (646593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/10.51  % (646593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/10.51  % (646593)CaDiCaL version: 2.1.3
% 62.21/10.51  % (646593)Termination reason: Instruction limit
% 62.21/10.51  % (646593)Termination phase: Property scanning
% 62.21/10.51  % (646593)Time elapsed: 0.051 s
% 62.21/10.51  % (646593)Peak memory usage: 112 MB
% 62.21/10.51  % (646593)Instructions burned: 115 (million)
% 62.21/10.51  % (646599)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1496376011:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 62.21/10.51  % (646595)Instruction limit reached! 
% 62.21/10.51  % (646595)------------------------------
% 62.21/10.51  % (646595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/10.51  % (646595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/10.51  % (646595)CaDiCaL version: 2.1.3
% 62.21/10.51  % (646595)Termination reason: Instruction limit
% 62.21/10.51  % (646595)Termination phase: Saturation
% 62.21/10.51  % (646595)Time elapsed: 0.257 s
% 62.21/10.51  % (646595)Peak memory usage: 118 MB
% 62.21/10.51  % (646595)Instructions burned: 438 (million)
% 62.21/10.51  % (646601)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1160150927:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 62.21/10.51  % (646594)Instruction limit reached! 
% 62.21/10.51  % (646594)------------------------------
% 62.21/10.51  % (646594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/10.51  % (646594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/10.51  % (646594)CaDiCaL version: 2.1.3
% 62.21/10.51  % (646594)Termination reason: Instruction limit
% 62.21/10.51  % (646594)Termination phase: Saturation
% 62.21/10.51  % (646594)Time elapsed: 0.537 s
% 62.21/10.51  % (646594)Peak memory usage: 132 MB
% 62.21/10.51  % (646594)Instructions burned: 908 (million)
% 62.21/10.51  % (646601)Instruction limit reached! 
% 62.21/10.51  % (646601)------------------------------
% 62.21/10.51  % (646601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/10.51  % (646601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/10.51  % (646601)CaDiCaL version: 2.1.3
% 62.21/10.51  % (646601)Termination reason: Instruction limit
% 62.21/10.51  % (646601)Termination phase: NewCNF
% 62.21/10.51  % (646601)Time elapsed: 0.117 s
% 62.21/10.51  % (646601)Peak memory usage: 115 MB
% 62.21/10.51  % (646601)Instructions burned: 134 (million)
% 62.21/10.51  % (646603)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2350813577:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 62.21/10.51  % (646604)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3896508258:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 62.21/10.51  % (646586)Instruction limit reached! 
% 62.21/10.51  % (646586)------------------------------
% 62.21/10.51  % (646586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/10.51  % (646586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/10.51  % (646586)CaDiCaL version: 2.1.3
% 62.21/10.51  % (646586)Termination reason: Instruction limit
% 62.21/10.51  % (646586)Termination phase: Property scanning
% 62.21/10.51  % (646586)Time elapsed: 1.234 s
% 62.21/10.51  % (646586)Peak memory usage: 170 MB
% 62.21/10.51  % (646586)Instructions burned: 2352 (million)
% 62.21/10.51  % (646607)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2747568065:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 62.21/10.51  % (646607)Instruction limit reached! 
% 62.21/10.51  % (646607)------------------------------
% 95.09/15.19  % (646607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646607)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646607)Termination reason: Instruction limit
% 95.09/15.19  % (646607)Termination phase: Property scanning
% 95.09/15.19  % (646607)Time elapsed: 0.054 s
% 95.09/15.19  % (646607)Peak memory usage: 112 MB
% 95.09/15.19  % (646607)Instructions burned: 125 (million)
% 95.09/15.19  % (646603)Instruction limit reached! 
% 95.09/15.19  % (646603)------------------------------
% 95.09/15.19  % (646603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646603)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646603)Termination reason: Instruction limit
% 95.09/15.19  % (646603)Termination phase: Preprocessing 3
% 95.09/15.19  % (646603)Time elapsed: 0.443 s
% 95.09/15.19  % (646603)Peak memory usage: 134 MB
% 95.09/15.19  % (646603)Instructions burned: 592 (million)
% 95.09/15.19  % (646609)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2833665724:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 95.09/15.19  % (646610)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=307710961:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 95.09/15.19  % (646609)Instruction limit reached! 
% 95.09/15.19  % (646609)------------------------------
% 95.09/15.19  % (646609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646609)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646609)Termination reason: Instruction limit
% 95.09/15.19  % (646609)Termination phase: Property scanning
% 95.09/15.19  % (646609)Time elapsed: 0.058 s
% 95.09/15.19  % (646609)Peak memory usage: 112 MB
% 95.09/15.19  % (646609)Instructions burned: 135 (million)
% 95.09/15.19  % (646610)Refutation not found, incomplete strategy
% 95.09/15.19  % (646610)------------------------------
% 95.09/15.19  % (646610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646610)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646610)Termination reason: Refutation not found, incomplete strategy
% 95.09/15.19  % (646610)Time elapsed: 0.120 s
% 95.09/15.19  % (646610)Peak memory usage: 117 MB
% 95.09/15.19  % (646610)Instructions burned: 139 (million)
% 95.09/15.19  % (646613)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2523033019:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 95.09/15.19  % (646610)------------------------------
% 95.09/15.19  % (646610)------------------------------
% 95.09/15.19  % (646613)Instruction limit reached! 
% 95.09/15.19  % (646613)------------------------------
% 95.09/15.19  % (646613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646613)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646613)Termination reason: Instruction limit
% 95.09/15.19  % (646613)Termination phase: Saturation
% 95.09/15.19  % (646613)Time elapsed: 0.297 s
% 95.09/15.19  % (646613)Peak memory usage: 121 MB
% 95.09/15.19  % (646613)Instructions burned: 432 (million)
% 95.09/15.19  % (646615)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1409557822:i=6060:aac=none:ins=25_2961 on theBenchmark for (2961ds/6060Mi)
% 95.09/15.19  % (646616)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=60469985:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 95.09/15.19  % (646616)Instruction limit reached! 
% 95.09/15.19  % (646616)------------------------------
% 95.09/15.19  % (646616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.09/15.19  % (646616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.09/15.19  % (646616)CaDiCaL version: 2.1.3
% 95.09/15.19  % (646616)Termination reason: Instruction limit
% 95.09/15.19  % (646616)Termination phase: Preprocessing 1
% 95.09/15.19  % (646616)Time elapsed: 0.124 s
% 95.09/15.19  % (646616)Peak memory usage: 113 MB
% 95.09/15.19  % (646616)Instructions burned: 151 (million)
% 71.59/17.74  % (646619)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2853489312:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 71.59/17.74  % (646599)Instruction limit reached! 
% 71.59/17.74  % (646599)------------------------------
% 71.59/17.74  % (646599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646599)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646599)Termination reason: Instruction limit
% 71.59/17.74  % (646599)Termination phase: Saturation
% 71.59/17.74  % (646599)Time elapsed: 3.028 s
% 71.59/17.74  % (646599)Peak memory usage: 243 MB
% 71.59/17.74  % (646599)Instructions burned: 5203 (million)
% 71.59/17.74  % (646621)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1973771837:i=667:av=off:fsr=off_2946 on theBenchmark for (2946ds/667Mi)
% 71.59/17.74  % (646621)Instruction limit reached! 
% 71.59/17.74  % (646621)------------------------------
% 71.59/17.74  % (646621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646621)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646621)Termination reason: Instruction limit
% 71.59/17.74  % (646621)Termination phase: NewCNF
% 71.59/17.74  % (646621)Time elapsed: 0.508 s
% 71.59/17.74  % (646621)Peak memory usage: 148 MB
% 71.59/17.74  % (646621)Instructions burned: 668 (million)
% 71.59/17.74  % (646623)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2219320074:s2a=on:i=185:s2at=1.8:fdi=4_2939 on theBenchmark for (2939ds/185Mi)
% 71.59/17.74  % (646623)Instruction limit reached! 
% 71.59/17.74  % (646623)------------------------------
% 71.59/17.74  % (646623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646623)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646623)Termination reason: Instruction limit
% 71.59/17.74  % (646623)Termination phase: SInE selection
% 71.59/17.74  % (646623)Time elapsed: 0.153 s
% 71.59/17.74  % (646623)Peak memory usage: 113 MB
% 71.59/17.74  % (646623)Instructions burned: 185 (million)
% 71.59/17.74  % (646625)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4265105519:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2936 on theBenchmark for (2936ds/193Mi)
% 71.59/17.74  % (646625)Instruction limit reached! 
% 71.59/17.74  % (646625)------------------------------
% 71.59/17.74  % (646625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646625)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646625)Termination reason: Instruction limit
% 71.59/17.74  % (646625)Termination phase: SInE selection
% 71.59/17.74  % (646625)Time elapsed: 0.157 s
% 71.59/17.74  % (646625)Peak memory usage: 112 MB
% 71.59/17.74  % (646625)Instructions burned: 193 (million)
% 71.59/17.74  % (646627)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3969424971:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2933 on theBenchmark for (2933ds/4850Mi)
% 71.59/17.74  % (646615)Instruction limit reached! 
% 71.59/17.74  % (646615)------------------------------
% 71.59/17.74  % (646615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646615)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646615)Termination reason: Instruction limit
% 71.59/17.74  % (646615)Termination phase: Saturation
% 71.59/17.74  % (646615)Time elapsed: 4.516 s
% 71.59/17.74  % (646615)Peak memory usage: 508 MB
% 71.59/17.74  % (646615)Instructions burned: 6062 (million)
% 71.59/17.74  % (646629)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4002912542:i=12111:sd=1:ss=included_2914 on theBenchmark for (2914ds/12111Mi)
% 71.59/17.74  % (646627)Instruction limit reached! 
% 71.59/17.74  % (646627)------------------------------
% 71.59/17.74  % (646627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646627)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646627)Termination reason: Instruction limit
% 71.59/17.74  % (646627)Termination phase: Saturation
% 71.59/17.74  % (646627)Time elapsed: 2.781 s
% 71.59/17.74  % (646627)Peak memory usage: 213 MB
% 71.59/17.74  % (646627)Instructions burned: 4851 (million)
% 71.59/17.74  % (646631)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=395282868:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 71.59/17.74  % (646631)Instruction limit reached! 
% 71.59/17.74  % (646631)------------------------------
% 71.59/17.74  % (646631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646631)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646631)Termination reason: Instruction limit
% 71.59/17.74  % (646631)Termination phase: Naming
% 71.59/17.74  % (646631)Time elapsed: 0.249 s
% 71.59/17.74  % (646631)Peak memory usage: 135 MB
% 71.59/17.74  % (646631)Instructions burned: 319 (million)
% 71.59/17.74  % (646633)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3703680570:i=2064:ep=RST_2899 on theBenchmark for (2899ds/2064Mi)
% 71.59/17.74  % (646604)Instruction limit reached! 
% 71.59/17.74  % (646604)------------------------------
% 71.59/17.74  % (646604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646604)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646604)Termination reason: Instruction limit
% 71.59/17.74  % (646604)Termination phase: Saturation
% 71.59/17.74  % (646604)Time elapsed: 7.653 s
% 71.59/17.74  % (646604)Peak memory usage: 315 MB
% 71.59/17.74  % (646604)Instructions burned: 13193 (million)
% 71.59/17.74  % (646635)dis-1011_128_sil=32000:random_seed=3716353384:i=3706:ep=RST:av=off_2894 on theBenchmark for (2894ds/3706Mi)
% 71.59/17.74  % (646633)Instruction limit reached! 
% 71.59/17.74  % (646633)------------------------------
% 71.59/17.74  % (646633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646633)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646633)Termination reason: Instruction limit
% 71.59/17.74  % (646633)Termination phase: Property scanning
% 71.59/17.74  % (646633)Time elapsed: 1.086 s
% 71.59/17.74  % (646633)Peak memory usage: 170 MB
% 71.59/17.74  % (646633)Instructions burned: 2064 (million)
% 71.59/17.74  % (646637)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3163519889:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2886 on theBenchmark for (2886ds/757Mi)
% 71.59/17.74  % (646637)Instruction limit reached! 
% 71.59/17.74  % (646637)------------------------------
% 71.59/17.74  % (646637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646637)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646637)Termination reason: Instruction limit
% 71.59/17.74  % (646637)Termination phase: Saturation
% 71.59/17.74  % (646637)Time elapsed: 0.557 s
% 71.59/17.74  % (646637)Peak memory usage: 129 MB
% 71.59/17.74  % (646637)Instructions burned: 757 (million)
% 71.59/17.74  % (646639)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4200108012:i=13913:ss=axioms:sgt=8_2879 on theBenchmark for (2879ds/13913Mi)
% 71.59/17.74  % (646635)Instruction limit reached! 
% 71.59/17.74  % (646635)------------------------------
% 71.59/17.74  % (646635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646635)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646635)Termination reason: Instruction limit
% 71.59/17.74  % (646635)Termination phase: Saturation
% 71.59/17.74  % (646635)Time elapsed: 1.885 s
% 71.59/17.74  % (646635)Peak memory usage: 186 MB
% 71.59/17.74  % (646635)Instructions burned: 3707 (million)
% 71.59/17.74  % (646641)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=141397101:i=9925:aac=none_2874 on theBenchmark for (2874ds/9925Mi)
% 71.59/17.74  % (646619)Instruction limit reached! 
% 71.59/17.74  % (646619)------------------------------
% 71.59/17.74  % (646619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646619)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646619)Termination reason: Instruction limit
% 71.59/17.74  % (646619)Termination phase: Saturation
% 71.59/17.74  % (646619)Time elapsed: 9.925 s
% 71.59/17.74  % (646619)Peak memory usage: 684 MB
% 71.59/17.74  % (646619)Instructions burned: 14155 (million)
% 71.59/17.74  % (646643)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3143288532:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2856 on theBenchmark for (2856ds/2479Mi)
% 71.59/17.74  % (646563)First to succeed.
% 71.59/17.74  % (646563)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-646558"
% 71.59/17.74  % (646643)Instruction limit reached! 
% 71.59/17.74  % (646643)------------------------------
% 71.59/17.74  % (646643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646643)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646643)Termination reason: Instruction limit
% 71.59/17.74  % (646643)Termination phase: Saturation
% 71.59/17.74  % (646643)Time elapsed: 2.066 s
% 71.59/17.74  % (646643)Peak memory usage: 134 MB
% 71.59/17.74  % (646643)Instructions burned: 2480 (million)
% 71.59/17.74  % (646629)Instruction limit reached! 
% 71.59/17.74  % (646629)------------------------------
% 71.59/17.74  % (646629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.59/17.74  % (646629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.59/17.74  % (646629)CaDiCaL version: 2.1.3
% 71.59/17.74  % (646629)Termination reason: Instruction limit
% 71.59/17.74  % (646629)Termination phase: Saturation
% 71.59/17.74  % (646629)Time elapsed: 8.064 s
% 71.59/17.74  % (646629)Peak memory usage: 241 MB
% 71.59/17.74  % (646629)Instructions burned: 12111 (million)
% 71.59/17.74  % (646645)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2442639141:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2833 on theBenchmark for (2833ds/440Mi)
% 71.59/17.74  % (646563)Refutation found. Thanks to Tanya!
% 71.59/17.74  % SZS status Theorem for theBenchmark
% 71.59/17.74  % SZS output start Proof for theBenchmark
% See solution above
% 112.97/17.92  % (646563)------------------------------
% 112.97/17.92  % (646563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.97/17.92  % (646563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.97/17.92  % (646563)CaDiCaL version: 2.1.3
% 112.97/17.92  % (646563)Termination reason: Refutation
% 112.97/17.92  % (646563)Time elapsed: 15.256 s
% 112.97/17.92  % (646563)Peak memory usage: 740 MB
% 112.97/17.92  % (646563)Instructions burned: 24899 (million)
% 112.97/17.92  % (646563)------------------------------
% 112.97/17.92  % (646563)------------------------------
% 112.97/17.92  % (646558)Success in time 16.874 s
% 112.97/17.92  % Vampire exiting
%------------------------------------------------------------------------------