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. %------------------------------------------------------------------------------