The bear is rough. The bear likes the tiger. The bear visits the dog. The cow likes the dog. The dog sees the cow. The tiger sees the bear. The tiger visits the dog. If something likes the bear and it visits the tiger then the tiger visits the cow. If the bear is cold and the bear sees the dog then the bear sees the tiger. If something is green and it sees the cow then it likes the dog. If something visits the bear and it is kind then it sees the bear. If something visits the tiger and it sees the bear then it is red. If something is green and it visits the dog then it visits the tiger. If something visits the bear and the bear is green then it sees the cow. If something is green then it visits the tiger.
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something likes the bear and it visits the tiger then the tiger visits the cow.
((("something" "likes" "bear" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
If the bear is cold and the bear sees the dog then the bear sees the tiger.
((("bear" "is" "cold" "+") ("bear" "sees" "dog" "+")) -> ("bear" "sees" "tiger" "+"))
If something is green and it sees the cow then it likes the dog.
((("something" "is" "green" "+") ("something" "sees" "cow" "+")) -> ("something" "likes" "dog" "+"))
If something visits the bear and it is kind then it sees the bear.
((("something" "visits" "bear" "+") ("something" "is" "kind" "+")) -> ("something" "sees" "bear" "+"))
If something visits the tiger and it sees the bear then it is red.
((("something" "visits" "tiger" "+") ("something" "sees" "bear" "+")) -> ("something" "is" "red" "+"))
If something is green and it visits the dog then it visits the tiger.
((("something" "is" "green" "+") ("something" "visits" "dog" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the bear and the bear is green then it sees the cow.
((("something" "visits" "bear" "+") ("bear" "is" "green" "+")) -> ("something" "sees" "cow" "+"))
If something is green then it visits the tiger.
((("something" "is" "green" "+")) -> ("something" "visits" "tiger" "+"))
The dog sees the cow.
True
1
proof
[(triple5)]
("dog" "sees" "cow" "+")
triple5
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "sees" "cow" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The bear is rough.[(triple1)] The bear likes the tiger.[(triple2)] The bear visits the dog.[(triple3)] The cow likes the dog.[(triple4)] The dog sees the cow.[(triple5)] The tiger sees the bear.[(triple6)] The tiger visits the dog.[(triple7)]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The cow likes the dog.
("cow" "likes" "dog" "+")
triple4
The dog sees the cow.
("dog" "sees" "cow" "+")
triple5
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple6
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple7