assign(max_seconds, 30).

%------------------------------------------------------------------------------
% File     : SWC258+1 : TPTP v3.0.1. Released v2.4.0.
% Domain   : Software Creation
% Problem  : cond_pst_sorted1_x_minimal
% Version  : [Wei00] axioms.
% English  : Find components in a software library that match a given target
%            specification given in first-order logic. The components are
%            specified in first-order logic as well. The problem represents
%            a test of one library module specification against a target
%            specification.

% Refs     : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
%          : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% Source   : [Wei00]
% Names    : cond_pst_sorted1_x_minimal [Wei00]

% Status   : Theorem
% Rating   : 0.56 v2.7.0, 0.50 v2.4.0
% Syntax   : Number of formulae    :   96 (   9 unit)
%            Number of atoms       :  410 (  77 equality)
%            Maximal formula depth :   21 (   7 average)
%            Number of connectives :  345 (  31 ~  ;  14  |;  42  &)
%                                         (  26 <=>; 232 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   20 (   0 propositional; 1-2 arity)
%            Number of functors    :    5 (   1 constant; 0-2 arity)
%            Number of variables   :  209 (   0 singleton; 195 !;  14 ?)
%            Maximal term depth    :    4 (   1 average)

% Comments : 
%          : tptp2X -f mace4 SWC258+1.p 
%------------------------------------------------------------------------------
%----NOTE WELL: conjecture has been negated
set(prolog_style_variables).

formulas(assumptions).

% ax1, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( neq(U,V)
           <-> -(U = V) ) ) ) ) ).

% ax2, axiom.
    ( exists U 
      ( ssItem(U)
       & ( exists V 
          ( ssItem(V)
           & -(U = V) ) ) ) ).

% ax3, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> ( memberP(U,V)
           <-> ( exists W 
                ( ssList(W)
                 & ( exists X 
                    ( ssList(X)
                     & app(W,cons(V,X)) = U ) ) ) ) ) ) ) ) ).

% ax4, axiom.
    ( all U 
      ( ssList(U)
      -> ( singletonP(U)
       <-> ( exists V 
            ( ssItem(V)
             & cons(V,nil) = U ) ) ) ) ).

% ax5, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( frontsegP(U,V)
           <-> ( exists W 
                ( ssList(W)
                 & app(V,W) = U ) ) ) ) ) ) ).

% ax6, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( rearsegP(U,V)
           <-> ( exists W 
                ( ssList(W)
                 & app(W,V) = U ) ) ) ) ) ) ).

% ax7, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( segmentP(U,V)
           <-> ( exists W 
                ( ssList(W)
                 & ( exists X 
                    ( ssList(X)
                     & app(app(W,V),X) = U ) ) ) ) ) ) ) ) ).

% ax8, axiom.
    ( all U 
      ( ssList(U)
      -> ( cyclefreeP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> -(( leq(V,W)
                                   & leq(W,V) )) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax9, axiom.
    ( all U 
      ( ssList(U)
      -> ( totalorderP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> ( leq(V,W)
                                 | leq(W,V) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax10, axiom.
    ( all U 
      ( ssList(U)
      -> ( strictorderP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> ( lt(V,W)
                                 | lt(W,V) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax11, axiom.
    ( all U 
      ( ssList(U)
      -> ( totalorderedP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> leq(V,W) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax12, axiom.
    ( all U 
      ( ssList(U)
      -> ( strictorderedP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> lt(V,W) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax13, axiom.
    ( all U 
      ( ssList(U)
      -> ( duplicatefreeP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( all Z 
                            ( ssList(Z)
                            -> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
                              -> -(V = W) ) ) ) ) ) ) ) ) ) ) ) ) ) ).

% ax14, axiom.
    ( all U 
      ( ssList(U)
      -> ( equalelemsP(U)
       <-> ( all V 
            ( ssItem(V)
            -> ( all W 
                ( ssItem(W)
                -> ( all X 
                    ( ssList(X)
                    -> ( all Y 
                        ( ssList(Y)
                        -> ( app(X,cons(V,cons(W,Y))) = U
                          -> V = W ) ) ) ) ) ) ) ) ) ) ) ).

% ax15, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( neq(U,V)
           <-> -(U = V) ) ) ) ) ).

% ax16, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> ssList(cons(V,U)) ) ) ) ).

