%------------------------------------------------------------------------------
% 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   : Unsatisfiable
% Rating   : 0.08 v9.3.0
% Syntax   : Number of clauses     :   49 (  45 unt;   0 nHn;  14 RR)
%            Number of literals    :   53 (  53 equ;   5 neg)
%            Maximal clause size   :    2 (   1 avg)
%            Maximal term depth    :    4 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   22 (  22 usr;   8 con; 0-2 aty)
%            Number of variables   :   59 (  27 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,
    append(nil,Y) = Y ).

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

cnf(axiom_004,axiom,
    linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil))) ).

cnf(axiom_005,axiom,
    linP(bP(Q)) = append(cons(b,nil),append(linP(Q),cons(b,nil))) ).

cnf(axiom_006,axiom,
    linP(pA) = cons(a,nil) ).

cnf(axiom_007,axiom,
    linP(pB) = cons(b,nil) ).

cnf(axiom_008,axiom,
    linP(pE) = nil ).

cnf(axiom_009,axiom,
    linC(c2(P,Q)) = append(linP(P),linP(Q)) ).

cnf(axiom_010,axiom,
    unambig(X,Y) = impl(eq(linC(X),linC(Y)),eq4(X,Y)) ).

cnf(axiom_011,axiom,
    eq2(a,b) = bfalse ).

cnf(axiom_012,axiom,
    eq2(b,a) = bfalse ).

cnf(axiom_013,axiom,
    eq3(pA,pB) = bfalse ).

cnf(axiom_014,axiom,
    eq3(pA,pE) = bfalse ).

cnf(axiom_015,axiom,
    eq3(pB,pA) = bfalse ).

cnf(axiom_016,axiom,
    eq3(pB,pE) = bfalse ).

cnf(axiom_017,axiom,
    eq3(pE,pA) = bfalse ).

cnf(axiom_018,axiom,
    eq3(pE,pB) = bfalse ).

cnf(axiom_019,axiom,
    eq5(bfalse,btrue) = bfalse ).

cnf(axiom_020,axiom,
    eq5(btrue,bfalse) = bfalse ).

cnf(axiom_021,axiom,
    eq3(aP(X),aP(Y)) = eq3(X,Y) ).

cnf(axiom_022,axiom,
    eq3(bP(X),bP(Y)) = eq3(X,Y) ).

cnf(axiom_023,axiom,
    eq3(aP(X),bP(Y)) = bfalse ).

cnf(axiom_024,axiom,
    eq3(aP(X),pA) = bfalse ).

cnf(axiom_025,axiom,
    eq3(aP(X),pB) = bfalse ).

cnf(axiom_026,axiom,
    eq3(aP(X),pE) = bfalse ).

cnf(axiom_027,axiom,
    eq3(bP(X),aP(Y)) = bfalse ).

cnf(axiom_028,axiom,
    eq3(bP(X),pA) = bfalse ).

cnf(axiom_029,axiom,
    eq3(bP(X),pB) = bfalse ).

cnf(axiom_030,axiom,
    eq3(bP(X),pE) = bfalse ).

cnf(axiom_031,axiom,
    eq3(pA,aP(X)) = bfalse ).

cnf(axiom_032,axiom,
    eq3(pA,bP(X)) = bfalse ).

cnf(axiom_033,axiom,
    eq3(pB,aP(X)) = bfalse ).

cnf(axiom_034,axiom,
    eq3(pB,bP(X)) = bfalse ).

cnf(axiom_035,axiom,
    eq3(pE,aP(X)) = bfalse ).

cnf(axiom_036,axiom,
    eq3(pE,bP(X)) = bfalse ).

cnf(axiom_037,axiom,
    ( eq3(X,Z) != bfalse
    | eq4(c2(X,Y),c2(Z,X2)) = bfalse ) ).

cnf(axiom_038,axiom,
    ( eq3(X,Z) != btrue
    | eq4(c2(X,Y),c2(Z,X2)) = eq3(Y,X2) ) ).

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

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

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

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

cnf(axiom_043,axiom,
    eq5(X,X) = btrue ).

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

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

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

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

cnf(goal,negated_conjecture,
    eq5(unambig(X,Y),bfalse) != btrue ).

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