Prover9---2026-6A.THM-CRf.s

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : SEU357+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p

% 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 : Sun Sep 27 08:45:54 AM UTC 2026

% Result   : Theorem 0.73s 0.56s
% Output   : CNFRefutation 0.73s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(d8_yellow_0,axiom,
    ! [A] :
      ( rel_str(A)
     => ! [B] :
          ( ex_inf_of_relstr_set(A,B)
        <=> ? [C] :
              ( ! [D] :
                  ( element(D,the_carrier(A))
                 => ( ( ! [E] :
                          ( element(E,the_carrier(A))
                         => ( relstr_element_smaller(A,B,E)
                           => related(A,E,D) ) )
                      & relstr_element_smaller(A,B,D) )
                   => D = C ) )
              & ! [D] :
                  ( element(D,the_carrier(A))
                 => ( relstr_element_smaller(A,B,D)
                   => related(A,D,C) ) )
              & relstr_element_smaller(A,B,C)
              & element(C,the_carrier(A)) ) ) ),
    file('theBenchmark.p',d8_yellow_0) ).

fof(t25_orders_2,axiom,
    ! [A] :
      ( ( rel_str(A)
        & antisymmetric_relstr(A) )
     => ! [B] :
          ( element(B,the_carrier(A))
         => ! [C] :
              ( element(C,the_carrier(A))
             => ( ( related(A,C,B)
                  & related(A,B,C) )
               => B = C ) ) ) ),
    file('theBenchmark.p',t25_orders_2) ).

fof(t16_yellow_0,conjecture,
    ! [A] :
      ( ( rel_str(A)
        & antisymmetric_relstr(A) )
     => ! [B] :
          ( ex_inf_of_relstr_set(A,B)
        <=> ? [C] :
              ( ! [D] :
                  ( element(D,the_carrier(A))
                 => ( relstr_element_smaller(A,B,D)
                   => related(A,D,C) ) )
              & relstr_element_smaller(A,B,C)
              & element(C,the_carrier(A)) ) ) ),
    file('theBenchmark.p',t16_yellow_0) ).

fof(t16_yellow_0_neg,negated_conjecture,
    ~ ! [A] :
        ( ( rel_str(A)
          & antisymmetric_relstr(A) )
       => ! [B] :
            ( ex_inf_of_relstr_set(A,B)
          <=> ? [C] :
                ( ! [D] :
                    ( element(D,the_carrier(A))
                   => ( relstr_element_smaller(A,B,D)
                     => related(A,D,C) ) )
                & relstr_element_smaller(A,B,C)
                & element(C,the_carrier(A)) ) ) ),
    inference(assume_negation,[status(cth)],[t16_yellow_0]) ).

fof(nnf_1,plain,
    ! [A] :
      ( ! [B] :
          ( ( ! [C] :
                ( ? [D] :
                    ( D != C
                    & ! [E] :
                        ( related(A,E,D)
                        | ~ relstr_element_smaller(A,B,E)
                        | ~ element(E,the_carrier(A)) )
                    & relstr_element_smaller(A,B,D)
                    & element(D,the_carrier(A)) )
                | ? [X4] :
                    ( ~ related(A,X4,C)
                    & relstr_element_smaller(A,B,X4)
                    & element(X4,the_carrier(A)) )
                | ~ relstr_element_smaller(A,B,C)
                | ~ element(C,the_carrier(A)) )
            | ex_inf_of_relstr_set(A,B) )
          & ( ? [X0] :
                ( ! [X2] :
                    ( X2 = X0
                    | ? [X3] :
                        ( ~ related(A,X3,X2)
                        & relstr_element_smaller(A,B,X3)
                        & element(X3,the_carrier(A)) )
                    | ~ relstr_element_smaller(A,B,X2)
                    | ~ element(X2,the_carrier(A)) )
                & ! [X1] :
                    ( related(A,X1,X0)
                    | ~ relstr_element_smaller(A,B,X1)
                    | ~ element(X1,the_carrier(A)) )
                & relstr_element_smaller(A,B,X0)
                & element(X0,the_carrier(A)) )
            | ~ ex_inf_of_relstr_set(A,B) ) )
      | ~ rel_str(A) ),
    inference(fof_nnf,[status(thm)],[d8_yellow_0]) ).

fof(sk_d8_yellow_0_sk,plain,
    ! [A] :
      ( ! [B] :
          ( ( ! [C] :
                ( ( sK1(A,B,C) != C
                  & ! [E] :
                      ( related(A,E,sK1(A,B,C))
                      | ~ relstr_element_smaller(A,B,E)
                      | ~ element(E,the_carrier(A)) )
                  & relstr_element_smaller(A,B,sK1(A,B,C))
                  & element(sK1(A,B,C),the_carrier(A)) )
                | ( ~ related(A,sK0(A,B,C),C)
                  & relstr_element_smaller(A,B,sK0(A,B,C))
                  & element(sK0(A,B,C),the_carrier(A)) )
                | ~ relstr_element_smaller(A,B,C)
                | ~ element(C,the_carrier(A)) )
            | ex_inf_of_relstr_set(A,B) )
          & ( ( ! [X2] :
                  ( X2 = sK2(A,B)
                  | ( ~ related(A,sK7(A,B,X2),X2)
                    & relstr_element_smaller(A,B,sK7(A,B,X2))
                    & element(sK7(A,B,X2),the_carrier(A)) )
                  | ~ relstr_element_smaller(A,B,X2)
                  | ~ element(X2,the_carrier(A)) )
              & ! [X1] :
                  ( related(A,X1,sK2(A,B))
                  | ~ relstr_element_smaller(A,B,X1)
                  | ~ element(X1,the_carrier(A)) )
              & relstr_element_smaller(A,B,sK2(A,B))
              & element(sK2(A,B),the_carrier(A)) )
            | ~ ex_inf_of_relstr_set(A,B) ) )
      | ~ rel_str(A) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK7,sK0,sK1]),skolemize(X0,sK2(A,B)),skolemize(X3,sK7(A,B,X2)),skolemize(X4,sK0(A,B,C)),skolemize(D,sK1(A,B,C))],[nnf_1]) ).

fof(sk_d8_yellow_0,plain,
    ( ! [VAR_0,VAR_1,VAR_2] :
        ( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
        | ~ related(VAR_0,sK0(VAR_0,VAR_1,VAR_2),VAR_2)
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2,VAR_3] :
        ( related(VAR_0,VAR_3,sK1(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_3)
        | ~ element(VAR_3,the_carrier(VAR_0))
        | ~ related(VAR_0,sK0(VAR_0,VAR_1,VAR_2),VAR_2)
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( relstr_element_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
        | ~ related(VAR_0,sK0(VAR_0,VAR_1,VAR_2),VAR_2)
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ related(VAR_0,sK0(VAR_0,VAR_1,VAR_2),VAR_2)
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
        | relstr_element_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2,VAR_3] :
        ( related(VAR_0,VAR_3,sK1(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_3)
        | ~ element(VAR_3,the_carrier(VAR_0))
        | relstr_element_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( relstr_element_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
        | relstr_element_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | relstr_element_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
        | element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2,VAR_3] :
        ( related(VAR_0,VAR_3,sK1(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_3)
        | ~ element(VAR_3,the_carrier(VAR_0))
        | element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( relstr_element_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
        | element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( VAR_2 = sK2(VAR_0,VAR_1)
        | ~ related(VAR_0,sK7(VAR_0,VAR_1,VAR_2),VAR_2)
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( VAR_2 = sK2(VAR_0,VAR_1)
        | relstr_element_smaller(VAR_0,VAR_1,sK7(VAR_0,VAR_1,VAR_2))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( VAR_2 = sK2(VAR_0,VAR_1)
        | element(sK7(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1,VAR_2] :
        ( related(VAR_0,VAR_2,sK2(VAR_0,VAR_1))
        | ~ relstr_element_smaller(VAR_0,VAR_1,VAR_2)
        | ~ element(VAR_2,the_carrier(VAR_0))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1] :
        ( relstr_element_smaller(VAR_0,VAR_1,sK2(VAR_0,VAR_1))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) )
    & ! [VAR_0,VAR_1] :
        ( element(sK2(VAR_0,VAR_1),the_carrier(VAR_0))
        | ~ ex_inf_of_relstr_set(VAR_0,VAR_1)
        | ~ rel_str(VAR_0) ) ),
    inference(cnf_transformation,[status(thm)],[sk_d8_yellow_0_sk]) ).

cnf(c_13,plain,
    ( sK1(A,B,C) != C
    | ~ related(A,sK0(A,B,C),C)
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_14,plain,
    ( related(A,D,sK1(A,B,C))
    | ~ relstr_element_smaller(A,B,D)
    | ~ element(D,the_carrier(A))
    | ~ related(A,sK0(A,B,C),C)
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_15,plain,
    ( relstr_element_smaller(A,B,sK1(A,B,C))
    | ~ related(A,sK0(A,B,C),C)
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_16,plain,
    ( element(sK1(A,B,C),the_carrier(A))
    | ~ related(A,sK0(A,B,C),C)
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_17,plain,
    ( sK1(A,B,C) != C
    | relstr_element_smaller(A,B,sK0(A,B,C))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_18,plain,
    ( related(A,D,sK1(A,B,C))
    | ~ relstr_element_smaller(A,B,D)
    | ~ element(D,the_carrier(A))
    | relstr_element_smaller(A,B,sK0(A,B,C))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_19,plain,
    ( relstr_element_smaller(A,B,sK1(A,B,C))
    | relstr_element_smaller(A,B,sK0(A,B,C))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_20,plain,
    ( element(sK1(A,B,C),the_carrier(A))
    | relstr_element_smaller(A,B,sK0(A,B,C))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_21,plain,
    ( sK1(A,B,C) != C
    | element(sK0(A,B,C),the_carrier(A))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_22,plain,
    ( related(A,D,sK1(A,B,C))
    | ~ relstr_element_smaller(A,B,D)
    | ~ element(D,the_carrier(A))
    | element(sK0(A,B,C),the_carrier(A))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_23,plain,
    ( relstr_element_smaller(A,B,sK1(A,B,C))
    | element(sK0(A,B,C),the_carrier(A))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_24,plain,
    ( element(sK1(A,B,C),the_carrier(A))
    | element(sK0(A,B,C),the_carrier(A))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_28,plain,
    ( related(A,C,sK2(A,B))
    | ~ relstr_element_smaller(A,B,C)
    | ~ element(C,the_carrier(A))
    | ~ ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_29,plain,
    ( relstr_element_smaller(A,B,sK2(A,B))
    | ~ ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_30,plain,
    ( element(sK2(A,B),the_carrier(A))
    | ~ ex_inf_of_relstr_set(A,B)
    | ~ rel_str(A) ),
    inference(split_conjunct,[status(thm)],[sk_d8_yellow_0]) ).

cnf(c_31,plain,
    ( C = B
    | ~ related(A,C,B)
    | ~ related(A,B,C)
    | ~ element(C,the_carrier(A))
    | ~ element(B,the_carrier(A))
    | ~ rel_str(A)
    | ~ antisymmetric_relstr(A) ),
    inference(clausify,[status(thm)],[t25_orders_2]) ).

fof(nnf_10,plain,
    ? [A] :
      ( ? [B] :
          ( ( ! [C] :
                ( ? [D] :
                    ( ~ related(A,D,C)
                    & relstr_element_smaller(A,B,D)
                    & element(D,the_carrier(A)) )
                | ~ relstr_element_smaller(A,B,C)
                | ~ element(C,the_carrier(A)) )
            | ~ ex_inf_of_relstr_set(A,B) )
          & ( ? [X4] :
                ( ! [X0] :
                    ( related(A,X0,X4)
                    | ~ relstr_element_smaller(A,B,X0)
                    | ~ element(X0,the_carrier(A)) )
                & relstr_element_smaller(A,B,X4)
                & element(X4,the_carrier(A)) )
            | ex_inf_of_relstr_set(A,B) ) )
      & rel_str(A)
      & antisymmetric_relstr(A) ),
    inference(fof_nnf,[status(thm)],[t16_yellow_0_neg]) ).

fof(sk_t16_yellow_0_neg_sk,plain,
    ( ( ! [C] :
          ( ( ~ related(sK3,sK6(C),C)
            & relstr_element_smaller(sK3,sK4,sK6(C))
            & element(sK6(C),the_carrier(sK3)) )
          | ~ relstr_element_smaller(sK3,sK4,C)
          | ~ element(C,the_carrier(sK3)) )
      | ~ ex_inf_of_relstr_set(sK3,sK4) )
    & ( ( ! [X0] :
            ( related(sK3,X0,sK5)
            | ~ relstr_element_smaller(sK3,sK4,X0)
            | ~ element(X0,the_carrier(sK3)) )
        & relstr_element_smaller(sK3,sK4,sK5)
        & element(sK5,the_carrier(sK3)) )
      | ex_inf_of_relstr_set(sK3,sK4) )
    & rel_str(sK3)
    & antisymmetric_relstr(sK3) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(A,sK3),skolemize(B,sK4),skolemize(X4,sK5),skolemize(D,sK6(C))],[nnf_10]) ).

fof(sk_t16_yellow_0_neg,plain,
    ( ! [VAR_0] :
        ( ~ related(sK3,sK6(VAR_0),VAR_0)
        | ~ relstr_element_smaller(sK3,sK4,VAR_0)
        | ~ element(VAR_0,the_carrier(sK3))
        | ~ ex_inf_of_relstr_set(sK3,sK4) )
    & ! [VAR_0] :
        ( relstr_element_smaller(sK3,sK4,sK6(VAR_0))
        | ~ relstr_element_smaller(sK3,sK4,VAR_0)
        | ~ element(VAR_0,the_carrier(sK3))
        | ~ ex_inf_of_relstr_set(sK3,sK4) )
    & ! [VAR_0] :
        ( element(sK6(VAR_0),the_carrier(sK3))
        | ~ relstr_element_smaller(sK3,sK4,VAR_0)
        | ~ element(VAR_0,the_carrier(sK3))
        | ~ ex_inf_of_relstr_set(sK3,sK4) )
    & ! [VAR_0] :
        ( related(sK3,VAR_0,sK5)
        | ~ relstr_element_smaller(sK3,sK4,VAR_0)
        | ~ element(VAR_0,the_carrier(sK3))
        | ex_inf_of_relstr_set(sK3,sK4) )
    & ( relstr_element_smaller(sK3,sK4,sK5)
      | ex_inf_of_relstr_set(sK3,sK4) )
    & ( element(sK5,the_carrier(sK3))
      | ex_inf_of_relstr_set(sK3,sK4) )
    & rel_str(sK3)
    & antisymmetric_relstr(sK3) ),
    inference(cnf_transformation,[status(thm)],[sk_t16_yellow_0_neg_sk]) ).

cnf(c_32,negated_conjecture,
    rel_str(sK3),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_34,negated_conjecture,
    antisymmetric_relstr(sK3),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_35,negated_conjecture,
    ( element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_36,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_37,negated_conjecture,
    ( related(sK3,A,sK5)
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_38,negated_conjecture,
    ( element(sK6(A),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_39,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK6(A))
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_40,negated_conjecture,
    ( ~ related(sK3,sK6(A),A)
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4) ),
    inference(split_conjunct,[status(thm)],[sk_t16_yellow_0_neg]) ).

cnf(c_63,negated_conjecture,
    ( B = A
    | ~ related(sK3,B,A)
    | ~ related(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ~ element(A,the_carrier(sK3))
    | ~ antisymmetric_relstr(sK3) ),
    inference(resolve,[status(thm)],[c_32,c_31]) ).

cnf(c_64,negated_conjecture,
    ( B = A
    | ~ related(sK3,B,A)
    | ~ related(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ~ element(A,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_34,c_63]) ).

cnf(c_65,negated_conjecture,
    ( sK1(sK3,A,B) != B
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_13]) ).

cnf(c_66,negated_conjecture,
    ( related(sK3,C,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,C)
    | ~ element(C,the_carrier(sK3))
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_14]) ).

cnf(c_67,negated_conjecture,
    ( relstr_element_smaller(sK3,A,sK1(sK3,A,B))
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_15]) ).

cnf(c_68,negated_conjecture,
    ( element(sK1(sK3,A,B),the_carrier(sK3))
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_16]) ).

cnf(c_69,negated_conjecture,
    ( sK1(sK3,A,B) != B
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_17]) ).

cnf(c_70,negated_conjecture,
    ( related(sK3,C,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,C)
    | ~ element(C,the_carrier(sK3))
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_18]) ).

cnf(c_71,negated_conjecture,
    ( relstr_element_smaller(sK3,A,sK1(sK3,A,B))
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_19]) ).

cnf(c_72,negated_conjecture,
    ( element(sK1(sK3,A,B),the_carrier(sK3))
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_20]) ).

cnf(c_73,negated_conjecture,
    ( sK1(sK3,A,B) != B
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_21]) ).

cnf(c_74,negated_conjecture,
    ( related(sK3,C,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,C)
    | ~ element(C,the_carrier(sK3))
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_22]) ).

cnf(c_75,negated_conjecture,
    ( relstr_element_smaller(sK3,A,sK1(sK3,A,B))
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_23]) ).

cnf(c_76,negated_conjecture,
    ( element(sK1(sK3,A,B),the_carrier(sK3))
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_24]) ).

cnf(c_83,negated_conjecture,
    ( related(sK3,B,sK2(sK3,A))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_28]) ).

cnf(c_84,negated_conjecture,
    ( relstr_element_smaller(sK3,A,sK2(sK3,A))
    | ~ ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_29]) ).

cnf(c_85,negated_conjecture,
    ( element(sK2(sK3,A),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,A) ),
    inference(resolve,[status(thm)],[c_32,c_30]) ).

cnf(c_725,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(factor,[status(thm)],[c_66]) ).

cnf(c_89,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | ~ related(sK3,sK0(sK3,A,B),B)
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(copy,[status(thm)],[c_725]) ).

cnf(c_726,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(factor,[status(thm)],[c_70]) ).

cnf(c_90,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | relstr_element_smaller(sK3,A,sK0(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(copy,[status(thm)],[c_726]) ).

cnf(c_727,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | ~ relstr_element_smaller(sK3,A,B)
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(factor,[status(thm)],[c_74]) ).

cnf(c_91,plain,
    ( related(sK3,B,sK1(sK3,A,B))
    | element(sK0(sK3,A,B),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,A,B)
    | ~ element(B,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,A) ),
    inference(copy,[status(thm)],[c_727]) ).

cnf(c_728,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) != sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_69,c_36]) ).

cnf(c_93,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_728]) ).

cnf(c_729,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_71,c_36]) ).

cnf(c_96,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_729]) ).

cnf(c_730,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_72,c_36]) ).

cnf(c_97,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_730]) ).

cnf(c_731,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) != sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_73,c_36]) ).

