The bald eagle is blue. The cat is blue. The rabbit likes the bald eagle. If something likes the rabbit and the rabbit is young then it sees the cat. If the rabbit visits the bald eagle and the bald eagle visits the cat then the cat likes the rabbit. If something likes the rabbit then the rabbit sees the cat. If something sees the bald eagle then the bald eagle visits the rabbit. If the rabbit visits the bald eagle and the rabbit is rough then the bald eagle is nice. If something likes the bald eagle then it likes the rabbit.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The cat is blue.
("cat" "is" "blue" "+")
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
If something likes the rabbit and the rabbit is young then it sees the cat.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("something" "sees" "cat" "+"))
If the rabbit visits the bald eagle and the bald eagle visits the cat then the cat likes the rabbit.
((("rabbit" "visits" "bald eagle" "+") ("bald eagle" "visits" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If something likes the rabbit then the rabbit sees the cat.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something sees the bald eagle then the bald eagle visits the rabbit.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "visits" "rabbit" "+"))
If the rabbit visits the bald eagle and the rabbit is rough then the bald eagle is nice.
((("rabbit" "visits" "bald eagle" "+") ("rabbit" "is" "rough" "+")) -> ("bald eagle" "is" "nice" "+"))
If something likes the bald eagle then it likes the rabbit.
((("something" "likes" "bald eagle" "+")) -> ("something" "likes" "rabbit" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The cat is not blue.
False
1
inv-proof
[(triple2)]
("cat" "is" "blue" "-")
triple2
The rabbit likes the rabbit.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the cat.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("rabbit" "sees" "cat" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit does not see the cat.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("rabbit" "sees" "cat" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The bald eagle does not see the cat.
Unknown
inv-rconc
[@1: The bald eagle sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "sees" "cat" "-")
The bald eagle visits the rabbit.
Unknown
rconc
[@1: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "visits" "rabbit" "+")
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bald eagle visits the cat.
Unknown
random
[@0: The bald eagle visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "cat" "+")
@0: The bald eagle is blue.[(triple1)] The cat is blue.[(triple2)] The rabbit likes the bald eagle.[(triple3)] @1: The rabbit likes the rabbit.[(((triple3) -> rule6))] @2: The rabbit sees the cat.[(((((triple3) -> rule6)) -> rule3))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
triple3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2