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

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

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 AutoIt, please visit: https://www.autoitscript.com/autoit3/docs/functions/StringRegExp.htm