The cow visits the dog. The dog sees the squirrel. The squirrel is red. The tiger is cold. If someone sees the cow and they need the tiger then the cow does not see the squirrel. If someone sees the squirrel then the squirrel does not see the tiger. If someone sees the squirrel then they visit the cow. If someone needs the dog and they are blue then they see the dog. If someone visits the dog and they do not need the tiger then the dog visits the tiger. If someone is cold then they are not blue. If someone sees the tiger and they see the squirrel then the squirrel visits the cow. If the tiger is not blue and the tiger does not visit the squirrel then the tiger does not need the cow.
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If someone sees the cow and they need the tiger then the cow does not see the squirrel.
((("someone" "sees" "cow" "+") ("someone" "needs" "tiger" "+")) -> ("cow" "sees" "squirrel" "-"))
If someone sees the squirrel then the squirrel does not see the tiger.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "-"))
If someone sees the squirrel then they visit the cow.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "cow" "+"))
If someone needs the dog and they are blue then they see the dog.
((("someone" "needs" "dog" "+") ("someone" "is" "blue" "+")) -> ("someone" "sees" "dog" "+"))
If someone visits the dog and they do not need the tiger then the dog visits the tiger.
((("someone" "visits" "dog" "+") ("someone" "needs" "tiger" "~")) -> ("dog" "visits" "tiger" "+"))
If someone is cold then they are not blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "-"))
If someone sees the tiger and they see the squirrel then the squirrel visits the cow.
((("someone" "sees" "tiger" "+") ("someone" "sees" "squirrel" "+")) -> ("squirrel" "visits" "cow" "+"))
If the tiger is not blue and the tiger does not visit the squirrel then the tiger does not need the cow.
((("tiger" "is" "blue" "~") ("tiger" "visits" "squirrel" "~")) -> ("tiger" "needs" "cow" "-"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The tiger is not cold.
False
1
inv-proof
[(triple4)]
("tiger" "is" "cold" "-")
triple4
The tiger does not visit the cow.
Unknown
inv-rconc
[@1: The tiger visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "cow" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow visits the dog.[(triple1)] The dog sees the squirrel.[(triple2)] The squirrel is red.[(triple3)] The tiger is cold.[(triple4)] @1: The dog visits the cow.[(((triple2) -> rule3))] The squirrel does not see the tiger.[(((triple2) -> rule2))] The tiger is not blue.[(((triple4) -> rule6))]
The cow visits the dog.
("cow" "visits" "dog" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The dog visits the cow.
("dog" "visits" "cow" "+")
((triple2) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
((triple2) -> (rule2 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The tiger is not blue.
("tiger" "is" "blue" "-")
((triple4) -> (rule6 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1