cnf(c_98,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_731]) ).

cnf(c_732,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_75,c_36]) ).

cnf(c_101,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_732]) ).

cnf(c_733,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_76,c_36]) ).

cnf(c_102,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_733]) ).

cnf(c_103,plain,
    ( element(sK5,the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK2(sK3,sK4)) ),
    inference(resolve,[status(thm)],[c_84,c_35]) ).

cnf(c_104,plain,
    ( element(sK5,the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_85,c_35]) ).

cnf(c_734,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | related(sK3,sK5,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_90,c_36]) ).

cnf(c_105,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_734]) ).

cnf(c_735,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | related(sK3,sK5,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_91,c_36]) ).

cnf(c_106,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_735]) ).

cnf(c_108,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_103,c_39]) ).

cnf(c_109,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_103,c_38]) ).

cnf(c_736,negated_conjecture,
    ( element(sK5,the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_108,c_35]) ).

cnf(c_112,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_736]) ).

cnf(c_737,negated_conjecture,
    ( element(sK5,the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_109,c_35]) ).

cnf(c_113,negated_conjecture,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_737]) ).

cnf(c_738,plain,
    ( element(sK5,the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_112,c_104]) ).

cnf(c_114,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_738]) ).

cnf(c_115,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_114,c_83]) ).

