The bald eagle likes the cow. The cow sees the bald eagle. If the bald eagle likes the cow then the bald eagle sees the cow. If something needs the cow and it likes the bald eagle then it is big. If something sees the cow and it likes the cow then it needs the cow.
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
If the bald eagle likes the cow then the bald eagle sees the cow.
((("bald eagle" "likes" "cow" "+")) -> ("bald eagle" "sees" "cow" "+"))
If something needs the cow and it likes the bald eagle then it is big.
((("something" "needs" "cow" "+") ("something" "likes" "bald eagle" "+")) -> ("something" "is" "big" "+"))
If something sees the cow and it likes the cow then it needs the cow.
((("something" "sees" "cow" "+") ("something" "likes" "cow" "+")) -> ("something" "needs" "cow" "+"))
The bald eagle likes the cow.
True
1
proof
[(triple1)]
("bald eagle" "likes" "cow" "+")
triple1
The cow does not see the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "sees" "bald eagle" "-")
triple2
The bald eagle sees the cow.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "sees" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle does not see the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("bald eagle" "sees" "cow" "-")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle needs the cow.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule3))]
("bald eagle" "needs" "cow" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2
The bald eagle does not need the cow.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule3))]
("bald eagle" "needs" "cow" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "+")
The bald eagle is not big.
Unknown
inv-rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "big" "-")
The bald eagle is kind.
Unknown
random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "+")
The bald eagle does not like the bald eagle.
Unknown
inv-random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The bald eagle likes the cow.[(triple1)] The cow sees the bald eagle.[(triple2)] @1: The bald eagle sees the cow.[(((triple1) -> rule1))] @2: The bald eagle needs the cow.[(((((triple1) -> rule1) triple1) -> rule3))]
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
triple1
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2