Regular Expressions 101

Save & Manage Regex

  • Current Version: 1
  • Save & Share
  • Community Library

Flavor

  • PCRE2 (PHP)
  • ECMAScript (JavaScript)
  • Python
  • Golang
  • Java
  • .NET 7.0 (C#)
  • Rust
  • PCRE (Legacy)
  • Regex Flavor Guide

Function

  • Match
  • Substitution
  • List
  • Unit Tests
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
Processing...

Test String

Code Generator

Language

Generated Code

import re regex = re.compile(r"^\[(?P<phase>\w+)\] (?P<operation>[\w ]+): (?P<formula_id>\d+)\. (?P<formula>.+) \[(?P<inference>[\w ,]*)\]$", flags=re.MULTILINE) test_str = ("/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") matches = regex.finditer(test_str) for match_num, match in enumerate(matches, start=1): print(f"Match {match_num} was found at {match.start()}-{match.end()}: {match.group()}") for group_num, group in enumerate(match.groups(), start=1): print(f"Group {group_num} found at {match.start(group_num)}-{match.end(group_num)}: {group}")

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 Python, please visit: https://docs.python.org/3/library/re.html