%------------------------------------------------------------------------------
% File     : SWX214+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Faulty property of regular expressions
% Version  : Especial.
% English  :

% Refs     : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source   : [CST26]
% Names    : RegExp_prop_star_plus_easy.p [CST26]

% Status   : Theorem
% Rating   : 1.00 v9.3.0
% Syntax   : Number of formulae    :   50 (  33 unt;   0 def)
%            Number of atoms       :   80 (  63 equ)
%            Maximal formula atoms :    5 (   1 avg)
%            Number of connectives :   71 (  41   ~;   1   |;   1   &)
%                                         (   4 <=>;  23  =>;   0  <=;   1 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of predicates  :    3 (   2 usr;   0 prp; 1-2 aty)
%            Number of functors    :   22 (  22 usr;   6 con; 0-2 aty)
%            Number of variables   :   87 (  83   !;   4   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
    ! [X,X2] : head(cons(X,X2)) = X ).

fof(axiom_002,axiom,
    ! [X,X2] : tail(cons(X,X2)) = X2 ).

fof(axiom_003,axiom,
    ! [X,X2] : nil != cons(X,X2) ).

fof(axiom_004,axiom,
    a != b ).

fof(axiom_005,axiom,
    a != c ).

fof(axiom_006,axiom,
    b != c ).

fof(axiom_007,axiom,
    ! [X] : proj1Atom(atom(X)) = X ).

fof(axiom_008,axiom,
    ! [X,X2] : proj1(x(X,X2)) = X ).

fof(axiom_009,axiom,
    ! [X,X2] : proj2(x(X,X2)) = X2 ).

fof(axiom_010,axiom,
    ! [X,X2] : proj12(y(X,X2)) = X ).

fof(axiom_011,axiom,
    ! [X,X2] : proj22(y(X,X2)) = X2 ).

fof(axiom_012,axiom,
    ! [X] : proj1Star(star(X)) = X ).

fof(axiom_013,axiom,
    nil2 != eps ).

fof(axiom_014,axiom,
    ! [X] : nil2 != atom(X) ).

fof(axiom_015,axiom,
    ! [X,X2] : nil2 != x(X,X2) ).

fof(axiom_016,axiom,
    ! [X,X2] : nil2 != y(X,X2) ).

fof(axiom_017,axiom,
    ! [X] : nil2 != star(X) ).

fof(axiom_018,axiom,
    ! [X] : eps != atom(X) ).

fof(axiom_019,axiom,
    ! [X,X2] : eps != x(X,X2) ).

fof(axiom_020,axiom,
    ! [X,X2] : eps != y(X,X2) ).

fof(axiom_021,axiom,
    ! [X] : eps != star(X) ).

fof(axiom_022,axiom,
    ! [X,X2,X3] : atom(X) != x(X2,X3) ).

fof(axiom_023,axiom,
    ! [X,X2,X3] : atom(X) != y(X2,X3) ).

fof(axiom_024,axiom,
    ! [X,X2] : atom(X) != star(X2) ).

fof(axiom_025,axiom,
    ! [X,X2,X3,X4] : x(X,X2) != y(X3,X4) ).

fof(axiom_026,axiom,
    ! [X,X2,X3] : x(X,X2) != star(X3) ).

fof(axiom_027,axiom,
    ! [X,X2,X3] : y(X,X2) != star(X3) ).

fof(axiom_028,axiom,
    ! [X,Y] :
      ( X != nil2
     => ( Y != nil2
       => ( X != eps
         => ( Y != eps
           => z(X,Y) = y(X,Y) ) ) ) ) ).

fof(axiom_029,axiom,
    ! [X] :
      ( X != nil2
     => ( X != eps
       => z(X,eps) = X ) ) ).

fof(axiom_030,axiom,
    ! [Y] :
      ( Y != nil2
     => z(eps,Y) = Y ) ).

fof(axiom_031,axiom,
    ! [X] :
      ( X != nil2
     => z(X,nil2) = nil2 ) ).

fof(axiom_032,axiom,
    ! [Y] : z(nil2,Y) = nil2 ).

fof(axiom_033,axiom,
    ! [X,Y] :
      ( X != nil2
     => ( Y != nil2
       => x2(X,Y) = x(X,Y) ) ) ).

fof(axiom_034,axiom,
    ! [X] :
      ( X != nil2
     => x2(X,nil2) = X ) ).

fof(axiom_035,axiom,
    ! [Y] : x2(nil2,Y) = Y ).

fof(axiom_036,axiom,
    ! [X] :
      ( X != eps
     => ( X != x(proj1(X),proj2(X))
       => ( X != y(proj12(X),proj22(X))
         => ( X != star(proj1Star(X))
           => ~ eps2(X) ) ) ) ) ).

fof(axiom_037,axiom,
    eps2(eps) ).

fof(axiom_038,axiom,
    ! [P,Q] :
      ( eps2(x(P,Q))
    <=> ( eps2(P)
        | eps2(Q) ) ) ).

fof(axiom_039,axiom,
    ! [R,Q2] :
      ( eps2(y(R,Q2))
    <=> ( eps2(R)
        & eps2(Q2) ) ) ).

fof(axiom_040,axiom,
    ! [Y] : eps2(star(Y)) ).

fof(axiom_041,axiom,
    ! [X,Y] :
      ( X != atom(proj1Atom(X))
     => ( X != x(proj1(X),proj2(X))
       => ( X != y(proj12(X),proj22(X))
         => ( X != star(proj1Star(X))
           => step(X,Y) = nil2 ) ) ) ) ).

fof(axiom_042,axiom,
    ! [Y,B] :
      ( B = Y
     => step(atom(B),Y) = eps ) ).

fof(axiom_043,axiom,
    ! [Y,B] :
      ( B != Y
     => step(atom(B),Y) = nil2 ) ).

fof(axiom_044,axiom,
    ! [Y,P,Q] : step(x(P,Q),Y) = x(step(P,Y),step(Q,Y)) ).

fof(axiom_045,axiom,
    ! [Y,R,Q2] :
      ( eps2(R)
     => step(y(R,Q2),Y) = x(y(step(R,Y),Q2),step(Q2,Y)) ) ).

fof(axiom_046,axiom,
    ! [Y,R,Q2] :
      ( ~ eps2(R)
     => step(y(R,Q2),Y) = x(y(step(R,Y),Q2),nil2) ) ).

fof(axiom_047,axiom,
    ! [Y,P2] : step(star(P2),Y) = y(step(P2,Y),star(P2)) ).

fof(axiom_048,axiom,
    ! [X] :
      ( rec(X,nil)
    <=> eps2(X) ) ).

fof(axiom_049,axiom,
    ! [X,Z,Xs] :
      ( rec(X,cons(Z,Xs))
    <=> rec(step(X,Z),Xs) ) ).

fof(goal_050,conjecture,
    ? [P,Q,A,B] :
      ( rec(star(x(P,Q)),cons(A,cons(B,nil)))
    <~> rec(x(star(P),star(Q)),cons(A,cons(B,nil))) ) ).

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