The cow visits the tiger. The mouse is green. The squirrel visits the cow. The tiger likes the squirrel. If the squirrel is round then the squirrel sees the cow. If the tiger visits the cow then the tiger does not like the squirrel.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If the squirrel is round then the squirrel sees the cow.
((("squirrel" "is" "round" "+")) -> ("squirrel" "sees" "cow" "+"))
If the tiger visits the cow then the tiger does not like the squirrel.
((("tiger" "visits" "cow" "+")) -> ("tiger" "likes" "squirrel" "-"))
The tiger likes the squirrel.
True
1
proof
[(triple4)]
("tiger" "likes" "squirrel" "+")
triple4
The tiger does not like the squirrel.
False
1
inv-proof
[(triple4)]
("tiger" "likes" "squirrel" "-")
triple4
The squirrel does not see the cow.
Unknown
inv-rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cow visits the tiger.[(triple1)] The mouse is green.[(triple2)] The squirrel visits the cow.[(triple3)] The tiger likes the squirrel.[(triple4)]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple4