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