The cow is cold. The cow likes the rabbit. The cow does not visit the rabbit. The rabbit does not chase the cow. The rabbit is red. The rabbit likes the cow. The tiger is kind. If someone chases the rabbit then the rabbit likes the tiger. If someone is red and they like the cow then the cow does not visit the tiger. If someone visits the tiger and the tiger chases the rabbit then the tiger does not visit the cow. If someone visits the rabbit and they are kind then they are cold. If someone likes the tiger and they are red then they like the rabbit. If someone visits the rabbit then they do not visit the cow.
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone chases the rabbit then the rabbit likes the tiger.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If someone is red and they like the cow then the cow does not visit the tiger.
((("someone" "is" "red" "+") ("someone" "likes" "cow" "+")) -> ("cow" "visits" "tiger" "-"))
If someone visits the tiger and the tiger chases the rabbit then the tiger does not visit the cow.
((("someone" "visits" "tiger" "+") ("tiger" "chases" "rabbit" "+")) -> ("tiger" "visits" "cow" "-"))
If someone visits the rabbit and they are kind then they are cold.
((("someone" "visits" "rabbit" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the tiger and they are red then they like the rabbit.
((("someone" "likes" "tiger" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone visits the rabbit then they do not visit the cow.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "cow" "-"))
The rabbit is red.
True
1
proof
[(triple5)]
("rabbit" "is" "red" "+")
triple5
The rabbit does not like the cow.
False
1
inv-proof
[(triple6)]
("rabbit" "likes" "cow" "-")
triple6
The cow does not visit the tiger.
True
3
proof
[(((triple5 triple6) -> rule2))]
("cow" "visits" "tiger" "-")
((triple5 triple6) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow visits the tiger.
False
3
inv-proof
[(((triple5 triple6) -> rule2))]
("cow" "visits" "tiger" "+")
((triple5 triple6) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@2: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The cow does not visit the rabbit.[(triple3)] The cow is cold.[(triple1)] The cow likes the rabbit.[(triple2)] The rabbit does not chase the cow.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the cow.[(triple6)] The tiger is kind.[(triple7)] @1: The cow does not visit the tiger.[(((triple5 triple6) -> rule2))]
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
((triple5 triple6) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1