The bear is round. The rabbit likes the bear. If someone likes the bear then they eat the bear. If someone needs the bear then they are blue. If someone eats the bear then they need the rabbit.
The bear is round.
("bear" "is" "round" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If someone likes the bear then they eat the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone needs the bear then they are blue.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the bear then they need the rabbit.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "rabbit" "+"))
The rabbit likes the bear.
True
1
proof
[(triple2)]
("rabbit" "likes" "bear" "+")
triple2
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The rabbit eats the bear.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "eats" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit does not eat the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "eats" "bear" "-")
((triple2) -> (rule1 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit needs the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("rabbit" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit does not need the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("rabbit" "needs" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The bear does not need the rabbit.
Unknown
inv-rconc
[@2: The bear needs the rabbit.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "+")
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "blue" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
@0: The bear is round.[(triple1)] The rabbit likes the bear.[(triple2)] @1: The rabbit eats the bear.[(((triple2) -> rule1))] @2: The rabbit needs the rabbit.[(((((triple2) -> rule1)) -> rule3))]
The bear is round.
("bear" "is" "round" "+")
triple1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2