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
  • Match everything enclosed
    (?:...)
  • Capture everything enclosed
    (...)
  • 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

# coding=utf8 # the above tag defines encoding for this document and is for Python 2.x compatibility import re regex = r"^(?P<formula_id>\d+)\. (?P<formula>.+) \[(?P<inference_rule>[\w ]*)(?: (?P<inference_parents>[\d,]+))?\](?: \{(?P<extra>[\w,:-]*)\})?$" test_str = ("/home/filip/projects/vampire/build/Debug/bin/vampire_z3_dbg_master_6348 --show_everything on --proof_extra free /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] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[PP] final: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[PP] final: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}\n" "[PP] final: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}\n" "[PP] final: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}\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] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}\n" "35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}\n" "42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}\n" "43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}\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] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 32. lives(butler) [cnf transformation 3] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 33. lives(charles) [cnf transformation 4] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36] {a:1,w:6,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36] {a:1,w:6,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,thAx:0,allAx:5,thDist:-5}\n" "[SA] passive: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,thAx:0,allAx:5,thDist:-5}\n" "[SA] active: 40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,nSel:1,thAx:0,allAx:5,thDist:-5}\n" "[SA] new: 49. butler = butler [resolution 47,38] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] forward reduce: 49. butler = butler [resolution 47,38] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] active: 34. ~lives(X0) | butler = X0 | agatha = X0 | charles = X0 [cnf transformation 18] {a:0,w:11,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}\n" "[SA] forward reduce: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[SA] forward reduce: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[SA] forward reduce: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31] {a:1,w:9,thAx:0,allAx:2,thDist:-2}\n" "[AVATAR] split a clause: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}\n" "[AVATAR] recomputeModel: + 2, - \n" "[SA] new: 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" " replaced by 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" " using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" " using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] forward reduce: 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 31. lives(agatha) [cnf transformation 2] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] new: 70. $false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new propositional: 70. $false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] forward reduce: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" " replaced by 70. $false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}\n" " using 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}\n" "[AVATAR] proved 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[AVATAR] recomputeModel: + ~2,3, - 2,\n" "[SA] new: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" " replaced by 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" " using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" " using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] forward reduce: 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 32. lives(butler) [cnf transformation 3] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 75. hates(butler,agatha) <- (3) [resolution 74,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] forward reduce: 75. hates(butler,agatha) <- (3) [resolution 74,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" " using 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 76. agatha != butler <- (~2, 3) [superposition 60,65] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] forward reduce: 76. agatha != butler <- (~2, 3) [superposition 60,65] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" " using 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] active: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] passive: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] active: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,thAx:0,allAx:4,thDist:-4}\n" "[SA] passive: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,thAx:0,allAx:4,thDist:-4}\n" "[SA] active: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "[SA] active: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "[SA] new: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] new: 80. $false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}\n" "[SA] new propositional: 80. $false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}\n" "[SA] forward reduce: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" " replaced by 80. $false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}\n" " using 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "[AVATAR] proved 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[AVATAR] recomputeModel: + 1,~3, - 3,\n" "[SA] new: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] new: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" " replaced by 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" " using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" " replaced by 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" " using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] forward reduce: 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}\n" " using 33. lives(charles) [cnf transformation 4] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[SA] passive: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "[SA] active: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "[SA] new: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] new: 86. hates(charles,agatha) <- (1) [resolution 84,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] passive: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] forward reduce: 86. hates(charles,agatha) <- (1) [resolution 84,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" " using 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "[SA] active: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] passive: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] active: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] passive: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}\n" "[SA] active: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "[SA] new: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] passive: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,thAx:0,allAx:4,thDist:-4}\n" "[SA] active: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "[SA] active: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,nSel:1,thAx:0,allAx:6,thDist:-6}\n" "[SA] active: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,nSel:1,thAx:0,allAx:6,thDist:-6}\n" "[SA] active: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "[SA] new: 90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}\n" "[SA] new: 91. $false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}\n" "[SA] new propositional: 91. $false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}\n" "[SA] forward reduce: 90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}\n" " replaced by 91. $false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}\n" " using 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "[AVATAR] proved 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\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] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "34. ~lives(X0) | butler = X0 | agatha = X0 | charles = X0 [cnf transformation 18] {a:0,w:11,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}\n" "43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}\n" "44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}\n" "55. 1 <=> charles = sK0 [avatar definition]\n" "57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "59. 2 <=> agatha = sK0 [avatar definition]\n" "61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}\n" "63. 3 <=> butler = sK0 [avatar definition]\n" "65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "66. 1 | 2 | 3 [avatar split clause 53,63,59,55]\n" "69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}\n" "70. $false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}\n" "71. ~2 [avatar contradiction clause 70]\n" "74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}\n" "77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}\n" "80. $false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}\n" "81. ~3 [avatar contradiction clause 80]\n" "82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}\n" "89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}\n" "90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}\n" "91. $false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}\n" "92. ~1 [avatar contradiction clause 91]\n" "93. $false [avatar sat refutation 66,71,81,92] {a:0,w:0,goal:1,thAx:0,allAx:19,thDist:-19}\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.015 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 = re.finditer(regex, test_str, re.MULTILINE) for matchNum, match in enumerate(matches, start=1): print ("Match {matchNum} was found at {start}-{end}: {match}".format(matchNum = matchNum, start = match.start(), end = match.end(), match = match.group())) for groupNum in range(0, len(match.groups())): groupNum = groupNum + 1 print ("Group {groupNum} found at {start}-{end}: {group}".format(groupNum = groupNum, start = match.start(groupNum), end = match.end(groupNum), group = match.group(groupNum))) # Note: for Python 2.7 compatibility, use ur"" to prefix the regex and u"" to prefix the test string and substitution.

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