The bear does not see the tiger. The dog chases the lion. The lion visits the dog. The tiger is rough. If someone is red and not cold then they visit the bear. If the bear is cold and the bear is young then the bear sees the tiger. If someone chases the lion then the lion visits the dog. If the tiger visits the dog and the dog visits the tiger then the tiger does not see the lion. If someone chases the dog then they do not see the tiger. If the tiger does not chase the lion then the lion visits the tiger.
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone is red and not cold then they visit the bear.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "visits" "bear" "+"))
If the bear is cold and the bear is young then the bear sees the tiger.
((("bear" "is" "cold" "+") ("bear" "is" "young" "+")) -> ("bear" "sees" "tiger" "+"))
If someone chases the lion then the lion visits the dog.
((("someone" "chases" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If the tiger visits the dog and the dog visits the tiger then the tiger does not see the lion.
((("tiger" "visits" "dog" "+") ("dog" "visits" "tiger" "+")) -> ("tiger" "sees" "lion" "-"))
If someone chases the dog then they do not see the tiger.
((("someone" "chases" "dog" "+")) -> ("someone" "sees" "tiger" "-"))
If the tiger does not chase the lion then the lion visits the tiger.
((("tiger" "chases" "lion" "~")) -> ("lion" "visits" "tiger" "+"))
The bear does not see the tiger.
True
1
proof
[(triple1)]
("bear" "sees" "tiger" "-")
triple1
The lion does not visit the dog.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3))]
("lion" "visits" "dog" "-")
triple3
((triple2) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "bear" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bear does not see the tiger.[(triple1)] The dog chases the lion.[(triple2)] The lion visits the dog.[(triple3 OR ((triple2) -> rule3))] The tiger is rough.[(triple4)]
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
triple1
The dog chases the lion.
("dog" "chases" "lion" "+")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
((triple2) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
triple4