The cat chases the tiger. The cat needs the mouse. The cat needs the tiger. The mouse is not cold. The tiger needs the mouse. The tiger visits the cat. The tiger does not visit the mouse. If someone is big then they chase the cat. If someone visits the tiger then they do not chase the tiger. If someone visits the mouse and they need the mouse then they do not chase the mouse. If someone chases the mouse then they do not need the tiger. If someone is young and they chase the tiger then the tiger needs the mouse. If someone chases the cat then the cat visits the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
If someone is big then they chase the cat.
((("someone" "is" "big" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the tiger then they do not chase the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "chases" "tiger" "-"))
If someone visits the mouse and they need the mouse then they do not chase the mouse.
((("someone" "visits" "mouse" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "chases" "mouse" "-"))
If someone chases the mouse then they do not need the tiger.
((("someone" "chases" "mouse" "+")) -> ("someone" "needs" "tiger" "-"))
If someone is young and they chase the tiger then the tiger needs the mouse.
((("someone" "is" "young" "+") ("someone" "chases" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone chases the cat then the cat visits the tiger.
((("someone" "chases" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
The cat needs the mouse.
True
1
proof
[(triple2)]
("cat" "needs" "mouse" "+")
triple2
The mouse is cold.
False
1
inv-proof
[(triple4)]
("mouse" "is" "cold" "+")
triple4
The tiger does not chase the cat.
Unknown
inv-rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "cat" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat needs the mouse.[(triple2)] The cat needs the tiger.[(triple3)] The mouse is not cold.[(triple4)] The tiger does not visit the mouse.[(triple7)] The tiger needs the mouse.[(triple5)] The tiger visits the cat.[(triple6)]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The mouse is not cold.
("mouse" "is" "cold" "-")
triple4
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple5
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple6