↑ Up

Vampire---5.0.1.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SCT151+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 12:37:01 PM UTC 2026

% Result   : Theorem 8.47s 2.07s
% Output   : Refutation 8.92s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   42
%            Number of leaves      :   19
% Syntax   : Number of formulae    :  183 (  36 unt;  10 def)
%            Number of atoms       :  906 ( 232 equ)
%            Maximal formula atoms :   14 (   4 avg)
%            Number of connectives : 1118 ( 395   ~; 684   |;   8   &)
%                                         (  10 <=>;  16  =>;   0  <=;   5 <~>)
%            Maximal formula depth :   18 (   7 avg)
%            Maximal term depth    :    5 (   1 avg)
%            Number of predicates  :    5 (   3 usr;   3 prp; 0-3 aty)
%            Number of functors    :   26 (  26 usr;  18 con; 0-6 aty)
%            Number of variables   :  338 (   0 sgn 332   !;   6   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f4,axiom,
    v_a____ != v_b____,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_A_I1_J) ).

fof(f5,axiom,
    v_b____ != v_c____,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_A_I2_J) ).

fof(f7,axiom,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),X0))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062_Iconverse_Ao_AP_J_Ai_092_060_094esub_062_Aa_J_A_061_A_Ib_A_060_092_060_094bsub_062P_H_Ai_092_060_094esub_062_Ac_J_096) ).

fof(f9,axiom,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),c_Arrow__Order__Mirabelle_OProf),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_cP) ).

fof(f10,axiom,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_A_I5_J) ).

fof(f28,axiom,
    ! [X0,X1,X2,X3,X4,X5] :
      ( X5 != X4
     => ( X3 != X2
       => ( X5 != X2
         => ( X4 != X3
           => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
             => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
               => ( ! [X6] :
                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
                 => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
                   => c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__C1_C) ).

fof(f29,axiom,
    ! [X0,X1,X2,X3,X4,X5] :
      ( X5 != X4
     => ( X3 != X2
       => ( X5 != X2
         => ( X4 != X3
           => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
             => ( c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
               => ( ! [X6] :
                      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
                    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
                 => ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
                  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__C2_C) ).

fof(f106,axiom,
    ! [X0,X1,X2,X3,X4,X5,X6] :
      ( c_Fun_Ocomp(X6,X5,X4,X3,X2) = X1
     => hAPP(X3,hAPP(X2,X0)) = hAPP(X1,X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_o__eq__dest__lhs) ).

fof(f519,conjecture,
    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____)))
  <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

fof(f520,negated_conjecture,
    ~ ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____)))
    <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____)) ),
    inference(negated_conjecture,[status(cth)],[f519]) ).

fof(f564,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ? [X6] :
          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
        <~> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(ennf_transformation,[],[f28]) ).

fof(f565,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ? [X6] :
          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
        <~> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(flattening,[],[f564]) ).

fof(f566,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) )
      | ? [X6] :
          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
        <~> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(ennf_transformation,[],[f29]) ).

fof(f567,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      <=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) )
      | ? [X6] :
          ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6))
        <~> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6)) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(flattening,[],[f566]) ).

fof(f646,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] :
      ( hAPP(X3,hAPP(X2,X0)) = hAPP(X1,X0)
      | c_Fun_Ocomp(X6,X5,X4,X3,X2) != X1 ),
    inference(ennf_transformation,[],[f106]) ).

fof(f1006,plain,
    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____)))
  <~> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____)) ),
    inference(ennf_transformation,[],[f520]) ).

fof(f1012,plain,
    ! [X0] :
      ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),X0))
        | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) )
      & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0))
        | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),X0)) ) ),
    inference(nnf_transformation,[],[f7]) ).

fof(f1025,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ? [X6] :
          ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6))
            | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6)) )
          & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6))
            | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6)) ) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(nnf_transformation,[],[f565]) ).

fof(f1026,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK4(X0,X1,X2,X3,X4,X5)))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK4(X0,X1,X2,X3,X4,X5))) )
        & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK4(X0,X1,X2,X3,X4,X5)))
          | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK4(X0,X1,X2,X3,X4,X5))) ) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X6,sK4(X0,X1,X2,X3,X4,X5))],[f1025]) ).

fof(f1027,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) )
        & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1)) ) )
      | ? [X6] :
          ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6))
            | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6)) )
          & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,X6))
            | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,X6)) ) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(nnf_transformation,[],[f567]) ).

