TPTP Problem File: SWX196+1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX196+1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : A buggy simplication function for expressions
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Expr_prop4.p [CST26]
% Status : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 69 ( 53 unt; 0 def)
% Number of atoms : 90 ( 90 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 52 ( 31 ~; 0 |; 0 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 32 ( 32 usr; 2 con; 0-2 aty)
% Number of variables : 140 ( 138 !; 2 ?)
% SPC : FOF_THM_RFO_PEQ
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_002,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_003,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_004,axiom,
! [X] : proj1Suc(suc(X)) = X ).
fof(axiom_005,axiom,
! [X] : zero != suc(X) ).
fof(axiom_006,axiom,
! [X] : proj1N(n(X)) = X ).
fof(axiom_007,axiom,
! [X,X2] : proj1Add(add(X,X2)) = X ).
fof(axiom_008,axiom,
! [X,X2] : proj2Add(add(X,X2)) = X2 ).
fof(axiom_009,axiom,
! [X,X2] : proj1Mul(mul(X,X2)) = X ).
fof(axiom_010,axiom,
! [X,X2] : proj2Mul(mul(X,X2)) = X2 ).
fof(axiom_011,axiom,
! [X,X2] : proj1Eq(eq(X,X2)) = X ).
fof(axiom_012,axiom,
! [X,X2] : proj2Eq(eq(X,X2)) = X2 ).
fof(axiom_013,axiom,
! [X] : proj1V(v(X)) = X ).
fof(axiom_014,axiom,
! [X,X2,X3] : n(X) != add(X2,X3) ).
fof(axiom_015,axiom,
! [X,X2,X3] : n(X) != mul(X2,X3) ).
fof(axiom_016,axiom,
! [X,X2,X3] : n(X) != eq(X2,X3) ).
fof(axiom_017,axiom,
! [X,X2] : n(X) != v(X2) ).
fof(axiom_018,axiom,
! [X,X2,X3,X4] : add(X,X2) != mul(X3,X4) ).
fof(axiom_019,axiom,
! [X,X2,X3,X4] : add(X,X2) != eq(X3,X4) ).
fof(axiom_020,axiom,
! [X,X2,X3] : add(X,X2) != v(X3) ).
fof(axiom_021,axiom,
! [X,X2,X3,X4] : mul(X,X2) != eq(X3,X4) ).
fof(axiom_022,axiom,
! [X,X2,X3] : mul(X,X2) != v(X3) ).
fof(axiom_023,axiom,
! [X,X2,X3] : eq(X,X2) != v(X3) ).
fof(axiom_024,axiom,
! [Y,B] :
( Y = B
=> fail1(Y,B) = mul(n(suc(suc(zero))),Y) ) ).
fof(axiom_025,axiom,
! [Y,B] :
( Y != B
=> ( Y != add(proj1Add(Y),proj2Add(Y))
=> fail1(Y,B) = add(Y,B) ) ) ).
fof(axiom_026,axiom,
! [B,A,B1] :
( add(A,B1) != B
=> fail1(add(A,B1),B) = add(A,add(B1,B)) ) ).
fof(axiom_027,axiom,
! [Y,B] :
( B != n(proj1N(B))
=> fail(Y,B) = fail1(Y,B) ) ).
fof(axiom_028,axiom,
! [Y] : fail(Y,n(zero)) = Y ).
fof(axiom_029,axiom,
! [Y,X2] : fail(Y,n(suc(X2))) = fail1(Y,n(suc(X2))) ).
fof(axiom_030,axiom,
! [X5,C] :
( X5 != mul(proj1Mul(X5),proj2Mul(X5))
=> fail3(X5,C) = mul(X5,C) ) ).
fof(axiom_031,axiom,
! [C,A2,B12] : fail3(mul(A2,B12),C) = mul(A2,mul(B12,C)) ).
fof(axiom_032,axiom,
! [X5,C] :
( C != n(proj1N(C))
=> fail22(X5,C) = fail3(X5,C) ) ).
fof(axiom_033,axiom,
! [X5] : fail22(X5,n(zero)) = fail3(X5,n(zero)) ).
fof(axiom_034,axiom,
! [X5] : fail22(X5,n(suc(zero))) = X5 ).
fof(axiom_035,axiom,
! [X5,X8] : fail22(X5,n(suc(suc(X8)))) = fail3(X5,n(suc(suc(X8)))) ).
fof(axiom_036,axiom,
! [X5,C] :
( X5 != n(proj1N(X5))
=> fail12(X5,C) = fail22(X5,C) ) ).
fof(axiom_037,axiom,
! [C] : fail12(n(zero),C) = fail22(n(zero),C) ).
fof(axiom_038,axiom,
! [C] : fail12(n(suc(zero)),C) = C ).
fof(axiom_039,axiom,
! [C,X11] : fail12(n(suc(suc(X11))),C) = fail22(n(suc(suc(X11))),C) ).
fof(axiom_040,axiom,
! [X5,C] :
( C != n(proj1N(C))
=> fail2(X5,C) = fail12(X5,C) ) ).
fof(axiom_041,axiom,
! [X5] : fail2(X5,n(zero)) = n(zero) ).
fof(axiom_042,axiom,
! [X5,X13] : fail2(X5,n(suc(X13))) = fail12(X5,n(suc(X13))) ).
fof(axiom_043,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> step4(X) = X ) ) ) ).
fof(axiom_044,axiom,
! [Y,B] :
( Y != n(proj1N(Y))
=> step4(add(Y,B)) = fail(Y,B) ) ).
fof(axiom_045,axiom,
! [B] : step4(add(n(zero),B)) = B ).
fof(axiom_046,axiom,
! [B,X4] : step4(add(n(suc(X4)),B)) = fail(n(suc(X4)),B) ).
fof(axiom_047,axiom,
! [X5,C] :
( X5 != n(proj1N(X5))
=> step4(mul(X5,C)) = fail2(X5,C) ) ).
fof(axiom_048,axiom,
! [C] : step4(mul(n(zero),C)) = n(zero) ).
fof(axiom_049,axiom,
! [C,X15] : step4(mul(n(suc(X15)),C)) = fail2(n(suc(X15)),C) ).
fof(axiom_050,axiom,
! [A3,B2] :
( A3 = B2
=> step4(eq(A3,B2)) = n(suc(zero)) ) ).
fof(axiom_051,axiom,
! [A3,B2] :
( A3 != B2
=> step4(eq(A3,B2)) = eq(A3,B2) ) ).
fof(axiom_052,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> simp4(X) = step4(X) ) ) ) ).
fof(axiom_053,axiom,
! [A,B] : simp4(add(A,B)) = step4(add(simp4(A),simp4(B))) ).
fof(axiom_054,axiom,
! [C,B2] : simp4(mul(C,B2)) = step4(mul(simp4(C),simp4(B2))) ).
fof(axiom_055,axiom,
! [A2,B3] : simp4(eq(A2,B3)) = step4(eq(simp4(A2),simp4(B3))) ).
fof(axiom_056,axiom,
! [Y] : fetch(nil,Y) = zero ).
fof(axiom_057,axiom,
! [N,St] : fetch(cons(N,St),zero) = N ).
fof(axiom_058,axiom,
! [N,St,Z] : fetch(cons(N,St),suc(Z)) = fetch(St,Z) ).
fof(axiom_059,axiom,
! [Y] : addNat(zero,Y) = Y ).
fof(axiom_060,axiom,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)) ).
fof(axiom_061,axiom,
! [Y] : mulNat(zero,Y) = zero ).
fof(axiom_062,axiom,
! [Y,Z] : mulNat(suc(Z),Y) = addNat(Y,mulNat(Z,Y)) ).
fof(axiom_063,axiom,
! [X,N] : eval(X,n(N)) = N ).
fof(axiom_064,axiom,
! [X,A,B] : eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)) ).
fof(axiom_065,axiom,
! [X,C,B2] : eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)) ).
fof(axiom_066,axiom,
! [X,A2,B3] :
( eval(X,A2) = eval(X,B3)
=> eval(X,eq(A2,B3)) = suc(zero) ) ).
fof(axiom_067,axiom,
! [X,A2,B3] :
( eval(X,A2) != eval(X,B3)
=> eval(X,eq(A2,B3)) = zero ) ).
fof(axiom_068,axiom,
! [X,Z] : eval(X,v(Z)) = fetch(X,Z) ).
fof(goal_069,conjecture,
? [St,A] : eval(St,A) != eval(St,simp4(A)) ).
%------------------------------------------------------------------------------