The bear sees the rabbit. The rabbit chases the bear. The squirrel is rough. If someone sees the bear then the bear sees the rabbit. If the rabbit is kind then the rabbit visits the bear. If someone is rough then they chase the bear. If the bear is rough and the bear chases the rabbit then the rabbit sees the bear. If someone visits the squirrel and they are kind then they are round. If someone visits the squirrel and the squirrel chases the rabbit then they chase the rabbit. If someone visits the bear then they are round. If someone sees the rabbit then they visit the rabbit.
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone sees the bear then the bear sees the rabbit.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "rabbit" "+"))
If the rabbit is kind then the rabbit visits the bear.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "visits" "bear" "+"))
If someone is rough then they chase the bear.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "bear" "+"))
If the bear is rough and the bear chases the rabbit then the rabbit sees the bear.
((("bear" "is" "rough" "+") ("bear" "chases" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If someone visits the squirrel and they are kind then they are round.
((("someone" "visits" "squirrel" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone visits the squirrel and the squirrel chases the rabbit then they chase the rabbit.
((("someone" "visits" "squirrel" "+") ("squirrel" "chases" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone visits the bear then they are round.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone sees the rabbit then they visit the rabbit.
((("someone" "sees" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
The rabbit chases the bear.
True
1
proof
[(triple2)]
("rabbit" "chases" "bear" "+")
triple2
The bear does not see the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "sees" "rabbit" "-")
triple1
The bear visits the rabbit.
True
2
proof
[(((triple1) -> rule8))]
("bear" "visits" "rabbit" "+")
((triple1) -> (rule8 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The squirrel does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "chases" "bear" "-")
((triple3) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The squirrel chases the rabbit.
Unknown
rconc
[@1: The squirrel chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "chases" "rabbit" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear sees the rabbit.[(triple1)] The rabbit chases the bear.[(triple2)] The squirrel is rough.[(triple3)] @1: The bear visits the rabbit.[(((triple1) -> rule8))] The squirrel chases the bear.[(((triple3) -> rule3))]
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
((triple1) -> (rule8 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((triple3) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1