The bear likes the rabbit. The rabbit chases the bear. If someone likes the rabbit and they chase the bear then the rabbit is not big. If someone is kind then they visit the rabbit. If someone is red then they chase the bear. If someone chases the bear then the bear is red. If someone likes the rabbit and the rabbit chases the bear then the rabbit is kind. If someone visits the rabbit then the rabbit is not nice. If someone visits the bear and the bear visits the rabbit then the bear chases the rabbit. If the rabbit visits the bear and the rabbit does not chase the bear then the bear does not visit the rabbit.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If someone likes the rabbit and they chase the bear then the rabbit is not big.
((("someone" "likes" "rabbit" "+") ("someone" "chases" "bear" "+")) -> ("rabbit" "is" "big" "-"))
If someone is kind then they visit the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is red then they chase the bear.
((("someone" "is" "red" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the bear then the bear is red.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "red" "+"))
If someone likes the rabbit and the rabbit chases the bear then the rabbit is kind.
((("someone" "likes" "rabbit" "+") ("rabbit" "chases" "bear" "+")) -> ("rabbit" "is" "kind" "+"))
If someone visits the rabbit then the rabbit is not nice.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "nice" "-"))
If someone visits the bear and the bear visits the rabbit then the bear chases the rabbit.
((("someone" "visits" "bear" "+") ("bear" "visits" "rabbit" "+")) -> ("bear" "chases" "rabbit" "+"))
If the rabbit visits the bear and the rabbit does not chase the bear then the bear does not visit the rabbit.
((("rabbit" "visits" "bear" "+") ("rabbit" "chases" "bear" "~")) -> ("bear" "visits" "rabbit" "-"))
The rabbit chases the bear.
True
1
proof
[(triple2)]
("rabbit" "chases" "bear" "+")
triple2
The rabbit does not chase the bear.
False
1
inv-proof
[(triple2)]
("rabbit" "chases" "bear" "-")
triple2
The rabbit is kind.
True
3
proof
[(((triple1 triple2) -> rule5))]
("rabbit" "is" "kind" "+")
((triple1 triple2) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("rabbit" "is" "kind" "-")
((triple1 triple2) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the rabbit.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is not nice.
True
5
proof
[(((((((triple1 triple2) -> rule5)) -> rule2)) -> rule6))]
("rabbit" "is" "nice" "-")
((((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The rabbit is nice.
False
5
inv-proof
[(((((((triple1 triple2) -> rule5)) -> rule2)) -> rule6))]
("rabbit" "is" "nice" "+")
((((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The bear does not chase the rabbit.
Unknown
inv-rconc
[@1: The bear chases the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "rabbit" "-")
The bear visits the rabbit.
Unknown
rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "visits" "rabbit" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear likes the rabbit.[(triple1)] The rabbit chases the bear.[(triple2)] @1: The bear is red.[(((triple2) -> rule4))] The rabbit is kind.[(((triple1 triple2) -> rule5))] @2: The bear chases the bear.[(((((triple2) -> rule4)) -> rule3))] The rabbit visits the rabbit.[(((((triple1 triple2) -> rule5)) -> rule2))] @3: The rabbit is not big.[(((triple1 ((((triple2) -> rule4)) -> rule3)) -> rule1))] The rabbit is not nice.[(((((((triple1 triple2) -> rule5)) -> rule2)) -> rule6))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
((triple2) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple1 triple2) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is not big.
("rabbit" "is" "big" "-")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3