The bald eagle chases the rabbit. The lion chases the bald eagle. The mouse is rough. The rabbit chases the bald eagle. Young things are rough. If something is nice then it likes the bald eagle. All rough things are blue. If something is rough and it likes the lion then the lion sees the bald eagle. If something sees the bald eagle then the bald eagle chases the rabbit. If something likes the lion and the lion likes the bald eagle then it sees the rabbit.
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it likes the bald eagle.
((("something" "is" "nice" "+")) -> ("something" "likes" "bald eagle" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is rough and it likes the lion then the lion sees the bald eagle.
((("something" "is" "rough" "+") ("something" "likes" "lion" "+")) -> ("lion" "sees" "bald eagle" "+"))
If something sees the bald eagle then the bald eagle chases the rabbit.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "chases" "rabbit" "+"))
If something likes the lion and the lion likes the bald eagle then it sees the rabbit.
((("something" "likes" "lion" "+") ("lion" "likes" "bald eagle" "+")) -> ("something" "sees" "rabbit" "+"))
The lion chases the bald eagle.
True
1
proof
[(triple2)]
("lion" "chases" "bald eagle" "+")
triple2
The lion does not chase the bald eagle.
False
1
inv-proof
[(triple2)]
("lion" "chases" "bald eagle" "-")
triple2
The lion does not see the rabbit.
Unknown
inv-rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "rabbit" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
@0: The bald eagle chases the rabbit.[(triple1)] The lion chases the bald eagle.[(triple2)] The mouse is rough.[(triple3)] The rabbit chases the bald eagle.[(triple4)] @1: The mouse is blue.[(((triple3) -> rule3))]
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
triple1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1