cnf(c_739,plain,
    ( element(sK5,the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_113,c_104]) ).

cnf(c_120,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_739]) ).

cnf(c_740,negated_conjecture,
    ( element(sK5,the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_115,c_35]) ).

cnf(c_121,negated_conjecture,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_740]) ).

cnf(c_741,plain,
    ( element(sK5,the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_121,c_120]) ).

cnf(c_122,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_741]) ).

cnf(c_124,plain,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_122,c_40]) ).

cnf(c_742,plain,
    ( element(sK5,the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_124,c_103]) ).

cnf(c_128,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_742]) ).

cnf(c_743,negated_conjecture,
    ( element(sK5,the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_128,c_35]) ).

cnf(c_129,negated_conjecture,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_743]) ).

cnf(c_744,plain,
    ( element(sK5,the_carrier(sK3))
    | element(sK5,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_129,c_104]) ).

cnf(c_130,plain,
    element(sK5,the_carrier(sK3)),
    inference(copy,[status(thm)],[c_744]) ).

cnf(c_131,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_106]) ).

cnf(c_132,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_105]) ).

cnf(c_133,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_102]) ).

cnf(c_134,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_101]) ).

cnf(c_137,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_98]) ).

cnf(c_138,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_97]) ).

cnf(c_139,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_96]) ).

