The bear eats the rabbit. The bear is red. The bear is round. The bear sees the rabbit. The bear visits the rabbit. The rabbit is kind. The rabbit sees the bear. If someone visits the rabbit then they do not eat the bear. If someone is green then they eat the bear. If someone eats the rabbit then the rabbit is green. If someone visits the rabbit then they see the rabbit. If someone is red then they see the bear. If someone is red and they do not visit the rabbit then the rabbit is not round. If someone sees the bear then the bear eats the rabbit. If someone visits the bear and they do not eat the rabbit then they are kind.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If someone visits the rabbit then they do not eat the bear.
((("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "bear" "-"))
If someone is green then they eat the bear.
((("someone" "is" "green" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the rabbit then the rabbit is green.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone visits the rabbit then they see the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is red then they see the bear.
((("someone" "is" "red" "+")) -> ("someone" "sees" "bear" "+"))
If someone is red and they do not visit the rabbit then the rabbit is not round.
((("someone" "is" "red" "+") ("someone" "visits" "rabbit" "~")) -> ("rabbit" "is" "round" "-"))
If someone sees the bear then the bear eats the rabbit.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "rabbit" "+"))
If someone visits the bear and they do not eat the rabbit then they are kind.
((("someone" "visits" "bear" "+") ("someone" "eats" "rabbit" "~")) -> ("someone" "is" "kind" "+"))
The rabbit is kind.
True
1
proof
[(triple6)]
("rabbit" "is" "kind" "+")
triple6
The bear does not see the rabbit.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule4))]
("bear" "sees" "rabbit" "-")
triple4
((triple5) -> (rule4 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit is green.
True
2
proof
[(((triple1) -> rule3) OR ((((triple7) -> rule7)) -> rule3) OR ((((((triple2) -> rule5)) -> rule7)) -> rule3))]
("rabbit" "is" "green" "+")
((triple1) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear does not see the bear.
False
2
inv-proof
[(((triple2) -> rule5))]
("bear" "sees" "bear" "-")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The rabbit eats the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2) OR ((((((((triple2) -> rule5)) -> rule7)) -> rule3)) -> rule2))]
("rabbit" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The rabbit does not eat the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2) OR ((((((((triple2) -> rule5)) -> rule7)) -> rule3)) -> rule2))]
("rabbit" "eats" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "kind" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The bear eats the rabbit.[(triple1 OR ((triple7) -> rule7) OR ((((triple2) -> rule5)) -> rule7))] The bear is red.[(triple2)] The bear is round.[(triple3)] The bear sees the rabbit.[(triple4 OR ((triple5) -> rule4))] The bear visits the rabbit.[(triple5)] The rabbit is kind.[(triple6)] The rabbit sees the bear.[(triple7)] @1: The bear does not eat the bear.[(((triple5) -> rule1))] The bear sees the bear.[(((triple2) -> rule5))] The rabbit is green.[(((triple1) -> rule3) OR ((((triple7) -> rule7)) -> rule3) OR ((((((triple2) -> rule5)) -> rule7)) -> rule3))] @2: The rabbit eats the bear.[(((((triple1) -> rule3)) -> rule2) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2) OR ((((((((triple2) -> rule5)) -> rule7)) -> rule3)) -> rule2))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
((triple7) -> (rule7 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
((triple5) -> (rule4 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple7
The bear does not eat the bear.
("bear" "eats" "bear" "-")
((triple5) -> (rule1 % int1))
The bear does not eat the bear.
("bear" "eats" "bear" "-")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple1) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
((((((((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4