Vampire---5.0.1.THM-Ref.s

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

% Computer : n012.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 01:38:01 PM UTC 2026

% Result   : Theorem 29.20s 4.56s
% Output   : Refutation 30.01s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   25
%            Number of leaves      :   20
% Syntax   : Number of formulae    :  142 (  33 unt;   6 def)
%            Number of atoms       :  441 ( 223 equ)
%            Maximal formula atoms :   24 (   3 avg)
%            Number of connectives :  475 ( 176   ~; 181   |;  87   &)
%                                         (  24 <=>;   7  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   15 (   5 avg)
%            Maximal term depth    :   12 (   2 avg)
%            Number of predicates  :    9 (   7 usr;   7 prp; 0-2 aty)
%            Number of functors    :   34 (  34 usr;  11 con; 0-3 aty)
%            Number of variables   :  315 (   0 sgn 302   !;  13   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f2,axiom,
    ~ p__01(s__02(cbool__00,cF__00)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','HL_FALSITY') ).

fof(f8,axiom,
    ! [X0,X1] :
      ( s__02(X0,X1) = s__02(X0,X1)
    <=> p__01(s__02(cbool__00,cT__00)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.bool.REFL_CLAUSE') ).

fof(f10,axiom,
    ! [X0] :
      ( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
      <=> p__01(s__02(cbool__00,X0)) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
      <=> p__01(s__02(cbool__00,X0)) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
      <=> ~ p__01(s__02(cbool__00,X0)) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
      <=> ~ p__01(s__02(cbool__00,X0)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.bool.EQ_CLAUSES') ).

fof(f20,axiom,
    ! [X0] :
      ( ! [X1,X2] : s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(X0,X1),s__02(X0,X2))) = s__02(X0,X1)
      & ! [X1,X2] : s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(X0,X1),s__02(X0,X2))) = s__02(X0,X2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.bool.bool_case_thm') ).

fof(f23,axiom,
    ! [X0,X1] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X0))),s__02(c_27type_2enum_2enum_27__00,X1))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.arithmetic.LESS_EQ') ).

fof(f27,axiom,
    ! [X0,X1,X2] :
      ( ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))))
        & p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2)))) )
     => p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X2)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.arithmetic.LESS_EQ_TRANS') ).

fof(f32,axiom,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> ~ p__01(s__02(cbool__00,X3)) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> p__01(s__02(cbool__00,X3)) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( ~ p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.option.IF_EQUALS_OPTION') ).

fof(f33,axiom,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> ( p__01(s__02(cbool__00,X3))
         => p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> ( p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
         => p__01(s__02(cbool__00,X3)) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( ~ p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.option.IF_NONE_EQUALS_OPTION') ).

fof(f34,axiom,
    ! [X0,X1,X2] :
      ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1))))
    <=> ? [X3] : s__02(c_27type_2elist_2elist_27__01(X0),X1) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.rich_list.IS_PREFIX_APPEND') ).

fof(f35,axiom,
    ! [X0,X1,X2,X3] :
      ( p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))))
     => s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.rich_list.EL_APPEND1') ).

fof(f36,axiom,
    ! [X0,X1,X2] :
      ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))))
     => p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2)))))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.rich_list.IS_PREFIX_LENGTH') ).

fof(f37,axiom,
    ! [X0,X1,X2] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.sptree.lookup_fromList') ).

fof(f38,axiom,
    ! [X0,X1,X2] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm.misc.lookup_fromList2') ).

fof(f39,conjecture,
    ! [X0,X1,X2,X3,X4] :
      ( ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))
        & s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) )
     => s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).

fof(f40,negated_conjecture,
    ~ ! [X0,X1,X2,X3,X4] :
        ( ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) )
       => s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) ),
    inference(negated_conjecture,[status(cth)],[f39]) ).

fof(f42,plain,
    ! [X0] :
      ( ! [X1,X2] : s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(X0,X1),s__02(X0,X2))) = s__02(X0,X1)
      & ! [X3,X4] : s__02(X0,X4) = s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(X0,X3),s__02(X0,X4))) ),
    inference(rectify,[],[f20]) ).

fof(f55,plain,
    ! [X0,X1,X2] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X2))))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2)))) ),
    inference(ennf_transformation,[],[f27]) ).

fof(f56,plain,
    ! [X0,X1,X2] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X2))))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2)))) ),
    inference(flattening,[],[f55]) ).

fof(f57,plain,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> ( p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
          | ~ p__01(s__02(cbool__00,X3)) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
      <=> ( p__01(s__02(cbool__00,X3))
          | ~ p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      <=> ( ~ p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) ) ),
    inference(ennf_transformation,[],[f33]) ).

fof(f58,plain,
    ! [X0,X1,X2,X3] :
      ( s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2)))
      | ~ p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2)))))) ),
    inference(ennf_transformation,[],[f35]) ).

fof(f59,plain,
    ! [X0,X1,X2] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))))
      | ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),X2)))) ),
    inference(ennf_transformation,[],[f36]) ).

fof(f60,plain,
    ? [X0,X1,X2,X3,X4] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X3)))))
      & p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))
      & s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) ),
    inference(ennf_transformation,[],[f40]) ).

fof(f61,plain,
    ? [X0,X1,X2,X3,X4] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X3)))))
      & p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))
      & s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X4))) ),
    inference(flattening,[],[f60]) ).

fof(f67,plain,
    ! [X0,X1] :
      ( ( s__02(X0,X1) = s__02(X0,X1)
        | ~ p__01(s__02(cbool__00,cT__00)) )
      & ( p__01(s__02(cbool__00,cT__00))
        | s__02(X0,X1) != s__02(X0,X1) ) ),
    inference(nnf_transformation,[],[f8]) ).

fof(f69,plain,
    ! [X0] :
      ( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
        | ~ p__01(s__02(cbool__00,X0)) )
      & ( p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
        | ~ p__01(s__02(cbool__00,X0)) )
      & ( p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
        | p__01(s__02(cbool__00,X0)) )
      & ( ~ p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cF__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
        | p__01(s__02(cbool__00,X0)) )
      & ( ~ p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cF__00) != s__02(cbool__00,X0) ) ),
    inference(nnf_transformation,[],[f10]) ).

fof(f70,plain,
    ! [X0] :
      ( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
        | ~ p__01(s__02(cbool__00,X0)) )
      & ( p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
        | ~ p__01(s__02(cbool__00,X0)) )
      & ( p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
        | p__01(s__02(cbool__00,X0)) )
      & ( ~ p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cF__00) != s__02(cbool__00,X0) )
      & ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
        | p__01(s__02(cbool__00,X0)) )
      & ( ~ p__01(s__02(cbool__00,X0))
        | s__02(cbool__00,cF__00) != s__02(cbool__00,X0) ) ),
    inference(flattening,[],[f69]) ).

fof(f92,plain,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | p__01(s__02(cbool__00,X3)) )
      & ( ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ~ p__01(s__02(cbool__00,X3)) )
      & ( p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(X0,X1) != s__02(X0,X2) )
      & ( ( p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | p__01(s__02(cbool__00,X3))
        | s__02(X0,X1) != s__02(X0,X2) )
      & ( ( ~ p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) ),
    inference(nnf_transformation,[],[f32]) ).

fof(f93,plain,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | p__01(s__02(cbool__00,X3)) )
      & ( ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ~ p__01(s__02(cbool__00,X3)) )
      & ( p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(X0,X1) != s__02(X0,X2) )
      & ( ( p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | p__01(s__02(cbool__00,X3))
        | s__02(X0,X1) != s__02(X0,X2) )
      & ( ( ~ p__01(s__02(cbool__00,X3))
          & s__02(X0,X2) = s__02(X0,X1) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ) ),
    inference(flattening,[],[f92]) ).

fof(f94,plain,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ( ~ p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
          & p__01(s__02(cbool__00,X3)) ) )
      & ( p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ( ~ p__01(s__02(cbool__00,X3))
          & p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))) ) )
      & ( p__01(s__02(cbool__00,X3))
        | ~ p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) )
      & ( ( p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) )
      & ( ( ~ p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) ) ),
    inference(nnf_transformation,[],[f57]) ).

fof(f95,plain,
    ! [X0,X1,X2,X3] :
      ( ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ( ~ p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
          & p__01(s__02(cbool__00,X3)) ) )
      & ( p__01(s__02(cbool__00,c_27const_2eoption_2eIS__NONE_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)
        | ( ~ p__01(s__02(cbool__00,X3))
          & p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))) ) )
      & ( p__01(s__02(cbool__00,X3))
        | ~ p__01(s__02(cbool__00,c_27const_2eoption_2eIS__SOME_27__01(s__02(c_27type_2eoption_2eoption_27__01(X0),X2))))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | ~ p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) )
      & ( ( p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) )
      & ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | p__01(s__02(cbool__00,X3))
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) )
      & ( ( ~ p__01(s__02(cbool__00,X3))
          & s__02(c_27type_2eoption_2eoption_27__01(X0),X2) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) )
        | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) ) ),
    inference(flattening,[],[f94]) ).

fof(f96,plain,
    ! [X0,X1,X2] :
      ( ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1))))
        | ! [X3] : s__02(c_27type_2elist_2elist_27__01(X0),X1) != s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))) )
      & ( ? [X3] : s__02(c_27type_2elist_2elist_27__01(X0),X1) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3)))
        | ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1)))) ) ),
    inference(nnf_transformation,[],[f34]) ).

fof(f97,plain,
    ! [X0,X1,X2] :
      ( ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1))))
        | ! [X3] : s__02(c_27type_2elist_2elist_27__01(X0),X1) != s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))) )
      & ( ? [X4] : s__02(c_27type_2elist_2elist_27__01(X0),X1) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X4)))
        | ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1)))) ) ),
    inference(rectify,[],[f96]) ).

fof(f98,plain,
    ! [X0,X1,X2] :
      ( ( p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1))))
        | ! [X3] : s__02(c_27type_2elist_2elist_27__01(X0),X1) != s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))) )
      & ( s__02(c_27type_2elist_2elist_27__01(X0),X1) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),sK2(X0,X1,X2))))
        | ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1)))) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X4,sK2(X0,X1,X2))],[f97]) ).

fof(f99,plain,
    ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))
    & p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))
    & s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7)],[f61]) ).

fof(f101,plain,
    ~ p__01(s__02(cbool__00,cF__00)),
    inference(cnf_transformation,[],[f2]) ).

fof(f113,plain,
    ! [X0,X1] :
      ( p__01(s__02(cbool__00,cT__00))
      | s__02(X0,X1) != s__02(X0,X1) ),
    inference(cnf_transformation,[],[f67]) ).

fof(f122,plain,
    ! [X0] :
      ( ~ p__01(s__02(cbool__00,X0))
      | s__02(cbool__00,cT__00) = s__02(cbool__00,X0) ),
    inference(cnf_transformation,[],[f70]) ).

fof(f171,plain,
    ! [X3,X0,X4] : s__02(X0,X4) = s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(X0,X3),s__02(X0,X4))),
    inference(cnf_transformation,[],[f42]) ).

fof(f172,plain,
    ! [X2,X0,X1] : s__02(X0,X1) = s__02(X0,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(X0,X1),s__02(X0,X2))),
    inference(cnf_transformation,[],[f42]) ).

fof(f178,plain,
    ! [X0,X1] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X0))),s__02(c_27type_2enum_2enum_27__00,X1))),
    inference(cnf_transformation,[],[f23]) ).

fof(f188,plain,
    ! [X2,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2))))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X1))))
      | p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,X2)))) ),
    inference(cnf_transformation,[],[f56]) ).

fof(f242,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
      | s__02(X0,X1) = s__02(X0,X2) ),
    inference(cnf_transformation,[],[f93]) ).

fof(f249,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),X2) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f251,plain,
    ! [X2,X3,X0,X1] :
      ( p__01(s__02(cbool__00,X3))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f252,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),X2) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f253,plain,
    ! [X2,X3,X0,X1] :
      ( p__01(s__02(cbool__00,X3))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f254,plain,
    ! [X2,X3,X0,X1] :
      ( ~ p__01(s__02(cbool__00,X3))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f257,plain,
    ! [X2,X3,X0] :
      ( ~ p__01(s__02(cbool__00,X3))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2))) ),
    inference(cnf_transformation,[],[f95]) ).

