The cat is cold. The cat is kind. The cat is rough. The cat likes the rabbit. The cat needs the rabbit. The cat visits the rabbit. The rabbit is cold. The rabbit is nice. The rabbit is red. The rabbit likes the cat. The rabbit needs the cat. The rabbit visits the cat. If something visits the cat then it needs the cat. If something needs the cat then the cat needs the rabbit.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something visits the cat then it needs the cat.
((("something" "visits" "cat" "+")) -> ("something" "needs" "cat" "+"))
If something needs the cat then the cat needs the rabbit.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
The rabbit needs the cat.
True
1
proof
[(triple11 OR ((triple12) -> rule1))]
("rabbit" "needs" "cat" "+")
triple11
((triple12) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat does not like the rabbit.
False
1
inv-proof
[(triple4)]
("cat" "likes" "rabbit" "-")
triple4
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat is rough.[(triple3)] The cat likes the rabbit.[(triple4)] The cat needs the rabbit.[(triple5 OR ((triple11) -> rule2) OR ((((triple12) -> rule1)) -> rule2))] The cat visits the rabbit.[(triple6)] The rabbit is cold.[(triple7)] The rabbit is nice.[(triple8)] The rabbit is red.[(triple9)] The rabbit likes the cat.[(triple10)] The rabbit needs the cat.[(triple11 OR ((triple12) -> rule1))] The rabbit visits the cat.[(triple12)]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple5
((triple11) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple10
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
((triple12) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple12