Regular Expressions 101

Save & Share

Flavor

  • PCRE2 (PHP >=7.3)
  • PCRE (PHP <7.3)
  • ECMAScript (JavaScript)
  • Python
  • Golang
  • Java 8
  • .NET 7.0 (C#)
  • Rust
  • Regex Flavor Guide

Function

  • Match
  • Substitution
  • List
  • Unit Tests

Tools

Sponsors
There are currently no sponsors. Become a sponsor today!
An explanation of your regex will be automatically generated as you type.
Detailed match information will be displayed here automatically.
  • All Tokens
  • Common Tokens
  • General Tokens
  • Anchors
  • Meta Sequences
  • Quantifiers
  • Group Constructs
  • Character Classes
  • Flags/Modifiers
  • Substitution
  • A single character of: a, b or c
    [abc]
  • A character except: a, b or c
    [^abc]
  • A character in the range: a-z
    [a-z]
  • A character not in the range: a-z
    [^a-z]
  • A character in the range: a-z or A-Z
    [a-zA-Z]
  • Any single character
    .
  • Alternate - match either a or b
    a|b
  • Any whitespace character
    \s
  • Any non-whitespace character
    \S
  • Any digit
    \d
  • Any non-digit
    \D
  • Any word character
    \w
  • Any non-word character
    \W
  • Non-capturing group
    (?:...)
  • Capturing group
    (...)
  • Zero or one of a
    a?
  • Zero or more of a
    a*
  • One or more of a
    a+
  • Exactly 3 of a
    a{3}
  • 3 or more of a
    a{3,}
  • Between 3 and 6 of a
    a{3,6}
  • Start of string
    ^
  • End of string
    $
  • A word boundary
    \b
  • Non-word boundary
    \B

Regular Expression
No Match

r"
"
mg

Test String

Code Generator

Language

Generated Code

import java.util.regex.Matcher; import java.util.regex.Pattern; public class Example { public static void main(String[] args) { final String regex = "^\\[(?P<phase>\\w+)\\] (?P<operation>[\\w ]+): (?P<formula_id>\\d+)\\. (?P<formula>.+) \\[(?P<inference>[\\w ,]*)\\]$"; final String string = "/home/filip/projects/vampire/build/Debug/bin/vampire_z3_dbg_master_6348 --show_everything on /home/filip/TPTP-v7.5.0/Problems/PUZ/PUZ001+1.p\n\n\n" + "--------------------------------------------------------------------------------\n\n\n" + "% Running in auto input_syntax mode. Trying TPTP\n" + "preprocessing started\n" + "[PP] input: 1. ? [X0] : (killed(X0,agatha) & lives(X0)) [input]\n" + "[PP] input: 2. lives(agatha) [input]\n" + "[PP] input: 3. lives(butler) [input]\n" + "[PP] input: 4. lives(charles) [input]\n" + "[PP] input: 5. ! [X0] : (lives(X0) => (charles = X0 | butler = X0 | agatha = X0)) [input]\n" + "[PP] input: 6. ! [X0,X1] : (killed(X0,X1) => hates(X0,X1)) [input]\n" + "[PP] input: 7. ! [X0,X1] : (killed(X0,X1) => ~richer(X0,X1)) [input]\n" + "[PP] input: 8. ! [X0] : (hates(agatha,X0) => ~hates(charles,X0)) [input]\n" + "[PP] input: 9. ! [X0] : (butler != X0 => hates(agatha,X0)) [input]\n" + "[PP] input: 10. ! [X0] : (~richer(X0,agatha) => hates(butler,X0)) [input]\n" + "[PP] input: 11. ! [X0] : (hates(agatha,X0) => hates(butler,X0)) [input]\n" + "[PP] input: 12. ! [X0] : ? [X1] : ~hates(X0,X1) [input]\n" + "[PP] input: 13. agatha != butler [input]\n" + "[PP] input: 15. ~killed(agatha,agatha) [negated conjecture 14]\n" + "preprocess1 (rectify, simplify false true, flatten)\n" + "[PP] flatten in: 15. ~killed(agatha,agatha) [negated conjecture 14]\n" + "[PP] flatten out: 16. ~killed(agatha,agatha) [flattening 15]\n" + "unused predicate definition removal\n" + "[PP] pred marked as built-in: =\n" + "=: +(4) -(1) 0(0)\n" + "lives: +(4) -(1) 0(0)\n" + "killed: +(1) -(3) 0(0)\n" + "hates: +(4) -(4) 0(0)\n" + "richer: +(1) -(1) 0(0)\n" + "=: +(4) -(1) 0(0)\n" + "lives: +(4) -(1) 0(0)\n" + "killed: +(1) -(3) 0(0)\n" + "hates: +(4) -(4) 0(0)\n" + "richer: +(1) -(1) 0(0)\n" + "preprocess 2 (ennf,flatten)\n" + "[PP] ennf in: 5. ! [X0] : (lives(X0) => (charles = X0 | butler = X0 | agatha = X0)) [input]\n" + "[PP] ennf out: 17. ! [X0] : ((charles = X0 | butler = X0 | agatha = X0) | ~lives(X0)) [ennf transformation 5]\n" + "[PP] flatten in: 17. ! [X0] : ((charles = X0 | butler = X0 | agatha = X0) | ~lives(X0)) [ennf transformation 5]\n" + "[PP] flatten out: 18. ! [X0] : (charles = X0 | butler = X0 | agatha = X0 | ~lives(X0)) [flattening 17]\n" + "[PP] ennf in: 6. ! [X0,X1] : (killed(X0,X1) => hates(X0,X1)) [input]\n" + "[PP] ennf out: 19. ! [X0,X1] : (hates(X0,X1) | ~killed(X0,X1)) [ennf transformation 6]\n" + "[PP] ennf in: 7. ! [X0,X1] : (killed(X0,X1) => ~richer(X0,X1)) [input]\n" + "[PP] ennf out: 20. ! [X0,X1] : (~richer(X0,X1) | ~killed(X0,X1)) [ennf transformation 7]\n" + "[PP] ennf in: 8. ! [X0] : (hates(agatha,X0) => ~hates(charles,X0)) [input]\n" + "[PP] ennf out: 21. ! [X0] : (~hates(charles,X0) | ~hates(agatha,X0)) [ennf transformation 8]\n" + "[PP] ennf in: 9. ! [X0] : (butler != X0 => hates(agatha,X0)) [input]\n" + "[PP] ennf out: 22. ! [X0] : (hates(agatha,X0) | butler = X0) [ennf transformation 9]\n" + "[PP] ennf in: 10. ! [X0] : (~richer(X0,agatha) => hates(butler,X0)) [input]\n" + "[PP] ennf out: 23. ! [X0] : (hates(butler,X0) | richer(X0,agatha)) [ennf transformation 10]\n" + "[PP] ennf in: 11. ! [X0] : (hates(agatha,X0) => hates(butler,X0)) [input]\n" + "[PP] ennf out: 24. ! [X0] : (hates(butler,X0) | ~hates(agatha,X0)) [ennf transformation 11]\n" + "naming\n" + "[PP] naming args: 1. ? [X0] : (killed(X0,agatha) & lives(X0)) [input]\n" + "[PP] naming args: 2. lives(agatha) [input]\n" + "[PP] naming args: 3. lives(butler) [input]\n" + "[PP] naming args: 4. lives(charles) [input]\n" + "[PP] naming args: 18. ! [X0] : (charles = X0 | butler = X0 | agatha = X0 | ~lives(X0)) [flattening 17]\n" + "[PP] naming args: 19. ! [X0,X1] : (hates(X0,X1) | ~killed(X0,X1)) [ennf transformation 6]\n" + "[PP] naming args: 20. ! [X0,X1] : (~richer(X0,X1) | ~killed(X0,X1)) [ennf transformation 7]\n" + "[PP] naming args: 21. ! [X0] : (~hates(charles,X0) | ~hates(agatha,X0)) [ennf transformation 8]\n" + "[PP] naming args: 22. ! [X0] : (hates(agatha,X0) | butler = X0) [ennf transformation 9]\n" + "[PP] naming args: 23. ! [X0] : (hates(butler,X0) | richer(X0,agatha)) [ennf transformation 10]\n" + "[PP] naming args: 24. ! [X0] : (hates(butler,X0) | ~hates(agatha,X0)) [ennf transformation 11]\n" + "[PP] naming args: 12. ! [X0] : ? [X1] : ~hates(X0,X1) [input]\n" + "[PP] naming args: 13. agatha != butler [input]\n" + "[PP] naming args: 16. ~killed(agatha,agatha) [flattening 15]\n" + "preprocess3 (nnf, flatten, skolemize)\n" + "Skolemising: sK0 for X0 in ? [X0] : (killed(X0,agatha) & lives(X0)) in formula 1. ? [X0] : (killed(X0,agatha) & lives(X0)) [input]\n" + "Skolemising: sK1(X0) for X1 in ? [X1] : ~hates(X0,X1) in formula 12. ! [X0] : ? [X1] : ~hates(X0,X1) [input]\n" + "clausify\n" + "[PP] clausify: 26. killed(sK0,agatha) & lives(sK0) [skolemisation 1,25]\n" + "[PP] clausify: 2. lives(agatha) [input]\n" + "[PP] clausify: 3. lives(butler) [input]\n" + "[PP] clausify: 4. lives(charles) [input]\n" + "[PP] clausify: 18. ! [X0] : (charles = X0 | butler = X0 | agatha = X0 | ~lives(X0)) [flattening 17]\n" + "[PP] clausify: 19. ! [X0,X1] : (hates(X0,X1) | ~killed(X0,X1)) [ennf transformation 6]\n" + "[PP] clausify: 20. ! [X0,X1] : (~richer(X0,X1) | ~killed(X0,X1)) [ennf transformation 7]\n" + "[PP] clausify: 21. ! [X0] : (~hates(charles,X0) | ~hates(agatha,X0)) [ennf transformation 8]\n" + "[PP] clausify: 22. ! [X0] : (hates(agatha,X0) | butler = X0) [ennf transformation 9]\n" + "[PP] clausify: 23. ! [X0] : (hates(butler,X0) | richer(X0,agatha)) [ennf transformation 10]\n" + "[PP] clausify: 24. ! [X0] : (hates(butler,X0) | ~hates(agatha,X0)) [ennf transformation 11]\n" + "[PP] clausify: 28. ! [X0] : ~hates(X0,sK1(X0)) [skolemisation 12,27]\n" + "[PP] clausify: 13. agatha != butler [input]\n" + "[PP] clausify: 16. ~killed(agatha,agatha) [flattening 15]\n" + "[PP] final: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[PP] final: 29. lives(sK0) [cnf transformation 26]\n" + "[PP] final: 31. lives(agatha) [cnf transformation 2]\n" + "[PP] final: 32. lives(butler) [cnf transformation 3]\n" + "[PP] final: 33. lives(charles) [cnf transformation 4]\n" + "[PP] final: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18]\n" + "[PP] final: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19]\n" + "[PP] final: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "[PP] final: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "[PP] final: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "[PP] final: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23]\n" + "[PP] final: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24]\n" + "[PP] final: 41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "[PP] final: 42. agatha != butler [cnf transformation 13]\n" + "[PP] final: 43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "preprocessing finished\n" + "[PP] onPreprocessingEnd(), Proving Helper\n" + "1. ? [X0] : (killed(X0,agatha) & lives(X0)) [input]\n" + "2. lives(agatha) [input]\n" + "3. lives(butler) [input]\n" + "4. lives(charles) [input]\n" + "5. ! [X0] : (lives(X0) => (charles = X0 | butler = X0 | agatha = X0)) [input]\n" + "6. ! [X0,X1] : (killed(X0,X1) => hates(X0,X1)) [input]\n" + "7. ! [X0,X1] : (killed(X0,X1) => ~richer(X0,X1)) [input]\n" + "8. ! [X0] : (hates(agatha,X0) => ~hates(charles,X0)) [input]\n" + "9. ! [X0] : (butler != X0 => hates(agatha,X0)) [input]\n" + "10. ! [X0] : (~richer(X0,agatha) => hates(butler,X0)) [input]\n" + "11. ! [X0] : (hates(agatha,X0) => hates(butler,X0)) [input]\n" + "12. ! [X0] : ? [X1] : ~hates(X0,X1) [input]\n" + "13. agatha != butler [input]\n" + "14. killed(agatha,agatha) [input]\n" + "15. ~killed(agatha,agatha) [negated conjecture 14]\n" + "16. ~killed(agatha,agatha) [flattening 15]\n" + "17. ! [X0] : ((charles = X0 | butler = X0 | agatha = X0) | ~lives(X0)) [ennf transformation 5]\n" + "18. ! [X0] : (charles = X0 | butler = X0 | agatha = X0 | ~lives(X0)) [flattening 17]\n" + "19. ! [X0,X1] : (hates(X0,X1) | ~killed(X0,X1)) [ennf transformation 6]\n" + "20. ! [X0,X1] : (~richer(X0,X1) | ~killed(X0,X1)) [ennf transformation 7]\n" + "21. ! [X0] : (~hates(charles,X0) | ~hates(agatha,X0)) [ennf transformation 8]\n" + "22. ! [X0] : (hates(agatha,X0) | butler = X0) [ennf transformation 9]\n" + "23. ! [X0] : (hates(butler,X0) | richer(X0,agatha)) [ennf transformation 10]\n" + "24. ! [X0] : (hates(butler,X0) | ~hates(agatha,X0)) [ennf transformation 11]\n" + "25. ? [X0] : (killed(X0,agatha) & lives(X0)) => (killed(sK0,agatha) & lives(sK0)) [choice axiom]\n" + "26. killed(sK0,agatha) & lives(sK0) [skolemisation 1,25]\n" + "27. ! [X0] : (? [X1] : ~hates(X0,X1) => ~hates(X0,sK1(X0))) [choice axiom]\n" + "28. ! [X0] : ~hates(X0,sK1(X0)) [skolemisation 12,27]\n" + "29. lives(sK0) [cnf transformation 26]\n" + "30. killed(sK0,agatha) [cnf transformation 26]\n" + "31. lives(agatha) [cnf transformation 2]\n" + "32. lives(butler) [cnf transformation 3]\n" + "33. lives(charles) [cnf transformation 4]\n" + "34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18]\n" + "35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19]\n" + "36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23]\n" + "40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24]\n" + "41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "42. agatha != butler [cnf transformation 13]\n" + "43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "% type constructor precedences, smallest symbols first (line format: `<name> <arity>`) \n" + "% ===== begin of type constructor precedences ===== \n" + "% $i 0\n" + "% $o 0\n" + "% $int 0\n" + "% $real 0\n" + "% $rat 0\n" + "% ===== end of type constructor precedences ===== \n" + "%\n" + "% function precedences, smallest symbols first (line format: `<name> <arity>`) \n" + "% ===== begin of function precedences ===== \n" + "% agatha 0\n" + "% butler 0\n" + "% charles 0\n" + "% sK0 0\n" + "% sK1 1\n" + "% ===== end of function precedences ===== \n" + "%\n" + "% predicate precedences, smallest symbols first (line format: `<name> <arity>`) \n" + "% ===== begin of predicate precedences ===== \n" + "% lives 1\n" + "% = 2\n" + "% killed 2\n" + "% hates 2\n" + "% richer 2\n" + "% ===== end of predicate precedences ===== \n" + "%\n" + "% Predicate levels (line format: `<name> <arity> <level>`)\n" + "% ===== begin of predicate levels ===== \n" + "% = 2 0\n" + "% lives 1 1\n" + "% killed 2 1\n" + "% hates 2 1\n" + "% richer 2 1\n" + "% ===== end of predicate levels ===== \n" + "%\n" + "% Weights of function (line format: `<name> <arity> <weight>`)\n" + "% ===== begin of function weights ===== \n" + "% charles 0 1\n" + "% butler 0 1\n" + "% agatha 0 1\n" + "% sK1 1 1\n" + "% sK0 0 1\n" + "% $introduced 1\n" + "% $var 1\n" + "% $real 1\n" + "% $rat 1\n" + "% $int 1\n" + "% ===== end of function weights ===== \n" + "[SA] new: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] new: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] new: 31. lives(agatha) [cnf transformation 2]\n" + "[SA] new: 32. lives(butler) [cnf transformation 3]\n" + "[SA] new: 33. lives(charles) [cnf transformation 4]\n" + "[SA] new: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18]\n" + "[SA] new: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19]\n" + "[SA] new: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "[SA] new: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "[SA] new: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "[SA] new: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23]\n" + "[SA] new: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24]\n" + "[SA] new: 41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "[SA] new: 42. agatha != butler [cnf transformation 13]\n" + "[SA] new: 43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] passive: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] passive: 31. lives(agatha) [cnf transformation 2]\n" + "[SA] passive: 32. lives(butler) [cnf transformation 3]\n" + "[SA] passive: 33. lives(charles) [cnf transformation 4]\n" + "[SA] passive: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18]\n" + "[SA] passive: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19]\n" + "[SA] passive: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "[SA] passive: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "[SA] passive: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "[SA] passive: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23]\n" + "[SA] passive: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24]\n" + "[SA] passive: 41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "[SA] passive: 42. agatha != butler [cnf transformation 13]\n" + "[SA] passive: 43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "[SA] active: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] active: 31. lives(agatha) [cnf transformation 2]\n" + "[SA] active: 32. lives(butler) [cnf transformation 3]\n" + "[SA] active: 33. lives(charles) [cnf transformation 4]\n" + "[SA] active: 43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "[SA] active: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] active: 42. agatha != butler [cnf transformation 13]\n" + "[SA] active: 41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "[SA] active: 35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19]\n" + "[SA] new: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] active: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "[SA] active: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] active: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "[SA] active: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "[SA] new: 45. butler = sK1(agatha) [resolution 38,41]\n" + "[SA] passive: 45. butler = sK1(agatha) [resolution 38,41]\n" + "[SA] active: 39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23]\n" + "[SA] new: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36]\n" + "[SA] passive: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36]\n" + "[SA] active: 45. butler = sK1(agatha) [resolution 38,41]\n" + "[SA] new: 47. ~hates(agatha,butler) [superposition 41,45]\n" + "[SA] passive: 47. ~hates(agatha,butler) [superposition 41,45]\n" + "[SA] active: 40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24]\n" + "[SA] new: 48. hates(butler,X0) | butler = X0 [resolution 40,38]\n" + "[SA] passive: 48. hates(butler,X0) | butler = X0 [resolution 40,38]\n" + "[SA] active: 47. ~hates(agatha,butler) [superposition 41,45]\n" + "[SA] new: 49. butler = butler [resolution 47,38]\n" + "[SA] forward reduce: 49. butler = butler [resolution 47,38]\n" + "[SA] active: 34. ~lives(X0) | butler = X0 | agatha = X0 | charles = X0 [cnf transformation 18]\n" + "[SA] new: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31]\n" + "[SA] new: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32]\n" + "[SA] new: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33]\n" + "[SA] new: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29]\n" + "[SA] forward reduce: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33]\n" + "[SA] forward reduce: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32]\n" + "[SA] forward reduce: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31]\n" + "[AVATAR] split a clause: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29]\n" + "[AVATAR] recomputeModel: + 2, - \n" + "[SA] new: 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[SA] new: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61]\n" + "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30]\n" + " replaced by 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61]\n" + " using 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[SA] new: 68. lives(agatha) <- (2) [backward demodulation 29,61]\n" + "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26]\n" + " replaced by 68. lives(agatha) <- (2) [backward demodulation 29,61]\n" + " using 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[SA] new: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61]\n" + "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26]\n" + " replaced by 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61]\n" + " using 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[SA] passive: 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[SA] passive: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61]\n" + "[SA] forward reduce: 68. lives(agatha) <- (2) [backward demodulation 29,61]\n" + " using 31. lives(agatha) [cnf transformation 2]\n" + "[SA] new: 70. $false <- (2) [subsumption resolution 69,43]\n" + "[SA] new propositional: 70. $false <- (2) [subsumption resolution 69,43]\n" + "[SA] forward reduce: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61]\n" + " replaced by 70. $false <- (2) [subsumption resolution 69,43]\n" + " using 43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "[AVATAR] proved 61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "[AVATAR] recomputeModel: + ~2,3, - 2,\n" + "[SA] new: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] new: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] new: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] new: 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] new: 60. agatha != sK0 <- (~2) [avatar component clause 59]\n" + "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] passive: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] new: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65]\n" + "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30]\n" + " replaced by 72. hates(butler,agatha) <- (3) [backward demodulation 44,65]\n" + " using 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] new: 73. lives(butler) <- (3) [backward demodulation 29,65]\n" + "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26]\n" + " replaced by 73. lives(butler) <- (3) [backward demodulation 29,65]\n" + " using 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] new: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65]\n" + "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26]\n" + " replaced by 74. killed(butler,agatha) <- (3) [backward demodulation 30,65]\n" + " using 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] passive: 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] passive: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65]\n" + "[SA] forward reduce: 73. lives(butler) <- (3) [backward demodulation 29,65]\n" + " using 32. lives(butler) [cnf transformation 3]\n" + "[SA] passive: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65]\n" + "[SA] passive: 60. agatha != sK0 <- (~2) [avatar component clause 59]\n" + "[SA] active: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65]\n" + "[SA] new: 75. hates(butler,agatha) <- (3) [resolution 74,35]\n" + "[SA] forward reduce: 75. hates(butler,agatha) <- (3) [resolution 74,35]\n" + " using 72. hates(butler,agatha) <- (3) [backward demodulation 44,65]\n" + "[SA] active: 60. agatha != sK0 <- (~2) [avatar component clause 59]\n" + "[SA] active: 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[SA] new: 76. agatha != butler <- (~2, 3) [superposition 60,65]\n" + "[SA] forward reduce: 76. agatha != butler <- (~2, 3) [superposition 60,65]\n" + " using 42. agatha != butler [cnf transformation 13]\n" + "[SA] active: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65]\n" + "[SA] active: 46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36]\n" + "[SA] new: 77. hates(butler,butler) <- (3) [resolution 46,74]\n" + "[SA] passive: 77. hates(butler,butler) <- (3) [resolution 46,74]\n" + "[SA] active: 48. hates(butler,X0) | butler = X0 [resolution 40,38]\n" + "[SA] new: 78. butler = sK1(butler) [resolution 48,41]\n" + "[SA] passive: 78. butler = sK1(butler) [resolution 48,41]\n" + "[SA] active: 77. hates(butler,butler) <- (3) [resolution 46,74]\n" + "[SA] active: 78. butler = sK1(butler) [resolution 48,41]\n" + "[SA] new: 79. ~hates(butler,butler) [superposition 41,78]\n" + "[SA] new: 80. $false <- (3) [subsumption resolution 79,77]\n" + "[SA] new propositional: 80. $false <- (3) [subsumption resolution 79,77]\n" + "[SA] forward reduce: 79. ~hates(butler,butler) [superposition 41,78]\n" + " replaced by 80. $false <- (3) [subsumption resolution 79,77]\n" + " using 77. hates(butler,butler) <- (3) [resolution 46,74]\n" + "[AVATAR] proved 65. butler = sK0 <- (3) [avatar component clause 63]\n" + "[AVATAR] recomputeModel: + 1,~3, - 3,\n" + "[SA] new: 79. ~hates(butler,butler) [superposition 41,78]\n" + "[SA] new: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] new: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] new: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] new: 64. butler != sK0 <- (~3) [avatar component clause 63]\n" + "[SA] new: 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] passive: 79. ~hates(butler,butler) [superposition 41,78]\n" + "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26]\n" + "[SA] passive: 29. lives(sK0) [cnf transformation 26]\n" + "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30]\n" + "[SA] passive: 64. butler != sK0 <- (~3) [avatar component clause 63]\n" + "[SA] new: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30]\n" + " replaced by 82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + " using 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] new: 83. lives(charles) <- (1) [backward demodulation 29,57]\n" + "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26]\n" + " replaced by 83. lives(charles) <- (1) [backward demodulation 29,57]\n" + " using 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] new: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57]\n" + "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26]\n" + " replaced by 84. killed(charles,agatha) <- (1) [backward demodulation 30,57]\n" + " using 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] passive: 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] passive: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + "[SA] forward reduce: 83. lives(charles) <- (1) [backward demodulation 29,57]\n" + " using 33. lives(charles) [cnf transformation 4]\n" + "[SA] passive: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57]\n" + "[SA] active: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57]\n" + "[SA] new: 85. hates(butler,charles) <- (1) [resolution 84,46]\n" + "[SA] new: 86. hates(charles,agatha) <- (1) [resolution 84,35]\n" + "[SA] passive: 85. hates(butler,charles) <- (1) [resolution 84,46]\n" + "[SA] forward reduce: 86. hates(charles,agatha) <- (1) [resolution 84,35]\n" + " using 82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + "[SA] active: 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "[SA] new: 87. agatha != charles <- (1, ~2) [superposition 60,57]\n" + "[SA] passive: 87. agatha != charles <- (1, ~2) [superposition 60,57]\n" + "[SA] active: 64. butler != sK0 <- (~3) [avatar component clause 63]\n" + "[SA] new: 88. butler != charles <- (1, ~3) [superposition 64,57]\n" + "[SA] passive: 88. butler != charles <- (1, ~3) [superposition 64,57]\n" + "[SA] active: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + "[SA] new: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37]\n" + "[SA] passive: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37]\n" + "[SA] active: 85. hates(butler,charles) <- (1) [resolution 84,46]\n" + "[SA] active: 87. agatha != charles <- (1, ~2) [superposition 60,57]\n" + "[SA] active: 88. butler != charles <- (1, ~3) [superposition 64,57]\n" + "[SA] active: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37]\n" + "[SA] new: 90. agatha = butler <- (1) [resolution 89,38]\n" + "[SA] new: 91. $false <- (1) [subsumption resolution 90,42]\n" + "[SA] new propositional: 91. $false <- (1) [subsumption resolution 90,42]\n" + "[SA] forward reduce: 90. agatha = butler <- (1) [resolution 89,38]\n" + " replaced by 91. $false <- (1) [subsumption resolution 90,42]\n" + " using 42. agatha != butler [cnf transformation 13]\n" + "[AVATAR] proved 57. charles = sK0 <- (1) [avatar component clause 55]\n" + "% Refutation found. Thanks to Tanya!\n" + "% SZS status Theorem for PUZ001+1\n" + "% SZS output start Proof for PUZ001+1\n" + "1. ? [X0] : (killed(X0,agatha) & lives(X0)) [input]\n" + "5. ! [X0] : (lives(X0) => (charles = X0 | butler = X0 | agatha = X0)) [input]\n" + "6. ! [X0,X1] : (killed(X0,X1) => hates(X0,X1)) [input]\n" + "7. ! [X0,X1] : (killed(X0,X1) => ~richer(X0,X1)) [input]\n" + "8. ! [X0] : (hates(agatha,X0) => ~hates(charles,X0)) [input]\n" + "9. ! [X0] : (butler != X0 => hates(agatha,X0)) [input]\n" + "10. ! [X0] : (~richer(X0,agatha) => hates(butler,X0)) [input]\n" + "11. ! [X0] : (hates(agatha,X0) => hates(butler,X0)) [input]\n" + "12. ! [X0] : ? [X1] : ~hates(X0,X1) [input]\n" + "13. agatha != butler [input]\n" + "14. killed(agatha,agatha) [input]\n" + "15. ~killed(agatha,agatha) [negated conjecture 14]\n" + "16. ~killed(agatha,agatha) [flattening 15]\n" + "17. ! [X0] : ((charles = X0 | butler = X0 | agatha = X0) | ~lives(X0)) [ennf transformation 5]\n" + "18. ! [X0] : (charles = X0 | butler = X0 | agatha = X0 | ~lives(X0)) [flattening 17]\n" + "19. ! [X0,X1] : (hates(X0,X1) | ~killed(X0,X1)) [ennf transformation 6]\n" + "20. ! [X0,X1] : (~richer(X0,X1) | ~killed(X0,X1)) [ennf transformation 7]\n" + "21. ! [X0] : (~hates(charles,X0) | ~hates(agatha,X0)) [ennf transformation 8]\n" + "22. ! [X0] : (hates(agatha,X0) | butler = X0) [ennf transformation 9]\n" + "23. ! [X0] : (hates(butler,X0) | richer(X0,agatha)) [ennf transformation 10]\n" + "24. ! [X0] : (hates(butler,X0) | ~hates(agatha,X0)) [ennf transformation 11]\n" + "25. ? [X0] : (killed(X0,agatha) & lives(X0)) => (killed(sK0,agatha) & lives(sK0)) [choice axiom]\n" + "26. killed(sK0,agatha) & lives(sK0) [skolemisation 1,25]\n" + "27. ! [X0] : (? [X1] : ~hates(X0,X1) => ~hates(X0,sK1(X0))) [choice axiom]\n" + "28. ! [X0] : ~hates(X0,sK1(X0)) [skolemisation 12,27]\n" + "29. lives(sK0) [cnf transformation 26]\n" + "30. killed(sK0,agatha) [cnf transformation 26]\n" + "34. ~lives(X0) | butler = X0 | agatha = X0 | charles = X0 [cnf transformation 18]\n" + "35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19]\n" + "36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20]\n" + "37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21]\n" + "38. hates(agatha,X0) | butler = X0 [cnf transformation 22]\n" + "39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23]\n" + "40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24]\n" + "41. ~hates(X0,sK1(X0)) [cnf transformation 28]\n" + "42. agatha != butler [cnf transformation 13]\n" + "43. ~killed(agatha,agatha) [cnf transformation 16]\n" + "44. hates(sK0,agatha) [resolution 35,30]\n" + "46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36]\n" + "48. hates(butler,X0) | butler = X0 [resolution 40,38]\n" + "53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29]\n" + "55. 1 <=> charles = sK0 [avatar definition]\n" + "57. charles = sK0 <- (1) [avatar component clause 55]\n" + "59. 2 <=> agatha = sK0 [avatar definition]\n" + "61. agatha = sK0 <- (2) [avatar component clause 59]\n" + "63. 3 <=> butler = sK0 [avatar definition]\n" + "65. butler = sK0 <- (3) [avatar component clause 63]\n" + "66. 1 | 2 | 3 [avatar split clause 53,63,59,55]\n" + "69. killed(agatha,agatha) <- (2) [backward demodulation 30,61]\n" + "70. $false <- (2) [subsumption resolution 69,43]\n" + "71. ~2 [avatar contradiction clause 70]\n" + "74. killed(butler,agatha) <- (3) [backward demodulation 30,65]\n" + "77. hates(butler,butler) <- (3) [resolution 46,74]\n" + "78. butler = sK1(butler) [resolution 48,41]\n" + "79. ~hates(butler,butler) [superposition 41,78]\n" + "80. $false <- (3) [subsumption resolution 79,77]\n" + "81. ~3 [avatar contradiction clause 80]\n" + "82. hates(charles,agatha) <- (1) [backward demodulation 44,57]\n" + "89. ~hates(agatha,agatha) <- (1) [resolution 82,37]\n" + "90. agatha = butler <- (1) [resolution 89,38]\n" + "91. $false <- (1) [subsumption resolution 90,42]\n" + "92. ~1 [avatar contradiction clause 91]\n" + "93. $false [avatar sat refutation 66,71,81,92]\n" + "% SZS output end Proof for PUZ001+1\n" + "% ------------------------------\n" + "% Version: Vampire 4.7 (commit d52d66222 on 2022-08-16 12:56:08 +0200)\n" + "% Linked with Z3 4.8.13.0 f03d756e086f81f2596157241e0decfb1c982299 z3-4.8.4-5390-gf03d756e0\n" + "% Termination reason: Refutation\n\n" + "% Memory used [KB]: 4989\n" + "% Time elapsed: 0.014 s\n" + "% ------------------------------\n" + "---- Runtime statistics ----\n" + "clauses created: 58\n" + "clauses deleted: 8\n" + "ssat_new_components: 3\n" + "ssat_sat_clauses: 4\n" + "total_frozen: 10\n" + "total_unfrozen: 7\n" + "unworthy child removed: 13\n" + "-----------------------------\n" + "% ------------------------------\n"; final Pattern pattern = Pattern.compile(regex, Pattern.MULTILINE); final Matcher matcher = pattern.matcher(string); while (matcher.find()) { System.out.println("Full match: " + matcher.group(0)); for (int i = 1; i <= matcher.groupCount(); i++) { System.out.println("Group " + i + ": " + matcher.group(i)); } } } }

Please keep in mind that these code samples are automatically generated and are not guaranteed to work. If you find any syntax errors, feel free to submit a bug report. For a full regex reference for Java, please visit: https://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html