The cat is green. The cat is kind. The cat is round. The cat sees the rabbit. The rabbit is cold. The rabbit is red. The rabbit is not round. The rabbit likes the cat. The rabbit needs the cat. The rabbit sees the cat. If someone likes the cat and they are red then the cat is red. If someone likes the rabbit and the rabbit sees the cat then the rabbit likes the cat. If someone is kind then they like the rabbit.
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If someone likes the cat and they are red then the cat is red.
((("someone" "likes" "cat" "+") ("someone" "is" "red" "+")) -> ("cat" "is" "red" "+"))
If someone likes the rabbit and the rabbit sees the cat then the rabbit likes the cat.
((("someone" "likes" "rabbit" "+") ("rabbit" "sees" "cat" "+")) -> ("rabbit" "likes" "cat" "+"))
If someone is kind then they like the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "rabbit" "+"))
The rabbit likes the cat.
True
1
proof
[(triple8 OR ((((triple2) -> rule3) triple10) -> rule2))]
("rabbit" "likes" "cat" "+")
triple8
((((triple2) -> (rule3 % int2)) triple10) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit does not see the cat.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "cat" "-")
triple10
The cat is red.
True
3
proof
[(((triple8 triple6) -> rule1) OR ((((((triple2) -> rule3) triple10) -> rule2) triple6) -> rule1))]
("cat" "is" "red" "+")
((triple8 triple6) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((((triple2) -> (rule3 % int3)) triple10) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The cat does not like the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "likes" "rabbit" "-")
((triple2) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The cat is green.[(triple1)] The cat is kind.[(triple2)] The cat is round.[(triple3)] The cat sees the rabbit.[(triple4)] The rabbit is cold.[(triple5)] The rabbit is not round.[(triple7)] The rabbit is red.[(triple6)] The rabbit likes the cat.[(triple8 OR ((((triple2) -> rule3) triple10) -> rule2))] The rabbit needs the cat.[(triple9)] The rabbit sees the cat.[(triple10)] @1: The cat is red.[(((triple8 triple6) -> rule1) OR ((((((triple2) -> rule3) triple10) -> rule2) triple6) -> rule1))] The cat likes the rabbit.[(((triple2) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit is not round.
("rabbit" "is" "round" "-")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple8
((((triple2) -> (rule3 % int2)) triple10) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple9
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple10
The cat is red.
("cat" "is" "red" "+")
((triple8 triple6) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((((triple2) -> (rule3 % int3)) triple10) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple2) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1