fof(f261,plain,
    ! [X2,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1))))
      | s__02(c_27type_2elist_2elist_27__01(X0),X1) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),sK2(X0,X1,X2)))) ),
    inference(cnf_transformation,[],[f98]) ).

fof(f263,plain,
    ! [X2,X3,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))))
      | s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))) ),
    inference(cnf_transformation,[],[f58]) ).

fof(f264,plain,
    ! [X2,X0,X1] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))))
      | ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),X2)))) ),
    inference(cnf_transformation,[],[f59]) ).

fof(f265,plain,
    ! [X2,X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))),
    inference(cnf_transformation,[],[f37]) ).

fof(f266,plain,
    ! [X2,X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X2))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))),
    inference(cnf_transformation,[],[f38]) ).

fof(f267,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),
    inference(cnf_transformation,[],[f99]) ).

fof(f268,plain,
    p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))),
    inference(cnf_transformation,[],[f99]) ).

fof(f269,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),
    inference(cnf_transformation,[],[f99]) ).

fof(f271,plain,
    p__01(s__02(cbool__00,cT__00)),
    inference(trivial_inequality_removal,[],[f113]) ).

fof(f300,definition,
    ( spl8_6
  <=> p__01(s__02(cbool__00,cF__00)) ),
    introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).

fof(f301,plain,
    ( ~ p__01(s__02(cbool__00,cF__00))
    | spl8_6 ),
    inference(avatar_component_clause,[],[f300]) ).

fof(f314,plain,
    ~ spl8_6,
    inference(avatar_split_clause,[],[f101,f300]) ).

fof(f357,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X3)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X3))) ),
    inference(superposition,[],[f252,f265]) ).

fof(f372,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X3)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X3))) ),
    inference(superposition,[],[f252,f266]) ).

fof(f1009,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X0),X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X4),X5))) ),
    inference(resolution,[],[f253,f257]) ).

fof(f1010,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) != s__02(c_27type_2eoption_2eoption_27__01(X4),X6)
      | s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) = s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X4),X6),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X0),X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) ),
    inference(resolution,[],[f253,f254]) ).

fof(f1044,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eSOME_27__01(s__02(X3,X4))) != s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X3),X5),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) ),
    inference(equality_resolution,[],[f1010]) ).

fof(f1077,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X3)))
      | s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) = s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X1))),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00))) ),
    inference(superposition,[],[f1044,f266]) ).

fof(f1265,plain,
    ( ! [X2,X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)))
    | spl8_6 ),
    inference(resolution,[],[f301,f253]) ).

fof(f1268,plain,
    ( ! [X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
    | spl8_6 ),
    inference(forward_demodulation,[],[f1265,f171]) ).

fof(f1327,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) != s__02(c_27type_2eoption_2eoption_27__01(X4),X6)
      | s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) = s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X4),X6)))
      | s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X3))))) = s__02(X0,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))) ),
    inference(resolution,[],[f263,f251]) ).

fof(f1998,plain,
    ! [X2,X3,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),X3))))
      | s__02(c_27type_2elist_2elist_27__01(X0),X3) = s__02(c_27type_2elist_2elist_27__01(X0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),sK2(X0,X3,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(c_27type_2elist_2elist_27__01(X0),X2),s__02(c_27type_2elist_2elist_27__01(X0),X1)))))) ),
    inference(superposition,[],[f261,f171]) ).

fof(f3414,plain,
    ! [X2,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0)))
      | s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00))) ),
    inference(superposition,[],[f1077,f267]) ).

fof(f3448,definition,
    ( spl8_21
  <=> ! [X2,X1] : s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00))) ),
    introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition]) ).

fof(f3449,plain,
    ( ! [X2,X1] : s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00)))
    | ~ spl8_21 ),
    inference(avatar_component_clause,[],[f3448]) ).

fof(f3451,definition,
    ( spl8_22
  <=> ! [X0] : s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0))) ),
    introduced(definition,[new_symbols(definition,[spl8_22])],[avatar_definition]) ).

fof(f3452,plain,
    ( ! [X0] : s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0)))
    | ~ spl8_22 ),
    inference(avatar_component_clause,[],[f3451]) ).

fof(f3453,plain,
    ( spl8_21
    | spl8_22 ),
    inference(avatar_split_clause,[],[f3414,f3451,f3448]) ).

fof(f3630,plain,
    ! [X0] : s__02(c_27type_2elist_2elist_27__01(sK3),sK6) = s__02(c_27type_2elist_2elist_27__01(sK3),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),sK2(sK3,sK6,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(c_27type_2elist_2elist_27__01(sK3),X0),s__02(c_27type_2elist_2elist_27__01(sK3),sK5)))))),
    inference(resolution,[],[f1998,f268]) ).

fof(f3943,plain,
    ! [X0] :
      ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0)))
      | s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))) ),
    inference(superposition,[],[f372,f267]) ).

fof(f3982,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),
    inference(equality_resolution,[],[f3943]) ).

fof(f3984,plain,
    ! [X0] :
      ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0)))
      | s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))) ),
    inference(superposition,[],[f357,f3982]) ).

fof(f4063,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),
    inference(equality_resolution,[],[f3984]) ).

fof(f4065,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eNONE_27__00))),
    inference(superposition,[],[f265,f4063]) ).

fof(f4177,plain,
    s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eNONE_27__00))),
    inference(forward_demodulation,[],[f4065,f3982]) ).

fof(f4267,plain,
    ( $false
    | ~ spl8_22 ),
    inference(unit_resulting_resolution,[],[f249,f171,f3452]) ).

fof(f4280,plain,
    ~ spl8_22,
    inference(avatar_contradiction_clause,[],[f4267]) ).

fof(f4296,plain,
    ! [X2,X3,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) != s__02(c_27type_2eoption_2eoption_27__01(X1),X3)
      | s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X0),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X1),X3)))
      | s__02(cbool__00,cT__00) = s__02(cbool__00,X0) ),
    inference(resolution,[],[f122,f251]) ).

