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 : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 88 ( 38 unt; 35 typ; 0 def)
% Number of atoms : 71 ( 57 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 31 ( 14 ~; 1 |; 0 &)
% ( 4 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of X terms : 1 ( 0 []; 1 ite; 0 let)
% Number of types : 2 ( 0 usr)
% Number of type conns : 64 ( 29 >; 35 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty)
% Number of functors : 31 ( 31 usr; 6 con; 0-5 aty)
% Number of variables : 153 ( 151 !; 2 ?; 153 :)
% SPC : TX0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
tff(lam_type,type,
lam: ( $i * $i ) > $i ).
tff(fail_type,type,
fail: ( $i * $i * $i * $i ) > $i ).
tff(proj2App_type,type,
proj2App: $i > $i ).
tff(apply1_type,type,
apply1: ( $i * $i ) > $i ).
tff(isJust2_type,type,
isJust2: $i > $o ).
tff(just_type,type,
just: $i > $i ).
tff(unify2_type,type,
unify2: ( $i * $i ) > $i ).
tff(unifyoccurs_type,type,
unifyoccurs: ( $i * $i ) > $o ).
tff(lam2_type,type,
lam2: ( $i * $i * $i ) > $i ).
tff(c_type,type,
c: $i ).
tff(proj1Just_type,type,
proj1Just: $i > $i ).
tff(var_type,type,
var: $i > $i ).
tff(proj1App_type,type,
proj1App: $i > $i ).
tff(head_type,type,
head: $i > $i ).
tff(a_type,type,
a: $i ).
tff(cons_type,type,
cons: ( $i * $i ) > $i ).
tff(subst_type,type,
subst: ( $i * $i ) > $i ).
tff(tail_type,type,
tail: $i > $i ).
tff(substList_type,type,
substList: ( $i * $i ) > $i ).
tff(extend_type,type,
extend: ( $i * $i * $i * $i ) > $i ).
tff(nil_type,type,
nil: $i ).
tff(substSubst_type,type,
substSubst: ( $i * $i * $i ) > $i ).
tff(nothing_type,type,
nothing: $i ).
tff(unifybind_type,type,
unifybind: ( $i * $i * $i * $i * $i ) > $i ).
tff(proj1Var_type,type,
proj1Var: $i > $i ).
tff(b_type,type,
b: $i ).
tff(unifyvar_type,type,
unifyvar: ( $i * $i * $i * $i * $i ) > $i ).
tff(app_type,type,
app: ( $i * $i ) > $i ).
tff(sub_type,type,
sub: ( $i * $i * $i ) > $i ).
tff(singleton_type,type,
singleton: ( $i * $i * $i ) > $i ).
tff(unificationOK_type,type,
unificationOK: ( $i * $i ) > $o ).
tff(lam3_type,type,
lam3: $i ).
tff(unifyloop_type,type,
unifyloop: ( $i * $i * $i ) > $i ).
tff(unify_type,type,
unify: ( $i * $i ) > $o ).
tff(append_type,type,
append: ( $i * $i ) > $i ).
tff(axiom_001,axiom,
a != b ).
tff(axiom_002,axiom,
a != c ).
tff(axiom_003,axiom,
b != c ).
tff(axiom_004,axiom,
! [X: $i,X2: $i] : ( proj1App(app(X,X2)) = X ) ).
tff(axiom_005,axiom,
! [X: $i,X2: $i] : ( proj2App(app(X,X2)) = X2 ) ).
tff(axiom_006,axiom,
! [X: $i] : ( proj1Var(var(X)) = X ) ).
tff(axiom_007,axiom,
! [X: $i,X2: $i,X3: $i] : ( app(X,X2) != var(X3) ) ).
tff(axiom_008,axiom,
! [X: $i,X2: $i] : ( head(cons(X,X2)) = X ) ).
tff(axiom_009,axiom,
! [X: $i,X2: $i] : ( tail(cons(X,X2)) = X2 ) ).
tff(axiom_010,axiom,
! [X: $i,X2: $i] : ( nil != cons(X,X2) ) ).
tff(axiom_011,axiom,
! [X: $i] : ( proj1Just(just(X)) = X ) ).
tff(axiom_012,axiom,
! [X: $i] : ( nothing != just(X) ) ).
tff(axiom_013,axiom,
! [X: $i,X4: $i,Ts: $i] : ( fail(X,nil,X4,Ts) = nothing ) ).
tff(axiom_014,axiom,
! [X: $i,X4: $i,Ts: $i,Us: $i,X6: $i,X7: $i] : ( fail(X,cons(app(X6,X7),Us),X4,Ts) = nothing ) ).
tff(axiom_015,axiom,
! [X: $i,X4: $i,Ts: $i,Us: $i,X8: $i] : ( fail(X,cons(var(X8),Us),X4,Ts) = unifyvar(X,X8,X4,Ts,Us) ) ).
tff(axiom_016,axiom,
! [X: $i,Y: $i,Z: $i] : ( sub(X,Y,Z) = lam2(X,Y,Z) ) ).
tff(axiom_017,axiom,
! [X: $i] : ~ unify(X,nil) ).
tff(axiom_018,axiom,
! [X: $i,Z: $i,Xs: $i] :
( unify(X,cons(Z,Xs))
<=> ( unifyoccurs(X,Z)
| unify(X,Xs) ) ) ).
tff(axiom_019,axiom,
! [X: $i,Z: $i,Ts: $i] :
( unifyoccurs(X,app(Z,Ts))
<=> unify(X,Ts) ) ).
tff(axiom_020,axiom,
! [X: $i,Y2: $i] :
( unifyoccurs(X,var(Y2))
<=> ( X = Y2 ) ) ).
tff(axiom_021,axiom,
! [X: $i,F: $i,Xs: $i] : ( subst(X,app(F,Xs)) = app(F,substList(X,Xs)) ) ).
tff(axiom_022,axiom,
! [X: $i,Z: $i] : ( subst(X,var(Z)) = apply1(X,Z) ) ).
tff(axiom_023,axiom,
! [Sub: $i] : ( substList(Sub,nil) = nil ) ).
tff(axiom_024,axiom,
! [Sub: $i,Y: $i,Xs: $i] : ( substList(Sub,cons(Y,Xs)) = cons(subst(Sub,Y),substList(Sub,Xs)) ) ).
tff(axiom_025,axiom,
! [X: $i,Y: $i,Z: $i] : ( substSubst(X,Y,Z) = subst(X,apply1(Y,Z)) ) ).
tff(axiom_026,axiom,
! [X: $i,Y: $i,Z: $i] :
( ( X = Z )
=> ( singleton(X,Y,Z) = Y ) ) ).
tff(axiom_027,axiom,
! [X: $i,Y: $i,Z: $i] :
( ( X != Z )
=> ( singleton(X,Y,Z) = var(Z) ) ) ).
tff(axiom_028,axiom,
! [X: $i,Y: $i,Z: $i,X2: $i] :
( ( X = X2 )
=> ( extend(X,Y,Z,X2) = Y ) ) ).
tff(axiom_029,axiom,
! [X: $i,Y: $i,Z: $i,X2: $i] :
( ( X != X2 )
=> ( extend(X,Y,Z,X2) = apply1(Z,X2) ) ) ).
tff(axiom_030,axiom,
! [X: $i] : ( unifyloop(X,nil,nil) = just(X) ) ).
tff(axiom_031,axiom,
! [X: $i,X2: $i,X3: $i] : ( unifyloop(X,nil,cons(X2,X3)) = nothing ) ).
tff(axiom_032,axiom,
! [X: $i,Ts: $i,F: $i,Ts2: $i] : ( unifyloop(X,cons(app(F,Ts2),Ts),nil) = fail(X,nil,app(F,Ts2),Ts) ) ).
tff(axiom_033,axiom,
! [X: $i,Ts: $i,F: $i,Ts2: $i,Us: $i,G: $i,Vs: $i] :
( ( F = G )
=> ( unifyloop(X,cons(app(F,Ts2),Ts),cons(app(G,Vs),Us)) = unifyloop(X,append(Ts2,Ts),append(Vs,Us)) ) ) ).
tff(axiom_034,axiom,
! [X: $i,Ts: $i,F: $i,Ts2: $i,Us: $i,G: $i,Vs: $i] :
( ( F != G )
=> ( unifyloop(X,cons(app(F,Ts2),Ts),cons(app(G,Vs),Us)) = fail(X,cons(app(G,Vs),Us),app(F,Ts2),Ts) ) ) ).
tff(axiom_035,axiom,
! [X: $i,Ts: $i,F: $i,Ts2: $i,Us: $i,X10: $i] : ( unifyloop(X,cons(app(F,Ts2),Ts),cons(var(X10),Us)) = fail(X,cons(var(X10),Us),app(F,Ts2),Ts) ) ).
tff(axiom_036,axiom,
! [X: $i,Ts: $i,X11: $i] : ( unifyloop(X,cons(var(X11),Ts),nil) = fail(X,nil,var(X11),Ts) ) ).
tff(axiom_037,axiom,
! [X: $i,Ts: $i,X11: $i,U1: $i,Ws: $i] : ( unifyloop(X,cons(var(X11),Ts),cons(U1,Ws)) = unifyvar(X,X11,U1,Ts,Ws) ) ).
tff(axiom_038,axiom,
! [X: $i,Y: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( unifyoccurs(Y,app(X4,X5))
=> ( unifyvar(X,Y,app(X4,X5),X2,X3) = nothing ) ) ).
tff(axiom_039,axiom,
! [X: $i,Y: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ unifyoccurs(Y,app(X4,X5))
=> ( unifyvar(X,Y,app(X4,X5),X2,X3) = unifybind(X,Y,app(X4,X5),X2,X3) ) ) ).
tff(axiom_040,axiom,
! [X: $i,Y: $i,X2: $i,X3: $i,Y2: $i] :
( ( Y = Y2 )
=> ( unifyvar(X,Y,var(Y2),X2,X3) = unifyloop(X,X2,X3) ) ) ).
tff(axiom_041,axiom,
! [X: $i,Y: $i,X2: $i,X3: $i,Y2: $i] :
( ( Y != Y2 )
=> ( unifyvar(X,Y,var(Y2),X2,X3) = unifybind(X,Y,var(Y2),X2,X3) ) ) ).
tff(axiom_042,axiom,
! [X: $i,Y: $i,Z: $i,X2: $i,X3: $i] : ( unifybind(X,Y,Z,X2,X3) = unifyloop(sub(X,Y,Z),substList(sub(X,Y,Z),X2),substList(sub(X,Y,Z),X3)) ) ).
tff(axiom_043,axiom,
! [X: $i,Y: $i] : ( unify2(X,Y) = unifyloop(lam3,cons(X,nil),cons(Y,nil)) ) ).
tff(axiom_044,axiom,
! [X: $i,Y: $i] :
( ( unify2(X,Y) = nothing )
=> unificationOK(X,Y) ) ).
tff(axiom_045,axiom,
! [X: $i,Y: $i,Sub: $i] :
( ( unify2(X,Y) = just(Sub) )
=> ( unificationOK(X,Y)
<=> ( subst(Sub,X) = subst(Sub,Y) ) ) ) ).
tff(axiom_046,axiom,
~ isJust2(nothing) ).
tff(axiom_047,axiom,
! [Y: $i] : isJust2(just(Y)) ).
tff(axiom_048,axiom,
! [Y: $i] : ( append(nil,Y) = Y ) ).
tff(axiom_049,axiom,
! [Y: $i,Z: $i,Xs: $i] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ) ).
tff(axiom_050,axiom,
! [X: $i,Y: $i,Z: $i,Y2: $i] :
( apply1(lam2(X,Y,Z),Y2) = $ite(Y = Y2,Z,subst(lam(Y,Z),apply1(X,Y2))) ) ).
tff(axiom_051,axiom,
! [Y: $i,Z: $i,X4: $i] : ( apply1(lam(Y,Z),X4) = singleton(Y,Z,X4) ) ).
tff(axiom_052,axiom,
! [Z: $i] : ( apply1(lam3,Z) = var(Z) ) ).
tff(goal_053,conjecture,
? [T1: $i,T2: $i] : ~ unificationOK(T1,T2) ).
%------------------------------------------------------------------------------