The bald eagle is red. The bald eagle likes the cat. The bald eagle needs the cat. The bald eagle needs the cow. The bald eagle sees the cat. The cat likes the bald eagle. The cat likes the mouse. The cat needs the cow. The cat needs the mouse. The cat sees the mouse. The cow is blue. The cow is kind. The cow likes the mouse. The cow needs the bald eagle. The mouse is cold. The mouse is kind. If something sees the bald eagle and it is blue then it sees the mouse. If something likes the mouse then it likes the cow. If something likes the cow then it sees the mouse.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If something sees the bald eagle and it is blue then it sees the mouse.
((("something" "sees" "bald eagle" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "mouse" "+"))
If something likes the mouse then it likes the cow.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cow then it sees the mouse.
((("something" "likes" "cow" "+")) -> ("something" "sees" "mouse" "+"))
The cow needs the bald eagle.
True
1
proof
[(triple14)]
("cow" "needs" "bald eagle" "+")
triple14
The cat does not need the cow.
False
1
inv-proof
[(triple8)]
("cat" "needs" "cow" "-")
triple8
The cow likes the cow.
True
2
proof
[(((triple13) -> rule2))]
("cow" "likes" "cow" "+")
((triple13) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple13) -> rule2))]
("cow" "likes" "cow" "-")
((triple13) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the mouse.
True
3
proof
[(((((triple13) -> rule2)) -> rule3))]
("cow" "sees" "mouse" "+")
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not see the mouse.
False
3
inv-proof
[(((((triple13) -> rule2)) -> rule3))]
("cow" "sees" "mouse" "-")
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The bald eagle does not see the mouse.
Unknown
inv-rconc
[@2: The bald eagle sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("bald eagle" "sees" "mouse" "-")
The bald eagle likes the cow.
Unknown
rconc
[@1: The bald eagle likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "cow" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@2: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The mouse does not like the cat.
Unknown
inv-random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "-")
The cow sees the bald eagle.
Unknown
random
[@0: The cow sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bald eagle" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle likes the cat.[(triple2)] The bald eagle needs the cat.[(triple3)] The bald eagle needs the cow.[(triple4)] The bald eagle sees the cat.[(triple5)] The cat likes the bald eagle.[(triple6)] The cat likes the mouse.[(triple7)] The cat needs the cow.[(triple8)] The cat needs the mouse.[(triple9)] The cat sees the mouse.[(triple10 OR ((((triple7) -> rule2)) -> rule3))] The cow is blue.[(triple11)] The cow is kind.[(triple12)] The cow likes the mouse.[(triple13)] The cow needs the bald eagle.[(triple14)] The mouse is cold.[(triple15)] The mouse is kind.[(triple16)] @1: The cat likes the cow.[(((triple7) -> rule2))] The cow likes the cow.[(((triple13) -> rule2))] @2: The cow sees the mouse.[(((((triple13) -> rule2)) -> rule3))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple3
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
triple4
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple5
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple6
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple7
The cat needs the cow.
("cat" "needs" "cow" "+")
triple8
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple9
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple10
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
triple11
The cow is kind.
("cow" "is" "kind" "+")
triple12
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple13
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple14
The mouse is cold.
("mouse" "is" "cold" "+")
triple15
The mouse is kind.
("mouse" "is" "kind" "+")
triple16
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple7) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple13) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2