%------------------------------------------------------------------------------
% 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   : Unsatisfiable
% Rating   : 0.33 v9.3.0
% Syntax   : Number of clauses     :   77 (  71 unt;   0 nHn;  41 RR)
%            Number of literals    :   83 (  83 equ;   7 neg)
%            Maximal clause size   :    2 (   1 avg)
%            Maximal term depth    :    5 (   1 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   24 (  24 usr;  11 con; 0-2 aty)
%            Number of variables   :   84 (  37 sgn)
% SPC      : CNF_UNS_RFO_PEQ_NUE

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    impl(btrue,Q) = Q ).

cnf(axiom_001,axiom,
    impl(bfalse,Q) = btrue ).

cnf(axiom_002,axiom,
    assoc(z(z(A,B),C)) = assoc(z(A,z(B,C))) ).

cnf(axiom_003,axiom,
    assoc(z(x2(X,X2),C)) = z(assoc(x2(X,X2)),assoc(C)) ).

cnf(axiom_004,axiom,
    assoc(z(eX,C)) = z(assoc(eX),assoc(C)) ).

cnf(axiom_005,axiom,
    assoc(z(eY,C)) = z(assoc(eY),assoc(C)) ).

cnf(axiom_006,axiom,
    assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)) ).

cnf(axiom_007,axiom,
    assoc(eX) = eX ).

cnf(axiom_008,axiom,
    assoc(eY) = eY ).

cnf(axiom_009,axiom,
    append(nil,Y) = Y ).

cnf(axiom_010,axiom,
    append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).

cnf(axiom_011,axiom,
    linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil))) ).

cnf(axiom_012,axiom,
    linTerm(z(X,X2)) = lin(z(X,X2)) ).

cnf(axiom_013,axiom,
    linTerm(eX) = lin(eX) ).

cnf(axiom_014,axiom,
    linTerm(eY) = lin(eY) ).

cnf(axiom_015,axiom,
    lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B))) ).

cnf(axiom_016,axiom,
    lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))) ).

cnf(axiom_017,axiom,
    lin(eX) = cons(x,nil) ).

cnf(axiom_018,axiom,
    lin(eY) = cons(y,nil) ).

cnf(axiom_019,axiom,
    prop_unambig(X,Y) = impl(eq(lin(X),lin(Y)),eq3(assoc(X),assoc(Y))) ).

cnf(axiom_020,axiom,
    eq2(c,d) = bfalse ).

cnf(axiom_021,axiom,
    eq2(c,x) = bfalse ).

cnf(axiom_022,axiom,
    eq2(c,y) = bfalse ).

cnf(axiom_023,axiom,
    eq2(c,plus) = bfalse ).

cnf(axiom_024,axiom,
    eq2(c,mul) = bfalse ).

cnf(axiom_025,axiom,
    eq2(d,c) = bfalse ).

cnf(axiom_026,axiom,
    eq2(d,x) = bfalse ).

cnf(axiom_027,axiom,
    eq2(d,y) = bfalse ).

cnf(axiom_028,axiom,
    eq2(d,plus) = bfalse ).

cnf(axiom_029,axiom,
    eq2(d,mul) = bfalse ).

cnf(axiom_030,axiom,
    eq2(x,c) = bfalse ).

cnf(axiom_031,axiom,
    eq2(x,d) = bfalse ).

cnf(axiom_032,axiom,
    eq2(x,y) = bfalse ).

cnf(axiom_033,axiom,
    eq2(x,plus) = bfalse ).

cnf(axiom_034,axiom,
    eq2(x,mul) = bfalse ).

cnf(axiom_035,axiom,
    eq2(y,c) = bfalse ).

cnf(axiom_036,axiom,
    eq2(y,d) = bfalse ).

cnf(axiom_037,axiom,
    eq2(y,x) = bfalse ).

cnf(axiom_038,axiom,
    eq2(y,plus) = bfalse ).

cnf(axiom_039,axiom,
    eq2(y,mul) = bfalse ).

cnf(axiom_040,axiom,
    eq2(plus,c) = bfalse ).

cnf(axiom_041,axiom,
    eq2(plus,d) = bfalse ).

cnf(axiom_042,axiom,
    eq2(plus,x) = bfalse ).

cnf(axiom_043,axiom,
    eq2(plus,y) = bfalse ).

cnf(axiom_044,axiom,
    eq2(plus,mul) = bfalse ).

cnf(axiom_045,axiom,
    eq2(mul,c) = bfalse ).

cnf(axiom_046,axiom,
    eq2(mul,d) = bfalse ).

cnf(axiom_047,axiom,
    eq2(mul,x) = bfalse ).

cnf(axiom_048,axiom,
    eq2(mul,y) = bfalse ).

cnf(axiom_049,axiom,
    eq2(mul,plus) = bfalse ).

cnf(axiom_050,axiom,
    eq3(eX,eY) = bfalse ).

cnf(axiom_051,axiom,
    eq3(eY,eX) = bfalse ).

cnf(axiom_052,axiom,
    eq4(bfalse,btrue) = bfalse ).

cnf(axiom_053,axiom,
    eq4(btrue,bfalse) = bfalse ).

cnf(axiom_054,axiom,
    ( eq3(X,Z) != bfalse
    | eq3(z(X,Y),z(Z,X2)) = bfalse ) ).

cnf(axiom_055,axiom,
    ( eq3(X,Z) != btrue
    | eq3(z(X,Y),z(Z,X2)) = eq3(Y,X2) ) ).

cnf(axiom_056,axiom,
    ( eq3(X,Z) != bfalse
    | eq3(x2(X,Y),x2(Z,X2)) = bfalse ) ).

cnf(axiom_057,axiom,
    ( eq3(X,Z) != btrue
    | eq3(x2(X,Y),x2(Z,X2)) = eq3(Y,X2) ) ).

cnf(axiom_058,axiom,
    eq3(z(X,Y),x2(Z,X2)) = bfalse ).

cnf(axiom_059,axiom,
    eq3(z(X,Y),eX) = bfalse ).

cnf(axiom_060,axiom,
    eq3(z(X,Y),eY) = bfalse ).

cnf(axiom_061,axiom,
    eq3(x2(X,Y),z(Z,X2)) = bfalse ).

cnf(axiom_062,axiom,
    eq3(x2(X,Y),eX) = bfalse ).

cnf(axiom_063,axiom,
    eq3(x2(X,Y),eY) = bfalse ).

cnf(axiom_064,axiom,
    eq3(eX,z(X,Y)) = bfalse ).

cnf(axiom_065,axiom,
    eq3(eX,x2(X,Y)) = bfalse ).

cnf(axiom_066,axiom,
    eq3(eY,z(X,Y)) = bfalse ).

cnf(axiom_067,axiom,
    eq3(eY,x2(X,Y)) = bfalse ).

cnf(axiom_068,axiom,
    eq(X,X) = btrue ).

cnf(axiom_069,axiom,
    eq2(X,X) = btrue ).

cnf(axiom_070,axiom,
    eq3(X,X) = btrue ).

cnf(axiom_071,axiom,
    eq4(X,X) = btrue ).

cnf(axiom_072,axiom,
    ( eq2(X,Z) != bfalse
    | eq(cons(X,Y),cons(Z,X2)) = bfalse ) ).

cnf(axiom_073,axiom,
    ( eq2(X,Z) != btrue
    | eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ).

cnf(axiom_074,axiom,
    eq(nil,cons(X,Y)) = bfalse ).

cnf(axiom_075,axiom,
    eq(cons(X,Y),nil) = bfalse ).

cnf(goal,negated_conjecture,
    eq4(prop_unambig(X,Y),bfalse) != btrue ).

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