The bald eagle is young. The cat is nice. The cat is young. The cat likes the rabbit. The lion likes the rabbit. The lion sees the rabbit. The rabbit chases the bald eagle. The rabbit does not chase the cat. The rabbit is not blue. The rabbit is green. The rabbit is red. The rabbit sees the lion. If something sees the cat then it sees the bald eagle. If something sees the bald eagle then the bald eagle chases the rabbit. If the lion likes the rabbit then the rabbit sees the cat.
The bald eagle is young.
("bald eagle" "is" "young" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something sees the cat then it sees the bald eagle.
((("something" "sees" "cat" "+")) -> ("something" "sees" "bald eagle" "+"))
If something sees the bald eagle then the bald eagle chases the rabbit.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "chases" "rabbit" "+"))
If the lion likes the rabbit then the rabbit sees the cat.
((("lion" "likes" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
The rabbit does not chase the cat.
True
1
proof
[(triple8)]
("rabbit" "chases" "cat" "-")
triple8
The cat does not like the rabbit.
False
1
inv-proof
[(triple4)]
("cat" "likes" "rabbit" "-")
triple4
The rabbit sees the cat.
True
2
proof
[(((triple5) -> rule3))]
("rabbit" "sees" "cat" "+")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
2
inv-proof
[(((triple5) -> rule3))]
("rabbit" "sees" "cat" "-")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit sees the bald eagle.
True
3
proof
[(((((triple5) -> rule3)) -> rule1))]
("rabbit" "sees" "bald eagle" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit does not see the bald eagle.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule1))]
("rabbit" "sees" "bald eagle" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The bald eagle chases the rabbit.
True
4
proof
[(((((((triple5) -> rule3)) -> rule1)) -> rule2))]
("bald eagle" "chases" "rabbit" "+")
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The bald eagle does not chase the rabbit.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule1)) -> rule2))]
("bald eagle" "chases" "rabbit" "-")
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cat does not see the bald eagle.
Unknown
inv-rconc
[@1: The cat sees the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "bald eagle" "-")
The bald eagle sees the bald eagle.
Unknown
rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
The lion does not see the bald eagle.
Unknown
inv-rconc
[@1: The lion sees the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "bald eagle" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The bald eagle sees the rabbit.
Unknown
random
[@0: The bald eagle sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "rabbit" "+")
@0: The bald eagle is young.[(triple1)] The cat is nice.[(triple2)] The cat is young.[(triple3)] The cat likes the rabbit.[(triple4)] The lion likes the rabbit.[(triple5)] The lion sees the rabbit.[(triple6)] The rabbit chases the bald eagle.[(triple7)] The rabbit does not chase the cat.[(triple8)] The rabbit is green.[(triple10)] The rabbit is not blue.[(triple9)] The rabbit is red.[(triple11)] The rabbit sees the lion.[(triple12)] @1: The rabbit sees the cat.[(((triple5) -> rule3))] @2: The rabbit sees the bald eagle.[(((((triple5) -> rule3)) -> rule1))] @3: The bald eagle chases the rabbit.[(((((((triple5) -> rule3)) -> rule1)) -> rule2))]
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
triple7
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3