fof(f1028,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0)) )
        & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1)) ) )
      | ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK5(X0,X1,X2,X3,X4,X5)))
          | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK5(X0,X1,X2,X3,X4,X5))) )
        & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK5(X0,X1,X2,X3,X4,X5)))
          | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK5(X0,X1,X2,X3,X4,X5))) ) )
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X6,sK5(X0,X1,X2,X3,X4,X5))],[f1027]) ).

fof(f1213,plain,
    ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____))) )
    & ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____))) ) ),
    inference(nnf_transformation,[],[f1006]) ).

fof(f1217,plain,
    v_a____ != v_b____,
    inference(cnf_transformation,[],[f4]) ).

fof(f1218,plain,
    v_b____ != v_c____,
    inference(cnf_transformation,[],[f5]) ).

fof(f1220,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),X0)) ),
    inference(cnf_transformation,[],[f1012]) ).

fof(f1221,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(cnf_transformation,[],[f1012]) ).

fof(f1224,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____),c_Arrow__Order__Mirabelle_OProf),
    inference(cnf_transformation,[],[f9]) ).

fof(f1225,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    inference(cnf_transformation,[],[f10]) ).

fof(f1265,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK4(X0,X1,X2,X3,X4,X5)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK4(X0,X1,X2,X3,X4,X5)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(cnf_transformation,[],[f1026]) ).

fof(f1266,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK4(X0,X1,X2,X3,X4,X5)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK4(X0,X1,X2,X3,X4,X5)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(cnf_transformation,[],[f1026]) ).

fof(f1269,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK5(X0,X1,X2,X3,X4,X5)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK5(X0,X1,X2,X3,X4,X5)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(cnf_transformation,[],[f1028]) ).

fof(f1270,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(X1,sK5(X0,X1,X2,X3,X4,X5)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X0,sK5(X0,X1,X2,X3,X4,X5)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X4),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | X3 = X4
      | X2 = X5
      | X2 = X3
      | X4 = X5 ),
    inference(cnf_transformation,[],[f1028]) ).

fof(f1426,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] :
      ( hAPP(X1,X0) = hAPP(X3,hAPP(X2,X0))
      | c_Fun_Ocomp(X6,X5,X4,X3,X2) != X1 ),
    inference(cnf_transformation,[],[f646]) ).

fof(f1949,plain,
    ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____))
    | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____))) ),
    inference(cnf_transformation,[],[f1213]) ).

fof(f1950,plain,
    ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_F,v_P_H____))
    | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_F,c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____))) ),
    inference(cnf_transformation,[],[f1213]) ).

fof(f2074,plain,
    ! [X2,X3,X0,X6,X4,X5] : hAPP(X3,hAPP(X2,X0)) = hAPP(c_Fun_Ocomp(X6,X5,X4,X3,X2),X0),
    inference(equality_resolution,[],[f1426]) ).

fof(f2142,definition,
    sF81 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
    introduced(definition,[new_symbols(definition,[sF81])],[function_definition]) ).

fof(f2143,plain,
    tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF81,
    inference(reorient_equations,[],[f2142]) ).

fof(f2144,definition,
    sF82 = c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),
    introduced(definition,[new_symbols(definition,[sF82])],[function_definition]) ).

fof(f2145,plain,
    c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____) = sF82,
    inference(reorient_equations,[],[f2144]) ).

fof(f2146,definition,
    sF83 = hAPP(v_F,v_P_H____),
    introduced(definition,[new_symbols(definition,[sF83])],[function_definition]) ).

fof(f2147,plain,
    hAPP(v_F,v_P_H____) = sF83,
    inference(reorient_equations,[],[f2146]) ).

fof(f2148,definition,
    sF84 = c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),
    introduced(definition,[new_symbols(definition,[sF84])],[function_definition]) ).

fof(f2149,plain,
    c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____) = sF84,
    inference(reorient_equations,[],[f2148]) ).

fof(f2150,definition,
    sF85 = tc_fun(sF81,tc_HOL_Obool),
    introduced(definition,[new_symbols(definition,[sF85])],[function_definition]) ).

fof(f2151,plain,
    tc_fun(sF81,tc_HOL_Obool) = sF85,
    inference(reorient_equations,[],[f2150]) ).

fof(f2152,definition,
    sF86 = c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
    introduced(definition,[new_symbols(definition,[sF86])],[function_definition]) ).

fof(f2153,plain,
    c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF86,
    inference(reorient_equations,[],[f2152]) ).

fof(f2154,definition,
    sF87 = c_Fun_Ocomp(sF85,sF85,tc_Arrow__Order__Mirabelle_Oindi,sF86,v_P____),
    introduced(definition,[new_symbols(definition,[sF87])],[function_definition]) ).

