TPTP Problem File: SWX197+1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX197+1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : A buggy compiler for a simple imperative language
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Imp_prop_Opti2.p [CST26]
% Status : Theorem
% Rating : 0.50 v9.3.0
% Syntax : Number of formulae : 74 ( 69 unt; 0 def)
% Number of atoms : 80 ( 80 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 29 ( 23 ~; 0 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 47 ( 47 usr; 4 con; 0-3 aty)
% Number of variables : 181 ( 180 !; 1 ?)
% SPC : FOF_THM_RFO_PEQ
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X] : proj1Suc(suc(X)) = X ).
fof(axiom_002,axiom,
! [X] : zero != suc(X) ).
fof(axiom_003,axiom,
! [X] : proj1N(n(X)) = X ).
fof(axiom_004,axiom,
! [X,X2] : proj1Add(add(X,X2)) = X ).
fof(axiom_005,axiom,
! [X,X2] : proj2Add(add(X,X2)) = X2 ).
fof(axiom_006,axiom,
! [X,X2] : proj1Mul(mul(X,X2)) = X ).
fof(axiom_007,axiom,
! [X,X2] : proj2Mul(mul(X,X2)) = X2 ).
fof(axiom_008,axiom,
! [X,X2] : proj1Eq(eq(X,X2)) = X ).
fof(axiom_009,axiom,
! [X,X2] : proj2Eq(eq(X,X2)) = X2 ).
fof(axiom_010,axiom,
! [X] : proj1V(v(X)) = X ).
fof(axiom_011,axiom,
! [X,X2,X3] : n(X) != add(X2,X3) ).
fof(axiom_012,axiom,
! [X,X2,X3] : n(X) != mul(X2,X3) ).
fof(axiom_013,axiom,
! [X,X2,X3] : n(X) != eq(X2,X3) ).
fof(axiom_014,axiom,
! [X,X2] : n(X) != v(X2) ).
fof(axiom_015,axiom,
! [X,X2,X3,X4] : add(X,X2) != mul(X3,X4) ).
fof(axiom_016,axiom,
! [X,X2,X3,X4] : add(X,X2) != eq(X3,X4) ).
fof(axiom_017,axiom,
! [X,X2,X3] : add(X,X2) != v(X3) ).
fof(axiom_018,axiom,
! [X,X2,X3,X4] : mul(X,X2) != eq(X3,X4) ).
fof(axiom_019,axiom,
! [X,X2,X3] : mul(X,X2) != v(X3) ).
fof(axiom_020,axiom,
! [X,X2,X3] : eq(X,X2) != v(X3) ).
fof(axiom_021,axiom,
! [X] : proj1Print(print(X)) = X ).
fof(axiom_022,axiom,
! [X,X2] : proj1(x(X,X2)) = X ).
fof(axiom_023,axiom,
! [X,X2] : proj2(x(X,X2)) = X2 ).
fof(axiom_024,axiom,
! [X,X2] : proj1While(while(X,X2)) = X ).
fof(axiom_025,axiom,
! [X,X2] : proj2While(while(X,X2)) = X2 ).
fof(axiom_026,axiom,
! [X,X2,X3] : proj1If(if(X,X2,X3)) = X ).
fof(axiom_027,axiom,
! [X,X2,X3] : proj2If(if(X,X2,X3)) = X2 ).
fof(axiom_028,axiom,
! [X,X2,X3] : proj3If(if(X,X2,X3)) = X3 ).
fof(axiom_029,axiom,
! [X,X2,X3] : print(X) != x(X2,X3) ).
fof(axiom_030,axiom,
! [X,X2,X3] : print(X) != while(X2,X3) ).
fof(axiom_031,axiom,
! [X,X2,X3,X4] : print(X) != if(X2,X3,X4) ).
fof(axiom_032,axiom,
! [X,X2,X3,X4] : x(X,X2) != while(X3,X4) ).
fof(axiom_033,axiom,
! [X,X2,X3,X4,X5] : x(X,X2) != if(X3,X4,X5) ).
fof(axiom_034,axiom,
! [X,X2,X3,X4,X5] : while(X,X2) != if(X3,X4,X5) ).
fof(axiom_035,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_036,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_037,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_038,axiom,
! [X,X2] : head2(cons2(X,X2)) = X ).
fof(axiom_039,axiom,
! [X,X2] : tail2(cons2(X,X2)) = X2 ).
fof(axiom_040,axiom,
! [X,X2] : nil2 != cons2(X,X2) ).
fof(axiom_041,axiom,
! [Z] : store(nil,zero,Z) = cons(Z,nil) ).
fof(axiom_042,axiom,
! [Z,X2] : store(nil,suc(X2),Z) = cons(zero,store(nil,X2,Z)) ).
fof(axiom_043,axiom,
! [Z,N,St] : store(cons(N,St),zero,Z) = cons(Z,St) ).
fof(axiom_044,axiom,
! [Z,N,St,X3] : store(cons(N,St),suc(X3),Z) = cons(N,store(St,X3,Z)) ).
fof(axiom_045,axiom,
! [X] :
( X != while(proj1While(X),proj2While(X))
=> ( X != if(proj1If(X),proj2If(X),proj3If(X))
=> opti2(X) = X ) ) ).
fof(axiom_046,axiom,
! [E,P] : opti2(while(E,P)) = while(E,map(lam,P)) ).
fof(axiom_047,axiom,
! [C,Q,R] : opti2(if(C,Q,R)) = if(add(n(suc(zero)),C),R,Q) ).
fof(axiom_048,axiom,
! [Y] : fetch(nil,Y) = zero ).
fof(axiom_049,axiom,
! [N,St] : fetch(cons(N,St),zero) = N ).
fof(axiom_050,axiom,
! [N,St,Z] : fetch(cons(N,St),suc(Z)) = fetch(St,Z) ).
fof(axiom_051,axiom,
! [Y] : addNat(zero,Y) = Y ).
fof(axiom_052,axiom,
! [Z] : addNat(suc(Z),zero) = suc(Z) ).
fof(axiom_053,axiom,
! [Z,X2] : addNat(suc(Z),suc(X2)) = suc(addNat(Z,suc(X2))) ).
fof(axiom_054,axiom,
! [Y] : mulNat(zero,Y) = zero ).
fof(axiom_055,axiom,
! [Z] : mulNat(suc(Z),zero) = zero ).
fof(axiom_056,axiom,
! [Z,X2] : mulNat(suc(Z),suc(X2)) = addNat(mulNat(Z,suc(X2)),suc(X2)) ).
fof(axiom_057,axiom,
! [X,N] : eval(X,n(N)) = N ).
fof(axiom_058,axiom,
! [X,A,B] : eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)) ).
fof(axiom_059,axiom,
! [X,C,B2] : eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)) ).
fof(axiom_060,axiom,
! [X,A2,B3] :
( eval(X,A2) = eval(X,B3)
=> eval(X,eq(A2,B3)) = suc(zero) ) ).
fof(axiom_061,axiom,
! [X,A2,B3] :
( eval(X,A2) != eval(X,B3)
=> eval(X,eq(A2,B3)) = zero ) ).
fof(axiom_062,axiom,
! [X,Z] : eval(X,v(Z)) = fetch(X,Z) ).
fof(axiom_063,axiom,
! [X] : run(X,nil2) = nil ).
fof(axiom_064,axiom,
! [X,R,E] : run(X,cons2(print(E),R)) = cons(eval(X,E),run(X,R)) ).
fof(axiom_065,axiom,
! [X,R,X2,E2] : run(X,cons2(x(X2,E2),R)) = run(store(X,X2,eval(X,E2)),R) ).
fof(axiom_066,axiom,
! [X,R,E3,P] : run(X,cons2(while(E3,P),R)) = run(X,cons2(if(E3,append(P,cons2(while(E3,P),nil2)),nil2),R)) ).
fof(axiom_067,axiom,
! [X,R,E4,Q,Q2] :
( eval(X,E4) = zero
=> run(X,cons2(if(E4,Q,Q2),R)) = run(X,append(Q2,R)) ) ).
fof(axiom_068,axiom,
! [X,R,E4,Q,Q2,X3] :
( eval(X,E4) = suc(X3)
=> run(X,cons2(if(E4,Q,Q2),R)) = run(X,append(Q,R)) ) ).
fof(axiom_069,axiom,
! [F] : map(F,nil2) = nil2 ).
fof(axiom_070,axiom,
! [F,Y,Xs] : map(F,cons2(Y,Xs)) = cons2(apply1(F,Y),map(F,Xs)) ).
fof(axiom_071,axiom,
! [Y] : append(nil2,Y) = Y ).
fof(axiom_072,axiom,
! [Y,Z,Xs] : append(cons2(Z,Xs),Y) = cons2(Z,append(Xs,Y)) ).
fof(axiom_073,axiom,
! [Y] : apply1(lam,Y) = opti2(Y) ).
fof(goal_074,conjecture,
? [P] : run(nil,cons2(P,nil2)) != run(nil,cons2(opti2(P),nil2)) ).
%------------------------------------------------------------------------------