cnf(c_142,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_93]) ).

cnf(c_745,negated_conjecture,
    ( sK5 = sK1(sK3,sK4,sK5)
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_131,c_64]) ).

cnf(c_746,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_745]) ).

cnf(c_144,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_746]) ).

cnf(c_747,negated_conjecture,
    ( sK5 = sK1(sK3,sK4,sK5)
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_132,c_64]) ).

cnf(c_748,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_747]) ).

cnf(c_145,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_748]) ).

cnf(c_146,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_133,c_85]) ).

cnf(c_147,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_133,c_84]) ).

cnf(c_749,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_134,c_37]) ).

cnf(c_160,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_749]) ).

cnf(c_750,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_138,c_37]) ).

cnf(c_174,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_750]) ).

cnf(c_751,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_139,c_37]) ).

cnf(c_187,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_751]) ).

cnf(c_190,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_147,c_39]) ).

cnf(c_191,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_147,c_38]) ).

cnf(c_752,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_160,c_146]) ).

cnf(c_200,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_752]) ).

cnf(c_753,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_144,c_200]) ).

cnf(c_754,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_753]) ).

cnf(c_204,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_754]) ).

cnf(c_755,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_204,c_146]) ).

cnf(c_756,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_755]) ).

cnf(c_206,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_756]) ).

cnf(c_757,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_206,c_85]) ).

cnf(c_207,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_757]) ).

cnf(c_208,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_207,c_174]) ).

cnf(c_758,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_208,c_68]) ).

cnf(c_759,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_758]) ).

cnf(c_760,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_759]) ).

cnf(c_210,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_760]) ).

cnf(c_761,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_210,c_36]) ).

cnf(c_215,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_761]) ).

cnf(c_762,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_215,c_85]) ).

cnf(c_216,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_762]) ).

cnf(c_218,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_216,c_187]) ).

cnf(c_763,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_218,c_145]) ).

cnf(c_764,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_763]) ).

cnf(c_765,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_764]) ).

cnf(c_219,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_765]) ).

cnf(c_766,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_219,c_216]) ).

cnf(c_767,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_766]) ).

cnf(c_220,plain,
    ( relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_767]) ).

cnf(c_768,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_220,c_37]) ).

cnf(c_235,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_768]) ).

cnf(c_769,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_235,c_207]) ).

cnf(c_770,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_769]) ).

cnf(c_237,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_770]) ).

cnf(c_771,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_237,c_89]) ).

cnf(c_772,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_771]) ).

cnf(c_238,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_772]) ).

cnf(c_773,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_237,c_67]) ).

cnf(c_774,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_773]) ).

cnf(c_239,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_774]) ).

cnf(c_775,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_238,c_36]) ).

cnf(c_242,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_775]) ).

cnf(c_776,negated_conjecture,
    ( sK5 = sK1(sK3,sK4,sK5)
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_242,c_64]) ).

cnf(c_777,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_776]) ).

cnf(c_778,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_777]) ).

cnf(c_243,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_778]) ).

cnf(c_779,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_239,c_36]) ).

cnf(c_244,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_779]) ).

cnf(c_780,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_244,c_37]) ).

cnf(c_259,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_780]) ).

cnf(c_781,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_259,c_216]) ).

cnf(c_782,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_781]) ).

cnf(c_262,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_782]) ).

cnf(c_783,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_262,c_243]) ).

cnf(c_784,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_783]) ).

cnf(c_785,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_784]) ).

cnf(c_263,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_785]) ).

cnf(c_786,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_263,c_216]) ).

cnf(c_787,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_786]) ).

cnf(c_264,plain,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_787]) ).

cnf(c_788,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_264,c_85]) ).

cnf(c_265,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_788]) ).

cnf(c_789,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_190,c_133]) ).

cnf(c_790,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_789]) ).

cnf(c_269,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_790]) ).

cnf(c_270,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_269,c_265]) ).

cnf(c_271,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_270,c_83]) ).

cnf(c_791,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_191,c_133]) ).

cnf(c_792,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_791]) ).

cnf(c_276,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_792]) ).

cnf(c_277,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_276,c_265]) ).

cnf(c_793,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_277,c_160]) ).

cnf(c_281,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_793]) ).

cnf(c_794,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_281,c_144]) ).

cnf(c_795,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_794]) ).

cnf(c_796,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_795]) ).

cnf(c_291,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_796]) ).

cnf(c_797,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_291,c_277]) ).

cnf(c_798,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_797]) ).

cnf(c_799,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_798]) ).

cnf(c_292,plain,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_799]) ).

cnf(c_293,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_292,c_84]) ).

cnf(c_800,negated_conjecture,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_293,c_38]) ).

cnf(c_296,negated_conjecture,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_800]) ).

cnf(c_801,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_296,c_292]) ).

cnf(c_802,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_801]) ).

cnf(c_803,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_802]) ).

cnf(c_297,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_803]) ).

cnf(c_804,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_297,c_265]) ).

cnf(c_298,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_804]) ).

cnf(c_299,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_298,c_174]) ).

cnf(c_805,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_299,c_68]) ).

cnf(c_806,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_805]) ).

cnf(c_807,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_806]) ).

cnf(c_306,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_130,c_807]) ).

cnf(c_808,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_306,c_36]) ).

cnf(c_308,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_808]) ).

cnf(c_309,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_308,c_84]) ).

cnf(c_809,negated_conjecture,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_309,c_38]) ).

cnf(c_312,negated_conjecture,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_809]) ).

cnf(c_810,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_312,c_308]) ).

cnf(c_811,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_810]) ).

cnf(c_812,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_811]) ).

cnf(c_313,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_812]) ).

cnf(c_813,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_313,c_265]) ).

cnf(c_314,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_813]) ).

cnf(c_316,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_314,c_187]) ).

cnf(c_814,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_316,c_145]) ).

cnf(c_815,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_814]) ).

cnf(c_816,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_815]) ).

cnf(c_317,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_816]) ).

cnf(c_817,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_317,c_314]) ).

cnf(c_818,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_817]) ).

cnf(c_319,plain,
    ( relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_818]) ).

cnf(c_819,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_319,c_37]) ).

cnf(c_334,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_819]) ).

cnf(c_820,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_334,c_298]) ).

cnf(c_821,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_820]) ).

cnf(c_335,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_821]) ).

cnf(c_822,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_335,c_89]) ).

cnf(c_823,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_822]) ).

cnf(c_336,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_130,c_823]) ).

cnf(c_824,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_335,c_67]) ).

cnf(c_825,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_824]) ).

cnf(c_337,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_130,c_825]) ).

cnf(c_826,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_336,c_36]) ).

cnf(c_340,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_826]) ).

cnf(c_827,negated_conjecture,
    ( sK5 = sK1(sK3,sK4,sK5)
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_340,c_64]) ).

cnf(c_828,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_827]) ).

cnf(c_829,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_828]) ).

cnf(c_341,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_130,c_829]) ).

cnf(c_830,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_337,c_36]) ).

cnf(c_342,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_830]) ).

cnf(c_831,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_342,c_37]) ).

cnf(c_357,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_831]) ).

cnf(c_832,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_357,c_314]) ).

cnf(c_833,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_832]) ).

cnf(c_358,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_833]) ).

cnf(c_834,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_358,c_341]) ).

cnf(c_835,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_834]) ).

cnf(c_836,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_835]) ).

cnf(c_359,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_836]) ).

cnf(c_837,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_359,c_314]) ).

cnf(c_838,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_837]) ).

cnf(c_360,plain,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_838]) ).

cnf(c_361,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_360,c_84]) ).

cnf(c_839,negated_conjecture,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_361,c_38]) ).

cnf(c_364,negated_conjecture,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_839]) ).

cnf(c_840,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_364,c_360]) ).

cnf(c_841,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_840]) ).

cnf(c_365,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_841]) ).

cnf(c_842,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_365,c_265]) ).

cnf(c_366,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_842]) ).

cnf(c_843,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_271,c_133]) ).

cnf(c_844,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_843]) ).

cnf(c_443,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_844]) ).

cnf(c_845,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_443,c_366]) ).

cnf(c_444,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_845]) ).

cnf(c_446,plain,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_444,c_40]) ).

cnf(c_846,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_446,c_147]) ).

cnf(c_847,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_846]) ).

cnf(c_447,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_847]) ).

cnf(c_848,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_447,c_133]) ).

cnf(c_849,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_848]) ).

cnf(c_448,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_849]) ).

cnf(c_850,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_448,c_265]) ).

cnf(c_449,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_850]) ).

cnf(c_851,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_449,c_160]) ).

cnf(c_466,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_851]) ).

cnf(c_852,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_466,c_144]) ).

cnf(c_853,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_852]) ).

cnf(c_854,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_853]) ).

cnf(c_476,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_854]) ).

cnf(c_855,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_476,c_449]) ).

cnf(c_856,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_855]) ).

cnf(c_477,plain,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_856]) ).

cnf(c_478,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_477,c_84]) ).

cnf(c_480,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_478,c_39]) ).

cnf(c_857,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_480,c_477]) ).

cnf(c_858,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_857]) ).

cnf(c_486,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_858]) ).

cnf(c_859,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_486,c_265]) ).

cnf(c_487,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_859]) ).

cnf(c_488,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_487,c_83]) ).

cnf(c_860,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_488,c_477]) ).

cnf(c_861,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_860]) ).

cnf(c_493,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_861]) ).

cnf(c_862,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_493,c_366]) ).

cnf(c_497,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_862]) ).

cnf(c_499,plain,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_497,c_40]) ).

cnf(c_863,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_499,c_478]) ).

cnf(c_864,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_863]) ).

cnf(c_500,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_864]) ).

cnf(c_865,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_500,c_477]) ).

cnf(c_866,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_865]) ).

cnf(c_501,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_866]) ).

cnf(c_867,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_501,c_265]) ).

cnf(c_502,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_867]) ).

cnf(c_505,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_502,c_174]) ).

cnf(c_868,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_505,c_68]) ).

cnf(c_869,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_868]) ).

cnf(c_870,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_869]) ).

cnf(c_516,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_870]) ).

cnf(c_871,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_516,c_36]) ).

cnf(c_518,negated_conjecture,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_871]) ).

cnf(c_519,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_518,c_84]) ).

cnf(c_521,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_519,c_39]) ).

cnf(c_872,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_521,c_518]) ).

cnf(c_873,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_872]) ).

cnf(c_527,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_873]) ).

cnf(c_874,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_527,c_265]) ).

cnf(c_528,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_874]) ).

cnf(c_529,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_528,c_83]) ).

cnf(c_875,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_529,c_518]) ).

cnf(c_876,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_875]) ).

cnf(c_534,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_876]) ).

cnf(c_877,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_534,c_366]) ).

cnf(c_535,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_877]) ).

cnf(c_538,plain,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_535,c_40]) ).

cnf(c_878,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_538,c_519]) ).

cnf(c_879,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_878]) ).

cnf(c_539,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_879]) ).

cnf(c_880,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_539,c_518]) ).

cnf(c_881,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_880]) ).

cnf(c_540,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_881]) ).

cnf(c_882,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_540,c_265]) ).

cnf(c_541,plain,
    ( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_882]) ).

cnf(c_545,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_541,c_187]) ).

cnf(c_883,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_545,c_145]) ).

cnf(c_884,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_883]) ).

cnf(c_885,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_884]) ).

cnf(c_554,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_885]) ).

cnf(c_886,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_554,c_541]) ).

cnf(c_556,plain,
    ( relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_886]) ).

cnf(c_887,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_556,c_37]) ).

cnf(c_571,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_887]) ).

cnf(c_888,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_571,c_502]) ).

cnf(c_572,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_888]) ).

cnf(c_889,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_572,c_89]) ).

cnf(c_890,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_889]) ).

cnf(c_573,plain,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_890]) ).

cnf(c_891,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_572,c_67]) ).

cnf(c_892,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_891]) ).

cnf(c_574,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_892]) ).

cnf(c_893,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_573,c_36]) ).

cnf(c_577,negated_conjecture,
    ( related(sK3,sK5,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_893]) ).

cnf(c_894,negated_conjecture,
    ( sK5 = sK1(sK3,sK4,sK5)
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_577,c_64]) ).

cnf(c_895,negated_conjecture,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_894]) ).

cnf(c_896,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_895]) ).

cnf(c_578,negated_conjecture,
    ( ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_130,c_896]) ).

cnf(c_897,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_574,c_36]) ).

cnf(c_579,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_897]) ).

cnf(c_898,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_579,c_37]) ).

cnf(c_594,negated_conjecture,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_898]) ).

cnf(c_899,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_594,c_541]) ).

cnf(c_595,plain,
    ( related(sK3,sK1(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_899]) ).

cnf(c_900,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_595,c_578]) ).

cnf(c_901,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_900]) ).

cnf(c_596,plain,
    ( ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_901]) ).

cnf(c_902,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_596,c_541]) ).

cnf(c_597,plain,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_902]) ).

cnf(c_598,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_597,c_84]) ).

cnf(c_600,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_598,c_39]) ).

cnf(c_903,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_600,c_597]) ).

cnf(c_603,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_903]) ).

cnf(c_904,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_603,c_265]) ).

cnf(c_604,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_904]) ).

cnf(c_605,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_604,c_83]) ).

cnf(c_905,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_605,c_597]) ).

cnf(c_610,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_905]) ).

cnf(c_906,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_610,c_366]) ).

cnf(c_611,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_906]) ).

cnf(c_613,plain,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_611,c_40]) ).

cnf(c_907,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_613,c_598]) ).

cnf(c_614,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_907]) ).

cnf(c_908,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_614,c_597]) ).

cnf(c_615,plain,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(copy,[status(thm)],[c_908]) ).

cnf(c_909,plain,
    ( sK1(sK3,sK4,sK5) = sK5
    | sK1(sK3,sK4,sK5) = sK5 ),
    inference(resolve,[status(thm)],[c_615,c_265]) ).

cnf(c_616,plain,
    sK1(sK3,sK4,sK5) = sK5,
    inference(copy,[status(thm)],[c_909]) ).

cnf(c_617,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_616,c_142]) ).

cnf(c_618,negated_conjecture,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_616,c_137]) ).

cnf(c_910,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_617,c_37]) ).

cnf(c_633,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_910]) ).

cnf(c_634,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_618,c_85]) ).

cnf(c_635,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_618,c_84]) ).

cnf(c_640,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_635,c_39]) ).

cnf(c_641,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_635,c_38]) ).

cnf(c_642,plain,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_633,c_634]) ).

cnf(c_911,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_642,c_65]) ).

cnf(c_912,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_911]) ).

cnf(c_913,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_912]) ).

cnf(c_647,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_616,c_913]) ).

cnf(c_914,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_647,c_36]) ).

cnf(c_649,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_914]) ).

cnf(c_915,negated_conjecture,
    ( element(sK2(sK3,sK4),the_carrier(sK3))
    | element(sK2(sK3,sK4),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_649,c_85]) ).

cnf(c_650,negated_conjecture,
    element(sK2(sK3,sK4),the_carrier(sK3)),
    inference(copy,[status(thm)],[c_915]) ).

cnf(c_651,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_650,c_641]) ).

cnf(c_652,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_650,c_640]) ).

cnf(c_916,plain,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_651,c_618]) ).

cnf(c_658,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_916]) ).

cnf(c_659,plain,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_658,c_633]) ).

cnf(c_917,plain,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_652,c_618]) ).

cnf(c_666,plain,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_917]) ).

cnf(c_667,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_666,c_83]) ).

cnf(c_918,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_659,c_65]) ).

cnf(c_919,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_918]) ).

cnf(c_920,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_130,c_919]) ).