fof(f2155,plain,
    c_Fun_Ocomp(sF85,sF85,tc_Arrow__Order__Mirabelle_Oindi,sF86,v_P____) = sF87,
    inference(reorient_equations,[],[f2154]) ).

fof(f2156,definition,
    sF88 = hAPP(v_F,sF87),
    introduced(definition,[new_symbols(definition,[sF88])],[function_definition]) ).

fof(f2157,plain,
    hAPP(v_F,sF87) = sF88,
    inference(reorient_equations,[],[f2156]) ).

fof(f2158,plain,
    ( ~ c_member(sF81,sF82,sF83)
    | ~ c_member(sF81,sF84,sF88) ),
    inference(definition_folding,[],[f1950,f2157,f2155,f2153,f2151,f2143,f2151,f2143,f2149,f2143,f2147,f2145,f2143]) ).

fof(f2159,plain,
    ( c_member(sF81,sF82,sF83)
    | c_member(sF81,sF84,sF88) ),
    inference(definition_folding,[],[f1949,f2157,f2155,f2153,f2151,f2143,f2151,f2143,f2149,f2143,f2147,f2145,f2143]) ).

fof(f2168,definition,
    ( spl89_1
  <=> c_member(sF81,sF84,sF88) ),
    introduced(definition,[new_symbols(definition,[spl89_1])],[avatar_definition]) ).

fof(f2169,plain,
    ( ~ c_member(sF81,sF84,sF88)
    | spl89_1 ),
    inference(avatar_component_clause,[],[f2168]) ).

fof(f2170,plain,
    ( c_member(sF81,sF84,sF88)
    | ~ spl89_1 ),
    inference(avatar_component_clause,[],[f2168]) ).

fof(f2172,definition,
    ( spl89_2
  <=> c_member(sF81,sF82,sF83) ),
    introduced(definition,[new_symbols(definition,[spl89_2])],[avatar_definition]) ).

fof(f2173,plain,
    ( ~ c_member(sF81,sF82,sF83)
    | spl89_2 ),
    inference(avatar_component_clause,[],[f2172]) ).

fof(f2174,plain,
    ( c_member(sF81,sF82,sF83)
    | ~ spl89_2 ),
    inference(avatar_component_clause,[],[f2172]) ).

fof(f2175,plain,
    ( spl89_1
    | spl89_2 ),
    inference(avatar_split_clause,[],[f2159,f2172,f2168]) ).

fof(f2176,plain,
    ( ~ spl89_1
    | ~ spl89_2 ),
    inference(avatar_split_clause,[],[f2158,f2172,f2168]) ).

fof(f2182,plain,
    ! [X0] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f1220,f2074]) ).

fof(f2183,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f1221,f2074]) ).

fof(f2186,plain,
    ! [X0] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(sF86,hAPP(v_P____,X0)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2182,f2153]) ).

fof(f2187,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(sF86,hAPP(v_P____,X0)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2183,f2153]) ).

fof(f2188,plain,
    ! [X0] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2186,f2149]) ).

fof(f2189,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2187,f2149]) ).

fof(f2190,plain,
    ! [X0] :
      ( ~ c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2188,f2143]) ).

fof(f2191,plain,
    ! [X0] :
      ( c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_c____),hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2189,f2143]) ).

fof(f2192,plain,
    ! [X0] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_P_H____,X0))
      | ~ c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0))) ),
    inference(forward_demodulation,[],[f2190,f2145]) ).

fof(f2193,plain,
    ! [X0] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_P_H____,X0))
      | c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0))) ),
    inference(forward_demodulation,[],[f2191,f2145]) ).

fof(f2194,plain,
    ! [X0] :
      ( ~ c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | c_member(sF81,sF82,hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2192,f2143]) ).

fof(f2195,plain,
    ! [X0] :
      ( c_member(sF81,sF84,hAPP(sF86,hAPP(v_P____,X0)))
      | ~ c_member(sF81,sF82,hAPP(v_P_H____,X0)) ),
    inference(forward_demodulation,[],[f2193,f2143]) ).

fof(f2245,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | v_a____ = v_b____
      | X2 = X3 ),
    inference(superposition,[],[f1269,f2149]) ).

fof(f2250,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_subsumption_resolution,[],[f2245,f1217]) ).

fof(f2259,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2250,f2143]) ).

fof(f2268,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF84,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2259,f2143]) ).

fof(f2277,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2268,f2143]) ).

fof(f2286,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2277,f2143]) ).

fof(f2295,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2286,f2143]) ).

fof(f2304,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2295,f2151]) ).

fof(f2313,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2304,f2143]) ).