% ax17, axiom.
    ssList(nil).

% ax18, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> -(cons(V,U) = U) ) ) ) ).

% ax19, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssItem(W)
              -> ( all X 
                  ( ssItem(X)
                  -> ( cons(W,U) = cons(X,V)
                    -> ( W = X
                       & V = U ) ) ) ) ) ) ) ) ) ).

% ax20, axiom.
    ( all U 
      ( ssList(U)
      -> ( nil = U
         | ( exists V 
            ( ssList(V)
             & ( exists W 
                ( ssItem(W)
                 & cons(W,V) = U ) ) ) ) ) ) ).

% ax21, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> -(nil = cons(V,U)) ) ) ) ).

% ax22, axiom.
    ( all U 
      ( ssList(U)
      -> ( -(nil = U)
        -> ssItem(hd(U)) ) ) ).

% ax23, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> hd(cons(V,U)) = V ) ) ) ).

% ax24, axiom.
    ( all U 
      ( ssList(U)
      -> ( -(nil = U)
        -> ssList(tl(U)) ) ) ).

% ax25, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> tl(cons(V,U)) = U ) ) ) ).

% ax26, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ssList(app(U,V)) ) ) ) ).

% ax27, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssItem(W)
              -> cons(W,app(V,U)) = app(cons(W,V),U) ) ) ) ) ) ).

% ax28, axiom.
    ( all U 
      ( ssList(U)
      -> app(nil,U) = U ) ).

% ax29, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( ( leq(U,V)
               & leq(V,U) )
            -> U = V ) ) ) ) ).

% ax30, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssItem(W)
              -> ( ( leq(U,V)
                   & leq(V,W) )
                -> leq(U,W) ) ) ) ) ) ) ).

% ax31, axiom.
    ( all U 
      ( ssItem(U)
      -> leq(U,U) ) ).

% ax32, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( geq(U,V)
           <-> leq(V,U) ) ) ) ) ).

% ax33, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( lt(U,V)
            -> -(lt(V,U)) ) ) ) ) ).

% ax34, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssItem(W)
              -> ( ( lt(U,V)
                   & lt(V,W) )
                -> lt(U,W) ) ) ) ) ) ) ).

% ax35, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( gt(U,V)
           <-> lt(V,U) ) ) ) ) ).

% ax36, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( memberP(app(V,W),U)
               <-> ( memberP(V,U)
                   | memberP(W,U) ) ) ) ) ) ) ) ).

% ax37, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssList(W)
              -> ( memberP(cons(V,W),U)
               <-> ( U = V
                   | memberP(W,U) ) ) ) ) ) ) ) ).

% ax38, axiom.
    ( all U 
      ( ssItem(U)
      -> -(memberP(nil,U)) ) ).

% ax39, axiom.
    -(singletonP(nil)).

% ax40, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( ( frontsegP(U,V)
                   & frontsegP(V,W) )
                -> frontsegP(U,W) ) ) ) ) ) ) ).

% ax41, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( ( frontsegP(U,V)
               & frontsegP(V,U) )
            -> U = V ) ) ) ) ).

% ax42, axiom.
    ( all U 
      ( ssList(U)
      -> frontsegP(U,U) ) ).

% ax43, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( frontsegP(U,V)
                -> frontsegP(app(U,W),V) ) ) ) ) ) ) ).

% ax44, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssList(W)
              -> ( all X 
                  ( ssList(X)
                  -> ( frontsegP(cons(U,W),cons(V,X))
                   <-> ( U = V
                       & frontsegP(W,X) ) ) ) ) ) ) ) ) ) ).

