TPTP Problem File: SWX240-1.p

View Solutions - Solve Problem 
%------------------------------------------------------------------------------
% File     : SWX240-1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Find a security leak in a faulty security type system (and no while loops in the language)
% Version  : Especial.
% English  :

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

% Status   : Unsatisfiable
% Rating   : 0.33 v9.3.0
% Syntax   : Number of clauses     :   88 (  79 unt;   0 nHn;  12 RR)
%            Number of literals    :   99 (  99 equ;  12 neg)
%            Maximal clause size   :    3 (   1 avg)
%            Maximal term depth    :    6 (   1 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   37 (  37 usr;   9 con; 0-5 aty)
%            Number of variables   :  190 ( 100 sgn)
% SPC      : CNF_UNS_RFO_PEQ_NUE

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    aux(X,Z,Ys,btrue) = del(X,Ys) ).

cnf(axiom_001,axiom,
    aux(X,Z,Ys,bfalse) = cons(Z,del(X,Ys)) ).

cnf(axiom_002,axiom,
    aux2(X,Z,E,btrue) = cons(Z,X) ).

cnf(axiom_003,axiom,
    aux2(X,Z,E,bfalse) = del(Z,X) ).

cnf(axiom_004,axiom,
    aux3(X,E2,R,Q2,btrue) = run(X,R) ).

cnf(axiom_005,axiom,
    aux3(X,E2,R,Q2,bfalse) = run(X,Q2) ).

cnf(axiom_006,axiom,
    orb(btrue,Q) = btrue ).

cnf(axiom_007,axiom,
    orb(bfalse,Q) = Q ).

cnf(axiom_008,axiom,
    secret(nand(A,B)) = orb(secret(A),secret(B)) ).

cnf(axiom_009,axiom,
    secret(var(high(Z))) = btrue ).

cnf(axiom_010,axiom,
    secret(var(low(X2))) = bfalse ).

cnf(axiom_011,axiom,
    secret(tT) = bfalse ).

cnf(axiom_012,axiom,
    secret(fF) = bfalse ).

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

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

cnf(axiom_015,axiom,
    l = low(zero) ).

cnf(axiom_016,axiom,
    impl(btrue,Q) = Q ).

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

cnf(axiom_018,axiom,
    h = high(zero) ).

cnf(axiom_019,axiom,
    elem(X,nil) = bfalse ).

cnf(axiom_020,axiom,
    elem(X,cons(Z,Xs)) = orb(eq2(Z,X),elem(X,Xs)) ).

cnf(axiom_021,axiom,
    del(X,nil) = nil ).

cnf(axiom_022,axiom,
    del(X,cons(Z,Ys)) = aux(X,Z,Ys,eq2(X,Z)) ).

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

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

cnf(axiom_025,axiom,
    eval(X,nand(A,B)) = notb(andb(eval(X,A),eval(X,B))) ).

cnf(axiom_026,axiom,
    eval(X,tT) = btrue ).

cnf(axiom_027,axiom,
    eval(X,fF) = bfalse ).

cnf(axiom_028,axiom,
    eval(X,var(Z)) = elem(Z,X) ).

cnf(axiom_029,axiom,
    run(X,skip) = X ).

cnf(axiom_030,axiom,
    run(X,assign(Z,E)) = aux2(X,Z,E,eval(X,E)) ).

cnf(axiom_031,axiom,
    run(X,seq(P,Q)) = run(run(X,P),Q) ).

cnf(axiom_032,axiom,
    run(X,ifThenElse(E2,R,Q2)) = aux3(X,E2,R,Q2,eval(X,E2)) ).

cnf(axiom_033,axiom,
    typeCorrect(skip) = btrue ).

cnf(axiom_034,axiom,
    typeCorrect(assign(high(Z),E)) = btrue ).

cnf(axiom_035,axiom,
    typeCorrect(assign(low(X2),E)) = notb(secret(E)) ).

cnf(axiom_036,axiom,
    typeCorrect(seq(P,Q)) = andb(typeCorrect(P),typeCorrect(Q)) ).

cnf(axiom_037,axiom,
    typeCorrect(ifThenElse(C,R,Q2)) = andb(typeCorrect(R),typeCorrect(Q2)) ).

cnf(axiom_038,axiom,
    prop(X,Y) = impl(typeCorrect(X),eq5(elem(l,run(Y,X)),elem(l,run(cons(h,Y),X)))) ).

cnf(axiom_039,axiom,
    eq3(tT,fF) = bfalse ).

