The bald eagle likes the bear. The bear likes the cow. The cat is round. The cat is young. The cat likes the bald eagle. The cat likes the bear. The cow is blue. If someone visits the bald eagle then they like the bald eagle. If someone likes the cat then they need the cow. If the cat visits the cow then the cat is blue. If someone needs the cow then they like the cow. If someone is round then they like the cat. If someone visits the cow then they visit the bear.
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cow is blue.
("cow" "is" "blue" "+")
If someone visits the bald eagle then they like the bald eagle.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "likes" "bald eagle" "+"))
If someone likes the cat then they need the cow.
((("someone" "likes" "cat" "+")) -> ("someone" "needs" "cow" "+"))
If the cat visits the cow then the cat is blue.
((("cat" "visits" "cow" "+")) -> ("cat" "is" "blue" "+"))
If someone needs the cow then they like the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone is round then they like the cat.
((("someone" "is" "round" "+")) -> ("someone" "likes" "cat" "+"))
If someone visits the cow then they visit the bear.
((("someone" "visits" "cow" "+")) -> ("someone" "visits" "bear" "+"))
The cat is round.
True
1
proof
[(triple3)]
("cat" "is" "round" "+")
triple3
The bear does not like the cow.
False
1
inv-proof
[(triple2)]
("bear" "likes" "cow" "-")
triple2
The cat likes the cat.
True
2
proof
[(((triple3) -> rule5))]
("cat" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "likes" "cat" "-")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the cow.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("cat" "needs" "cow" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat does not need the cow.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("cat" "needs" "cow" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
True
4
proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule4))]
("cat" "likes" "cow" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat does not like the cow.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule4))]
("cat" "likes" "cow" "-")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cow does not visit the bear.
Unknown
inv-rconc
[@1: The cow visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "visits" "bear" "-")
The cat is blue.
Unknown
rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "blue" "+")
The bear does not need the cow.
Unknown
inv-rconc
[@2: The bear needs the cow.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("bear" "needs" "cow" "-")
The bald eagle needs the cow.
Unknown
rconc
[@2: The bald eagle needs the cow.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("bald eagle" "needs" "cow" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
The bald eagle is not round.
Unknown
inv-random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
@0: The bald eagle likes the bear.[(triple1)] The bear likes the cow.[(triple2)] The cat is round.[(triple3)] The cat is young.[(triple4)] The cat likes the bald eagle.[(triple5)] The cat likes the bear.[(triple6)] The cow is blue.[(triple7)] @1: The cat likes the cat.[(((triple3) -> rule5))] @2: The cat needs the cow.[(((((triple3) -> rule5)) -> rule2))] @3: The cat likes the cow.[(((((((triple3) -> rule5)) -> rule2)) -> rule4))]
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple1
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple5
The cat likes the bear.
("cat" "likes" "bear" "+")
triple6
The cow is blue.
("cow" "is" "blue" "+")
triple7
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3