The bald eagle chases the lion. The cow sees the bald eagle. The lion sees the cow. If something chases the bald eagle and it chases the lion then the bald eagle is red. If something sees the cow then it sees the bald eagle. If something is nice then it sees the bald eagle. If something eats the cow then it is blue. If something sees the cow then it is blue. If something eats the cow then it is young.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something chases the bald eagle and it chases the lion then the bald eagle is red.
((("something" "chases" "bald eagle" "+") ("something" "chases" "lion" "+")) -> ("bald eagle" "is" "red" "+"))
If something sees the cow then it sees the bald eagle.
((("something" "sees" "cow" "+")) -> ("something" "sees" "bald eagle" "+"))
If something is nice then it sees the bald eagle.
((("something" "is" "nice" "+")) -> ("something" "sees" "bald eagle" "+"))
If something eats the cow then it is blue.
((("something" "eats" "cow" "+")) -> ("something" "is" "blue" "+"))
If something sees the cow then it is blue.
((("something" "sees" "cow" "+")) -> ("something" "is" "blue" "+"))
If something eats the cow then it is young.
((("something" "eats" "cow" "+")) -> ("something" "is" "young" "+"))
The cow sees the bald eagle.
True
1
proof
[(triple2)]
("cow" "sees" "bald eagle" "+")
triple2
The bald eagle does not chase the lion.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "lion" "-")
triple1
The lion sees the bald eagle.
True
2
proof
[(((triple3) -> rule2))]
("lion" "sees" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion does not see the bald eagle.
False
2
inv-proof
[(((triple3) -> rule2))]
("lion" "sees" "bald eagle" "-")
((triple3) -> (rule2 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The bald eagle is not young.
Unknown
inv-rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "young" "-")
The bald eagle is blue.
Unknown
rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "blue" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
@0: The bald eagle chases the lion.[(triple1)] The cow sees the bald eagle.[(triple2)] The lion sees the cow.[(triple3)] @1: The lion is blue.[(((triple3) -> rule5))] The lion sees the bald eagle.[(((triple3) -> rule2))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple2
The lion sees the cow.
("lion" "sees" "cow" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
((triple3) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1