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