The cat is rough. The mouse chases the tiger. The tiger sees the cat. If the mouse chases the cat and the mouse is rough then the mouse sees the cat. All kind people are rough. If someone needs the tiger and they are kind then the tiger is green. If the tiger needs the mouse and the tiger needs the cat then the cat chases the mouse. If the cat is rough then the cat chases the tiger. If the cat chases the mouse then the cat sees the mouse.
The cat is rough.
("cat" "is" "rough" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the mouse chases the cat and the mouse is rough then the mouse sees the cat.
((("mouse" "chases" "cat" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "sees" "cat" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the tiger and they are kind then the tiger is green.
((("someone" "needs" "tiger" "+") ("someone" "is" "kind" "+")) -> ("tiger" "is" "green" "+"))
If the tiger needs the mouse and the tiger needs the cat then the cat chases the mouse.
((("tiger" "needs" "mouse" "+") ("tiger" "needs" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If the cat is rough then the cat chases the tiger.
((("cat" "is" "rough" "+")) -> ("cat" "chases" "tiger" "+"))
If the cat chases the mouse then the cat sees the mouse.
((("cat" "chases" "mouse" "+")) -> ("cat" "sees" "mouse" "+"))
The tiger sees the cat.
True
1
proof
[(triple3)]
("tiger" "sees" "cat" "+")
triple3
The tiger does not see the cat.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "cat" "-")
triple3
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "cat" "-")
The cat sees the tiger.
Unknown
random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "+")
@0: The cat is rough.[(triple1)] The mouse chases the tiger.[(triple2)] The tiger sees the cat.[(triple3)] @1: The cat chases the tiger.[(((triple1) -> rule5))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple3
The cat chases the tiger.
("cat" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1