SInE---0.4.THM-CRf.s

%------------------------------------------------------------------------------
% File     : SInE---0.4
% Problem  : SWB069+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : Source/sine.py -e eprover -t %d %s

% Computer : art05.cs.miami.edu
% Model    : i686 i686
% CPU      : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory   : 2018MB
% OS       : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Fri Mar  4 00:45:42 EST 2011

% Result   : Theorem 9.60s
% Output   : CNFRefutation 9.60s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   40
%            Number of leaves      :    7
% Syntax   : Number of formulae    :  258 (  16 unt;   0 def)
%            Number of atoms       : 1601 (   0 equ)
%            Maximal formula atoms :  160 (   6 avg)
%            Number of connectives : 2104 ( 761   ~;1215   |; 123   &)
%                                         (   2 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   32 (   7 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of predicates  :    4 (   3 usr;   1 prp; 0-3 aty)
%            Number of functors    :   20 (  20 usr;  13 con; 0-6 aty)
%            Number of variables   :  583 (   0 sgn 110   !;  30   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(5,axiom,
    ! [X4,X5,X6,X7] :
      ( ( iext(uri_rdf_first,X4,X5)
        & iext(uri_rdf_rest,X4,X6)
        & iext(uri_rdf_first,X6,X7)
        & iext(uri_rdf_rest,X6,uri_rdf_nil)
        & ! [X1] :
            ~ ( icext(X5,X1)
              & icext(X7,X1) ) )
     => ? [X3] :
          ( icext(uri_owl_AllDisjointClasses,X3)
          & iext(uri_owl_members,X3,X4) ) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',owl_ndis_alldisjointclasses_fi_002) ).

fof(6,axiom,
    ! [X4,X5,X6,X7,X8,X9] :
      ( ( iext(uri_rdf_first,X4,X5)
        & iext(uri_rdf_rest,X4,X6)
        & iext(uri_rdf_first,X6,X7)
        & iext(uri_rdf_rest,X6,X8)
        & iext(uri_rdf_first,X8,X9)
        & iext(uri_rdf_rest,X8,uri_rdf_nil)
        & ! [X1] :
            ~ ( icext(X5,X1)
              & icext(X7,X1) )
        & ! [X1] :
            ~ ( icext(X5,X1)
              & icext(X9,X1) )
        & ! [X1] :
            ~ ( icext(X7,X1)
              & icext(X9,X1) ) )
     => ? [X3] :
          ( icext(uri_owl_AllDisjointClasses,X3)
          & iext(uri_owl_members,X3,X4) ) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',owl_ndis_alldisjointclasses_fi_003) ).

fof(8,axiom,
    ! [X5,X7] :
      ( iext(uri_owl_disjointWith,X5,X7)
    <=> ( ic(X5)
        & ic(X7)
        & ! [X1] :
            ~ ( icext(X5,X1)
              & icext(X7,X1) ) ) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',owl_eqdis_disjointwith) ).

fof(11,axiom,
    ! [X3,X4,X5,X6,X7] :
      ( ( iext(uri_rdf_first,X4,X5)
        & iext(uri_rdf_rest,X4,X6)
        & iext(uri_rdf_first,X6,X7)
        & iext(uri_rdf_rest,X6,uri_rdf_nil)
        & icext(uri_owl_AllDisjointClasses,X3)
        & iext(uri_owl_members,X3,X4) )
     => ! [X1] :
          ~ ( icext(X5,X1)
            & icext(X7,X1) ) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',owl_ndis_alldisjointclasses_if_002) ).

fof(21,axiom,
    ! [X1,X13] :
      ( iext(uri_rdf_type,X1,X13)
    <=> icext(X13,X1) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',rdfs_cext_def) ).

fof(23,conjecture,
    ? [X14,X15,X16,X17] :
      ( iext(uri_rdf_first,X16,uri_ex_c2)
      & iext(uri_rdf_rest,X16,X17)
      & iext(uri_rdf_first,X17,uri_ex_c3)
      & iext(uri_rdf_rest,X17,uri_rdf_nil)
      & iext(uri_rdf_type,X14,uri_owl_AllDisjointClasses)
      & iext(uri_owl_members,X14,X15)
      & iext(uri_rdf_first,X15,uri_ex_c1)
      & iext(uri_rdf_rest,X15,X16) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',conclusion_rdfbased_sem_ndis_alldisjointclasses_bw) ).

fof(24,axiom,
    ? [X17,X14,X16] :
      ( iext(uri_owl_disjointWith,uri_ex_c2,uri_ex_c3)
      & iext(uri_rdf_first,X16,uri_ex_c2)
      & iext(uri_rdf_rest,X16,X17)
      & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)
      & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c3)
      & iext(uri_rdf_first,X14,uri_ex_c1)
      & iext(uri_rdf_rest,X14,X16)
      & iext(uri_rdf_first,X17,uri_ex_c3)
      & iext(uri_rdf_rest,X17,uri_rdf_nil) ),
    file('/tmp/tmpbLT2nm/sel_SWB069+1.p_1',premise_rdfbased_sem_ndis_alldisjointclasses_bw) ).

fof(25,negated_conjecture,
    ~ ? [X14,X15,X16,X17] :
        ( iext(uri_rdf_first,X16,uri_ex_c2)
        & iext(uri_rdf_rest,X16,X17)
        & iext(uri_rdf_first,X17,uri_ex_c3)
        & iext(uri_rdf_rest,X17,uri_rdf_nil)
        & iext(uri_rdf_type,X14,uri_owl_AllDisjointClasses)
        & iext(uri_owl_members,X14,X15)
        & iext(uri_rdf_first,X15,uri_ex_c1)
        & iext(uri_rdf_rest,X15,X16) ),
    inference(assume_negation,[status(cth)],[23]) ).

fof(45,plain,
    ! [X4,X5,X6,X7] :
      ( ~ iext(uri_rdf_first,X4,X5)
      | ~ iext(uri_rdf_rest,X4,X6)
      | ~ iext(uri_rdf_first,X6,X7)
      | ~ iext(uri_rdf_rest,X6,uri_rdf_nil)
      | ? [X1] :
          ( icext(X5,X1)
          & icext(X7,X1) )
      | ? [X3] :
          ( icext(uri_owl_AllDisjointClasses,X3)
          & iext(uri_owl_members,X3,X4) ) ),
    inference(fof_nnf,[status(thm)],[5]) ).

fof(46,plain,
    ! [X8,X9,X10,X11] :
      ( ~ iext(uri_rdf_first,X8,X9)
      | ~ iext(uri_rdf_rest,X8,X10)
      | ~ iext(uri_rdf_first,X10,X11)
      | ~ iext(uri_rdf_rest,X10,uri_rdf_nil)
      | ? [X12] :
          ( icext(X9,X12)
          & icext(X11,X12) )
      | ? [X13] :
          ( icext(uri_owl_AllDisjointClasses,X13)
          & iext(uri_owl_members,X13,X8) ) ),
    inference(variable_rename,[status(thm)],[45]) ).

fof(47,plain,
    ! [X8,X9,X10,X11] :
      ( ~ iext(uri_rdf_first,X8,X9)
      | ~ iext(uri_rdf_rest,X8,X10)
      | ~ iext(uri_rdf_first,X10,X11)
      | ~ iext(uri_rdf_rest,X10,uri_rdf_nil)
      | ( icext(X9,esk3_4(X8,X9,X10,X11))
        & icext(X11,esk3_4(X8,X9,X10,X11)) )
      | ( icext(uri_owl_AllDisjointClasses,esk4_4(X8,X9,X10,X11))
        & iext(uri_owl_members,esk4_4(X8,X9,X10,X11),X8) ) ),
    inference(skolemize,[status(esa)],[46]) ).

fof(48,plain,
    ! [X8,X9,X10,X11] :
      ( ( icext(uri_owl_AllDisjointClasses,esk4_4(X8,X9,X10,X11))
        | icext(X9,esk3_4(X8,X9,X10,X11))
        | ~ iext(uri_rdf_first,X8,X9)
        | ~ iext(uri_rdf_rest,X8,X10)
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk4_4(X8,X9,X10,X11),X8)
        | icext(X9,esk3_4(X8,X9,X10,X11))
        | ~ iext(uri_rdf_first,X8,X9)
        | ~ iext(uri_rdf_rest,X8,X10)
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk4_4(X8,X9,X10,X11))
        | icext(X11,esk3_4(X8,X9,X10,X11))
        | ~ iext(uri_rdf_first,X8,X9)
        | ~ iext(uri_rdf_rest,X8,X10)
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk4_4(X8,X9,X10,X11),X8)
        | icext(X11,esk3_4(X8,X9,X10,X11))
        | ~ iext(uri_rdf_first,X8,X9)
        | ~ iext(uri_rdf_rest,X8,X10)
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,uri_rdf_nil) ) ),
    inference(distribute,[status(thm)],[47]) ).

cnf(49,plain,
    ( icext(X2,esk3_4(X3,X4,X1,X2))
    | iext(uri_owl_members,esk4_4(X3,X4,X1,X2),X3)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4) ),
    inference(split_conjunct,[status(thm)],[48]) ).

cnf(50,plain,
    ( icext(X2,esk3_4(X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk4_4(X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4) ),
    inference(split_conjunct,[status(thm)],[48]) ).

cnf(51,plain,
    ( icext(X4,esk3_4(X3,X4,X1,X2))
    | iext(uri_owl_members,esk4_4(X3,X4,X1,X2),X3)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4) ),
    inference(split_conjunct,[status(thm)],[48]) ).

cnf(52,plain,
    ( icext(X4,esk3_4(X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk4_4(X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4) ),
    inference(split_conjunct,[status(thm)],[48]) ).

fof(53,plain,
    ! [X4,X5,X6,X7,X8,X9] :
      ( ~ iext(uri_rdf_first,X4,X5)
      | ~ iext(uri_rdf_rest,X4,X6)
      | ~ iext(uri_rdf_first,X6,X7)
      | ~ iext(uri_rdf_rest,X6,X8)
      | ~ iext(uri_rdf_first,X8,X9)
      | ~ iext(uri_rdf_rest,X8,uri_rdf_nil)
      | ? [X1] :
          ( icext(X5,X1)
          & icext(X7,X1) )
      | ? [X1] :
          ( icext(X5,X1)
          & icext(X9,X1) )
      | ? [X1] :
          ( icext(X7,X1)
          & icext(X9,X1) )
      | ? [X3] :
          ( icext(uri_owl_AllDisjointClasses,X3)
          & iext(uri_owl_members,X3,X4) ) ),
    inference(fof_nnf,[status(thm)],[6]) ).

fof(54,plain,
    ! [X10,X11,X12,X13,X14,X15] :
      ( ~ iext(uri_rdf_first,X10,X11)
      | ~ iext(uri_rdf_rest,X10,X12)
      | ~ iext(uri_rdf_first,X12,X13)
      | ~ iext(uri_rdf_rest,X12,X14)
      | ~ iext(uri_rdf_first,X14,X15)
      | ~ iext(uri_rdf_rest,X14,uri_rdf_nil)
      | ? [X16] :
          ( icext(X11,X16)
          & icext(X13,X16) )
      | ? [X17] :
          ( icext(X11,X17)
          & icext(X15,X17) )
      | ? [X18] :
          ( icext(X13,X18)
          & icext(X15,X18) )
      | ? [X19] :
          ( icext(uri_owl_AllDisjointClasses,X19)
          & iext(uri_owl_members,X19,X10) ) ),
    inference(variable_rename,[status(thm)],[53]) ).

fof(55,plain,
    ! [X10,X11,X12,X13,X14,X15] :
      ( ~ iext(uri_rdf_first,X10,X11)
      | ~ iext(uri_rdf_rest,X10,X12)
      | ~ iext(uri_rdf_first,X12,X13)
      | ~ iext(uri_rdf_rest,X12,X14)
      | ~ iext(uri_rdf_first,X14,X15)
      | ~ iext(uri_rdf_rest,X14,uri_rdf_nil)
      | ( icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        & icext(X13,esk5_6(X10,X11,X12,X13,X14,X15)) )
      | ( icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        & icext(X15,esk6_6(X10,X11,X12,X13,X14,X15)) )
      | ( icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        & icext(X15,esk7_6(X10,X11,X12,X13,X14,X15)) )
      | ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        & iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10) ) ),
    inference(skolemize,[status(esa)],[54]) ).

fof(56,plain,
    ! [X10,X11,X12,X13,X14,X15] :
      ( ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X11,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X13,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( icext(uri_owl_AllDisjointClasses,esk8_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) )
      & ( iext(uri_owl_members,esk8_6(X10,X11,X12,X13,X14,X15),X10)
        | icext(X15,esk7_6(X10,X11,X12,X13,X14,X15))
        | icext(X15,esk6_6(X10,X11,X12,X13,X14,X15))
        | icext(X13,esk5_6(X10,X11,X12,X13,X14,X15))
        | ~ iext(uri_rdf_first,X10,X11)
        | ~ iext(uri_rdf_rest,X10,X12)
        | ~ iext(uri_rdf_first,X12,X13)
        | ~ iext(uri_rdf_rest,X12,X14)
        | ~ iext(uri_rdf_first,X14,X15)
        | ~ iext(uri_rdf_rest,X14,uri_rdf_nil) ) ),
    inference(distribute,[status(thm)],[55]) ).

cnf(57,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(58,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(59,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(60,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(61,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(62,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(63,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(64,plain,
    ( icext(X4,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(65,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(66,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(67,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(68,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(69,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(70,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X2,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(71,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | iext(uri_owl_members,esk8_6(X5,X6,X3,X4,X1,X2),X5)
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

cnf(72,plain,
    ( icext(X6,esk5_6(X5,X6,X3,X4,X1,X2))
    | icext(X6,esk6_6(X5,X6,X3,X4,X1,X2))
    | icext(X4,esk7_6(X5,X6,X3,X4,X1,X2))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X5,X6,X3,X4,X1,X2))
    | ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X5,X3)
    | ~ iext(uri_rdf_first,X5,X6) ),
    inference(split_conjunct,[status(thm)],[56]) ).

fof(75,plain,
    ! [X5,X7] :
      ( ( ~ iext(uri_owl_disjointWith,X5,X7)
        | ( ic(X5)
          & ic(X7)
          & ! [X1] :
              ( ~ icext(X5,X1)
              | ~ icext(X7,X1) ) ) )
      & ( ~ ic(X5)
        | ~ ic(X7)
        | ? [X1] :
            ( icext(X5,X1)
            & icext(X7,X1) )
        | iext(uri_owl_disjointWith,X5,X7) ) ),
    inference(fof_nnf,[status(thm)],[8]) ).

fof(76,plain,
    ! [X8,X9] :
      ( ( ~ iext(uri_owl_disjointWith,X8,X9)
        | ( ic(X8)
          & ic(X9)
          & ! [X10] :
              ( ~ icext(X8,X10)
              | ~ icext(X9,X10) ) ) )
      & ( ~ ic(X8)
        | ~ ic(X9)
        | ? [X11] :
            ( icext(X8,X11)
            & icext(X9,X11) )
        | iext(uri_owl_disjointWith,X8,X9) ) ),
    inference(variable_rename,[status(thm)],[75]) ).

fof(77,plain,
    ! [X8,X9] :
      ( ( ~ iext(uri_owl_disjointWith,X8,X9)
        | ( ic(X8)
          & ic(X9)
          & ! [X10] :
              ( ~ icext(X8,X10)
              | ~ icext(X9,X10) ) ) )
      & ( ~ ic(X8)
        | ~ ic(X9)
        | ( icext(X8,esk9_2(X8,X9))
          & icext(X9,esk9_2(X8,X9)) )
        | iext(uri_owl_disjointWith,X8,X9) ) ),
    inference(skolemize,[status(esa)],[76]) ).

fof(78,plain,
    ! [X8,X9,X10] :
      ( ( ( ( ~ icext(X8,X10)
            | ~ icext(X9,X10) )
          & ic(X8)
          & ic(X9) )
        | ~ iext(uri_owl_disjointWith,X8,X9) )
      & ( ~ ic(X8)
        | ~ ic(X9)
        | ( icext(X8,esk9_2(X8,X9))
          & icext(X9,esk9_2(X8,X9)) )
        | iext(uri_owl_disjointWith,X8,X9) ) ),
    inference(shift_quantors,[status(thm)],[77]) ).

fof(79,plain,
    ! [X8,X9,X10] :
      ( ( ~ icext(X8,X10)
        | ~ icext(X9,X10)
        | ~ iext(uri_owl_disjointWith,X8,X9) )
      & ( ic(X8)
        | ~ iext(uri_owl_disjointWith,X8,X9) )
      & ( ic(X9)
        | ~ iext(uri_owl_disjointWith,X8,X9) )
      & ( icext(X8,esk9_2(X8,X9))
        | ~ ic(X8)
        | ~ ic(X9)
        | iext(uri_owl_disjointWith,X8,X9) )
      & ( icext(X9,esk9_2(X8,X9))
        | ~ ic(X8)
        | ~ ic(X9)
        | iext(uri_owl_disjointWith,X8,X9) ) ),
    inference(distribute,[status(thm)],[78]) ).

cnf(84,plain,
    ( ~ iext(uri_owl_disjointWith,X1,X2)
    | ~ icext(X2,X3)
    | ~ icext(X1,X3) ),
    inference(split_conjunct,[status(thm)],[79]) ).

fof(91,plain,
    ! [X3,X4,X5,X6,X7] :
      ( ~ iext(uri_rdf_first,X4,X5)
      | ~ iext(uri_rdf_rest,X4,X6)
      | ~ iext(uri_rdf_first,X6,X7)
      | ~ iext(uri_rdf_rest,X6,uri_rdf_nil)
      | ~ icext(uri_owl_AllDisjointClasses,X3)
      | ~ iext(uri_owl_members,X3,X4)
      | ! [X1] :
          ( ~ icext(X5,X1)
          | ~ icext(X7,X1) ) ),
    inference(fof_nnf,[status(thm)],[11]) ).

fof(92,plain,
    ! [X8,X9,X10,X11,X12] :
      ( ~ iext(uri_rdf_first,X9,X10)
      | ~ iext(uri_rdf_rest,X9,X11)
      | ~ iext(uri_rdf_first,X11,X12)
      | ~ iext(uri_rdf_rest,X11,uri_rdf_nil)
      | ~ icext(uri_owl_AllDisjointClasses,X8)
      | ~ iext(uri_owl_members,X8,X9)
      | ! [X13] :
          ( ~ icext(X10,X13)
          | ~ icext(X12,X13) ) ),
    inference(variable_rename,[status(thm)],[91]) ).

fof(93,plain,
    ! [X8,X9,X10,X11,X12,X13] :
      ( ~ icext(X10,X13)
      | ~ icext(X12,X13)
      | ~ iext(uri_rdf_first,X9,X10)
      | ~ iext(uri_rdf_rest,X9,X11)
      | ~ iext(uri_rdf_first,X11,X12)
      | ~ iext(uri_rdf_rest,X11,uri_rdf_nil)
      | ~ icext(uri_owl_AllDisjointClasses,X8)
      | ~ iext(uri_owl_members,X8,X9) ),
    inference(shift_quantors,[status(thm)],[92]) ).

cnf(94,plain,
    ( ~ iext(uri_owl_members,X1,X2)
    | ~ icext(uri_owl_AllDisjointClasses,X1)
    | ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3)
    | ~ iext(uri_rdf_first,X2,X5)
    | ~ icext(X4,X6)
    | ~ icext(X5,X6) ),
    inference(split_conjunct,[status(thm)],[93]) ).

fof(125,plain,
    ! [X1,X13] :
      ( ( ~ iext(uri_rdf_type,X1,X13)
        | icext(X13,X1) )
      & ( ~ icext(X13,X1)
        | iext(uri_rdf_type,X1,X13) ) ),
    inference(fof_nnf,[status(thm)],[21]) ).

fof(126,plain,
    ! [X14,X15] :
      ( ( ~ iext(uri_rdf_type,X14,X15)
        | icext(X15,X14) )
      & ( ~ icext(X15,X14)
        | iext(uri_rdf_type,X14,X15) ) ),
    inference(variable_rename,[status(thm)],[125]) ).

cnf(127,plain,
    ( iext(uri_rdf_type,X1,X2)
    | ~ icext(X2,X1) ),
    inference(split_conjunct,[status(thm)],[126]) ).

cnf(128,plain,
    ( icext(X1,X2)
    | ~ iext(uri_rdf_type,X2,X1) ),
    inference(split_conjunct,[status(thm)],[126]) ).

fof(130,negated_conjecture,
    ! [X14,X15,X16,X17] :
      ( ~ iext(uri_rdf_first,X16,uri_ex_c2)
      | ~ iext(uri_rdf_rest,X16,X17)
      | ~ iext(uri_rdf_first,X17,uri_ex_c3)
      | ~ iext(uri_rdf_rest,X17,uri_rdf_nil)
      | ~ iext(uri_rdf_type,X14,uri_owl_AllDisjointClasses)
      | ~ iext(uri_owl_members,X14,X15)
      | ~ iext(uri_rdf_first,X15,uri_ex_c1)
      | ~ iext(uri_rdf_rest,X15,X16) ),
    inference(fof_nnf,[status(thm)],[25]) ).

fof(131,negated_conjecture,
    ! [X18,X19,X20,X21] :
      ( ~ iext(uri_rdf_first,X20,uri_ex_c2)
      | ~ iext(uri_rdf_rest,X20,X21)
      | ~ iext(uri_rdf_first,X21,uri_ex_c3)
      | ~ iext(uri_rdf_rest,X21,uri_rdf_nil)
      | ~ iext(uri_rdf_type,X18,uri_owl_AllDisjointClasses)
      | ~ iext(uri_owl_members,X18,X19)
      | ~ iext(uri_rdf_first,X19,uri_ex_c1)
      | ~ iext(uri_rdf_rest,X19,X20) ),
    inference(variable_rename,[status(thm)],[130]) ).

cnf(132,negated_conjecture,
    ( ~ iext(uri_rdf_rest,X1,X2)
    | ~ iext(uri_rdf_first,X1,uri_ex_c1)
    | ~ iext(uri_owl_members,X3,X1)
    | ~ iext(uri_rdf_type,X3,uri_owl_AllDisjointClasses)
    | ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X4,uri_ex_c3)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_first,X2,uri_ex_c2) ),
    inference(split_conjunct,[status(thm)],[131]) ).

fof(133,plain,
    ? [X18,X19,X20] :
      ( iext(uri_owl_disjointWith,uri_ex_c2,uri_ex_c3)
      & iext(uri_rdf_first,X20,uri_ex_c2)
      & iext(uri_rdf_rest,X20,X18)
      & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)
      & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c3)
      & iext(uri_rdf_first,X19,uri_ex_c1)
      & iext(uri_rdf_rest,X19,X20)
      & iext(uri_rdf_first,X18,uri_ex_c3)
      & iext(uri_rdf_rest,X18,uri_rdf_nil) ),
    inference(variable_rename,[status(thm)],[24]) ).

fof(134,plain,
    ( iext(uri_owl_disjointWith,uri_ex_c2,uri_ex_c3)
    & iext(uri_rdf_first,esk13_0,uri_ex_c2)
    & iext(uri_rdf_rest,esk13_0,esk11_0)
    & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)
    & iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c3)
    & iext(uri_rdf_first,esk12_0,uri_ex_c1)
    & iext(uri_rdf_rest,esk12_0,esk13_0)
    & iext(uri_rdf_first,esk11_0,uri_ex_c3)
    & iext(uri_rdf_rest,esk11_0,uri_rdf_nil) ),
    inference(skolemize,[status(esa)],[133]) ).

cnf(135,plain,
    iext(uri_rdf_rest,esk11_0,uri_rdf_nil),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(136,plain,
    iext(uri_rdf_first,esk11_0,uri_ex_c3),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(137,plain,
    iext(uri_rdf_rest,esk12_0,esk13_0),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(138,plain,
    iext(uri_rdf_first,esk12_0,uri_ex_c1),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(139,plain,
    iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c3),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(140,plain,
    iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(141,plain,
    iext(uri_rdf_rest,esk13_0,esk11_0),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(142,plain,
    iext(uri_rdf_first,esk13_0,uri_ex_c2),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(143,plain,
    iext(uri_owl_disjointWith,uri_ex_c2,uri_ex_c3),
    inference(split_conjunct,[status(thm)],[134]) ).

cnf(175,plain,
    ( ~ icext(uri_ex_c3,X1)
    | ~ icext(uri_ex_c2,X1) ),
    inference(spm,[status(thm)],[84,143,theory(equality)]) ).

cnf(176,plain,
    ( ~ icext(uri_ex_c2,X1)
    | ~ icext(uri_ex_c1,X1) ),
    inference(spm,[status(thm)],[84,140,theory(equality)]) ).

cnf(177,plain,
    ( ~ icext(uri_ex_c3,X1)
    | ~ icext(uri_ex_c1,X1) ),
    inference(spm,[status(thm)],[84,139,theory(equality)]) ).

cnf(183,plain,
    ( ~ icext(uri_owl_AllDisjointClasses,X1)
    | ~ icext(X2,X3)
    | ~ icext(X4,X3)
    | ~ iext(uri_owl_members,X1,X5)
    | ~ iext(uri_rdf_first,esk11_0,X4)
    | ~ iext(uri_rdf_first,X5,X2)
    | ~ iext(uri_rdf_rest,X5,esk11_0) ),
    inference(spm,[status(thm)],[94,135,theory(equality)]) ).

cnf(184,negated_conjecture,
    ( ~ iext(uri_rdf_first,esk11_0,uri_ex_c3)
    | ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_first,X2,uri_ex_c1)
    | ~ iext(uri_rdf_type,X3,uri_owl_AllDisjointClasses)
    | ~ iext(uri_owl_members,X3,X2)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,X2,X1) ),
    inference(spm,[status(thm)],[132,135,theory(equality)]) ).

cnf(185,negated_conjecture,
    ( $false
    | ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_first,X2,uri_ex_c1)
    | ~ iext(uri_rdf_type,X3,uri_owl_AllDisjointClasses)
    | ~ iext(uri_owl_members,X3,X2)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,X2,X1) ),
    inference(rw,[status(thm)],[184,136,theory(equality)]) ).

cnf(186,negated_conjecture,
    ( ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_first,X2,uri_ex_c1)
    | ~ iext(uri_rdf_type,X3,uri_owl_AllDisjointClasses)
    | ~ iext(uri_owl_members,X3,X2)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,X2,X1) ),
    inference(cn,[status(thm)],[185,theory(equality)]) ).

cnf(187,plain,
    ( icext(X1,esk3_4(X2,X1,esk11_0,X3))
    | iext(uri_owl_members,esk4_4(X2,X1,esk11_0,X3),X2)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_rest,X2,esk11_0) ),
    inference(spm,[status(thm)],[51,135,theory(equality)]) ).

cnf(188,plain,
    ( icext(X1,esk3_4(X2,X3,esk11_0,X1))
    | iext(uri_owl_members,esk4_4(X2,X3,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,esk11_0) ),
    inference(spm,[status(thm)],[49,135,theory(equality)]) ).

cnf(189,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(X1,X2,esk11_0,X3))
    | icext(X2,esk3_4(X1,X2,esk11_0,X3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk11_0) ),
    inference(spm,[status(thm)],[52,135,theory(equality)]) ).

cnf(190,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(X1,X2,esk11_0,X3))
    | icext(X3,esk3_4(X1,X2,esk11_0,X3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk11_0) ),
    inference(spm,[status(thm)],[50,135,theory(equality)]) ).

cnf(191,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X1,esk11_0,X5))
    | icext(X3,esk6_6(X2,X3,X4,X1,esk11_0,X5))
    | icext(X3,esk5_6(X2,X3,X4,X1,esk11_0,X5))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X1,esk11_0,X5),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X1)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[71,135,theory(equality)]) ).

cnf(192,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X3,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X3,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[69,135,theory(equality)]) ).

cnf(196,plain,
    ( icext(X1,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X5,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X3,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[67,135,theory(equality)]) ).

cnf(197,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X1,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X3,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[65,135,theory(equality)]) ).

cnf(198,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X1,esk11_0,X5))
    | icext(X1,esk5_6(X2,X3,X4,X1,esk11_0,X5))
    | icext(X3,esk6_6(X2,X3,X4,X1,esk11_0,X5))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X1,esk11_0,X5),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X1)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[63,135,theory(equality)]) ).

cnf(199,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X5,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X3,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[61,135,theory(equality)]) ).

cnf(200,plain,
    ( icext(X1,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X5,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X5,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[59,135,theory(equality)]) ).

cnf(201,plain,
    ( icext(X1,esk7_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X1,esk6_6(X2,X3,X4,X5,esk11_0,X1))
    | icext(X5,esk5_6(X2,X3,X4,X5,esk11_0,X1))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X5,esk11_0,X1),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X5)
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_rest,X2,X4)
    | ~ iext(uri_rdf_rest,X4,esk11_0) ),
    inference(spm,[status(thm)],[57,135,theory(equality)]) ).

cnf(202,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[72,135,theory(equality)]) ).

cnf(203,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[70,135,theory(equality)]) ).

cnf(204,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[68,135,theory(equality)]) ).

cnf(205,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[66,135,theory(equality)]) ).

cnf(206,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[64,135,theory(equality)]) ).

cnf(207,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[62,135,theory(equality)]) ).

cnf(208,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[60,135,theory(equality)]) ).

cnf(209,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk7_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X5,esk6_6(X1,X2,X3,X4,esk11_0,X5))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,X5))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_first,esk11_0,X5)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_rest,X3,esk11_0) ),
    inference(spm,[status(thm)],[58,135,theory(equality)]) ).

cnf(211,plain,
    ( ~ icext(uri_ex_c2,X1)
    | ~ iext(uri_rdf_type,X1,uri_ex_c3) ),
    inference(spm,[status(thm)],[175,128,theory(equality)]) ).

cnf(238,plain,
    ( ~ icext(uri_ex_c3,X1)
    | ~ iext(uri_rdf_type,X1,uri_ex_c1) ),
    inference(spm,[status(thm)],[177,128,theory(equality)]) ).

cnf(421,plain,
    ( icext(X1,esk3_4(X2,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk4_4(X2,X1,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X2,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1) ),
    inference(spm,[status(thm)],[187,136,theory(equality)]) ).

cnf(449,plain,
    ( icext(uri_ex_c3,esk3_4(X1,X2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk4_4(X1,X2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[188,136,theory(equality)]) ).

cnf(483,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(X1,X2,esk11_0,uri_ex_c3))
    | icext(X2,esk3_4(X1,X2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[189,136,theory(equality)]) ).

cnf(508,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(X1,X2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk3_4(X1,X2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[190,136,theory(equality)]) ).

cnf(555,plain,
    ( icext(X1,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[191,136,theory(equality)]) ).

cnf(582,plain,
    ( icext(X1,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[192,136,theory(equality)]) ).

cnf(698,plain,
    ( icext(X1,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[196,136,theory(equality)]) ).

cnf(707,plain,
    ( icext(X1,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[197,136,theory(equality)]) ).

cnf(718,plain,
    ( icext(X1,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[198,136,theory(equality)]) ).

cnf(728,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,X1,esk11_0,uri_ex_c3))
    | icext(X1,esk3_4(esk13_0,X1,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(spm,[status(thm)],[483,141,theory(equality)]) ).

cnf(729,plain,
    ( icext(X1,esk6_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X2,X1,X3,X4,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,X3,X4,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X2,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X2,X3) ),
    inference(spm,[status(thm)],[199,136,theory(equality)]) ).

cnf(750,plain,
    ( icext(X1,esk5_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | icext(X1,esk7_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X1,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X4,esk11_0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X1)
    | ~ iext(uri_rdf_rest,X2,X4) ),
    inference(spm,[status(thm)],[200,136,theory(equality)]) ).

cnf(792,plain,
    ( icext(X1,esk5_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X2,X3,X4,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X3,X4,X1,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X4,esk11_0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,X4,X1)
    | ~ iext(uri_rdf_rest,X2,X4) ),
    inference(spm,[status(thm)],[201,136,theory(equality)]) ).

cnf(804,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[202,136,theory(equality)]) ).

cnf(824,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[203,136,theory(equality)]) ).

cnf(828,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(X1,X2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c2,esk3_4(X1,X2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[175,508,theory(equality)]) ).

cnf(836,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk3_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[728,142,theory(equality)]) ).

cnf(837,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[204,136,theory(equality)]) ).

cnf(867,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[205,136,theory(equality)]) ).

cnf(890,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,esk13_0,esk11_0)
    | ~ iext(uri_rdf_first,esk13_0,uri_ex_c2) ),
    inference(spm,[status(thm)],[828,836,theory(equality)]) ).

cnf(891,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false
    | ~ iext(uri_rdf_first,esk13_0,uri_ex_c2) ),
    inference(rw,[status(thm)],[890,141,theory(equality)]) ).

cnf(892,plain,
    ( icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false
    | $false ),
    inference(rw,[status(thm)],[891,142,theory(equality)]) ).

cnf(893,plain,
    icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)),
    inference(cn,[status(thm)],[892,theory(equality)]) ).

cnf(894,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[206,136,theory(equality)]) ).

cnf(937,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[207,136,theory(equality)]) ).

cnf(962,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[208,136,theory(equality)]) ).

cnf(967,plain,
    ( icext(uri_ex_c3,esk3_4(esk13_0,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk4_4(esk13_0,X1,esk11_0,uri_ex_c3),esk13_0)
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(spm,[status(thm)],[449,141,theory(equality)]) ).

cnf(969,plain,
    ( iext(uri_owl_members,esk4_4(esk13_0,X1,esk11_0,uri_ex_c3),esk13_0)
    | ~ icext(uri_ex_c2,esk3_4(esk13_0,X1,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(spm,[status(thm)],[175,967,theory(equality)]) ).

cnf(974,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(X4,esk5_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,X3,X4,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X3,esk11_0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3) ),
    inference(spm,[status(thm)],[209,136,theory(equality)]) ).

cnf(987,plain,
    ( icext(X1,esk3_4(esk13_0,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk4_4(esk13_0,X1,esk11_0,uri_ex_c3),esk13_0)
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(spm,[status(thm)],[421,141,theory(equality)]) ).

cnf(1069,plain,
    ( iext(uri_owl_members,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk13_0)
    | ~ iext(uri_rdf_first,esk13_0,uri_ex_c2) ),
    inference(spm,[status(thm)],[969,987,theory(equality)]) ).

cnf(1081,plain,
    ( iext(uri_owl_members,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk13_0)
    | $false ),
    inference(rw,[status(thm)],[1069,142,theory(equality)]) ).

cnf(1082,plain,
    iext(uri_owl_members,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk13_0),
    inference(cn,[status(thm)],[1081,theory(equality)]) ).

cnf(1085,plain,
    ( ~ icext(uri_owl_AllDisjointClasses,esk4_4(esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(X1,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_rest,esk13_0,esk11_0)
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(spm,[status(thm)],[183,1082,theory(equality)]) ).

cnf(1087,plain,
    ( $false
    | ~ icext(X1,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_rest,esk13_0,esk11_0)
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(rw,[status(thm)],[1085,893,theory(equality)]) ).

cnf(1088,plain,
    ( $false
    | ~ icext(X1,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | $false
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(rw,[status(thm)],[1087,141,theory(equality)]) ).

cnf(1089,plain,
    ( ~ icext(X1,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,esk11_0,X3)
    | ~ iext(uri_rdf_first,esk13_0,X1) ),
    inference(cn,[status(thm)],[1088,theory(equality)]) ).

cnf(1090,plain,
    ( icext(X1,esk7_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | icext(X3,esk6_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,esk13_0,X1)
    | ~ iext(uri_rdf_rest,X2,esk13_0) ),
    inference(spm,[status(thm)],[555,141,theory(equality)]) ).

cnf(1108,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[582,141,theory(equality)]) ).

cnf(1218,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[698,141,theory(equality)]) ).

cnf(1229,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[707,141,theory(equality)]) ).

cnf(1243,plain,
    ( icext(X1,esk7_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | icext(X3,esk6_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X3,esk13_0,X1,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_rdf_first,esk13_0,X1)
    | ~ iext(uri_rdf_rest,X2,esk13_0) ),
    inference(spm,[status(thm)],[718,141,theory(equality)]) ).

cnf(1272,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[729,141,theory(equality)]) ).

cnf(1318,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[750,141,theory(equality)]) ).

cnf(1371,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[792,141,theory(equality)]) ).

cnf(1395,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[804,141,theory(equality)]) ).

cnf(1414,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[824,141,theory(equality)]) ).

cnf(1595,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[837,141,theory(equality)]) ).

cnf(1781,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[867,141,theory(equality)]) ).

cnf(1823,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[894,141,theory(equality)]) ).

cnf(1964,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[937,141,theory(equality)]) ).

cnf(2028,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[962,141,theory(equality)]) ).

cnf(2064,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | icext(X3,esk5_6(X1,X2,esk13_0,X3,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_first,esk13_0,X3)
    | ~ iext(uri_rdf_rest,X1,esk13_0) ),
    inference(spm,[status(thm)],[974,141,theory(equality)]) ).

cnf(2237,plain,
    ( icext(X1,esk5_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X2,esk13_0)
    | ~ iext(uri_rdf_first,X2,X1) ),
    inference(spm,[status(thm)],[1090,142,theory(equality)]) ).

cnf(2413,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1108,142,theory(equality)]) ).

cnf(2570,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1218,142,theory(equality)]) ).

cnf(2608,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1229,142,theory(equality)]) ).

cnf(2632,plain,
    ( icext(X1,esk6_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X2,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X2,esk13_0)
    | ~ iext(uri_rdf_first,X2,X1) ),
    inference(spm,[status(thm)],[1243,142,theory(equality)]) ).

cnf(2659,plain,
    ( icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1272,142,theory(equality)]) ).

cnf(2701,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1318,142,theory(equality)]) ).

cnf(2718,plain,
    ( icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1371,142,theory(equality)]) ).

cnf(2733,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1395,142,theory(equality)]) ).

cnf(2747,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1414,142,theory(equality)]) ).

cnf(3318,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1595,142,theory(equality)]) ).

cnf(3660,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1781,142,theory(equality)]) ).

cnf(3747,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1823,142,theory(equality)]) ).

cnf(3971,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X2,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[1964,142,theory(equality)]) ).

cnf(3988,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[2028,142,theory(equality)]) ).

cnf(4044,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[2064,142,theory(equality)]) ).

cnf(4748,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2237,137,theory(equality)]) ).

cnf(4968,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2413,137,theory(equality)]) ).

cnf(5008,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2570,137,theory(equality)]) ).

cnf(5049,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2608,137,theory(equality)]) ).

cnf(5081,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2632,137,theory(equality)]) ).

cnf(5109,plain,
    ( icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2659,137,theory(equality)]) ).

cnf(5131,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2701,137,theory(equality)]) ).

cnf(5162,plain,
    ( icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2718,137,theory(equality)]) ).

cnf(5199,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2733,137,theory(equality)]) ).

cnf(5236,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[2747,137,theory(equality)]) ).

cnf(5290,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[3318,137,theory(equality)]) ).

cnf(5391,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[3660,137,theory(equality)]) ).

cnf(5430,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[3747,137,theory(equality)]) ).

cnf(5452,plain,
    ( icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(X1,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[3971,137,theory(equality)]) ).

cnf(5563,plain,
    ( icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c2,esk7_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[175,4044,theory(equality)]) ).

cnf(5602,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[4748,138,theory(equality)]) ).

cnf(5683,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[4968,138,theory(equality)]) ).

cnf(5690,plain,
    ( icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[5008,138,theory(equality)]) ).

cnf(5730,plain,
    ( icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[5049,138,theory(equality)]) ).

cnf(5746,plain,
    ( icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[5081,138,theory(equality)]) ).

cnf(5760,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(spm,[status(thm)],[5109,138,theory(equality)]) ).

cnf(5803,plain,
    ( icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c2,esk7_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(spm,[status(thm)],[175,5162,theory(equality)]) ).

cnf(5842,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5199,138,theory(equality)]) ).

cnf(5878,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5236,138,theory(equality)]) ).

cnf(5918,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5290,138,theory(equality)]) ).

cnf(6690,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5391,138,theory(equality)]) ).

cnf(6713,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5430,138,theory(equality)]) ).

cnf(6728,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c1,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[5452,138,theory(equality)]) ).

cnf(6812,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5602,theory(equality)]) ).

cnf(8280,plain,
    ( icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(csr,[status(thm)],[5563,3988]) ).

cnf(8283,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk6_6(X1,X2,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1)
    | ~ iext(uri_rdf_rest,X1,esk13_0)
    | ~ iext(uri_rdf_first,X1,X2) ),
    inference(spm,[status(thm)],[238,8280,theory(equality)]) ).

cnf(8376,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5683,theory(equality)]) ).

cnf(8642,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5746,theory(equality)]) ).

cnf(8687,plain,
    ( icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5760,theory(equality)]) ).

cnf(8797,plain,
    ( icext(uri_ex_c3,esk6_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,X1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk12_0,X1) ),
    inference(csr,[status(thm)],[5803,5131]) ).

cnf(8878,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5842,theory(equality)]) ).

cnf(8916,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,5878,theory(equality)]) ).

cnf(14830,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[177,6713,theory(equality)]) ).

cnf(14900,plain,
    ( iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[127,6728,theory(equality)]) ).

cnf(15815,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(csr,[status(thm)],[6812,5690]) ).

cnf(15817,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[176,15815,theory(equality)]) ).

cnf(25801,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(csr,[status(thm)],[8376,5730]) ).

cnf(25803,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[176,25801,theory(equality)]) ).

cnf(28542,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(csr,[status(thm)],[8642,15817]) ).

cnf(28545,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(spm,[status(thm)],[28542,8797,theory(equality)]) ).

cnf(28549,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false ),
    inference(rw,[status(thm)],[28545,138,theory(equality)]) ).

cnf(28550,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[28549,theory(equality)]) ).

cnf(28923,plain,
    ( icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0) ),
    inference(csr,[status(thm)],[28550,15817]) ).

cnf(28928,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_first,esk13_0,uri_ex_c2) ),
    inference(spm,[status(thm)],[1089,28923,theory(equality)]) ).

cnf(28951,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | $false ),
    inference(rw,[status(thm)],[28928,142,theory(equality)]) ).

cnf(28952,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1) ),
    inference(cn,[status(thm)],[28951,theory(equality)]) ).

cnf(29203,plain,
    ( icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(csr,[status(thm)],[8687,25803]) ).

cnf(29337,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk11_0,uri_ex_c3)
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[28952,25803,theory(equality)]) ).

cnf(29341,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ iext(uri_rdf_first,esk11_0,uri_ex_c3)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[28952,29203,theory(equality)]) ).

cnf(29352,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | $false
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(rw,[status(thm)],[29337,136,theory(equality)]) ).

cnf(29353,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[29352,theory(equality)]) ).

cnf(29358,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | $false
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(rw,[status(thm)],[29341,136,theory(equality)]) ).

cnf(29359,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | ~ icext(uri_ex_c3,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[29358,theory(equality)]) ).

cnf(29544,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(spm,[status(thm)],[29359,8797,theory(equality)]) ).

cnf(29548,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false ),
    inference(rw,[status(thm)],[29544,138,theory(equality)]) ).

cnf(29549,plain,
    ( iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0)
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[29548,theory(equality)]) ).

cnf(29550,plain,
    iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),esk12_0),
    inference(csr,[status(thm)],[29549,29353]) ).

cnf(30942,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(csr,[status(thm)],[8878,5918]) ).

cnf(30944,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[176,30942,theory(equality)]) ).

cnf(31451,plain,
    ( icext(uri_ex_c1,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(csr,[status(thm)],[8916,6690]) ).

cnf(31453,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c3,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[176,31451,theory(equality)]) ).

cnf(46338,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_rest,esk12_0,esk13_0)
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(spm,[status(thm)],[14830,8280,theory(equality)]) ).

cnf(46340,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(rw,[status(thm)],[46338,137,theory(equality)]) ).

cnf(46341,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false
    | $false ),
    inference(rw,[status(thm)],[46340,138,theory(equality)]) ).

cnf(46342,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[46341,theory(equality)]) ).

cnf(47329,plain,
    ( iext(uri_rdf_type,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c3)
    | icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1) ),
    inference(spm,[status(thm)],[127,14900,theory(equality)]) ).

cnf(92114,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(csr,[status(thm)],[46342,30944]) ).

cnf(92116,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c3) ),
    inference(spm,[status(thm)],[211,92114,theory(equality)]) ).

cnf(92119,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | ~ iext(uri_rdf_first,esk13_0,uri_ex_c2) ),
    inference(spm,[status(thm)],[1089,92114,theory(equality)]) ).

cnf(92136,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1)
    | $false ),
    inference(rw,[status(thm)],[92119,142,theory(equality)]) ).

cnf(92137,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(X1,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,X1) ),
    inference(cn,[status(thm)],[92136,theory(equality)]) ).

cnf(98585,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_first,esk11_0,uri_ex_c3)
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(spm,[status(thm)],[92137,31453,theory(equality)]) ).

cnf(98606,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | $false
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(rw,[status(thm)],[98585,136,theory(equality)]) ).

cnf(98607,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)) ),
    inference(cn,[status(thm)],[98606,theory(equality)]) ).

cnf(98916,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1)
    | ~ iext(uri_rdf_rest,esk12_0,esk13_0)
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(spm,[status(thm)],[98607,8283,theory(equality)]) ).

cnf(98946,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1)
    | $false
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1) ),
    inference(rw,[status(thm)],[98916,137,theory(equality)]) ).

cnf(98947,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1)
    | $false
    | $false ),
    inference(rw,[status(thm)],[98946,138,theory(equality)]) ).

cnf(98948,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | ~ iext(uri_rdf_type,esk6_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c1) ),
    inference(cn,[status(thm)],[98947,theory(equality)]) ).

cnf(113627,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | icext(uri_ex_c2,esk5_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_rdf_type,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c3) ),
    inference(csr,[status(thm)],[47329,98948]) ).

cnf(113628,plain,
    ( icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3))
    | iext(uri_rdf_type,esk7_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_ex_c3) ),
    inference(csr,[status(thm)],[113627,98607]) ).

cnf(113629,plain,
    icext(uri_owl_AllDisjointClasses,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3)),
    inference(csr,[status(thm)],[113628,92116]) ).

cnf(113630,plain,
    iext(uri_rdf_type,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),uri_owl_AllDisjointClasses),
    inference(spm,[status(thm)],[127,113629,theory(equality)]) ).

cnf(114214,negated_conjecture,
    ( ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_first,X2,uri_ex_c1)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_owl_members,esk8_6(esk12_0,uri_ex_c1,esk13_0,uri_ex_c2,esk11_0,uri_ex_c3),X2)
    | ~ iext(uri_rdf_rest,X2,X1) ),
    inference(spm,[status(thm)],[186,113630,theory(equality)]) ).

cnf(116769,negated_conjecture,
    ( ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_first,esk12_0,uri_ex_c1)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,esk12_0,X1) ),
    inference(spm,[status(thm)],[114214,29550,theory(equality)]) ).

cnf(116770,negated_conjecture,
    ( ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | $false
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,esk12_0,X1) ),
    inference(rw,[status(thm)],[116769,138,theory(equality)]) ).

cnf(116771,negated_conjecture,
    ( ~ iext(uri_rdf_first,X1,uri_ex_c2)
    | ~ iext(uri_rdf_rest,X1,esk11_0)
    | ~ iext(uri_rdf_rest,esk12_0,X1) ),
    inference(cn,[status(thm)],[116770,theory(equality)]) ).

cnf(116772,negated_conjecture,
    ( ~ iext(uri_rdf_first,esk13_0,uri_ex_c2)
    | ~ iext(uri_rdf_rest,esk12_0,esk13_0) ),
    inference(spm,[status(thm)],[116771,141,theory(equality)]) ).

cnf(116773,negated_conjecture,
    ( $false
    | ~ iext(uri_rdf_rest,esk12_0,esk13_0) ),
    inference(rw,[status(thm)],[116772,142,theory(equality)]) ).

cnf(116774,negated_conjecture,
    ( $false
    | $false ),
    inference(rw,[status(thm)],[116773,137,theory(equality)]) ).

cnf(116775,negated_conjecture,
    $false,
    inference(cn,[status(thm)],[116774,theory(equality)]) ).

cnf(116776,negated_conjecture,
    $false,
    116775,
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWB/SWB069+1.p
% --creating new selector for [SWB001+0.ax]
% -running prover on /tmp/tmpbLT2nm/sel_SWB069+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWB069+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWB/SWB069+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWB/SWB069+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
% 
%------------------------------------------------------------------------------