fof(f4298,plain,
    ! [X2,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eisPREFIX_27__02(s__02(c_27type_2elist_2elist_27__01(X0),X1),s__02(c_27type_2elist_2elist_27__01(X0),X2))))
      | s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X2))))) ),
    inference(resolution,[],[f122,f264]) ).

fof(f4380,plain,
    s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),
    inference(resolution,[],[f4298,f268]) ).

fof(f5336,definition,
    ( spl8_25
  <=> ! [X2,X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) ),
    introduced(definition,[new_symbols(definition,[spl8_25])],[avatar_definition]) ).

fof(f5337,plain,
    ( ! [X2,X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
    | ~ spl8_25 ),
    inference(avatar_component_clause,[],[f5336]) ).

fof(f5650,plain,
    ( ! [X2,X3,X0,X1,X4] :
        ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X2))) != s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X3),X4))) )
    | ~ spl8_21 ),
    inference(superposition,[],[f1009,f3449]) ).

fof(f5663,plain,
    ! [X2,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X0)))
      | s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X1),X2))) ),
    inference(superposition,[],[f1009,f4177]) ).

fof(f5667,definition,
    ( spl8_28
  <=> ! [X2,X1] : s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X1),X2))) ),
    introduced(definition,[new_symbols(definition,[spl8_28])],[avatar_definition]) ).

fof(f5668,plain,
    ( ! [X2,X1] : s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X1),X2)))
    | ~ spl8_28 ),
    inference(avatar_component_clause,[],[f5667]) ).

fof(f5669,plain,
    ( spl8_28
    | spl8_22 ),
    inference(avatar_split_clause,[],[f5663,f3451,f5667]) ).

fof(f5672,definition,
    ( spl8_29
  <=> ! [X4,X3] : s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X3),X4))) ),
    introduced(definition,[new_symbols(definition,[spl8_29])],[avatar_definition]) ).

fof(f5673,plain,
    ( ! [X3,X4] : s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X3),X4)))
    | ~ spl8_29 ),
    inference(avatar_component_clause,[],[f5672]) ).

fof(f5674,plain,
    ( spl8_29
    | spl8_25
    | ~ spl8_21 ),
    inference(avatar_split_clause,[],[f5650,f3448,f5336,f5672]) ).

fof(f5683,plain,
    ( $false
    | ~ spl8_25 ),
    inference(unit_resulting_resolution,[],[f3984,f4063,f5337]) ).

fof(f5792,plain,
    ~ spl8_25,
    inference(avatar_contradiction_clause,[],[f5683]) ).

fof(f9914,plain,
    ! [X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X0),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,X1))),s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eNONE_27__00)))
      | s__02(sK3,X1) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))) ),
    inference(superposition,[],[f242,f4063]) ).

fof(f16476,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X3),X4))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))))
      | s__02(X3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2elist_2elist_27__01(X3),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X3),X4),s__02(c_27type_2elist_2elist_27__01(X3),X5))))) = s__02(X3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2elist_2elist_27__01(X3),X4))) ),
    inference(equality_resolution,[],[f1327]) ).

fof(f18974,plain,
    ! [X2,X0,X1] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))))
      | s__02(cbool__00,cT__00) = s__02(cbool__00,X2) ),
    inference(equality_resolution,[],[f4296]) ).

fof(f22899,plain,
    ( ! [X0,X1] :
        ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4))) )
    | ~ spl8_29 ),
    inference(superposition,[],[f18974,f5673]) ).

fof(f23120,plain,
    ( s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,sK4)))
    | spl8_6
    | ~ spl8_29 ),
    inference(forward_subsumption_resolution,[],[f22899,f1268]) ).

fof(f24443,plain,
    ! [X0] :
      ( ~ p__01(s__02(cbool__00,cT__00))
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))))
      | p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))) ),
    inference(superposition,[],[f188,f4380]) ).

fof(f24446,plain,
    ! [X0] :
      ( ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))))
      | p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))) ),
    inference(forward_subsumption_resolution,[],[f24443,f271]) ).

fof(f24518,plain,
    ! [X0] :
      ( ~ p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))))
      | p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X0))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))) ),
    inference(superposition,[],[f24446,f178]) ).

fof(f24523,plain,
    ! [X0] :
      ( p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))))
      | ~ p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5)))))) ),
    inference(forward_demodulation,[],[f24518,f178]) ).

fof(f24557,plain,
    ! [X2,X3,X0,X1] :
      ( ~ p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))))
      | s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) = s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X0),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X1),X3),s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eNONE_27__00)))
      | s__02(c_27type_2eoption_2eoption_27__01(X1),c_27const_2eoption_2eSOME_27__01(s__02(X1,X2))) != s__02(c_27type_2eoption_2eoption_27__01(X1),X3) ),
    inference(resolution,[],[f24523,f254]) ).

fof(f24580,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) != s__02(c_27type_2eoption_2eoption_27__01(X4),X6)
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X3)
      | s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eSOME_27__01(s__02(X4,X5))) = s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X4),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X4),X6)))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X0),X3),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) ),
    inference(resolution,[],[f24557,f251]) ).

fof(f24772,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) != s__02(c_27type_2eoption_2eoption_27__01(X0),X2)
      | s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eSOME_27__01(s__02(X3,X4))) = s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eSOME_27__01(s__02(X3,X4)))))
      | s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X0),X2),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00))) ),
    inference(equality_resolution,[],[f24580]) ).

fof(f24939,plain,
    ! [X2,X3,X0,X1,X4] :
      ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK5))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))))
      | s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eSOME_27__01(s__02(X3,X4))) = s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eSOME_27__01(s__02(X3,X4))),s__02(c_27type_2eoption_2eoption_27__01(X3),c_27const_2eoption_2eNONE_27__00))) ),
    inference(equality_resolution,[],[f24772]) ).

fof(f39276,plain,
    ( ! [X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))),s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00)))
    | spl8_6
    | ~ spl8_29 ),
    inference(superposition,[],[f266,f23120]) ).

