The bald eagle is big. The cow eats the bald eagle. The lion chases the bald eagle. If someone sees the lion then they eat the cow. If someone sees the lion and the lion chases the cow then they are green. If someone sees the lion then they are red. If the cow chases the bald eagle then the bald eagle sees the lion. If someone eats the bald eagle then they eat the lion. If someone chases the cow then they see the cow. If the lion eats the bald eagle then the lion sees the cow. Red people are cold.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
If someone sees the lion then they eat the cow.
((("someone" "sees" "lion" "+")) -> ("someone" "eats" "cow" "+"))
If someone sees the lion and the lion chases the cow then they are green.
((("someone" "sees" "lion" "+") ("lion" "chases" "cow" "+")) -> ("someone" "is" "green" "+"))
If someone sees the lion then they are red.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "red" "+"))
If the cow chases the bald eagle then the bald eagle sees the lion.
((("cow" "chases" "bald eagle" "+")) -> ("bald eagle" "sees" "lion" "+"))
If someone eats the bald eagle then they eat the lion.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "eats" "lion" "+"))
If someone chases the cow then they see the cow.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If the lion eats the bald eagle then the lion sees the cow.
((("lion" "eats" "bald eagle" "+")) -> ("lion" "sees" "cow" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
The lion chases the bald eagle.
True
1
proof
[(triple3)]
("lion" "chases" "bald eagle" "+")
triple3
The cow does not eat the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "eats" "bald eagle" "-")
triple2
The cow eats the lion.
True
2
proof
[(((triple2) -> rule5))]
("cow" "eats" "lion" "+")
((triple2) -> (rule5 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "eats" "lion" "-")
((triple2) -> (rule5 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "red" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "lion" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The lion sees the bald eagle.
Unknown
random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "+")
@0: The bald eagle is big.[(triple1)] The cow eats the bald eagle.[(triple2)] The lion chases the bald eagle.[(triple3)] @1: The cow eats the lion.[(((triple2) -> rule5))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
triple2
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple3
The cow eats the lion.
("cow" "eats" "lion" "+")
((triple2) -> (rule5 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1