fof(f2322,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,X2,X3)))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = X2
      | v_a____ = X3
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2313,f2151]) ).

fof(f2411,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3
      | v_b____ = v_c____ ),
    inference(superposition,[],[f1265,f2145]) ).

fof(f2412,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3
      | v_b____ = v_c____ ),
    inference(superposition,[],[f1266,f2145]) ).

fof(f2418,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3
      | v_b____ = v_c____ ),
    inference(superposition,[],[f1270,f2145]) ).

fof(f2419,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_subsumption_resolution,[],[f2418,f1218]) ).

fof(f2425,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_subsumption_resolution,[],[f2412,f1218]) ).

fof(f2426,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_subsumption_resolution,[],[f2411,f1218]) ).

fof(f2428,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2419,f2143]) ).

fof(f2434,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2425,f2143]) ).

fof(f2435,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2426,f2143]) ).

fof(f2437,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2428,f2143]) ).

fof(f2443,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2434,f2143]) ).

fof(f2444,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2435,f2143]) ).

fof(f2446,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2437,f2143]) ).

fof(f2452,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2443,f2143]) ).

fof(f2453,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2444,f2143]) ).

fof(f2455,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2446,f2143]) ).

fof(f2461,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2452,f2143]) ).

fof(f2462,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2453,f2143]) ).

fof(f2464,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2455,f2143]) ).

fof(f2470,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2461,f2143]) ).

fof(f2471,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2462,f2143]) ).

fof(f2473,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2464,f2151]) ).

fof(f2479,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2470,f2151]) ).

fof(f2480,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2471,f2151]) ).

fof(f2482,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2473,f2143]) ).

fof(f2488,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2479,f2143]) ).

fof(f2489,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2480,f2143]) ).

fof(f2491,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,X2,X3,v_c____,v_b____)))
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2482,f2151]) ).

fof(f2497,plain,
    ! [X2,X3,X0,X1] :
      ( ~ c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2488,f2151]) ).

fof(f2498,plain,
    ! [X2,X3,X0,X1] :
      ( c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(X1,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(X1,X0,X2,X3,v_c____,v_b____)))
      | c_member(sF81,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X2),hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_c____ = X3
      | v_b____ = X2
      | X2 = X3 ),
    inference(forward_demodulation,[],[f2489,f2151]) ).

fof(f2501,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Fun_Ocomp(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,sF86,v_P____),c_Arrow__Order__Mirabelle_OProf),
    inference(superposition,[],[f1224,f2153]) ).

fof(f2502,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),c_Fun_Ocomp(tc_fun(sF81,tc_HOL_Obool),tc_fun(sF81,tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,sF86,v_P____),c_Arrow__Order__Mirabelle_OProf),
    inference(forward_demodulation,[],[f2501,f2143]) ).

fof(f2504,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),c_Fun_Ocomp(sF85,sF85,tc_Arrow__Order__Mirabelle_Oindi,sF86,v_P____),c_Arrow__Order__Mirabelle_OProf),
    inference(forward_demodulation,[],[f2502,f2151]) ).

fof(f2506,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),sF87,c_Arrow__Order__Mirabelle_OProf),
    inference(forward_demodulation,[],[f2504,f2155]) ).

fof(f2867,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_b____ = v_c____
      | v_a____ = v_b____
      | v_a____ = v_b____ ),
    inference(superposition,[],[f2497,f2149]) ).

fof(f2871,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_b____ = v_c____
      | v_a____ = v_b____ ),
    inference(duplicate_literal_removal,[],[f2867]) ).

fof(f2873,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_a____ = v_b____ ),
    inference(forward_subsumption_resolution,[],[f2871,f1218]) ).

fof(f2874,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____))) ),
    inference(forward_subsumption_resolution,[],[f2873,f1217]) ).

fof(f3015,plain,
    ! [X0] : hAPP(sF86,hAPP(v_P____,X0)) = hAPP(sF87,X0),
    inference(superposition,[],[f2074,f2155]) ).

fof(f3016,plain,
    ! [X0] :
      ( ~ c_member(sF81,sF84,hAPP(sF87,X0))
      | c_member(sF81,sF82,hAPP(v_P_H____,X0)) ),
    inference(superposition,[],[f2194,f3015]) ).

fof(f3017,plain,
    ! [X0] :
      ( ~ c_member(sF81,sF82,hAPP(v_P_H____,X0))
      | c_member(sF81,sF84,hAPP(sF87,X0)) ),
    inference(superposition,[],[f2195,f3015]) ).

fof(f3028,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = v_c____
      | v_a____ = v_b____
      | v_a____ = v_b____ ),
    inference(superposition,[],[f2498,f2149]) ).