fof(f39450,plain,
    ( ! [X0,X1] : s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1))))) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(X0),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(X0),X1)))))
    | spl8_6
    | ~ spl8_29 ),
    inference(forward_demodulation,[],[f39276,f172]) ).

fof(f51591,plain,
    ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) != s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7)))
    | s__02(sK3,sK7) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))) ),
    inference(superposition,[],[f9914,f4177]) ).

fof(f51624,plain,
    s__02(sK3,sK7) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))),
    inference(trivial_inequality_removal,[],[f51591]) ).

fof(f88074,plain,
    ( ! [X2,X3,X0,X1] :
        ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eSOME_27__01(s__02(X2,X3))) = s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eSOME_27__01(s__02(X2,X3))),s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eNONE_27__00))) )
    | ~ spl8_28 ),
    inference(superposition,[],[f24939,f5668]) ).

fof(f88075,plain,
    ( ! [X2,X0,X1] :
        ( s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eNONE_27__00) = s__02(c_27type_2eoption_2eoption_27__01(X0),c_27const_2eoption_2eSOME_27__01(s__02(X0,X1)))
        | s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),X2))))) )
    | ~ spl8_28 ),
    inference(superposition,[],[f16476,f5668]) ).

fof(f88568,plain,
    ( ! [X2] : s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK5))) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),X2)))))
    | spl8_6
    | ~ spl8_28 ),
    inference(forward_subsumption_resolution,[],[f88075,f1268]) ).

fof(f88569,plain,
    ( ! [X2,X3] : s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eSOME_27__01(s__02(X2,X3))) = s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))),s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eSOME_27__01(s__02(X2,X3))),s__02(c_27type_2eoption_2eoption_27__01(X2),c_27const_2eoption_2eNONE_27__00)))
    | spl8_6
    | ~ spl8_28 ),
    inference(forward_subsumption_resolution,[],[f88074,f1268]) ).

fof(f88578,plain,
    ( ! [X2] : s__02(sK3,sK7) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(sK3),sK5),s__02(c_27type_2elist_2elist_27__01(sK3),X2)))))
    | spl8_6
    | ~ spl8_28 ),
    inference(forward_demodulation,[],[f88568,f51624]) ).

fof(f89559,plain,
    ( s__02(sK3,sK7) = s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))
    | spl8_6
    | ~ spl8_28 ),
    inference(superposition,[],[f88578,f3630]) ).

fof(f90009,plain,
    ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6))))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))
    | spl8_6
    | ~ spl8_28 ),
    inference(superposition,[],[f88569,f265]) ).

fof(f90465,plain,
    ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eDIV_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))))),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2esptree_2efromList_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))
    | spl8_6
    | ~ spl8_28 ),
    inference(forward_demodulation,[],[f90009,f89559]) ).

fof(f90468,plain,
    ( s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2eoption_2eSOME_27__01(s__02(sK3,sK7))) = s__02(c_27type_2eoption_2eoption_27__01(sK3),c_27const_2esptree_2elookup_27__02(s__02(c_27type_2enum_2enum_27__00,sK4),s__02(c_27type_2esptree_2espt_27__01(sK3),c_27const_2emisc_2efromList2_27__01(s__02(c_27type_2elist_2elist_27__01(sK3),sK6)))))
    | spl8_6
    | ~ spl8_28
    | ~ spl8_29 ),
    inference(forward_demodulation,[],[f90465,f39450]) ).

fof(f90471,plain,
    ( $false
    | spl8_6
    | ~ spl8_28
    | ~ spl8_29 ),
    inference(forward_subsumption_resolution,[],[f90468,f269]) ).

fof(f90472,plain,
    ( spl8_6
    | ~ spl8_28
    | ~ spl8_29 ),
    inference(avatar_contradiction_clause,[],[f90471]) ).

cnf(s11,plain,
    ~ spl8_6,
    inference(sat_conversion,[],[f314]) ).

cnf(s35,plain,
    ( spl8_21
    | spl8_22 ),
    inference(sat_conversion,[],[f3453]) ).

cnf(s44,plain,
    ~ spl8_22,
    inference(sat_conversion,[],[f4280]) ).

cnf(s59,plain,
    ( spl8_22
    | spl8_28 ),
    inference(sat_conversion,[],[f5669]) ).

cnf(s60,plain,
    ( ~ spl8_21
    | spl8_25
    | spl8_29 ),
    inference(sat_conversion,[],[f5674]) ).

cnf(s70,plain,
    ~ spl8_25,
    inference(sat_conversion,[],[f5792]) ).

cnf(s996,plain,
    ( spl8_6
    | ~ spl8_28
    | ~ spl8_29 ),
    inference(sat_conversion,[],[f90472]) ).

cnf(s1041,plain,
    ( ~ spl8_21
    | spl8_29 ),
    inference(rat,[],[s60,s70]) ).

cnf(s1045,plain,
    spl8_28,
    inference(rat,[],[s59,s44]) ).

cnf(s1049,plain,
    spl8_21,
    inference(rat,[],[s35,s44]) ).

cnf(s1050,plain,
    spl8_29,
    inference(rat,[],[s1041,s1049]) ).

cnf(s1051,plain,
    spl8_6,
    inference(rat,[],[s996,s1045,s1050]) ).

cnf(s1052,plain,
    $false,
    inference(rat,[],[s11,s1051]) ).

