The cat chases the rabbit. The cat is nice. The rabbit does not chase the cat. The rabbit is kind. The rabbit is rough. The rabbit is round. The rabbit likes the cat. If something likes the cat and the cat visits the rabbit then the cat likes the rabbit. If something is rough then it likes the rabbit.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is nice.
("cat" "is" "nice" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
If something likes the cat and the cat visits the rabbit then the cat likes the rabbit.
((("something" "likes" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("cat" "likes" "rabbit" "+"))
If something is rough then it likes the rabbit.
((("something" "is" "rough" "+")) -> ("something" "likes" "rabbit" "+"))
The cat chases the rabbit.
True
1
proof
[(triple1)]
("cat" "chases" "rabbit" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "kind" "-")
triple4
The rabbit likes the rabbit.
True
2
proof
[(((triple5) -> rule2))]
("rabbit" "likes" "rabbit" "+")
((triple5) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple5) -> rule2))]
("rabbit" "likes" "rabbit" "-")
((triple5) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The cat does not like the rabbit.
Unknown
inv-rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "rabbit" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is nice.[(triple2)] The rabbit does not chase the cat.[(triple3)] The rabbit is kind.[(triple4)] The rabbit is rough.[(triple5)] The rabbit is round.[(triple6)] The rabbit likes the cat.[(triple7)] @1: The rabbit likes the rabbit.[(((triple5) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple7
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple5) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1