The bear sees the squirrel. The cow sees the tiger. The squirrel does not see the bear. The tiger is nice. If someone sees the cow then the cow eats the bear. If someone sees the cow then they are round. If the cow sees the squirrel and the cow does not visit the squirrel then the squirrel sees the tiger.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone sees the cow then the cow eats the bear.
((("someone" "sees" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If someone sees the cow then they are round.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "round" "+"))
If the cow sees the squirrel and the cow does not visit the squirrel then the squirrel sees the tiger.
((("cow" "sees" "squirrel" "+") ("cow" "visits" "squirrel" "~")) -> ("squirrel" "sees" "tiger" "+"))
The bear sees the squirrel.
True
1
proof
[(triple1)]
("bear" "sees" "squirrel" "+")
triple1
The cow does not see the tiger.
False
1
inv-proof
[(triple2)]
("cow" "sees" "tiger" "-")
triple2
The cow does not eat the bear.
Unknown
inv-rconc
[@1: The cow eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "bear" "-")
The tiger eats the cow.
Unknown
random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "+")
@0: The bear sees the squirrel.[(triple1)] The cow sees the tiger.[(triple2)] The squirrel does not see the bear.[(triple3)] The tiger is nice.[(triple4)]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple2
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4