The bear is nice. The mouse likes the bear. The mouse likes the tiger. The mouse sees the tiger. The squirrel likes the mouse. The tiger likes the squirrel. The tiger visits the mouse. If someone likes the mouse then they see the squirrel.
The bear is nice.
("bear" "is" "nice" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone likes the mouse then they see the squirrel.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "squirrel" "+"))
The tiger visits the mouse.
True
1
proof
[(triple7)]
("tiger" "visits" "mouse" "+")
triple7
The tiger does not like the squirrel.
False
1
inv-proof
[(triple6)]
("tiger" "likes" "squirrel" "-")
triple6
The squirrel sees the squirrel.
True
2
proof
[(((triple5) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple5) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
Unknown
inv-rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The bear is nice.[(triple1)] The mouse likes the bear.[(triple2)] The mouse likes the tiger.[(triple3)] The mouse sees the tiger.[(triple4)] The squirrel likes the mouse.[(triple5)] The tiger likes the squirrel.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The squirrel sees the squirrel.[(((triple5) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple5
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1