const regex = new RegExp('^(?P<formula_id>\\d+)\\. (?P<formula>.+) \\[(?P<inference_rule>[\\w ]*)(?: (?P<inference_parents>[\\d,]+))?\\](?: \\{(?P<extra>[\\w,:-]*)\\})?$', 'mg')
const 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
--------------------------------------------------------------------------------
% 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] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[PP] final: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[PP] final: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[PP] final: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[PP] final: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[PP] final: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}
[PP] final: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[PP] final: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}
[PP] final: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}
[PP] final: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}
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] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}
35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}
42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}
43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}
% 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] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[SA] new: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] new: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] new: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] new: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}
[SA] new: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] new: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}
[SA] new: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}
[SA] new: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}
[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[SA] passive: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] passive: 32. lives(butler) [cnf transformation 3] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] passive: 33. lives(charles) [cnf transformation 4] {a:0,w:2,thAx:0,allAx:1,thDist:-1}
[SA] passive: 34. charles = X0 | butler = X0 | agatha = X0 | ~lives(X0) [cnf transformation 18] {a:0,w:11,thAx:0,allAx:1,thDist:-1}
[SA] passive: 35. hates(X0,X1) | ~killed(X0,X1) [cnf transformation 19] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 39. hates(butler,X0) | richer(X0,agatha) [cnf transformation 23] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 40. hates(butler,X0) | ~hates(agatha,X0) [cnf transformation 24] {a:0,w:6,thAx:0,allAx:1,thDist:-1}
[SA] passive: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,thAx:0,allAx:2,thDist:-2}
[SA] passive: 42. agatha != butler [cnf transformation 13] {a:0,w:3,thAx:0,allAx:1,thDist:-1}
[SA] passive: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,goal:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] active: 31. lives(agatha) [cnf transformation 2] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 32. lives(butler) [cnf transformation 3] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 33. lives(charles) [cnf transformation 4] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] active: 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] active: 35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] active: 36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] active: 37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] new: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,thAx:0,allAx:3,thDist:-3}
[SA] passive: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,thAx:0,allAx:3,thDist:-3}
[SA] active: 39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] new: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36] {a:1,w:6,thAx:0,allAx:2,thDist:-2}
[SA] passive: 46. hates(butler,X0) | ~killed(X0,agatha) [resolution 39,36] {a:1,w:6,thAx:0,allAx:2,thDist:-2}
[SA] active: 45. butler = sK1(agatha) [resolution 38,41] {a:1,w:4,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,thAx:0,allAx:5,thDist:-5}
[SA] passive: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,thAx:0,allAx:5,thDist:-5}
[SA] active: 40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] new: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,thAx:0,allAx:2,thDist:-2}
[SA] passive: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,thAx:0,allAx:2,thDist:-2}
[SA] active: 47. ~hates(agatha,butler) [superposition 41,45] {a:2,w:3,nSel:1,thAx:0,allAx:5,thDist:-5}
[SA] new: 49. butler = butler [resolution 47,38] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
[SA] forward reduce: 49. butler = butler [resolution 47,38] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
[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}
[SA] new: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[SA] new: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[SA] new: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[SA] new: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}
[SA] forward reduce: 52. butler = charles | agatha = charles | charles = charles [resolution 34,33] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[SA] forward reduce: 51. butler = butler | agatha = butler | butler = charles [resolution 34,32] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[SA] forward reduce: 50. agatha = butler | agatha = agatha | agatha = charles [resolution 34,31] {a:1,w:9,thAx:0,allAx:2,thDist:-2}
[AVATAR] split a clause: 53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}
[AVATAR] recomputeModel: + 2, -
[SA] new: 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
replaced by 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
using 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 67. hates(agatha,agatha) <- (2) [backward demodulation 44,61] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] forward reduce: 68. lives(agatha) <- (2) [backward demodulation 29,61] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 31. lives(agatha) [cnf transformation 2] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] new: 70. \$false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}
[SA] new propositional: 70. \$false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}
[SA] forward reduce: 69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
replaced by 70. \$false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}
using 43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}
[AVATAR] proved 61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[AVATAR] recomputeModel: + ~2,3, - 2,
[SA] new: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
replaced by 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
using 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] forward reduce: 73. lives(butler) <- (3) [backward demodulation 29,65] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 32. lives(butler) [cnf transformation 3] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] passive: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] passive: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] active: 74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 75. hates(butler,agatha) <- (3) [resolution 74,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] forward reduce: 75. hates(butler,agatha) <- (3) [resolution 74,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
using 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] active: 60. agatha != sK0 <- (~2) [avatar component clause 59] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] active: 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 76. agatha != butler <- (~2, 3) [superposition 60,65] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
[SA] forward reduce: 76. agatha != butler <- (~2, 3) [superposition 60,65] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
using 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] active: 72. hates(butler,agatha) <- (3) [backward demodulation 44,65] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] active: 46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] passive: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] active: 48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,thAx:0,allAx:4,thDist:-4}
[SA] passive: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,thAx:0,allAx:4,thDist:-4}
[SA] active: 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
[SA] active: 78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,nSel:1,thAx:0,allAx:4,thDist:-4}
[SA] new: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
[SA] new: 80. \$false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}
[SA] new propositional: 80. \$false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}
[SA] forward reduce: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
replaced by 80. \$false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}
using 77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
[AVATAR] proved 65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[AVATAR] recomputeModel: + 1,~3, - 3,
[SA] new: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
[SA] new: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
[SA] passive: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] passive: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] passive: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] passive: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] backward reduce: 44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
replaced by 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 29. lives(sK0) [cnf transformation 26] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] new: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] backward reduce: 30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
replaced by 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
using 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] forward reduce: 83. lives(charles) <- (1) [backward demodulation 29,57] {a:0,w:2,thAx:0,allAx:2,thDist:-2}
using 33. lives(charles) [cnf transformation 4] {a:0,w:2,nSel:1,thAx:0,allAx:1,thDist:-1}
[SA] passive: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
[SA] active: 84. killed(charles,agatha) <- (1) [backward demodulation 30,57] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
[SA] new: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] new: 86. hates(charles,agatha) <- (1) [resolution 84,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] passive: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] forward reduce: 86. hates(charles,agatha) <- (1) [resolution 84,35] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
using 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
[SA] active: 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
[SA] passive: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
[SA] active: 64. butler != sK0 <- (~3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
[SA] passive: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,thAx:0,allAx:6,thDist:-6}
[SA] active: 82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
[SA] new: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] passive: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,thAx:0,allAx:4,thDist:-4}
[SA] active: 85. hates(butler,charles) <- (1) [resolution 84,46] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
[SA] active: 87. agatha != charles <- (1, ~2) [superposition 60,57] {a:2,w:3,nSel:1,thAx:0,allAx:6,thDist:-6}
[SA] active: 88. butler != charles <- (1, ~3) [superposition 64,57] {a:2,w:3,nSel:1,thAx:0,allAx:6,thDist:-6}
[SA] active: 89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
[SA] new: 90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}
[SA] new: 91. \$false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}
[SA] new propositional: 91. \$false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}
[SA] forward reduce: 90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}
replaced by 91. \$false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}
using 42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}
[AVATAR] proved 57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
% 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] {a:0,w:2,nSel:1,thAx:0,allAx:2,thDist:-2}
30. killed(sK0,agatha) [cnf transformation 26] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
34. ~lives(X0) | butler = X0 | agatha = X0 | charles = X0 [cnf transformation 18] {a:0,w:11,nSel:1,thAx:0,allAx:1,thDist:-1}
35. ~killed(X0,X1) | hates(X0,X1) [cnf transformation 19] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
36. ~richer(X0,X1) | ~killed(X0,X1) [cnf transformation 20] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
37. ~hates(charles,X0) | ~hates(agatha,X0) [cnf transformation 21] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
38. hates(agatha,X0) | butler = X0 [cnf transformation 22] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
39. richer(X0,agatha) | hates(butler,X0) [cnf transformation 23] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
40. ~hates(agatha,X0) | hates(butler,X0) [cnf transformation 24] {a:0,w:6,nSel:1,thAx:0,allAx:1,thDist:-1}
41. ~hates(X0,sK1(X0)) [cnf transformation 28] {a:0,w:4,nSel:1,thAx:0,allAx:2,thDist:-2}
42. agatha != butler [cnf transformation 13] {a:0,w:3,nSel:1,thAx:0,allAx:1,thDist:-1}
43. ~killed(agatha,agatha) [cnf transformation 16] {a:0,w:3,nSel:1,goal:1,thAx:0,allAx:1,thDist:-1}
44. hates(sK0,agatha) [resolution 35,30] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
46. ~killed(X0,agatha) | hates(butler,X0) [resolution 39,36] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}
48. hates(butler,X0) | butler = X0 [resolution 40,38] {a:1,w:6,nSel:1,thAx:0,allAx:2,thDist:-2}
53. butler = sK0 | agatha = sK0 | charles = sK0 [resolution 34,29] {a:1,w:9,thAx:0,allAx:3,thDist:-3}
55. 1 <=> charles = sK0 [avatar definition]
57. charles = sK0 <- (1) [avatar component clause 55] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
59. 2 <=> agatha = sK0 [avatar definition]
61. agatha = sK0 <- (2) [avatar component clause 59] {a:1,w:3,thAx:0,allAx:3,thDist:-3}
63. 3 <=> butler = sK0 [avatar definition]
65. butler = sK0 <- (3) [avatar component clause 63] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
66. 1 | 2 | 3 [avatar split clause 53,63,59,55]
69. killed(agatha,agatha) <- (2) [backward demodulation 30,61] {a:0,w:3,thAx:0,allAx:2,thDist:-2}
70. \$false <- (2) [subsumption resolution 69,43] {a:0,w:0,goal:1,thAx:0,allAx:2,thDist:-2}
71. ~2 [avatar contradiction clause 70]
74. killed(butler,agatha) <- (3) [backward demodulation 30,65] {a:0,w:3,nSel:1,thAx:0,allAx:2,thDist:-2}
77. hates(butler,butler) <- (3) [resolution 46,74] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
78. butler = sK1(butler) [resolution 48,41] {a:2,w:4,nSel:1,thAx:0,allAx:4,thDist:-4}
79. ~hates(butler,butler) [superposition 41,78] {a:3,w:3,thAx:0,allAx:6,thDist:-6}
80. \$false <- (3) [subsumption resolution 79,77] {a:3,w:0,thAx:0,allAx:6,thDist:-6}
81. ~3 [avatar contradiction clause 80]
82. hates(charles,agatha) <- (1) [backward demodulation 44,57] {a:1,w:3,nSel:1,thAx:0,allAx:3,thDist:-3}
89. ~hates(agatha,agatha) <- (1) [resolution 82,37] {a:2,w:3,nSel:1,thAx:0,allAx:4,thDist:-4}
90. agatha = butler <- (1) [resolution 89,38] {a:3,w:3,thAx:0,allAx:5,thDist:-5}
91. \$false <- (1) [subsumption resolution 90,42] {a:3,w:0,thAx:0,allAx:5,thDist:-5}
92. ~1 [avatar contradiction clause 91]
93. \$false [avatar sat refutation 66,71,81,92] {a:0,w:0,goal:1,thAx:0,allAx:19,thDist:-19}
% 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.015 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
-----------------------------
% ------------------------------
`;
// Reset `lastIndex` if this regex is defined globally
// regex.lastIndex = 0;
let m;
while ((m = regex.exec(str)) !== null) {
// This is necessary to avoid infinite loops with zero-width matches
if (m.index === regex.lastIndex) {
regex.lastIndex++;
}
// The result can be accessed through the `m`-variable.
m.forEach((match, groupIndex) => {
console.log(`Found match, group ${groupIndex}: ${match}`);
});
}
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 JavaScript, please visit: https://developer.mozilla.org/en/docs/Web/JavaScript/Guide/Regular_Expressions