The bear is kind. The bear does not need the rabbit. The bear sees the rabbit. The lion sees the rabbit. The lion visits the bear. The rabbit is cold. The rabbit is round. The rabbit is young. The rabbit sees the bear. The rabbit sees the lion. If someone needs the bear and the bear is kind then they are young. If someone is kind then they need the bear. If someone sees the lion and they do not visit the lion then the lion does not need the rabbit. If someone needs the lion and they do not see the bear then they see the lion. If someone visits the lion and they are round then they see the lion. If the lion sees the rabbit and the rabbit is round then the rabbit is cold. If someone is young and cold then they need the rabbit. If someone is young then they are round.
The bear is kind.
("bear" "is" "kind" "+")
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone needs the bear and the bear is kind then they are young.
((("someone" "needs" "bear" "+") ("bear" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they need the bear.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the lion and they do not visit the lion then the lion does not need the rabbit.
((("someone" "sees" "lion" "+") ("someone" "visits" "lion" "~")) -> ("lion" "needs" "rabbit" "-"))
If someone needs the lion and they do not see the bear then they see the lion.
((("someone" "needs" "lion" "+") ("someone" "sees" "bear" "~")) -> ("someone" "sees" "lion" "+"))
If someone visits the lion and they are round then they see the lion.
((("someone" "visits" "lion" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "lion" "+"))
If the lion sees the rabbit and the rabbit is round then the rabbit is cold.
((("lion" "sees" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is young and cold then they need the rabbit.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
The rabbit sees the bear.
True
1
proof
[(triple9)]
("rabbit" "sees" "bear" "+")
triple9
The bear does not see the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "sees" "rabbit" "-")
triple3
The bear needs the bear.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is young.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("bear" "is" "young" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is not young.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("bear" "is" "young" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is round.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule1)) -> rule8))]
("bear" "is" "round" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The bear is not round.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule1)) -> rule8))]
("bear" "is" "round" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The rabbit does not need the bear.
Unknown
inv-rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "bear" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "lion" "+")
The lion is not young.
Unknown
inv-rconc
[@2: The lion is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "is" "young" "-")
The lion needs the bear.
Unknown
rconc
[@1: The lion needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "bear" "+")
The lion does not visit the rabbit.
Unknown
inv-random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "-")
The lion sees the bear.
Unknown
random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "+")
The rabbit does not need the lion.
Unknown
inv-random
[@0: The rabbit needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "lion" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear does not need the rabbit.[(triple2)] The bear is kind.[(triple1)] The bear sees the rabbit.[(triple3)] The lion sees the rabbit.[(triple4)] The lion visits the bear.[(triple5)] The rabbit is cold.[(triple6 OR ((triple4 triple7) -> rule6) OR ((triple4 ((triple8) -> rule8)) -> rule6))] The rabbit is round.[(triple7 OR ((triple8) -> rule8))] The rabbit is young.[(triple8)] The rabbit sees the bear.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The bear needs the bear.[(((triple1) -> rule2))] The rabbit needs the rabbit.[(((triple8 triple6) -> rule7) OR ((triple8 ((triple4 triple7) -> rule6)) -> rule7) OR ((triple8 ((triple4 ((triple8) -> rule8)) -> rule6)) -> rule7))] @2: The bear is young.[(((((triple1) -> rule2) triple1) -> rule1))] @3: The bear is round.[(((((((triple1) -> rule2) triple1) -> rule1)) -> rule8))]
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The lion visits the bear.
("lion" "visits" "bear" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
((triple4 triple7) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple4 ((triple8) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
((triple8) -> (rule8 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple8 triple6) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((triple8 ((triple4 triple7) -> (rule6 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
((triple8 ((triple4 ((triple8) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bear is young.
("bear" "is" "young" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3