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 : Unsatisfiable
% Rating : 0.83 v9.3.0
% Syntax : Number of clauses : 105 ( 88 unt; 0 nHn; 3 RR)
% Number of literals : 124 ( 124 equ; 20 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 37 ( 37 usr; 6 con; 0-6 aty)
% Number of variables : 299 ( 162 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(X,A2,B3,btrue) = suc(zero) ).
cnf(axiom_001,axiom,
aux(X,A2,B3,bfalse) = zero ).
cnf(axiom_002,axiom,
aux2(X,R,E4,Q,Q2,btrue) = run(X,append(Q2,R)) ).
cnf(axiom_003,axiom,
aux2(X,R,E4,Q,Q2,bfalse) = run(X,append(Q,R)) ).
cnf(axiom_004,axiom,
store(nil,zero,Z) = cons(Z,nil) ).
cnf(axiom_005,axiom,
store(nil,suc(X2),Z) = cons(zero,store(nil,X2,Z)) ).
cnf(axiom_006,axiom,
store(cons(N,St),zero,Z) = cons(Z,St) ).
cnf(axiom_007,axiom,
store(cons(N,St),suc(X3),Z) = cons(N,store(St,X3,Z)) ).
cnf(axiom_008,axiom,
opti2(while(E,P)) = while(E,map(lam,P)) ).
cnf(axiom_009,axiom,
opti2(if(C,Q,R)) = if(add(n(suc(zero)),C),R,Q) ).
cnf(axiom_010,axiom,
opti2(print(X)) = print(X) ).
cnf(axiom_011,axiom,
opti2(x(X,X2)) = x(X,X2) ).
cnf(axiom_012,axiom,
fetch(nil,Y) = zero ).
cnf(axiom_013,axiom,
fetch(cons(N,St),zero) = N ).
cnf(axiom_014,axiom,
fetch(cons(N,St),suc(Z)) = fetch(St,Z) ).
cnf(axiom_015,axiom,
addNat(zero,Y) = Y ).
cnf(axiom_016,axiom,
addNat(suc(Z),zero) = suc(Z) ).
cnf(axiom_017,axiom,
addNat(suc(Z),suc(X2)) = suc(addNat(Z,suc(X2))) ).
cnf(axiom_018,axiom,
mulNat(zero,Y) = zero ).
cnf(axiom_019,axiom,
mulNat(suc(Z),zero) = zero ).
cnf(axiom_020,axiom,
mulNat(suc(Z),suc(X2)) = addNat(mulNat(Z,suc(X2)),suc(X2)) ).
cnf(axiom_021,axiom,
eval(X,n(N)) = N ).
cnf(axiom_022,axiom,
eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)) ).
cnf(axiom_023,axiom,
eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)) ).
cnf(axiom_024,axiom,
eval(X,eq(A2,B3)) = aux(X,A2,B3,eq4(eval(X,A2),eval(X,B3))) ).
cnf(axiom_025,axiom,
eval(X,v(Z)) = fetch(X,Z) ).
cnf(axiom_026,axiom,
run(X,nil2) = nil ).
cnf(axiom_027,axiom,
run(X,cons2(print(E),R)) = cons(eval(X,E),run(X,R)) ).
cnf(axiom_028,axiom,
run(X,cons2(x(X2,E2),R)) = run(store(X,X2,eval(X,E2)),R) ).
cnf(axiom_029,axiom,
run(X,cons2(while(E3,P),R)) = run(X,cons2(if(E3,append(P,cons2(while(E3,P),nil2)),nil2),R)) ).
cnf(axiom_030,axiom,
run(X,cons2(if(E4,Q,Q2),R)) = aux2(X,R,E4,Q,Q2,eq4(eval(X,E4),zero)) ).
cnf(axiom_031,axiom,
prop_Opti2(X) = eq2(run(nil,cons2(X,nil2)),run(nil,cons2(opti2(X),nil2))) ).
cnf(axiom_032,axiom,
map(F,nil2) = nil2 ).
cnf(axiom_033,axiom,
map(F,cons2(Y,Xs)) = cons2(apply1(F,Y),map(F,Xs)) ).
cnf(axiom_034,axiom,
append(nil2,Y) = Y ).
cnf(axiom_035,axiom,
append(cons2(Z,Xs),Y) = cons2(Z,append(Xs,Y)) ).
cnf(axiom_036,axiom,
eq7(bfalse,btrue) = bfalse ).
cnf(axiom_037,axiom,
eq7(btrue,bfalse) = bfalse ).
cnf(axiom_038,axiom,
eq4(X,X) = btrue ).
cnf(axiom_039,axiom,
eq5(X,X) = btrue ).
cnf(axiom_040,axiom,
eq6(X,X) = btrue ).
cnf(axiom_041,axiom,
eq7(X,X) = btrue ).
cnf(axiom_042,axiom,
eq2(X,X) = btrue ).
cnf(axiom_043,axiom,
eq3(X,X) = btrue ).
cnf(axiom_044,axiom,
( eq4(X,Z) != bfalse
| eq2(cons(X,Y),cons(Z,X2)) = bfalse ) ).
cnf(axiom_045,axiom,
( eq6(X,Z) != bfalse
| eq3(cons2(X,Y),cons2(Z,X2)) = bfalse ) ).
cnf(axiom_046,axiom,
( eq4(X,Z) != btrue
| eq2(cons(X,Y),cons(Z,X2)) = eq2(Y,X2) ) ).
cnf(axiom_047,axiom,
( eq6(X,Z) != btrue
| eq3(cons2(X,Y),cons2(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_048,axiom,
eq2(nil,cons(X,Y)) = bfalse ).
cnf(axiom_049,axiom,
eq3(nil2,cons2(X,Y)) = bfalse ).
cnf(axiom_050,axiom,
eq2(cons(X,Y),nil) = bfalse ).
cnf(axiom_051,axiom,
eq3(cons2(X,Y),nil2) = bfalse ).
cnf(axiom_052,axiom,
eq5(n(X),n(Y)) = eq4(X,Y) ).
cnf(axiom_053,axiom,
( eq5(X,Z) != bfalse
| eq5(add(X,Y),add(Z,X2)) = bfalse ) ).
cnf(axiom_054,axiom,
( eq5(X,Z) != btrue
| eq5(add(X,Y),add(Z,X2)) = eq5(Y,X2) ) ).
cnf(axiom_055,axiom,
( eq5(X,Z) != bfalse
| eq5(mul(X,Y),mul(Z,X2)) = bfalse ) ).
cnf(axiom_056,axiom,
( eq5(X,Z) != btrue
| eq5(mul(X,Y),mul(Z,X2)) = eq5(Y,X2) ) ).
cnf(axiom_057,axiom,
( eq5(X,Z) != bfalse
| eq5(eq(X,Y),eq(Z,X2)) = bfalse ) ).
cnf(axiom_058,axiom,
( eq5(X,Z) != btrue
| eq5(eq(X,Y),eq(Z,X2)) = eq5(Y,X2) ) ).
cnf(axiom_059,axiom,
eq5(v(X),v(Y)) = eq4(X,Y) ).
cnf(axiom_060,axiom,
eq5(n(X),add(Y,Z)) = bfalse ).
cnf(axiom_061,axiom,
eq5(n(X),mul(Y,Z)) = bfalse ).
cnf(axiom_062,axiom,
eq5(n(X),eq(Y,Z)) = bfalse ).
cnf(axiom_063,axiom,
eq5(n(X),v(Y)) = bfalse ).
cnf(axiom_064,axiom,
eq5(add(X,Y),n(Z)) = bfalse ).
cnf(axiom_065,axiom,
eq5(add(X,Y),mul(Z,X2)) = bfalse ).
cnf(axiom_066,axiom,
eq5(add(X,Y),eq(Z,X2)) = bfalse ).
cnf(axiom_067,axiom,
eq5(add(X,Y),v(Z)) = bfalse ).
cnf(axiom_068,axiom,
eq5(mul(X,Y),n(Z)) = bfalse ).
cnf(axiom_069,axiom,
eq5(mul(X,Y),add(Z,X2)) = bfalse ).
cnf(axiom_070,axiom,
eq5(mul(X,Y),eq(Z,X2)) = bfalse ).
cnf(axiom_071,axiom,
eq5(mul(X,Y),v(Z)) = bfalse ).
cnf(axiom_072,axiom,
eq5(eq(X,Y),n(Z)) = bfalse ).
cnf(axiom_073,axiom,
eq5(eq(X,Y),add(Z,X2)) = bfalse ).
cnf(axiom_074,axiom,
eq5(eq(X,Y),mul(Z,X2)) = bfalse ).
cnf(axiom_075,axiom,
eq5(eq(X,Y),v(Z)) = bfalse ).
cnf(axiom_076,axiom,
eq5(v(X),n(Y)) = bfalse ).
cnf(axiom_077,axiom,
eq5(v(X),add(Y,Z)) = bfalse ).
cnf(axiom_078,axiom,
eq5(v(X),mul(Y,Z)) = bfalse ).
cnf(axiom_079,axiom,
eq5(v(X),eq(Y,Z)) = bfalse ).
cnf(axiom_080,axiom,
eq4(suc(X),suc(Y)) = eq4(X,Y) ).
cnf(axiom_081,axiom,
eq4(zero,suc(X)) = bfalse ).
cnf(axiom_082,axiom,
eq4(suc(X),zero) = bfalse ).
cnf(axiom_083,axiom,
eq6(print(X),print(Y)) = eq5(X,Y) ).
cnf(axiom_084,axiom,
( eq4(X,Z) != bfalse
| eq6(x(X,Y),x(Z,X2)) = bfalse ) ).
cnf(axiom_085,axiom,
( eq4(X,Z) != btrue
| eq6(x(X,Y),x(Z,X2)) = eq5(Y,X2) ) ).
cnf(axiom_086,axiom,
( eq5(X,Z) != bfalse
| eq6(while(X,Y),while(Z,X2)) = bfalse ) ).
cnf(axiom_087,axiom,
( eq5(X,Z) != btrue
| eq6(while(X,Y),while(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_088,axiom,
( eq5(X,X2) != bfalse
| eq6(if(X,Y,Z),if(X2,X3,X4)) = bfalse ) ).
cnf(axiom_089,axiom,
( eq5(X,X2) != btrue
| eq3(Y,X3) != bfalse
| eq6(if(X,Y,Z),if(X2,X3,X4)) = bfalse ) ).
cnf(axiom_090,axiom,
( eq5(X,X2) != btrue
| eq3(Y,X3) != btrue
| eq6(if(X,Y,Z),if(X2,X3,X4)) = eq3(Z,X4) ) ).
cnf(axiom_091,axiom,
eq6(print(X),x(Y,Z)) = bfalse ).
cnf(axiom_092,axiom,
eq6(print(X),while(Y,Z)) = bfalse ).
cnf(axiom_093,axiom,
eq6(print(X),if(Y,Z,X2)) = bfalse ).
cnf(axiom_094,axiom,
eq6(x(X,Y),print(Z)) = bfalse ).
cnf(axiom_095,axiom,
eq6(x(X,Y),while(Z,X2)) = bfalse ).
cnf(axiom_096,axiom,
eq6(x(X,Y),if(Z,X2,X3)) = bfalse ).
cnf(axiom_097,axiom,
eq6(while(X,Y),print(Z)) = bfalse ).
cnf(axiom_098,axiom,
eq6(while(X,Y),x(Z,X2)) = bfalse ).
cnf(axiom_099,axiom,
eq6(while(X,Y),if(Z,X2,X3)) = bfalse ).
cnf(axiom_100,axiom,
eq6(if(X,Y,Z),print(X2)) = bfalse ).
cnf(axiom_101,axiom,
eq6(if(X,Y,Z),x(X2,X3)) = bfalse ).
cnf(axiom_102,axiom,
eq6(if(X,Y,Z),while(X2,X3)) = bfalse ).
cnf(axiom_103,axiom,
apply1(lam,Y) = opti2(Y) ).
cnf(goal,negated_conjecture,
eq7(prop_Opti2(X),bfalse) != btrue ).
%------------------------------------------------------------------------------