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