fof(f90473,plain,
    $false,
    inference(avatar_sat_refutation,[],[s1052]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : SWW910+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10  % Computer : n012.cluster.edu
% 0.00/0.10  % Model    : x86_64 x86_64
% 0.00/0.10  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10  % Memory   : 8046.5625MB
% 0.00/0.10  % OS       : Linux 6.8.0-71-generic
% 0.00/0.10  % CPULimit : 300
% 0.00/0.10  % WCLimit  : 300
% 0.00/0.10  % DateTime : Mon Sep 28 14:39:34 UTC 2026
% 0.00/0.11  % CPUTime  : 
% 0.00/0.11  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12  Running first-order theorem proving
% 0.08/0.12  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.26/1.63  % (3426368)Detected formulas, will run a generic FOF schedule.
% 8.26/1.63  % (3426373)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=2696339302:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.26/1.63  % (3426378)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=778586886:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.26/1.63  % (3426374)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=3148212279:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.26/1.63  % (3426377)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2782485015:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.26/1.63  % (3426379)dis-21_1_sil=8000:lcm=predicate:random_seed=3766878266: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.26/1.63  % (3426376)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1312299757:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.26/1.63  % (3426375)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=3491504163:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.26/1.63  % (3426376)Refutation not found, incomplete strategy
% 8.26/1.63  % (3426376)------------------------------
% 8.26/1.63  % (3426376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.26/1.63  % (3426376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.63  % (3426376)CaDiCaL version: 2.1.3
% 8.26/1.63  % (3426376)Termination reason: Refutation not found, incomplete strategy
% 8.26/1.63  % (3426376)Time elapsed: 0.005 s
% 8.26/1.63  % (3426376)Peak memory usage: 88 MB
% 8.26/1.63  % (3426376)Instructions burned: 15 (million)
% 8.26/1.63  % (3426377)Instruction limit reached! 
% 8.26/1.63  % (3426377)------------------------------
% 8.26/1.63  % (3426377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.26/1.63  % (3426377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.63  % (3426377)CaDiCaL version: 2.1.3
% 8.26/1.63  % (3426377)Termination reason: Instruction limit
% 8.26/1.63  % (3426377)Termination phase: Saturation
% 8.26/1.63  % (3426377)Time elapsed: 0.032 s
% 8.26/1.63  % (3426377)Peak memory usage: 87 MB
% 8.26/1.63  % (3426377)Instructions burned: 119 (million)
% 8.26/1.63  % (3426379)Instruction limit reached! 
% 8.26/1.63  % (3426379)------------------------------
% 8.26/1.63  % (3426379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.26/1.63  % (3426379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.63  % (3426379)CaDiCaL version: 2.1.3
% 8.26/1.63  % (3426379)Termination reason: Instruction limit
% 8.26/1.63  % (3426379)Termination phase: Saturation
% 8.26/1.63  % (3426379)Time elapsed: 0.038 s
% 8.26/1.63  % (3426379)Peak memory usage: 89 MB
% 8.26/1.63  % (3426379)Instructions burned: 130 (million)
% 8.26/1.63  % (3426378)Instruction limit reached! 
% 8.26/1.63  % (3426378)------------------------------
% 8.26/1.63  % (3426378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.26/1.63  % (3426378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.63  % (3426378)CaDiCaL version: 2.1.3
% 8.26/1.63  % (3426378)Termination reason: Instruction limit
% 8.26/1.63  % (3426378)Termination phase: Saturation
% 8.26/1.63  % (3426378)Time elapsed: 0.042 s
% 8.26/1.63  % (3426378)Peak memory usage: 90 MB
% 8.26/1.63  % (3426378)Instructions burned: 140 (million)
% 8.26/1.63  % (3426387)lrs+10_1_sil=8000:sp=occurrence:random_seed=1796766188:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.26/1.63  % (3426389)lrs+1011_1_sil=32000:sp=occurrence:random_seed=334140582:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 8.26/1.63  % (3426388)lrs+10_1_sil=32000:urr=on:br=off:random_seed=137470122:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 8.26/1.63  % (3426376)------------------------------
% 8.26/1.63  % (3426376)------------------------------
% 8.26/1.63  % (3426388)Instruction limit reached! 
% 8.26/1.63  % (3426388)------------------------------
% 8.26/1.63  % (3426388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426388)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426388)Termination reason: Instruction limit
% 13.14/2.21  % (3426388)Termination phase: Saturation
% 13.14/2.21  % (3426388)Time elapsed: 0.047 s
% 13.14/2.21  % (3426388)Peak memory usage: 89 MB
% 13.14/2.21  % (3426388)Instructions burned: 160 (million)
% 13.14/2.21  % (3426387)Instruction limit reached! 
% 13.14/2.21  % (3426387)------------------------------
% 13.14/2.21  % (3426387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426387)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426387)Termination reason: Instruction limit
% 13.14/2.21  % (3426387)Termination phase: Saturation
% 13.14/2.21  % (3426387)Time elapsed: 0.081 s
% 13.14/2.21  % (3426387)Peak memory usage: 91 MB
% 13.14/2.21  % (3426387)Instructions burned: 287 (million)
% 13.14/2.21  % (3426389)Instruction limit reached! 
% 13.14/2.21  % (3426389)------------------------------
% 13.14/2.21  % (3426389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426389)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426389)Termination reason: Instruction limit
% 13.14/2.21  % (3426389)Termination phase: Saturation
% 13.14/2.21  % (3426389)Time elapsed: 0.094 s
% 13.14/2.21  % (3426389)Peak memory usage: 91 MB
% 13.14/2.21  % (3426389)Instructions burned: 329 (million)
% 13.14/2.21  % (3426393)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=2097551735:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 13.14/2.21  % (3426394)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2988050908:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 13.14/2.21  % (3426395)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=826056964:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 13.14/2.21  % (3426393)Instruction limit reached! 
% 13.14/2.21  % (3426393)------------------------------
% 13.14/2.21  % (3426393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426393)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426393)Termination reason: Instruction limit
% 13.14/2.21  % (3426393)Termination phase: Saturation
% 13.14/2.21  % (3426393)Time elapsed: 0.077 s
% 13.14/2.21  % (3426393)Peak memory usage: 90 MB
% 13.14/2.21  % (3426393)Instructions burned: 251 (million)
% 13.14/2.21  % (3426396)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3244963390:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 13.14/2.21  % (3426394)Instruction limit reached! 
% 13.14/2.21  % (3426394)------------------------------
% 13.14/2.21  % (3426394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426394)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426394)Termination reason: Instruction limit
% 13.14/2.21  % (3426394)Termination phase: Saturation
% 13.14/2.21  % (3426394)Time elapsed: 0.078 s
% 13.14/2.21  % (3426394)Peak memory usage: 89 MB
% 13.14/2.21  % (3426394)Instructions burned: 296 (million)
% 13.14/2.21  % (3426396)Instruction limit reached! 
% 13.14/2.21  % (3426396)------------------------------
% 13.14/2.21  % (3426396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426396)CaDiCaL version: 2.1.3
% 13.14/2.21  % (3426396)Termination reason: Instruction limit
% 13.14/2.21  % (3426396)Termination phase: Saturation
% 13.14/2.21  % (3426396)Time elapsed: 0.032 s
% 13.14/2.21  % (3426396)Peak memory usage: 89 MB
% 13.14/2.21  % (3426396)Instructions burned: 116 (million)
% 13.14/2.21  % (3426400)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=791412994:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 13.14/2.21  % (3426400)Instruction limit reached! 
% 13.14/2.21  % (3426400)------------------------------
% 13.14/2.21  % (3426400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.21  % (3426400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.21  % (3426400)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426400)Termination reason: Instruction limit
% 29.20/4.56  % (3426400)Termination phase: Saturation
% 29.20/4.56  % (3426400)Time elapsed: 0.031 s
% 29.20/4.56  % (3426400)Peak memory usage: 88 MB
% 29.20/4.56  % (3426400)Instructions burned: 128 (million)
% 29.20/4.56  % (3426402)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1855030479:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 29.20/4.56  % (3426403)lrs+10_1_sil=8000:sp=occurrence:random_seed=3703797036:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 29.20/4.56  % (3426402)Instruction limit reached! 
% 29.20/4.56  % (3426402)------------------------------
% 29.20/4.56  % (3426402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426402)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426402)Termination reason: Instruction limit
% 29.20/4.56  % (3426402)Termination phase: Saturation
% 29.20/4.56  % (3426402)Time elapsed: 0.030 s
% 29.20/4.56  % (3426402)Peak memory usage: 89 MB
% 29.20/4.56  % (3426402)Instructions burned: 117 (million)
% 29.20/4.56  % (3426405)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=64112952:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 29.20/4.56  % (3426408)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2819644122:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi)
% 29.20/4.56  % (3426405)Instruction limit reached! 
% 29.20/4.56  % (3426405)------------------------------
% 29.20/4.56  % (3426405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426405)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426405)Termination reason: Instruction limit
% 29.20/4.56  % (3426405)Termination phase: Saturation
% 29.20/4.56  % (3426405)Time elapsed: 0.106 s
% 29.20/4.56  % (3426405)Peak memory usage: 90 MB
% 29.20/4.56  % (3426405)Instructions burned: 439 (million)
% 29.20/4.56  % (3426403)Instruction limit reached! 
% 29.20/4.56  % (3426403)------------------------------
% 29.20/4.56  % (3426403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426403)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426403)Termination reason: Instruction limit
% 29.20/4.56  % (3426403)Termination phase: Saturation
% 29.20/4.56  % (3426403)Time elapsed: 0.248 s
% 29.20/4.56  % (3426403)Peak memory usage: 94 MB
% 29.20/4.56  % (3426403)Instructions burned: 909 (million)
% 29.20/4.56  % (3426411)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3723220532:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 29.20/4.56  % (3426411)Instruction limit reached! 
% 29.20/4.56  % (3426411)------------------------------
% 29.20/4.56  % (3426411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426411)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426411)Termination reason: Instruction limit
% 29.20/4.56  % (3426411)Termination phase: Saturation
% 29.20/4.56  % (3426411)Time elapsed: 0.036 s
% 29.20/4.56  % (3426411)Peak memory usage: 90 MB
% 29.20/4.56  % (3426411)Instructions burned: 138 (million)
% 29.20/4.56  % (3426412)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=967902083:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi)
% 29.20/4.56  % (3426415)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2520104378:st=3:i=13193:sd=3:ss=axioms_2989 on theBenchmark for (2989ds/13193Mi)
% 29.20/4.56  % (3426412)Instruction limit reached! 
% 29.20/4.56  % (3426412)------------------------------
% 29.20/4.56  % (3426412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426412)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426412)Termination reason: Instruction limit
% 29.20/4.56  % (3426412)Termination phase: Saturation
% 29.20/4.56  % (3426412)Time elapsed: 0.179 s
% 29.20/4.56  % (3426412)Peak memory usage: 93 MB
% 29.20/4.56  % (3426412)Instructions burned: 594 (million)
% 29.20/4.56  % (3426395)Instruction limit reached! 
% 29.20/4.56  % (3426395)------------------------------
% 29.20/4.56  % (3426395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426395)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426395)Termination reason: Instruction limit
% 29.20/4.56  % (3426395)Termination phase: Saturation
% 29.20/4.56  % (3426395)Time elapsed: 0.832 s
% 29.20/4.56  % (3426395)Peak memory usage: 140 MB
% 29.20/4.56  % (3426395)Instructions burned: 2350 (million)
% 29.20/4.56  % (3426417)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=16537187:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/125Mi)
% 29.20/4.56  % (3426417)Instruction limit reached! 
% 29.20/4.56  % (3426417)------------------------------
% 29.20/4.56  % (3426417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426417)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426417)Termination reason: Instruction limit
% 29.20/4.56  % (3426417)Termination phase: Saturation
% 29.20/4.56  % (3426417)Time elapsed: 0.030 s
% 29.20/4.56  % (3426417)Peak memory usage: 90 MB
% 29.20/4.56  % (3426417)Instructions burned: 127 (million)
% 29.20/4.56  % (3426418)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3148904086:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi)
% 29.20/4.56  % (3426418)Instruction limit reached! 
% 29.20/4.56  % (3426418)------------------------------
% 29.20/4.56  % (3426418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426418)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426418)Termination reason: Instruction limit
% 29.20/4.56  % (3426418)Termination phase: Saturation
% 29.20/4.56  % (3426418)Time elapsed: 0.040 s
% 29.20/4.56  % (3426418)Peak memory usage: 90 MB
% 29.20/4.56  % (3426418)Instructions burned: 135 (million)
% 29.20/4.56  % (3426420)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=178501923:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/141Mi)
% 29.20/4.56  % (3426420)Refutation not found, incomplete strategy
% 29.20/4.56  % (3426420)------------------------------
% 29.20/4.56  % (3426420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426420)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426420)Termination reason: Refutation not found, incomplete strategy
% 29.20/4.56  % (3426420)Time elapsed: 0.002 s
% 29.20/4.56  % (3426420)Peak memory usage: 88 MB
% 29.20/4.56  % (3426420)Instructions burned: 4 (million)
% 29.20/4.56  % (3426422)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3163120392:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/431Mi)
% 29.20/4.56  % (3426420)------------------------------
% 29.20/4.56  % (3426420)------------------------------
% 29.20/4.56  % (3426422)Instruction limit reached! 
% 29.20/4.56  % (3426422)------------------------------
% 29.20/4.56  % (3426422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426422)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426422)Termination reason: Instruction limit
% 29.20/4.56  % (3426422)Termination phase: Saturation
% 29.20/4.56  % (3426422)Time elapsed: 0.103 s
% 29.20/4.56  % (3426422)Peak memory usage: 89 MB
% 29.20/4.56  % (3426422)Instructions burned: 434 (million)
% 29.20/4.56  % (3426425)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3771917580:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi)
% 29.20/4.56  % (3426426)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3733408118:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi)
% 29.20/4.56  % (3426426)Instruction limit reached! 
% 29.20/4.56  % (3426426)------------------------------
% 29.20/4.56  % (3426426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426426)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426426)Termination reason: Instruction limit
% 29.20/4.56  % (3426426)Termination phase: Saturation
% 29.20/4.56  % (3426426)Time elapsed: 0.041 s
% 29.20/4.56  % (3426426)Peak memory usage: 90 MB
% 29.20/4.56  % (3426426)Instructions burned: 150 (million)
% 29.20/4.56  % (3426429)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3718724437:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi)
% 29.20/4.56  % (3426408)Instruction limit reached! 
% 29.20/4.56  % (3426408)------------------------------
% 29.20/4.56  % (3426408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426408)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426408)Termination reason: Instruction limit
% 29.20/4.56  % (3426408)Termination phase: Saturation
% 29.20/4.56  % (3426408)Time elapsed: 1.485 s
% 29.20/4.56  % (3426408)Peak memory usage: 139 MB
% 29.20/4.56  % (3426408)Instructions burned: 5206 (million)
% 29.20/4.56  % (3426431)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1014807636:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi)
% 29.20/4.56  % (3426431)Instruction limit reached! 
% 29.20/4.56  % (3426431)------------------------------
% 29.20/4.56  % (3426431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426431)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426431)Termination reason: Instruction limit
% 29.20/4.56  % (3426431)Termination phase: Saturation
% 29.20/4.56  % (3426431)Time elapsed: 0.191 s
% 29.20/4.56  % (3426431)Peak memory usage: 115 MB
% 29.20/4.56  % (3426431)Instructions burned: 669 (million)
% 29.20/4.56  % (3426433)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2708219226:s2a=on:i=185:s2at=1.8:fdi=4_2973 on theBenchmark for (2973ds/185Mi)
% 29.20/4.56  % (3426433)Instruction limit reached! 
% 29.20/4.56  % (3426433)------------------------------
% 29.20/4.56  % (3426433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426433)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426433)Termination reason: Instruction limit
% 29.20/4.56  % (3426433)Termination phase: Saturation
% 29.20/4.56  % (3426433)Time elapsed: 0.055 s
% 29.20/4.56  % (3426433)Peak memory usage: 91 MB
% 29.20/4.56  % (3426433)Instructions burned: 185 (million)
% 29.20/4.56  % (3426435)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4189533936:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/193Mi)
% 29.20/4.56  % (3426435)Instruction limit reached! 
% 29.20/4.56  % (3426435)------------------------------
% 29.20/4.56  % (3426435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426435)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426435)Termination reason: Instruction limit
% 29.20/4.56  % (3426435)Termination phase: Saturation
% 29.20/4.56  % (3426435)Time elapsed: 0.052 s
% 29.20/4.56  % (3426435)Peak memory usage: 89 MB
% 29.20/4.56  % (3426435)Instructions burned: 194 (million)
% 29.20/4.56  % (3426437)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1050800177:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2969 on theBenchmark for (2969ds/4850Mi)
% 29.20/4.56  % (3426425)Instruction limit reached! 
% 29.20/4.56  % (3426425)------------------------------
% 29.20/4.56  % (3426425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.20/4.56  % (3426425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.20/4.56  % (3426425)CaDiCaL version: 2.1.3
% 29.20/4.56  % (3426425)Termination reason: Instruction limit
% 29.20/4.56  % (3426425)Termination phase: Saturation
% 29.20/4.56  % (3426425)Time elapsed: 2.073 s
% 29.20/4.56  % (3426425)Peak memory usage: 166 MB
% 29.20/4.56  % (3426425)Instructions burned: 6061 (million)
% 29.20/4.56  % (3426439)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3273942086:i=12111:sd=1:ss=included_2961 on theBenchmark for (2961ds/12111Mi)
% 29.20/4.56  % (3426374)First to succeed.
% 29.20/4.56  % (3426374)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3426368"
% 29.20/4.56  % (3426374)Refutation found. Thanks to Tanya!
% 29.20/4.56  % SZS status Theorem for theBenchmark
% 29.20/4.56  % SZS output start Proof for theBenchmark
% See solution above
% 30.01/4.65  % (3426374)------------------------------
% 30.01/4.65  % (3426374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.01/4.65  % (3426374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.01/4.65  % (3426374)CaDiCaL version: 2.1.3
% 30.01/4.65  % (3426374)Termination reason: Refutation
% 30.01/4.65  % (3426374)Time elapsed: 3.924 s
% 30.01/4.65  % (3426374)Peak memory usage: 166 MB
% 30.01/4.65  % (3426374)Instructions burned: 13400 (million)
% 30.01/4.65  % (3426374)------------------------------
% 30.01/4.65  % (3426374)------------------------------
% 30.01/4.65  % (3426368)Success in time 4.237 s
% 30.01/4.65  % Vampire exiting
%------------------------------------------------------------------------------