The bear does not like the lion. The lion is not rough. The lion sees the squirrel. The lion visits the squirrel. The rabbit is round. The rabbit does not see the squirrel. The squirrel visits the bear. If someone visits the squirrel then the squirrel likes the rabbit. If someone sees the lion and the lion is not young then they do not see the bear. If the lion sees the rabbit and the lion likes the rabbit then the lion does not visit the rabbit.
The bear does not like the lion.
("bear" "likes" "lion" "-")
The lion is not rough.
("lion" "is" "rough" "-")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone visits the squirrel then the squirrel likes the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone sees the lion and the lion is not young then they do not see the bear.
((("someone" "sees" "lion" "+") ("lion" "is" "young" "~")) -> ("someone" "sees" "bear" "-"))
If the lion sees the rabbit and the lion likes the rabbit then the lion does not visit the rabbit.
((("lion" "sees" "rabbit" "+") ("lion" "likes" "rabbit" "+")) -> ("lion" "visits" "rabbit" "-"))
The rabbit is round.
True
1
proof
[(triple5)]
("rabbit" "is" "round" "+")
triple5
The rabbit is not round.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "round" "-")
triple5
The squirrel likes the rabbit.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "likes" "rabbit" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel does not like the rabbit.
False
2
inv-proof
[(((triple4) -> rule1))]
("squirrel" "likes" "rabbit" "-")
((triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The lion does not like the rabbit.
Unknown
inv-random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The rabbit does not like the lion.
Unknown
inv-random
[@0: The rabbit likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "lion" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
@0: The bear does not like the lion.[(triple1)] The lion is not rough.[(triple2)] The lion sees the squirrel.[(triple3)] The lion visits the squirrel.[(triple4)] The rabbit does not see the squirrel.[(triple6)] The rabbit is round.[(triple5)] The squirrel visits the bear.[(triple7)] @1: The squirrel likes the rabbit.[(((triple4) -> rule1))]
The bear does not like the lion.
("bear" "likes" "lion" "-")
triple1
The lion is not rough.
("lion" "is" "rough" "-")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple4
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple7
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1