The bald eagle is rough. The bald eagle likes the cat. The bald eagle sees the cat. The cat is blue. The cow likes the lion. The cow sees the bald eagle. The cow sees the lion. The lion likes the cat. The lion sees the bald eagle. The lion sees the cow. If the lion likes the cow and the lion is rough then the lion sees the cow. If something likes the cat then the cat sees the lion. If something likes the cat then it is green.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If the lion likes the cow and the lion is rough then the lion sees the cow.
((("lion" "likes" "cow" "+") ("lion" "is" "rough" "+")) -> ("lion" "sees" "cow" "+"))
If something likes the cat then the cat sees the lion.
((("something" "likes" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If something likes the cat then it is green.
((("something" "likes" "cat" "+")) -> ("something" "is" "green" "+"))
The cow sees the bald eagle.
True
1
proof
[(triple6)]
("cow" "sees" "bald eagle" "+")
triple6
The lion does not like the cat.
False
1
inv-proof
[(triple8)]
("lion" "likes" "cat" "-")
triple8
The bald eagle is green.
True
2
proof
[(((triple2) -> rule3))]
("bald eagle" "is" "green" "+")
((triple2) -> (rule3 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The cat does not see the lion.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple8) -> rule2))]
("cat" "sees" "lion" "-")
((triple2) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
((triple8) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "green" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "green" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The cow visits the lion.
Unknown
random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle likes the cat.[(triple2)] The bald eagle sees the cat.[(triple3)] The cat is blue.[(triple4)] The cow likes the lion.[(triple5)] The cow sees the bald eagle.[(triple6)] The cow sees the lion.[(triple7)] The lion likes the cat.[(triple8)] The lion sees the bald eagle.[(triple9)] The lion sees the cow.[(triple10)] @1: The bald eagle is green.[(((triple2) -> rule3))] The cat sees the lion.[(((triple2) -> rule2) OR ((triple8) -> rule2))] The lion is green.[(((triple8) -> rule3))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cow likes the lion.
("cow" "likes" "lion" "+")
triple5
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple6
The cow sees the lion.
("cow" "sees" "lion" "+")
triple7
The lion likes the cat.
("lion" "likes" "cat" "+")
triple8
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The bald eagle is green.
("bald eagle" "is" "green" "+")
((triple2) -> (rule3 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple2) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
((triple8) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((triple8) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1