TPTP Problem File: SWX215-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX215-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Faulty property of regular expressions
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : RegExp_prop_star_plus_easy_2.p [CST26]
% Status : Unsatisfiable
% Rating : 1.00 v9.3.0
% Syntax : Number of clauses : 93 ( 93 unt; 0 nHn; 13 RR)
% Number of literals : 93 ( 93 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 26 ( 26 usr; 8 con; 0-4 aty)
% Number of variables : 177 ( 22 sgn)
% SPC : CNF_UNS_RFO_PEQ_UEQ
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Y,B,btrue) = eps ).
cnf(axiom_001,axiom,
aux(Y,B,bfalse) = nil2 ).
cnf(axiom_002,axiom,
aux2(Y,R,Q2,btrue) = x(y(step(R,Y),Q2),step(Q2,Y)) ).
cnf(axiom_003,axiom,
aux2(Y,R,Q2,bfalse) = x(y(step(R,Y),Q2),nil2) ).
cnf(axiom_004,axiom,
z(nil2,Y) = nil2 ).
cnf(axiom_005,axiom,
z(eps,Y) = Y ).
cnf(axiom_006,axiom,
z(atom(X),nil2) = nil2 ).
cnf(axiom_007,axiom,
z(atom(X),eps) = atom(X) ).
cnf(axiom_008,axiom,
z(atom(X),atom(X2)) = y(atom(X),atom(X2)) ).
cnf(axiom_009,axiom,
z(atom(X),x(X2,X3)) = y(atom(X),x(X2,X3)) ).
cnf(axiom_010,axiom,
z(atom(X),y(X2,X3)) = y(atom(X),y(X2,X3)) ).
cnf(axiom_011,axiom,
z(atom(X),star(X2)) = y(atom(X),star(X2)) ).
cnf(axiom_012,axiom,
z(x(X,X2),nil2) = nil2 ).
cnf(axiom_013,axiom,
z(x(X,X2),eps) = x(X,X2) ).
cnf(axiom_014,axiom,
z(x(X,X2),atom(X3)) = y(x(X,X2),atom(X3)) ).
cnf(axiom_015,axiom,
z(x(X,X2),x(X3,X4)) = y(x(X,X2),x(X3,X4)) ).
cnf(axiom_016,axiom,
z(x(X,X2),y(X3,X4)) = y(x(X,X2),y(X3,X4)) ).
cnf(axiom_017,axiom,
z(x(X,X2),star(X3)) = y(x(X,X2),star(X3)) ).
cnf(axiom_018,axiom,
z(y(X,X2),nil2) = nil2 ).
cnf(axiom_019,axiom,
z(y(X,X2),eps) = y(X,X2) ).
cnf(axiom_020,axiom,
z(y(X,X2),atom(X3)) = y(y(X,X2),atom(X3)) ).
cnf(axiom_021,axiom,
z(y(X,X2),x(X3,X4)) = y(y(X,X2),x(X3,X4)) ).
cnf(axiom_022,axiom,
z(y(X,X2),y(X3,X4)) = y(y(X,X2),y(X3,X4)) ).
cnf(axiom_023,axiom,
z(y(X,X2),star(X3)) = y(y(X,X2),star(X3)) ).
cnf(axiom_024,axiom,
z(star(X),nil2) = nil2 ).
cnf(axiom_025,axiom,
z(star(X),eps) = star(X) ).
cnf(axiom_026,axiom,
z(star(X),atom(X2)) = y(star(X),atom(X2)) ).
cnf(axiom_027,axiom,
z(star(X),x(X2,X3)) = y(star(X),x(X2,X3)) ).
cnf(axiom_028,axiom,
z(star(X),y(X2,X3)) = y(star(X),y(X2,X3)) ).
cnf(axiom_029,axiom,
z(star(X),star(X2)) = y(star(X),star(X2)) ).
cnf(axiom_030,axiom,
x2(nil2,Y) = Y ).
cnf(axiom_031,axiom,
x2(eps,nil2) = eps ).
cnf(axiom_032,axiom,
x2(eps,eps) = x(eps,eps) ).
cnf(axiom_033,axiom,
x2(eps,atom(X)) = x(eps,atom(X)) ).
cnf(axiom_034,axiom,
x2(eps,x(X,X2)) = x(eps,x(X,X2)) ).
cnf(axiom_035,axiom,
x2(eps,y(X,X2)) = x(eps,y(X,X2)) ).
cnf(axiom_036,axiom,
x2(eps,star(X)) = x(eps,star(X)) ).
cnf(axiom_037,axiom,
x2(atom(X),nil2) = atom(X) ).
cnf(axiom_038,axiom,
x2(atom(X),eps) = x(atom(X),eps) ).
cnf(axiom_039,axiom,
x2(atom(X),atom(X2)) = x(atom(X),atom(X2)) ).
cnf(axiom_040,axiom,
x2(atom(X),x(X2,X3)) = x(atom(X),x(X2,X3)) ).
cnf(axiom_041,axiom,
x2(atom(X),y(X2,X3)) = x(atom(X),y(X2,X3)) ).
cnf(axiom_042,axiom,
x2(atom(X),star(X2)) = x(atom(X),star(X2)) ).
cnf(axiom_043,axiom,
x2(x(X,X2),nil2) = x(X,X2) ).
cnf(axiom_044,axiom,
x2(x(X,X2),eps) = x(x(X,X2),eps) ).
cnf(axiom_045,axiom,
x2(x(X,X2),atom(X3)) = x(x(X,X2),atom(X3)) ).
cnf(axiom_046,axiom,
x2(x(X,X2),x(X3,X4)) = x(x(X,X2),x(X3,X4)) ).
cnf(axiom_047,axiom,
x2(x(X,X2),y(X3,X4)) = x(x(X,X2),y(X3,X4)) ).
cnf(axiom_048,axiom,
x2(x(X,X2),star(X3)) = x(x(X,X2),star(X3)) ).
cnf(axiom_049,axiom,
x2(y(X,X2),nil2) = y(X,X2) ).
cnf(axiom_050,axiom,
x2(y(X,X2),eps) = x(y(X,X2),eps) ).
cnf(axiom_051,axiom,
x2(y(X,X2),atom(X3)) = x(y(X,X2),atom(X3)) ).
cnf(axiom_052,axiom,
x2(y(X,X2),x(X3,X4)) = x(y(X,X2),x(X3,X4)) ).
cnf(axiom_053,axiom,
x2(y(X,X2),y(X3,X4)) = x(y(X,X2),y(X3,X4)) ).
cnf(axiom_054,axiom,
x2(y(X,X2),star(X3)) = x(y(X,X2),star(X3)) ).
cnf(axiom_055,axiom,
x2(star(X),nil2) = star(X) ).
cnf(axiom_056,axiom,
x2(star(X),eps) = x(star(X),eps) ).
cnf(axiom_057,axiom,
x2(star(X),atom(X2)) = x(star(X),atom(X2)) ).
cnf(axiom_058,axiom,
x2(star(X),x(X2,X3)) = x(star(X),x(X2,X3)) ).
cnf(axiom_059,axiom,
x2(star(X),y(X2,X3)) = x(star(X),y(X2,X3)) ).
cnf(axiom_060,axiom,
x2(star(X),star(X2)) = x(star(X),star(X2)) ).
cnf(axiom_061,axiom,
orb(btrue,Q) = btrue ).
cnf(axiom_062,axiom,
orb(bfalse,Q) = Q ).
cnf(axiom_063,axiom,
impl(btrue,Q) = Q ).
cnf(axiom_064,axiom,
impl(bfalse,Q) = btrue ).
cnf(axiom_065,axiom,
andb(btrue,Q) = Q ).
cnf(axiom_066,axiom,
andb(bfalse,Q) = bfalse ).
cnf(axiom_067,axiom,
eps2(eps) = btrue ).
cnf(axiom_068,axiom,
eps2(x(P,Q)) = orb(eps2(P),eps2(Q)) ).
cnf(axiom_069,axiom,
eps2(y(R,Q2)) = andb(eps2(R),eps2(Q2)) ).
cnf(axiom_070,axiom,
eps2(star(Y)) = btrue ).
cnf(axiom_071,axiom,
eps2(nil2) = bfalse ).
cnf(axiom_072,axiom,
eps2(atom(X)) = bfalse ).
cnf(axiom_073,axiom,
step(atom(B),Y) = aux(Y,B,eq(B,Y)) ).
cnf(axiom_074,axiom,
step(x(P,Q),Y) = x(step(P,Y),step(Q,Y)) ).
cnf(axiom_075,axiom,
step(y(R,Q2),Y) = aux2(Y,R,Q2,eps2(R)) ).
cnf(axiom_076,axiom,
step(star(P2),Y) = y(step(P2,Y),star(P2)) ).
cnf(axiom_077,axiom,
step(nil2,Y) = nil2 ).
cnf(axiom_078,axiom,
step(eps,Y) = nil2 ).
cnf(axiom_079,axiom,
rec(X,nil) = eps2(X) ).
cnf(axiom_080,axiom,
rec(X,cons(Z,Xs)) = rec(step(X,Z),Xs) ).
cnf(axiom_081,axiom,
prop_star_plus_easy_2(X,Y,Z,X2) = impl(eq2(rec(x(star(X),star(Y)),cons(Z,cons(X2,nil))),btrue),eq2(rec(star(x(X,Y)),cons(Z,cons(X2,nil))),btrue)) ).
cnf(axiom_082,axiom,
eq(a,b) = bfalse ).
cnf(axiom_083,axiom,
eq(a,c) = bfalse ).
cnf(axiom_084,axiom,
eq(b,a) = bfalse ).
cnf(axiom_085,axiom,
eq(b,c) = bfalse ).
cnf(axiom_086,axiom,
eq(c,a) = bfalse ).
cnf(axiom_087,axiom,
eq(c,b) = bfalse ).
cnf(axiom_088,axiom,
eq2(bfalse,btrue) = bfalse ).
cnf(axiom_089,axiom,
eq2(btrue,bfalse) = bfalse ).
cnf(axiom_090,axiom,
eq(X,X) = btrue ).
cnf(axiom_091,axiom,
eq2(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq2(prop_star_plus_easy_2(X,Y,Z,X2),bfalse) != btrue ).
%------------------------------------------------------------------------------