The bear does not chase the lion. The bear is cold. The bear is red. The bear likes the lion. The cat chases the rabbit. The cat is nice. The cat sees the bear. The cat sees the lion. The lion chases the bear. The rabbit likes the bear. If the cat chases the rabbit then the cat is nice. If the rabbit likes the cat then the cat sees the rabbit. If someone sees the lion then they chase the rabbit. If someone is cold then they chase the cat. If someone chases the cat and they like the lion then they like the cat. If someone sees the lion and they do not like the cat then the cat is rough.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If the cat chases the rabbit then the cat is nice.
((("cat" "chases" "rabbit" "+")) -> ("cat" "is" "nice" "+"))
If the rabbit likes the cat then the cat sees the rabbit.
((("rabbit" "likes" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone sees the lion then they chase the rabbit.
((("someone" "sees" "lion" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone is cold then they chase the cat.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat and they like the lion then they like the cat.
((("someone" "chases" "cat" "+") ("someone" "likes" "lion" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the lion and they do not like the cat then the cat is rough.
((("someone" "sees" "lion" "+") ("someone" "likes" "cat" "~")) -> ("cat" "is" "rough" "+"))
The cat chases the rabbit.
True
1
proof
[(triple5 OR ((triple8) -> rule3))]
("cat" "chases" "rabbit" "+")
triple5
((triple8) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat does not chase the rabbit.
False
1
inv-proof
[(triple5 OR ((triple8) -> rule3))]
("cat" "chases" "rabbit" "-")
triple5
((triple8) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The bear chases the cat.
True
2
proof
[(((triple2) -> rule4))]
("bear" "chases" "cat" "+")
((triple2) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear does not chase the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("bear" "chases" "cat" "-")
((triple2) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear likes the cat.
True
4
proof
[(((((triple2) -> rule4) triple4) -> rule5))]
("bear" "likes" "cat" "+")
((((triple2) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear does not like the cat.
False
4
inv-proof
[(((((triple2) -> rule4) triple4) -> rule5))]
("bear" "likes" "cat" "-")
((((triple2) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "rough" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cat" "+")
The lion does not like the cat.
Unknown
inv-rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "likes" "cat" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The lion does not see the rabbit.
Unknown
inv-random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The bear does not chase the lion.[(triple1)] The bear is cold.[(triple2)] The bear is red.[(triple3)] The bear likes the lion.[(triple4)] The cat chases the rabbit.[(triple5 OR ((triple8) -> rule3))] The cat is nice.[(triple6 OR ((triple5) -> rule1) OR ((((triple8) -> rule3)) -> rule1))] The cat sees the bear.[(triple7)] The cat sees the lion.[(triple8)] The lion chases the bear.[(triple9)] The rabbit likes the bear.[(triple10)] @1: The bear chases the cat.[(((triple2) -> rule4))] @2: The bear likes the cat.[(((((triple2) -> rule4) triple4) -> rule5))]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear likes the lion.
("bear" "likes" "lion" "+")
triple4
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple5
((triple8) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
triple7
The cat sees the lion.
("cat" "sees" "lion" "+")
triple8
The lion chases the bear.
("lion" "chases" "bear" "+")
triple9
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
The bear chases the cat.
("bear" "chases" "cat" "+")
((triple2) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
((((triple2) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2