The bear does not visit the lion. The lion likes the squirrel. The squirrel likes the lion. If someone is blue then they do not chase the lion. If someone likes the bear then the bear is rough. If the lion chases the bear and the lion likes the bear then the bear is rough. If the lion is not rough then the lion does not visit the bear. If someone is green and not nice then they like the bear. If someone likes the squirrel then they like the bear. If someone visits the lion and they like the bear then they visit the squirrel. If someone visits the bear and they are not rough then the bear likes the lion.
The bear does not visit the lion.
("bear" "visits" "lion" "-")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If someone is blue then they do not chase the lion.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "lion" "-"))
If someone likes the bear then the bear is rough.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "rough" "+"))
If the lion chases the bear and the lion likes the bear then the bear is rough.
((("lion" "chases" "bear" "+") ("lion" "likes" "bear" "+")) -> ("bear" "is" "rough" "+"))
If the lion is not rough then the lion does not visit the bear.
((("lion" "is" "rough" "~")) -> ("lion" "visits" "bear" "-"))
If someone is green and not nice then they like the bear.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "likes" "bear" "+"))
If someone likes the squirrel then they like the bear.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "bear" "+"))
If someone visits the lion and they like the bear then they visit the squirrel.
((("someone" "visits" "lion" "+") ("someone" "likes" "bear" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the bear and they are not rough then the bear likes the lion.
((("someone" "visits" "bear" "+") ("someone" "is" "rough" "~")) -> ("bear" "likes" "lion" "+"))
The squirrel likes the lion.
True
1
proof
[(triple3)]
("squirrel" "likes" "lion" "+")
triple3
The lion does not like the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "likes" "squirrel" "-")
triple2
The lion likes the bear.
True
2
proof
[(((triple2) -> rule6))]
("lion" "likes" "bear" "+")
((triple2) -> (rule6 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion does not like the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "likes" "bear" "-")
((triple2) -> (rule6 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear is rough.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("bear" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear is not rough.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("bear" "is" "rough" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "bear" "+")
The squirrel does not like the bear.
Unknown
inv-rconc
[@1: The squirrel likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "bear" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The bear does not visit the lion.[(triple1)] The lion likes the squirrel.[(triple2)] The squirrel likes the lion.[(triple3)] @1: The lion likes the bear.[(((triple2) -> rule6))] @2: The bear is rough.[(((((triple2) -> rule6)) -> rule2))]
The bear does not visit the lion.
("bear" "visits" "lion" "-")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple3
The lion likes the bear.
("lion" "likes" "bear" "+")
((triple2) -> (rule6 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2