The rabbit sees the squirrel. The squirrel is young. The tiger chases the rabbit. If someone visits the tiger then the tiger is nice. If someone visits the rabbit and they see the tiger then they are nice.
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If someone visits the tiger then the tiger is nice.
((("someone" "visits" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If someone visits the rabbit and they see the tiger then they are nice.
((("someone" "visits" "rabbit" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "is" "nice" "+"))
The tiger chases the rabbit.
True
1
proof
[(triple3)]
("tiger" "chases" "rabbit" "+")
triple3
The squirrel is not young.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "young" "-")
triple2
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
@0: The rabbit sees the squirrel.[(triple1)] The squirrel is young.[(triple2)] The tiger chases the rabbit.[(triple3)]
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple1
The squirrel is young.
("squirrel" "is" "young" "+")
triple2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple3