The bald eagle visits the mouse. The cow visits the dog. The dog is green. The mouse is green. If something visits the mouse then it likes the cow. If something likes the cow then the cow sees the mouse. If something is big and it likes the bald eagle then the bald eagle is green.
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The mouse is green.
("mouse" "is" "green" "+")
If something visits the mouse then it likes the cow.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cow then the cow sees the mouse.
((("something" "likes" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something is big and it likes the bald eagle then the bald eagle is green.
((("something" "is" "big" "+") ("something" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "green" "+"))
The dog is green.
True
1
proof
[(triple3)]
("dog" "is" "green" "+")
triple3
The bald eagle does not visit the mouse.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "mouse" "-")
triple1
The bald eagle likes the cow.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The bald eagle does not like the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("bald eagle" "likes" "cow" "-")
((triple1) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cow sees the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("cow" "sees" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow does not see the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("cow" "sees" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The bald eagle is not green.
Unknown
inv-rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "is" "green" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "+")
The mouse does not like the cow.
Unknown
inv-rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow does not see the dog.
Unknown
inv-random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The bald eagle visits the mouse.[(triple1)] The cow visits the dog.[(triple2)] The dog is green.[(triple3)] The mouse is green.[(triple4)] @1: The bald eagle likes the cow.[(((triple1) -> rule1))] @2: The cow sees the mouse.[(((((triple1) -> rule1)) -> rule2))]
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
triple1
The cow visits the dog.
("cow" "visits" "dog" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2