The bear is big. The bear is cold. The bear is green. The bear is kind. The lion chases the rabbit. The lion eats the bear. The lion is cold. The lion is kind. The rabbit eats the lion. The rabbit likes the bear. If someone eats the lion then the lion likes the rabbit. If someone eats the lion then they are kind. If someone is round and they like the bear then the bear chases the rabbit. If the bear likes the lion and the bear is not big then the bear does not eat the rabbit. If someone chases the lion then the lion eats the rabbit. If someone likes the rabbit then the rabbit is round.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If someone eats the lion then the lion likes the rabbit.
((("someone" "eats" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If someone eats the lion then they are kind.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and they like the bear then the bear chases the rabbit.
((("someone" "is" "round" "+") ("someone" "likes" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If the bear likes the lion and the bear is not big then the bear does not eat the rabbit.
((("bear" "likes" "lion" "+") ("bear" "is" "big" "~")) -> ("bear" "eats" "rabbit" "-"))
If someone chases the lion then the lion eats the rabbit.
((("someone" "chases" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone likes the rabbit then the rabbit is round.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
The bear is green.
True
1
proof
[(triple3)]
("bear" "is" "green" "+")
triple3
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The rabbit is kind.
True
2
proof
[(((triple9) -> rule2))]
("rabbit" "is" "kind" "+")
((triple9) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The lion does not like the rabbit.
False
2
inv-proof
[(((triple9) -> rule1))]
("lion" "likes" "rabbit" "-")
((triple9) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple9) -> rule1)) -> rule6))]
("rabbit" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule6))]
("rabbit" "is" "round" "-")
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The lion does not eat the rabbit.
Unknown
inv-rconc
[@1: The lion eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The bear does not eat the rabbit.
Unknown
inv-random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The rabbit does not chase the bear.
Unknown
inv-random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "-")
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 is big.[(triple1)] The bear is cold.[(triple2)] The bear is green.[(triple3)] The bear is kind.[(triple4)] The lion chases the rabbit.[(triple5)] The lion eats the bear.[(triple6)] The lion is cold.[(triple7)] The lion is kind.[(triple8)] The rabbit eats the lion.[(triple9)] The rabbit likes the bear.[(triple10)] @1: The lion likes the rabbit.[(((triple9) -> rule1))] The rabbit is kind.[(((triple9) -> rule2))] @2: The rabbit is round.[(((((triple9) -> rule1)) -> rule6))] @3: The bear chases the rabbit.[(((((((triple9) -> rule1)) -> rule6) triple10) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is kind.
("bear" "is" "kind" "+")
triple4
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple5
The lion eats the bear.
("lion" "eats" "bear" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
triple8
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple9
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((triple9) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple9) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
((((((triple9) -> (rule1 % int3))) -> (rule6 % int2)) triple10) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3