The dog is blue. The lion sees the squirrel. The squirrel is rough. The tiger sees the squirrel. If the squirrel does not visit the dog and the dog is not red then the dog sees the tiger.
The dog is blue.
("dog" "is" "blue" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the squirrel does not visit the dog and the dog is not red then the dog sees the tiger.
((("squirrel" "visits" "dog" "~") ("dog" "is" "red" "~")) -> ("dog" "sees" "tiger" "+"))
The tiger sees the squirrel.
True
1
proof
[(triple4)]
("tiger" "sees" "squirrel" "+")
triple4
The tiger does not see the squirrel.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "squirrel" "-")
triple4
The dog does not see the tiger.
Unknown
inv-rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "tiger" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The dog is blue.[(triple1)] The lion sees the squirrel.[(triple2)] The squirrel is rough.[(triple3)] The tiger sees the squirrel.[(triple4)]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple4