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

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

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 Ruby, please visit: http://ruby-doc.org/core-2.2.0/Regexp.html