The cat chases the mouse. The mouse likes the cat. If someone needs the mouse then they are kind. If the mouse needs the cat then the cat likes the mouse. If someone chases the cat and the cat is green then the cat likes the mouse. If someone chases the mouse and they need the mouse then the mouse is kind. If the mouse chases the cat then the cat likes the mouse. If someone chases the mouse then the mouse chases the cat. If the mouse needs the cat and the mouse likes the cat then the cat is big. If someone is kind and they chase the mouse then the mouse needs the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If someone needs the mouse then they are kind.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "kind" "+"))
If the mouse needs the cat then the cat likes the mouse.
((("mouse" "needs" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If someone chases the cat and the cat is green then the cat likes the mouse.
((("someone" "chases" "cat" "+") ("cat" "is" "green" "+")) -> ("cat" "likes" "mouse" "+"))
If someone chases the mouse and they need the mouse then the mouse is kind.
((("someone" "chases" "mouse" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse chases the cat then the cat likes the mouse.
((("mouse" "chases" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If someone chases the mouse then the mouse chases the cat.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
If the mouse needs the cat and the mouse likes the cat then the cat is big.
((("mouse" "needs" "cat" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "is" "big" "+"))
If someone is kind and they chase the mouse then the mouse needs the cat.
((("someone" "is" "kind" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The mouse chases the cat.
True
2
proof
[(((triple1) -> rule6))]
("mouse" "chases" "cat" "+")
((triple1) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule6))]
("mouse" "chases" "cat" "-")
((triple1) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat is not big.
Unknown
inv-rconc
[@3: The cat is big.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule1 <- FAIL)]]
("cat" "is" "big" "-")
The mouse needs the cat.
Unknown
rconc
[@2: The mouse needs the cat.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("mouse" "needs" "cat" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat chases the mouse.[(triple1)] The mouse likes the cat.[(triple2)] @1: The mouse chases the cat.[(((triple1) -> rule6))] @2: The cat likes the mouse.[(((((triple1) -> rule6)) -> rule5))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple1) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2