The bear is big. The lion visits the rabbit. The rabbit is blue. The squirrel sees the rabbit. If the rabbit is green then the rabbit visits the bear. If someone likes the rabbit then the rabbit sees the squirrel. If someone visits the rabbit then the rabbit is green. If the rabbit sees the bear and the rabbit sees the squirrel then the rabbit likes the lion. If the rabbit likes the squirrel then the squirrel likes the lion. If someone is rough then they visit the bear. If someone sees the bear and the bear sees the rabbit then the rabbit visits the lion. If someone sees the squirrel then they visit the rabbit.
The bear is big.
("bear" "is" "big" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If the rabbit is green then the rabbit visits the bear.
((("rabbit" "is" "green" "+")) -> ("rabbit" "visits" "bear" "+"))
If someone likes the rabbit then the rabbit sees the squirrel.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone visits the rabbit then the rabbit is green.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If the rabbit sees the bear and the rabbit sees the squirrel then the rabbit likes the lion.
((("rabbit" "sees" "bear" "+") ("rabbit" "sees" "squirrel" "+")) -> ("rabbit" "likes" "lion" "+"))
If the rabbit likes the squirrel then the squirrel likes the lion.
((("rabbit" "likes" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If someone is rough then they visit the bear.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "bear" "+"))
If someone sees the bear and the bear sees the rabbit then the rabbit visits the lion.
((("someone" "sees" "bear" "+") ("bear" "sees" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
If someone sees the squirrel then they visit the rabbit.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "rabbit" "+"))
The squirrel sees the rabbit.
True
1
proof
[(triple4)]
("squirrel" "sees" "rabbit" "+")
triple4
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple4)]
("squirrel" "sees" "rabbit" "-")
triple4
The rabbit is green.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "is" "green" "+")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "is" "green" "-")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not visit the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "visits" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "bear" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "bear" "+")
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
The lion does not like the squirrel.
Unknown
inv-random
[@0: The lion likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "squirrel" "-")
The lion likes the bear.
Unknown
random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "+")
@0: The bear is big.[(triple1)] The lion visits the rabbit.[(triple2)] The rabbit is blue.[(triple3)] The squirrel sees the rabbit.[(triple4)] @1: The rabbit is green.[(((triple2) -> rule3))] @2: The rabbit visits the bear.[(((((triple2) -> rule3)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple4
The rabbit is green.
("rabbit" "is" "green" "+")
((triple2) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2