The bald eagle chases the cow. The bald eagle is not round. The bald eagle sees the cow. The bald eagle sees the lion. The cat sees the lion. The cow is blue. The lion sees the cat. If something chases the lion then it chases the bald eagle. If something chases the bald eagle then the bald eagle sees the lion. If the bald eagle is big and the bald eagle sees the cow then the bald eagle does not chase the lion. If something sees the cow then the cow chases the bald eagle. If something is big then it sees the cat. If something sees the lion and the lion visits the bald eagle then it is not nice.
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
The bald eagle is not round.
("bald eagle" "is" "round" "-")
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cow is blue.
("cow" "is" "blue" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something chases the lion then it chases the bald eagle.
((("something" "chases" "lion" "+")) -> ("something" "chases" "bald eagle" "+"))
If something chases the bald eagle then the bald eagle sees the lion.
((("something" "chases" "bald eagle" "+")) -> ("bald eagle" "sees" "lion" "+"))
If the bald eagle is big and the bald eagle sees the cow then the bald eagle does not chase the lion.
((("bald eagle" "is" "big" "+") ("bald eagle" "sees" "cow" "+")) -> ("bald eagle" "chases" "lion" "-"))
If something sees the cow then the cow chases the bald eagle.
((("something" "sees" "cow" "+")) -> ("cow" "chases" "bald eagle" "+"))
If something is big then it sees the cat.
((("something" "is" "big" "+")) -> ("something" "sees" "cat" "+"))
If something sees the lion and the lion visits the bald eagle then it is not nice.
((("something" "sees" "lion" "+") ("lion" "visits" "bald eagle" "+")) -> ("something" "is" "nice" "-"))
The bald eagle sees the lion.
True
1
proof
[(triple4 OR ((((triple3) -> rule4)) -> rule2))]
("bald eagle" "sees" "lion" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
int2
The bald eagle does not chase the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "cow" "-")
triple1
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The bald eagle chases the cow.[(triple1)] The bald eagle is not round.[(triple2)] The bald eagle sees the cow.[(triple3)] The bald eagle sees the lion.[(triple4 OR ((((triple3) -> rule4)) -> rule2))] The cat sees the lion.[(triple5)] The cow is blue.[(triple6)] The lion sees the cat.[(triple7)] @1: The cow chases the bald eagle.[(((triple3) -> rule4))]
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
triple1
The bald eagle is not round.
("bald eagle" "is" "round" "-")
triple2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
triple3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
int2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
((triple3) -> (rule4 % int1))
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
int1