%------------------------------------------------------------------------------
% File     : SWX207+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Ambiguous printing function
% Version  : Especial.
% English  :

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

% Status   : Theorem
% Rating   : 0.00 v9.3.0
% Syntax   : Number of formulae    :   27 (  26 unt;   0 def)
%            Number of atoms       :   28 (  28 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :   14 (  13   ~;   0   |;   0   &)
%                                         (   0 <=>;   1  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   3 avg)
%            Maximal term depth    :    4 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   19 (  19 usr;   6 con; 0-2 aty)
%            Number of variables   :   30 (  28   !;   2   ?)
% SPC      : FOF_THM_RFO_PEQ

% 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,
    ! [X] : proj1AP(aP(X)) = X ).

fof(axiom_006,axiom,
    ! [X] : proj1BP(bP(X)) = X ).

fof(axiom_007,axiom,
    ! [X,X2] : aP(X) != bP(X2) ).

fof(axiom_008,axiom,
    ! [X] : aP(X) != pA ).

fof(axiom_009,axiom,
    ! [X] : aP(X) != pB ).

fof(axiom_010,axiom,
    ! [X] : aP(X) != pE ).

fof(axiom_011,axiom,
    ! [X] : bP(X) != pA ).

fof(axiom_012,axiom,
    ! [X] : bP(X) != pB ).

fof(axiom_013,axiom,
    ! [X] : bP(X) != pE ).

fof(axiom_014,axiom,
    pA != pB ).

fof(axiom_015,axiom,
    pA != pE ).

fof(axiom_016,axiom,
    pB != pE ).

fof(axiom_017,axiom,
    ! [X,X2] : proj1C(c2(X,X2)) = X ).

fof(axiom_018,axiom,
    ! [X,X2] : proj2C(c2(X,X2)) = X2 ).

fof(axiom_019,axiom,
    ! [Y] : append(nil,Y) = Y ).

fof(axiom_020,axiom,
    ! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).

fof(axiom_021,axiom,
    ! [P] : linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil))) ).

fof(axiom_022,axiom,
    ! [Q] : linP(bP(Q)) = append(cons(b,nil),append(linP(Q),cons(b,nil))) ).

fof(axiom_023,axiom,
    linP(pA) = cons(a,nil) ).

fof(axiom_024,axiom,
    linP(pB) = cons(b,nil) ).

fof(axiom_025,axiom,
    linP(pE) = nil ).

fof(axiom_026,axiom,
    ! [P,Q] : linC(c2(P,Q)) = append(linP(P),linP(Q)) ).

fof(goal_027,conjecture,
    ? [U,V] :
      ~ ( linC(U) = linC(V)
       => U = V ) ).

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