The mouse is round. The rabbit is kind. The rabbit needs the mouse. The rabbit visits the squirrel. The squirrel is kind. The squirrel sees the mouse. The squirrel sees the rabbit. The squirrel visits the tiger. The tiger needs the rabbit. The tiger sees the rabbit. The tiger sees the squirrel. The tiger visits the squirrel. If someone is round then they see the squirrel.
The mouse is round.
("mouse" "is" "round" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is round then they see the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
The rabbit visits the squirrel.
True
1
proof
[(triple4)]
("rabbit" "visits" "squirrel" "+")
triple4
The rabbit is not kind.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "kind" "-")
triple2
The mouse sees the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "sees" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "sees" "squirrel" "-")
((triple1) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The mouse does not need the rabbit.
Unknown
inv-random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "-")
The rabbit needs the squirrel.
Unknown
random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "+")
@0: The mouse is round.[(triple1)] The rabbit is kind.[(triple2)] The rabbit needs the mouse.[(triple3)] The rabbit visits the squirrel.[(triple4)] The squirrel is kind.[(triple5)] The squirrel sees the mouse.[(triple6)] The squirrel sees the rabbit.[(triple7)] The squirrel visits the tiger.[(triple8)] The tiger needs the rabbit.[(triple9)] The tiger sees the rabbit.[(triple10)] The tiger sees the squirrel.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The mouse sees the squirrel.[(((triple1) -> rule1))]
The mouse is round.
("mouse" "is" "round" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple3
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple4
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple5
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple6
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple7
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple8
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1