; running example 1, section 3, 4, and 6, equation (14) ; ; to see the set of SNF clauses ; trp++uc -s BFS -f ltl --no-nnf --sharing=none --no-direct-clauses --no-snf-simplification -i running1.trp ; ; to see the UC in SNF without sets of time points ; trp++uc -s BFS -f ltl --no-nnf --sharing=none --no-direct-clauses --no-snf-simplification -u -g snf running1.trp ; ; to see the UC in LTL without sets of time points ; trp++uc -s BFS -f ltl --no-nnf --sharing=none --no-direct-clauses --no-snf-simplification -u -g ltl running1.trp ; ; to see the UC in SNF with sets of time points ; trp++uc -s BFS -f ltl --no-nnf --sharing=none --no-direct-clauses --no-snf-simplification -u --sets-of-time-points-uc -g snf running1.trp ; ; to see the UC in SNF with sets of time points ; trp++uc -s BFS -f ltl --no-nnf --sharing=none --no-direct-clauses --no-snf-simplification -u --sets-of-time-points-uc -g ltl running1.trp ; ((next not p) & always not q) & (p until (q & r))