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

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

% Status   : Theorem
% Rating   : 0.25 v9.3.0
% Syntax   : Number of formulae    :   41 (  37 unt;   0 def)
%            Number of atoms       :   46 (  46 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   32 (  27   ~;   0   |;   0   &)
%                                         (   0 <=>;   5  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    6 (   3 avg)
%            Maximal term depth    :    5 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   22 (  22 usr;   9 con; 0-2 aty)
%            Number of variables   :   47 (  45   !;   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,
    c != d ).

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

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

fof(axiom_007,axiom,
    c != plus ).

fof(axiom_008,axiom,
    c != mul ).

fof(axiom_009,axiom,
    d != x ).

fof(axiom_010,axiom,
    d != y ).

fof(axiom_011,axiom,
    d != plus ).

fof(axiom_012,axiom,
    d != mul ).

fof(axiom_013,axiom,
    x != y ).

fof(axiom_014,axiom,
    x != plus ).

fof(axiom_015,axiom,
    x != mul ).

fof(axiom_016,axiom,
    y != plus ).

fof(axiom_017,axiom,
    y != mul ).

fof(axiom_018,axiom,
    plus != mul ).

fof(axiom_019,axiom,
    ! [X,X2] : proj1(z(X,X2)) = X ).

fof(axiom_020,axiom,
    ! [X,X2] : proj2(z(X,X2)) = X2 ).

fof(axiom_021,axiom,
    ! [X,X2] : proj12(x2(X,X2)) = X ).

fof(axiom_022,axiom,
    ! [X,X2] : proj22(x2(X,X2)) = X2 ).

fof(axiom_023,axiom,
    ! [X,X2,X3,X4] : z(X,X2) != x2(X3,X4) ).

fof(axiom_024,axiom,
    ! [X,X2] : z(X,X2) != eX ).

fof(axiom_025,axiom,
    ! [X,X2] : z(X,X2) != eY ).

fof(axiom_026,axiom,
    ! [X,X2] : x2(X,X2) != eX ).

fof(axiom_027,axiom,
    ! [X,X2] : x2(X,X2) != eY ).

fof(axiom_028,axiom,
    eX != eY ).

fof(axiom_029,axiom,
    ! [X] :
      ( X != z(proj1(X),proj2(X))
     => ( X != x2(proj12(X),proj22(X))
       => assoc(X) = X ) ) ).

fof(axiom_030,axiom,
    ! [Y,C] :
      ( Y != z(proj1(Y),proj2(Y))
     => assoc(z(Y,C)) = z(assoc(Y),assoc(C)) ) ).

fof(axiom_031,axiom,
    ! [C,A,B] : assoc(z(z(A,B),C)) = assoc(z(A,z(B,C))) ).

fof(axiom_032,axiom,
    ! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)) ).

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

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

fof(axiom_035,axiom,
    ! [X] :
      ( X != x2(proj12(X),proj22(X))
     => linTerm(X) = lin(X) ) ).

fof(axiom_036,axiom,
    ! [A,B] : linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil))) ).

fof(axiom_037,axiom,
    ! [A,B] : lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B))) ).

fof(axiom_038,axiom,
    ! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))) ).

fof(axiom_039,axiom,
    lin(eX) = cons(x,nil) ).

fof(axiom_040,axiom,
    lin(eY) = cons(y,nil) ).

fof(goal_041,conjecture,
    ? [U,V] :
      ~ ( lin(U) = lin(V)
       => assoc(U) = assoc(V) ) ).

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