% ax45, axiom.
    ( all U 
      ( ssList(U)
      -> frontsegP(U,nil) ) ).

% ax46, axiom.
    ( all U 
      ( ssList(U)
      -> ( frontsegP(nil,U)
       <-> nil = U ) ) ).

% ax47, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( ( rearsegP(U,V)
                   & rearsegP(V,W) )
                -> rearsegP(U,W) ) ) ) ) ) ) ).

% ax48, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( ( rearsegP(U,V)
               & rearsegP(V,U) )
            -> U = V ) ) ) ) ).

% ax49, axiom.
    ( all U 
      ( ssList(U)
      -> rearsegP(U,U) ) ).

% ax50, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( rearsegP(U,V)
                -> rearsegP(app(W,U),V) ) ) ) ) ) ) ).

% ax51, axiom.
    ( all U 
      ( ssList(U)
      -> rearsegP(U,nil) ) ).

% ax52, axiom.
    ( all U 
      ( ssList(U)
      -> ( rearsegP(nil,U)
       <-> nil = U ) ) ).

% ax53, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( ( segmentP(U,V)
                   & segmentP(V,W) )
                -> segmentP(U,W) ) ) ) ) ) ) ).

% ax54, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( ( segmentP(U,V)
               & segmentP(V,U) )
            -> U = V ) ) ) ) ).

% ax55, axiom.
    ( all U 
      ( ssList(U)
      -> segmentP(U,U) ) ).

% ax56, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( all X 
                  ( ssList(X)
                  -> ( segmentP(U,V)
                    -> segmentP(app(app(W,U),X),V) ) ) ) ) ) ) ) ) ).

% ax57, axiom.
    ( all U 
      ( ssList(U)
      -> segmentP(U,nil) ) ).

% ax58, axiom.
    ( all U 
      ( ssList(U)
      -> ( segmentP(nil,U)
       <-> nil = U ) ) ).

% ax59, axiom.
    ( all U 
      ( ssItem(U)
      -> cyclefreeP(cons(U,nil)) ) ).

% ax60, axiom.
    cyclefreeP(nil).

% ax61, axiom.
    ( all U 
      ( ssItem(U)
      -> totalorderP(cons(U,nil)) ) ).

% ax62, axiom.
    totalorderP(nil).

% ax63, axiom.
    ( all U 
      ( ssItem(U)
      -> strictorderP(cons(U,nil)) ) ).

% ax64, axiom.
    strictorderP(nil).

% ax65, axiom.
    ( all U 
      ( ssItem(U)
      -> totalorderedP(cons(U,nil)) ) ).

% ax66, axiom.
    totalorderedP(nil).

% ax67, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssList(V)
          -> ( totalorderedP(cons(U,V))
           <-> ( nil = V
               | ( -(nil = V)
                 & totalorderedP(V)
                 & leq(U,hd(V)) ) ) ) ) ) ) ).

% ax68, axiom.
    ( all U 
      ( ssItem(U)
      -> strictorderedP(cons(U,nil)) ) ).

% ax69, axiom.
    strictorderedP(nil).

% ax70, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssList(V)
          -> ( strictorderedP(cons(U,V))
           <-> ( nil = V
               | ( -(nil = V)
                 & strictorderedP(V)
                 & lt(U,hd(V)) ) ) ) ) ) ) ).

% ax71, axiom.
    ( all U 
      ( ssItem(U)
      -> duplicatefreeP(cons(U,nil)) ) ).

% ax72, axiom.
    duplicatefreeP(nil).

% ax73, axiom.
    ( all U 
      ( ssItem(U)
      -> equalelemsP(cons(U,nil)) ) ).

% ax74, axiom.
    equalelemsP(nil).

