// #TestSpec: redundant:ID001; results:-1
Input R is bool
Input S is bool
Input P is bool 

ID000: Globally, it is always the case that once "R" becomes satisfied, "S" holds for at least "5" time units
ID001: After "P", it is always the case that once "R" becomes satisfied, "S" holds for at least "5" time units

// Unable to prove that Requirements ID001, ID001 are non-redundant (line -1). Cancelled while NwaCegarLoop was analyzing trace of length 14 with TraceHistMax 4,while TraceCheckSpWp was constructing backward predicates,while PolyPacSimplificationTermWalker was simplifying a ∨-10-1 term,while PolyPacSimplificationTermWalker was simplifying 10 xjuncts wrt. a ∧-23-10-6-12-3-7-4-10-3-9-3-5-4-3-3-6-3-4-2-5-3-8-3-6-2-9-3-2-1 context.)