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