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