cnf(axiom_040,axiom,
    eq3(fF,tT) = bfalse ).

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

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

cnf(axiom_043,axiom,
    ( eq3(X,Z) != bfalse
    | eq3(nand(X,Y),nand(Z,X2)) = bfalse ) ).

cnf(axiom_044,axiom,
    ( eq3(X,Z) != btrue
    | eq3(nand(X,Y),nand(Z,X2)) = eq3(Y,X2) ) ).

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

cnf(axiom_046,axiom,
    eq3(nand(X,Y),tT) = bfalse ).

cnf(axiom_047,axiom,
    eq3(nand(X,Y),fF) = bfalse ).

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

cnf(axiom_049,axiom,
    eq3(tT,nand(X,Y)) = bfalse ).

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

cnf(axiom_051,axiom,
    eq3(fF,nand(X,Y)) = bfalse ).

cnf(axiom_052,axiom,
    eq3(fF,var(X)) = bfalse ).

cnf(axiom_053,axiom,
    eq3(var(X),nand(Y,Z)) = bfalse ).

cnf(axiom_054,axiom,
    eq3(var(X),tT) = bfalse ).

cnf(axiom_055,axiom,
    eq3(var(X),fF) = bfalse ).

cnf(axiom_056,axiom,
    eq2(high(X),high(Y)) = eq(X,Y) ).

cnf(axiom_057,axiom,
    eq2(low(X),low(Y)) = eq(X,Y) ).

cnf(axiom_058,axiom,
    eq2(high(X),low(Y)) = bfalse ).

cnf(axiom_059,axiom,
    eq2(low(X),high(Y)) = bfalse ).

cnf(axiom_060,axiom,
    eq(suc(X),suc(Y)) = eq(X,Y) ).

cnf(axiom_061,axiom,
    eq(zero,suc(X)) = bfalse ).

cnf(axiom_062,axiom,
    eq(suc(X),zero) = bfalse ).

cnf(axiom_063,axiom,
    ( eq2(X,Z) != bfalse
    | eq4(assign(X,Y),assign(Z,X2)) = bfalse ) ).

cnf(axiom_064,axiom,
    ( eq2(X,Z) != btrue
    | eq4(assign(X,Y),assign(Z,X2)) = eq3(Y,X2) ) ).

cnf(axiom_065,axiom,
    ( eq4(X,Z) != bfalse
    | eq4(seq(X,Y),seq(Z,X2)) = bfalse ) ).

cnf(axiom_066,axiom,
    ( eq4(X,Z) != btrue
    | eq4(seq(X,Y),seq(Z,X2)) = eq4(Y,X2) ) ).

cnf(axiom_067,axiom,
    ( eq3(X,X2) != bfalse
    | eq4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4)) = bfalse ) ).

cnf(axiom_068,axiom,
    ( eq3(X,X2) != btrue
    | eq4(Y,X3) != bfalse
    | eq4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4)) = bfalse ) ).

cnf(axiom_069,axiom,
    ( eq3(X,X2) != btrue
    | eq4(Y,X3) != btrue
    | eq4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4)) = eq4(Z,X4) ) ).

cnf(axiom_070,axiom,
    eq4(skip,assign(X,Y)) = bfalse ).

cnf(axiom_071,axiom,
    eq4(skip,seq(X,Y)) = bfalse ).

cnf(axiom_072,axiom,
    eq4(skip,ifThenElse(X,Y,Z)) = bfalse ).

cnf(axiom_073,axiom,
    eq4(assign(X,Y),skip) = bfalse ).

cnf(axiom_074,axiom,
    eq4(assign(X,Y),seq(Z,X2)) = bfalse ).

cnf(axiom_075,axiom,
    eq4(assign(X,Y),ifThenElse(Z,X2,X3)) = bfalse ).

cnf(axiom_076,axiom,
    eq4(seq(X,Y),skip) = bfalse ).

cnf(axiom_077,axiom,
    eq4(seq(X,Y),assign(Z,X2)) = bfalse ).

cnf(axiom_078,axiom,
    eq4(seq(X,Y),ifThenElse(Z,X2,X3)) = bfalse ).

cnf(axiom_079,axiom,
    eq4(ifThenElse(X,Y,Z),skip) = bfalse ).

cnf(axiom_080,axiom,
    eq4(ifThenElse(X,Y,Z),assign(X2,X3)) = bfalse ).

cnf(axiom_081,axiom,
    eq4(ifThenElse(X,Y,Z),seq(X2,X3)) = bfalse ).

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

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

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

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

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

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

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