TPTP Problem File: SWX194+1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX194+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_prop1.p [CST26]
% Status : Theorem
% Rating : 0.75 v9.3.0
% Syntax : Number of formulae : 72 ( 53 unt; 0 def)
% Number of atoms : 100 ( 100 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 65 ( 37 ~; 0 |; 0 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 146 ( 144 !; 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))
=> ( Y != v(proj1V(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,
! [B,Z] :
( v(Z) != B
=> ( B != v(proj1V(B))
=> fail1(v(Z),B) = add(v(Z),B) ) ) ).
fof(axiom_028,axiom,
! [Z,Y2] :
( Z != Y2
=> ( Z = Z
=> fail1(v(Z),v(Y2)) = mul(n(suc(suc(zero))),v(Z)) ) ) ).
fof(axiom_029,axiom,
! [Z,Y2] :
( Z != Y2
=> ( Z != Z
=> fail1(v(Z),v(Y2)) = add(v(Z),v(Y2)) ) ) ).
fof(axiom_030,axiom,
! [Y,B] :
( B != n(proj1N(B))
=> fail(Y,B) = fail1(Y,B) ) ).
fof(axiom_031,axiom,
! [Y] : fail(Y,n(zero)) = Y ).
fof(axiom_032,axiom,
! [Y,X3] : fail(Y,n(suc(X3))) = fail1(Y,n(suc(X3))) ).
fof(axiom_033,axiom,
! [X6,C] :
( X6 != mul(proj1Mul(X6),proj2Mul(X6))
=> fail3(X6,C) = mul(X6,C) ) ).
fof(axiom_034,axiom,
! [C,A2,B12] : fail3(mul(A2,B12),C) = mul(A2,mul(B12,C)) ).
fof(axiom_035,axiom,
! [X6,C] :
( C != n(proj1N(C))
=> fail22(X6,C) = fail3(X6,C) ) ).
fof(axiom_036,axiom,
! [X6] : fail22(X6,n(zero)) = fail3(X6,n(zero)) ).
fof(axiom_037,axiom,
! [X6] : fail22(X6,n(suc(zero))) = X6 ).
fof(axiom_038,axiom,
! [X6,X9] : fail22(X6,n(suc(suc(X9)))) = fail3(X6,n(suc(suc(X9)))) ).
fof(axiom_039,axiom,
! [X6,C] :
( X6 != n(proj1N(X6))
=> fail12(X6,C) = fail22(X6,C) ) ).
fof(axiom_040,axiom,
! [C] : fail12(n(zero),C) = fail22(n(zero),C) ).
fof(axiom_041,axiom,
! [C] : fail12(n(suc(zero)),C) = C ).
fof(axiom_042,axiom,
! [C,X12] : fail12(n(suc(suc(X12))),C) = fail22(n(suc(suc(X12))),C) ).
fof(axiom_043,axiom,
! [X6,C] :
( C != n(proj1N(C))
=> fail2(X6,C) = fail12(X6,C) ) ).
fof(axiom_044,axiom,
! [X6] : fail2(X6,n(zero)) = n(zero) ).
fof(axiom_045,axiom,
! [X6,X14] : fail2(X6,n(suc(X14))) = fail12(X6,n(suc(X14))) ).
fof(axiom_046,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> step1(X) = X ) ) ) ).
fof(axiom_047,axiom,
! [Y,B] :
( Y != n(proj1N(Y))
=> step1(add(Y,B)) = fail(Y,B) ) ).
fof(axiom_048,axiom,
! [B] : step1(add(n(zero),B)) = B ).
fof(axiom_049,axiom,
! [B,X5] : step1(add(n(suc(X5)),B)) = fail(n(suc(X5)),B) ).
fof(axiom_050,axiom,
! [X6,C] :
( X6 != n(proj1N(X6))
=> step1(mul(X6,C)) = fail2(X6,C) ) ).
fof(axiom_051,axiom,
! [C] : step1(mul(n(zero),C)) = n(zero) ).
fof(axiom_052,axiom,
! [C,X16] : step1(mul(n(suc(X16)),C)) = fail2(n(suc(X16)),C) ).
fof(axiom_053,axiom,
! [A3,B2] :
( A3 = B2
=> step1(eq(A3,B2)) = n(suc(zero)) ) ).
fof(axiom_054,axiom,
! [A3,B2] :
( A3 != B2
=> step1(eq(A3,B2)) = eq(A3,B2) ) ).
fof(axiom_055,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> simp1(X) = step1(X) ) ) ) ).
fof(axiom_056,axiom,
! [A,B] : simp1(add(A,B)) = step1(add(simp1(A),simp1(B))) ).
fof(axiom_057,axiom,
! [C,B2] : simp1(mul(C,B2)) = step1(mul(simp1(C),simp1(B2))) ).
fof(axiom_058,axiom,
! [A2,B3] : simp1(eq(A2,B3)) = step1(eq(simp1(A2),simp1(B3))) ).
fof(axiom_059,axiom,
! [Y] : fetch(nil,Y) = zero ).
fof(axiom_060,axiom,
! [N,St] : fetch(cons(N,St),zero) = N ).
fof(axiom_061,axiom,
! [N,St,Z] : fetch(cons(N,St),suc(Z)) = fetch(St,Z) ).
fof(axiom_062,axiom,
! [Y] : addNat(zero,Y) = Y ).
fof(axiom_063,axiom,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)) ).
fof(axiom_064,axiom,
! [Y] : mulNat(zero,Y) = zero ).
fof(axiom_065,axiom,
! [Y,Z] : mulNat(suc(Z),Y) = addNat(Y,mulNat(Z,Y)) ).
fof(axiom_066,axiom,
! [X,N] : eval(X,n(N)) = N ).
fof(axiom_067,axiom,
! [X,A,B] : eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)) ).
fof(axiom_068,axiom,
! [X,C,B2] : eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)) ).
fof(axiom_069,axiom,
! [X,A2,B3] :
( eval(X,A2) = eval(X,B3)
=> eval(X,eq(A2,B3)) = suc(zero) ) ).
fof(axiom_070,axiom,
! [X,A2,B3] :
( eval(X,A2) != eval(X,B3)
=> eval(X,eq(A2,B3)) = zero ) ).
fof(axiom_071,axiom,
! [X,Z] : eval(X,v(Z)) = fetch(X,Z) ).
fof(goal_072,conjecture,
? [St,A] : eval(St,A) != eval(St,simp1(A)) ).
%------------------------------------------------------------------------------