The cat is rough. The cat needs the mouse. The cat sees the mouse. The cat sees the tiger. The cat visits the mouse. The mouse is green. The mouse needs the cat. The mouse sees the cat. The mouse sees the tiger. The mouse visits the cat. The mouse visits the tiger. The tiger needs the cat. The tiger sees the cat. The tiger sees the mouse. The tiger visits the cat. The tiger visits the mouse. If the tiger needs the mouse and the tiger visits the mouse then the tiger is red. If the tiger visits the mouse then the mouse is rough. If something needs the tiger and the tiger visits the mouse then the mouse visits the tiger.
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the tiger needs the mouse and the tiger visits the mouse then the tiger is red.
((("tiger" "needs" "mouse" "+") ("tiger" "visits" "mouse" "+")) -> ("tiger" "is" "red" "+"))
If the tiger visits the mouse then the mouse is rough.
((("tiger" "visits" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something needs the tiger and the tiger visits the mouse then the mouse visits the tiger.
((("something" "needs" "tiger" "+") ("tiger" "visits" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
The mouse sees the tiger.
True
1
proof
[(triple9)]
("mouse" "sees" "tiger" "+")
triple9
The mouse does not visit the tiger.
False
1
inv-proof
[(triple11)]
("mouse" "visits" "tiger" "-")
triple11
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat is rough.[(triple1)] The cat needs the mouse.[(triple2)] The cat sees the mouse.[(triple3)] The cat sees the tiger.[(triple4)] The cat visits the mouse.[(triple5)] The mouse is green.[(triple6)] The mouse needs the cat.[(triple7)] The mouse sees the cat.[(triple8)] The mouse sees the tiger.[(triple9)] The mouse visits the cat.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger needs the cat.[(triple12)] The tiger sees the cat.[(triple13)] The tiger sees the mouse.[(triple14)] The tiger visits the cat.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The mouse is rough.[(((triple16) -> rule2))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple7
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple8
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple9
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple12
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple13
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The mouse is rough.
("mouse" "is" "rough" "+")
((triple16) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1