The bald eagle visits the cow. The cow sees the bald eagle. The tiger visits the cow. If something is red then it chases the tiger. If something sees the bald eagle and the bald eagle visits the cow then it visits the bald eagle. If something visits the cow and it is not red then it chases the bald eagle.
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is red then it chases the tiger.
((("something" "is" "red" "+")) -> ("something" "chases" "tiger" "+"))
If something sees the bald eagle and the bald eagle visits the cow then it visits the bald eagle.
((("something" "sees" "bald eagle" "+") ("bald eagle" "visits" "cow" "+")) -> ("something" "visits" "bald eagle" "+"))
If something visits the cow and it is not red then it chases the bald eagle.
((("something" "visits" "cow" "+") ("something" "is" "red" "~")) -> ("something" "chases" "bald eagle" "+"))
The bald eagle visits the cow.
True
1
proof
[(triple1)]
("bald eagle" "visits" "cow" "+")
triple1
The bald eagle does not visit the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "cow" "-")
triple1
The cow visits the bald eagle.
True
3
proof
[(((triple2 triple1) -> rule2))]
("cow" "visits" "bald eagle" "+")
((triple2 triple1) -> (rule2 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow does not visit the bald eagle.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("cow" "visits" "bald eagle" "-")
((triple2 triple1) -> (rule2 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow does not chase the bald eagle.
Unknown
inv-rconc
[@1: The cow chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "bald eagle" "-")
The tiger visits the bald eagle.
Unknown
rconc
[@1: The tiger visits the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "bald eagle" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bald eagle visits the cow.[(triple1)] The cow sees the bald eagle.[(triple2)] The tiger visits the cow.[(triple3)] @1: The cow visits the bald eagle.[(((triple2 triple1) -> rule2))]
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
triple1
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple3
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
((triple2 triple1) -> (rule2 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1