TPTP Problem File: SWX242-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX242-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find a bug in a faulty unification function
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Unify_prop_unify_makes_equal.p [CST26]
% Status : Unsatisfiable
% Rating : 0.50 v9.3.0
% Syntax : Number of clauses : 73 ( 69 unt; 0 nHn; 10 RR)
% Number of literals : 77 ( 77 equ; 5 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 44 ( 44 usr; 8 con; 0-8 aty)
% Number of variables : 208 ( 57 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(X,Y,Z,btrue) = Y ).
cnf(axiom_001,axiom,
aux(X,Y,Z,bfalse) = var(Z) ).
cnf(axiom_002,axiom,
aux2(X,Y,Z,X2,btrue) = Y ).
cnf(axiom_003,axiom,
aux2(X,Y,Z,X2,bfalse) = apply1(Z,X2) ).
cnf(axiom_004,axiom,
aux3(X,Ts,F,Ts2,Us,G,Vs,btrue) = unifyloop(X,append(Ts2,Ts),append(Vs,Us)) ).
cnf(axiom_005,axiom,
aux3(X,Ts,F,Ts2,Us,G,Vs,bfalse) = fail(X,cons(app(G,Vs),Us),app(F,Ts2),Ts) ).
cnf(axiom_006,axiom,
aux4(X,Y,X2,X3,X4,X5,btrue) = nothing ).
cnf(axiom_007,axiom,
aux4(X,Y,X2,X3,X4,X5,bfalse) = unifybind(X,Y,app(X4,X5),X2,X3) ).
cnf(axiom_008,axiom,
aux5(X,Y,X2,X3,Y2,btrue) = unifyloop(X,X2,X3) ).
cnf(axiom_009,axiom,
aux5(X,Y,X2,X3,Y2,bfalse) = unifybind(X,Y,var(Y2),X2,X3) ).
cnf(axiom_010,axiom,
aux6(X,Y,nothing) = btrue ).
cnf(axiom_011,axiom,
aux6(X,Y,just(Sub)) = eq3(subst(Sub,X),subst(Sub,Y)) ).
cnf(axiom_012,axiom,
aux7(X,Y,Z,Y2,btrue) = Z ).
cnf(axiom_013,axiom,
aux7(X,Y,Z,Y2,bfalse) = subst(lam(Y,Z),apply1(X,Y2)) ).
cnf(axiom_014,axiom,
fail(X,nil,X4,Ts) = nothing ).
cnf(axiom_015,axiom,
fail(X,cons(app(X6,X7),Us),X4,Ts) = nothing ).
cnf(axiom_016,axiom,
fail(X,cons(var(X8),Us),X4,Ts) = unifyvar(X,X8,X4,Ts,Us) ).
cnf(axiom_017,axiom,
sub(X,Y,Z) = lam2(X,Y,Z) ).
cnf(axiom_018,axiom,
subst(X,app(F,Xs)) = app(F,substList(X,Xs)) ).
cnf(axiom_019,axiom,
subst(X,var(Z)) = apply1(X,Z) ).
cnf(axiom_020,axiom,
substList(Sub,nil) = nil ).
cnf(axiom_021,axiom,
substList(Sub,cons(Y,Xs)) = cons(subst(Sub,Y),substList(Sub,Xs)) ).
cnf(axiom_022,axiom,
substSubst(X,Y,Z) = subst(X,apply1(Y,Z)) ).
cnf(axiom_023,axiom,
singleton(X,Y,Z) = aux(X,Y,Z,eq2(X,Z)) ).
cnf(axiom_024,axiom,
orb(btrue,Q) = btrue ).
cnf(axiom_025,axiom,
orb(bfalse,Q) = Q ).
cnf(axiom_026,axiom,
unify(X,nil) = bfalse ).
cnf(axiom_027,axiom,
unify(X,cons(Z,Xs)) = orb(unifyoccurs(X,Z),unify(X,Xs)) ).
cnf(axiom_028,axiom,
unifyoccurs(X,app(Z,Ts)) = unify(X,Ts) ).
cnf(axiom_029,axiom,
unifyoccurs(X,var(Y2)) = eq2(X,Y2) ).
cnf(axiom_030,axiom,
extend(X,Y,Z,X2) = aux2(X,Y,Z,X2,eq2(X,X2)) ).
cnf(axiom_031,axiom,
unifyloop(X,nil,nil) = just(X) ).
cnf(axiom_032,axiom,
unifyloop(X,nil,cons(X2,X3)) = nothing ).
cnf(axiom_033,axiom,
unifyloop(X,cons(app(F,Ts2),Ts),nil) = fail(X,nil,app(F,Ts2),Ts) ).
cnf(axiom_034,axiom,
unifyloop(X,cons(app(F,Ts2),Ts),cons(app(G,Vs),Us)) = aux3(X,Ts,F,Ts2,Us,G,Vs,eq2(F,G)) ).
cnf(axiom_035,axiom,
unifyloop(X,cons(app(F,Ts2),Ts),cons(var(X10),Us)) = fail(X,cons(var(X10),Us),app(F,Ts2),Ts) ).
cnf(axiom_036,axiom,
unifyloop(X,cons(var(X11),Ts),nil) = fail(X,nil,var(X11),Ts) ).
cnf(axiom_037,axiom,
unifyloop(X,cons(var(X11),Ts),cons(U1,Ws)) = unifyvar(X,X11,U1,Ts,Ws) ).
cnf(axiom_038,axiom,
unifyvar(X,Y,app(X4,X5),X2,X3) = aux4(X,Y,X2,X3,X4,X5,unifyoccurs(Y,app(X4,X5))) ).
cnf(axiom_039,axiom,
unifyvar(X,Y,var(Y2),X2,X3) = aux5(X,Y,X2,X3,Y2,eq2(Y,Y2)) ).
cnf(axiom_040,axiom,
unifybind(X,Y,Z,X2,X3) = unifyloop(sub(X,Y,Z),substList(sub(X,Y,Z),X2),substList(sub(X,Y,Z),X3)) ).
cnf(axiom_041,axiom,
unify2(X,Y) = unifyloop(lam3,cons(X,nil),cons(Y,nil)) ).
cnf(axiom_042,axiom,
unificationOK(X,Y) = aux6(X,Y,unify2(X,Y)) ).
cnf(axiom_043,axiom,
prop_unify_makes_equal(X,Y) = eq4(unificationOK(X,Y),btrue) ).
cnf(axiom_044,axiom,
isJust2(nothing) = bfalse ).
cnf(axiom_045,axiom,
isJust2(just(Y)) = btrue ).
cnf(axiom_046,axiom,
append(nil,Y) = Y ).
cnf(axiom_047,axiom,
append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
cnf(axiom_048,axiom,
eq2(a,b) = bfalse ).
cnf(axiom_049,axiom,
eq2(a,c) = bfalse ).
cnf(axiom_050,axiom,
eq2(b,a) = bfalse ).
cnf(axiom_051,axiom,
eq2(b,c) = bfalse ).
cnf(axiom_052,axiom,
eq2(c,a) = bfalse ).
cnf(axiom_053,axiom,
eq2(c,b) = bfalse ).
cnf(axiom_054,axiom,
eq4(bfalse,btrue) = bfalse ).
cnf(axiom_055,axiom,
eq4(btrue,bfalse) = bfalse ).
cnf(axiom_056,axiom,
eq2(X,X) = btrue ).
cnf(axiom_057,axiom,
eq3(X,X) = btrue ).
cnf(axiom_058,axiom,
eq4(X,X) = btrue ).
cnf(axiom_059,axiom,
eq(X,X) = btrue ).
cnf(axiom_060,axiom,
( eq3(X,Z) != bfalse
| eq(cons(X,Y),cons(Z,X2)) = bfalse ) ).
cnf(axiom_061,axiom,
( eq3(X,Z) != btrue
| eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ).
cnf(axiom_062,axiom,
eq(nil,cons(X,Y)) = bfalse ).
cnf(axiom_063,axiom,
eq(cons(X,Y),nil) = bfalse ).
cnf(axiom_064,axiom,
( eq2(X,Z) != bfalse
| eq3(app(X,Y),app(Z,X2)) = bfalse ) ).
cnf(axiom_065,axiom,
( eq2(X,Z) != btrue
| eq3(app(X,Y),app(Z,X2)) = eq(Y,X2) ) ).
cnf(axiom_066,axiom,
eq3(var(X),var(Y)) = eq2(X,Y) ).
cnf(axiom_067,axiom,
eq3(app(X,Y),var(Z)) = bfalse ).
cnf(axiom_068,axiom,
eq3(var(X),app(Y,Z)) = bfalse ).
cnf(axiom_069,axiom,
apply1(lam2(X,Y,Z),Y2) = aux7(X,Y,Z,Y2,eq2(Y,Y2)) ).
cnf(axiom_070,axiom,
apply1(lam(Y,Z),X4) = singleton(Y,Z,X4) ).
cnf(axiom_071,axiom,
apply1(lam3,Z) = var(Z) ).
cnf(goal,negated_conjecture,
eq4(prop_unify_makes_equal(X,Y),bfalse) != btrue ).
%------------------------------------------------------------------------------