fof(f3033,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = v_c____
      | v_a____ = v_b____ ),
    inference(duplicate_literal_removal,[],[f3028]) ).

fof(f3036,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | v_a____ = v_b____ ),
    inference(forward_subsumption_resolution,[],[f3033,f1218]) ).

fof(f3037,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF84,hAPP(X0,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X1,sK4(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_subsumption_resolution,[],[f3036,f1217]) ).

fof(f3062,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF81,tc_HOL_Obool)),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    inference(superposition,[],[f1225,f2143]) ).

fof(f3063,plain,
    c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf),
    inference(forward_demodulation,[],[f3062,f2151]) ).

fof(f3087,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(X1,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = v_c____
      | v_a____ = v_b____
      | v_b____ = v_c____ ),
    inference(superposition,[],[f2322,f2145]) ).

fof(f3090,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(X1,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_b____ = v_c____
      | v_a____ = v_b____ ),
    inference(duplicate_literal_removal,[],[f3087]) ).

fof(f3094,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(X1,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | v_a____ = v_b____ ),
    inference(forward_subsumption_resolution,[],[f3090,f1218]) ).

fof(f3096,plain,
    ! [X0,X1] :
      ( c_member(sF81,sF84,hAPP(X1,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK5(X1,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_subsumption_resolution,[],[f3094,f1217]) ).

fof(f3117,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X1,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_b____ = v_c____
      | v_a____ = v_b____
      | v_a____ = v_b____ ),
    inference(superposition,[],[f2491,f2149]) ).

fof(f3121,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X1,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_b____ = v_c____
      | v_a____ = v_b____ ),
    inference(duplicate_literal_removal,[],[f3117]) ).

fof(f3126,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X1,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | v_a____ = v_b____ ),
    inference(forward_subsumption_resolution,[],[f3121,f1218]) ).

fof(f3127,plain,
    ! [X0,X1] :
      ( ~ c_member(sF81,sF84,hAPP(X0,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf)
      | c_member(sF81,sF82,hAPP(v_F,X1))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X1,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(sF81,sF84,hAPP(v_F,X0))
      | ~ c_member(sF81,sF82,hAPP(X1,sK5(X0,X1,v_a____,v_b____,v_c____,v_b____))) ),
    inference(forward_subsumption_resolution,[],[f3126,f1217]) ).

fof(f3355,plain,
    ! [X0] :
      ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,sF87))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),sF87,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(resolution,[],[f3016,f3037]) ).

fof(f3358,plain,
    ! [X0] :
      ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),sF87,c_Arrow__Order__Mirabelle_OProf)
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(resolution,[],[f3016,f3096]) ).

fof(f3365,plain,
    ! [X0] :
      ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_subsumption_resolution,[],[f3358,f2506]) ).

fof(f3368,plain,
    ! [X0] :
      ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF84,hAPP(v_F,sF87))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_subsumption_resolution,[],[f3355,f2506]) ).

fof(f3373,plain,
    ! [X0] :
      ( ~ c_member(sF81,sF84,sF88)
      | c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_demodulation,[],[f3365,f2157]) ).

fof(f3376,plain,
    ! [X0] :
      ( c_member(sF81,sF84,sF88)
      | c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | c_member(sF81,sF82,hAPP(X0,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
      | ~ c_member(sF81,sF82,hAPP(v_F,X0))
      | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) ),
    inference(forward_demodulation,[],[f3368,f2157]) ).

fof(f3381,plain,
    ( ! [X0] :
        ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
        | c_member(sF81,sF82,hAPP(X0,sK4(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
        | ~ c_member(sF81,sF82,hAPP(v_F,X0))
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) )
    | spl89_1 ),
    inference(forward_subsumption_resolution,[],[f3376,f2169]) ).

fof(f3383,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | spl89_1 ),
    inference(factoring,[],[f3381]) ).

fof(f3385,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | spl89_1 ),
    inference(forward_subsumption_resolution,[],[f3383,f3063]) ).

fof(f3386,plain,
    ( ~ c_member(sF81,sF82,sF83)
    | c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1 ),
    inference(forward_demodulation,[],[f3385,f2147]) ).

fof(f3387,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3386,f2174]) ).

fof(f3388,plain,
    ( c_member(sF81,sF84,hAPP(sF87,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1
    | ~ spl89_2 ),
    inference(resolution,[],[f3387,f3017]) ).

fof(f3389,plain,
    ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),sF87,c_Arrow__Order__Mirabelle_OProf)
    | c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1
    | ~ spl89_2 ),
    inference(resolution,[],[f3388,f2874]) ).

fof(f3391,plain,
    ( c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3389,f2506]) ).

fof(f3392,plain,
    ( c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK4(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3391,f3063]) ).

fof(f3393,plain,
    ( c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3392,f3387]) ).

fof(f3394,plain,
    ( c_member(sF81,sF84,sF88)
    | ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_demodulation,[],[f3393,f2157]) ).

fof(f3395,plain,
    ( ~ c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3394,f2169]) ).

fof(f3396,plain,
    ( ~ c_member(sF81,sF82,sF83)
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_demodulation,[],[f3395,f2147]) ).

fof(f3397,plain,
    ( $false
    | spl89_1
    | ~ spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3396,f2174]) ).

fof(f3398,plain,
    ( spl89_1
    | ~ spl89_2 ),
    inference(avatar_contradiction_clause,[],[f3397]) ).

fof(f3403,plain,
    ( ! [X0] :
        ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
        | c_member(sF81,sF82,hAPP(X0,sK5(sF87,X0,v_a____,v_b____,v_c____,v_b____)))
        | c_member(sF81,sF82,hAPP(v_F,X0))
        | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),X0,c_Arrow__Order__Mirabelle_OProf) )
    | ~ spl89_1 ),
    inference(forward_subsumption_resolution,[],[f3373,f2170]) ).

fof(f3468,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ spl89_1 ),
    inference(factoring,[],[f3403]) ).

fof(f3470,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ spl89_1 ),
    inference(forward_subsumption_resolution,[],[f3468,f3063]) ).

fof(f3471,plain,
    ( c_member(sF81,sF82,sF83)
    | c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1 ),
    inference(forward_demodulation,[],[f3470,f2147]) ).

fof(f3472,plain,
    ( c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3471,f2173]) ).

fof(f3473,plain,
    ( c_member(sF81,sF84,hAPP(sF87,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1
    | spl89_2 ),
    inference(resolution,[],[f3472,f3017]) ).

fof(f3474,plain,
    ( ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),sF87,c_Arrow__Order__Mirabelle_OProf)
    | c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1
    | spl89_2 ),
    inference(resolution,[],[f3473,f3127]) ).

fof(f3478,plain,
    ( c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF85),v_P_H____,c_Arrow__Order__Mirabelle_OProf)
    | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3474,f2506]) ).

fof(f3480,plain,
    ( c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ c_member(sF81,sF82,hAPP(v_P_H____,sK5(sF87,v_P_H____,v_a____,v_b____,v_c____,v_b____)))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3478,f3063]) ).

fof(f3482,plain,
    ( c_member(sF81,sF82,hAPP(v_F,v_P_H____))
    | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3480,f3472]) ).

fof(f3484,plain,
    ( c_member(sF81,sF82,sF83)
    | ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_demodulation,[],[f3482,f2147]) ).

fof(f3485,plain,
    ( ~ c_member(sF81,sF84,hAPP(v_F,sF87))
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3484,f2173]) ).

fof(f3486,plain,
    ( ~ c_member(sF81,sF84,sF88)
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_demodulation,[],[f3485,f2157]) ).

fof(f3487,plain,
    ( $false
    | ~ spl89_1
    | spl89_2 ),
    inference(forward_subsumption_resolution,[],[f3486,f2170]) ).

fof(f3488,plain,
    ( ~ spl89_1
    | spl89_2 ),
    inference(avatar_contradiction_clause,[],[f3487]) ).

cnf(s1,plain,
    ( spl89_1
    | spl89_2 ),
    inference(sat_conversion,[],[f2175]) ).

cnf(s2,plain,
    ( ~ spl89_1
    | ~ spl89_2 ),
    inference(sat_conversion,[],[f2176]) ).

cnf(s13,plain,
    ( spl89_1
    | ~ spl89_2 ),
    inference(sat_conversion,[],[f3398]) ).

cnf(s14,plain,
    ( ~ spl89_1
    | spl89_2 ),
    inference(sat_conversion,[],[f3488]) ).

cnf(s15,plain,
    spl89_1,
    inference(rat,[],[s1,s13]) ).

cnf(s16,plain,
    spl89_2,
    inference(rat,[],[s14,s15]) ).

cnf(s17,plain,
    $false,
    inference(rat,[],[s2,s16,s15]) ).

