The bald eagle likes the cat. The bear is rough. The cat likes the rabbit. The rabbit likes the bald eagle. If someone likes the bear then the bear visits the bald eagle. If someone needs the cat then they are rough. If someone needs the bald eagle then the bald eagle needs the cat. If someone visits the rabbit and the rabbit is round then they are red. If someone likes the rabbit then they need the bald eagle. If someone is nice and cold then they need the bald eagle.
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bear is rough.
("bear" "is" "rough" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
If someone likes the bear then the bear visits the bald eagle.
((("someone" "likes" "bear" "+")) -> ("bear" "visits" "bald eagle" "+"))
If someone needs the cat then they are rough.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the bald eagle then the bald eagle needs the cat.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "cat" "+"))
If someone visits the rabbit and the rabbit is round then they are red.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone likes the rabbit then they need the bald eagle.
((("someone" "likes" "rabbit" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone is nice and cold then they need the bald eagle.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "bald eagle" "+"))
The cat likes the rabbit.
True
1
proof
[(triple3)]
("cat" "likes" "rabbit" "+")
triple3
The bald eagle does not like the cat.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "cat" "-")
triple1
The cat needs the bald eagle.
True
2
proof
[(((triple3) -> rule5))]
("cat" "needs" "bald eagle" "+")
((triple3) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The cat does not need the bald eagle.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "needs" "bald eagle" "-")
((triple3) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The bald eagle needs the cat.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("bald eagle" "needs" "cat" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The bald eagle does not need the cat.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("bald eagle" "needs" "cat" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The bald eagle is rough.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("bald eagle" "is" "rough" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
int1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3
The bald eagle is not rough.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("bald eagle" "is" "rough" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
int1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "red" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "red" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "+")
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 likes the cat.
Unknown
random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bald eagle likes the cat.[(triple1)] The bear is rough.[(triple2)] The cat likes the rabbit.[(triple3)] The rabbit likes the bald eagle.[(triple4)] @1: The cat needs the bald eagle.[(((triple3) -> rule5))] @2: The bald eagle needs the cat.[(((((triple3) -> rule5)) -> rule3))] @3: The bald eagle is rough.[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
triple4
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
((triple3) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
int1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3