cnf(c_677,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_616,c_920]) ).

cnf(c_921,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_677,c_36]) ).

cnf(c_679,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_921]) ).

cnf(c_680,plain,
    ( relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_679,c_84]) ).

cnf(c_922,negated_conjecture,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_680,c_38]) ).

cnf(c_923,negated_conjecture,
    ( ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_922]) ).

cnf(c_683,negated_conjecture,
    ( ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_650,c_923]) ).

cnf(c_924,plain,
    ( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
    | element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_683,c_679]) ).

cnf(c_684,plain,
    element(sK6(sK2(sK3,sK4)),the_carrier(sK3)),
    inference(copy,[status(thm)],[c_924]) ).

cnf(c_689,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_684,c_667]) ).

cnf(c_925,plain,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_689,c_618]) ).

cnf(c_690,plain,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_925]) ).

cnf(c_926,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_690,c_40]) ).

cnf(c_692,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_650,c_926]) ).

cnf(c_927,plain,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_692,c_635]) ).

cnf(c_693,plain,
    ( ~ ex_inf_of_relstr_set(sK3,sK4)
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(copy,[status(thm)],[c_927]) ).

cnf(c_928,plain,
    ( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
    | element(sK0(sK3,sK4,sK5),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_693,c_618]) ).

cnf(c_694,plain,
    element(sK0(sK3,sK4,sK5),the_carrier(sK3)),
    inference(copy,[status(thm)],[c_928]) ).

cnf(c_695,negated_conjecture,
    ( related(sK3,sK0(sK3,sK4,sK5),sK5)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_694,c_633]) ).

cnf(c_929,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_695,c_65]) ).

cnf(c_930,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ~ element(sK5,the_carrier(sK3))
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(copy,[status(thm)],[c_929]) ).

cnf(c_931,negated_conjecture,
    ( sK1(sK3,sK4,sK5) != sK5
    | ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_130,c_930]) ).

cnf(c_714,negated_conjecture,
    ( ~ relstr_element_smaller(sK3,sK4,sK5)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_616,c_931]) ).

cnf(c_932,negated_conjecture,
    ( ex_inf_of_relstr_set(sK3,sK4)
    | ex_inf_of_relstr_set(sK3,sK4) ),
    inference(resolve,[status(thm)],[c_714,c_36]) ).

cnf(c_716,negated_conjecture,
    ex_inf_of_relstr_set(sK3,sK4),
    inference(copy,[status(thm)],[c_932]) ).

cnf(c_717,negated_conjecture,
    ( ~ related(sK3,sK6(A),A)
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_716,c_40]) ).

cnf(c_718,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK6(A))
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_716,c_39]) ).

cnf(c_720,plain,
    relstr_element_smaller(sK3,sK4,sK2(sK3,sK4)),
    inference(resolve,[status(thm)],[c_716,c_84]) ).

cnf(c_933,negated_conjecture,
    ( ~ related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ relstr_element_smaller(sK3,sK4,sK2(sK3,sK4)) ),
    inference(resolve,[status(thm)],[c_717,c_650]) ).

cnf(c_722,negated_conjecture,
    ~ related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4)),
    inference(resolve,[status(thm)],[c_933,c_720]) ).

cnf(c_934,negated_conjecture,
    ( relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
    | ~ element(sK2(sK3,sK4),the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_718,c_720]) ).

cnf(c_723,negated_conjecture,
    relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4))),
    inference(resolve,[status(thm)],[c_650,c_934]) ).

cnf(c_935,negated_conjecture,
    ( related(sK3,A,sK2(sK3,sK4))
    | ~ relstr_element_smaller(sK3,sK4,A)
    | ~ element(A,the_carrier(sK3)) ),
    inference(resolve,[status(thm)],[c_83,c_716]) ).

cnf(c_936,negated_conjecture,
    ( related(sK3,sK6(sK2(sK3,sK4)),sK2(sK3,sK4))
    | ~ relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4))) ),
    inference(resolve,[status(thm)],[c_935,c_684]) ).

cnf(c_937,negated_conjecture,
    ~ relstr_element_smaller(sK3,sK4,sK6(sK2(sK3,sK4))),
    inference(resolve,[status(thm)],[c_936,c_722]) ).

cnf(c_724,negated_conjecture,
    $false,
    inference(resolve,[status(thm)],[c_723,c_937]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SEU357+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37  % Computer : n003.cluster.edu
% 0.10/0.37  % Model    : x86_64 x86_64
% 0.10/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37  % Memory   : 8046.5625MB
% 0.10/0.37  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Sat Sep 26 09:20:09 UTC 2026
% 0.10/0.38  % CPUTime  : 
% 0.10/0.38  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38  % Process 2545374 was started by sandbox2 on n003,
% 0.10/0.38  % Sat Sep 26 09:20:09 2026
% 0.10/0.38  % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38  
% 0.10/0.38  % From the command line: assign(max_seconds, 300).
% 0.73/0.56  
% 0.73/0.56  % SZS status Theorem for theBenchmark
% 0.73/0.56  
% 0.73/0.56  % Proof 1 at 0.11 (+ 0.03) seconds.
% 0.73/0.56  % Length of proof is 242.
% 0.73/0.56  % Level of proof is 145.
% 0.73/0.56  % Maximum clause weight is 54.000.
% 0.73/0.56  % Given clauses 378.
% 0.73/0.56  
% 0.73/0.56  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------