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