%------------------------------------------------------------------------------
% File     : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Show a specific given type is inhabited by a normal form
% Version  : Especial.
% English  :

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

% Status   : Unsatisfiable
% Rating   : 0.00 v9.3.0
% Syntax   : Number of clauses     :   56 (  51 unt;   0 nHn;  11 RR)
%            Number of literals    :   63 (  63 equ;   8 neg)
%            Maximal clause size   :    3 (   1 avg)
%            Maximal term depth    :    6 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   26 (  26 usr;   8 con; 0-4 aty)
%            Number of variables   :  118 (  64 sgn)
% SPC      : CNF_UNS_RFO_PEQ_NUE

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    aux(X,Z,X3,nothing) = bfalse ).

cnf(axiom_001,axiom,
    aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z) ).

cnf(axiom_002,axiom,
    notb(btrue) = bfalse ).

cnf(axiom_003,axiom,
    notb(bfalse) = btrue ).

cnf(axiom_004,axiom,
    index(nil,Y) = nothing ).

cnf(axiom_005,axiom,
    index(cons(Z,Xs),zero) = just(Z) ).

cnf(axiom_006,axiom,
    index(cons(Z,Xs),suc(N)) = index(Xs,N) ).

cnf(axiom_007,axiom,
    andb(btrue,Q) = Q ).

cnf(axiom_008,axiom,
    andb(bfalse,Q) = bfalse ).

cnf(axiom_009,axiom,
    nf(app(lam(X3),Z,X2)) = bfalse ).

cnf(axiom_010,axiom,
    nf(app(app(X,X3,X4),Z,X2)) = andb(nf(app(X,X3,X4)),nf(Z)) ).

cnf(axiom_011,axiom,
    nf(app(var(X),Z,X2)) = andb(nf(var(X)),nf(Z)) ).

cnf(axiom_012,axiom,
    nf(lam(E)) = nf(E) ).

cnf(axiom_013,axiom,
    nf(var(X4)) = btrue ).

cnf(axiom_014,axiom,
    tc(X,app(F,X2,Tx),Z) = andb(tc(X,F,arr(Tx,Z)),tc(X,X2,Tx)) ).

cnf(axiom_015,axiom,
    tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1) ).

cnf(axiom_016,axiom,
    tc(X,lam(E),a) = bfalse ).

cnf(axiom_017,axiom,
    tc(X,lam(E),b) = bfalse ).

cnf(axiom_018,axiom,
    tc(X,lam(E),c) = bfalse ).

cnf(axiom_019,axiom,
    tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)) ).

cnf(axiom_020,axiom,
    sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))) ).

cnf(axiom_021,axiom,
    eq(a,b) = bfalse ).

cnf(axiom_022,axiom,
    eq(a,c) = bfalse ).

cnf(axiom_023,axiom,
    eq(b,a) = bfalse ).

cnf(axiom_024,axiom,
    eq(b,c) = bfalse ).

cnf(axiom_025,axiom,
    eq(c,a) = bfalse ).

cnf(axiom_026,axiom,
    eq(c,b) = bfalse ).

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

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

cnf(axiom_029,axiom,
    eq2(suc(X),suc(Y)) = eq2(X,Y) ).

cnf(axiom_030,axiom,
    eq2(zero,suc(X)) = bfalse ).

cnf(axiom_031,axiom,
    eq2(suc(X),zero) = bfalse ).

cnf(axiom_032,axiom,
    ( eq(X,Z) != bfalse
    | eq(arr(X,Y),arr(Z,X2)) = bfalse ) ).

cnf(axiom_033,axiom,
    ( eq(X,Z) != btrue
    | eq(arr(X,Y),arr(Z,X2)) = eq(Y,X2) ) ).

cnf(axiom_034,axiom,
    eq(arr(X,Y),a) = bfalse ).

cnf(axiom_035,axiom,
    eq(arr(X,Y),b) = bfalse ).

cnf(axiom_036,axiom,
    eq(arr(X,Y),c) = bfalse ).

cnf(axiom_037,axiom,
    eq(a,arr(X,Y)) = bfalse ).

cnf(axiom_038,axiom,
    eq(b,arr(X,Y)) = bfalse ).

cnf(axiom_039,axiom,
    eq(c,arr(X,Y)) = bfalse ).

cnf(axiom_040,axiom,
    ( eq3(X,X2) != bfalse
    | eq3(app(X,Y,Z),app(X2,X3,X4)) = bfalse ) ).

cnf(axiom_041,axiom,
    ( eq3(Y,X3) != bfalse
    | eq3(X,X2) != btrue
    | eq3(app(X,Y,Z),app(X2,X3,X4)) = bfalse ) ).

cnf(axiom_042,axiom,
    ( eq3(X,X2) != btrue
    | eq3(Y,X3) != btrue
    | eq3(app(X,Y,Z),app(X2,X3,X4)) = eq(Z,X4) ) ).

cnf(axiom_043,axiom,
    eq3(lam(X),lam(Y)) = eq3(X,Y) ).

cnf(axiom_044,axiom,
    eq3(var(X),var(Y)) = eq2(X,Y) ).

cnf(axiom_045,axiom,
    eq3(app(X,Y,Z),lam(X2)) = bfalse ).

cnf(axiom_046,axiom,
    eq3(app(X,Y,Z),var(X2)) = bfalse ).

cnf(axiom_047,axiom,
    eq3(lam(X),app(Y,Z,X2)) = bfalse ).

cnf(axiom_048,axiom,
    eq3(lam(X),var(Y)) = bfalse ).

cnf(axiom_049,axiom,
    eq3(var(X),app(Y,Z,X2)) = bfalse ).

cnf(axiom_050,axiom,
    eq3(var(X),lam(Y)) = bfalse ).

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

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

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

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

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

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