fof(f3489,plain,
    $false,
    inference(avatar_sat_refutation,[],[s17]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SCT151+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39  % Computer : n026.cluster.edu
% 0.11/0.39  % Model    : x86_64 x86_64
% 0.11/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39  % Memory   : 8046.5625MB
% 0.11/0.39  % OS       : Linux 6.8.0-71-generic
% 0.11/0.39  % CPULimit : 300
% 0.11/0.39  % WCLimit  : 300
% 0.11/0.39  % DateTime : Sun Sep 27 23:53:26 UTC 2026
% 0.11/0.39  % CPUTime  : 
% 0.11/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43  Running first-order theorem proving
% 0.11/0.43  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.47/2.07  % (3337339)Detected formulas, will run a generic FOF schedule.
% 8.47/2.07  % (3337344)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=394096307:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.47/2.07  % (3337349)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=496738420:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.47/2.07  % (3337347)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2847842266:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.47/2.07  % (3337348)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1201310523:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.47/2.07  % (3337345)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=918126313:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.47/2.07  % (3337346)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2053841021:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.47/2.07  % (3337347)Refutation not found, incomplete strategy
% 8.47/2.07  % (3337347)------------------------------
% 8.47/2.07  % (3337347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337347)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337347)Termination reason: Refutation not found, incomplete strategy
% 8.47/2.07  % (3337347)Time elapsed: 0.008 s
% 8.47/2.07  % (3337347)Peak memory usage: 89 MB
% 8.47/2.07  % (3337347)Instructions burned: 12 (million)
% 8.47/2.07  % (3337350)dis-21_1_sil=8000:lcm=predicate:random_seed=1131463369:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.47/2.07  % (3337348)Instruction limit reached! 
% 8.47/2.07  % (3337348)------------------------------
% 8.47/2.07  % (3337348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337348)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337348)Termination reason: Instruction limit
% 8.47/2.07  % (3337348)Termination phase: Saturation
% 8.47/2.07  % (3337348)Time elapsed: 0.076 s
% 8.47/2.07  % (3337348)Peak memory usage: 89 MB
% 8.47/2.07  % (3337348)Instructions burned: 120 (million)
% 8.47/2.07  % (3337349)Instruction limit reached! 
% 8.47/2.07  % (3337349)------------------------------
% 8.47/2.07  % (3337349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337349)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337349)Termination reason: Instruction limit
% 8.47/2.07  % (3337349)Termination phase: Saturation
% 8.47/2.07  % (3337349)Time elapsed: 0.083 s
% 8.47/2.07  % (3337349)Peak memory usage: 90 MB
% 8.47/2.07  % (3337349)Instructions burned: 139 (million)
% 8.47/2.07  % (3337350)Instruction limit reached! 
% 8.47/2.07  % (3337350)------------------------------
% 8.47/2.07  % (3337350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337350)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337350)Termination reason: Instruction limit
% 8.47/2.07  % (3337350)Termination phase: Saturation
% 8.47/2.07  % (3337350)Time elapsed: 0.068 s
% 8.47/2.07  % (3337350)Peak memory usage: 89 MB
% 8.47/2.07  % (3337350)Instructions burned: 130 (million)
% 8.47/2.07  % (3337359)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3949404189:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.47/2.07  % (3337358)lrs+10_1_sil=8000:sp=occurrence:random_seed=3027732340:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.47/2.07  % (3337360)lrs+1011_1_sil=32000:sp=occurrence:random_seed=130845329:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.47/2.07  % (3337347)------------------------------
% 8.47/2.07  % (3337347)------------------------------
% 8.47/2.07  % (3337359)Instruction limit reached! 
% 8.47/2.07  % (3337359)------------------------------
% 8.47/2.07  % (3337359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337359)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337359)Termination reason: Instruction limit
% 8.47/2.07  % (3337359)Termination phase: Saturation
% 8.47/2.07  % (3337359)Time elapsed: 0.087 s
% 8.47/2.07  % (3337359)Peak memory usage: 90 MB
% 8.47/2.07  % (3337359)Instructions burned: 158 (million)
% 8.47/2.07  % (3337364)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1364160538:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.47/2.07  % (3337358)Instruction limit reached! 
% 8.47/2.07  % (3337358)------------------------------
% 8.47/2.07  % (3337358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337358)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337358)Termination reason: Instruction limit
% 8.47/2.07  % (3337358)Termination phase: Saturation
% 8.47/2.07  % (3337358)Time elapsed: 0.184 s
% 8.47/2.07  % (3337358)Peak memory usage: 91 MB
% 8.47/2.07  % (3337358)Instructions burned: 286 (million)
% 8.47/2.07  % (3337360)Instruction limit reached! 
% 8.47/2.07  % (3337360)------------------------------
% 8.47/2.07  % (3337360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337360)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337360)Termination reason: Instruction limit
% 8.47/2.07  % (3337360)Termination phase: Saturation
% 8.47/2.07  % (3337360)Time elapsed: 0.201 s
% 8.47/2.07  % (3337360)Peak memory usage: 92 MB
% 8.47/2.07  % (3337360)Instructions burned: 326 (million)
% 8.47/2.07  % (3337365)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=74542065:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.47/2.07  % (3337364)Instruction limit reached! 
% 8.47/2.07  % (3337364)------------------------------
% 8.47/2.07  % (3337364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337364)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337364)Termination reason: Instruction limit
% 8.47/2.07  % (3337364)Termination phase: Saturation
% 8.47/2.07  % (3337364)Time elapsed: 0.074 s
% 8.47/2.07  % (3337364)Peak memory usage: 91 MB
% 8.47/2.07  % (3337364)Instructions burned: 251 (million)
% 8.47/2.07  % (3337365)Refutation not found, incomplete strategy
% 8.47/2.07  % (3337365)------------------------------
% 8.47/2.07  % (3337365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337365)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337365)Termination reason: Refutation not found, incomplete strategy
% 8.47/2.07  % (3337365)Time elapsed: 0.034 s
% 8.47/2.07  % (3337365)Peak memory usage: 90 MB
% 8.47/2.07  % (3337365)Instructions burned: 44 (million)
% 8.47/2.07  % (3337370)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2331654609:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 8.47/2.07  % (3337367)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2053848194:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.47/2.07  % (3337370)Instruction limit reached! 
% 8.47/2.07  % (3337370)------------------------------
% 8.47/2.07  % (3337370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337370)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337370)Termination reason: Instruction limit
% 8.47/2.07  % (3337370)Termination phase: Saturation
% 8.47/2.07  % (3337370)Time elapsed: 0.031 s
% 8.47/2.07  % (3337370)Peak memory usage: 89 MB
% 8.47/2.07  % (3337370)Instructions burned: 128 (million)
% 8.47/2.07  % (3337368)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3996766883:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 8.47/2.07  % (3337368)Instruction limit reached! 
% 8.47/2.07  % (3337368)------------------------------
% 8.47/2.07  % (3337368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337368)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337368)Termination reason: Instruction limit
% 8.47/2.07  % (3337368)Termination phase: Saturation
% 8.47/2.07  % (3337368)Time elapsed: 0.062 s
% 8.47/2.07  % (3337368)Peak memory usage: 90 MB
% 8.47/2.07  % (3337368)Instructions burned: 115 (million)
% 8.47/2.07  % (3337374)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1806538070:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 8.47/2.07  % (3337365)------------------------------
% 8.47/2.07  % (3337365)------------------------------
% 8.47/2.07  % (3337375)lrs+10_1_sil=8000:sp=occurrence:random_seed=787217658:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 8.47/2.07  % (3337374)Instruction limit reached! 
% 8.47/2.07  % (3337374)------------------------------
% 8.47/2.07  % (3337374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.47/2.07  % (3337374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.47/2.07  % (3337374)CaDiCaL version: 2.1.3
% 8.47/2.07  % (3337374)Termination reason: Instruction limit
% 8.47/2.07  % (3337374)Termination phase: Saturation
% 8.47/2.07  % (3337374)Time elapsed: 0.058 s
% 8.47/2.07  % (3337374)Peak memory usage: 89 MB
% 8.47/2.07  % (3337374)Instructions burned: 115 (million)
% 8.47/2.07  % (3337344)First to succeed.
% 8.47/2.07  % (3337344)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3337339"
% 8.47/2.07  % (3337377)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4072785884:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 8.47/2.07  % (3337379)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=127526173:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 8.47/2.07  % (3337344)Refutation found. Thanks to Tanya!
% 8.47/2.07  % SZS status Theorem for theBenchmark
% 8.47/2.07  % SZS output start Proof for theBenchmark
% See solution above
% 8.92/2.26  % (3337344)------------------------------
% 8.92/2.26  % (3337344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.26  % (3337344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.26  % (3337344)CaDiCaL version: 2.1.3
% 8.92/2.26  % (3337344)Termination reason: Refutation
% 8.92/2.26  % (3337344)Time elapsed: 0.807 s
% 8.92/2.26  % (3337344)Peak memory usage: 141 MB
% 8.92/2.26  % (3337344)Instructions burned: 1624 (million)
% 8.92/2.26  % (3337344)------------------------------
% 8.92/2.26  % (3337344)------------------------------
% 8.92/2.26  % (3337339)Success in time 1.199 s
% 8.92/2.26  % Vampire exiting
%------------------------------------------------------------------------------