% ax75, axiom.
    ( all U 
      ( ssList(U)
      -> ( -(nil = U)
        -> ( exists V 
            ( ssItem(V)
             & hd(U) = V ) ) ) ) ).

% ax76, axiom.
    ( all U 
      ( ssList(U)
      -> ( -(nil = U)
        -> ( exists V 
            ( ssList(V)
             & tl(U) = V ) ) ) ) ).

% ax77, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( ( -(nil = V)
               & -(nil = U)
               & hd(V) = hd(U)
               & tl(V) = tl(U) )
            -> V = U ) ) ) ) ).

% ax78, axiom.
    ( all U 
      ( ssList(U)
      -> ( -(nil = U)
        -> cons(hd(U),tl(U)) = U ) ) ).

% ax79, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( app(W,V) = app(U,V)
                -> W = U ) ) ) ) ) ) ).

% ax80, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> ( app(V,W) = app(V,U)
                -> W = U ) ) ) ) ) ) ).

% ax81, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssItem(V)
          -> cons(V,U) = app(cons(V,nil),U) ) ) ) ).

% ax82, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( all W 
              ( ssList(W)
              -> app(app(U,V),W) = app(U,app(V,W)) ) ) ) ) ) ).

% ax83, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( nil = app(U,V)
           <-> ( nil = V
               & nil = U ) ) ) ) ) ).

% ax84, axiom.
    ( all U 
      ( ssList(U)
      -> app(U,nil) = U ) ).

% ax85, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( -(nil = U)
            -> hd(app(U,V)) = hd(U) ) ) ) ) ).

% ax86, axiom.
    ( all U 
      ( ssList(U)
      -> ( all V 
          ( ssList(V)
          -> ( -(nil = U)
            -> tl(app(U,V)) = app(tl(U),V) ) ) ) ) ).

% ax87, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( ( geq(U,V)
               & geq(V,U) )
            -> U = V ) ) ) ) ).

% ax88, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssItem(W)
              -> ( ( geq(U,V)
                   & geq(V,W) )
                -> geq(U,W) ) ) ) ) ) ) ).

% ax89, axiom.
    ( all U 
      ( ssItem(U)
      -> geq(U,U) ) ).

% ax90, axiom.
    ( all U 
      ( ssItem(U)
      -> -(lt(U,U)) ) ).

% ax91, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssItem(W)
              -> ( ( leq(U,V)
                   & lt(V,W) )
                -> lt(U,W) ) ) ) ) ) ) ).

% ax92, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( leq(U,V)
            -> ( U = V
               | lt(U,V) ) ) ) ) ) ).

% ax93, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( lt(U,V)
           <-> ( -(U = V)
               & leq(U,V) ) ) ) ) ) ).

% ax94, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( gt(U,V)
            -> -(gt(V,U)) ) ) ) ) ).

% ax95, axiom.
    ( all U 
      ( ssItem(U)
      -> ( all V 
          ( ssItem(V)
          -> ( all W 
              ( ssItem(W)
              -> ( ( gt(U,V)
                   & gt(V,W) )
                -> gt(U,W) ) ) ) ) ) ) ).

% co1, negated_conjecture.
    -(( ( all U 
          ( ssList(U)
          -> ( all V 
              ( ssList(V)
              -> ( all W 
                  ( ssList(W)
                  -> ( all X 
                      ( ssList(X)
                      -> ( -(V = X)
                         | -(U = W)
                         | totalorderedP(U)
                         | ( ( all Y 
                              ( ssItem(Y)
                              -> ( -(cons(Y,nil) = W)
                                 | -(memberP(X,Y))
                                 | ( exists Z 
                                    ( ssItem(Z)
                                     & -(Y = Z)
                                     & memberP(X,Z)
                                     & leq(Z,Y) ) ) ) ) )
                           & ( -(nil = X)
                             | -(nil = W) ) ) ) ) ) ) ) ) ) ) ) )).
end_of_list.

%------------------------------------------------------------------------------
