The bear is red. The bear does not like the rabbit. The rabbit is big. If the rabbit chases the bear then the rabbit is young. If someone chases the bear then the bear does not like the rabbit. If the bear is young then the bear likes the rabbit. If someone is big then they like the bear. If someone likes the rabbit then they like the bear. If someone likes the bear then the bear does not chase the rabbit.
The bear is red.
("bear" "is" "red" "+")
The bear does not like the rabbit.
("bear" "likes" "rabbit" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
If the rabbit chases the bear then the rabbit is young.
((("rabbit" "chases" "bear" "+")) -> ("rabbit" "is" "young" "+"))
If someone chases the bear then the bear does not like the rabbit.
((("someone" "chases" "bear" "+")) -> ("bear" "likes" "rabbit" "-"))
If the bear is young then the bear likes the rabbit.
((("bear" "is" "young" "+")) -> ("bear" "likes" "rabbit" "+"))
If someone is big then they like the bear.
((("someone" "is" "big" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the rabbit then they like the bear.
((("someone" "likes" "rabbit" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the bear then the bear does not chase the rabbit.
((("someone" "likes" "bear" "+")) -> ("bear" "chases" "rabbit" "-"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The rabbit is not big.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "big" "-")
triple3
The rabbit likes the bear.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "likes" "bear" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit does not like the bear.
False
2
inv-proof
[(((triple3) -> rule4))]
("rabbit" "likes" "bear" "-")
((triple3) -> (rule4 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear does not chase the rabbit.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("bear" "chases" "rabbit" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The bear chases the rabbit.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("bear" "chases" "rabbit" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "bear" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "young" "+")
The rabbit does not need the bear.
Unknown
inv-random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bear does not like the rabbit.[(triple2)] The bear is red.[(triple1)] The rabbit is big.[(triple3)] @1: The rabbit likes the bear.[(((triple3) -> rule4))] @2: The bear does not chase the rabbit.[(((((triple3) -> rule4)) -> rule6))]
The bear does not like the rabbit.
("bear" "likes" "rabbit" "-")
triple2
The bear is red.
("bear" "is" "red" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2